This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

Strong_Relations.thy 1.33 KB
Newer Older
benkeks committed
1 2 3
section \<open>Notions of Equivalence\<close>

subsection \<open>Strong Simulation and Bisimulation\<close>
4 5 6 7 8 9 10 11 12

theory Strong_Relations
  imports Transition_Systems
begin

context lts
begin
  
definition simulation :: 
benkeks committed
13
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
14
where
benkeks committed
15 16 17
  \<open>simulation R \<equiv> \<forall> p q. R p q \<longrightarrow> 
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow> 
      (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q')))\<close>
18 19
  
definition bisimulation :: 
benkeks committed
20
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
21
where
benkeks committed
22 23 24 25 26 27
  \<open>bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow> 
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow> 
      (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))) \<and>
    (\<forall> q' a. q \<longmapsto>a q' \<longrightarrow> 
      (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p')))\<close>

28
lemma bisim_ruleformat:
benkeks committed
29 30 31 32 33
  assumes \<open>bisimulation R\<close>
    and \<open>R p q\<close>
  shows
    \<open>p \<longmapsto>a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))\<close>
    \<open>q \<longmapsto>a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p'))\<close>
34
  using assms unfolding bisimulation_def by auto
benkeks committed
35

benkeks committed
36
end \<comment>\<open>context lts\<close>
37 38 39

end