# Theory Backwards_Reachability_Analysis

```section ‹Backwards Reachability Analysis›

text ‹This theory introduces function @{text "select_inputs"} which is used for the calculation of
both state preambles and state separators.›

theory Backwards_Reachability_Analysis
imports "../FSM"
begin

text ‹Function @{text "select_inputs"} calculates an associative list that maps states to a single
input each such that the FSM induced by this input selection is acyclic, single input and
whose only deadlock states (if any) are contained in @{text "stateSet"}.
The following parameters are used:
1) transition function @{text "f"} (typically @{text "(h M)"} for some FSM @{text "M"})
2) a source state @{text "q0"} (selection terminates as soon as this states is assigned some input)
3) a list of inputs that may be assigned to states
4) a list of states not yet taken (these are considered when searching for the next possible
assignment)
5) a set @{text "stateSet"} of all states that already have an input assigned to them by @{text "m"}
6) an associative list @{text "m"} containing previously chosen assignments›

function select_inputs :: "(('a × 'b) ⇒ ('c × 'a) set) ⇒ 'a ⇒ 'b list ⇒ 'a list ⇒ 'a set ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where
"select_inputs f q0 inputList [] stateSet m = (case find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList of
Some x ⇒ m@[(q0,x)] |
None   ⇒ m)" |
"select_inputs f q0 inputList (n#nL) stateSet m =
(case find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList of
Some x ⇒ m@[(q0,x)] |
None   ⇒ (case find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList
of None            ⇒ m |
Some (q',x,stateList') ⇒ select_inputs f q0 inputList stateList' (insert q' stateSet) (m@[(q',x)])))"
by pat_completeness auto
termination
proof -
{
fix f :: "(('a × 'b) ⇒ ('c × 'a) set)"
fix q0 :: 'a
fix inputList :: "'b list"
fix n :: 'a
fix nL :: "'a list"
fix stateSet :: "'a set"
fix m :: "('a × 'b) list"
fix qynL' q ynL' x nL'
assume "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None"
and "find_remove_2 (λq' x. f (q', x) ≠ {} ∧ (∀(y, q'')∈f (q', x). q'' ∈ stateSet)) (n # nL) inputList = Some qynL'"
and "(q, ynL') = qynL'"
and "(x, nL') = ynL'"

then have *: "find_remove_2 (λq' x. f (q', x) ≠ {} ∧ (∀(y, q'')∈f (q', x). q'' ∈ stateSet)) (n # nL) inputList = Some (q,x,nL')"
by auto

have "q ∈ set (n # nL)"
and  "nL' = remove1 q (n # nL)"
using find_remove_2_set(2,6)[OF *] by simp+

then have "length nL' < length (n # nL)"
using remove1_length by metis

then have "((f, q0, inputList, nL', insert q stateSet, m @ [(q, x)]), f, q0, inputList, n # nL, stateSet, m)
∈ measure (λ(f, q0, iL, nL, nS, m). length nL)"
by auto
}
then show ?thesis
by (relation "measure (λ (f,q0,iL,nL,nS,m) . length nL)"; simp)
qed

lemma select_inputs_length :
"length (select_inputs f q0 inputList stateList stateSet m) ≤ (length m) + Suc (length stateList)"
proof (induction "length stateList" arbitrary: stateList stateSet m)
case 0
then show ?case
by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
case (Suc k)
then obtain n nL where "stateList = n # nL"
by (meson Suc_length_conv)

show ?case
proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
case None
then show ?thesis
proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
case None
then show ?thesis
using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None›
unfolding ‹stateList = n # nL› by auto
next
case (Some a)
then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList
= Some (q',x,stateList')"
unfolding ‹stateList = n # nL› by (metis prod_cases3)
have "k = length stateList'"
using find_remove_2_length[OF *] ‹Suc k = length stateList›
unfolding ‹stateList = n # nL›
by simp
show ?thesis
using Suc.hyps(1)[of stateList' "insert q' stateSet" "m@[(q',x)]", OF ‹k = length stateList'›]
unfolding ‹stateList = n # nL› select_inputs.simps None * find_remove_2_length[OF *]
by simp
qed
next
case (Some a)
then show ?thesis
unfolding ‹stateList = n # nL› by auto
qed
qed

lemma select_inputs_length_min :
"length (select_inputs f q0 inputList stateList stateSet m) ≥ (length m)"
proof (induction "length stateList" arbitrary: stateList stateSet m)
case 0
then show ?case
by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
case (Suc k)
then obtain n nL where "stateList = n # nL"
by (meson Suc_length_conv)

show ?case
proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
case None
then show ?thesis
proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
case None
then show ?thesis using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None›
unfolding ‹stateList = n # nL› by auto
next
case (Some a)
then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList
= Some (q',x,stateList')"
unfolding ‹stateList = n # nL› by (metis prod_cases3)
have "k = length stateList'"
using find_remove_2_length[OF *] ‹Suc k = length stateList›
unfolding ‹stateList = n # nL›
by simp
show ?thesis
unfolding ‹stateList = n # nL› select_inputs.simps None * find_remove_2_length[OF *]
using Suc.hyps(1)[of stateList' "m@[(q',x)]" "insert q' stateSet" , OF ‹k = length stateList'›]
by simp
qed
next
case (Some a)
then show ?thesis unfolding ‹stateList = n # nL› by auto
qed
qed

lemma select_inputs_helper1 :
"find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = Some x
⟹ (select_inputs f q0 iL nL nS m) = m@[(q0,x)]"
by (cases nL; auto)

lemma select_inputs_take :
"take (length m) (select_inputs f q0 inputList stateList stateSet m) = m"
proof (induction "length stateList" arbitrary: stateList stateSet m)
case 0
then show ?case
by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList"; auto)
next
case (Suc k)
then obtain n nL where "stateList = n # nL"
by (meson Suc_length_conv)

show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ stateSet))) inputList")
case None
then show ?thesis
proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) stateList inputList")
case None
then show ?thesis using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ stateSet)) inputList = None›
unfolding ‹stateList = n # nL› by auto
next
case (Some a)
then obtain q' x stateList' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ stateSet))) (n#nL) inputList
= Some (q',x,stateList')"
unfolding ‹stateList = n # nL›
by (metis prod_cases3)
have "k = length stateList'"
using find_remove_2_length[OF *] ‹Suc k = length stateList›
unfolding ‹stateList = n # nL›
by simp

have **: "(select_inputs f q0 inputList stateList stateSet m)
= select_inputs f q0 inputList stateList' (insert q' stateSet) (m @ [(q', x)])"
unfolding ‹stateList = n # nL› select_inputs.simps None *
by simp
show ?thesis
unfolding **
using Suc.hyps(1)[of stateList' "m@[(q',x)]" "insert q' stateSet" , OF ‹k = length stateList'›]
by (metis butlast_snoc butlast_take diff_Suc_1 length_append_singleton select_inputs_length_min)
qed
next
case (Some a)
then show ?thesis unfolding ‹stateList = n # nL› by auto
qed
qed

lemma select_inputs_take' :
"take (length m) (select_inputs f q0 iL nL nS (m@m')) = m"
using select_inputs_take
by (metis (no_types, lifting) add_leE append_eq_append_conv select_inputs_length_min length_append

lemma select_inputs_distinct :
assumes "distinct (map fst m)"
and     "set (map fst m) ⊆ nS"
and     "q0 ∉ nS"
and     "distinct nL"
and     "q0 ∉ set nL"
and     "set nL ∩ nS = {}"
shows "distinct (map fst (select_inputs f q0 iL nL nS m))"
using assms proof (induction "length nL" arbitrary: nL nS m)
case 0
then show ?case
by (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL"; auto)
next
case (Suc k)
then obtain n nL'' where "nL = n # nL''"
by (meson Suc_length_conv)

show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL")
case None
then show ?thesis
proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
case None
then have "(select_inputs f q0 iL nL nS m) = m"
using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None›
unfolding ‹nL = n # nL''› by auto
then show ?thesis
using Suc.prems by auto
next
case (Some a)
then obtain q' x nL' where *: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL
= Some (q',x,nL')"
by (metis prod_cases3)

have "k = length nL'"
using find_remove_2_length[OF *] ‹Suc k = length nL›
by simp

have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])"
using *
unfolding  ‹nL = n # nL''› select_inputs.simps None
by auto

have "q' ∈ set nL"
and  "set nL' = set nL - {q'}"
and  "distinct nL'"
using find_remove_2_set[OF * ]  ‹distinct nL› by auto

have "distinct (map fst (m@[(q',x)]))"
using ‹(set (map fst m)) ⊆ nS› ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)›
by auto
have "q0 ∉ insert q' nS"
using Suc.prems(3) Suc.prems(5) ‹q' ∈ set nL› by auto
have "set (map fst (m@[(q',x)])) ⊆ insert q' nS"
using ‹(set (map fst m)) ⊆ nS› by auto
have "(set (map fst (m@[(q',x)]))) ⊆ insert q' nS"
using‹(set (map fst m)) ⊆ nS› by auto
have "q0 ∉ set nL'"
by (simp add: Suc.prems(5) ‹set nL' = set nL - {q'}›)
have "set nL' ∩ insert q' nS = {}"
using Suc.prems(6) ‹set nL' = set nL - {q'}› by auto

show ?thesis
unfolding select_inputs.simps None *
using Suc.hyps(1)[OF ‹k = length nL'› ‹distinct (map fst (m@[(q',x)]))›
‹set (map fst (m@[(q',x)])) ⊆ insert q' nS›
‹q0 ∉ insert q' nS›
‹distinct nL'›
‹q0 ∉ set nL'›
‹set nL' ∩ insert q' nS = {}›]
unfolding ‹select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])›
by assumption
qed
next
case (Some a)
then show ?thesis
using Suc ‹nL = n # nL''› by auto
qed
qed

lemma select_inputs_index_properties :
assumes "i < length (select_inputs (h M) q0 iL nL nS m)"
and     "i ≥ length m"
and     "distinct (map fst m)"
and     "nS = nS0 ∪ set (map fst m)"
and     "q0 ∉ nS"
and     "distinct nL"
and     "q0 ∉ set nL"
and     "set nL ∩ nS = {}"
shows "fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))"
"fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
"snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL"
"(∀ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx')"
"(∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))"
"(∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"
proof -
have combined_props :
"fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))
∧ snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL
∧ fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0
∧ (∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))
∧ (∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"
using assms proof (induction "length nL" arbitrary: nL nS m)
case 0
show ?case proof (cases "find (λ x . (h M) (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q0,x) . (q'' ∈ nS))) iL")
case None
then have "(select_inputs (h M) q0 iL nL nS m) = m" using 0 by auto
then have "False" using "0.prems"(1,2) by auto
then show ?thesis by simp
next
case (Some x)
have "(select_inputs (h M) q0 iL nL nS m) = m@[(q0,x)]" using select_inputs_helper1[OF Some] by assumption
then have "(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)" using "0.prems"(1,2)
using antisym by fastforce

have "fst (q0, x) ∈ insert q0 (set nL)" by auto
moreover have "snd (q0, x) ∈ set iL" using find_set[OF Some] by auto
moreover have "fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
using ‹select_inputs (h M) q0 iL nL nS m ! i = (q0, x)› assms(4) assms(5) by auto

moreover have "(∃t∈FSM.transitions M. t_source t = fst (q0, x) ∧ t_input t = snd (q0, x))"
using find_condition[OF Some] unfolding fst_conv snd_conv h.simps
by fastforce
moreover have "⋀ t . t ∈ FSM.transitions M ⟹
t_source t = fst (q0, x) ⟹ t_input t = snd (q0, x) ⟹
t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
proof -
fix t assume "t ∈ FSM.transitions M" "t_source t = fst (q0, x)" "t_input t = snd (q0, x)"
then have "t_target t ∈ nS"
using find_condition[OF Some] unfolding h.simps fst_conv snd_conv
by (metis (no_types, lifting) case_prod_beta' h_simps mem_Collect_eq prod.collapse)
then show "t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
using ‹nS = nS0 ∪ set (map fst m)›
using "0.prems"(1) "0.prems"(2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by fastforce
qed

ultimately show ?thesis
unfolding ‹(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)› by blast
qed
next
case (Suc k)
then obtain n nL'' where "nL = n # nL''"
by (meson Suc_length_conv)

show ?case proof (cases "find (λ x . (h M) (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q0,x) . (q'' ∈ nS))) iL")
case None
show ?thesis proof (cases "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS))) nL iL")
case None
then have "(select_inputs (h M) q0 iL nL nS m) = m" using ‹find (λx. h M (q0, x) ≠ {} ∧ (∀(y, q'')∈h M (q0, x). q'' ∈ nS)) iL = None› ‹nL = n # nL''› by auto
then have "False" using Suc.prems(1,2) by auto
then show ?thesis by simp
next
case (Some a)
then obtain q' x nL' where **: "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
by (metis prod_cases3)

have "k = length nL'"
using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

have "select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m @ [(q', x)])"
using **
unfolding  ‹nL = n # nL''› select_inputs.simps None by auto
then have "i < length (select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)]))"
using Suc.prems(1) by auto

have "(set (map fst (m @ [(q', x)]))) ⊆ insert q' nS"
using Suc.prems(4) by auto

have "q' ∈ set nL"
and  "set nL' = set nL - {q'}"
and  "distinct nL'"
using find_remove_2_set[OF ** ]  ‹distinct nL› by auto
have "set nL' ⊆ set nL"
using find_remove_2_set(4)[OF ** ‹distinct nL›] by blast

have "distinct (map fst (m @ [(q', x)]))"
using Suc.prems(4) ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)› by auto
have "distinct (map fst (m@[(q',x)]))"
using Suc.prems(4) ‹set nL ∩ nS = {}› ‹q' ∈ set nL› ‹distinct (map fst m)› by auto
have "q0 ∉ insert q' nS"
using Suc.prems(7) Suc.prems(5) ‹q' ∈ set nL› by auto
have "insert q' nS = nS0 ∪ set (map fst (m@[(q',x)]))"
using Suc.prems(4) by auto
have "q0 ∉ set nL'"
by (metis Suc.prems(7) ‹set nL' ⊆ set nL› subset_code(1))
have "set nL' ∩ insert q' nS = {}"
using Suc.prems(8) ‹set nL' = set nL - {q'}› by auto

show ?thesis proof (cases "length (m @ [(q', x)]) ≤ i")
case True

show ?thesis
using Suc.hyps(1)[OF ‹k = length nL'› ‹i < length (select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)]))›
True
‹distinct (map fst (m @ [(q', x)]))›
‹insert q' nS = nS0 ∪ set (map fst (m@[(q',x)]))›
‹q0 ∉ insert q' nS›
‹distinct nL'›
‹q0 ∉ set nL'›
‹set nL' ∩ insert q' nS = {}› ]
unfolding ‹select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)])›
using ‹set nL' ⊆ set nL› by blast
next
case False
then have "i = length m"
using Suc.prems(2) by auto
then have ***: "select_inputs (h M) q0 iL nL nS m ! i = (q',x)"
unfolding ‹select_inputs (h M) q0 iL nL nS m = select_inputs (h M) q0 iL nL' (insert q' nS) (m@[(q',x)])›
using select_inputs_take
by (metis length_append_singleton lessI nth_append_length nth_take)

have "q' ∈ insert q0 (set nL)"
by (simp add: ‹q' ∈ set nL›)
moreover have "x ∈ set iL"
using find_remove_2_set(3)[OF ** ] by auto
moreover have "q' ∉ nS0"
using Suc.prems(4) Suc.prems(8) ‹q' ∈ set nL› by blast
moreover have "(∃t∈FSM.transitions M. t_source t = q' ∧ t_input t = x) "
using find_remove_2_set(1)[OF ** ] unfolding h.simps by force
moreover have "(∀t∈FSM.transitions M. t_source t = q' ∧ t_input t = x ⟶ t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t))"
unfolding ‹i = length m› select_inputs_take
using find_remove_2_set(1)[OF ** ] unfolding h.simps ‹nS = nS0 ∪ (set (map fst m))› by force
ultimately show ?thesis
unfolding *** fst_conv snd_conv by blast
qed
qed
next
case (Some x)
have "(select_inputs (h M) q0 iL nL nS m) = m@[(q0,x)]" using select_inputs_helper1[OF Some] by assumption
then have "(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)" using Suc.prems(1,2)
using antisym by fastforce

have "fst (q0, x) ∈ insert q0 (set nL)" by auto
moreover have "snd (q0, x) ∈ set iL" using find_set[OF Some] by auto
moreover have "fst (q0, x) ∉ nS0"
using assms(4) assms(5) by auto
moreover have "⋀ qx' . qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) - set (take (length m) (select_inputs (h M) q0 iL nL nS m)) ⟹ fst (q0, x) ≠ fst qx'"
using Suc.prems(1,2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by auto
moreover have "(∃t∈FSM.transitions M. t_source t = fst (q0, x) ∧ t_input t = snd (q0, x))"
using find_condition[OF Some] unfolding fst_conv snd_conv h.simps
by fastforce
moreover have "⋀ t . t ∈ FSM.transitions M ⟹
t_source t = fst (q0, x) ⟹ t_input t = snd (q0, x) ⟹
t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
proof -
fix t assume "t ∈ FSM.transitions M" "t_source t = fst (q0, x)" "t_input t = snd (q0, x)"
then have "t_target t ∈ nS"
using find_condition[OF Some] unfolding h.simps fst_conv snd_conv
by (metis (no_types, lifting) case_prod_beta' h_simps mem_Collect_eq prod.collapse)
then show "t_target t ∈ nS0 ∨ (∃qx'∈set (take i (select_inputs (h M) q0 iL nL nS m)). fst qx' = t_target t)"
using ‹nS = nS0 ∪ (set (map fst m))›
using Suc.prems(1,2) ‹select_inputs (h M) q0 iL nL nS m = m @ [(q0, x)]› by fastforce
qed

ultimately show ?thesis
unfolding ‹(select_inputs (h M) q0 iL nL nS m ! i) = (q0,x)› by blast
qed
qed

then show "fst (select_inputs (h M) q0 iL nL nS m ! i) ∈ (insert q0 (set nL))"
"snd (select_inputs (h M) q0 iL nL nS m ! i) ∈ set iL"
"fst (select_inputs (h M) q0 iL nL nS m ! i) ∉ nS0"
"(∃ t ∈ transitions M . t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i))"
"(∀ t ∈ transitions M . (t_source t = fst (select_inputs (h M) q0 iL nL nS m ! i) ∧ t_input t = snd (select_inputs (h M) q0 iL nL nS m ! i)) ⟶ (t_target t ∈ nS0 ∨ (∃ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst qx' = (t_target t))))"
by blast+

show "(∀ qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m)) . fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx')"
proof
fix qx' assume "qx' ∈ set (take i (select_inputs (h M) q0 iL nL nS m))"
then obtain j where "(take i (select_inputs (h M) q0 iL nL nS m)) ! j = qx'" and "j < length (take i (select_inputs (h M) q0 iL nL nS m))"
by (meson in_set_conv_nth)
then have "fst qx' = (map fst (select_inputs (h M) q0 iL nL nS m)) ! j" and "j < length (select_inputs (h M) q0 iL nL nS m)" by auto

moreover have "fst (select_inputs (h M) q0 iL nL nS m ! i) = (map fst (select_inputs (h M) q0 iL nL nS m)) ! i"
using assms(1) by auto

moreover have "j ≠ i"
using ‹j < length (take i (select_inputs (h M) q0 iL nL nS m))› by auto

moreover have "set (map fst m) ⊆ nS"
using ‹nS = nS0 ∪ set (map fst m)› by blast

ultimately show "fst (select_inputs (h M) q0 iL nL nS m ! i) ≠ fst qx'"
using assms(1)
using select_inputs_distinct[OF ‹distinct (map fst m)› _ ‹q0 ∉ nS› ‹distinct nL› ‹q0 ∉ set nL› ‹set nL ∩ nS = {}›]
by (metis distinct_Ex1 in_set_conv_nth length_map)
qed
qed

lemma select_inputs_initial :
assumes "qx ∈ set (select_inputs f q0 iL nL nS m) - set m"
and     "fst qx = q0"
shows "(last (select_inputs f q0 iL nL nS m)) = qx"
using assms(1) proof (induction "length nL" arbitrary: nS nL m)
case 0
then have "nL = []" by auto

have "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL ≠ None"
using 0 unfolding ‹nL = []› select_inputs.simps
by (metis Diff_cancel empty_iff option.simps(4))
then obtain x where *: "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = Some x"
by auto

have "set (select_inputs f q0 iL nL nS m) - set m = {qx}"
using "0.prems"(1) unfolding select_inputs_helper1[OF *]
by auto

then show ?case unfolding select_inputs_helper1[OF *]
by (metis DiffD1 DiffD2 UnE empty_iff empty_set insert_iff last_snoc list.simps(15) set_append)
next
case (Suc k)
then obtain n nL'' where "nL = n # nL''"
by (meson Suc_length_conv)

show ?case proof (cases "find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL")
case None
show ?thesis proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
case None
have "(select_inputs f q0 iL nL nS m) = m"
using ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None› None ‹nL = n # nL''› by auto
then have "False"
using Suc.prems(1)
by simp
then show ?thesis by simp
next
case (Some a)
then obtain q' x nL' where **: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
by (metis prod_cases3)

have "k = length nL'"
using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])"
using **
unfolding  ‹nL = n # nL''› select_inputs.simps None by auto
then have "qx ∈ set (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) - set m"
using Suc.prems by auto
moreover have "q0 ≠ q'"
using None unfolding find_None_iff
using find_remove_2_set(1,2,3)[OF **]
by blast
ultimately have "qx ∈ set (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) - set (m@[(q',x)])"
using ‹fst qx = q0› by auto
then show ?thesis
using Suc.hyps unfolding ‹(select_inputs f q0 iL nL nS m) = (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)]))›
using ‹k = length nL'› by blast
qed
next
case (Some a)

have "set (select_inputs f q0 iL nL nS m ) - set m = {qx}"
using Suc.prems(1) unfolding select_inputs_helper1[OF Some]
by auto

then show ?thesis unfolding select_inputs_helper1[OF Some]
by (metis DiffD1 DiffD2 UnE empty_iff empty_set insert_iff last_snoc list.simps(15) set_append)
qed
qed

lemma select_inputs_max_length :
assumes "distinct nL"
shows "length (select_inputs f q0 iL nL nS m) ≤ length m + Suc (length nL)"
using assms proof (induction "length nL" arbitrary: nL nS m)
case 0
then show ?case by (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL"; auto)
next
case (Suc k)
then obtain n nL'' where "nL = n # nL''"
by (meson Suc_length_conv)

show ?case proof (cases "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL")
case None
show ?thesis proof (cases "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL")
case None
show ?thesis unfolding ‹nL = n # nL''› select_inputs.simps None ‹find (λx. f (q0, x) ≠ {} ∧ (∀(y, q'')∈f (q0, x). q'' ∈ nS)) iL = None›
using None ‹nL = n # nL''› by auto
next
case (Some a)
then obtain q' x nL' where **: "find_remove_2 (λ q' x . f (q',x) ≠ {} ∧ (∀ (y,q'') ∈ f (q',x) . (q'' ∈ nS))) nL iL = Some (q',x,nL')"
by (metis prod_cases3)
have "k = length nL'"
using find_remove_2_length[OF **] ‹Suc k = length nL› by simp

have "select_inputs f q0 iL nL nS m = select_inputs f q0 iL nL' (insert q' nS) (m @ [(q', x)])"
using **
unfolding  ‹nL = n # nL''› select_inputs.simps None by auto

have "length nL = Suc (length nL') ∧ distinct nL'"
using find_remove_2_set(2,4,5)[OF **] ‹distinct nL›
by (metis One_nat_def Suc_pred distinct_card distinct_remove1 equals0D length_greater_0_conv length_remove1 set_empty2 set_remove1_eq)
then have "length (select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])) ≤ length m + Suc (length nL)"
using Suc.hyps(1)[OF ‹k = length nL'›]
then show ?thesis
using ‹(select_inputs f q0 iL nL nS m) = select_inputs f q0 iL nL' (insert q' nS) (m@[(q',x)])› by simp
qed
next
case (Some a)
show ?thesis unfolding select_inputs_helper1[OF Some] by auto
qed
qed

lemma select_inputs_q0_containment :
assumes "f (q0,x) ≠ {}"
and     "(∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))"
and     "x ∈ set iL"
shows "(∃ qx ∈ set (select_inputs f q0 iL nL nS m) . fst qx = q0)"
proof -
have "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL ≠ None"
using assms unfolding find_None_iff by blast
then obtain x' where *: "find (λ x . f (q0,x) ≠ {} ∧ (∀ (y,q'') ∈ f (q0,x) . (q'' ∈ nS))) iL = Some x'"
by auto
show ?thesis
unfolding select_inputs_helper1[OF *] by auto
qed

lemma select_inputs_from_submachine :
assumes "single_input S"
and     "acyclic S"
and     "is_submachine S M"
and     "⋀ q x . q ∈ reachable_states S ⟹ h S (q,x) ≠ {} ⟹ h S (q,x) = h M (q,x)"
and     "⋀ q . q ∈ reachable_states S ⟹ deadlock_state S q ⟹ q ∈ nS0 ∪ set (map fst m)"
and     "states M = insert (initial S) (set nL ∪ nS0 ∪ set (map fst m))"
and     "(initial S) ∉ (set nL ∪ nS0 ∪ set (map fst m))"
shows "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S)"
and   "length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
proof -
have "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S) ∧ length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
using assms(5,6,7) proof (induction "length nL" arbitrary: nL m)
case 0
then have "nL = []" by auto

have "¬ (deadlock_state S (initial S))"
using assms(5,6,3,7) reachable_states_initial by blast
then obtain x where "x ∈ set (inputs_as_list M)" and "h S ((initial S),x) ≠ {}"
using assms(3) unfolding deadlock_state.simps h.simps inputs_as_list_set
by fastforce

then have "h M ((initial S),x) ≠ {}"
using assms(4)[OF reachable_states_initial]  by fastforce

have "(initial S) ∈ reachable_states M"
using assms(3) reachable_states_initial by auto

then have "(initial S) ∈ states M"
using reachable_state_is_state by force

have "⋀ y q'' . (y,q'') ∈ h M ((initial S),x) ⟹ q'' ∈ (nS0 ∪ set (map fst m))"
proof -
fix y q'' assume "(y,q'') ∈ h M ((initial S),x)"
then have "q'' ∈ reachable_states M" using fsm_transition_target unfolding h.simps
using ‹FSM.initial S ∈ reachable_states M› reachable_states_next by fastforce
then have "q'' ∈ insert (initial S) (nS0 ∪ set (map fst m))" using "0.prems"(2) ‹nL = []›
using reachable_state_is_state by force
moreover have "q'' ≠ (initial S)"
using acyclic_no_self_loop[OF ‹acyclic S› reachable_states_initial]
using ‹(y,q'') ∈ h M ((initial S),x)› assms(4)[OF reachable_states_initial ‹h S ((initial S),x) ≠ {}›] unfolding h_simps
by blast
ultimately show "q'' ∈ (nS0 ∪ set (map fst m))" by blast
qed
then have "x ∈ set (inputs_as_list M) ∧ h M ((initial S), x) ≠ {} ∧ (∀(y, q'')∈h M ((initial S), x). q'' ∈ nS0 ∪ set (map fst m))"
using ‹x ∈ set (inputs_as_list M) › ‹h M ((initial S), x) ≠ {}› by blast
then have "find (λ x . (h M) ((initial S),x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) ((initial S),x) . (q'' ∈ (nS0 ∪ set (map fst m))))) (inputs_as_list M) ≠ None"
unfolding find_None_iff by blast
then show ?case
unfolding ‹nL = []› select_inputs.simps by auto
next
case (Suc k)
then obtain n nL'' where "nL = n # nL''"
by (meson Suc_length_conv)

have "∃ q x . q ∈ reachable_states S - (nS0 ∪ set (map fst m)) ∧ h M (q,x) ≠ {} ∧ (∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))"
proof -
define ndlps where ndlps_def: "ndlps = {p . path S (initial S) p ∧ target (initial S) p ∉ (nS0 ∪ set (map fst m))}"

have "path S (initial S) [] ∧ target (initial S) [] ∉ (nS0 ∪ set (map fst m))"
using Suc.prems(3) by auto
then have "[] ∈ ndlps"
unfolding ndlps_def by blast
then have "ndlps ≠ {}" by auto
moreover have "finite ndlps"
using acyclic_finite_paths_from_reachable_state[OF ‹acyclic S›, of "[]"] unfolding ndlps_def by fastforce
ultimately have "∃ p ∈ ndlps . ∀ p' ∈ ndlps . length p' ≤ length p"
by (meson max_length_elem not_le_imp_less)
then obtain p where "path S (initial S) p"
and "target (initial S) p ∉ (nS0 ∪ set (map fst m))"
and "⋀ p' . path S (initial S) p' ⟹ target (initial S) p' ∉ (nS0 ∪ set (map fst m)) ⟹ length p' ≤ length p"
unfolding ndlps_def by blast

let ?q = "target (initial S) p"
using Suc.prems(1) reachable_states_intro[OF ‹path S (initial S) p›] using ‹?q ∉ (nS0 ∪ set (map fst m))› by blast
then obtain x where "h S (?q,x) ≠ {}"
then have "h M (?q,x) ≠ {}"
using assms(4)[of ?q _] reachable_states_intro[OF ‹path S (initial S) p›]
by blast

moreover have "⋀ y q'' . (y,q'') ∈ h M (?q,x) ⟹ q'' ∈ (nS0 ∪ set (map fst m))"
proof (rule ccontr)
fix y q'' assume "(y,q'') ∈ h M (?q,x)" and "q'' ∉ nS0 ∪ set (map fst m)"
then have "(?q,x,y,q'') ∈ transitions S"
using assms(4)[OF reachable_states_intro[OF ‹path S (initial S) p›] ‹h S (?q,x) ≠ {}›] unfolding h_simps
by blast
then have "path S (initial S) (p@[(?q,x,y,q'')])"
using ‹path S (initial S) p› by (simp add: path_append_transition)
moreover have "target (initial S) (p@[(?q,x,y,q'')]) ∉ (nS0 ∪ set (map fst m))"
using ‹q'' ∉ nS0 ∪ set (map fst m)› by auto
ultimately show "False"
using ‹⋀ p' . path S (initial S) p' ⟹ target (initial S) p' ∉ (nS0 ∪ set (map fst m)) ⟹ length p' ≤ length p›[of "(p@[(?q,x,y,q'')])"] by simp
qed

moreover have "?q ∈ reachable_states S - (nS0 ∪ set (map fst m))"
using  ‹?q ∉ (nS0 ∪ set (map fst m))› ‹path S (initial S) p›  by blast

ultimately show ?thesis by blast
qed

then obtain q x where "q ∈ reachable_states S" and "q ∉ (nS0 ∪ set (map fst m))" and "h M (q,x) ≠ {}" and "(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))"
by blast
then have "x ∈ set (inputs_as_list M)"
unfolding h.simps using fsm_transition_input inputs_as_list_set by fastforce

show ?case proof (cases "q = initial S")
case True
have "find (λx. h M (FSM.initial S, x) ≠ {} ∧ (∀(y, q'')∈h M (FSM.initial S, x). q'' ∈ nS0 ∪ set (map fst m))) (inputs_as_list M) ≠ None"
using ‹h M (q,x) ≠ {}› ‹(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))› ‹x ∈ set (inputs_as_list M)›
unfolding True find_None_iff by blast
then show ?thesis unfolding ‹nL = n # nL''› by auto
next
case False
then have "q ∈ set nL"
using submachine_reachable_subset[OF ‹is_submachine S M›]
unfolding is_submachine.simps ‹states M = insert (initial S) (set nL ∪ nS0 ∪ set (map fst m))›
using ‹q ∈ reachable_states S›  ‹q ∉ (nS0 ∪ set (map fst m))›
by (metis (no_types, lifting) Suc.prems(2) UnE insertE reachable_state_is_state subsetD sup_assoc)

show ?thesis proof (cases "find (λx. h M (FSM.initial S, x) ≠ {} ∧ (∀(y, q'')∈h M (FSM.initial S, x). q'' ∈ nS0 ∪ set (map fst m))) (inputs_as_list M)")
case None

have "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS0 ∪ set (map fst m)))) (nL) (inputs_as_list M) ≠ None"
using ‹q ∈ set nL› ‹h M (q,x) ≠ {}› ‹(∀ (y,q'') ∈ h M (q,x) . q'' ∈ (nS0 ∪ set (map fst m)))› ‹x ∈ set (inputs_as_list M)›
unfolding find_remove_2_None_iff ‹nL = n # nL''›
by blast
then obtain q' x' nL' where *: "find_remove_2 (λ q' x . (h M) (q',x) ≠ {} ∧ (∀ (y,q'') ∈ (h M) (q',x) . (q'' ∈ nS0 ∪ set (map fst m)))) (n#nL'') (inputs_as_list M) = Some (q',x',nL')"
unfolding ‹nL = n # nL''› by auto
have "k = length nL'"
using find_remove_2_length[OF *] ‹Suc k = length nL›  ‹nL = n # nL''› by simp

have **: "select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m
= select_inputs (h M) (initial S) (inputs_as_list M) nL' (nS0 ∪ set (map fst (m@[(q',x')]))) (m@[(q',x')])"
unfolding ‹nL = n # nL''› select_inputs.simps None * by auto

have p1: "(⋀q. q ∈ reachable_states S ⟹ deadlock_state S q ⟹ q ∈ nS0 ∪ set (map fst (m@[(q',x')])))"
using Suc.prems(1) by fastforce

have "set nL = insert q' (set nL')" using find_remove_2_set(2,6)[OF *] unfolding ‹nL = n # nL''› by auto
then have "(set nL ∪ set (map fst m)) = (set nL' ∪ set (map fst (m @ [(q', x')])))" by auto
then have p2: "states M = insert (initial S) (set nL' ∪ nS0 ∪ set (map fst (m @ [(q', x')])))"
using Suc.prems(2) by auto

have p3: "initial S ∉ set nL' ∪ nS0 ∪ set (map fst (m @ [(q', x')]))"
using Suc.prems(3) False ‹set nL = insert q' (set nL')› by auto

show ?thesis unfolding **
using Suc.hyps(1)[OF ‹k = length nL'› p1 p2 p3] by blast
next
case (Some a)
then show ?thesis unfolding ‹nL = n # nL''› by auto
qed
qed
qed
then show "fst (last (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m)) = (initial S)"
and  "length (select_inputs (h M) (initial S) (inputs_as_list M) nL (nS0 ∪ set (map fst m)) m) > 0"
by blast+
qed

end```