# Theory Intermediate_Implementations

```section ‹Intermediate Implementations›

text ‹This theory implements various functions to be supplied to the H, SPY, and Pair-Frameworks.›

theory Intermediate_Implementations
imports H_Framework SPY_Framework Pair_Framework "../Distinguishability"  Automatic_Refinement.Misc
begin

subsection ‹Functions for the Pair Framework›

definition get_initial_test_suite_H :: "('a,'b,'c) state_cover_assignment ⇒
('a::linorder,'b::linorder,'c::linorder) fsm ⇒
nat ⇒
('b×'c) prefix_tree"
where
"get_initial_test_suite_H V M m =
(let
rstates       = reachable_states_as_list M;
n             = size_r M;
iM            = inputs_as_list M;
T             = from_list (concat (map (λq . map (λτ. (V q)@τ) (h_extensions M q (m-n))) rstates))
in T)"

lemma get_initial_test_suite_H_set_and_finite :
shows  "{(V q)@io@[(x,y)] | q io x y . q ∈ reachable_states M ∧ io ∈ LS M q ∧ length io ≤ m - size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} ⊆ set (get_initial_test_suite_H V M m)"
and "finite_tree (get_initial_test_suite_H V M m)"
proof -

define rstates where "rstates       = reachable_states_as_list M"
moreover define n where "n             = size_r M"
moreover define iM where "iM            = inputs_as_list M"
moreover define T where "T             = from_list (concat (map (λq . map (λτ. (V q)@τ) (h_extensions M q (m-n))) rstates))"
ultimately have res: "get_initial_test_suite_H V M m = T"
unfolding get_initial_test_suite_H_def Let_def by auto

define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M})"

have "list.set rstates = reachable_states M"
unfolding rstates_def reachable_states_as_list_set by simp

have "{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} ⊆ set T"
proof
fix io assume "io ∈ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
then obtain q τ where "io = (V q) @ τ"
and "q ∈ reachable_states M"
and "τ ∈ 𝒳 q"
by blast

have "τ ∈ list.set (h_extensions M q (m - n))"
using ‹τ ∈ 𝒳 q› unfolding 𝒳
using h_extensions_set[OF reachable_state_is_state[OF ‹q ∈ reachable_states M›]]
by auto
then have "io ∈ list.set (map ((@) (V q)) (h_extensions M q (m - n)))"
unfolding ‹io = (V q) @ τ› by auto
moreover have "q ∈ list.set rstates"
using ‹list.set rstates = reachable_states M› ‹q ∈ reachable_states M› by auto
ultimately have "io ∈ list.set (concat (map (λq. map ((@) (V q)) (h_extensions M q (m - n))) rstates))"
by auto
then show "io ∈ set T"
unfolding T_def from_list_set by blast
qed
moreover have "{ (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q} = {(V q)@io@[(x,y)] | q io x y . q ∈ reachable_states M ∧ io ∈ LS M q ∧ length io ≤ m - size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M}"
unfolding 𝒳 n_def[symmetric] by force
ultimately show "{(V q)@io@[(x,y)] | q io x y . q ∈ reachable_states M ∧ io ∈ LS M q ∧ length io ≤ m - size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} ⊆ set (get_initial_test_suite_H V M m)"
unfolding res by simp

show "finite_tree (get_initial_test_suite_H V M m)"
unfolding res T_def
using from_list_finite_tree by auto
qed

fun complete_inputs_to_tree :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'c list ⇒ 'b list ⇒ ('b × 'c) prefix_tree" where
"complete_inputs_to_tree M q ys [] = Prefix_Tree.empty" |
"complete_inputs_to_tree M q ys (x#xs) = foldl (λ t y . case h_obs M q x y of None ⇒ insert t [(x,y)] |
Some q' ⇒ combine_after t [(x,y)] (complete_inputs_to_tree M q' ys xs)) Prefix_Tree.empty ys"

lemma complete_inputs_to_tree_finite_tree :
"finite_tree (complete_inputs_to_tree M q ys xs)"
proof (induction xs arbitrary: q ys)
case Nil
then show ?case using empty_finite_tree by auto
next
case (Cons x xs)

define ys' where "ys' = ys"
moreover define f where "f = (λ t y . case h_obs M q x y of None ⇒ insert t [(x,y)] | Some q' ⇒ combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
ultimately have *:"complete_inputs_to_tree M q ys (x # xs)
= foldl f Prefix_Tree.empty ys"
by auto
moreover have "finite_tree (foldl f Prefix_Tree.empty ys)"
proof (induction ys rule: rev_induct)
case Nil
then show ?case using empty_finite_tree by auto
next
case (snoc y ys)

define t where "t = foldl (λ t y . case h_obs M q x y of None ⇒ insert t [(x,y)] | Some q' ⇒ combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys"
then have *:"foldl f Prefix_Tree.empty (ys@[y])
= (case h_obs M q x y of None ⇒ insert t [(x,y)] | Some q' ⇒ combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
unfolding f_def by auto

have "finite_tree t"
using snoc unfolding t_def f_def by force

have "finite_tree (insert t [(x,y)])"
using ‹finite_tree t› insert_finite_tree by blast
moreover have "⋀ q' . finite_tree (combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
using ‹finite_tree t› ‹⋀ q ys . finite_tree (complete_inputs_to_tree M q ys xs)› combine_after_finite_tree by blast
ultimately show ?case
unfolding * by auto
qed
ultimately show ?case by auto
qed

fun complete_inputs_to_tree_initial :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'b list ⇒ ('b × 'c) prefix_tree" where
"complete_inputs_to_tree_initial M xs = complete_inputs_to_tree M (initial M) (outputs_as_list M) xs"

definition get_initial_test_suite_H_2 :: "bool ⇒ ('a,'b,'c) state_cover_assignment ⇒
('a::linorder,'b::linorder,'c::linorder) fsm ⇒
nat ⇒
('b×'c) prefix_tree" where
"get_initial_test_suite_H_2 c V M m =
(if c then get_initial_test_suite_H V M m
else let TS = get_initial_test_suite_H V M m;
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS);
ys  = outputs_as_list M
in
foldl (λ t xs . combine t (complete_inputs_to_tree_initial M xs)) TS xss)"

lemma get_initial_test_suite_H_2_set_and_finite :
shows  "{(V q)@io@[(x,y)] | q io x y . q ∈ reachable_states M ∧ io ∈ LS M q ∧ length io ≤ m - size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} ⊆ set (get_initial_test_suite_H_2 c V M m)" (is ?P1)
and "finite_tree (get_initial_test_suite_H_2 c V M m)" (is ?P2)
proof -
have "?P1 ∧ ?P2"
proof (cases c)
case True
then have "get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m"
unfolding get_initial_test_suite_H_2_def by auto
then show ?thesis
using get_initial_test_suite_H_set_and_finite
by fastforce
next
case False

define TS where "TS = get_initial_test_suite_H V M m"
moreover define xss where "xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)"
moreover define ys where "ys  = outputs_as_list M"
ultimately have "get_initial_test_suite_H_2 c V M m = foldl (λ t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss"
unfolding get_initial_test_suite_H_2_def Let_def using False by auto
moreover have "set TS ⊆ set (foldl (λ t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss)"
using combine_set by (induction xss rule: rev_induct; auto)
moreover have "finite_tree (foldl (λ t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss)"
using complete_inputs_to_tree_finite_tree get_initial_test_suite_H_set_and_finite(2)[of V M m] combine_finite_tree
unfolding TS_def[symmetric] by (induction xss rule: rev_induct; auto; blast)
ultimately show ?thesis
using get_initial_test_suite_H_set_and_finite(1)[of V M m] unfolding TS_def[symmetric]
by force
qed
then show ?P1 and ?P2
by blast+
qed

definition get_pairs_H :: "('a,'b,'c) state_cover_assignment ⇒
('a::linorder,'b::linorder,'c::linorder) fsm ⇒
nat ⇒
((('b × 'c) list × 'a) × (('b × 'c) list × 'a)) list"
where
"get_pairs_H V M m =
(let
rstates       = reachable_states_as_list M;
n             = size_r M;
iM            = inputs_as_list M;
hMap          = mapping_of (map (λ(q,x) . ((q,x), map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) (List.product (states_as_list M) iM));
hM            = (λ q x . case Mapping.lookup hMap (q,x) of Some ts ⇒ ts | None ⇒ []);
pairs         = pairs_to_distinguish M V (λq . paths_up_to_length_with_targets q hM iM ((m-n)+1)) rstates
in
pairs)"

lemma get_pairs_H_set :
assumes "observable M"
and     "is_state_cover_assignment M V"
shows
"⋀ α β . (α,β) ∈ (V ` reachable_states M) × (V ` reachable_states M)
∪ (V ` reachable_states M) × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M}}
∪ (⋃ q ∈ reachable_states M . ⋃ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ}) ⟹
α ∈ L M ⟹ β ∈ L M ⟹ after_initial M α ≠ after_initial M β ⟹
((α,after_initial M α),(β,after_initial M β)) ∈ list.set (get_pairs_H V M m)"
and "⋀ α q' β q'' . ((α,q'),(β,q'')) ∈ list.set (get_pairs_H V M m) ⟹ α ∈ L M ∧ β ∈ L M ∧ after_initial M α ≠ after_initial M β ∧ q' = after_initial M α ∧ q'' = after_initial M β"
proof -

define rstates where "rstates       = reachable_states_as_list M"
moreover define n where "n             = size_r M"
moreover define iM where "iM            = inputs_as_list M"
moreover define hMap' where "hMap'          = mapping_of (map (λ(q,x) . ((q,x), map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) (List.product (states_as_list M) iM))"
moreover define hM' where "hM'            = (λ q x . case Mapping.lookup hMap' (q,x) of Some ts ⇒ ts | None ⇒ [])"
ultimately have "get_pairs_H V M m = pairs_to_distinguish M V (λq . paths_up_to_length_with_targets q hM' iM ((m-n)+1)) rstates"
unfolding get_pairs_H_def Let_def by force

define hMap where "hMap          = map_of (map (λ(q,x) . ((q,x), map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) (List.product (states_as_list M) iM))"
define hM where "hM            = (λ q x . case hMap (q,x) of Some ts ⇒ ts | None ⇒ [])"

have "distinct (List.product (states_as_list M) iM)"
using states_as_list_distinct inputs_as_list_distinct distinct_product
unfolding iM_def
by blast

then have "Mapping.lookup hMap' = hMap"
using mapping_of_map_of
unfolding hMap_def hMap'_def
using map_pair_fst_helper[of "λ q x . map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x)))"]
by (metis (no_types, lifting))
then have "hM' = hM"
unfolding hM'_def hM_def
by meson
moreover define pairs where "pairs         = pairs_to_distinguish M V (λq . paths_up_to_length_with_targets q hM iM ((m-n)+1)) rstates"
ultimately have res: "get_pairs_H V M m = pairs"
unfolding ‹get_pairs_H V M m = pairs_to_distinguish M V (λq . paths_up_to_length_with_targets q hM' iM ((m-n)+1)) rstates›
by force

have *:"list.set rstates = reachable_states M"
unfolding rstates_def reachable_states_as_list_set by simp

define 𝒳' where 𝒳': "𝒳' = (λq . paths_up_to_length_with_targets q hM iM ((m-n)+1))"

have **: "⋀ q p q' . q ∈ reachable_states M ⟹ (p,q') ∈ list.set (𝒳' q) ⟷ path M q p ∧ target q p = q' ∧ length p ≤ m-n+1"
proof -
fix q p q' assume "q ∈ reachable_states M"

define qxPairs where qxPairs: "qxPairs = (List.product (states_as_list M) iM)"
moreover define mapList where mapList: "mapList = (map (λ(q,x) . ((q,x), map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) qxPairs)"
ultimately have hMap': "hMap = map_of mapList"
unfolding hMap_def by simp

have "distinct (states_as_list M)" and "distinct iM"
unfolding iM_def
by auto
then have "distinct qxPairs"
unfolding qxPairs by (simp add: distinct_product)
moreover have "(map fst mapList) = qxPairs"
unfolding mapList by (induction qxPairs; auto)
ultimately have "distinct (map fst mapList)"
by auto

have "⋀ q x . hM q x = map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))"
proof -
fix q x
show "hM q x = map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))"
proof (cases "q ∈ states M ∧ x ∈ inputs M")
case False
then have "(h M (q, x)) = {}"
unfolding h_simps using fsm_transition_source fsm_transition_input by fastforce
then have "map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))) = []"
by auto

have "q ∉ list.set (states_as_list M) ∨ x ∉ list.set iM"
using False unfolding states_as_list_set iM_def inputs_as_list_set by simp
then have "(q,x) ∉ list.set qxPairs"
unfolding qxPairs by auto
then have "∄ y . ((q,x),y) ∈ list.set mapList"
unfolding mapList by auto
then have "hMap (q,x) = None"
unfolding hMap' using map_of_eq_Some_iff[OF ‹distinct (map fst mapList)›]
by (meson option.exhaust)
then show ?thesis
using ‹map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))) = []›
unfolding hM_def by auto
next
case True
then have "q ∈ list.set (states_as_list M) ∧ x ∈ list.set iM"
unfolding states_as_list_set iM_def inputs_as_list_set by simp
then have "(q,x) ∈ list.set qxPairs"
unfolding qxPairs by auto
then have "((q,x),map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))) ∈ list.set mapList"
unfolding mapList by auto
then have "hMap (q,x) = Some (map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))"
unfolding hMap' using map_of_eq_Some_iff[OF ‹distinct (map fst mapList)›]
by (meson option.exhaust)
then show ?thesis
unfolding hM_def by auto
qed
qed
then have hM_alt_def: "hM = (λ q x . map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))"
by auto

show "(p,q') ∈ list.set (𝒳' q) ⟷ path M q p ∧ target q p = q' ∧ length p ≤ m-n+1"
unfolding 𝒳' hM_alt_def iM_def
paths_up_to_length_with_targets_set[OF reachable_state_is_state[OF ‹q ∈ reachable_states M›]]
by blast
qed

show "⋀ α β . (α,β) ∈ (V ` reachable_states M) × (V ` reachable_states M)
∪ (V ` reachable_states M) × { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M}}
∪ (⋃ q ∈ reachable_states M . ⋃ τ ∈ {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-size_r M ∧ x ∈ inputs M ∧ y ∈ outputs M} . { (V q) @ τ' | τ' . τ' ∈ list.set (prefixes τ)} × {(V q)@τ}) ⟹
α ∈ L M ⟹ β ∈ L M ⟹ after_initial M α ≠ after_initial M β ⟹
((α,after_initial M α),(β,after_initial M β)) ∈ list.set (get_pairs_H V M m)"
using pairs_to_distinguish_containment[OF assms(1,2) * **]
unfolding res pairs_def 𝒳'[symmetric] n_def[symmetric]
by presburger

show "⋀ α q' β q'' . ((α,q'),(β,q'')) ∈ list.set (get_pairs_H V M m) ⟹ α ∈ L M ∧ β ∈ L M ∧ after_initial M α ≠ after_initial M β ∧ q' = after_initial M α ∧ q'' = after_initial M β"
using pairs_to_distinguish_elems(3,4,5,6,7)[OF assms(1,2) * **]
unfolding res pairs_def 𝒳'[symmetric] n_def[symmetric]
by blast
qed

subsection ‹Functions of the SPYH-Method›

subsubsection ‹Heuristic Functions for Selecting Traces to Extend›

(* results:
errorValue - (x,y) need not be considered, as it is not in the language of either state
or (x,y) reaches the same states again or converges to a single state
1    - (x,y) immediately distinguishes the states
else - |(x,y)| + twice the length of the shortest distinguishing trace for the states
*)
fun estimate_growth :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ 'a ⇒ 'a ⇒ 'b ⇒ 'c ⇒ nat ⇒ nat" where
"estimate_growth M dist_fun q1 q2 x y errorValue= (case h_obs M q1 x y of
None ⇒ (case h_obs M q1 x y of
None ⇒ errorValue |
Some q2' ⇒ 1) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ 1 |
Some q2' ⇒ if q1' = q2' ∨ {q1',q2'} = {q1,q2}
then errorValue
else 1 + 2 * (length (dist_fun q1 q2))))"

lemma estimate_growth_result :
assumes "observable M"
and     "minimal M"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
and     "estimate_growth M dist_fun q1 q2 x y errorValue < errorValue"
shows "∃ γ . distinguishes M q1 q2 ([(x,y)]@γ)"
proof (cases "h_obs M q1 x y")
case None
show ?thesis proof (cases "h_obs M q2 x y")
case None
then show ?thesis
using ‹h_obs M q1 x y = None› assms(5)
by auto
next
case (Some a)
then have "distinguishes M q1 q2 [(x,y)]"
using h_obs_distinguishes[OF assms(1) _ None] distinguishes_sym
by metis
then show ?thesis
by auto
qed
next
case (Some q1')
show ?thesis proof (cases "h_obs M q2 x y")
case None
then have "distinguishes M q1 q2 [(x,y)]"
using h_obs_distinguishes[OF assms(1) Some]
by metis
then show ?thesis
by auto
next
case (Some q2')
then have "q1' ≠ q2'"
using ‹h_obs M q1 x y = Some q1'› assms(5)
by auto
then obtain γ where "distinguishes M q1' q2' γ"
using h_obs_state[OF ‹h_obs M q1 x y = Some q1'›]
using h_obs_state[OF Some]
using ‹minimal M› unfolding minimal.simps distinguishes_def
by blast
then have "distinguishes M q1 q2 ([(x,y)]@γ)"
using h_obs_language_iff[OF assms(1), of x y γ]
using ‹h_obs M q1 x y = Some q1'› Some
unfolding distinguishes_def
by force
then show ?thesis
by blast
qed
qed

fun shortest_list_or_default :: "'a list list ⇒ 'a list ⇒ 'a list" where
"shortest_list_or_default xs x = foldl (λ a b . if length a < length b then a else b) x xs"

lemma shortest_list_or_default_elem :
"shortest_list_or_default xs x ∈ Set.insert x (list.set xs)"
by (induction xs rule: rev_induct; auto)

fun shortest_list :: "'a list list ⇒ 'a list" where
"shortest_list [] = undefined" |
"shortest_list (x#xs) = shortest_list_or_default xs x"

lemma shortest_list_elem :
assumes "xs ≠ []"
shows "shortest_list xs ∈ list.set xs"
using assms shortest_list_or_default_elem
by (metis list.simps(15) shortest_list.elims)

fun shortest_list_in_tree_or_default :: "'a list list ⇒ 'a prefix_tree ⇒ 'a list ⇒ 'a list" where
"shortest_list_in_tree_or_default xs T x = foldl (λ a b . if isin T a ∧ length a < length b then a else b) x xs"

lemma shortest_list_in_tree_or_default_elem :
"shortest_list_in_tree_or_default xs T x ∈ Set.insert x (list.set xs)"
by (induction xs rule: rev_induct; auto)

fun has_leaf :: "('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('b×'c) list ⇒ bool" where
"has_leaf T G cg_lookup α =
(find (λ β . is_maximal_in T β) (α # cg_lookup G α) ≠ None)"

fun has_extension :: "('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('b×'c) list ⇒ 'b ⇒ 'c ⇒ bool" where
"has_extension T G cg_lookup α x y =
(find (λ β . isin T (β@[(x,y)])) (α # cg_lookup G α) ≠ None)"

fun get_extension :: "('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('b×'c) list ⇒ 'b ⇒ 'c ⇒ ('b×'c) list option" where
"get_extension T G cg_lookup α x y =
(find (λ β . isin T (β@[(x,y)])) (α # cg_lookup G α))"

(* uses a fixed recursion depth to avoid partiality, as the lookup function of the convergence
graph is not constrained here in any way *)
fun get_prefix_of_separating_sequence :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('a ⇒ 'a ⇒ ('b×'c) list) ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ nat ⇒ (nat × ('b×'c) list)" where
"get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v 0 = (1,[])" |
"get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v (Suc k)= (let
u' = shortest_list_or_default (cg_lookup G u) u;
v' = shortest_list_or_default (cg_lookup G v) v;
su = after_initial M u;
sv = after_initial M v;
bestPrefix0 = get_distinguishing_trace su sv;
minEst0 = length bestPrefix0 + (if (has_leaf T G cg_lookup u') then 0 else length u') + (if (has_leaf T G cg_lookup v') then 0 else length v');
errorValue = Suc minEst0;
XY = List.product (inputs_as_list M) (outputs_as_list M);
tryIO = (λ (minEst,bestPrefix) (x,y) .
if minEst = 0
then (minEst,bestPrefix)
else (case get_extension T G cg_lookup u' x y of
Some u'' ⇒ (case get_extension T G cg_lookup v' x y of
Some v'' ⇒ if (h_obs M su x y = None) ≠ (h_obs M sv x y = None)
then (0,[])
else if h_obs M su x y = h_obs M sv x y
then (minEst,bestPrefix)
else (let (e,w) = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k
in if e = 0
then (0,[])
else if e ≤ minEst
then (e,(x,y)#w)
else (minEst,bestPrefix)) |
None ⇒ (let e = estimate_growth M get_distinguishing_trace su sv x y errorValue;
e' = if e ≠ 1
then if has_leaf T G cg_lookup u''
then e + 1
else if ¬(has_leaf T G cg_lookup (u''@[(x,y)]))
then e + length u' + 1
else e
else e;
e'' = e' + (if ¬(has_leaf T G cg_lookup v') then length v' else 0)
in if e'' ≤ minEst
then (e'',[(x,y)])
else (minEst,bestPrefix))) |
None ⇒ (case get_extension T G cg_lookup v' x y of
Some v'' ⇒ (let e = estimate_growth M get_distinguishing_trace su sv x y errorValue;
e' = if e ≠ 1
then if has_leaf T G cg_lookup v''
then e + 1
else if ¬(has_leaf T G cg_lookup (v''@[(x,y)]))
then e + length v' + 1
else e
else e;
e'' = e' + (if ¬(has_leaf T G cg_lookup u') then length u' else 0)
in if e'' ≤ minEst
then (e'',[(x,y)])
else (minEst,bestPrefix)) |
None ⇒ (minEst,bestPrefix))))
in if ¬ isin T u' ∨ ¬ isin T v'
then (errorValue,[])
else foldl tryIO (minEst0,[]) XY)"

lemma estimate_growth_Suc :
assumes "errorValue > 0"
shows "estimate_growth M get_distinguishing_trace q1 q2 x y errorValue > 0"
using assms unfolding estimate_growth.simps
by (cases "FSM.h_obs M q1 x y"; cases "FSM.h_obs M q2 x y"; fastforce)

lemma get_extension_result:
assumes "u ∈ L M1" and "u ∈ L M2"
and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
and     "get_extension T G cg_lookup u x y = Some u'"
shows "converge M1 u u'" and "u' ∈ L M2 ⟹ converge M2 u u'" and "u'@[(x,y)] ∈ set T"
proof -

have "find (λ β . isin T (β@[(x,y)])) (u # cg_lookup G u) = Some u'"
using assms(4)
by auto
then have "isin T (u'@[(x,y)])"
using find_condition by metis
then show "u'@[(x,y)] ∈ set T"
by auto

have "u' ∈ Set.insert u (list.set (cg_lookup G u))"
using ‹find (λ β . isin T (β@[(x,y)])) (u # cg_lookup G u) = Some u'›
by (metis find_set list.simps(15))
then show "converge M1 u u'" and "u' ∈ L M2 ⟹ converge M2 u u'"
using assms(1,2,3)
by (metis converge.elims(3) convergence_graph_lookup_invar_def insert_iff)+
qed

lemma get_prefix_of_separating_sequence_result :
fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
assumes "observable M1"
and     "observable M2"
and     "minimal M1"
and     "u ∈ L M1" and "u ∈ L M2"
and     "v ∈ L M1" and "v ∈ L M2"
and     "after_initial M1 u ≠ after_initial M1 v"
and     "⋀ α β q1 q2 . q1 ∈ states M1 ⟹ q2 ∈ states M1 ⟹ q1 ≠ q2 ⟹ distinguishes M1 q1 q2 (get_distinguishing_trace q1 q2)"
and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
and     "L M1 ∩ set T = L M2 ∩ set T"
shows "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) = 0 ⟹ ¬ converge M2 u v"
and   "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) ≠ 0 ⟹  ∃ γ . distinguishes M1 (after_initial M1 u) (after_initial M1 v) ((snd (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k))@γ)"
proof -
have "(fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) = 0 ⟶ ¬ converge M2 u v)
∧ (fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) ≠ 0 ⟶  (∃ γ . distinguishes M1 (after_initial M1 u) (after_initial M1 v) ((snd (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k))@γ)))"
using assms(4,5,6,7,8)
proof (induction k arbitrary: u v)
case 0

then have "∃ γ . distinguishes M1 (after_initial M1 u) (after_initial M1 v) γ"
using ‹minimal M1› unfolding minimal.simps
by (meson after_is_state assms(1) assms(9))
then show ?case
unfolding get_prefix_of_separating_sequence.simps fst_conv snd_conv
by auto
next
case (Suc k)

define u' where u': "u' = shortest_list_or_default (cg_lookup G u) u"
define v' where v': "v' = shortest_list_or_default (cg_lookup G v) v"
define su where su: "su = after_initial M1 u"
define sv where sv: "sv = after_initial M1 v"
define bestPrefix0 where bestPrefix0: "bestPrefix0 = get_distinguishing_trace su sv"
define minEst0 where minEst0: "minEst0 = length bestPrefix0 + (if (has_leaf T G cg_lookup u') then 0 else length u') + (if (has_leaf T G cg_lookup v') then 0 else length v')"
define errorValue where errorValue: "errorValue = Suc minEst0"
define XY where XY: "XY = List.product (inputs_as_list M1) (outputs_as_list M1)"
define tryIO where tryIO: "tryIO = (λ (minEst,bestPrefix) (x,y) .
if minEst = 0
then (minEst,bestPrefix)
else (case get_extension T G cg_lookup u' x y of
Some u'' ⇒ (case get_extension T G cg_lookup v' x y of
Some v'' ⇒ if (h_obs M1 su x y = None) ≠ (h_obs M1 sv x y = None)
then (0,[])
else if h_obs M1 su x y = h_obs M1 sv x y
then (minEst,bestPrefix)
else (let (e,w) = get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k
in if e = 0
then (0,[])
else if e ≤ minEst
then (e,(x,y)#w)
else (minEst,bestPrefix)) |
None ⇒ (let e = estimate_growth M1 get_distinguishing_trace su sv x y errorValue;
e' = if e ≠ 1
then if has_leaf T G cg_lookup u''
then e + 1
else if ¬(has_leaf T G cg_lookup (u''@[(x,y)]))
then e + length u' + 1
else e
else e;
e'' = e' + (if ¬(has_leaf T G cg_lookup v') then length v' else 0)
in if e'' ≤ minEst
then (e'',[(x,y)])
else (minEst,bestPrefix))) |
None ⇒ (case get_extension T G cg_lookup v' x y of
Some v'' ⇒ (let e = estimate_growth M1 get_distinguishing_trace su sv x y errorValue;
e' = if e ≠ 1
then if has_leaf T G cg_lookup v''
then e + 1
else if ¬(has_leaf T G cg_lookup (v''@[(x,y)]))
then e + length v' + 1
else e
else e;
e'' = e' + (if ¬(has_leaf T G cg_lookup u') then length u' else 0)
in if e'' ≤ minEst
then (e'',[(x,y)])
else (minEst,bestPrefix)) |
None ⇒ (minEst,bestPrefix))))"

have res': "(get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v (Suc k)) =
(if ¬ isin T u' ∨ ¬ isin T v' then (errorValue,[]) else foldl tryIO (minEst0,[]) XY)"
unfolding tryIO XY errorValue minEst0 bestPrefix0 sv su v' u'
unfolding get_prefix_of_separating_sequence.simps Let_def
by force

show ?case proof (cases "¬ isin T u' ∨ ¬ isin T v'")
case True
then have *:"(get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v (Suc k)) = (errorValue,[])"
using res' by auto

show ?thesis
unfolding * fst_conv snd_conv errorValue
by (metis Suc.prems(1,3,5) Zero_not_Suc after_is_state append_Nil assms(1) assms(9))
next
case False

then have res: "(get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v (Suc k)) = foldl tryIO (minEst0,[]) XY"
using res' by auto

have "converge M1 u u'" and "converge M2 u u'"
unfolding u'
using shortest_list_or_default_elem[of "cg_lookup G u" u] assms(10) Suc.prems(1,2,3)
by (metis converge.elims(3) convergence_graph_lookup_invar_def insertE)+

have "converge M1 v v'" and "converge M2 v v'"
unfolding v'
using shortest_list_or_default_elem[of "cg_lookup G v" v] assms(10) Suc.prems
by (metis converge.elims(3) convergence_graph_lookup_invar_def insertE)+

have "su ∈ states M1"
unfolding su
using after_is_state[OF assms(1) Suc.prems(1)] .

have "sv ∈ states M1"
unfolding sv
using after_is_state[OF assms(1) Suc.prems(3)] .

define P where P: "P = (λ (ew :: (nat × ('b × 'c) list)) .
(fst ew = 0 ⟶ ¬ converge M2 u v)
∧ (fst ew ≠ 0 ⟶  (∃ γ . distinguishes M1 (after_initial M1 u) (after_initial M1 v) ((snd ew)@γ))))"

have "P (minEst0,[])"
proof -
have "distinguishes M1 (after_initial M1 u) (after_initial M1 v) bestPrefix0"
using assms(9)[of su sv]
using ‹su ∈ states M1› ‹sv ∈ states M1›
using Suc.prems(5)
unfolding bestPrefix0 su sv
by blast

moreover have "minEst0 ≠ 0"
unfolding minEst0
using calculation distinguishes_not_Nil[OF _ after_is_state[OF assms(1) Suc.prems(1)] after_is_state[OF assms(1) Suc.prems(3)]]
by auto
ultimately show ?thesis
unfolding P fst_conv snd_conv
by (metis append.left_neutral)
qed

have "errorValue > 0"
unfolding errorValue by auto

have "⋀ x y e w . e < errorValue ⟹ P (e,w) ⟹ P (tryIO (e,w) (x,y)) ∧ fst (tryIO (e,w) (x,y)) ≤ e"
proof -
fix x y e w
assume "e < errorValue" and "P (e,w)"

have *:"⋀ x y a b f . (case (x, y) of (x, y) ⇒ (λ(a, b). f x y a b)) (a,b)  = f x y a b"
by auto

show "P (tryIO (e,w) (x,y)) ∧ fst (tryIO (e,w) (x,y)) ≤ e"
proof (cases "e = 0")
case True
then have "tryIO (e,w) (x,y) = (e,w)"
unfolding P tryIO fst_conv snd_conv case_prod_conv
by auto
then show ?thesis
using ‹P (e,w)›
by auto
next
case False
show ?thesis
proof (cases "get_extension T G cg_lookup u' x y")
case None

show ?thesis
proof (cases "get_extension T G cg_lookup v' x y")
case None
then have "tryIO (e,w) (x,y) = (e,w)"
using ‹get_extension T G cg_lookup u' x y = None›
unfolding tryIO by auto
then show ?thesis
using ‹P (e,w)›
by auto
next
case (Some v'')

define c where c: "c = estimate_growth M1 get_distinguishing_trace su sv x y errorValue"
define c' where c': "c' = (if c ≠ 1 then if has_leaf T G cg_lookup v'' then c + 1 else if ¬(has_leaf T G cg_lookup (v''@[(x,y)])) then c + length v' + 1 else c else c)"
define c'' where c'': "c'' = c' + (if ¬(has_leaf T G cg_lookup u') then length u' else 0)"

have "tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))"
unfolding c c' c'' tryIO Let_def
using None Some False
by auto

show ?thesis proof (cases "c'' ≤ e")
case True
then have "c'' < errorValue"
using ‹e < errorValue› by auto
then have "c' < errorValue"
unfolding c'' by auto
then have "estimate_growth M1 get_distinguishing_trace su sv x y errorValue < errorValue"
unfolding c' c

have "c > 0"
using estimate_growth_Suc[OF ‹errorValue > 0›] unfolding c
by blast
then have "c'' > 0"
unfolding c' c''
then have "c'' ≠ 0"
by auto
then have "P (c'',[(x,y)])"
using True estimate_growth_result[OF assms(1,3) ‹su ∈ states M1› ‹sv ∈ states M1› ‹estimate_growth M1 get_distinguishing_trace su sv x y errorValue < errorValue›]
unfolding P fst_conv su sv snd_conv
by blast
then show ?thesis
using ‹tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))› True
by auto
next
case False
then show ?thesis
using ‹tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))› ‹P (e,w)›
by auto
qed
qed
next
case (Some u'')

show ?thesis proof (cases "get_extension T G cg_lookup v' x y")
case None

define c where c: "c = estimate_growth M1 get_distinguishing_trace su sv x y errorValue"
define c' where c': "c' = (if c ≠ 1 then if has_leaf T G cg_lookup u'' then c + 1 else if ¬(has_leaf T G cg_lookup (u''@[(x,y)])) then c + length u' + 1 else c else c)"
define c'' where c'': "c'' = c' + (if ¬(has_leaf T G cg_lookup v') then length v' else 0)"

have "tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))"
unfolding c c' c'' tryIO Let_def
using None Some False
by auto

show ?thesis proof (cases "c'' ≤ e")
case True
then have "c'' < errorValue"
using ‹e < errorValue› by auto
then have "c' < errorValue"
unfolding c'' by auto
then have "estimate_growth M1 get_distinguishing_trace su sv x y errorValue < errorValue"
unfolding c' c

have "c > 0"
using estimate_growth_Suc[OF ‹errorValue > 0›] unfolding c
by blast
then have "c'' > 0"
unfolding c' c''
then have "c'' ≠ 0"
by auto
then have "P (c'',[(x,y)])"
using True estimate_growth_result[OF assms(1,3) ‹su ∈ states M1› ‹sv ∈ states M1› ‹estimate_growth M1 get_distinguishing_trace su sv x y errorValue < errorValue›]
unfolding P fst_conv su sv snd_conv
by blast
then show ?thesis
using ‹tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))› True
by auto
next
case False
then show ?thesis
using ‹tryIO (e,w) (x,y) = (if c'' ≤ e then (c'',[(x,y)]) else (e,w))› ‹P (e,w)›
by auto
qed

next
case (Some v'')

have "u' ∈ L M1"
using ‹converge M1 u u'› converge.simps by blast
have "v' ∈ L M1"
using ‹converge M1 v v'› converge.simps by blast
have "u' ∈ L M2"
using ‹converge M2 u u'› converge.simps by blast
have "v' ∈ L M2"
using ‹converge M2 v v'› converge.simps by blast

have "converge M1 u' u''" and "u'' @ [(x, y)] ∈ set T"
using get_extension_result(1,3)[OF ‹u' ∈ L M1› ‹u' ∈ L M2› assms(10) ‹get_extension T G cg_lookup u' x y = Some u''›]
by blast+
then have "converge M1 u u''"
using ‹converge M1 u u'› by auto
then have "u'' ∈ set T ∩ L M1"
using set_prefix[OF ‹u'' @ [(x, y)] ∈ set T›] by auto

have "converge M1 v' v''" and "v'' @ [(x, y)] ∈ set T"
using get_extension_result[OF ‹v' ∈ L M1› ‹v' ∈ L M2› assms(10) ‹get_extension T G cg_lookup v' x y = Some v''›]
by blast+
then have "converge M1 v v''"
using ‹converge M1 v v'› by auto
then have "v'' ∈ set T ∩ L M1"
using set_prefix[OF ‹v'' @ [(x, y)] ∈ set T›] by auto

show ?thesis proof (cases "(h_obs M1 su x y = None) ≠ (h_obs M1 sv x y = None)")
case True

then have "tryIO (e,w) (x,y) = (0,[])"
using Some ‹get_extension T G cg_lookup u' x y = Some u''› False
unfolding tryIO Let_def by auto

have "¬ converge M2 u v"
proof -
note ‹L M1 ∩ set T = L M2 ∩ set T›

then have "u' ∈ L M2" and "v' ∈ L M2"
using False ‹u' ∈ L M1› ‹v' ∈ L M1› ‹¬ (¬ isin T u' ∨ ¬ isin T v')›
by auto

have "u'' ∈ L M2"
using ‹L M1 ∩ set T = L M2 ∩ set T› ‹u'' ∈ set T ∩ L M1›
by blast
then have "converge M2 u' u''"
using get_extension_result(2)[OF ‹u' ∈ L M1› ‹u' ∈ L M2› assms(10) ‹get_extension T G cg_lookup u' x y = Some u''›]
by blast
moreover note ‹converge M2 u u'›
ultimately have "converge M2 u u''"
by auto

have "v'' ∈ L M2"
using ‹L M1 ∩ set T = L M2 ∩ set T› ‹v'' ∈ set T ∩ L M1›
by blast
then have "converge M2 v' v''"
using get_extension_result(2)[OF ‹v' ∈ L M1› ‹v' ∈ L M2› assms(10) ‹get_extension T G cg_lookup v' x y = Some v''›]
by blast
moreover note ‹converge M2 v v'›
ultimately have "converge M2 v v''"
by auto

have "distinguishes M1 su sv ([(x,y)])"
using h_obs_distinguishes[OF assms(1), of su x y _ sv]
using distinguishes_sym[OF h_obs_distinguishes[OF assms(1), of sv x y _ su]]
using True
by (cases "h_obs M1 su x y"; cases "h_obs M1 sv x y"; metis)
then have "distinguishes M1 (after_initial M1 u) (after_initial M1 v) ([(x,y)])"
unfolding su sv by auto

show "¬ converge M2 u v"
using distinguish_converge_diverge[OF assms(1-3) _ _ ‹converge M1 u u''› ‹converge M1 v v''› ‹converge M2 u u''› ‹converge M2 v v''› ‹distinguishes M1 (after_initial M1 u) (after_initial M1 v) ([(x,y)])› ‹u'' @ [(x, y)] ∈ set T› ‹v'' @ [(x, y)] ∈ set T› ‹L M1 ∩ set T = L M2 ∩ set T›]
‹u'' ∈ set T ∩ L M1› ‹v'' ∈ set T ∩ L M1›
by blast
qed
then show ?thesis
unfolding P ‹tryIO (e,w) (x,y) = (0,[])› fst_conv snd_conv su sv
by blast

next
case False

show ?thesis proof (cases "h_obs M1 su x y = h_obs M1 sv x y")
case True

then have "tryIO (e,w) (x,y) = (e,w)"
using ‹get_extension T G cg_lookup u' x y = Some u''› Some
unfolding tryIO by auto
then show ?thesis
using ‹P (e,w)›
by auto
next
case False

then have "h_obs M1 su x y ≠ None" and "h_obs M1 sv x y ≠ None"
using ‹¬ (h_obs M1 su x y = None) ≠ (h_obs M1 sv x y = None)›
by metis+

have "u''@[(x,y)] ∈ L M1"
by (metis ‹converge M1 u u''› ‹h_obs M1 su x y ≠ None› after_language_iff assms(1) converge.elims(2) h_obs_language_single_transition_iff su)
have "v''@[(x,y)] ∈ L M1"
by (metis ‹converge M1 v v''› ‹h_obs M1 sv x y ≠ None› after_language_iff assms(1) converge.elims(2) h_obs_language_single_transition_iff sv)

have "u''@[(x,y)] ∈ L M2"
using ‹u''@[(x,y)] ∈ L M1› ‹u''@[(x,y)] ∈ set T› ‹L M1 ∩ set T = L M2 ∩ set T›
by blast
have "v''@[(x,y)] ∈ L M2"
using ‹v''@[(x,y)] ∈ L M1› ‹v''@[(x,y)] ∈ set T› ‹L M1 ∩ set T = L M2 ∩ set T›
by blast

have "FSM.after M1 (FSM.initial M1) (u'' @ [(x, y)]) ≠ FSM.after M1 (FSM.initial M1) (v'' @ [(x, y)])"
using False ‹converge M1 u u''› ‹converge M1 v v''› unfolding su sv
proof - (* auto-generated proof *)
assume a1: "h_obs M1 (FSM.after M1 (FSM.initial M1) u) x y ≠ h_obs M1 (FSM.after M1 (FSM.initial M1) v) x y"
have f2: "∀f ps psa. converge (f::('a, 'b, 'c) fsm) ps psa = (ps ∈ L f ∧ psa ∈ L f ∧ LS f (FSM.after f (FSM.initial f) ps) = LS f (FSM.after f (FSM.initial f) psa))"
by (meson converge.simps)
then have f3: "u ∈ L M1 ∧ u'' ∈ L M1 ∧ LS M1 (FSM.after M1 (FSM.initial M1) u) = LS M1 (FSM.after M1 (FSM.initial M1) u'')"
using ‹converge M1 u u''› by presburger
have f4: "∀f ps psa. ¬ minimal (f::('a, 'b, 'c) fsm) ∨ ¬ observable f ∨ ps ∉ L f ∨ psa ∉ L f ∨ converge f ps psa = (FSM.after f (FSM.initial f) ps = FSM.after f (FSM.initial f) psa)"
using convergence_minimal by blast
have f5: "v ∈ L M1 ∧ v'' ∈ L M1 ∧ LS M1 (FSM.after M1 (FSM.initial M1) v) = LS M1 (FSM.after M1 (FSM.initial M1) v'')"
using f2 ‹converge M1 v v''› by blast
then have f6: "FSM.after M1 (FSM.initial M1) v = FSM.after M1 (FSM.initial M1) v''"
using f4 ‹converge M1 v v''› assms(1) assms(3) by blast
have "FSM.after M1 (FSM.initial M1) u = FSM.after M1 (FSM.initial M1) u''"
using f4 f3 ‹converge M1 u u''› assms(1) assms(3) by blast
then show ?thesis
using f6 f5 f3 a1 by (metis (no_types) ‹u'' @ [(x, y)] ∈ L M1› ‹v'' @ [(x, y)] ∈ L M1› after_h_obs after_language_iff after_split assms(1) h_obs_from_LS)
qed

obtain e' w' where "get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k = (e',w')"
using prod.exhaust by metis

then have "tryIO (e,w) (x,y) = (if e' = 0 then (0,[]) else if e' ≤ e then (e',(x,y)#w') else (e,w))"
using ‹get_extension T G cg_lookup u' x y = Some u''› Some False ‹¬ (h_obs M1 su x y = None) ≠ (h_obs M1 sv x y = None)› ‹e ≠ 0›
unfolding tryIO Let_def by auto

show ?thesis proof (cases "e' = 0")
case True

have "¬ converge M2 u v"
proof -
note ‹L M1 ∩ set T = L M2 ∩ set T›
then have "u' ∈ L M2" and "v' ∈ L M2"
using ‹¬ (¬ isin T u' ∨ ¬ isin T v')› ‹u' ∈ L M1› ‹v' ∈ L M1›
by auto

have "u'' ∈ L M2"
using ‹L M1 ∩ set T = L M2 ∩ set T› ‹u'' ∈ set T ∩ L M1›
by blast
then have "converge M2 u' u''"
using get_extension_result(2)[OF ‹u' ∈ L M1› ‹u' ∈ L M2› assms(10) ‹get_extension T G cg_lookup u' x y = Some u''›]
by blast
moreover note ‹converge M2 u u'›
ultimately have "converge M2 u u''"
by auto

have "v'' ∈ L M2"
using ‹L M1 ∩ set T = L M2 ∩ set T› ‹v'' ∈ set T ∩ L M1›
by blast
then have "converge M2 v' v''"
using get_extension_result(2)[OF ‹v' ∈ L M1› ‹v' ∈ L M2› assms(10) ‹get_extension T G cg_lookup v' x y = Some v''›]
by blast
moreover note ‹converge M2 v v'›
ultimately have "converge M2 v v''"
by auto

have "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u'' @ [(x, y)]) (v'' @ [(x, y)]) k) = 0"
using True ‹get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k = (e',w')›
by auto
then have "¬ converge M2 (u'' @ [(x, y)]) (v'' @ [(x, y)])"
using Suc.IH[OF ‹u''@[(x,y)] ∈ L M1› ‹u''@[(x,y)] ∈ L M2› ‹v''@[(x,y)] ∈ L M1› ‹v''@[(x,y)] ∈ L M2› ‹FSM.after M1 (FSM.initial M1) (u'' @ [(x, y)]) ≠ FSM.after M1 (FSM.initial M1) (v'' @ [(x, y)])›]
using ‹L M1 ∩ Prefix_Tree.set T = L M2 ∩ Prefix_Tree.set T›
by blast
then have "¬ converge M2 u'' v''"
using diverge_prefix[OF assms(2) ‹u''@[(x,y)] ∈ L M2› ‹v''@[(x,y)] ∈ L M2›]
by blast
then show "¬ converge M2 u v"
using ‹converge M2 u u''› ‹converge M2 v v''›
by fastforce
qed
then show ?thesis
unfolding P ‹tryIO (e,w) (x,y) = (if e' = 0 then (0,[]) else if e' ≤ e then (e',(x,y)#w') else (e,w))› True fst_conv snd_conv su sv
by simp
next
case False

show ?thesis proof (cases "e' ≤ e")
case True
then have "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u'' @ [(x, y)]) (v'' @ [(x, y)]) k) ≠ 0"
using ‹get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k = (e',w')› False
by auto
then have "(∃γ. distinguishes M1 (FSM.after M1 (FSM.initial M1) (u'' @ [(x, y)])) (FSM.after M1 (FSM.initial M1) (v'' @ [(x, y)]))
(snd (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u'' @ [(x, y)]) (v'' @ [(x, y)]) k) @ γ))"
using Suc.IH[OF ‹u''@[(x,y)] ∈ L M1› ‹u''@[(x,y)] ∈ L M2› ‹v''@[(x,y)] ∈ L M1› ‹v''@[(x,y)] ∈ L M2› ‹FSM.after M1 (FSM.initial M1) (u'' @ [(x, y)]) ≠ FSM.after M1 (FSM.initial M1) (v'' @ [(x, y)])›]
by blast
then obtain γ where "distinguishes M1 (FSM.after M1 (FSM.initial M1) (u'' @ [(x, y)])) (FSM.after M1 (FSM.initial M1) (v'' @ [(x, y)])) (w'@γ)"
unfolding ‹get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace (u''@[(x,y)]) (v''@[(x,y)]) k = (e',w')›  snd_conv
by blast
have "distinguishes M1 (after_initial M1 u'') (after_initial M1 v'')  ((x,y)#(w'@γ))"
using distinguishes_after_initial_prepend[OF assms(1) language_prefix[OF ‹u''@[(x,y)] ∈ L M1›] language_prefix[OF ‹v''@[(x,y)] ∈ L M1›]]
by (metis Suc.prems(1) Suc.prems(3) ‹converge M1 u u'› ‹converge M1 u' u''› ‹converge M1 v v''› ‹distinguishes M1 (after_initial M1 (u'' @ [(x, y)])) (after_initial M1 (v'' @ [(x, y)])) (w' @ γ)› ‹h_obs M1 su x y ≠ None› ‹h_obs M1 sv x y ≠ None› ‹u' ∈ L M1› ‹u'' @ [(x, y)] ∈ L M1› ‹v'' @ [(x, y)] ∈ L M1› assms(1) assms(3) convergence_minimal language_prefix su sv)
then have "distinguishes M1 (after_initial M1 u) (after_initial M1 v)  (((x,y)#w')@γ)"
by (metis Cons_eq_appendI Suc.prems(1) Suc.prems(3) ‹converge M1 u u''› ‹converge M1 v v''› ‹u'' @ [(x, y)] ∈ L M1› ‹v'' @ [(x, y)] ∈ L M1› assms(1) assms(3) convergence_minimal language_prefix)

have "tryIO (e,w) (x,y) = (e',(x,y)#w')"
using ‹tryIO (e,w) (x,y) = (if e' = 0 then (0,[]) else if e' ≤ e then (e',(x,y)#w') else (e,w))› True False
by auto

show ?thesis
unfolding P ‹tryIO (e,w) (x,y) = (e',(x,y)#w')› fst_conv snd_conv
using ‹distinguishes M1 (after_initial M1 u) (after_initial M1 v) (((x,y)#w')@γ)›
False True
by blast
next
case False

then have "tryIO (e,w) (x,y) = (e,w)"
using ‹e' ≠ 0› ‹tryIO (e,w) (x,y) = (if e' = 0 then (0,[]) else if e' ≤ e then (e',(x,y)#w') else (e,w))›
by auto
then show ?thesis
using ‹P (e,w)›
by auto
qed
qed
qed
qed
qed
qed
qed
qed

have "minEst0 < errorValue"
unfolding errorValue by auto

have "P (foldl tryIO (minEst0,[]) XY) ∧ fst (foldl tryIO (minEst0,[]) XY) ≤ minEst0"
proof (induction XY rule: rev_induct)
case Nil
then show ?case
using ‹P (minEst0,[])›
by auto
next
case (snoc a XY)

obtain x y where "a = (x,y)"
using prod.exhaust by metis
moreover obtain e w where "(foldl tryIO (minEst0,[]) XY) = (e,w)"
using prod.exhaust by metis
ultimately have "(foldl tryIO (minEst0, []) (XY@[a])) = tryIO (e,w) (x,y)"
by auto

have "P (e,w)" and "e ≤ minEst0" and "e < errorValue"
using snoc.IH ‹minEst0 < errorValue›
unfolding ‹(foldl tryIO (minEst0,[]) XY) = (e,w)›
by auto

then show ?case
unfolding ‹(foldl tryIO (minEst0, []) (XY@[a])) = tryIO (e,w) (x,y)›
using ‹⋀ x y e w . e < errorValue ⟹ P (e,w) ⟹ P (tryIO (e,w) (x,y)) ∧ fst (tryIO (e,w) (x,y)) ≤ e›
using dual_order.trans by blast
qed

then have "P (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v (Suc k))"
unfolding res by blast
then show ?thesis
unfolding P by blast
qed
qed

then show "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) = 0 ⟹ ¬ converge M2 u v"
and  "fst (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k) ≠ 0 ⟹  ∃ γ . distinguishes M1 (after_initial M1 u) (after_initial M1 v) ((snd (get_prefix_of_separating_sequence M1 T G cg_lookup get_distinguishing_trace u v k))@γ)"
by blast+
qed

subsubsection ‹Distributing Convergent Traces›

fun append_heuristic_io :: "('b×'c) prefix_tree ⇒ ('b×'c) list ⇒ (('b×'c) list × int) ⇒ ('b×'c) list ⇒ (('b×'c) list × int)" where
"append_heuristic_io T w (uBest,lBest) u' = (let t' = after T u';
w' = maximum_prefix t' w
in if w' = w
then (u',0::int)
else if (is_maximal_in t' w' ∧ (int (length w') > lBest ∨ (int (length w') = lBest ∧ length u' < length uBest)))
then (u', int (length w'))
else (uBest,lBest))"

lemma append_heuristic_io_in :
"fst (append_heuristic_io T w (uBest,lBest) u') ∈ {u',uBest}"
unfolding append_heuristic_io.simps Let_def by auto

fun append_heuristic_input :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) list ⇒ (('b×'c) list × int) ⇒ ('b×'c) list ⇒ (('b×'c) list × int)" where
"append_heuristic_input M T w (uBest,lBest) u' = (let t' = after T u';
ws = maximum_fst_prefixes t' (map fst w) (outputs_as_list M)
in
foldr (λ w' (uBest',lBest'::int) .
if w' = w
then (u',0::int)
else if (int (length w') > lBest' ∨ (int (length w') = lBest' ∧ length u' < length uBest'))
then (u',int (length w'))
else (uBest',lBest'))
ws (uBest,lBest))"

lemma append_heuristic_input_in :
"fst (append_heuristic_input M T w (uBest,lBest) u') ∈ {u',uBest}"
proof -
define ws where ws: "ws = maximum_fst_prefixes (after T u') (map fst w) (outputs_as_list M)"
define f where f: "f = (λ w' (uBest',lBest'::int) .
if w' = w
then (u',0::int)
else if (int (length w') > lBest' ∨ (int (length w') = lBest' ∧ length u' < length uBest'))
then (u',int (length w'))
else (uBest',lBest'))"

have "⋀ w' b' . fst b' ∈ {u',uBest} ⟹ fst (f w' b') ∈ {u',uBest}"
unfolding f by auto
then have "fst (foldr f ws (uBest,lBest)) ∈ {u',uBest}"
by (induction ws; auto)
moreover have "append_heuristic_input M T w (uBest,lBest) u' = foldr f ws (uBest,lBest)"
unfolding append_heuristic_input.simps Let_def ws f by force
ultimately show ?thesis
by simp
qed

fun distribute_extension :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒('b×'c) list ⇒ ('b×'c) list ⇒ bool ⇒ (('b×'c) prefix_tree ⇒ ('b×'c) list ⇒ (('b×'c) list × int) ⇒ ('b×'c) list ⇒ (('b×'c) list × int)) ⇒ (('b×'c) prefix_tree ×'d)" where
"distribute_extension M T G cg_lookup cg_insert u w completeInputTraces append_heuristic = (let
cu = cg_lookup G u;
u0 = shortest_list_in_tree_or_default cu T u;
l0 = -1::int;
u' = fst ((foldl (append_heuristic T w) (u0,l0) (filter (isin T) cu)) :: (('b×'c) list × int));
T' = insert T (u'@w);
G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))
in if completeInputTraces
then let TC = complete_inputs_to_tree M (initial M) (outputs_as_list M) (map fst (u'@w));
T'' = Prefix_Tree.combine T' TC
in (T'',G')
else (T',G'))"

(* alternative implementation: consider inserting the intersection of L M and TC into G' *)
(*
fun distribute_extension :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒('b×'c) list ⇒ ('b×'c) list ⇒ bool ⇒ (('b×'c) prefix_tree ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ (('b×'c) list × int) ⇒ (('b×'c) list × int)) ⇒ (('b×'c) prefix_tree ×'d)" where
"distribute_extension M T G cg_lookup cg_insert u w completeInputTraces append_heuristic = (let
u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u;
l0 = -1::int;
u' = fst ((foldr (append_heuristic T w) (filter (isin T) (cg_lookup G u)) (u0,l0)) :: (('b×'c) list × int));
T' = insert T (u'@w);
G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))
in if completeInputTraces
then let lang = language_for_input M (after_initial M u') (map fst w);
T'' = combine_after T' u' (Prefix_Tree.from_list lang);
G'' = foldr (λ io G . cg_insert G (u'@io)) lang G'
in (T'',G'')
else (T',G'))"
*)

lemma distribute_extension_subset :
"set T ⊆ set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))"
proof -

define u0 where u0: "u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u"
define l0 where l0: "l0 = (-1::int)"
define u' where u': "u' = fst (foldl (heuristic T w) (u0,l0) (filter (isin T) (cg_lookup G u)))"
define T' where T': "T' = insert T (u'@w)"
define G' where G': "G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))"

have "set T ⊆ set T'"
unfolding T' insert_set
by blast

show ?thesis proof (cases b)
case True
then show ?thesis
using ‹set T ⊆ set T'›
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
using combine_set
by force
next
case False
then have "fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'"
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def by force
then show ?thesis
using ‹set T ⊆ set T'›
by blast
qed
qed

lemma distribute_extension_finite :
assumes "finite_tree T"
shows "finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))"
proof -

define u0 where u0: "u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u"
define l0 where l0: "l0 = (-1::int)"
define u' where u': "u' = fst (foldl (heuristic T w) (u0,l0) (filter (isin T) (cg_lookup G u)))"
define T' where T': "T' = insert T (u'@w)"
define G' where G': "G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))"

have "finite_tree T'"
unfolding T'
using insert_finite_tree[OF assms]
by blast

show ?thesis proof (cases b)
case True
then show ?thesis
using ‹finite_tree T'›
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
next
case False
then have "fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'"
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def by force
then show ?thesis
using ‹finite_tree T'›
by blast
qed
qed