diff --git a/thys/Extended_Finite_State_Machines/EFSM.thy b/thys/Extended_Finite_State_Machines/EFSM.thy
--- a/thys/Extended_Finite_State_Machines/EFSM.thy
+++ b/thys/Extended_Finite_State_Machines/EFSM.thy
@@ -1,1495 +1,1496 @@
 section \<open>Extended Finite State Machines\<close>
 
 text\<open>This theory defines extended finite state machines as presented in \cite{foster2018}. States
 are indexed by natural numbers, however, since transition matrices are implemented by finite sets,
 the number of reachable states in $S$ is necessarily finite. For ease of implementation, we
 implicitly make the initial state zero for all EFSMs. This allows EFSMs to be represented purely by
 their transition matrix which, in this implementation, is a finite set of tuples of the form
 $((s_1, s_2), t)$ in which $s_1$ is the origin state, $s_2$ is the destination state, and $t$ is a
 transition.\<close>
 
 theory EFSM
   imports "HOL-Library.FSet" Transition FSet_Utils
 begin
 
 declare One_nat_def [simp del]
 
 type_synonym cfstate = nat
 type_synonym inputs = "value list"
 type_synonym outputs = "value option list"
 
 type_synonym action = "(label \<times> inputs)"
 type_synonym execution = "action list"
 type_synonym observation = "outputs list"
 type_synonym transition_matrix = "((cfstate \<times> cfstate) \<times> transition) fset"
 
 no_notation relcomp (infixr "O" 75) and comp (infixl "o" 55)
 
 type_synonym event = "(label \<times> inputs \<times> value list)"
 type_synonym trace = "event list"
 type_synonym log = "trace list"
 
 definition Str :: "string \<Rightarrow> value" where
   "Str s \<equiv> value.Str (String.implode s)"
 
 lemma str_not_num: "Str s \<noteq> Num x1"
   by (simp add: Str_def)
 
 definition S :: "transition_matrix \<Rightarrow> nat fset" where
   "S m = (fimage (\<lambda>((s, s'), t). s) m) |\<union>| fimage (\<lambda>((s, s'), t). s') m"
 
 lemma S_ffUnion: "S e = ffUnion (fimage (\<lambda>((s, s'), _). {|s, s'|}) e)"
   unfolding S_def
   by(induct e, auto)
 
 subsection\<open>Possible Steps\<close>
 text\<open>From a given state, the possible steps for a given action are those transitions with labels
 which correspond to the action label, arities which correspond to the number of inputs, and guards
 which are satisfied by those inputs.\<close>
 
 definition possible_steps :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> label \<Rightarrow> inputs \<Rightarrow> (cfstate \<times> transition) fset" where
   "possible_steps e s r l i = fimage (\<lambda>((origin, dest), t). (dest, t)) (ffilter (\<lambda>((origin, dest), t). origin = s \<and> (Label t) = l \<and> (length i) = (Arity t) \<and> apply_guards (Guards t) (join_ir i r)) e)"
 
 lemma possible_steps_finsert:
 "possible_steps (finsert ((s, s'), t) e) ss r l i = (
   if s = ss \<and> (Label t) = l \<and> (length i) = (Arity t) \<and> apply_guards (Guards t) (join_ir i r) then
     finsert (s', t) (possible_steps e s r l i)
   else
     possible_steps e ss r l i
 )"
   by (simp add: possible_steps_def ffilter_finsert)
 
 
 lemma split_origin:
 "ffilter (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> can_take_transition t i r) e =
 ffilter (\<lambda>((origin, dest), t). Label t = l \<and> can_take_transition t i r) (ffilter (\<lambda>((origin, dest), t). origin = s) e)"
   by auto
 
 lemma split_label:
 "ffilter (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> can_take_transition t i r) e =
 ffilter (\<lambda>((origin, dest), t). origin = s \<and> can_take_transition t i r) (ffilter (\<lambda>((origin, dest), t). Label t = l) e)"
   by auto
 
 lemma possible_steps_empty_guards_false:
   "\<forall>((s1, s2), t) |\<in>| ffilter (\<lambda>((origin, dest), t). Label t = l) e. \<not>can_take_transition t i r \<Longrightarrow>
   possible_steps e s r l i = {||}"
   apply (simp add: possible_steps_def can_take[symmetric] split_label)
   by (simp add: Abs_ffilter fBall_def Ball_def)
 
 lemma fmember_possible_steps: "(s', t) |\<in>| possible_steps e s r l i = (((s, s'), t) \<in> {((origin, dest), t) \<in> fset e. origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)})"
   apply (simp add: possible_steps_def ffilter_def fimage_def fmember_def Abs_fset_inverse)
   by force
 
 lemma possible_steps_alt_aux:
   "possible_steps e s r l i = {|(d, t)|} \<Longrightarrow>
        ffilter (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)) e = {|((s, d), t)|}"
 proof(induct e)
   case empty
   then show ?case
     by (simp add: fempty_not_finsert possible_steps_def)
 next
   case (insert x e)
   then show ?case
     apply (case_tac x)
     subgoal for a b 
       apply (case_tac a)
       subgoal for aa _
         apply (simp add: possible_steps_def)
         apply (simp add: ffilter_finsert)
         apply (case_tac "aa = s \<and> Label b = l \<and> length i = Arity b \<and> apply_guards (Guards b) (join_ir i r)")
         by auto
       done
     done
 qed
 
 lemma possible_steps_alt: "(possible_steps e s r l i = {|(d, t)|}) = (ffilter
      (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r))
      e = {|((s, d), t)|})"
   apply standard
    apply (simp add: possible_steps_alt_aux)
   by (simp add: possible_steps_def)
 
 lemma possible_steps_alt3: "(possible_steps e s r l i = {|(d, t)|}) = (ffilter
      (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> can_take_transition t i r)
      e = {|((s, d), t)|})"
   apply standard
    apply (simp add: possible_steps_alt_aux can_take)
   by (simp add: possible_steps_def can_take)
 
 lemma possible_steps_alt_atom: "(possible_steps e s r l i = {|dt|}) = (ffilter
      (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> can_take_transition t i r)
      e = {|((s, fst dt), snd dt)|})"
   apply (cases dt)
   by (simp add: possible_steps_alt can_take_transition_def can_take_def)
 
 lemma possible_steps_alt2: "(possible_steps e s r l i = {|(d, t)|}) = (
      (ffilter (\<lambda>((origin, dest), t). Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)) (ffilter (\<lambda>((origin, dest), t). origin = s) e) = {|((s, d), t)|}))"
   apply (simp add: possible_steps_alt)
   apply (simp only: filter_filter)
   apply (rule arg_cong [of "(\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r))"])
   by (rule ext, auto)
 
 lemma possible_steps_single_out:
 "ffilter (\<lambda>((origin, dest), t). origin = s) e = {|((s, d), t)|} \<Longrightarrow>
 Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r) \<Longrightarrow>
 possible_steps e s r l i = {|(d, t)|}"
   apply (simp add: possible_steps_alt2 Abs_ffilter)
   by blast
 
 lemma possible_steps_singleton: "(possible_steps e s r l i = {|(d, t)|}) =
     ({((origin, dest), t) \<in> fset e. origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)} = {((s, d), t)})"
   apply (simp add: possible_steps_alt Abs_ffilter Set.filter_def)
   by fast
 
 lemma possible_steps_apply_guards:
   "possible_steps e s r l i = {|(s', t)|} \<Longrightarrow>
    apply_guards (Guards t) (join_ir i r)"
   apply (simp add: possible_steps_singleton)
   by auto
 
 lemma possible_steps_empty:
   "(possible_steps e s r l i = {||}) = (\<forall>((origin, dest), t) \<in> fset e. origin \<noteq> s \<or> Label t \<noteq> l \<or> \<not> can_take_transition t i r)"
   apply (simp add: can_take_transition_def can_take_def)
   apply (simp add: possible_steps_def Abs_ffilter Set.filter_def)
   by auto
 
 lemma singleton_dest:
   assumes "fis_singleton (possible_steps e s r aa b)"
       and "fthe_elem (possible_steps e s r aa b) = (baa, aba)"
     shows "((s, baa), aba) |\<in>| e"
   using assms
   apply (simp add: fis_singleton_fthe_elem)
   using possible_steps_alt_aux by force
 
 lemma no_outgoing_transitions:
 "ffilter (\<lambda>((s', _), _). s = s') e = {||} \<Longrightarrow>
 possible_steps e s r l i = {||}"
   apply (simp add: possible_steps_def)
   by auto
 
 lemma ffilter_split: "ffilter (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)) e =
                       ffilter (\<lambda>((origin, dest), t). Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)) (ffilter (\<lambda>((origin, dest), t). origin = s) e)"
   by auto
 
 lemma one_outgoing_transition:
   defines "outgoing s \<equiv> (\<lambda>((origin, dest), t). origin = s)"
   assumes prem: "size (ffilter (outgoing s) e) = 1"
   shows "size (possible_steps e s r l i) \<le> 1"
 proof-
   have less_eq_1: "\<And>x::nat. (x \<le> 1) = (x = 1 \<or> x = 0)"
     by auto
   have size_empty: "\<And>f. (size f = 0) = (f = {||})"
     subgoal for f
       by (induct f, auto)
     done
   show ?thesis
     using prem
     apply (simp only: possible_steps_def)
     apply (rule fimage_size_le)
     apply (simp only: ffilter_split outgoing_def[symmetric])
     by (metis (no_types, lifting) size_ffilter)
 qed
 
 subsection\<open>Choice\<close>
 text\<open>Here we define the \texttt{choice} operator which determines whether or not two transitions are
 nondeterministic.\<close>
 
 definition choice :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
   "choice t t' = (\<exists> i r. apply_guards (Guards t) (join_ir i r) \<and> apply_guards (Guards t') (join_ir i r))"
 
 definition choice_alt :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
   "choice_alt t t' = (\<exists> i r. apply_guards (Guards t@Guards t') (join_ir i r))"
 
 lemma choice_alt: "choice t t' = choice_alt t t'"
   by (simp add: choice_def choice_alt_def apply_guards_append)
 
 lemma choice_symmetry: "choice x y = choice y x"
   using choice_def by auto
 
 definition deterministic :: "transition_matrix \<Rightarrow> bool" where
   "deterministic e = (\<forall>s r l i. size (possible_steps e s r l i) \<le> 1)"
 
 lemma deterministic_alt_aux: "size (possible_steps e s r l i) \<le> 1 =(
         possible_steps e s r l i = {||} \<or>
         (\<exists>s' t.
             ffilter
              (\<lambda>((origin, dest), t). origin = s \<and> Label t = l \<and> length i = Arity t \<and> apply_guards (Guards t) (join_ir i r)) e =
             {|((s, s'), t)|}))"
   apply (case_tac "size (possible_steps e s r l i) = 0")
    apply (simp add: fset_equiv)
   apply (case_tac "possible_steps e s r l i = {||}")
    apply simp
   apply (simp only: possible_steps_alt[symmetric])
   by (metis le_neq_implies_less le_numeral_extra(4) less_one prod.collapse size_fsingleton)
 
 lemma deterministic_alt: "deterministic e = (
   \<forall>s r l i.
     possible_steps e s r l i = {||} \<or>
     (\<exists>s' t. ffilter (\<lambda>((origin, dest), t). origin = s \<and> (Label t) = l \<and> (length i) = (Arity t) \<and> apply_guards (Guards t) (join_ir i r)) e = {|((s, s'), t)|})
 )"
   using deterministic_alt_aux
   by (simp add: deterministic_def)
 
 lemma size_le_1: "size f \<le> 1 = (f = {||} \<or> (\<exists>e. f = {|e|}))"
   apply standard
    apply (metis bot.not_eq_extremum gr_implies_not0 le_neq_implies_less less_one size_fsingleton size_fsubset)
   by auto
 
 lemma ffilter_empty_if: "\<forall>x |\<in>| xs. \<not> P x \<Longrightarrow> ffilter P xs = {||}"
   by auto
 
 lemma empty_ffilter: "ffilter P xs = {||} = (\<forall>x |\<in>| xs. \<not> P x)"
   by auto
 
 lemma all_states_deterministic:
 "(\<forall>s l i r.
   ffilter (\<lambda>((origin, dest), t). origin = s \<and> (Label t) = l \<and> can_take_transition t i r) e = {||} \<or>
   (\<exists>x. ffilter (\<lambda>((origin, dest), t). origin = s \<and> (Label t) = l \<and> can_take_transition t i r) e = {|x|})
 ) \<Longrightarrow> deterministic e"
   unfolding deterministic_def
   apply clarify
   subgoal for s r l i
     apply (erule_tac x=s in allE)
     apply (erule_tac x=l in allE)
     apply (erule_tac x=i in allE)
     apply (erule_tac x=r in allE)
     apply (simp only: size_le_1)
     apply (erule disjE)
      apply (rule_tac disjI1)
      apply (simp add: possible_steps_def can_take_transition_def can_take_def)
     apply (erule exE)
     subgoal for x
       apply (case_tac x)
       subgoal for a b
         apply (case_tac a)
         apply simp
         apply (induct e)
          apply auto[1]
         subgoal for _ _ _ ba
           apply (rule disjI2)
           apply (rule_tac x=ba in exI)
           apply (rule_tac x=b in exI)
           by (simp add: possible_steps_def can_take_transition_def[symmetric] can_take_def[symmetric])
         done
       done
     done
   done
 
 lemma deterministic_finsert:
 "\<forall>i r l.
 \<forall>((a, b), t) |\<in>| ffilter (\<lambda>((origin, dest), t). origin = s) (finsert ((s, s'), t') e).
 Label t = l \<and> can_take_transition t i r \<longrightarrow> \<not> can_take_transition t' i r \<Longrightarrow>
 deterministic e \<Longrightarrow>
 deterministic (finsert ((s, s'), t') e)"
   apply (simp add: deterministic_def possible_steps_finsert can_take del: size_fset_overloaded_simps)
   apply clarify
   subgoal for r i
     apply (erule_tac x=s in allE)
     apply (erule_tac x=r in allE)
     apply (erule_tac x="Label t'" in allE)
     apply (erule_tac x=i in allE)
     apply (erule_tac x=r in allE)
     apply (erule_tac x=i in allE)
     apply (erule_tac x="Label t'" in allE)
     by auto
   done
 
 lemma ffilter_fBall: "(\<forall>x |\<in>| xs. P x) = (ffilter P xs = xs)"
   by auto
 
 lemma fsubset_if: "\<forall>x. x |\<in>| f1 \<longrightarrow> x |\<in>| f2 \<Longrightarrow> f1 |\<subseteq>| f2"
   by auto
 
 lemma in_possible_steps: "(((s, s'), t)|\<in>|e \<and> Label t = l \<and> can_take_transition t i r) = ((s', t) |\<in>| possible_steps e s r l i)"
   apply (simp add: fmember_possible_steps)
   by (simp add: can_take_def can_take_transition_def fmember.rep_eq)
 
 lemma possible_steps_can_take_transition:
   "(s2, t1) |\<in>| possible_steps e1 s1 r l i \<Longrightarrow> can_take_transition t1 i r"
   using in_possible_steps by blast
 
 lemma not_deterministic:
   "\<exists>s l i r.
     \<exists>d1 d2 t1 t2.
       d1 \<noteq> d2 \<and> t1 \<noteq> t2 \<and>
       ((s, d1), t1) |\<in>| e \<and>
       ((s, d2), t2) |\<in>| e \<and>
       Label t1 = Label t2 \<and>
       can_take_transition t1 i r \<and>
       can_take_transition t2 i r \<Longrightarrow>
   \<not>deterministic e"
   apply (simp add: deterministic_def not_le del: size_fset_overloaded_simps)
   apply clarify
   subgoal for s i r d1 d2 t1 t2
     apply (rule_tac x=s in exI)
     apply (rule_tac x=r in exI)
     apply (rule_tac x="Label t1" in exI)
     apply (rule_tac x=i in exI)
     apply (case_tac "(d1, t1) |\<in>| possible_steps e s r (Label t1) i")
      defer using in_possible_steps apply blast
     apply (case_tac "(d2, t2) |\<in>| possible_steps e s r (Label t1) i")
      apply (metis fempty_iff fsingleton_iff not_le_imp_less prod.inject size_le_1)
     using in_possible_steps by force
   done
 
 lemma not_deterministic_conv:
   "\<not>deterministic e \<Longrightarrow>
   \<exists>s l i r.
     \<exists>d1 d2 t1 t2.
       (d1 \<noteq> d2 \<or> t1 \<noteq> t2) \<and>
       ((s, d1), t1) |\<in>| e \<and>
       ((s, d2), t2) |\<in>| e \<and>
       Label t1 = Label t2 \<and>
       can_take_transition t1 i r \<and>
       can_take_transition t2 i r"
   apply (simp add: deterministic_def not_le del: size_fset_overloaded_simps)
   apply clarify
   subgoal for s r l i
     apply (case_tac "\<exists>e1 e2 f'. e1 \<noteq> e2 \<and> possible_steps e s r l i = finsert e1 (finsert e2 f')")
      defer using size_gt_1 apply blast
     apply (erule exE)+
     subgoal for e1 e2 f'
       apply (case_tac e1, case_tac e2)
       subgoal for a b aa ba
         apply (simp del: size_fset_overloaded_simps)
         apply (rule_tac x=s in exI)
         apply (rule_tac x=i in exI)
         apply (rule_tac x=r in exI)
         apply (rule_tac x=a in exI)
         apply (rule_tac x=aa in exI)
         apply (rule_tac x=b in exI)
         apply (rule_tac x=ba in exI)
         by (metis finsertI1 finsert_commute in_possible_steps)
       done
     done
   done
 
 lemma deterministic_if:
 "\<nexists>s l i r.
   \<exists>d1 d2 t1 t2.
     (d1 \<noteq> d2 \<or> t1 \<noteq> t2) \<and>
     ((s, d1), t1) |\<in>| e \<and>
     ((s, d2), t2) |\<in>| e \<and>
     Label t1 = Label t2 \<and>
     can_take_transition t1 i r \<and>
     can_take_transition t2 i r \<Longrightarrow>
   deterministic e"
   using not_deterministic_conv by blast
 
 lemma "\<forall>l i r.
   (\<forall>((s, s'), t) |\<in>| e. Label t = l \<and> can_take_transition t i r \<and>
   (\<nexists>t' s''. ((s, s''), t') |\<in>| e \<and> (s' \<noteq> s'' \<or> t' \<noteq> t) \<and> Label t' = l \<and> can_take_transition t' i r))
  \<Longrightarrow> deterministic e"
   apply (simp add: deterministic_def del: size_fset_overloaded_simps)
   apply (rule allI)+
   apply (simp only: size_le_1 possible_steps_empty)
   apply (case_tac "\<exists>t s'. ((s, s'), t)|\<in>|e \<and> Label t = l \<and> can_take_transition t i r")
    defer using notin_fset apply fastforce
   apply (rule disjI2)
   apply clarify
   apply (rule_tac x="(s', t)" in exI)
   apply standard
    defer apply (meson fempty_fsubsetI finsert_fsubset in_possible_steps)
   apply standard
   apply (case_tac x)
   apply (simp add: in_possible_steps[symmetric])
   apply (erule_tac x="Label t" in allE)
   apply (erule_tac x=i in allE)
   apply (erule_tac x=r in allE)
   apply (erule_tac x="((s, s'), t)" in fBallE)
    defer apply simp
   apply simp
   apply (erule_tac x=b in allE)
   apply simp
   apply (erule_tac x=a in allE)
   by simp
 
 definition "outgoing_transitions e s = ffilter (\<lambda>((o, _), _). o = s) e"
 
 lemma in_outgoing: "((s1, s2), t) |\<in>| outgoing_transitions e s = (((s1, s2), t) |\<in>| e \<and> s1 = s)"
   by (simp add: outgoing_transitions_def)
 
 lemma outgoing_transitions_deterministic:
   "\<forall>s.
     \<forall>((s1, s2), t) |\<in>| outgoing_transitions e s.
       \<forall>((s1', s2'), t') |\<in>| outgoing_transitions e s.
         s2 \<noteq> s2' \<or> t \<noteq> t' \<longrightarrow> Label t = Label t' \<longrightarrow> \<not> choice t t' \<Longrightarrow> deterministic e"
   apply (rule deterministic_if)
   apply simp
   apply (rule allI)
   subgoal for s
     apply (erule_tac x=s in allE)
     apply (simp add: fBall_def Ball_def)
     apply (rule allI)+
     subgoal for i r d1 d2 t1
       apply (erule_tac x=s in allE)
       apply (erule_tac x=d1 in allE)
       apply (erule_tac x=t1 in allE)
       apply (rule impI, rule allI)
       subgoal for t2
         apply (case_tac "((s, d1), t1) \<in> fset (outgoing_transitions e s)")
          apply simp
          apply (erule_tac x=s in allE)
          apply (erule_tac x=d2 in allE)
          apply (erule_tac x=t2 in allE)
          apply (simp add: outgoing_transitions_def choice_def can_take)
          apply (meson fmember_implies_member)
         apply (simp add: outgoing_transitions_def)
         by (meson fmember_implies_member)
       done
     done
   done
 
 lemma outgoing_transitions_deterministic2: "(\<And>s a b ba aa bb bc.
        ((a, b), ba) |\<in>| outgoing_transitions e s \<Longrightarrow>
        ((aa, bb), bc) |\<in>| (outgoing_transitions e s) - {|((a, b), ba)|} \<Longrightarrow> b \<noteq> bb \<or> ba \<noteq> bc \<Longrightarrow> \<not>choice ba bc)
         \<Longrightarrow> deterministic e"
   apply (rule outgoing_transitions_deterministic)
   by blast
 
 lemma outgoing_transitions_fprod_deterministic:
 "(\<And>s b ba bb bc.
 (((s, b), ba), ((s, bb), bc)) \<in> fset (outgoing_transitions e s) \<times> fset (outgoing_transitions e s)
 \<Longrightarrow> b \<noteq> bb \<or> ba \<noteq> bc \<Longrightarrow> Label ba = Label bc \<Longrightarrow> \<not>choice ba bc)
 \<Longrightarrow> deterministic e"
   apply (rule outgoing_transitions_deterministic)
   apply clarify
   by (metis SigmaI fmember_implies_member in_outgoing)
 
 text\<open>The \texttt{random\_member} function returns a random member from a finite set, or
 \texttt{None}, if the set is empty.\<close>
 definition random_member :: "'a fset \<Rightarrow> 'a option" where
   "random_member f = (if f = {||} then None else Some (Eps (\<lambda>x. x |\<in>| f)))"
 
 lemma random_member_nonempty: "s \<noteq> {||} = (random_member s \<noteq> None)"
   by (simp add: random_member_def)
 
 lemma random_member_singleton [simp]: "random_member {|a|} = Some a"
   by (simp add: random_member_def)
 
 lemma random_member_is_member:
   "random_member ss = Some s \<Longrightarrow> s |\<in>| ss"
   apply (simp add: random_member_def)
   by (metis equalsffemptyI option.distinct(1) option.inject verit_sko_ex_indirect)
 
 lemma random_member_None[simp]: "random_member ss = None = (ss = {||})"
   by (simp add: random_member_def)
 
 lemma random_member_empty[simp]: "random_member {||} = None"
   by simp
 
 definition step :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> label \<Rightarrow> inputs \<Rightarrow> (transition \<times> cfstate \<times> outputs \<times> registers) option" where
   "step e s r l i = (case random_member (possible_steps e s r l i) of
       None \<Rightarrow> None |
       Some (s', t) \<Rightarrow>  Some (t, s', evaluate_outputs t i r, evaluate_updates t i r)
   )"
 
 lemma possible_steps_not_empty_iff:
   "step e s r a b \<noteq> None \<Longrightarrow>
    \<exists>aa ba. (aa, ba) |\<in>| possible_steps e s r a b"
   apply (simp add: step_def)
   apply (case_tac "possible_steps e s r a b")
    apply (simp add: random_member_def)
   by auto
 
 lemma step_member: "step e s r l i = Some (t, s', p, r') \<Longrightarrow> (s', t) |\<in>| possible_steps e s r l i"
   apply (simp add: step_def)
   apply (case_tac "random_member (possible_steps e s r l i)")
    apply simp
   subgoal for a by (case_tac a, simp add: random_member_is_member)
   done
 
 lemma step_outputs: "step e s r l i = Some (t, s', p, r') \<Longrightarrow> evaluate_outputs t i r = p"
   apply (simp add: step_def)
   apply (case_tac "random_member (possible_steps e s r l i)")
   by auto
 
 lemma step:
   "possibilities = (possible_steps e s r l i) \<Longrightarrow>
    random_member possibilities = Some (s', t) \<Longrightarrow>
    evaluate_outputs t i r = p \<Longrightarrow>
    evaluate_updates t i r = r' \<Longrightarrow>
    step e s r l i = Some (t, s', p, r')"
   by (simp add: step_def)
 
 lemma step_None: "step e s r l i = None = (possible_steps e s r l i = {||})"
   by (simp add: step_def prod.case_eq_if random_member_def)
 
 lemma step_Some: "step e s r l i = Some (t, s', p, r') =
   (
     random_member (possible_steps e s r l i) = Some (s', t) \<and>
     evaluate_outputs t i r = p \<and>
     evaluate_updates t i r = r'
   )"
   apply (simp add: step_def)
   apply (case_tac "random_member (possible_steps e s r l i)")
    apply simp
   subgoal for a by (case_tac a, auto)
   done
 
 lemma no_possible_steps_1:
   "possible_steps e s r l i = {||} \<Longrightarrow> step e s r l i = None"
   by (simp add: step_def random_member_def)
 
 subsection\<open>Execution Observation\<close>
 text\<open>One of the key features of this formalisation of EFSMs is their ability to produce
 \emph{outputs}, which represent function return values. When action sequences are executed in an
 EFSM, they produce a corresponding \emph{observation}.\<close>
 
 text_raw\<open>\snip{observe}{1}{2}{%\<close>
 fun observe_execution :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> outputs list" where
   "observe_execution _ _ _ [] = []" |
   "observe_execution e s r ((l, i)#as)  = (
     let viable = possible_steps e s r l i in
     if viable = {||} then
       []
     else
       let (s', t) = Eps (\<lambda>x. x |\<in>| viable) in
       (evaluate_outputs t i r)#(observe_execution e s' (evaluate_updates t i r) as)
     )"
 text_raw\<open>}%endsnip\<close>
 
 lemma observe_execution_step_def: "observe_execution e s r ((l, i)#as)  = (
     case step e s r l i of
       None \<Rightarrow> []|
       Some (t, s', p, r') \<Rightarrow> p#(observe_execution e s' r' as)
     )"
   apply (simp add: step_def)
   apply (case_tac "possible_steps e s r l i")
    apply simp
   subgoal for x S'
     apply (simp add: random_member_def)
     apply (case_tac "SOME xa. xa = x \<or> xa |\<in>| S'")
     by simp
   done
 
 lemma observe_execution_first_outputs_equiv:
   "observe_execution e1 s1 r1 ((l, i) # ts) = observe_execution e2 s2 r2 ((l, i) # ts) \<Longrightarrow>
    step e1 s1 r1 l i = Some (t, s', p, r') \<Longrightarrow>
    \<exists>(s2', t2)|\<in>|possible_steps e2 s2 r2 l i. evaluate_outputs t2 i r2 = p"
   apply (simp only: observe_execution_step_def)
   apply (case_tac "step e2 s2 r2 l i")
    apply simp
   subgoal for a
     apply simp
     apply (case_tac a)
     apply clarsimp
     by (meson step_member case_prodI rev_fBexI step_outputs)
   done
 
 lemma observe_execution_step:
   "step e s r (fst h) (snd h) = Some (t, s', p, r') \<Longrightarrow>
    observe_execution e s' r' es = obs \<Longrightarrow>
    observe_execution e s r (h#es) = p#obs"
   apply (cases h, simp add: step_def)
   apply (case_tac "possible_steps e s r a b = {||}")
    apply simp
   subgoal for a b
     apply (case_tac "SOME x. x |\<in>| possible_steps e s r a b")
-    apply (simp add: random_member_def)
-    by auto
+    by (simp add: random_member_def)
   done
 
 lemma observe_execution_possible_step:
   "possible_steps e s r (fst h) (snd h) = {|(s', t)|} \<Longrightarrow>
    apply_outputs (Outputs t) (join_ir (snd h) r) = p \<Longrightarrow>
    apply_updates (Updates t) (join_ir (snd h) r) r = r' \<Longrightarrow>
    observe_execution e s' r' es = obs \<Longrightarrow>
    observe_execution e s r (h#es) = p#obs"
   by (simp add: observe_execution_step step)
 
 lemma observe_execution_no_possible_step:
   "possible_steps e s r (fst h) (snd h) = {||} \<Longrightarrow>
    observe_execution e s r (h#es) = []"
   by (cases h, simp)
 
 lemma observe_execution_no_possible_steps:
   "possible_steps e1 s1 r1 (fst h) (snd h) = {||} \<Longrightarrow>
    possible_steps e2 s2 r2 (fst h) (snd h) = {||} \<Longrightarrow>
    (observe_execution e1 s1 r1 (h#t)) = (observe_execution e2 s2 r2 (h#t))"
   by (simp add: observe_execution_no_possible_step)
 
 lemma observe_execution_one_possible_step:
   "possible_steps e1 s1 r (fst h) (snd h) = {|(s1', t1)|} \<Longrightarrow>
    possible_steps e2 s2 r (fst h) (snd h) = {|(s2', t2)|} \<Longrightarrow>
    apply_outputs (Outputs t1) (join_ir (snd h) r) = apply_outputs (Outputs t2) (join_ir (snd h) r) \<Longrightarrow>
 
    apply_updates (Updates t1) (join_ir (snd h) r) r = r' \<Longrightarrow>
    apply_updates (Updates t2) (join_ir (snd h) r) r = r' \<Longrightarrow>
    (observe_execution e1 s1' r' t) = (observe_execution e2 s2' r' t) \<Longrightarrow>
    (observe_execution e1 s1 r (h#t)) = (observe_execution e2 s2 r (h#t))"
   by (simp add: observe_execution_possible_step)
 
 subsubsection\<open>Utilities\<close>
 text\<open>Here we define some utility functions to access the various key properties of a given EFSM.\<close>
 
 definition max_reg :: "transition_matrix \<Rightarrow> nat option" where
   "max_reg e = (let maxes = (fimage (\<lambda>(_, t). Transition.max_reg t) e) in if maxes = {||} then None else fMax maxes)"
 
 definition enumerate_ints :: "transition_matrix \<Rightarrow> int set" where
   "enumerate_ints e = \<Union> (image (\<lambda>(_, t). Transition.enumerate_ints t) (fset e))"
 
 definition max_int :: "transition_matrix \<Rightarrow> int" where
   "max_int e = Max (insert 0 (enumerate_ints e))"
 
 definition max_output :: "transition_matrix \<Rightarrow> nat" where
   "max_output e = fMax (fimage (\<lambda>(_, t). length (Outputs t)) e)"
 
 definition all_regs :: "transition_matrix \<Rightarrow> nat set" where
   "all_regs e = \<Union> (image (\<lambda>(_, t). enumerate_regs t) (fset e))"
 
 text_raw\<open>\snip{finiteRegs}{1}{2}{%\<close>
 lemma finite_all_regs: "finite (all_regs e)"
 text_raw\<open>}%endsnip\<close>
   apply (simp add: all_regs_def enumerate_regs_def)
   apply clarify
   apply standard
    apply (rule finite_UnI)+
   using GExp.finite_enumerate_regs apply blast
   using AExp.finite_enumerate_regs apply blast
    apply (simp add: AExp.finite_enumerate_regs prod.case_eq_if)
   by auto
 
 definition max_input :: "transition_matrix \<Rightarrow> nat option" where
   "max_input e = fMax (fimage (\<lambda>(_, t). Transition.max_input t) e)"
 
 fun maxS :: "transition_matrix \<Rightarrow> nat" where
   "maxS t = (if t = {||} then 0 else fMax ((fimage (\<lambda>((origin, dest), t). origin) t) |\<union>| (fimage (\<lambda>((origin, dest), t). dest) t)))"
 
 subsection\<open>Execution Recognition\<close>
 text\<open>The \texttt{recognises} function returns true if the given EFSM recognises a given execution.
 That is, the EFSM is able to respond to each event in sequence. There is no restriction on the
 outputs produced. When a recognised execution is observed, it produces an accepted trace of the
 EFSM.\<close>
 
 text_raw\<open>\snip{recognises}{1}{2}{%\<close>
 inductive recognises_execution :: "transition_matrix \<Rightarrow> nat \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   base [simp]: "recognises_execution e s r []" |
   step: "\<exists>(s', T) |\<in>| possible_steps e s r l i.
          recognises_execution e s' (evaluate_updates T i r) t \<Longrightarrow>
          recognises_execution e s r ((l, i)#t)"
 text_raw\<open>}%endsnip\<close>
 
 abbreviation "recognises e t \<equiv> recognises_execution e 0 <> t"
 
 definition "E e = {x. recognises e x}"
 
 lemma no_possible_steps_rejects:
   "possible_steps e s r l i = {||} \<Longrightarrow> \<not> recognises_execution e s r ((l, i)#t)"
   apply clarify
   by (rule recognises_execution.cases, auto)
 
 lemma recognises_step_equiv: "recognises_execution e s r ((l, i)#t) =
    (\<exists>(s', T) |\<in>| possible_steps e s r l i. recognises_execution e s' (evaluate_updates T i r) t)"
   apply standard
    apply (rule recognises_execution.cases)
   by (auto simp: recognises_execution.step)
 
 fun recognises_prim :: "transition_matrix \<Rightarrow> nat \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   "recognises_prim e s r [] = True" |
   "recognises_prim e s r ((l, i)#t) = (
     let poss_steps = possible_steps e s r l i in
     (\<exists>(s', T) |\<in>| poss_steps. recognises_prim e s' (evaluate_updates T i r) t)
   )"
 
 lemma recognises_prim [code]: "recognises_execution e s r t = recognises_prim e s r t"
 proof(induct t arbitrary: r s)
   case Nil
   then show ?case
     by simp
 next
   case (Cons h t)
   then show ?case
     apply (cases h)
     apply simp
     apply standard
      apply (rule recognises_execution.cases, simp)
       apply simp
      apply auto[1]
     using recognises_execution.step by blast
 qed
 
 lemma recognises_single_possible_step:
   assumes "possible_steps e s r l i = {|(s', t)|}"
       and "recognises_execution e s' (evaluate_updates t i r) trace"
     shows "recognises_execution e s r ((l, i)#trace)"
   apply (rule recognises_execution.step)
   using assms by auto
 
 lemma recognises_single_possible_step_atomic:
   assumes "possible_steps e s r (fst h) (snd h) = {|(s', t)|}"
       and "recognises_execution e s' (apply_updates (Updates t) (join_ir (snd h) r) r) trace"
     shows "recognises_execution e s r (h#trace)"
   by (metis assms prod.collapse recognises_single_possible_step)
 
 lemma recognises_must_be_possible_step:
   "recognises_execution e s r (h # t) \<Longrightarrow>
    \<exists>aa ba. (aa, ba) |\<in>| possible_steps e s r (fst h) (snd h)"
   using recognises_step_equiv by fastforce
 
 lemma recognises_possible_steps_not_empty:
   "recognises_execution e s r (h#t) \<Longrightarrow> possible_steps e s r (fst h) (snd h) \<noteq> {||}"
   apply (rule recognises_execution.cases)
   by auto
 
 lemma recognises_must_be_step:
   "recognises_execution e s r (h#ts) \<Longrightarrow>
    \<exists>t s' p d'. step e s r (fst h) (snd h) = Some (t, s', p, d')"
   apply (cases h)
   subgoal for a b 
     apply (simp add: recognises_step_equiv step_def)
     apply clarify
     apply (case_tac "(possible_steps e s r a b)")
      apply (simp add: random_member_def)
     apply (simp add: random_member_def)
     subgoal for _ _ x S' apply (case_tac "SOME xa. xa = x \<or> xa |\<in>| S'")
       by simp
     done
   done
 
 lemma recognises_cons_step:
   "recognises_execution e s r (h # t) \<Longrightarrow> step e s r (fst h) (snd h) \<noteq>  None"
   by (simp add: recognises_must_be_step)
 
 lemma no_step_none:
   "step e s r aa ba = None \<Longrightarrow> \<not> recognises_execution e s r ((aa, ba) # p)"
   using recognises_cons_step by fastforce
 
 lemma step_none_rejects:
   "step e s r (fst h) (snd h) = None \<Longrightarrow> \<not> recognises_execution e s r (h#t)"
   using no_step_none surjective_pairing by fastforce
 
 lemma trace_reject:
   "(\<not> recognises_execution e s r ((l, i)#t)) = (possible_steps e s r l i = {||} \<or> (\<forall>(s', T) |\<in>| possible_steps e s r l i. \<not> recognises_execution e s' (evaluate_updates T i r) t))"
   using recognises_prim by fastforce
 
 lemma trace_reject_no_possible_steps_atomic:
   "possible_steps e s r (fst a) (snd a) = {||} \<Longrightarrow> \<not> recognises_execution e s r (a#t)"
   using recognises_possible_steps_not_empty by auto
 
 lemma trace_reject_later:
   "\<forall>(s', T) |\<in>| possible_steps e s r l i. \<not> recognises_execution e s' (evaluate_updates T i r) t \<Longrightarrow>
    \<not> recognises_execution e s r ((l, i)#t)"
   using trace_reject by auto
 
 lemma recognition_prefix_closure: "recognises_execution e s r (t@t') \<Longrightarrow> recognises_execution e s r t"
 proof(induct t arbitrary: s r)
   case (Cons a t)
   then show ?case
     apply (cases a, clarsimp)
     apply (rule recognises_execution.cases)
       apply simp
      apply simp
     by (rule recognises_execution.step, auto)
 qed auto
 
 lemma rejects_prefix: "\<not> recognises_execution e s r t \<Longrightarrow> \<not> recognises_execution e s r (t @ t')"
   using recognition_prefix_closure by blast
 
 lemma recognises_head: "recognises_execution e s r (h#t) \<Longrightarrow> recognises_execution e s r [h]"
   by (simp add: recognition_prefix_closure)
 
 subsubsection\<open>Trace Acceptance\<close>
 text\<open>The \texttt{accepts} function returns true if the given EFSM accepts a given trace. That is,
 the EFSM is able to respond to each event in sequence \emph{and} is able to produce the expected
 output. Accepted traces represent valid runs of an EFSM.\<close>
 
 text_raw\<open>\snip{accepts}{1}{2}{%\<close>
 inductive accepts_trace :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> bool" where
   base [simp]: "accepts_trace e s r []" |
   step: "\<exists>(s', T) |\<in>| possible_steps e s r l i.
          evaluate_outputs T i r = map Some p \<and> accepts_trace e s' (evaluate_updates T i r) t \<Longrightarrow>
          accepts_trace e s r ((l, i, p)#t)"
 text_raw\<open>}%endsnip\<close>
 
 text_raw\<open>\snip{T}{1}{2}{%\<close>
 definition T :: "transition_matrix \<Rightarrow> trace set" where
   "T e = {t. accepts_trace e 0 <> t}"
 text_raw\<open>}%endsnip\<close>
 
 abbreviation "rejects_trace e s r t \<equiv> \<not> accepts_trace e s r t"
 
 lemma accepts_trace_step:
   "accepts_trace e s r ((l, i, p)#t) = (\<exists>(s', T) |\<in>| possible_steps e s r l i.
          evaluate_outputs T i r = map Some p \<and>
          accepts_trace e s' (evaluate_updates T i r) t)"
   apply standard
   by (rule accepts_trace.cases, auto simp: accepts_trace.step)
 
 lemma accepts_trace_exists_possible_step:
   "accepts_trace e1 s1 r1 ((aa, b, c) # t) \<Longrightarrow>
        \<exists>(s1', t1)|\<in>|possible_steps e1 s1 r1 aa b.
           evaluate_outputs t1 b r1 = map Some c"
   using accepts_trace_step by auto
 
 lemma rejects_trace_step:
 "rejects_trace e s r ((l, i, p)#t) = (
   (\<forall>(s', T) |\<in>| possible_steps e s r l i.  evaluate_outputs T i r \<noteq> map Some p \<or> rejects_trace e s' (evaluate_updates T i r) t)
 )"
   apply (simp add: accepts_trace_step)
   by auto
 
 definition accepts_log :: "trace set \<Rightarrow> transition_matrix \<Rightarrow> bool" where
   "accepts_log l e = (\<forall>t \<in> l. accepts_trace e 0 <> t)"
 
 text_raw\<open>\snip{prefixClosure}{1}{2}{%\<close>
 lemma prefix_closure: "accepts_trace e s r (t@t') \<Longrightarrow> accepts_trace e s r t"
 text_raw\<open>}%endsnip\<close>
 proof(induct t arbitrary: s r)
 next
   case (Cons a t)
   then show ?case
     apply (cases a, clarsimp)
     apply (simp add: accepts_trace_step)
     by auto
 qed auto
 
 text\<open>For code generation, it is much more efficient to re-implement the \texttt{accepts\_trace}
 function primitively than to use the code generator's default setup for inductive definitions.\<close>
 fun accepts_trace_prim :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> bool" where
   "accepts_trace_prim _ _ _ [] = True" |
   "accepts_trace_prim e s r ((l, i, p)#t) = (
     let poss_steps = possible_steps e s r l i in
     if fis_singleton poss_steps then
       let (s', T) = fthe_elem poss_steps in
       if evaluate_outputs T i r = map Some p then
         accepts_trace_prim e s' (evaluate_updates T i r) t
       else False
     else
       (\<exists>(s', T) |\<in>| poss_steps.
          evaluate_outputs T i r = (map Some p) \<and>
          accepts_trace_prim e s' (evaluate_updates T i r) t))"
 
 lemma accepts_trace_prim [code]: "accepts_trace e s r l = accepts_trace_prim e s r l"
 proof(induct l arbitrary: s r)
   case (Cons a l)
   then show ?case
     apply (cases a)
     apply (simp add: accepts_trace_step Let_def fis_singleton_alt)
     by auto
 qed auto
 
 subsection\<open>EFSM Comparison\<close>
 text\<open>Here, we define some different metrics of EFSM equality.\<close>
 
 subsubsection\<open>State Isomporphism\<close>
 text\<open>Two EFSMs are isomorphic with respect to states if there exists a bijective function between
 the state names of the two EFSMs, i.e. the only difference between the two models is the way the
 states are indexed.\<close>
 
 definition isomorphic :: "transition_matrix \<Rightarrow> transition_matrix \<Rightarrow> bool" where
   "isomorphic e1 e2 = (\<exists>f. bij f \<and> (\<forall>((s1, s2), t) |\<in>| e1. ((f s1, f s2), t) |\<in>| e2))"
 
 subsubsection\<open>Register Isomporphism\<close>
 text\<open>Two EFSMs are isomorphic with respect to registers if there exists a bijective function between
 the indices of the registers in the two EFSMs, i.e. the only difference between the two models is
 the way the registers are indexed.\<close>
 definition rename_regs :: "(nat \<Rightarrow> nat) \<Rightarrow> transition_matrix \<Rightarrow> transition_matrix" where
   "rename_regs f e = fimage (\<lambda>(tf, t). (tf, Transition.rename_regs f t)) e"
 
 definition eq_upto_rename_strong :: "transition_matrix \<Rightarrow> transition_matrix \<Rightarrow> bool" where
   "eq_upto_rename_strong e1 e2 = (\<exists>f. bij f \<and> rename_regs f e1 = e2)"
 
 subsubsection\<open>Trace Simulation\<close>
 text\<open>An EFSM, $e_1$ simulates another EFSM $e_2$ if there is a function between the states of the
 states of $e_1$ and $e_1$ such that in each state, if $e_1$ can respond to the event and produce
 the correct output, so can $e_2$.\<close>
 
 text_raw\<open>\snip{traceSim}{1}{2}{%\<close>
 inductive trace_simulation :: "(cfstate \<Rightarrow> cfstate) \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow>
 transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> bool" where
   base: "s2 = f s1 \<Longrightarrow> trace_simulation f e1 s1 r1 e2 s2 r2 []" |
   step: "s2 = f s1 \<Longrightarrow>
          \<forall>(s1', t1) |\<in>| ffilter (\<lambda>(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i).
            \<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i. evaluate_outputs t2 i r2 = map Some o \<and>
             trace_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es \<Longrightarrow>
          trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es)"
 text_raw\<open>}%endsnip\<close>
 
 lemma trace_simulation_step:
 "trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es) = (
   (s2 = f s1) \<and> (\<forall>(s1', t1) |\<in>| ffilter (\<lambda>(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i).
          (\<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i. evaluate_outputs t2 i r2 = map Some o \<and>
          trace_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es))
 )"
   apply standard
    apply (rule trace_simulation.cases, simp+)
   apply (rule trace_simulation.step)
    apply simp
   by blast
 
 lemma trace_simulation_step_none:
   "s2 = f s1 \<Longrightarrow>
    \<nexists>(s1', t1) |\<in>| possible_steps e1 s1 r1 l i. evaluate_outputs t1 i r1 = map Some o \<Longrightarrow>
    trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es)"
   apply (rule trace_simulation.step)
    apply simp
   apply (case_tac "ffilter (\<lambda>(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i)")
    apply simp
   by fastforce
 
 definition "trace_simulates e1 e2 = (\<exists>f. \<forall>t. trace_simulation f e1 0 <> e2 0 <> t)"
 
 lemma rejects_trace_simulation:
   "rejects_trace e2 s2 r2 t \<Longrightarrow>
    accepts_trace e1 s1 r1 t \<Longrightarrow>
    \<not>trace_simulation f e1 s1 r1 e2 s2 r2 t"
 proof(induct t arbitrary: s1 r1 s2 r2)
   case Nil
   then show ?case
     using accepts_trace.base by blast
 next
   case (Cons a t)
   then show ?case
     apply (cases a)
     apply (simp add: rejects_trace_step)
     apply (simp add: accepts_trace_step)
     apply clarify
     apply (rule trace_simulation.cases)
       apply simp
      apply simp
     apply clarsimp
-    subgoal for _ _ i o l
+    subgoal for l o _ _ i
       apply (case_tac "ffilter (\<lambda>(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i) = {||}")
        apply auto[1]
       by fastforce
     done
 qed
 
 lemma accepts_trace_simulation:
   "accepts_trace e1 s1 r1 t \<Longrightarrow>
    trace_simulation f e1 s1 r1 e2 s2 r2 t \<Longrightarrow>
    accepts_trace e2 s2 r2 t"
   using rejects_trace_simulation by blast
 
 lemma simulates_trace_subset: "trace_simulates e1 e2 \<Longrightarrow> T e1 \<subseteq> T e2"
   using T_def accepts_trace_simulation trace_simulates_def by fastforce
 
 subsubsection\<open>Trace Equivalence\<close>
 text\<open>Two EFSMs are trace equivalent if they accept the same traces. This is the intuitive definition
 of ``observable equivalence'' between the behaviours of the two models. If two EFSMs are trace
 equivalent, there is no trace which can distinguish the two.\<close>
 
 text_raw\<open>\snip{traceEquiv}{1}{2}{%\<close>
 definition "trace_equivalent e1 e2 = (T e1 = T e2)"
 text_raw\<open>}%endsnip\<close>
 
 text_raw\<open>\snip{simEquiv}{1}{2}{%\<close>
 lemma simulation_implies_trace_equivalent:
   "trace_simulates e1 e2 \<Longrightarrow> trace_simulates e2 e1 \<Longrightarrow> trace_equivalent e1 e2"
 text_raw\<open>}%endsnip\<close>
   using simulates_trace_subset trace_equivalent_def by auto
 
 lemma trace_equivalent_reflexive: "trace_equivalent e1 e1"
   by (simp add: trace_equivalent_def)
 
 lemma trace_equivalent_symmetric:
   "trace_equivalent e1 e2 = trace_equivalent e2 e1"
   using trace_equivalent_def by auto
 
 lemma trace_equivalent_transitive:
   "trace_equivalent e1 e2 \<Longrightarrow>
    trace_equivalent e2 e3 \<Longrightarrow>
    trace_equivalent e1 e3"
   by (simp add: trace_equivalent_def)
 
 text\<open>Two EFSMs are trace equivalent if they accept the same traces.\<close>
 lemma trace_equivalent:
   "\<forall>t. accepts_trace e1 0 <> t = accepts_trace e2 0 <> t \<Longrightarrow> trace_equivalent e1 e2"
   by (simp add: T_def trace_equivalent_def)
 
 lemma accepts_trace_step_2: "(s2', t2) |\<in>| possible_steps e2 s2 r2 l i \<Longrightarrow>
        accepts_trace e2 s2' (evaluate_updates t2 i r2) t \<Longrightarrow>
        evaluate_outputs t2 i r2 = map Some p \<Longrightarrow>
        accepts_trace e2 s2 r2 ((l, i, p)#t)"
   by (rule accepts_trace.step, auto)
 
 subsubsection\<open>Execution Simulation\<close>
 text\<open>Execution simulation is similar to trace simulation but for executions rather than traces.
 Execution simulation has no notion of ``expected'' output. It simply requires that the simulating
 EFSM must be able to produce equivalent output for each action.\<close>
 
 text_raw\<open>\snip{execSim}{1}{2}{%\<close>
 inductive execution_simulation :: "(cfstate \<Rightarrow> cfstate) \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow>
 registers \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   base: "s2 = f s1 \<Longrightarrow> execution_simulation f e1 s1 r1 e2 s2 r2 []" |
   step: "s2 = f s1 \<Longrightarrow>
          \<forall>(s1', t1) |\<in>| (possible_steps e1 s1 r1 l i).
            \<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i.
             evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
             execution_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es \<Longrightarrow>
          execution_simulation f e1 s1 r1 e2 s2 r2 ((l, i)#es)"
 text_raw\<open>}%endsnip\<close>
 
 definition "execution_simulates e1 e2 = (\<exists>f. \<forall>t. execution_simulation f e1 0 <> e2 0 <> t)"
 
 lemma execution_simulation_step:
 "execution_simulation f e1 s1 r1 e2 s2 r2 ((l, i)#es) =
  (s2 = f s1 \<and>
  (\<forall>(s1', t1) |\<in>| (possible_steps e1 s1 r1 l i).
          (\<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
          execution_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es))
 )"
   apply standard
    apply (rule execution_simulation.cases)
      apply simp
     apply simp
    apply simp
   apply (rule execution_simulation.step)
    apply simp
   by blast
 
 text_raw\<open>\snip{execTraceSim}{1}{2}{%\<close>
 lemma execution_simulation_trace_simulation:
   "execution_simulation f e1 s1 r1 e2 s2 r2 (map (\<lambda>(l, i, o). (l, i)) t) \<Longrightarrow>
    trace_simulation f e1 s1 r1 e2 s2 r2 t"
 text_raw\<open>}%endsnip\<close>
 proof(induct t arbitrary: s1 s2 r1 r2)
 case Nil
   then show ?case
     apply (rule execution_simulation.cases)
      apply (simp add: trace_simulation.base)
     by simp
 next
   case (Cons a t)
   then show ?case
     apply (cases a, clarsimp)
     apply (rule execution_simulation.cases)
       apply simp
      apply simp
     apply (rule trace_simulation.step)
      apply simp
     apply clarsimp
     subgoal for _ _ _ aa ba
       apply (erule_tac x="(aa, ba)" in fBallE)
        apply clarsimp
        apply blast
       by simp
     done
 qed
 
 lemma execution_simulates_trace_simulates:
   "execution_simulates e1 e2 \<Longrightarrow> trace_simulates e1 e2"
   apply (simp add: execution_simulates_def trace_simulates_def)
   using execution_simulation_trace_simulation by blast
 
 subsubsection\<open>Executional Equivalence\<close>
 text\<open>Two EFSMs are executionally equivalent if there is no execution which can distinguish between
 the two. That is, for every execution, they must produce equivalent outputs.\<close>
 
 text_raw\<open>\snip{execEquiv}{1}{2}{%\<close>
 inductive executionally_equivalent :: "transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow>
 transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   base [simp]: "executionally_equivalent e1 s1 r1 e2 s2 r2 []" |
   step: "\<forall>(s1', t1) |\<in>| possible_steps e1 s1 r1 l i.
            \<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i.
              evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
              executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es \<Longrightarrow>
          \<forall>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i.
            \<exists>(s1', t1) |\<in>| possible_steps e1 s1 r1 l i.
              evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
              executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es \<Longrightarrow>
          executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es)"
 text_raw\<open>}%endsnip\<close>
 
 lemma executionally_equivalent_step:
 "executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es) = (
   (\<forall>(s1', t1) |\<in>| (possible_steps e1 s1 r1 l i). (\<exists>(s2', t2) |\<in>| possible_steps e2 s2 r2 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
    executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es)) \<and>
   (\<forall>(s2', t2) |\<in>| (possible_steps e2 s2 r2 l i). (\<exists>(s1', t1) |\<in>| possible_steps e1 s1 r1 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 \<and>
    executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es)))"
   apply standard
    apply (rule executionally_equivalent.cases)
      apply simp
     apply simp
    apply simp
   by (rule executionally_equivalent.step, auto)
 
 lemma execution_end:
   "possible_steps e1 s1 r1 l i = {||} \<Longrightarrow>
    possible_steps e2 s2 r2 l i = {||} \<Longrightarrow>
   executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es)"
   by (simp add: executionally_equivalent_step)
 
 lemma possible_steps_disparity:
   "possible_steps e1 s1 r1 l i \<noteq> {||} \<Longrightarrow>
    possible_steps e2 s2 r2 l i = {||} \<Longrightarrow>
    \<not>executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es)"
   by (simp add: executionally_equivalent_step, auto)
 
 lemma executionally_equivalent_acceptance_map:
   "executionally_equivalent e1 s1 r1 e2 s2 r2 (map (\<lambda>(l, i, o). (l, i)) t) \<Longrightarrow>
    accepts_trace e2 s2 r2 t = accepts_trace e1 s1 r1 t"
 proof(induct t arbitrary: s1 s2 r1 r2)
   case (Cons a t)
   then show ?case
     apply (cases a, simp)
     apply (rule executionally_equivalent.cases)
       apply simp
      apply simp
     apply clarsimp
     apply standard
-    subgoal for p l i
+    subgoal for i p l
       apply (rule accepts_trace.cases)
         apply simp
        apply simp
       apply clarsimp
       subgoal for aa b
         apply (rule accepts_trace.step)
         apply (erule_tac x="(aa, b)" in fBallE[of "possible_steps e2 s2 r2 l i"])
          defer apply simp
         apply simp
         by blast
       done
     apply (rule accepts_trace.cases)
       apply simp
      apply simp
     apply clarsimp
-    apply (rule accepts_trace.step)
-    apply (erule_tac x="(aa, b)" in fBallE)
-     defer apply simp
-    apply simp
-    by fastforce
+    subgoal for _ _ _ aa b
+      apply (rule accepts_trace.step)
+      apply (erule_tac x="(aa, b)" in fBallE)
+       defer apply simp
+      apply simp
+      by fastforce
+    done
 qed auto
 
 lemma executionally_equivalent_acceptance:
   "\<forall>x. executionally_equivalent e1 s1 r1 e2 s2 r2 x \<Longrightarrow> accepts_trace e1 s1 r1  t \<Longrightarrow> accepts_trace e2 s2 r2 t"
   using executionally_equivalent_acceptance_map by blast
 
 lemma executionally_equivalent_trace_equivalent:
   "\<forall>x. executionally_equivalent e1 0 <> e2 0 <> x \<Longrightarrow> trace_equivalent e1 e2"
   apply (rule trace_equivalent)
   apply clarify
   subgoal for t apply (erule_tac x="map (\<lambda>(l, i, o). (l, i)) t" in allE)
     by (simp add: executionally_equivalent_acceptance_map)
   done
 
 lemma executionally_equivalent_symmetry:
   "executionally_equivalent e1 s1 r1 e2 s2 r2 x \<Longrightarrow>
    executionally_equivalent e2 s2 r2 e1 s1 r1 x"
 proof(induct x arbitrary: s1 s2 r1 r2)
   case (Cons a x)
   then show ?case
     apply (cases a, clarsimp)
     apply (simp add: executionally_equivalent_step)
     apply standard
      apply (rule fBallI)
      apply clarsimp
     subgoal for aa b aaa ba
       apply (erule_tac x="(aaa, ba)" in fBallE[of "possible_steps e2 s2 r2 aa b"])
       by (force, simp)
     apply (rule fBallI)
     apply clarsimp
     subgoal for aa b aaa ba
       apply (erule_tac x="(aaa, ba)" in fBallE)
       by (force, simp)
     done
 qed auto
 
 lemma executionally_equivalent_transitivity:
   "executionally_equivalent e1 s1 r1 e2 s2 r2 x \<Longrightarrow>
    executionally_equivalent e2 s2 r2 e3 s3 r3 x \<Longrightarrow>
    executionally_equivalent e1 s1 r1 e3 s3 r3 x"
 proof(induct x arbitrary: s1 s2 s3 r1 r2 r3)
   case (Cons a x)
   then show ?case
     apply (cases a, clarsimp)
     apply (simp add: executionally_equivalent_step)
     apply clarsimp
     apply standard
      apply (rule fBallI)
      apply clarsimp
     subgoal for aa b ab ba
       apply (erule_tac x="(ab, ba)" in fBallE[of "possible_steps e1 s1 r1 aa b"])
        prefer 2 apply simp
       apply simp
       apply (erule fBexE)
       subgoal for x apply (case_tac x)
         apply simp
         by blast
       done
     apply (rule fBallI)
     apply clarsimp
     subgoal for aa b ab ba
       apply (erule_tac x="(ab, ba)" in fBallE[of "possible_steps e3 s3 r3 aa b"])
        prefer 2 apply simp
       apply simp
       apply (erule fBexE)
       subgoal for x apply (case_tac x)
         apply clarsimp
         subgoal for aaa baa
           apply (erule_tac x="(aaa, baa)" in fBallE[of "possible_steps e2 s2 r2 aa b"])
            prefer 2 apply simp
           apply simp
           by blast
         done
       done
     done
 qed auto
 
 subsection\<open>Reachability\<close>
 text\<open>Here, we define the function \texttt{visits} which returns true if the given execution
 leaves the given EFSM in the given state.\<close>
 
 text_raw\<open>\snip{reachable}{1}{2}{%\<close>
 inductive visits :: "cfstate \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   base [simp]: "visits s e s r []" |
   step: "\<exists>(s', T) |\<in>| possible_steps e s r l i. visits target e s' (evaluate_updates T i r) t \<Longrightarrow>
          visits target e s r ((l, i)#t)"
 
 definition "reachable s e = (\<exists>t. visits s e 0 <> t)"
 text_raw\<open>}%endsnip\<close>
 
 lemma no_further_steps:
   "s \<noteq> s' \<Longrightarrow> \<not> visits s e s' r []"
   apply safe
   apply (rule visits.cases)
   by auto
 
 lemma visits_base: "visits target e s r [] = (s = target)"
   by (metis visits.base no_further_steps)
 
 lemma visits_step:
   "visits target e s r (h#t) = (\<exists>(s', T) |\<in>| possible_steps e s r (fst h) (snd h). visits target e s' (evaluate_updates T (snd h) r) t)"
   apply standard
    apply (rule visits.cases)
      apply simp+
   apply (cases h)
   using visits.step by auto
 
 lemma reachable_initial: "reachable 0 e"
   apply (simp add: reachable_def)
   apply (rule_tac x="[]" in exI)
   by simp
 
 lemma visits_finsert:
   "visits s e s' r t \<Longrightarrow> visits s (finsert ((aa, ba), b) e) s' r t"
 proof(induct t arbitrary: s' r)
   case Nil
   then show ?case
     by (simp add: visits_base)
 next
   case (Cons a t)
   then show ?case
     apply (simp add: visits_step)
     apply (erule fBexE)
     apply (rule_tac x=x in fBexI)
      apply auto[1]
     by (simp add: possible_steps_finsert)
 qed
 
 lemma reachable_finsert:
   "reachable s e \<Longrightarrow> reachable s (finsert ((aa, ba), b) e)"
   apply (simp add: reachable_def)
   by (meson visits_finsert)
 
 lemma reachable_finsert_contra:
   "\<not> reachable s (finsert ((aa, ba), b) e) \<Longrightarrow> \<not>reachable s e"
   using reachable_finsert by blast
 
 lemma visits_empty: "visits s e s' r [] = (s = s')"
   apply standard
   by (rule visits.cases, auto)
 
 definition "remove_state s e = ffilter (\<lambda>((from, to), t). from \<noteq> s \<and> to \<noteq> s) e"
 
 text_raw\<open>\snip{obtainable}{1}{2}{%\<close>
 inductive "obtains" :: "cfstate \<Rightarrow> registers \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> execution \<Rightarrow> bool" where
   base [simp]: "obtains s r e s r []" |
   step: "\<exists>(s'', T) |\<in>| possible_steps e s' r' l i. obtains s r e s'' (evaluate_updates T i r') t \<Longrightarrow>
          obtains s r e s' r' ((l, i)#t)"
 
 definition "obtainable s r e = (\<exists>t. obtains s r e 0 <> t)"
 text_raw\<open>}%endsnip\<close>
 
 lemma obtains_obtainable:
   "obtains s r e 0 <> t \<Longrightarrow> obtainable s r e"
   apply (simp add: obtainable_def)
   by auto
 
 lemma obtains_base: "obtains s r e s' r' [] = (s = s' \<and> r = r')"
   apply standard
   by (rule obtains.cases, auto)
 
 lemma obtains_step: "obtains s r e s' r' ((l, i)#t) = (\<exists>(s'', T) |\<in>| possible_steps e s' r' l i. obtains s r e s'' (evaluate_updates T i r') t)"
   apply standard
   by (rule obtains.cases, auto simp add: obtains.step)
 
 lemma obtains_recognises:
   "obtains s c e s' r t \<Longrightarrow> recognises_execution e s' r t"
 proof(induct t arbitrary: s' r)
   case Nil
   then show ?case
     by (simp add: obtains_base)
 next
   case (Cons a t)
   then show ?case
     apply (cases a)
     apply simp
     apply (rule obtains.cases)
       apply simp
      apply simp
     apply clarsimp
     using recognises_execution.step by fastforce
 qed
 
 lemma ex_comm4:
   "(\<exists>c1 s a b. (a, b) \<in> fset (possible_steps e s' r l i) \<and> obtains s c1 e a (evaluate_updates b i r) t) =
    (\<exists>a b s c1. (a, b) \<in> fset (possible_steps e s' r l i) \<and> obtains s c1 e a (evaluate_updates b i r) t)"
   by auto
 
 lemma recognises_execution_obtains:
   "recognises_execution e s' r t \<Longrightarrow> \<exists>c1 s. obtains s c1 e s' r t"
 proof(induct t arbitrary: s' r)
   case Nil
   then show ?case
     by (simp add: obtains_base)
 next
   case (Cons a t)
   then show ?case
     apply (cases a)
     apply (simp add: obtains_step)
     apply (rule recognises_execution.cases)
       apply simp
      apply simp
     apply clarsimp
     apply (simp add: fBex_def Bex_def ex_comm4)
     subgoal for _ _ aa ba
       apply (rule_tac x=aa in exI)
       apply (rule_tac x=ba in exI)
       apply (simp add: fmember_implies_member)
       by blast
     done  
 qed
 
 lemma obtainable_empty_efsm:
   "obtainable s c {||} = (s=0 \<and> c = <>)"
   apply (simp add: obtainable_def)
   apply standard
   apply (metis ffilter_empty no_outgoing_transitions no_step_none obtains.cases obtains_recognises step_None)
   using obtains_base by blast
 
 lemma obtains_visits: "obtains s r e s' r' t \<Longrightarrow> visits s e s' r' t"
 proof(induct t arbitrary: s' r')
   case Nil
   then show ?case
     by (simp add: obtains_base)
 next
   case (Cons a t)
   then show ?case
     apply (cases a)
     apply (rule obtains.cases)
       apply simp
      apply simp
     apply clarsimp
     apply (rule visits.step)
     by auto
 qed
 
 lemma unobtainable_if: "\<not> visits s e s' r' t \<Longrightarrow> \<not> obtains s r e s' r' t"
   using obtains_visits by blast
 
 lemma obtainable_if_unreachable: "\<not>reachable s e \<Longrightarrow> \<not>obtainable s r e"
   by (simp add: reachable_def obtainable_def unobtainable_if)
 
 lemma obtains_step_append:
   "obtains s r e s' r' t \<Longrightarrow>
   (s'', ta) |\<in>| possible_steps e s r l i \<Longrightarrow>
   obtains s'' (evaluate_updates ta i r) e s' r' (t @ [(l, i)])"
 proof(induct t arbitrary: s' r')
   case Nil
   then show ?case
     apply (simp add: obtains_base)
     apply (rule obtains.step)
     apply (rule_tac x="(s'', ta)" in fBexI)
     by auto
 next
   case (Cons a t)
   then show ?case
     apply simp
     apply (rule obtains.cases)
       apply simp
      apply simp
     apply clarsimp
     apply (rule obtains.step)
     by auto
 qed
 
 lemma reachable_if_obtainable_step:
   "obtainable s r e \<Longrightarrow> \<exists>l i t. (s', t) |\<in>| possible_steps e s r l i \<Longrightarrow> reachable s' e"
   apply (simp add: reachable_def obtainable_def)
   apply clarify
   subgoal for t l i
     apply (rule_tac x="t@[(l, i)]" in exI)
     using obtains_step_append unobtainable_if by blast
   done
 
 lemma possible_steps_remove_unreachable:
   "obtainable s r e \<Longrightarrow>
   \<not> reachable s' e \<Longrightarrow>
   possible_steps (remove_state s' e) s r l i = possible_steps e s r l i"
   apply standard
   apply (simp add: fsubset_eq)
    apply (rule fBallI)
    apply clarsimp
    apply (metis ffmember_filter in_possible_steps remove_state_def)
   apply (simp add: fsubset_eq)
    apply (rule fBallI)
   apply clarsimp
   subgoal for a b
     apply (case_tac "a = s'")
     using reachable_if_obtainable_step apply blast
     apply (simp add: remove_state_def)
     by (metis (mono_tags, lifting) ffmember_filter in_possible_steps obtainable_if_unreachable old.prod.case)
   done
 
 text_raw\<open>\snip{removeUnreachableArb}{1}{2}{%\<close>
 lemma executionally_equivalent_remove_unreachable_state_arbitrary:
   "obtainable s r e \<Longrightarrow> \<not> reachable s' e \<Longrightarrow> executionally_equivalent e s r (remove_state s' e) s r x"
 text_raw\<open>}%endsnip\<close>
 proof(induct x arbitrary: s r)
   case (Cons a x)
   then show ?case
     apply (cases a, simp)
     apply (rule executionally_equivalent.step)
     apply (simp add: possible_steps_remove_unreachable)
     apply standard
      apply clarsimp
     subgoal for aa b ab ba
       apply (rule_tac x="(ab, ba)" in fBexI)
        apply (metis (mono_tags, lifting) obtainable_def obtains_step_append case_prodI)
       apply simp
       done
     apply (rule fBallI)
     apply clarsimp
     apply (rule_tac x="(ab, ba)" in fBexI)
      apply simp
      apply (metis obtainable_def obtains_step_append possible_steps_remove_unreachable)
     by (simp add: possible_steps_remove_unreachable)
 qed auto
 
 text_raw\<open>\snip{removeUnreachable}{1}{2}{%\<close>
 lemma executionally_equivalent_remove_unreachable_state:
   "\<not> reachable s' e \<Longrightarrow> executionally_equivalent e 0 <> (remove_state s' e) 0 <> x"
 text_raw\<open>}%endsnip\<close>
   by (meson executionally_equivalent_remove_unreachable_state_arbitrary
       obtains.simps obtains_obtainable)
 
 subsection\<open>Transition Replacement\<close>
 text\<open>Here, we define the function \texttt{replace} to replace one transition with another, and prove
 some of its properties.\<close>
 
 definition "replace e1 old new = fimage (\<lambda>x. if x = old then new else x) e1"
 
 lemma replace_finsert:
   "replace (finsert ((aaa, baa), b) e1) old new = (if ((aaa, baa), b) = old then (finsert new (replace e1 old new)) else (finsert ((aaa, baa), b) (replace e1 old new)))"
   by (simp add: replace_def)
 
 lemma possible_steps_replace_unchanged:
   "((s, aa), ba) \<noteq> ((s1, s2), t1) \<Longrightarrow>
   (aa, ba) |\<in>| possible_steps e1 s r l i \<Longrightarrow>
   (aa, ba) |\<in>| possible_steps (replace e1 ((s1, s2), t1) ((s1, s2), t2)) s r l i"
   apply (simp add: in_possible_steps[symmetric] replace_def)
   by fastforce
 
 end