Theory EFSM

section ‹Extended Finite State Machines›

text‹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.›

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 × inputs)"
type_synonym execution = "action list"
type_synonym observation = "outputs list"
type_synonym transition_matrix = "((cfstate × cfstate) × transition) fset"

unbundle no relcomp_syntax
no_notation comp (infixl ‹o› 55)

type_synonym event = "(label × inputs × value list)"
type_synonym trace = "event list"
type_synonym log = "trace list"

definition Str :: "string ⇒ value" where
  "Str s ≡ value.Str (String.implode s)"

lemma str_not_num: "Str s ≠ Num x1"
  by (simp add: Str_def)

definition S :: "transition_matrix ⇒ nat fset" where
  "S m = (fimage (λ((s, s'), t). s) m) |∪| fimage (λ((s, s'), t). s') m"

lemma S_ffUnion: "S e = ffUnion (fimage (λ((s, s'), _). {|s, s'|}) e)"
  unfolding S_def
  by(induct e, auto)

subsection‹Possible Steps›
text‹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.›

definition possible_steps :: "transition_matrix ⇒ cfstate ⇒ registers ⇒ label ⇒ inputs ⇒ (cfstate × transition) fset" where
  "possible_steps e s r l i = fimage (λ((origin, dest), t). (dest, t)) (ffilter (λ((origin, dest), t). origin = s ∧ (Label t) = l ∧ (length i) = (Arity t) ∧ 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 ∧ (Label t) = l ∧ (length i) = (Arity t) ∧ 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 (λ((origin, dest), t). origin = s ∧ Label t = l ∧ can_take_transition t i r) e =
ffilter (λ((origin, dest), t). Label t = l ∧ can_take_transition t i r) (ffilter (λ((origin, dest), t). origin = s) e)"
  by auto

lemma split_label:
"ffilter (λ((origin, dest), t). origin = s ∧ Label t = l ∧ can_take_transition t i r) e =
ffilter (λ((origin, dest), t). origin = s ∧ can_take_transition t i r) (ffilter (λ((origin, dest), t). Label t = l) e)"
  by auto

lemma possible_steps_empty_guards_false:
  "∀((s1, s2), t) |∈| ffilter (λ((origin, dest), t). Label t = l) e. ¬can_take_transition t i r ⟹
  possible_steps e s r l i = {||}"
  apply (simp add: possible_steps_def can_take[symmetric] split_label)
  by (simp add: Abs_ffilter Ball_def)

lemma fmember_possible_steps: "(s', t) |∈| possible_steps e s r l i = (((s, s'), t) ∈ {((origin, dest), t) ∈ fset e. origin = s ∧ Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r)})"
  apply (simp add: possible_steps_def ffilter_def fimage_def Abs_fset_inverse)
  by force

lemma possible_steps_alt_aux:
  "possible_steps e s r l i = {|(d, t)|} ⟹
       ffilter (λ((origin, dest), t). origin = s ∧ Label t = l ∧ length i = Arity t ∧ 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 ∧ Label b = l ∧ length i = Arity b ∧ 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
     (λ((origin, dest), t). origin = s ∧ Label t = l ∧ length i = Arity t ∧ 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
     (λ((origin, dest), t). origin = s ∧ Label t = l ∧ 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
     (λ((origin, dest), t). origin = s ∧ Label t = l ∧ 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 (λ((origin, dest), t). Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r)) (ffilter (λ((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 "(λ((origin, dest), t). origin = s ∧ Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r))"])
  by (rule ext, auto)

lemma possible_steps_single_out:
"ffilter (λ((origin, dest), t). origin = s) e = {|((s, d), t)|} ⟹
Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r) ⟹
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) ∈ fset e. origin = s ∧ Label t = l ∧ length i = Arity t ∧ 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)|} ⟹
   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 = {||}) = (∀((origin, dest), t) ∈ fset e. origin ≠ s ∨ Label t ≠ l ∨ ¬ 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) |∈| e"
  using assms
  apply (simp add: fis_singleton_fthe_elem)
  using possible_steps_alt_aux by force

lemma no_outgoing_transitions:
"ffilter (λ((s', _), _). s = s') e = {||} ⟹
possible_steps e s r l i = {||}"
  apply (simp add: possible_steps_def)
  by (smt (verit, best) case_prod_beta eq_ffilter ffilter_empty ffmember_filter)

lemma ffilter_split: "ffilter (λ((origin, dest), t). origin = s ∧ Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r)) e =
                      ffilter (λ((origin, dest), t). Label t = l ∧ length i = Arity t ∧ apply_guards (Guards t) (join_ir i r)) (ffilter (λ((origin, dest), t). origin = s) e)"
  by auto

lemma one_outgoing_transition:
  defines "outgoing s ≡ (λ((origin, dest), t). origin = s)"
  assumes prem: "size (ffilter (outgoing s) e) = 1"
  shows "size (possible_steps e s r l i) ≤ 1"
proof-
  have less_eq_1: "⋀x::nat. (x ≤ 1) = (x = 1 ∨ x = 0)"
    by auto
  have size_empty: "⋀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‹Choice›
text‹Here we define the \texttt{choice} operator which determines whether or not two transitions are
nondeterministic.›

definition choice :: "transition ⇒ transition ⇒ bool" where
  "choice t t' = (∃ i r. apply_guards (Guards t) (join_ir i r) ∧ apply_guards (Guards t') (join_ir i r))"

definition choice_alt :: "transition ⇒ transition ⇒ bool" where
  "choice_alt t t' = (∃ 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 ⇒ bool" where
  "deterministic e = (∀s r l i. size (possible_steps e s r l i) ≤ 1)"

lemma deterministic_alt_aux: "size (possible_steps e s r l i) ≤ 1 =(
        possible_steps e s r l i = {||} ∨
        (∃s' t.
            ffilter
             (λ((origin, dest), t). origin = s ∧ Label t = l ∧ length i = Arity t ∧ 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 = (
  ∀s r l i.
    possible_steps e s r l i = {||} ∨
    (∃s' t. ffilter (λ((origin, dest), t). origin = s ∧ (Label t) = l ∧ (length i) = (Arity t) ∧ 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 ≤ 1 = (f = {||} ∨ (∃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: "∀x |∈| xs. ¬ P x ⟹ ffilter P xs = {||}"
  by auto

lemma empty_ffilter: "ffilter P xs = {||} = (∀x |∈| xs. ¬ P x)"
  by auto

lemma all_states_deterministic:
"(∀s l i r.
  ffilter (λ((origin, dest), t). origin = s ∧ (Label t) = l ∧ can_take_transition t i r) e = {||} ∨
  (∃x. ffilter (λ((origin, dest), t). origin = s ∧ (Label t) = l ∧ can_take_transition t i r) e = {|x|})
) ⟹ 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:
"∀i r l.
∀((a, b), t) |∈| ffilter (λ((origin, dest), t). origin = s) (finsert ((s, s'), t') e).
Label t = l ∧ can_take_transition t i r ⟶ ¬ can_take_transition t' i r ⟹
deterministic e ⟹
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: "(∀x |∈| xs. P x) = (ffilter P xs = xs)"
  by auto

lemma fsubset_if: "∀x. x |∈| f1 ⟶ x |∈| f2 ⟹ f1 |⊆| f2"
  by auto

lemma in_possible_steps: "(((s, s'), t)|∈|e ∧ Label t = l ∧ can_take_transition t i r) = ((s', t) |∈| possible_steps e s r l i)"
  apply (simp add: fmember_possible_steps)
  by (simp add: can_take_def can_take_transition_def)

lemma possible_steps_can_take_transition:
  "(s2, t1) |∈| possible_steps e1 s1 r l i ⟹ can_take_transition t1 i r"
  using in_possible_steps by blast

lemma not_deterministic:
  "∃s l i r.
    ∃d1 d2 t1 t2.
      d1 ≠ d2 ∧ t1 ≠ t2 ∧
      ((s, d1), t1) |∈| e ∧
      ((s, d2), t2) |∈| e ∧
      Label t1 = Label t2 ∧
      can_take_transition t1 i r ∧
      can_take_transition t2 i r ⟹
  ¬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) |∈| possible_steps e s r (Label t1) i")
     defer using in_possible_steps apply blast
    apply (case_tac "(d2, t2) |∈| 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:
  "¬deterministic e ⟹
  ∃s l i r.
    ∃d1 d2 t1 t2.
      (d1 ≠ d2 ∨ t1 ≠ t2) ∧
      ((s, d1), t1) |∈| e ∧
      ((s, d2), t2) |∈| e ∧
      Label t1 = Label t2 ∧
      can_take_transition t1 i r ∧
      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 "∃e1 e2 f'. e1 ≠ e2 ∧ 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 finsertCI in_possible_steps)
      done
    done
  done

lemma deterministic_if:
"∄s l i r.
  ∃d1 d2 t1 t2.
    (d1 ≠ d2 ∨ t1 ≠ t2) ∧
    ((s, d1), t1) |∈| e ∧
    ((s, d2), t2) |∈| e ∧
    Label t1 = Label t2 ∧
    can_take_transition t1 i r ∧
    can_take_transition t2 i r ⟹
  deterministic e"
  using not_deterministic_conv by blast

lemma "∀l i r.
  (∀((s, s'), t) |∈| e. Label t = l ∧ can_take_transition t i r ∧
  (∄t' s''. ((s, s''), t') |∈| e ∧ (s' ≠ s'' ∨ t' ≠ t) ∧ Label t' = l ∧ can_take_transition t' i r))
 ⟹ 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 "∃t s'. ((s, s'), t)|∈|e ∧ Label t = l ∧ can_take_transition t i r")
   defer 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 (λ((o, _), _). o = s) e"

lemma in_outgoing: "((s1, s2), t) |∈| outgoing_transitions e s = (((s1, s2), t) |∈| e ∧ s1 = s)"
  by (auto simp add: outgoing_transitions_def)

lemma outgoing_transitions_deterministic:
  "∀s.
    ∀((s1, s2), t) |∈| outgoing_transitions e s.
      ∀((s1', s2'), t') |∈| outgoing_transitions e s.
        s2 ≠ s2' ∨ t ≠ t' ⟶ Label t = Label t' ⟶ ¬ choice t t' ⟹ deterministic e"
  apply (rule deterministic_if)
  apply simp
  apply (rule allI)
  subgoal for s
    apply (erule_tac x=s in allE)
    apply (simp add: 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) ∈ 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
        by (simp add: outgoing_transitions_def)
      done
    done
  done

lemma outgoing_transitions_deterministic2: "(⋀s a b ba aa bb bc.
       ((a, b), ba) |∈| outgoing_transitions e s ⟹
       ((aa, bb), bc) |∈| (outgoing_transitions e s) - {|((a, b), ba)|} ⟹ b ≠ bb ∨ ba ≠ bc ⟹ ¬choice ba bc)
        ⟹ deterministic e"
  apply (rule outgoing_transitions_deterministic)
  by blast

lemma outgoing_transitions_fprod_deterministic:
"(⋀s b ba bb bc.
(((s, b), ba), ((s, bb), bc)) ∈ fset (outgoing_transitions e s) × fset (outgoing_transitions e s)
⟹ b ≠ bb ∨ ba ≠ bc ⟹ Label ba = Label bc ⟹ ¬choice ba bc)
⟹ deterministic e"
  apply (rule outgoing_transitions_deterministic)
  apply clarify
  by (metis SigmaI in_outgoing)

text‹The \texttt{random\_member} function returns a random member from a finite set, or
\texttt{None}, if the set is empty.›
definition random_member :: "'a fset ⇒ 'a option" where
  "random_member f = (if f = {||} then None else Some (Eps (λx. x |∈| f)))"

lemma random_member_nonempty: "s ≠ {||} = (random_member s ≠ 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 ⟹ s |∈| 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 ⇒ cfstate ⇒ registers ⇒ label ⇒ inputs ⇒ (transition × cfstate × outputs × registers) option" where
  "step e s r l i = (case random_member (possible_steps e s r l i) of
      None ⇒ None |
      Some (s', t) ⇒  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 ≠ None ⟹
   ∃aa ba. (aa, ba) |∈| 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') ⟹ (s', t) |∈| 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') ⟹ 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) ⟹
   random_member possibilities = Some (s', t) ⟹
   evaluate_outputs t i r = p ⟹
   evaluate_updates t i r = r' ⟹
   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) ∧
    evaluate_outputs t i r = p ∧
    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 = {||} ⟹ step e s r l i = None"
  by (simp add: step_def random_member_def)

subsection‹Execution Observation›
text‹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}.›

text_raw‹\snip{observe}{1}{2}{%›
fun observe_execution :: "transition_matrix ⇒ cfstate ⇒ registers ⇒ execution ⇒ 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 (λx. x |∈| viable) in
      (evaluate_outputs t i r)#(observe_execution e s' (evaluate_updates t i r) as)
    )"
text_raw‹}%endsnip›

lemma observe_execution_step_def: "observe_execution e s r ((l, i)#as)  = (
    case step e s r l i of
      None ⇒ []|
      Some (t, s', p, r') ⇒ 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 ∨ xa |∈| 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) ⟹
   step e1 s1 r1 l i = Some (t, s', p, r') ⟹
   ∃(s2', t2)|∈|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') ⟹
   observe_execution e s' r' es = obs ⟹
   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 |∈| possible_steps e s r a b")
    by (simp add: random_member_def)
  done

lemma observe_execution_possible_step:
  "possible_steps e s r (fst h) (snd h) = {|(s', t)|} ⟹
   apply_outputs (Outputs t) (join_ir (snd h) r) = p ⟹
   apply_updates (Updates t) (join_ir (snd h) r) r = r' ⟹
   observe_execution e s' r' es = obs ⟹
   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) = {||} ⟹
   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) = {||} ⟹
   possible_steps e2 s2 r2 (fst h) (snd h) = {||} ⟹
   (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)|} ⟹
   possible_steps e2 s2 r (fst h) (snd h) = {|(s2', t2)|} ⟹
   apply_outputs (Outputs t1) (join_ir (snd h) r) = apply_outputs (Outputs t2) (join_ir (snd h) r) ⟹

   apply_updates (Updates t1) (join_ir (snd h) r) r = r' ⟹
   apply_updates (Updates t2) (join_ir (snd h) r) r = r' ⟹
   (observe_execution e1 s1' r' t) = (observe_execution e2 s2' r' t) ⟹
   (observe_execution e1 s1 r (h#t)) = (observe_execution e2 s2 r (h#t))"
  by (simp add: observe_execution_possible_step)

subsubsection‹Utilities›
text‹Here we define some utility functions to access the various key properties of a given EFSM.›

definition max_reg :: "transition_matrix ⇒ nat option" where
  "max_reg e = (let maxes = (fimage (λ(_, t). Transition.max_reg t) e) in if maxes = {||} then None else fMax maxes)"

definition enumerate_ints :: "transition_matrix ⇒ int set" where
  "enumerate_ints e = ⋃ (image (λ(_, t). Transition.enumerate_ints t) (fset e))"

definition max_int :: "transition_matrix ⇒ int" where
  "max_int e = Max (insert 0 (enumerate_ints e))"

definition max_output :: "transition_matrix ⇒ nat" where
  "max_output e = fMax (fimage (λ(_, t). length (Outputs t)) e)"

definition all_regs :: "transition_matrix ⇒ nat set" where
  "all_regs e = ⋃ (image (λ(_, t). enumerate_regs t) (fset e))"

text_raw‹\snip{finiteRegs}{1}{2}{%›
lemma finite_all_regs: "finite (all_regs e)"
text_raw‹}%endsnip›
  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 ⇒ nat option" where
  "max_input e = fMax (fimage (λ(_, t). Transition.max_input t) e)"

fun maxS :: "transition_matrix ⇒ nat" where
  "maxS t = (if t = {||} then 0 else fMax ((fimage (λ((origin, dest), t). origin) t) |∪| (fimage (λ((origin, dest), t). dest) t)))"

subsection‹Execution Recognition›
text‹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.›

text_raw‹\snip{recognises}{1}{2}{%›
inductive recognises_execution :: "transition_matrix ⇒ nat ⇒ registers ⇒ execution ⇒ bool" where
  base [simp]: "recognises_execution e s r []" |
  step: "∃(s', T) |∈| possible_steps e s r l i.
         recognises_execution e s' (evaluate_updates T i r) t ⟹
         recognises_execution e s r ((l, i)#t)"
text_raw‹}%endsnip›

abbreviation "recognises e t ≡ recognises_execution e 0 <> t"

definition "E e = {x. recognises e x}"

lemma no_possible_steps_rejects:
  "possible_steps e s r l i = {||} ⟹ ¬ 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) =
   (∃(s', T) |∈| 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 ⇒ nat ⇒ registers ⇒ execution ⇒ 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
    (∃(s', T) |∈| 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) ⟹
   ∃aa ba. (aa, ba) |∈| 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) ⟹ possible_steps e s r (fst h) (snd h) ≠ {||}"
  apply (rule recognises_execution.cases)
  by auto

lemma recognises_must_be_step:
  "recognises_execution e s r (h#ts) ⟹
   ∃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 ∨ xa |∈| S'")
      by simp
    done
  done

lemma recognises_cons_step:
  "recognises_execution e s r (h # t) ⟹ step e s r (fst h) (snd h) ≠  None"
  by (simp add: recognises_must_be_step)

lemma no_step_none:
  "step e s r aa ba = None ⟹ ¬ 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 ⟹ ¬ recognises_execution e s r (h#t)"
  using no_step_none surjective_pairing by fastforce

lemma trace_reject:
  "(¬ recognises_execution e s r ((l, i)#t)) = (possible_steps e s r l i = {||} ∨ (∀(s', T) |∈| possible_steps e s r l i. ¬ 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) = {||} ⟹ ¬ recognises_execution e s r (a#t)"
  using recognises_possible_steps_not_empty by auto

lemma trace_reject_later:
  "∀(s', T) |∈| possible_steps e s r l i. ¬ recognises_execution e s' (evaluate_updates T i r) t ⟹
   ¬ recognises_execution e s r ((l, i)#t)"
  using trace_reject by auto

lemma recognition_prefix_closure: "recognises_execution e s r (t@t') ⟹ 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: "¬ recognises_execution e s r t ⟹ ¬ recognises_execution e s r (t @ t')"
  using recognition_prefix_closure by blast

lemma recognises_head: "recognises_execution e s r (h#t) ⟹ recognises_execution e s r [h]"
  by (simp add: recognition_prefix_closure)

subsubsection‹Trace Acceptance›
text‹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.›

text_raw‹\snip{accepts}{1}{2}{%›
inductive accepts_trace :: "transition_matrix ⇒ cfstate ⇒ registers ⇒ trace ⇒ bool" where
  base [simp]: "accepts_trace e s r []" |
  step: "∃(s', T) |∈| possible_steps e s r l i.
         evaluate_outputs T i r = map Some p ∧ accepts_trace e s' (evaluate_updates T i r) t ⟹
         accepts_trace e s r ((l, i, p)#t)"
text_raw‹}%endsnip›

text_raw‹\snip{T}{1}{2}{%›
definition T :: "transition_matrix ⇒ trace set" where
  "T e = {t. accepts_trace e 0 <> t}"
text_raw‹}%endsnip›

abbreviation "rejects_trace e s r t ≡ ¬ accepts_trace e s r t"

lemma accepts_trace_step:
  "accepts_trace e s r ((l, i, p)#t) = (∃(s', T) |∈| possible_steps e s r l i.
         evaluate_outputs T i r = map Some p ∧
         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) ⟹
       ∃(s1', t1)|∈|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) = (
  (∀(s', T) |∈| possible_steps e s r l i.  evaluate_outputs T i r ≠ map Some p ∨ rejects_trace e s' (evaluate_updates T i r) t)
)"
  apply (simp add: accepts_trace_step)
  by auto

definition accepts_log :: "trace set ⇒ transition_matrix ⇒ bool" where
  "accepts_log l e = (∀t ∈ l. accepts_trace e 0 <> t)"

text_raw‹\snip{prefixClosure}{1}{2}{%›
lemma prefix_closure: "accepts_trace e s r (t@t') ⟹ accepts_trace e s r t"
text_raw‹}%endsnip›
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‹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.›
fun accepts_trace_prim :: "transition_matrix ⇒ cfstate ⇒ registers ⇒ trace ⇒ 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
      (∃(s', T) |∈| poss_steps.
         evaluate_outputs T i r = (map Some p) ∧
         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‹EFSM Comparison›
text‹Here, we define some different metrics of EFSM equality.›

subsubsection‹State Isomporphism›
text‹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.›

definition isomorphic :: "transition_matrix ⇒ transition_matrix ⇒ bool" where
  "isomorphic e1 e2 = (∃f. bij f ∧ (∀((s1, s2), t) |∈| e1. ((f s1, f s2), t) |∈| e2))"

subsubsection‹Register Isomporphism›
text‹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.›
definition rename_regs :: "(nat ⇒ nat) ⇒ transition_matrix ⇒ transition_matrix" where
  "rename_regs f e = fimage (λ(tf, t). (tf, Transition.rename_regs f t)) e"

definition eq_upto_rename_strong :: "transition_matrix ⇒ transition_matrix ⇒ bool" where
  "eq_upto_rename_strong e1 e2 = (∃f. bij f ∧ rename_regs f e1 = e2)"

subsubsection‹Trace Simulation›
text‹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$.›

text_raw‹\snip{traceSim}{1}{2}{%›
inductive trace_simulation :: "(cfstate ⇒ cfstate) ⇒ transition_matrix ⇒ cfstate ⇒ registers ⇒
transition_matrix ⇒ cfstate ⇒ registers ⇒ trace ⇒ bool" where
  base: "s2 = f s1 ⟹ trace_simulation f e1 s1 r1 e2 s2 r2 []" |
  step: "s2 = f s1 ⟹
         ∀(s1', t1) |∈| ffilter (λ(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i).
           ∃(s2', t2) |∈| possible_steps e2 s2 r2 l i. evaluate_outputs t2 i r2 = map Some o ∧
            trace_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es ⟹
         trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es)"
text_raw‹}%endsnip›

lemma trace_simulation_step:
"trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es) = (
  (s2 = f s1) ∧ (∀(s1', t1) |∈| ffilter (λ(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i).
         (∃(s2', t2) |∈| possible_steps e2 s2 r2 l i. evaluate_outputs t2 i r2 = map Some o ∧
         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 fastforce

lemma trace_simulation_step_none:
  "s2 = f s1 ⟹
   ∄(s1', t1) |∈| possible_steps e1 s1 r1 l i. evaluate_outputs t1 i r1 = map Some o ⟹
   trace_simulation f e1 s1 r1 e2 s2 r2 ((l, i, o)#es)"
  apply (rule trace_simulation.step)
   apply simp
  apply (case_tac "ffilter (λ(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 = (∃f. ∀t. trace_simulation f e1 0 <> e2 0 <> t)"

lemma rejects_trace_simulation:
  "rejects_trace e2 s2 r2 t ⟹
   accepts_trace e1 s1 r1 t ⟹
   ¬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 l o _ _ i
      by blast
    done
qed

lemma accepts_trace_simulation:
  "accepts_trace e1 s1 r1 t ⟹
   trace_simulation f e1 s1 r1 e2 s2 r2 t ⟹
   accepts_trace e2 s2 r2 t"
  using rejects_trace_simulation by blast

lemma simulates_trace_subset: "trace_simulates e1 e2 ⟹ T e1 ⊆ T e2"
  using T_def accepts_trace_simulation trace_simulates_def by fastforce

subsubsection‹Trace Equivalence›
text‹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.›

text_raw‹\snip{traceEquiv}{1}{2}{%›
definition "trace_equivalent e1 e2 = (T e1 = T e2)"
text_raw‹}%endsnip›

text_raw‹\snip{simEquiv}{1}{2}{%›
lemma simulation_implies_trace_equivalent:
  "trace_simulates e1 e2 ⟹ trace_simulates e2 e1 ⟹ trace_equivalent e1 e2"
text_raw‹}%endsnip›
  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 ⟹
   trace_equivalent e2 e3 ⟹
   trace_equivalent e1 e3"
  by (simp add: trace_equivalent_def)

text‹Two EFSMs are trace equivalent if they accept the same traces.›
lemma trace_equivalent:
  "∀t. accepts_trace e1 0 <> t = accepts_trace e2 0 <> t ⟹ trace_equivalent e1 e2"
  by (simp add: T_def trace_equivalent_def)

lemma accepts_trace_step_2: "(s2', t2) |∈| possible_steps e2 s2 r2 l i ⟹
       accepts_trace e2 s2' (evaluate_updates t2 i r2) t ⟹
       evaluate_outputs t2 i r2 = map Some p ⟹
       accepts_trace e2 s2 r2 ((l, i, p)#t)"
  by (rule accepts_trace.step, auto)

subsubsection‹Execution Simulation›
text‹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.›

text_raw‹\snip{execSim}{1}{2}{%›
inductive execution_simulation :: "(cfstate ⇒ cfstate) ⇒ transition_matrix ⇒ cfstate ⇒
registers ⇒ transition_matrix ⇒ cfstate ⇒ registers ⇒ execution ⇒ bool" where
  base: "s2 = f s1 ⟹ execution_simulation f e1 s1 r1 e2 s2 r2 []" |
  step: "s2 = f s1 ⟹
         ∀(s1', t1) |∈| (possible_steps e1 s1 r1 l i).
           ∃(s2', t2) |∈| possible_steps e2 s2 r2 l i.
            evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
            execution_simulation f e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es ⟹
         execution_simulation f e1 s1 r1 e2 s2 r2 ((l, i)#es)"
text_raw‹}%endsnip›

definition "execution_simulates e1 e2 = (∃f. ∀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 ∧
 (∀(s1', t1) |∈| (possible_steps e1 s1 r1 l i).
         (∃(s2', t2) |∈| possible_steps e2 s2 r2 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
         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‹\snip{execTraceSim}{1}{2}{%›
lemma execution_simulation_trace_simulation:
  "execution_simulation f e1 s1 r1 e2 s2 r2 (map (λ(l, i, o). (l, i)) t) ⟹
   trace_simulation f e1 s1 r1 e2 s2 r2 t"
text_raw‹}%endsnip›
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 ⟹ trace_simulates e1 e2"
  apply (simp add: execution_simulates_def trace_simulates_def)
  using execution_simulation_trace_simulation by blast

subsubsection‹Executional Equivalence›
text‹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.›

text_raw‹\snip{execEquiv}{1}{2}{%›
inductive executionally_equivalent :: "transition_matrix ⇒ cfstate ⇒ registers ⇒
transition_matrix ⇒ cfstate ⇒ registers ⇒ execution ⇒ bool" where
  base [simp]: "executionally_equivalent e1 s1 r1 e2 s2 r2 []" |
  step: "∀(s1', t1) |∈| possible_steps e1 s1 r1 l i.
           ∃(s2', t2) |∈| possible_steps e2 s2 r2 l i.
             evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
             executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es ⟹
         ∀(s2', t2) |∈| possible_steps e2 s2 r2 l i.
           ∃(s1', t1) |∈| possible_steps e1 s1 r1 l i.
             evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
             executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es ⟹
         executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es)"
text_raw‹}%endsnip›

lemma executionally_equivalent_step:
"executionally_equivalent e1 s1 r1 e2 s2 r2 ((l, i)#es) = (
  (∀(s1', t1) |∈| (possible_steps e1 s1 r1 l i). (∃(s2', t2) |∈| possible_steps e2 s2 r2 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
   executionally_equivalent e1 s1' (evaluate_updates t1 i r1) e2 s2' (evaluate_updates t2 i r2) es)) ∧
  (∀(s2', t2) |∈| (possible_steps e2 s2 r2 l i). (∃(s1', t1) |∈| possible_steps e1 s1 r1 l i. evaluate_outputs t1 i r1 = evaluate_outputs t2 i r2 ∧
   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 = {||} ⟹
   possible_steps e2 s2 r2 l i = {||} ⟹
  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 ≠ {||} ⟹
   possible_steps e2 s2 r2 l i = {||} ⟹
   ¬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 (λ(l, i, o). (l, i)) t) ⟹
   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 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
    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:
  "∀x. executionally_equivalent e1 s1 r1 e2 s2 r2 x ⟹ accepts_trace e1 s1 r1  t ⟹ accepts_trace e2 s2 r2 t"
  using executionally_equivalent_acceptance_map by blast

lemma executionally_equivalent_trace_equivalent:
  "∀x. executionally_equivalent e1 0 <> e2 0 <> x ⟹ trace_equivalent e1 e2"
  apply (rule trace_equivalent)
  apply clarify
  subgoal for t apply (erule_tac x="map (λ(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 ⟹
   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 ⟹
   executionally_equivalent e2 s2 r2 e3 s3 r3 x ⟹
   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‹Reachability›
text‹Here, we define the function \texttt{visits} which returns true if the given execution
leaves the given EFSM in the given state.›

text_raw‹\snip{reachable}{1}{2}{%›
inductive visits :: "cfstate ⇒ transition_matrix ⇒ cfstate ⇒ registers ⇒ execution ⇒ bool" where
  base [simp]: "visits s e s r []" |
  step: "∃(s', T) |∈| possible_steps e s r l i. visits target e s' (evaluate_updates T i r) t ⟹
         visits target e s r ((l, i)#t)"

definition "reachable s e = (∃t. visits s e 0 <> t)"
text_raw‹}%endsnip›

lemma no_further_steps:
  "s ≠ s' ⟹ ¬ 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) = (∃(s', T) |∈| 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 ⟹ 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 ⟹ reachable s (finsert ((aa, ba), b) e)"
  apply (simp add: reachable_def)
  by (meson visits_finsert)

lemma reachable_finsert_contra:
  "¬ reachable s (finsert ((aa, ba), b) e) ⟹ ¬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 (λ((from, to), t). from ≠ s ∧ to ≠ s) e"

text_raw‹\snip{obtainable}{1}{2}{%›
inductive "obtains" :: "cfstate ⇒ registers ⇒ transition_matrix ⇒ cfstate ⇒ registers ⇒ execution ⇒ bool" where
  base [simp]: "obtains s r e s r []" |
  step: "∃(s'', T) |∈| possible_steps e s' r' l i. obtains s r e s'' (evaluate_updates T i r') t ⟹
         obtains s r e s' r' ((l, i)#t)"

definition "obtainable s r e = (∃t. obtains s r e 0 <> t)"
text_raw‹}%endsnip›

lemma obtains_obtainable:
  "obtains s r e 0 <> t ⟹ obtainable s r e"
  apply (simp add: obtainable_def)
  by auto

lemma obtains_base: "obtains s r e s' r' [] = (s = s' ∧ r = r')"
  apply standard
  by (rule obtains.cases, auto)

lemma obtains_step: "obtains s r e s' r' ((l, i)#t) = (∃(s'', T) |∈| 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 ⟹ 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:
  "(∃c1 s a b. (a, b) ∈ fset (possible_steps e s' r l i) ∧ obtains s c1 e a (evaluate_updates b i r) t) =
   (∃a b s c1. (a, b) ∈ fset (possible_steps e s' r l i) ∧ obtains s c1 e a (evaluate_updates b i r) t)"
  by auto

lemma recognises_execution_obtains:
  "recognises_execution e s' r t ⟹ ∃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: Bex_def ex_comm4)
    subgoal for _ _ aa ba
      apply (rule_tac x=aa in exI)
      apply (rule_tac x=ba in exI)
      apply simp
      by blast
    done  
qed

lemma obtainable_empty_efsm:
  "obtainable s c {||} = (s=0 ∧ 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 ⟹ 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: "¬ visits s e s' r' t ⟹ ¬ obtains s r e s' r' t"
  using obtains_visits by blast

lemma obtainable_if_unreachable: "¬reachable s e ⟹ ¬obtainable s r e"
  by (simp add: reachable_def obtainable_def unobtainable_if)

lemma obtains_step_append:
  "obtains s r e s' r' t ⟹
  (s'', ta) |∈| possible_steps e s r l i ⟹
  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 ⟹ ∃l i t. (s', t) |∈| possible_steps e s r l i ⟹ 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 ⟹
  ¬ reachable s' e ⟹
  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‹\snip{removeUnreachableArb}{1}{2}{%›
lemma executionally_equivalent_remove_unreachable_state_arbitrary:
  "obtainable s r e ⟹ ¬ reachable s' e ⟹ executionally_equivalent e s r (remove_state s' e) s r x"
text_raw‹}%endsnip›
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‹\snip{removeUnreachable}{1}{2}{%›
lemma executionally_equivalent_remove_unreachable_state:
  "¬ reachable s' e ⟹ executionally_equivalent e 0 <> (remove_state s' e) 0 <> x"
text_raw‹}%endsnip›
  by (meson executionally_equivalent_remove_unreachable_state_arbitrary
      obtains.simps obtains_obtainable)

subsection‹Transition Replacement›
text‹Here, we define the function \texttt{replace} to replace one transition with another, and prove
some of its properties.›

definition "replace e1 old new = fimage (λ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) ≠ ((s1, s2), t1) ⟹
  (aa, ba) |∈| possible_steps e1 s r l i ⟹
  (aa, ba) |∈| possible_steps (replace e1 ((s1, s2), t1) ((s1, s2), t2)) s r l i"
  by (simp add: in_possible_steps[symmetric] replace_def)

end