diff --git a/thys/VeriComp/Compiler.thy b/thys/VeriComp/Compiler.thy
--- a/thys/VeriComp/Compiler.thy
+++ b/thys/VeriComp/Compiler.thy
@@ -1,157 +1,157 @@
 section \<open>Compiler Between Static Representations\<close>
 
 theory Compiler
   imports Language Simulation
 begin
 
 definition option_comp :: "('a \<Rightarrow> 'b option) \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> 'c \<Rightarrow> 'b option" (infix "\<Lleftarrow>" 50) where
   "(f \<Lleftarrow> g) x \<equiv> Option.bind (g x) f"
 
 context
   fixes f :: "('a \<Rightarrow> 'a option)"
 begin
 
 fun option_comp_pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a option" where
   "option_comp_pow 0 = (\<lambda>_. None)" |
   "option_comp_pow (Suc 0) = f" |
   "option_comp_pow (Suc n) = (option_comp_pow n \<Lleftarrow> f)"
 
 end
 
 locale compiler =
   L1: language step1 final1 load1 +
   L2: language step2 final2 load2 +
   backward_simulation step1 step2 final1 final2 order match
   for
     step1 and step2 and
     final1 and final2 and
     load1 :: "'prog1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     load2 :: "'prog2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" and
     match +
   fixes
     compile :: "'prog1 \<Rightarrow> 'prog2 option"
   assumes
     compile_load:
       "compile p1 = Some p2 \<Longrightarrow> load2 p2 s2 \<Longrightarrow> \<exists>s1 i. load1 p1 s1 \<and> match i s1 s2"
 begin
 
 text \<open>
 The @{locale compiler} locale relates two languages, L1 and L2, by a backward simulation and provides a @{term compile} partial function from a concrete program in L1 to a concrete program in L2.
 The only assumption is that a successful compilation results in a program which, when loaded, is equivalent to the loaded initial program.
 \<close>
 
 
 subsection \<open>Preservation of behaviour\<close>
 
 corollary behaviour_preservation:
   assumes
     compiles: "compile p1 = Some p2" and
-    behaves: "L2.behaves p2 b2" and
+    behaves: "L2.prog_behaves p2 b2" and
     not_wrong: "\<not> is_wrong b2"
-  shows "\<exists>b1 i.  L1.behaves p1 b1 \<and> rel_behaviour (match i) b1 b2"
+  shows "\<exists>b1 i.  L1.prog_behaves p1 b1 \<and> rel_behaviour (match i) b1 b2"
 proof -
-  obtain s2 where "load2 p2 s2" and "L2.sem_behaves s2 b2"
-    using behaves L2.behaves_def by auto
+  obtain s2 where "load2 p2 s2" and "L2.state_behaves s2 b2"
+    using behaves L2.prog_behaves_def by auto
   obtain i s1 where "load1 p1 s1" "match i s1 s2"
     using compile_load[OF compiles \<open>load2 p2 s2\<close>]
     by auto
   then show ?thesis
-    using simulation_behaviour[OF \<open>L2.sem_behaves s2 b2\<close> not_wrong \<open>match i s1 s2\<close>]
-    by (auto simp: L1.behaves_def)
+    using simulation_behaviour[OF \<open>L2.state_behaves s2 b2\<close> not_wrong \<open>match i s1 s2\<close>]
+    by (auto simp: L1.prog_behaves_def)
 qed
 
 end
 
 subsection \<open>Composition of compilers\<close>
 
 lemma compiler_composition:
   assumes
     "compiler step1 step2 final1 final2 load1 load2 order1 match1 compile1" and
     "compiler step2 step3 final2 final3 load2 load3 order2 match2 compile2"
   shows "compiler step1 step3 final1 final3 load1 load3
     (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2) (compile2 \<Lleftarrow> compile1)"
 proof (rule compiler.intro) 
   show "language step1 final1"
     using assms(1)[THEN compiler.axioms(1)] .
 next
   show "language step3 final3"
     using assms(2)[THEN compiler.axioms(2)] .
 next
   show "backward_simulation step1 step3 final1 final3
      (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)"
     using backward_simulation_composition[OF assms[THEN compiler.axioms(3)]] .
 next
   show "compiler_axioms load1 load3 (rel_comp match1 match2) (compile2 \<Lleftarrow> compile1)"
   proof unfold_locales
     fix p1 p3 s3
     assume
       compile: "(compile2 \<Lleftarrow> compile1) p1 = Some p3" and
       load: "load3 p3 s3"
     obtain p2 where c1: "compile1 p1 = Some p2" and c2: "compile2 p2 = Some p3"
       using compile by (auto simp: bind_eq_Some_conv option_comp_def)
     obtain s2 i' where l2: "load2 p2 s2" and "match2 i' s2 s3"
       using assms(2)[THEN compiler.compile_load, OF c2 load]
       by auto
     moreover obtain s1 i where "load1 p1 s1" and "match1 i s1 s2"
       using assms(1)[THEN compiler.compile_load, OF c1 l2]
       by auto
     ultimately show "\<exists>s1 i. load1 p1 s1 \<and> rel_comp match1 match2 i s1 s3"
       unfolding rel_comp_def by auto
   qed
 qed
 
 lemma compiler_composition_pow:
   assumes
     "compiler step step final final load load order match compile"
   shows "compiler step step final final load load
     (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match) (option_comp_pow compile n)"
 proof (induction n rule: option_comp_pow.induct)
   case 1
   show ?case
     using assms
     by (auto intro: compiler.axioms compiler.intro compiler_axioms.intro backward_simulation_pow)
 next
   case 2
   show ?case
   proof (rule compiler.intro)
     show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc 0))"
     proof unfold_locales
       fix p1 p2 s2
       assume
         "option_comp_pow compile (Suc 0) p1 = Some p2" and
         "load p2 s2"
       thus "\<exists>s1 i. load p1 s1 \<and> rel_comp_pow match i s1 s2"
         using compiler.compile_load[OF assms(1)]
         by (metis option_comp_pow.simps(2) rel_comp_pow.simps(2))
     qed
   qed (auto intro: assms compiler.axioms backward_simulation_pow)
 next
   case (3 n')
   show ?case
   proof (rule compiler.intro)
     show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc (Suc n')))"
     proof unfold_locales
       fix p1 p3 s3
       assume
         "option_comp_pow compile  (Suc (Suc n')) p1 = Some p3" and
         "load p3 s3"
       then obtain p2 where
         comp: "compile p1 = Some p2" and
         comp_IH: "option_comp_pow compile (Suc n') p2 = Some p3"
         by (auto simp: option_comp_def bind_eq_Some_conv)
       obtain s2 i' where "load p2 s2" and "rel_comp_pow match i' s2 s3"
         using compiler.compile_load[OF "3.IH" comp_IH \<open>load p3 s3\<close>]
         by auto
       moreover obtain s1 i where "load p1 s1" and "match i s1 s2"
         using compiler.compile_load[OF assms comp \<open>load p2 s2\<close>]
         by auto
       moreover have "rel_comp_pow match (i # i') s1 s3"
         using \<open>rel_comp_pow match i' s2 s3\<close> \<open>match i s1 s2\<close> rel_comp_pow.elims(2) by fastforce
       ultimately show "\<exists>s1 i. load p1 s1 \<and> rel_comp_pow match i s1 s3"
         by blast
     qed
   qed (auto intro: assms compiler.axioms backward_simulation_pow)
 qed
 
 end
\ No newline at end of file
diff --git a/thys/VeriComp/Inf.thy b/thys/VeriComp/Inf.thy
--- a/thys/VeriComp/Inf.thy
+++ b/thys/VeriComp/Inf.thy
@@ -1,59 +1,58 @@
 section \<open>Infinitely Transitive Closure\<close>
 
 theory Inf
   imports Well_founded
 begin
 
 coinductive inf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" for r where
   inf_step: "r x y \<Longrightarrow> inf r y \<Longrightarrow> inf r x"
 
 coinductive inf_wf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" for r order where
   inf_wf: "order n m \<Longrightarrow> inf_wf r order n x \<Longrightarrow> inf_wf r order m x" |
   inf_wf_step: "r\<^sup>+\<^sup>+ x y \<Longrightarrow> inf_wf r order n y \<Longrightarrow> inf_wf r order m x"
 
 lemma inf_wf_to_step_inf_wf:
   assumes "well_founded order"
   shows "inf_wf r order n x \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y"
 proof (induction n arbitrary: x rule: well_founded.induct[OF assms(1)])
   case (1 n)
   from "1.prems"(1) show ?case
   proof (induction rule: inf_wf.cases)
     case (inf_wf m n' x')
     then show ?case using "1.IH" by simp
   next
     case (inf_wf_step x' y m n')
     then show ?case
       by (metis converse_tranclpE inf_wf.inf_wf_step)
   qed
 qed
 
 lemma inf_wf_to_inf:
   assumes "well_founded order"
   shows "inf_wf r order n x \<Longrightarrow> inf r x"
 proof (coinduction arbitrary: x n rule: inf.coinduct)
   case (inf x n)
   then obtain y m where "r x y" and "inf_wf r order m y"
     using inf_wf_to_step_inf_wf[OF assms(1) inf(1)] by metis
   thus ?case by auto
 qed
 
 lemma step_inf:
-  assumes
-    deterministic: "\<And>x y z. r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
+  assumes "right_unique r"
   shows "r x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
-  by (metis deterministic inf.cases)
+  using right_uniqueD[OF \<open>right_unique r\<close>]
+  by (metis inf.cases)
 
 lemma star_inf:
-  assumes
-    deterministic: "\<And>x y z. r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
+  assumes "right_unique r"
   shows "r\<^sup>*\<^sup>* x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
 proof (induction y rule: rtranclp_induct)
   case base
-  then show ?case .
+  then show ?case by assumption
 next
   case (step y z)
   then show ?case
-    using step_inf deterministic by metis
+    using step_inf[OF \<open>right_unique r\<close>] by metis
 qed
 
 end
\ No newline at end of file
diff --git a/thys/VeriComp/Language.thy b/thys/VeriComp/Language.thy
--- a/thys/VeriComp/Language.thy
+++ b/thys/VeriComp/Language.thy
@@ -1,48 +1,41 @@
 section \<open>The Static Representation of a Language\<close>
 
 theory Language
   imports Semantics
 begin
 
 locale language =
   semantics step final
   for
     step :: "'state \<Rightarrow> 'state \<Rightarrow> bool" and
     final :: "'state \<Rightarrow> bool" +
   fixes
     load :: "'prog \<Rightarrow> 'state \<Rightarrow> bool"
 
 context language begin
 
 text \<open>
 The language locale represents the concrete program representation (type variable @{typ 'prog}), which can be transformed into a program state (type variable @{typ 'state}) by the @{term load } function.
 The set of initial states of the transition system is implicitly defined by the codomain of @{term load}.
 \<close>
 
 
-subsection \<open>Behaviour of a dynamic execution\<close>
+subsection \<open>Program behaviour\<close>
 
-definition behaves :: "'prog \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
-  "behaves = load OO sem_behaves"
+definition prog_behaves :: "'prog \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
+  "prog_behaves = load OO state_behaves"
 
 text \<open>If both the @{term load} and @{term step} relations are deterministic, then so is the behaviour of a program.\<close>
 
-lemma behaves_deterministic:
+lemma right_unique_prog_behaves:
   assumes
-    load_deterministic: "\<And>p s s'. load p s \<Longrightarrow> load p s' \<Longrightarrow> s = s'" and
-    step_deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z" and
-    behaves: "p \<Down> b" "p \<Down> b'"
-  shows "b = b'"
-proof -
-  obtain s where "load p s" and "s \<down> b" and "s \<down> b'"
-    using behaves load_deterministic
-    by (auto simp: behaves_def)
-
-  thus ?thesis
-    using step_deterministic sem_behaves_deterministic[OF _ \<open>s \<down> b\<close> \<open>s \<down> b'\<close>]
-    by simp
-qed
+    right_unique_load: "right_unique load" and
+    right_unique_step: "right_unique step"
+  shows "right_unique prog_behaves"
+  unfolding prog_behaves_def
+  using right_unique_state_behaves[OF right_unique_step] right_unique_load
+  by (auto intro: right_unique_OO)
 
 end
 
 end
\ No newline at end of file
diff --git a/thys/VeriComp/Semantics.thy b/thys/VeriComp/Semantics.thy
--- a/thys/VeriComp/Semantics.thy
+++ b/thys/VeriComp/Semantics.thy
@@ -1,138 +1,142 @@
 section \<open>The Dynamic Representation of a Language\<close>
 
 theory Semantics
-  imports Main Behaviour Inf begin
+  imports Main Behaviour Inf Transfer_Extras begin
 
 text \<open>
 The definition of programming languages is separated into two parts: an abstract semantics and a concrete program representation.
 \<close>
 
 definition finished :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
   "finished r x = (\<nexists>y. r x y)"
 
 lemma finished_star:
   assumes "finished r x"
   shows "r\<^sup>*\<^sup>* x y \<Longrightarrow> x = y"
 proof (induction y rule: rtranclp_induct)
   case base
   then show ?case by simp
 next
   case (step y z)
   then show ?case
     using assms by (auto simp: finished_def)
 qed
 
 locale semantics =
   fixes
     step :: "'state \<Rightarrow> 'state \<Rightarrow> bool" (infix "\<rightarrow>" 50) and
     final :: "'state \<Rightarrow> bool"
   assumes
     final_finished: "final s \<Longrightarrow> finished step s"
 begin
 
 text \<open>
 The semantics locale represents the semantics as an abstract machine.
 It is expressed by a transition system with a transition relation @{term step}---usually written as an infix @{text \<rightarrow>} arrow---and final states @{term final}.
 \<close>
 
 lemma finished_step:
   "step s s' \<Longrightarrow> \<not>finished step s"
 by (auto simp add: finished_def)
 
 abbreviation eval :: "'state \<Rightarrow> 'state \<Rightarrow> bool" (infix "\<rightarrow>\<^sup>*" 50) where
   "eval \<equiv> step\<^sup>*\<^sup>*"
 
 abbreviation inf_step :: "'state \<Rightarrow> bool" where
   "inf_step \<equiv> inf step"
 
 notation
   inf_step ("'(\<rightarrow>\<^sup>\<infinity>')" [] 50) and
   inf_step ("_ \<rightarrow>\<^sup>\<infinity>" [55] 50)
 
-lemma finished_inf: "s \<rightarrow>\<^sup>\<infinity> \<Longrightarrow> \<not> finished step s"
+lemma inf_not_finished: "s \<rightarrow>\<^sup>\<infinity> \<Longrightarrow> \<not> finished step s"
   using inf.cases finished_step by metis
 
 lemma eval_deterministic:
   assumes
-    deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z"
-  shows "s1 \<rightarrow>\<^sup>* s2 \<Longrightarrow> s1 \<rightarrow>\<^sup>* s3 \<Longrightarrow> finished step s2 \<Longrightarrow> finished step s3 \<Longrightarrow> s2 = s3"
-proof(induction s1 arbitrary: s3 rule: converse_rtranclp_induct)
-  case base
-  then show ?case by (simp add: finished_star)
-next
-  case (step y z)
-  then show ?case
-    by (metis converse_rtranclpE deterministic finished_step)
+    deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z" and
+    "s1 \<rightarrow>\<^sup>* s2" and "s1 \<rightarrow>\<^sup>* s3" and "finished step s2" and "finished step s3"
+  shows "s2 = s3"
+proof -
+  have "right_unique step"
+    using deterministic by (auto intro: right_uniqueI)
+  with assms show ?thesis
+    by (auto simp: finished_def intro: rtranclp_complete_run_right_unique)
 qed
 
+lemma step_converges_or_diverges: "(\<exists>s'. s \<rightarrow>\<^sup>* s' \<and> finished step s') \<or> s \<rightarrow>\<^sup>\<infinity>"
+  by (smt (verit, del_insts) finished_def inf.coinduct rtranclp.intros(2) rtranclp.rtrancl_refl)
+
 subsection \<open>Behaviour of a dynamic execution\<close>
 
-inductive sem_behaves :: "'state \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<down>" 50) where
+inductive state_behaves :: "'state \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<down>" 50) where
   state_terminates:
     "s1 \<rightarrow>\<^sup>* s2 \<Longrightarrow> finished step s2 \<Longrightarrow> final s2 \<Longrightarrow> s1 \<down> (Terminates s2)" |
   state_diverges:
     "s1 \<rightarrow>\<^sup>\<infinity> \<Longrightarrow> s1 \<down> Diverges" |
   state_goes_wrong:
     "s1 \<rightarrow>\<^sup>* s2 \<Longrightarrow> finished step s2 \<Longrightarrow> \<not> final s2 \<Longrightarrow> s1 \<down> (Goes_wrong s2)"
 
 
 text \<open>
 Even though the @{term step} transition relation in the @{locale semantics} locale need not be deterministic, if it happens to be, then the behaviour of a program becomes deterministic too.
 \<close>
 
-lemma sem_behaves_deterministic:
+lemma right_unique_state_behaves:
   assumes
-    deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z"
-  shows "s \<down> b1 \<Longrightarrow> s \<down> b2 \<Longrightarrow> b1 = b2"
-proof (induction s b1 rule: sem_behaves.induct)
-  case (state_terminates s1 s2)
-  show ?case using state_terminates.prems state_terminates.hyps
-  proof (induction s1 b2 rule: sem_behaves.induct)
-    case (state_terminates s1 s3)
-    then show ?case
-      using eval_deterministic deterministic by simp
-  next
-    case (state_diverges s1)
-    then show ?case
-      using deterministic star_inf[THEN finished_inf] by simp
+    "right_unique (\<rightarrow>)"
+  shows "right_unique (\<down>)"
+proof (rule right_uniqueI)
+  fix s b1 b2
+  assume "s \<down> b1" "s \<down> b2"
+  thus "b1 = b2"
+    by (auto simp: finished_def simp del: not_ex
+        elim!: state_behaves.cases
+        dest: rtranclp_complete_run_right_unique[OF \<open>right_unique (\<rightarrow>)\<close>, of s]
+        dest: final_finished star_inf[OF \<open>right_unique (\<rightarrow>)\<close>, THEN inf_not_finished])
+qed
+
+lemma left_total_state_behaves: "left_total (\<down>)"
+proof (rule left_totalI)
+  fix s
+  show "\<exists>b. s \<down> b"
+    using step_converges_or_diverges[of s]
+  proof (elim disjE exE conjE)
+    fix s'
+    assume "s \<rightarrow>\<^sup>* s'" and "finished (\<rightarrow>) s'"
+    thus "\<exists>b. s \<down> b"
+      by (cases "final s'") (auto intro: state_terminates state_goes_wrong)
   next
-    case (state_goes_wrong s1 s3)
-    then show ?case
-      using eval_deterministic deterministic by blast
-  qed
-next
-  case (state_diverges s1)
-  show ?case using state_diverges.prems state_diverges.hyps
-  proof (induction s1 b2 rule: sem_behaves.induct)
-    case (state_terminates s1 s2)
-    then show ?case
-      using deterministic star_inf[THEN finished_inf] by simp
-  next
-    case (state_diverges s1)
-    then show ?case by simp
-  next
-    case (state_goes_wrong s1 s2)
-    then show ?case
-      using deterministic star_inf[THEN finished_inf] by simp
-  qed
-next
-  case (state_goes_wrong s1 s2)
-  show ?case using state_goes_wrong.prems state_goes_wrong.hyps
-  proof (induction s1 b2 rule: sem_behaves.induct)
-    case (state_terminates s1 s3)
-    then show ?case 
-      using eval_deterministic deterministic by blast
-  next
-    case (state_diverges s1)
-    then show ?case
-      using deterministic star_inf[THEN finished_inf] by simp
-  next
-    case (state_goes_wrong s1 s3)
-    then show ?case
-      using eval_deterministic deterministic by simp
+    assume "s \<rightarrow>\<^sup>\<infinity>"
+    thus "\<exists>b. s \<down> b"
+      by (auto intro: state_diverges)
   qed
 qed
 
+subsection \<open>Safe states\<close>
+
+definition safe where
+  "safe s \<longleftrightarrow> (\<forall>s'. step\<^sup>*\<^sup>* s s' \<longrightarrow> final s' \<or> (\<exists>s''. step s' s''))"
+
+lemma final_safeI: "final s \<Longrightarrow> safe s"
+  by (metis final_finished finished_star safe_def)
+
+lemma step_safe: "step s s' \<Longrightarrow> safe s \<Longrightarrow> safe s'"
+  by (simp add: converse_rtranclp_into_rtranclp safe_def)
+
+lemma steps_safe: "step\<^sup>*\<^sup>* s s' \<Longrightarrow> safe s \<Longrightarrow> safe s'"
+  by (meson rtranclp_trans safe_def)
+
+lemma safe_state_behaves_not_wrong:
+  assumes "safe s" and "s \<down> b"
+  shows "\<not> is_wrong b"
+  using \<open>s \<down> b\<close>
+proof (cases rule: state_behaves.cases)
+  case (state_goes_wrong s2)
+  then show ?thesis
+    using \<open>safe s\<close> by (auto simp: safe_def finished_def)
+qed simp_all
+
 end
 
 end
\ No newline at end of file
diff --git a/thys/VeriComp/Simulation.thy b/thys/VeriComp/Simulation.thy
--- a/thys/VeriComp/Simulation.thy
+++ b/thys/VeriComp/Simulation.thy
@@ -1,445 +1,542 @@
 section \<open>Simulations Between Dynamic Executions\<close>
 
 theory Simulation
   imports Semantics Inf Well_founded
 begin
 
+subsection \<open>Backward simulation\<close>
+
 locale backward_simulation =
   L1: semantics step1 final1 +
   L2: semantics step2 final2 +
   well_founded "(\<sqsubset>)"
   for
     step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     final1 :: "'state1 \<Rightarrow> bool" and
     final2 :: "'state2 \<Rightarrow> bool" and
     order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" (infix "\<sqsubset>" 70) +
   fixes
     match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
   assumes
     match_final:
       "match i s1 s2 \<Longrightarrow> final2 s2 \<Longrightarrow> final1 s1" and
     simulation:
       "match i1 s1 s2 \<Longrightarrow> step2 s2 s2' \<Longrightarrow>
         (\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2') \<or> (\<exists>i2. match i2 s1 s2' \<and> i2 \<sqsubset> i1)"
 begin
 
 text \<open>
 A simulation is defined between two @{locale semantics} L1 and L2.
 A @{term match} predicate expresses that two states from L1 and L2 are equivalent.
 The @{term match} predicate is also parameterized with an ordering used to avoid stuttering.
 The only two assumptions of a backward simulation are that a final state in L2 will also be a final in L1,and that a step in L2 will either represent a non-empty sequence of steps in L1 or will result in an equivalent state.
 Stuttering is ruled out by the requirement that the index on the @{term match} predicate decreases with respect to the well-founded @{term order} ordering.
 \<close>
 
-end
-
-
-locale forward_simulation =
-  L1: semantics step1 final1 +
-  L2: semantics step2 final2 +
-  well_founded "(\<sqsubset>)"
-  for
-    step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
-    step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
-    final1 :: "'state1 \<Rightarrow> bool" and
-    final2 :: "'state2 \<Rightarrow> bool" and
-    order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" (infix "\<sqsubset>" 70) +
-  fixes
-    match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
-  assumes
-    match_final:
-      "match i s1 s2 \<Longrightarrow> final1 s1 \<Longrightarrow> final2 s2" and
-    simulation:
-      "match i1 s1 s2 \<Longrightarrow> step1 s1 s1' \<Longrightarrow>
-        (\<exists>i' s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match i' s1' s2') \<or> (\<exists>i'. match i' s1 s2' \<and> i' \<sqsubset> i1)"
-
-locale bisimulation =
-  forward_simulation step1 step2 final1 final2 order match +
-  backward_simulation step1 step2 final1 final2 order match
-  for
-    step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
-    step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
-    final1 :: "'state1 \<Rightarrow> bool" and
-    final2 :: "'state2 \<Rightarrow> bool" and
-    order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" and
-    match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
-
-context backward_simulation begin
-
 lemma lift_simulation_plus:
   "step2\<^sup>+\<^sup>+ s2 s2' \<Longrightarrow> match i1 s1 s2 \<Longrightarrow>
     (\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2') \<or>
     (\<exists>i2. match i2 s1 s2' \<and> order\<^sup>+\<^sup>+ i2 i1)"
   thm tranclp_induct
 proof(induction s2' arbitrary: i1 s1 rule: tranclp_induct)
   case (base s2')
   from simulation[OF base.prems(1) base.hyps(1)] show ?case
     by auto
 next
   case (step s2' s2'')
   show ?case
     using step.IH[OF \<open>match i1 s1 s2\<close>]
   proof
     assume "\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2'"
     then obtain i2 s1' where "step1\<^sup>+\<^sup>+ s1 s1'" and "match i2 s1' s2'" by auto
     from simulation[OF \<open>match i2 s1' s2'\<close> \<open>step2 s2' s2''\<close>] show ?thesis
     proof
       assume "\<exists>i3 s1''. step1\<^sup>+\<^sup>+ s1' s1'' \<and> match i3 s1'' s2''"
       then obtain i3 s1'' where "step1\<^sup>+\<^sup>+ s1' s1''" and "match i3 s1'' s2''" by auto
       then show ?thesis
         using tranclp_trans[OF \<open>step1\<^sup>+\<^sup>+ s1 s1'\<close>] by auto
     next
       assume "\<exists>i3. match i3 s1' s2'' \<and> i3 \<sqsubset> i2"
       then obtain i3 where "match i3 s1' s2''" and "i3 \<sqsubset> i2" by auto
       then show ?thesis
         using \<open>step1\<^sup>+\<^sup>+ s1 s1'\<close> by auto
     qed
   next
     assume "\<exists>i2. match i2 s1 s2' \<and> (\<sqsubset>)\<^sup>+\<^sup>+ i2 i1"
     then obtain i3 where "match i3 s1 s2'" and "(\<sqsubset>)\<^sup>+\<^sup>+ i3 i1" by auto
     then show ?thesis
       using simulation[OF \<open>match i3 s1 s2'\<close> \<open>step2 s2' s2''\<close>] by auto
   qed
 qed
 
 lemma lift_simulation_eval:
   "L2.eval s2 s2' \<Longrightarrow> match i1 s1 s2 \<Longrightarrow> \<exists>i2 s1'. L1.eval s1 s1' \<and> match i2 s1' s2'"
 proof(induction s2 arbitrary: i1 s1 rule: converse_rtranclp_induct)
   case (base s2)
   thus ?case by auto
 next
   case (step s2 s2'')
   from simulation[OF \<open>match i1 s1 s2\<close> \<open>step2 s2 s2''\<close>] show ?case
   proof
     assume "\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2''"
     thus ?thesis
       by (meson rtranclp_trans step.IH tranclp_into_rtranclp)
   next
     assume "\<exists>i2. match i2 s1 s2'' \<and> i2 \<sqsubset> i1"
     thus ?thesis
       by (auto intro: step.IH)
   qed
 qed
 
-lemma backward_simulation_inf:
+lemma match_inf:
   assumes
     "match i s1 s2" and
     "inf step2 s2"
   shows "inf step1 s1"
 proof -
   from assms have "inf_wf step1 order i s1"
   proof (coinduction arbitrary: i s1 s2)
     case inf_wf
     obtain s2' where "step2 s2 s2'" and "inf step2 s2'"
       using inf_wf(2) by (auto elim: inf.cases)
     from simulation[OF \<open>match i s1 s2\<close> \<open>step2 s2 s2'\<close>] show ?case
       using \<open>inf step2 s2'\<close> by auto
   qed
   thus ?thesis using inf_wf_to_inf
     by (auto intro: inf_wf_to_inf well_founded_axioms)
 qed
 
-subsection \<open>Preservation of behaviour\<close>
+subsubsection \<open>Preservation of behaviour\<close>
 
 text \<open>
 The main correctness theorem states that, for any two matching programs, any not wrong behaviour of the later is also a behaviour of the former.
 In other words, if the compiled program does not crash, then its behaviour, whether it terminates or not, is a also a valid behaviour of the source program.
 \<close>
 
 lemma simulation_behaviour :
-  "L2.sem_behaves s\<^sub>2 b\<^sub>2 \<Longrightarrow> \<not>is_wrong b\<^sub>2 \<Longrightarrow> match i s\<^sub>1 s\<^sub>2 \<Longrightarrow>
-    \<exists>b\<^sub>1 i'. L1.sem_behaves s\<^sub>1 b\<^sub>1 \<and> rel_behaviour (match i') b\<^sub>1 b\<^sub>2"
-proof(induction rule: L2.sem_behaves.cases)
+  "L2.state_behaves s\<^sub>2 b\<^sub>2 \<Longrightarrow> \<not>is_wrong b\<^sub>2 \<Longrightarrow> match i s\<^sub>1 s\<^sub>2 \<Longrightarrow>
+    \<exists>b\<^sub>1 i'. L1.state_behaves s\<^sub>1 b\<^sub>1 \<and> rel_behaviour (match i') b\<^sub>1 b\<^sub>2"
+proof(induction rule: L2.state_behaves.cases)
   case (state_terminates s2 s2')
   then obtain i' s1' where "L1.eval s\<^sub>1 s1'" and "match i' s1' s2'"
     using lift_simulation_eval by blast
   hence "final1 s1'"
     by (auto intro: state_terminates.hyps match_final)
-  hence "L1.sem_behaves s\<^sub>1 (Terminates s1')"
+  hence "L1.state_behaves s\<^sub>1 (Terminates s1')"
     using L1.final_finished
     by (simp add: L1.state_terminates \<open>L1.eval s\<^sub>1 s1'\<close>)
   moreover have "rel_behaviour (match i') (Terminates s1') b\<^sub>2"
     by (simp add: \<open>match i' s1' s2'\<close> state_terminates.hyps)
   ultimately show ?case by blast
 next
   case (state_diverges s2)
   then show ?case
-    using backward_simulation_inf L1.state_diverges by fastforce
+    using match_inf L1.state_diverges by fastforce
 next
   case (state_goes_wrong s2 s2')
   then show ?case using \<open>\<not>is_wrong b\<^sub>2\<close> by simp
 qed
 
 end
 
+subsection \<open>Forward simulation\<close>
+
+locale forward_simulation =
+  L1: semantics step1 final1 +
+  L2: semantics step2 final2 +
+  well_founded "(\<sqsubset>)"
+  for
+    step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
+    step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
+    final1 :: "'state1 \<Rightarrow> bool" and
+    final2 :: "'state2 \<Rightarrow> bool" and
+    order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" (infix "\<sqsubset>" 70) +
+  fixes
+    match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
+  assumes
+    match_final:
+      "match i s1 s2 \<Longrightarrow> final1 s1 \<Longrightarrow> final2 s2" and
+    simulation:
+      "match i s1 s2 \<Longrightarrow> step1 s1 s1' \<Longrightarrow>
+        (\<exists>i' s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match i' s1' s2') \<or> (\<exists>i'. match i' s1' s2 \<and> i' \<sqsubset> i)"
+begin
+
+lemma lift_simulation_eval:
+  "L1.eval s1 s1' \<Longrightarrow> match i s1 s2 \<Longrightarrow> \<exists>i' s2'. L2.eval s2 s2' \<and> match i' s1' s2'"
+proof(induction s1 arbitrary: i s2 rule: converse_rtranclp_induct)
+  case (base s2)
+  thus ?case by auto
+next
+  case (step s1 s1'')
+  show ?case
+    using simulation[OF \<open>match i s1 s2\<close> \<open>step1 s1 s1''\<close>]
+  proof (elim disjE exE conjE)
+    fix i' s2'
+    assume "step2\<^sup>+\<^sup>+ s2 s2'" and "match i' s1'' s2'"
+    thus ?thesis
+      by (auto intro: rtranclp_trans dest!: tranclp_into_rtranclp step.IH)
+  next
+    fix i'
+    assume "match i' s1'' s2" and "i' \<sqsubset> i"
+    thus ?thesis
+      by (auto intro: step.IH)
+  qed
+qed
+
+lemma match_inf:
+  assumes "match i s1 s2" and "inf step1 s1"
+  shows "inf step2 s2"
+proof -
+  from assms have "inf_wf step2 order i s2"
+  proof (coinduction arbitrary: i s1 s2)
+    case inf_wf
+    obtain s1' where step_s1: "step1 s1 s1'" and inf_s1': "inf step1 s1'"
+      using inf_wf(2) by (auto elim: inf.cases)
+    from simulation[OF \<open>match i s1 s2\<close> step_s1] show ?case
+      using inf_s1' by auto
+  qed
+  thus ?thesis using inf_wf_to_inf
+    by (auto intro: inf_wf_to_inf well_founded_axioms)
+qed
+
+
+subsubsection \<open>Preservation of behaviour\<close>
+
+lemma simulation_behaviour :
+  "L1.state_behaves s1 b1 \<Longrightarrow> \<not> is_wrong b1 \<Longrightarrow> match i s1 s2 \<Longrightarrow>
+    \<exists>b2 i'. L2.state_behaves s2 b2 \<and> rel_behaviour (match i') b1 b2"
+proof(induction rule: L1.state_behaves.cases)
+  case (state_terminates s1 s1')
+  then obtain i' s2' where steps_s2: "L2.eval s2 s2'" and match_s1'_s2': "match i' s1' s2'"
+    using lift_simulation_eval by blast
+  hence "final2 s2'"
+    by (auto intro: state_terminates.hyps match_final)
+  hence "L2.state_behaves s2 (Terminates s2')"
+    using L2.final_finished L2.state_terminates[OF steps_s2]
+    by simp
+  moreover have "rel_behaviour (match i') b1 (Terminates s2')"
+    by (simp add: \<open>match i' s1' s2'\<close> state_terminates.hyps)
+  ultimately show ?case by blast
+next
+  case (state_diverges s2)
+  then show ?case
+    using match_inf[THEN L2.state_diverges] by fastforce
+next
+  case (state_goes_wrong s2 s2')
+  then show ?case using \<open>\<not>is_wrong b1\<close> by simp
+qed
+
+
+subsubsection \<open>Forward to backward\<close>
+
+lemma state_behaves_forward_to_backward:
+  assumes
+    match_s1_s2: "match i s1 s2" and
+    safe_s1: "L1.safe s1" and
+    behaves_s2: "L2.state_behaves s2 b2" and
+    right_unique2: "right_unique step2"
+  shows "\<exists>b1 i. L1.state_behaves s1 b1 \<and> rel_behaviour (match i) b1 b2"
+proof -
+  obtain b1 where behaves_s1: "L1.state_behaves s1 b1"
+    using L1.left_total_state_behaves
+    by (auto elim: left_totalE)
+
+  have not_wrong_b1: "\<not> is_wrong b1"
+    by (rule L1.safe_state_behaves_not_wrong[OF safe_s1 behaves_s1])
+
+  obtain i' where "L2.state_behaves s2 b2" and rel_b1_B2: "rel_behaviour (match i') b1 b2"
+    using simulation_behaviour[OF behaves_s1 not_wrong_b1 match_s1_s2]
+    using L2.right_unique_state_behaves[OF right_unique2, THEN right_uniqueD]
+    using behaves_s2
+    by auto
+
+  show ?thesis
+    using behaves_s1 rel_b1_B2 by auto
+qed
+
+end
+
+subsection \<open>Bisimulation\<close>
+
+locale bisimulation =
+  forward_simulation step1 step2 final1 final2 order match +
+  backward_simulation step1 step2 final1 final2 order match
+  for
+    step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
+    step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
+    final1 :: "'state1 \<Rightarrow> bool" and
+    final2 :: "'state2 \<Rightarrow> bool" and
+    order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" and
+    match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
+
 subsection \<open>Composition of backward simulations\<close>
 
 definition rel_comp ::
   "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('d \<Rightarrow> 'c \<Rightarrow> 'e \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'd) \<Rightarrow> 'b \<Rightarrow> 'e \<Rightarrow> bool" where
   "rel_comp r1 r2 i \<equiv> (r1 (fst i) OO r2 (snd i))"
 
 lemma backward_simulation_composition:
   assumes
     "backward_simulation step1 step2 final1 final2 order1 match1"
     "backward_simulation step2 step3 final2 final3 order2 match2"
   shows
     "backward_simulation step1 step3 final1 final3
       (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)"
 proof intro_locales
   show "semantics step1 final1"
     by (auto intro: backward_simulation.axioms assms)
 next
   show "semantics step3 final3"
     by (auto intro: backward_simulation.axioms assms)
 next
   show "well_founded (lex_prodp order1\<^sup>+\<^sup>+ order2)"
     using assms[THEN backward_simulation.axioms(3)]
     by (simp add: lex_prodp_well_founded well_founded.intro well_founded.wf wfP_trancl)
 next
   show "backward_simulation_axioms step1 step3 final1 final3
     (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)"
   proof
     fix i s1 s3
     assume
       match: "rel_comp match1 match2 i s1 s3" and
       final: "final3 s3"
     obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and "i = (i1, i2)"
       using match unfolding rel_comp_def by auto
     thus "final1 s1"
       using final assms[THEN backward_simulation.match_final]
       by simp
   next
     fix i s1 s3 s3'
     assume
       match: "rel_comp match1 match2 i s1 s3" and
       step: "step3 s3 s3'"
     obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and i_def: "i = (i1, i2)"
       using match unfolding rel_comp_def by auto
     from backward_simulation.simulation[OF assms(2) \<open>match2 i2 s2 s3\<close> step]
     show "(\<exists>i' s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> rel_comp match1 match2 i' s1' s3') \<or>
        (\<exists>i'. rel_comp match1 match2 i' s1 s3' \<and> lex_prodp order1\<^sup>+\<^sup>+ order2 i' i)"
       (is "(\<exists>i' s1'. ?STEPS i' s1') \<or> ?STALL")
     proof
       assume "\<exists>i2' s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match2 i2' s2' s3'"
       then obtain i2' s2' where "step2\<^sup>+\<^sup>+ s2 s2'" and "match2 i2' s2' s3'" by auto
       from backward_simulation.lift_simulation_plus[OF assms(1) \<open>step2\<^sup>+\<^sup>+ s2 s2'\<close> \<open>match1 i1 s1 s2\<close>]
       show ?thesis
       proof
         assume "\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match1 i2 s1' s2'"
         then obtain i2 s1' where "step1\<^sup>+\<^sup>+ s1 s1'" and "match1 i2 s1' s2'" by auto
         hence "?STEPS (i2, i2') s1'"
           by (auto intro: \<open>match2 i2' s2' s3'\<close> simp: rel_comp_def)
         thus ?thesis by auto
       next
         assume "\<exists>i2. match1 i2 s1 s2' \<and> order1\<^sup>+\<^sup>+ i2 i1"
         then obtain i2'' where "match1 i2'' s1 s2'" and "order1\<^sup>+\<^sup>+ i2'' i1" by auto
         hence ?STALL
           unfolding rel_comp_def i_def lex_prodp_def
           using \<open>match2 i2' s2' s3'\<close> by auto
         thus ?thesis by simp
       qed
     next
       assume "\<exists>i2'. match2 i2' s2 s3' \<and> order2 i2' i2"
       then obtain i2' where "match2 i2' s2 s3'" and "order2 i2' i2" by auto
       hence ?STALL
         unfolding rel_comp_def i_def lex_prodp_def
         using \<open>match1 i1 s1 s2\<close> by auto
       thus ?thesis by simp
     qed
   qed
 qed
 
 context
   fixes r :: "'i \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 fun rel_comp_pow where
   "rel_comp_pow [] x y = False" |
   "rel_comp_pow [i] x y = r i x y" |
   "rel_comp_pow (i # is) x z = (\<exists>y. r i x y \<and> rel_comp_pow is y z)"
 
 end
 
 lemma backward_simulation_pow:
   assumes
     "backward_simulation step step final final order match"
   shows
     "backward_simulation step step final final (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match)"
 proof intro_locales
   show "semantics step final"
     by (auto intro: backward_simulation.axioms assms)
 next
   show "well_founded (lexp order\<^sup>+\<^sup>+)"
     using backward_simulation.axioms(3)[OF assms] lex_list_well_founded
     using well_founded.intro well_founded.wf wfP_trancl by blast
 next
   show "backward_simulation_axioms step step final final (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match)"
   proof unfold_locales
     fix "is" s1 s2
     assume "rel_comp_pow match is s1 s2" and "final s2"
     thus "final s1" thm rel_comp_pow.induct
     proof (induction "is" s1 s2 rule: rel_comp_pow.induct)
       case (1 x y)
       then show ?case by simp
     next
       case (2 i x y)
       then show ?case
         using backward_simulation.match_final[OF assms(1)] by simp
     next
       case (3 i1 i2 "is" x z)
       from "3.prems"[simplified] obtain y where
         match: "match i1 x y" and "rel_comp_pow match (i2 # is) y z"
         by auto
       hence "final y" using "3.IH" "3.prems" by simp
       thus ?case
         using "3.prems" match backward_simulation.match_final[OF assms(1)] by auto
     qed
   next
     fix "is" s1 s3 s3'
     assume "rel_comp_pow match is s1 s3" and "step s3 s3'"
     hence "(\<exists>is' s1'. step\<^sup>+\<^sup>+ s1 s1' \<and> length is' = length is \<and> rel_comp_pow match is' s1' s3') \<or>
       (\<exists>is'. rel_comp_pow match is' s1 s3' \<and> lexp order\<^sup>+\<^sup>+ is' is)"
     proof (induction "is" s1 s3 arbitrary: s3' rule: rel_comp_pow.induct)
       case 1
       then show ?case by simp
     next
       case (2 i s1 s3)
       from backward_simulation.simulation[OF assms(1) "2.prems"[simplified]] show ?case
       proof
         assume "\<exists>i' s1'. step\<^sup>+\<^sup>+ s1 s1' \<and> match i' s1' s3'"
         then obtain i' s1' where "step\<^sup>+\<^sup>+ s1 s1'" and "match i' s1' s3'" by auto
         hence "step\<^sup>+\<^sup>+ s1 s1' \<and> rel_comp_pow match [i'] s1' s3'" by simp
         thus ?thesis
           by (metis length_Cons)
       next
         assume "\<exists>i'. match i' s1 s3' \<and> order i' i"
         then obtain i' where "match i' s1 s3'" and "order i' i" by auto
         hence "rel_comp_pow match [i'] s1 s3' \<and> lexp order\<^sup>+\<^sup>+ [i'] [i]"
           by (simp add: lexp_head tranclp.r_into_trancl)
         thus ?thesis by blast
       qed
     next
       case (3 i1 i2 "is" s1 s3)
       from "3.prems"[simplified] obtain s2 where
         "match i1 s1 s2" and 0: "rel_comp_pow match (i2 # is) s2 s3"
         by auto
       from "3.IH"[OF 0 "3.prems"(2)] show ?case
       proof
         assume "\<exists>is' s2'. step\<^sup>+\<^sup>+ s2 s2' \<and> length is' = length (i2 # is) \<and>
           rel_comp_pow match is' s2' s3'"
         then obtain i2' is' s2' where
           "step\<^sup>+\<^sup>+ s2 s2'" and "length is' = length is" and "rel_comp_pow match (i2' # is') s2' s3'"
           by (metis Suc_length_conv)
         from backward_simulation.lift_simulation_plus[OF assms(1) \<open>step\<^sup>+\<^sup>+ s2 s2'\<close> \<open>match i1 s1 s2\<close>]
         show ?thesis
         proof
           assume "\<exists>i2 s1'. step\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2'"
           thus ?thesis
             using \<open>rel_comp_pow match (i2' # is') s2' s3'\<close>
             by (metis \<open>length is' = length is\<close> length_Cons rel_comp_pow.simps(3))
         next
           assume "\<exists>i2. match i2 s1 s2' \<and> order\<^sup>+\<^sup>+ i2 i1"
           then obtain i1' where "match i1' s1 s2'" and "order\<^sup>+\<^sup>+ i1' i1" by auto
           hence "rel_comp_pow match (i1' # i2' # is') s1 s3'"
             using \<open>rel_comp_pow match (i2' # is') s2' s3'\<close> by auto
           moreover have "lexp order\<^sup>+\<^sup>+ (i1' # i2' # is') (i1 # i2 # is)"
             using \<open>order\<^sup>+\<^sup>+ i1' i1\<close> \<open>length is' = length is\<close>
             by (auto intro: lexp_head)
           ultimately show ?thesis by fast
         qed
       next
         assume "\<exists>i'. rel_comp_pow match i' s2 s3' \<and> lexp order\<^sup>+\<^sup>+ i' (i2 # is)"
         then obtain i2' is' where
           "rel_comp_pow match (i2' # is') s2 s3'" and "lexp order\<^sup>+\<^sup>+ (i2' # is') (i2 # is)"
           by (metis lexp.simps)
         thus ?thesis
           by (metis \<open>match i1 s1 s2\<close> lexp.simps(1) rel_comp_pow.simps(3))
       qed
     qed
     thus "(\<exists>is' s1'. step\<^sup>+\<^sup>+ s1 s1' \<and> rel_comp_pow match is' s1' s3') \<or>
       (\<exists>is'. rel_comp_pow match is' s1 s3' \<and> lexp order\<^sup>+\<^sup>+ is' is)"
       by auto
   qed
 qed
 
 definition lockstep_backward_simulation where
   "lockstep_backward_simulation step1 step2 match \<equiv>
     \<forall>s1 s2 s2'. match s1 s2 \<longrightarrow> step2 s2 s2' \<longrightarrow> (\<exists>s1'. step1 s1 s1' \<and> match s1' s2')"
 
 definition plus_backward_simulation where
   "plus_backward_simulation step1 step2 match \<equiv>
     \<forall>s1 s2 s2'. match s1 s2 \<longrightarrow> step2 s2 s2' \<longrightarrow> (\<exists>s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match s1' s2')"
 
 lemma
   assumes "lockstep_backward_simulation step1 step2 match"
   shows "plus_backward_simulation step1 step2 match"
 unfolding plus_backward_simulation_def
 proof safe
   fix s1 s2 s2'
   assume "match s1 s2" and "step2 s2 s2'"
   then obtain s1' where "step1 s1 s1'" and "match s1' s2'"
     using assms(1) unfolding lockstep_backward_simulation_def by blast
   then show "\<exists>s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match s1' s2'"
     by auto
 qed
 
 lemma lockstep_to_plus_backward_simulation:
   fixes
     match :: "'state1 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool"
   assumes
     lockstep_simulation: "\<And>s1 s2 s2'. match s1 s2 \<Longrightarrow> step2 s2 s2' \<Longrightarrow> (\<exists>s1'. step1 s1 s1' \<and> match s1' s2')" and
     match: "match s1 s2" and
     step: "step2 s2 s2'"
   shows "\<exists>s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match s1' s2'"
 proof -
   obtain s1' where "step1 s1 s1'" and "match s1' s2'"
     using lockstep_simulation[OF match step] by auto
   thus ?thesis by auto
 qed
 
 lemma lockstep_to_option_backward_simulation:
   fixes
     match :: "'state1 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     measure :: "'state2 \<Rightarrow> nat"
   assumes
     lockstep_simulation: "\<And>s1 s2 s2'. match s1 s2 \<Longrightarrow> step2 s2 s2' \<Longrightarrow> (\<exists>s1'. step1 s1 s1' \<and> match s1' s2')" and
     match: "match s1 s2" and
     step: "step2 s2 s2'"
   shows "(\<exists>s1'. step1 s1 s1' \<and> match s1' s2') \<or> match s1 s2' \<and> measure s2' < measure s2"
   using lockstep_simulation[OF match step] ..
 
 lemma plus_to_star_backward_simulation:
   fixes
     match :: "'state1 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     measure :: "'state2 \<Rightarrow> nat"
   assumes
     star_simulation: "\<And>s1 s2 s2'. match s1 s2 \<Longrightarrow> step2 s2 s2' \<Longrightarrow> (\<exists>s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match s1' s2')" and
     match: "match s1 s2" and
     step: "step2 s2 s2'"
   shows "(\<exists>s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match s1' s2') \<or> match s1 s2' \<and> measure s2' < measure s2"
   using star_simulation[OF match step] ..
 
 lemma lockstep_to_plus_forward_simulation:
   fixes
     match :: "'state1 \<Rightarrow> 'state2 \<Rightarrow> bool" and
     step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
     step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool"
   assumes
     lockstep_simulation: "\<And>s1 s2 s2'. match s1 s2 \<Longrightarrow> step1 s1 s1' \<Longrightarrow> (\<exists>s2'. step2 s2 s2' \<and> match s1' s2')" and
     match: "match s1 s2" and
     step: "step1 s1 s1'"
   shows "\<exists>s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match s1' s2'"
 proof -
   obtain s2' where "step2 s2 s2'" and "match s1' s2'"
     using lockstep_simulation[OF match step] by auto
   thus ?thesis by auto
 qed
 
 end
\ No newline at end of file
diff --git a/thys/VeriComp/Transfer_Extras.thy b/thys/VeriComp/Transfer_Extras.thy
new file mode 100644
--- /dev/null
+++ b/thys/VeriComp/Transfer_Extras.thy
@@ -0,0 +1,29 @@
+theory Transfer_Extras
+  imports Main
+begin
+
+lemma rtranclp_complete_run_right_unique:
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and x y z :: 'a
+  assumes "right_unique R"
+  shows "R\<^sup>*\<^sup>* x y \<Longrightarrow> (\<nexists>w. R y w) \<Longrightarrow> R\<^sup>*\<^sup>* x z \<Longrightarrow> (\<nexists>w. R z w) \<Longrightarrow> y = z"
+proof (induction x arbitrary: z rule: converse_rtranclp_induct)
+  case base
+  then show ?case
+    by (auto elim: converse_rtranclpE)
+next
+  case (step x w)
+  hence "R\<^sup>*\<^sup>* w z"
+    using right_uniqueD[OF \<open>right_unique R\<close>]
+    by (metis converse_rtranclpE)
+  with step show ?case
+    by simp
+qed
+
+lemma tranclp_complete_run_right_unique:
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and x y z :: 'a
+  assumes "right_unique R"
+  shows "R\<^sup>+\<^sup>+ x y \<Longrightarrow> (\<nexists>w. R y w) \<Longrightarrow> R\<^sup>+\<^sup>+ x z \<Longrightarrow> (\<nexists>w. R z w) \<Longrightarrow> y = z"
+  using right_uniqueD[OF \<open>right_unique R\<close>, of x]
+  by (auto dest!: tranclpD intro!: rtranclp_complete_run_right_unique[OF \<open>right_unique R\<close>, of _ y z])
+
+end
\ No newline at end of file