Theory H_Method_Implementations

section ‹Implementations of the H-Method›

theory H_Method_Implementations
imports Intermediate_Frameworks Pair_Framework "../Distinguishability" Test_Suite_Representations "../OFSM_Tables_Refined" "HOL-Library.List_Lexorder"
begin

subsection ‹Using the H-Framework›

definition h_method_via_h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ ('b×'c) prefix_tree" where
  "h_method_via_h_framework = h_framework_dynamic (λ M V t X l . False)"

definition h_method_via_h_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ (('b×'c) × bool) list list" where
  "h_method_via_h_framework_lists M m completeInputTraces useInputHeuristic = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (h_method_via_h_framework M m completeInputTraces useInputHeuristic))"

lemma h_method_via_h_framework_completeness_and_finiteness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)) = (L M2 ∩ set (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)))"
and "finite_tree (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)"
  using h_framework_dynamic_completeness_and_finiteness[OF assms]
  unfolding h_method_via_h_framework_def 
  by blast+

lemma h_method_via_h_framework_lists_completeness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('d,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (initial M2)) (h_method_via_h_framework_lists M1 m completeInputTraces useInputHeuristic)"
  using h_framework_dynamic_lists_completeness[OF assms]
  unfolding h_method_via_h_framework_lists_def h_framework_dynamic_lists_def h_method_via_h_framework_def
  by blast



subsection ‹Using the Pair-Framework›

subsubsection ‹Selection of Distinguishing Traces›

fun add_distinguishing_sequence_if_required :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ ('a,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
  "add_distinguishing_sequence_if_required dist_fun M ((α,q1), (β,q2)) t = (if intersection_is_distinguishing M (after t α) q1 (after t β) q2
    then empty
    else insert empty (dist_fun q1 q2))"

lemma add_distinguishing_sequence_if_required_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "α ∈ L M"
  and     "β ∈ L M" 
  and     "after_initial M α ≠ after_initial M β" 
  and     "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) .  distinguishes M (after_initial M α) (after_initial M β) io"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
  case True
  then have "(add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t = empty"
    by auto
  then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) = (set (after t α) ∩ set (after t β))"
    using Prefix_Tree.set_empty
    by (metis Int_insert_right inf.absorb_iff2 inf_bot_right insert_is_Un set_Nil sup_absorb2) 
  moreover have "∃ io ∈ (set (after t α) ∩ set (after t β)) .  distinguishes M (after_initial M α) (after_initial M β) io"
    using True unfolding intersection_is_distinguishing_correctness[OF assms(1) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)]]
    by auto 
  ultimately show ?thesis 
    by blast
next
  case False
  then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = set (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
    by auto
  then have "dist_fun (after_initial M α) (after_initial M β) ∈ set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
    unfolding insert_set by auto
  then show ?thesis 
    using assms(6)[OF after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)] by blast
qed

lemma add_distinguishing_sequence_if_required_finite : 
  "finite_tree ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
  case True
  then have "((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = empty"
    by auto
  then show ?thesis
    using empty_finite_tree by simp
next
  case False
  then have "((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
    by auto
  then show ?thesis
    using insert_finite_tree[OF empty_finite_tree] by metis
qed

fun add_distinguishing_sequence_and_complete_if_required :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ bool ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
  "add_distinguishing_sequence_and_complete_if_required distFun completeInputTraces M ((α,q1), (β,q2)) t = 
    (if intersection_is_distinguishing M (after t α) q1 (after t β) q2
      then empty
      else let w = distFun q1 q2;
               T = insert empty w
            in if completeInputTraces 
              then let T1 = from_list (language_for_input M q1 (map fst w));
                       T2 = from_list (language_for_input M q2 (map fst w))
                   in Prefix_Tree.combine T (Prefix_Tree.combine T1 T2)
              else T)" 

lemma add_distinguishing_sequence_and_complete_if_required_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "α ∈ L M"
  and     "β ∈ L M" 
  and     "after_initial M α ≠ after_initial M β" 
  and     "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) .  distinguishes M (after_initial M α) (after_initial M β) io"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
  case True
  then have "(add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t = empty"
    by auto
  then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) = (set (after t α) ∩ set (after t β))"
    using Prefix_Tree.set_empty
    by (metis Int_insert_right inf.absorb_iff2 inf_bot_right insert_is_Un set_Nil sup_absorb2) 
  moreover have "∃ io ∈ (set (after t α) ∩ set (after t β)) .  distinguishes M (after_initial M α) (after_initial M β) io"
    using True unfolding intersection_is_distinguishing_correctness[OF assms(1) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)]]
    by auto 
  ultimately show ?thesis 
    by blast
next
  case False
  then have "set (insert empty (dist_fun (after_initial M α) (after_initial M β))) ⊆ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
    using combine_set[of "insert empty (dist_fun (after_initial M α) (after_initial M β))"] 
    unfolding add_distinguishing_sequence_and_complete_if_required.simps Let_def 
    by (cases c; fastforce)
  moreover have "dist_fun (after_initial M α) (after_initial M β) ∈ set (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
    unfolding insert_set by auto
  ultimately have "dist_fun (after_initial M α) (after_initial M β) ∈ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
    by blast
  then show ?thesis 
    using assms(6)[OF after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)] 
    by (meson distinguishes_def) 
qed

lemma add_distinguishing_sequence_and_complete_if_required_finite : 
  "finite_tree ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
  case True
  then have "((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) = empty"
    by auto
  then show ?thesis
    using empty_finite_tree by simp
next
  case False

  define w where w: "w = dist_fun (after_initial M α) (after_initial M β)"
  define T where T: "T = insert empty w"
  define T1 where T1: "T1 = from_list (language_for_input M (after_initial M α) (map fst w))"
  define T2 where T2: "T2 = from_list (language_for_input M (after_initial M β) (map fst w))"

  have "finite_tree T"
    using insert_finite_tree[OF empty_finite_tree]
    unfolding T by auto
  moreover have "finite_tree (Prefix_Tree.combine T (Prefix_Tree.combine T1 T2))"
    using combine_finite_tree[OF ‹finite_tree T› combine_finite_tree[OF from_list_finite_tree from_list_finite_tree]]
    unfolding T1 T2
    by auto
  ultimately show ?thesis
    using False
    unfolding add_distinguishing_sequence_and_complete_if_required.simps w T T1 T2 Let_def
    by presburger
qed




function find_cheapest_distinguishing_trace :: "('a,'b::linorder,'c::linorder) fsm ⇒ ('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ ('b×'c) list ⇒ ('b×'c) prefix_tree ⇒ 'a ⇒ ('b×'c) prefix_tree ⇒ 'a ⇒ (('b×'c) list × nat × nat)" where
  "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = 
    (let
      f = (λ (ω,l,w) (x,y) . if (x,y) ∉ list.set ios then (ω,l,w) else  
            (let 
              w1L = if (PT m1) = empty then 0 else 1;
              w1C = if (x,y) ∈ dom m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if (PT m2) = empty then 0 else 1;
              w2C = if (x,y) ∈ dom m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in 
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2' 
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' 
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
     in 
       foldl f (distFun q1 q2, 0, 3) ios)"
  by pat_completeness auto
termination   
proof -

  let ?f = "(λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"

  have "⋀(M::('a,'b::linorder,'c::linorder) fsm) 
          (distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list)) 
          (ios :: ('b×'c) list)
           m1 (q1::'a) m2 (q2::'a) x y t2' q1' q2'.
       ¬ (x, y) ∉ list.set ios ⟹
       m1 (x, y) = None ⟹
       m2 (x, y) = Some t2' ⟹
       ((M, distFun, ios, Prefix_Tree.empty, q1', t2', q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
  proof -
    fix M::"('a,'b::linorder,'c::linorder) fsm" 
    fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
    fix ios :: "('b×'c) list"
    fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
    fix t2'
    fix q1 q2 q1' q2' :: 'a
    fix x 
    fix y 

    assume "m1 (x, y) = None"
    assume "m2 (x, y) = Some t2'"
    assume "¬ (x, y) ∉ list.set ios"

    define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
    define post where "post = (M, distFun, ios, Prefix_Tree.empty::('b×'c) prefix_tree, q1', t2', q2')"

    have "height_over ios empty ≤ height_over ios (PT m1)"
      unfolding height_over.simps height_over_empty by auto
    then have "?f post < ?f pre" 
      unfolding pre_def post_def case_prod_conv
      by (meson ‹¬ (x, y) ∉ list.set ios› ‹m2 (x, y) = Some t2'› add_le_less_mono height_over_subtree_less) 
    then show "((M, distFun, ios, Prefix_Tree.empty, q1', t2', q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
      unfolding pre_def[symmetric] post_def[symmetric]
      by simp 
  qed

  moreover have "⋀(M::('a,'b::linorder,'c::linorder) fsm) 
          (distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list)) 
          (ios :: ('b×'c) list)
           m1 (q1::'a) m2 (q2::'a) x y t1' q1' q2'.
       ¬ (x, y) ∉ list.set ios ⟹
       m1 (x, y) = Some t1' ⟹
       m2 (x, y) = None ⟹
       ((M, distFun, ios, t1', q1', empty, q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
  proof -
    fix M::"('a,'b::linorder,'c::linorder) fsm" 
    fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
    fix ios :: "('b×'c) list"
    fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
    fix t1'
    fix q1 q2 q1' q2' :: 'a
    fix x :: 'b
    fix y :: 'c

    assume "m1 (x, y) = Some t1'"
    assume "m2 (x, y) = None"
    assume "¬ (x, y) ∉ list.set ios"


    define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
    define post where "post = (M, distFun, ios, t1', q1',  Prefix_Tree.empty::('b×'c) prefix_tree, q2')"

    have "height_over ios empty ≤ height_over ios (PT m2)"
      unfolding height_over.simps height_over_empty by auto
    then have "?f post < ?f pre" 
      unfolding pre_def post_def case_prod_conv
      by (meson ‹¬ (x, y) ∉ list.set ios› ‹m1 (x, y) = Some t1'› add_mono_thms_linordered_field(3) height_over_subtree_less)
    then show "((M, distFun, ios, t1', q1', Prefix_Tree.empty, q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
      unfolding pre_def[symmetric] post_def[symmetric]
      by simp 
  qed


  moreover have "⋀(M::('a,'b::linorder,'c::linorder) fsm) 
          (distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list)) 
          (ios :: ('b×'c) list)
           m1 (q1::'a) m2 (q2::'a) x y t1' t2' q1' q2'.
       ¬ (x, y) ∉ list.set ios ⟹
       m1 (x, y) = Some t1' ⟹
       m2 (x, y) = Some t2' ⟹
       ((M, distFun, ios, t1', q1', t2', q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
  proof -
    fix M::"('a,'b::linorder,'c::linorder) fsm" 
    fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
    fix ios :: "('b×'c) list"
    fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
    fix t1' t2' :: "('b×'c) prefix_tree"
    fix q1 q2 q1' q2' :: 'a
    fix x :: 'b
    fix y :: 'c

    define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
    define post where "post = (M, distFun, ios, t1', q1', t2', q2')"

    assume "m1 (x, y) = Some t1'"
    moreover assume "m2 (x, y) = Some t2'"
    moreover assume "¬ (x, y) ∉ list.set ios"
    ultimately have "?f post < ?f pre" 
      unfolding pre_def post_def case_prod_conv
      by (meson add_less_mono height_over_subtree_less)
    then show "((M, distFun, ios, t1', q1',t2', q2'), M, distFun, ios,
        PT m1, q1, PT m2, q2)
       ∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
      unfolding pre_def[symmetric] post_def[symmetric]
      by simp 
  qed

  ultimately show ?thesis
    by (relation "measure (λ (M,dF,ios,t1,q1,t2,q2) . height_over ios t1 + height_over ios t2)"; simp)
qed




(* removes the elem-check on (x,y) and ios *)
lemma find_cheapest_distinguishing_trace_alt_def :
  "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = 
    (let
      f = (λ (ω,l,w) (x,y). 
            (let 
              w1L = if (PT m1) = empty then 0 else 1;
              w1C = if (x,y) ∈ dom m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if (PT m2) = empty then 0 else 1;
              w2C = if (x,y) ∈ dom m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in  
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2' 
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'  
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
     in 
       foldl f (distFun q1 q2, 0, 3) ios)"
  (is "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = ?find_cheapest_distinguishing_trace")

proof -
  define f' where "f' = (λ (ω,l,w) (x,y) . 
            (let 
              w1L = if (PT m1) = empty then 0 else 1;
              w1C = if (x,y) ∈ dom m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if (PT m2) = empty then 0 else 1;
              w2C = if (x,y) ∈ dom m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in  
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' 
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"

  define f where "f = (λ (ω,l,w) (x,y) . if (x,y) ∉ list.set ios then (ω,l,w) else  
            (let 
              w1L = if (PT m1) = empty then 0 else 1;
              w1C = if (x,y) ∈ dom m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if (PT m2) = empty then 0 else 1;
              w2C = if (x,y) ∈ dom m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in 
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"
  then have "f = (λ y x . if x ∉ list.set ios then y else f' y x)"
    unfolding f'_def by fast
  moreover have "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = foldl f (distFun q1 q2, 0, 3) ios"
    unfolding find_cheapest_distinguishing_trace.simps f_def[symmetric] by auto
  ultimately have "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = foldl (λ y x . if x ∉ list.set ios then y else f' y x) (distFun q1 q2, 0, 3) ios"
    by auto
  then show ?thesis
    unfolding f'_def[symmetric]  
    using foldl_elem_check[of ios "list.set ios"]
    by auto
qed


lemma find_cheapest_distinguishing_trace_code[code] :
  "find_cheapest_distinguishing_trace M distFun ios (MPT m1) q1 (MPT m2) q2 = 
    (let
      f = (λ (ω,l,w) (x,y) . 
            (let 
              w1L = if is_leaf (MPT m1) then 0 else 1;
              w1C = if (x,y) ∈ Mapping.keys m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if is_leaf (MPT m2) then 0 else 1;
              w2C = if(x,y) ∈ Mapping.keys m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in  
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case Mapping.lookup m1 (x,y) of
                      None ⇒ (case Mapping.lookup m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2' 
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case Mapping.lookup m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'  
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
     in 
       foldl f (distFun q1 q2, 0, 3) ios)"
  unfolding find_cheapest_distinguishing_trace_alt_def MPT_def
  by (simp add: keys_dom_lookup) 



lemma find_cheapest_distinguishing_trace_is_distinguishing_trace :
  assumes "observable M"
  and     "minimal M"
  and     "q1 ∈ states M"
  and     "q2 ∈ states M" 
  and     "q1 ≠ q2"   
  and     "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (distFun q1 q2)"
shows "distinguishes M q1 q2 (fst (find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2))"
  using assms(3,4,5)
proof (induction "height_over ios t1 + height_over ios t2" arbitrary: t1 q1 t2 q2 rule: less_induct)
  case less

  obtain m1 where "t1 = PT m1"
    using prefix_tree.exhaust by blast
  obtain m2 where "t2 = PT m2"
    using prefix_tree.exhaust by blast


  define f where "f = (λ (ω,l,w) (x,y) . 
            (let 
              w1L = if (PT m1) = empty then 0 else 1;
              w1C = if (x,y) ∈ dom m1 then 0 else 1;
              w1 = min w1L w1C;
              w2L = if (PT m2) = empty then 0 else 1;
              w2C = if (x,y) ∈ dom m2 then 0 else 1;
              w2 = min w2L w2C;
              w' = w1 + w2
            in  
              case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' 
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"

  then have "find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2 = foldl f (distFun q1 q2, 0, 3) ios"
    unfolding ‹t1 = PT m1› ‹t2 = PT m2› 
    unfolding find_cheapest_distinguishing_trace_alt_def Let_def
    by fast

  define ios' where "ios'=ios"

  have "list.set ios' ⊆ list.set ios ⟹ distinguishes M q1 q2 (fst (foldl f (distFun q1 q2, 0, 3) ios'))"
  proof (induction ios' rule: rev_induct)
    case Nil
    then show ?case using assms(6)[OF less.prems] by auto
  next
    case (snoc xy ios')

    obtain x y where "xy = (x,y)"
      using prod.exhaust by metis
    moreover obtain ω l w where "(foldl f (distFun q1 q2, 0, 3) ios') = (ω,l,w)"
      using prod.exhaust by metis
    ultimately have "foldl f (distFun q1 q2, 0, 3) (ios'@[xy]) = f (ω,l,w) (x,y)"
      by auto
    
    have "distinguishes M q1 q2 ω"
      using ‹(foldl f (distFun q1 q2, 0, 3) ios') = (ω,l,w)› snoc by auto

    have "(x,y) ∈ list.set ios"
      using snoc.prems unfolding ‹xy = (x,y)› by auto

    define w1L where "w1L = (if (PT m1) = empty then 0 else 1::nat)"
    define w1C where "w1C = (if (x,y) ∈ dom m1 then 0 else 1::nat)"
    define w1 where "w1 = min w1L w1C"
    define w2L where "w2L = (if (PT m2) = empty then 0 else 1::nat)"
    define w2C where "w2C = (if (x,y) ∈ dom m2 then 0 else 1::nat)"
    define w2 where "w2 = min w2L w2C"
    define w' where "w' = w1 + w2"

    have *:"f (ω,l,w) (x,y) = (case h_obs M q1 x y of
                None ⇒ (case h_obs M q2 x y of 
                  None ⇒ (ω,l,w) |
                  Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
                Some q1' ⇒ (case h_obs M q2 x y of 
                  None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
                  Some q2' ⇒ (if q1' = q2' 
                    then (ω,l,w)
                    else (case m1 (x,y) of
                      None ⇒ (case m2 (x,y) of
                        None ⇒ let ω' = distFun q1' q2';
                                    l' = 2 + 2 * length ω'
                                in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) | 
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
                      Some t1' ⇒ (case m2 (x,y) of
                        None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
                        Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' 
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w))))))"
      unfolding w1_def w2_def w'_def w1L_def w1C_def w2L_def w2C_def
      unfolding f_def case_prod_conv Let_def 
      by fast

    have "distinguishes M q1 q2 (fst (f (ω,l,w) (x,y)))"
    proof (cases "h_obs M q1 x y")
      case None
      then show ?thesis proof (cases "h_obs M q2 x y")
        case None
        have "f (ω,l,w) (x,y) = (ω,l,w)"
          unfolding *
          unfolding ‹h_obs M q1 x y = None› None by auto
        then show ?thesis 
          using ‹distinguishes M q1 q2 ω› by auto
      next
        case (Some a)
        have "f (ω,l,w) (x,y) = (if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w))"
          unfolding * None Some by auto
        moreover have "distinguishes M q1 q2 [(x,y)]"
          using distinguishes_sym[OF h_obs_distinguishes[OF assms(1) Some None]] .
        ultimately show ?thesis
          using ‹distinguishes M q1 q2 ω› by auto
      qed
    next
      case (Some q1')
      then have "q1' ∈ states M"
        by (meson h_obs_state)
      
      show ?thesis proof (cases "h_obs M q2 x y")
        case None
        have "f (ω,l,w) (x,y) = (if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w))"
          unfolding * None Some by auto
        moreover have "distinguishes M q1 q2 [(x,y)]"
          using h_obs_distinguishes[OF assms(1) Some None] .
        ultimately show ?thesis
          using ‹distinguishes M q1 q2 ω› by auto
      next
        case (Some q2')     
        then have "q2' ∈ states M"
          by (meson h_obs_state)
        
        show ?thesis proof (cases "q1' = q2'")
          case True
          have "f (ω,l,w) (x,y) = (ω,l,w)"
            unfolding *
            unfolding ‹h_obs M q1 x y = Some q1'› Some True by auto
          then show ?thesis 
            using ‹distinguishes M q1 q2 ω› by auto
        next
          case False
          
          have dist': "⋀ ω . distinguishes M q1' q2' ω ⟹ distinguishes M q1 q2 ((x,y)#ω)"
            using distinguishes_after_prepend[OF assms(1), of q1 x y q2]
            using ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'›
            unfolding after_h_obs[OF assms(1) ‹h_obs M q1 x y = Some q1'›]
            unfolding after_h_obs[OF assms(1) ‹h_obs M q2 x y = Some q2'›] 
            by auto
          
          show ?thesis proof (cases "m1 (x,y)")
            case None
            show ?thesis proof (cases "m2 (x,y)")
              case None

              have **: "f (ω,l,w) (x,y) = (let ω' = distFun q1' q2';  l' = 2 + 2 * length ω'
                                       in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w))"
                unfolding *
                unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = None› ‹m2 (x, y) = None›
                using False
                by auto

              have "distinguishes M q1' q2' (distFun q1' q2')"
                using ‹q1' ∈ states M› ‹q2' ∈ states M› assms(6) False by blast
              then have "distinguishes M q1 q2 ((x,y)#(distFun q1' q2'))"
                using dist' by auto
              then  show ?thesis 
                using ‹distinguishes M q1 q2 ω›
                unfolding ** Let_def by auto
            next
              case (Some t2')

              have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
                                    in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w))"
                unfolding *
                unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = None› ‹m2 (x, y) = Some t2'›
                using False
                by auto

              obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios Prefix_Tree.empty q1' t2' q2' = (ω'', l'', w'')"
                using prod.exhaust by metis

              have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'))"
              proof -

                have "height_over ios empty + height_over ios t2' < height_over ios t1 + height_over ios t2"
                  using height_over_subtree_less[of m2 "(x,y)", OF ‹m2 (x,y) = Some t2'› ‹(x,y) ∈ list.set ios› ]
                  unfolding height_over_empty ‹t2 = PT m2›[symmetric]
                  by (simp add: ‹t1 = PT m1›)
                then show ?thesis
                  using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
                  by blast
              qed
              then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2')))"
                using dist' by blast
              then  show ?thesis 
                using ‹distinguishes M q1 q2 ω›                
                unfolding ** *** Let_def fst_conv case_prod_conv by auto
            qed
          next
            case (Some t1')
            show ?thesis proof (cases "m2 (x,y)")
              case None

              have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' 
                                in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w))"
                unfolding *
                unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = Some t1'› ‹m2 (x, y) = None›
                using False
                by auto

              obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' = (ω'', l'', w'')"
                using prod.exhaust by metis

              have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'))"
              proof -

                have "height_over ios t1' + height_over ios empty < height_over ios t1 + height_over ios t2"
                  using height_over_subtree_less[of m1 "(x,y)", OF ‹m1 (x,y) = Some t1'› ‹(x,y) ∈ list.set ios› ]
                  unfolding height_over_empty ‹t1 = PT m1›[symmetric]
                  by (simp add: ‹t2 = PT m2›)
                then show ?thesis
                  using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
                  by blast
              qed
              then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2')))"
                using dist' by blast
              then  show ?thesis 
                using ‹distinguishes M q1 q2 ω›                
                unfolding ** *** Let_def fst_conv case_prod_conv by auto
            next
              case (Some t2')

              have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' 
                                    in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w))"
                unfolding *
                unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = Some t1'› ‹m2 (x, y) = Some t2'›
                using False
                by auto
              obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' = (ω'', l'', w'')"
                using prod.exhaust by metis

              have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'))"
              proof -

                have "height_over ios t1' + height_over ios t2' < height_over ios t1 + height_over ios t2"
                  using height_over_subtree_less[of m1 "(x,y)", OF ‹m1 (x,y) = Some t1'› ‹(x,y) ∈ list.set ios› ]
                  using height_over_subtree_less[of m2 "(x,y)", OF ‹m2 (x,y) = Some t2'› ‹(x,y) ∈ list.set ios› ]
                  unfolding ‹t1 = PT m1›[symmetric] ‹t2 = PT m2›[symmetric]
                  by auto
                then show ?thesis
                  using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
                  by blast
              qed
              then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2')))"
                using dist' by blast
              then  show ?thesis 
                using ‹distinguishes M q1 q2 ω›                
                unfolding ** *** Let_def fst_conv case_prod_conv by auto
            qed
          qed
        qed
      qed
    qed
    then show ?case 
      unfolding ‹foldl f (distFun q1 q2, 0, 3) (ios'@[xy]) = f (ω,l,w) (x,y)› .
  qed 
      

  then show ?case 
    unfolding ‹find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2 = foldl f (distFun q1 q2, 0, 3) ios›
              ‹ios' = ios›
    by blast
qed


fun add_cheapest_distinguishing_trace :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ bool ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
  "add_cheapest_distinguishing_trace distFun completeInputTraces M ((α,q1), (β,q2)) t = 
    (let w = (fst (find_cheapest_distinguishing_trace M distFun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) q1 (after t β) q2));
         T = insert empty w
      in if completeInputTraces 
        then let T1 = complete_inputs_to_tree M q1 (outputs_as_list M) (map fst w);
                 T2 = complete_inputs_to_tree M q2 (outputs_as_list M) (map fst w)
             in Prefix_Tree.combine T (Prefix_Tree.combine T1 T2)
        else T)" 


lemma add_cheapest_distinguishing_trace_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "α ∈ L M"
  and     "β ∈ L M" 
  and     "after_initial M α ≠ after_initial M β" 
  and     "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) .  distinguishes M (after_initial M α) (after_initial M β) io"
proof -
  define w where "w = (fst (find_cheapest_distinguishing_trace M dist_fun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) (after_initial M α) (after t β) (after_initial M β)))"

  have "set (insert empty w) ⊆ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
    using combine_set[of "insert empty w"] w_def
    unfolding add_cheapest_distinguishing_trace.simps Let_def 
    by (cases c; fastforce)
  moreover have "w ∈ set (insert empty w)"
    unfolding insert_set by auto
  ultimately have "w ∈ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
    by blast
  moreover have "distinguishes M (after_initial M α) (after_initial M β) w"
    using find_cheapest_distinguishing_trace_is_distinguishing_trace[OF assms(1,2) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5,6)]
    unfolding w_def 
    by blast
  ultimately show ?thesis 
    by blast 
qed

lemma add_cheapest_distinguishing_trace_finite : 
  "finite_tree ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof -

  define w where w: "w = (fst (find_cheapest_distinguishing_trace M dist_fun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) (after_initial M α) (after t β) (after_initial M β)))"
  define T where T: "T = insert empty w"
  define T1 where T1: "T1 = complete_inputs_to_tree M (after_initial M α) (outputs_as_list M) (map fst w)"
  define T2 where T2: "T2 = complete_inputs_to_tree M (after_initial M β) (outputs_as_list M) (map fst w)"

  have "finite_tree T"
    using insert_finite_tree[OF empty_finite_tree]
    unfolding T by auto
  moreover have "finite_tree (Prefix_Tree.combine T (Prefix_Tree.combine T1 T2))"
    using combine_finite_tree[OF ‹finite_tree T› combine_finite_tree[OF complete_inputs_to_tree_finite_tree complete_inputs_to_tree_finite_tree]]
    unfolding T1 T2
    by auto
  ultimately show ?thesis
    unfolding add_cheapest_distinguishing_trace.simps w T T1 T2 Let_def
    by presburger
qed





subsubsection ‹Implementation›

definition h_method_via_pair_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ ('b×'c) prefix_tree" where
  "h_method_via_pair_framework M m = pair_framework_h_components M m (add_distinguishing_sequence_if_required (get_distinguishing_sequence_from_ofsm_tables M))"

lemma h_method_via_pair_framework_completeness_and_finiteness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework M m) = L I ∩ set (h_method_via_pair_framework M m))"
and   "finite_tree (h_method_via_pair_framework M m)"
  using pair_framework_h_components_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_distinguishing_sequence_if_required (get_distinguishing_sequence_from_ofsm_tables M))", OF add_distinguishing_sequence_if_required_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_distinguishing_sequence_if_required_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
  using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
  unfolding h_method_via_pair_framework_def[symmetric]
  by blast+

definition h_method_via_pair_framework_2 :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ ('b×'c) prefix_tree" where
  "h_method_via_pair_framework_2 M m c = pair_framework_h_components M m (add_distinguishing_sequence_and_complete_if_required (get_distinguishing_sequence_from_ofsm_tables M) c)"

lemma h_method_via_pair_framework_2_completeness_and_finiteness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework_2 M m c) = L I ∩ set (h_method_via_pair_framework_2 M m c))"
and   "finite_tree (h_method_via_pair_framework_2 M m c)"
  using pair_framework_h_components_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_distinguishing_sequence_and_complete_if_required (get_distinguishing_sequence_from_ofsm_tables M) c)", OF add_distinguishing_sequence_and_complete_if_required_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_distinguishing_sequence_and_complete_if_required_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
  using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
  unfolding h_method_via_pair_framework_2_def[symmetric]
  by blast+

definition h_method_via_pair_framework_3 :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ ('b×'c) prefix_tree" where
  "h_method_via_pair_framework_3 M m c1 c2 = pair_framework_h_components_2 M m (add_cheapest_distinguishing_trace (get_distinguishing_sequence_from_ofsm_tables M) c2) c1"

lemma h_method_via_pair_framework_3_completeness_and_finiteness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework_3 M m c1 c2) = L I ∩ set (h_method_via_pair_framework_3 M m c1 c2))"
and   "finite_tree (h_method_via_pair_framework_3 M m c1 c2)"
  using pair_framework_h_components_2_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_cheapest_distinguishing_trace (get_distinguishing_sequence_from_ofsm_tables M) c2)", OF add_cheapest_distinguishing_trace_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_cheapest_distinguishing_trace_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
  using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
  unfolding h_method_via_pair_framework_3_def[symmetric]
  by blast+


definition h_method_via_pair_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ (('b×'c) × bool) list list" where
  "h_method_via_pair_framework_lists M m = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (h_method_via_pair_framework M m))"

lemma h_method_implementation_lists_completeness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
shows "(L M = L I) ⟷ list_all (passes_test_case I (initial I)) (h_method_via_pair_framework_lists M m)"
unfolding h_method_via_pair_framework_lists_def
            h_method_via_pair_framework_completeness_and_finiteness(1)[OF assms]
            passes_test_cases_from_io_tree[OF assms(1,2) fsm_initial fsm_initial h_method_via_pair_framework_completeness_and_finiteness(2)[OF assms]]
  by blast

subsubsection ‹Code Equations›

(* to avoid repeated computation of the same OFSM-tables by get_distinguishing_sequence_from_ofsm_tables,
   we pre-compute all distinguishing traces *)
lemma h_method_via_pair_framework_code[code] :
  "h_method_via_pair_framework M m = (let 
    tables = (compute_ofsm_tables M (size M - 1));
    distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                      (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
    distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
    distFun = add_distinguishing_sequence_if_required distHelper 
  in pair_framework_h_components M m distFun)"
  unfolding h_method_via_pair_framework_def
  apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
  unfolding Let_def
  by presburger

lemma h_method_via_pair_framework_2_code[code] :
  "h_method_via_pair_framework_2 M m c = (let 
    tables = (compute_ofsm_tables M (size M - 1));
    distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                      (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
    distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
    distFun = add_distinguishing_sequence_and_complete_if_required distHelper c
  in pair_framework_h_components M m distFun)"
  unfolding h_method_via_pair_framework_2_def
  apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
  unfolding Let_def
  by presburger

lemma h_method_via_pair_framework_3_code[code] :
  "h_method_via_pair_framework_3 M m c1 c2 = (let 
    tables = (compute_ofsm_tables M (size M - 1));
    distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                      (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
    distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
    distFun = add_cheapest_distinguishing_trace distHelper c2 
  in pair_framework_h_components_2 M m distFun c1)"
  unfolding h_method_via_pair_framework_3_def 
  apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
  unfolding Let_def
  by presburger

end