diff --git a/thys/VeriComp/Compiler.thy b/thys/VeriComp/Compiler.thy
--- a/thys/VeriComp/Compiler.thy
+++ b/thys/VeriComp/Compiler.thy
@@ -1,154 +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 option" and
-    load2 :: "'prog2 \<Rightarrow> 'state2 option" 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> load1 p1 = Some s1 \<Longrightarrow> \<exists>s2 i. load2 p2 = Some s2 \<and> match i s1 s2"
+      "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
-    loads: "load1 p1 = Some s1" "load2 p2 = Some s2" and
-    behaves: "L2.behaves s2 b2" and
+    behaves: "L2.behaves p2 b2" and
     not_wrong: "\<not> is_wrong b2"
-  shows "\<exists>b1 i. L1.behaves s1 b1 \<and> rel_behaviour (match i) b1 b2"
+  shows "\<exists>b1 i.  L1.behaves p1 b1 \<and> rel_behaviour (match i) b1 b2"
 proof -
-  obtain i where "match i s1 s2"
-    using compile_load[OF compiles] loads by auto
+  obtain s2 where "load2 p2 s2" and "L2.sem_behaves s2 b2"
+    using behaves L2.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 behaves not_wrong]
-    by simp
+    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)
 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 s1
+    fix p1 p3 s3
     assume
       compile: "(compile2 \<Lleftarrow> compile1) p1 = Some p3" and
-      load: "load1 p1 = Some s1"
-    obtain p2 where "compile1 p1 = Some p2" and "compile2 p2 = Some p3"
+      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)
-    then obtain s2 i where "load2 p2 = Some s2" and "match1 i s1 s2"
-      using assms(1)[THEN compiler.compile_load] load
-      by blast
-    moreover obtain s3 i' where "load3 p3 = Some s3" and "match2 i' s2 s3"
-      using assms(2)[THEN compiler.compile_load, OF \<open>compile2 p2 = Some p3\<close> \<open>load2 p2 = Some s2\<close>]
+    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
-    ultimately show "\<exists>s3 i. load3 p3 = Some s3 \<and> rel_comp match1 match2 i s1 s3"
+    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 s1
+      fix p1 p2 s2
       assume
         "option_comp_pow compile (Suc 0) p1 = Some p2" and
-        "load p1 = Some s1"
-      thus "\<exists>s2 i. load p2 = Some s2 \<and> rel_comp_pow match i s1 s2"
+        "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 s1
+      fix p1 p3 s3
       assume
         "option_comp_pow compile  (Suc (Suc n')) p1 = Some p3" and
-        "load p1 = Some s1"
+        "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)
-      then obtain s2 i where "load p2 = Some s2" and "match i s1 s2"
-        using compiler.compile_load[OF assms(1) _ \<open>load p1 = Some s1\<close>] by blast
-      then obtain s3 i' where "load p3 = Some s3" and "rel_comp_pow match i' s2 s3"
-        using compiler.compile_load[OF "3.IH" comp_IH] by blast
+      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>match i s1 s2\<close> \<open>rel_comp_pow match i' s2 s3\<close>
-        using rel_comp_pow.elims(2) by fastforce
-      ultimately show "\<exists>s3 i. load p3 = Some s3 \<and> rel_comp_pow match i s1 s3"
-        by auto
+        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/Fixpoint.thy b/thys/VeriComp/Fixpoint.thy
--- a/thys/VeriComp/Fixpoint.thy
+++ b/thys/VeriComp/Fixpoint.thy
@@ -1,84 +1,84 @@
 section \<open>Fixpoint of Converging Program Transformations\<close>
 
 theory Fixpoint
   imports Compiler
 begin
 
 context
   fixes
     m :: "'a \<Rightarrow> nat" and
     f :: "'a \<Rightarrow> 'a option"
 begin
 
 function fixpoint :: "'a \<Rightarrow> 'a option" where
   "fixpoint x = (
     case f x of
       None \<Rightarrow> None |
       Some x' \<Rightarrow> if m x' < m x then fixpoint x' else Some x'
   )"
 by pat_completeness auto
 termination
 proof (relation "measure m")
   show "wf (measure m)" by auto
 next
   fix x x'
   assume "f x = Some x'" and "m x' < m x"
   thus "(x', x) \<in> measure m" by simp
 qed
 
 end
 
 lemma fixpoint_to_comp_pow:
   "fixpoint m f x = y \<Longrightarrow> \<exists>n. option_comp_pow f n x = y"
 proof (induction x arbitrary: y rule: fixpoint.induct[where f = f and m = m])
   case (1 x)
   show ?case
   proof (cases "f x")
     case None
     then show ?thesis
       using "1.prems"
       by (metis (no_types, lifting) fixpoint.simps option.case_eq_if option_comp_pow.simps(1))
   next
     case (Some a)
     show ?thesis
     proof (cases "m a < m x")
       case True
       hence "fixpoint m f a = y"
         using "1.prems" Some by simp
       then show ?thesis
         using "1.IH"[OF Some True]
         by (metis Some bind.simps(2) old.nat.exhaust option_comp_def option_comp_pow.simps(1,3))
     next
       case False
       then show ?thesis
         using "1.prems" Some
         apply simp
         by (metis option_comp_pow.simps(2))
     qed
   qed
 qed
 
 lemma fixpoint_eq_comp_pow:
   "\<exists>n. fixpoint m f x = option_comp_pow f n x"
   by (metis fixpoint_to_comp_pow)
 
 lemma compiler_composition_fixpoint:
   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) (fixpoint m compile)"
 proof (rule compiler.intro)
   show "compiler_axioms load load (rel_comp_pow match) (fixpoint m compile)"
   proof unfold_locales
-    fix p1 p2 s1
-    assume "fixpoint m compile p1 = Some p2" and "load p1 = Some s1"
+    fix p1 p2 s2
+    assume "fixpoint m compile p1 = Some p2" and "load p2 s2"
     obtain n where "fixpoint m compile p1 = option_comp_pow compile n p1"
       using fixpoint_eq_comp_pow by metis
 
-    thus "\<exists>s2 i. load p2 = Some s2 \<and> rel_comp_pow match i s1 s2"
+    thus "\<exists>s1 i. load p1 s1 \<and> rel_comp_pow match i s1 s2"
       using \<open>fixpoint m compile p1 = Some p2\<close> assms compiler.compile_load compiler_composition_pow
-      using \<open>load p1 = Some s1\<close> by fastforce
+      using \<open>load p2 s2\<close> by fastforce
   qed
 qed (auto intro: assms compiler.axioms backward_simulation_pow)
 
 end
diff --git a/thys/VeriComp/Language.thy b/thys/VeriComp/Language.thy
--- a/thys/VeriComp/Language.thy
+++ b/thys/VeriComp/Language.thy
@@ -1,24 +1,48 @@
 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 option"
+    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>
+
+definition behaves :: "'prog \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
+  "behaves = load OO sem_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:
+  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
+
 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,138 @@
 section \<open>The Dynamic Representation of a Language\<close>
 
 theory Semantics
   imports Main Behaviour Inf 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"
   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)
 qed
 
 subsection \<open>Behaviour of a dynamic execution\<close>
 
-inductive behaves :: "'state \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
+inductive sem_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)" |
+    "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" |
+    "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)"
+    "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 behaves_deterministic:
+lemma sem_behaves_deterministic:
   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: behaves.induct)
+  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: behaves.induct)
+  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
   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: behaves.induct)
+  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)
+  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
   qed
 qed
 
 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,445 @@
 section \<open>Simulations Between Dynamic Executions\<close>
 
 theory Simulation
   imports Semantics Inf Well_founded
 begin
 
 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:
   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>
 
 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.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.behaves s\<^sub>1 b\<^sub>1 \<and> rel_behaviour (match i') b\<^sub>1 b\<^sub>2"
-proof(induction rule: L2.behaves.cases)
+  "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)
   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.behaves s\<^sub>1 (Terminates s1')"
+  hence "L1.sem_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
 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>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/document/root.bib b/thys/VeriComp/document/root.bib
--- a/thys/VeriComp/document/root.bib
+++ b/thys/VeriComp/document/root.bib
@@ -1,8 +1,8 @@
 @article{desharnais-jfla2020,
-  title={A Generic Framework for Verified Compilers Using {I}sabelle/{HOL}’s Locales},
+  title={A Generic Framework for Verified Compilers Using Isabelle/HOL’s Locales},
   author={Desharnais, Martin and Brunthaler, Stefan},
   journal={31 {\`e}me Journ{\'e}es Francophones des Langages Applicatifs},
   pages={198},
   year = {2020},
   url = {https://hal.inria.fr/hal-02427360}
 }