# 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"

no_notation relcomp (infixr "O" 75) and 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"

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
)"

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)

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
next
case (insert x e)
then show ?case
apply (case_tac x)
subgoal for a b
apply (case_tac a)
subgoal for aa _
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

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

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 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)|}"
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)"
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: 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
using possible_steps_alt_aux by force

lemma no_outgoing_transitions:
"ffilter (λ((s', _), _). s = s') e = {||} ⟹
possible_steps e s r l i = {||}"
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 (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

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 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)"

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 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 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 (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 (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 (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)"

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 (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
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)"

lemma random_member_singleton [simp]: "random_member {|a|} = Some a"

lemma random_member_is_member:
"random_member ss = Some s ⟹ s |∈| ss"
by (metis equalsffemptyI option.distinct(1) option.inject verit_sko_ex_indirect)

lemma random_member_None[simp]: "random_member ss = None = (ss = {||})"

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 (case_tac "possible_steps e s r a b")
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 (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 (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')"

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 (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"

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 (case_tac "possible_steps e s r l i")
apply simp
subgoal for x S'
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")
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 ⟹
observe_execution e s' r' es = obs ⟹
observe_execution e s r (h#es) = p#obs"

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))"

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) ⟹

(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))"

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 clarify
apply standard
apply (rule finite_UnI)+
using GExp.finite_enumerate_regs apply blast
using AExp.finite_enumerate_regs apply blast
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 clarify
apply (case_tac "(possible_steps e s r a b)")
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"

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]"

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)
)"
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)
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 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"

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"

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"

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)
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"
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)"

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)"

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)
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 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 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 (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
next
case (Cons a t)
then show ?case
apply (erule fBexE)
apply (rule_tac x=x in fBexI)
apply auto[1]
qed

lemma reachable_finsert:
"reachable s e ⟹ reachable s (finsert ((aa, ba), b) e)"
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"
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
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
next
case (Cons a t)
then show ?case
apply (cases a)
apply (rule recognises_execution.cases)
apply simp
apply simp
apply clarsimp
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 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
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 (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 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 (rule fBallI)
apply clarsimp
apply (metis ffmember_filter in_possible_steps remove_state_def)
apply (rule fBallI)
apply clarsimp
subgoal for a b
apply (case_tac "a = s'")
using reachable_if_obtainable_step apply blast
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 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)
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)))"