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
                  using add_lessD1 by presburger
    
                have "c > 0"
                  using estimate_growth_Suc[OF errorValue > 0] unfolding c
                  by blast 
                then have "c'' > 0"
                  unfolding c' c''
                  using add_gr_0 by presburger 
                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
                  using add_lessD1 by presburger
    
                have "c > 0"
                  using estimate_growth_Suc[OF errorValue > 0] unfolding c
                  by blast 
                then have "c'' > 0"
                  unfolding c' c''
                  using add_gr_0 by presburger 
                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
      by (simp add: combine_finite_tree complete_inputs_to_tree_finite_tree)
  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
  

lemma distribute_extension_adds_sequence :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  assumes "observable M1"
  and     "minimal M1"
  and     "u  L M1" and "u  L M2"
  and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
  and     "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
  and     "(L M1  set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) = L M2  set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)))"
  and     " u' uBest lBest . fst (heuristic T w (uBest,lBest) u')  {u',uBest}"
shows " u' . converge M1 u u'  u'@w  set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))  converge M2 u u'"
and   "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 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<