Theory H_Framework

section ‹H-Framework›

text ‹This theory defines the H-Framework and provides completeness properties.›

theory H_Framework
imports Convergence_Graph "../Prefix_Tree" "../State_Cover"
begin


subsection ‹Abstract H-Condition›

(* assumes that V is a state cover assignment *)
definition satisfies_abstract_h_condition :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ nat ⇒ bool" where
  "satisfies_abstract_h_condition M1 M2 V m = (∀ q γ . 
    q ∈ reachable_states M1 ⟶ 
    length γ ≤ Suc (m-size_r M1) ⟶ 
    list.set γ ⊆ inputs M1 × outputs M1  ⟶ 
    butlast γ ∈ LS M1 q ⟶ 
    (let traces = (V ` reachable_states M1)
                  ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)} 
      in (L M1 ∩ traces = L M2 ∩ traces)
         ∧ preserves_divergence M1 M2 traces))"



lemma abstract_h_condition_exhaustiveness :
  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"
  and     "is_state_cover_assignment M V"
  and     "satisfies_abstract_h_condition M I V m"
shows "L M = L I"
proof (rule ccontr)
  assume "L M ≠ L I"

  (* unfold the sufficient condition for easier reference *)

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

  have pass_prop: "⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-n) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹
                    (L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                     = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and dist_prop: "⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-n) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹
                     preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
    using ‹satisfies_abstract_h_condition M I V m› 
    unfolding satisfies_abstract_h_condition_def Let_def Π n  by blast+

  have pass_prop_𝒳 : "⋀ q γ . q ∈ reachable_states M ⟹ γ ∈ 𝒳 q ⟹
                           (L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                            = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
   and dist_prop_𝒳 : "⋀ q γ . q ∈ reachable_states M ⟹ γ ∈ 𝒳 q ⟹
                           preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
  proof -
    fix q γ assume *: "q ∈ reachable_states M" and "γ ∈ 𝒳 q"
    then obtain io x y where "γ = io@[(x,y)]" and "io ∈ LS M q" and "length io ≤ m-n" and "x ∈ inputs M" and "y ∈ outputs M"
      unfolding 𝒳 by blast

    have **:"length γ ≤ Suc (m-n)"
      using ‹γ = io@[(x,y)]› ‹length io ≤ m-n› by auto
    have ***:"list.set γ ⊆ inputs M × outputs M"
      using language_io[OF ‹io ∈ LS M q›] ‹x ∈ inputs M› ‹y ∈ outputs M›
      unfolding ‹γ = io@[(x,y)]› by auto
    have ****:"butlast γ ∈ LS M q"
      unfolding ‹γ = io@[(x,y)]› using ‹io ∈ LS M q› by auto
    
    show "(L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                            = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
      using pass_prop[OF * ** *** ****] .
    show "preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
      using dist_prop[OF * ** *** ****] .
  qed


  (* obtain minimal trace that
      - extends some sequence of the state cover (which contains the empty sequence), and
      - is contained in either L M or L I *)
 
  have "(L M ∩ Π) = (L I ∩ Π)"
    using pass_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
  moreover have "Π ⊆ L M"
    unfolding Π using state_cover_assignment_after(1)[OF assms(1) ‹is_state_cover_assignment M V›]
    by blast
  ultimately have "Π ⊆ L I"
    using ‹Π = (V ` reachable_states M)› by blast

  obtain π τ' where "π ∈ Π"
                and "π @ τ' ∈ (L M - L I) ∪ (L I - L M)"
                and "⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io"
    using ‹(L M ∩ Π) = (L I ∩ Π)›
    using minimal_sequence_to_failure_from_state_cover_assignment_ob[OF ‹L M ≠ L I› ‹is_state_cover_assignment M V›] 
    unfolding Π
    by blast

  obtain q where "q ∈ reachable_states M" and "π = V q"
    using ‹π ∈ Π› unfolding Π by blast
  then have "π ∈ L M" and "after_initial M π = q"
    using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M V›]
    by blast+
  

  have τ'_min: "⋀ π' io . π' ∈ Π ⟹ π'@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io"
  proof -
    fix π' io
    assume "π' ∈ Π" and "π'@io ∈ (L M - L I) ∪ (L I - L M)"
    then obtain q where "q ∈ reachable_states M" and "π' = V q"
      unfolding Π by blast
    then show "length τ' ≤ length io"
      using ‹⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io›
            ‹π'@io ∈ (L M - L I) ∪ (L I - L M)› by auto
  qed


  

  obtain πτ xy τ'' where "π @ τ' = πτ @ [xy] @ τ''"
                      and "πτ ∈ L M ∩ L I"
                      and "πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)"
    using minimal_failure_prefix_ob[OF ‹observable M› ‹observable I› fsm_initial fsm_initial, of "π @ τ'"]
    using minimal_failure_prefix_ob[OF ‹observable I› ‹observable M› fsm_initial fsm_initial, of "π @ τ'"]
    using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
    by (metis Int_commute Un_iff)

  moreover obtain x y where "xy = (x,y)"
    using surjective_pairing by blast

  moreover have "πτ = π @ butlast τ'"
  proof -
    have "length πτ ≥ length π"
    proof (rule ccontr) 
      assume "¬ length π ≤ length πτ"
      then have "length (πτ@[xy]) ≤ length π"
        by auto
      then have "take (length (πτ@[xy])) π = πτ@[xy]"
        using ‹π @ τ' = πτ @ [xy] @ τ''›
        by (metis append_assoc append_eq_append_conv_if) 
      then have "π = (πτ@[xy]) @ (drop (length (πτ@[xy])) π)"
        by (metis append_take_drop_id)          
      then have "πτ@[xy] ∈ L M ∩ L I"
        using ‹π ∈ Π› ‹Π ⊆ L I› ‹Π ⊆ L M› 
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of M "initial M"]
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of I "initial I"]
        by auto
      then show "False"
        using ‹πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)› by blast
    qed

    then have "πτ = π @ (take (length πτ - length π) τ')"
      using ‹π @ τ' = πτ @ [xy] @ τ''›
      by (metis dual_order.refl take_all take_append take_le) 
    then have "π @ ((take (length πτ - length π) τ')@[xy]) ∈ (L I - L M) ∪ (L M - L I)"
      using ‹πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)›
      by (metis append_assoc)        
    then have "length τ' ≤ Suc (length (take (length πτ - length π) τ'))"
      using τ'_min[OF ‹π ∈ Π›]
      by (metis Un_commute length_append_singleton)
    moreover have "length τ' ≥ Suc (length (take (length πτ - length π) τ'))"
      using ‹π @ τ' = πτ @ [xy] @ τ''› ‹πτ = π @ take (length πτ - length π) τ'› not_less_eq_eq by fastforce
    ultimately have "length τ' = Suc (length (take (length πτ - length π) τ'))"
      by simp
    then show ?thesis
    proof -
      have "π @ τ' = (π @ take (length πτ - length π) τ') @ [xy] @ τ''"
        using ‹π @ τ' = πτ @ [xy] @ τ''› ‹πτ = π @ take (length πτ - length π) τ'› by presburger
      then have "take (length πτ - length π) τ' = butlast τ'"
        by (metis (no_types) ‹length τ' = Suc (length (take (length πτ - length π) τ'))› append_assoc append_butlast_last_id append_eq_append_conv diff_Suc_1 length_butlast length_greater_0_conv zero_less_Suc)
      then show ?thesis
        using ‹πτ = π @ take (length πτ - length π) τ'› by fastforce
    qed 
  qed

  ultimately have "π @ (butlast τ') ∈ L M ∩ L I"
              and "(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)"
    by auto

  have "τ' = (butlast τ')@[(x,y)]"
    using ‹π @ τ' = πτ @ [xy] @ τ''› ‹xy = (x,y)› 
    unfolding ‹πτ = π @ butlast τ'›
    by (metis (no_types, opaque_lifting) append_Cons append_butlast_last_id butlast.simps(1) butlast_append last_appendR list.distinct(1) self_append_conv)


  have "x ∈ inputs M" and "y ∈ outputs M"
  proof -
    have *: "(x,y) ∈ list.set ((π @ (butlast τ'))@[(x,y)])"
      by auto

    show "x ∈ inputs M"
      using ‹(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)› 
            language_io(1)[OF _ *, of I]
            language_io(1)[OF _ *, of M]
            ‹inputs I = inputs M›
      by blast

    show "y ∈ outputs M"
      using ‹(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)› 
            language_io(2)[OF _ *, of I]
            language_io(2)[OF _ *, of M]
            ‹outputs I = outputs M›
      by blast
  qed

  have "π @ (butlast τ') ∈ L M"
    using  ‹π @ (butlast τ') ∈ L M ∩ L I› by auto
  have "list.set (π @ τ') ⊆ inputs M × outputs M"
    using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
    using language_io[of ‹π @ τ'› M "initial M"]
    using language_io[of ‹π @ τ'› I "initial I"]
    unfolding assms(6,7) by fast 
  then have "list.set τ' ⊆ inputs M × outputs M"
    by auto
  have "list.set (butlast τ') ⊆ inputs M × outputs M"
    using language_io[OF ‹π @ (butlast τ') ∈ L M›] by force
  have "butlast τ' ∈ LS M q"
    using after_language_iff[OF assms(1) ‹π ∈ L M›] ‹π @ (butlast τ') ∈ L M›
    unfolding ‹after_initial M π = q›
    by blast

  have "length τ' > m - n + 1"
  proof (rule ccontr)
    assume "¬ m - n + 1 < length τ'"
    then have "length τ' ≤ Suc (m - n)"
      by auto

    have "π @ τ' ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes τ')})"
      unfolding ‹π = V q› using ‹q ∈ reachable_states M›  unfolding prefixes_set by auto
    then have "L M ∩ {π @ τ'} = L I ∩ {π @ τ'}"
      using pass_prop[OF ‹q ∈ reachable_states M› ‹length τ' ≤ Suc (m - n)› ‹list.set τ' ⊆ inputs M × outputs M› ‹butlast τ' ∈ LS M q›]
      by blast
    then show False
      using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)› by blast
  qed



  define τ where τ_def: "τ = (λi . take i (butlast τ'))"

  have "⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q"
  proof -
    fix i assume "i > 0" and "i ≤ m - n + 1"
    
    then have "τ i = (butlast (τ i)) @ [last (τ i)]"
      using τ_def ‹length τ' > m - n + 1›
      by (metis add_less_same_cancel2 append_butlast_last_id length_butlast less_diff_conv list.size(3) not_add_less2 take_eq_Nil) 

    have "length (butlast (τ i)) ≤ m - n" 
      using τ_def ‹length τ' > m - n + 1› ‹i ≤ m - n + 1› by auto


    have "q ∈ io_targets M π (initial M)"
      using ‹is_state_cover_assignment M V› ‹q ∈ reachable_states M› ‹π = V q›
      by simp 
    then have "(butlast τ') ∈ LS M q"
      using ‹π @ (butlast τ') ∈ L M ∩ L I› 
      using observable_io_targets_language[OF _ ‹observable M›] 
      by force
    then have "τ i @ (drop i (butlast τ')) ∈ LS M q"
      using τ_def by auto
    then have "τ i ∈ LS M q"
      using language_prefix
      by fastforce 
    then have "butlast (τ i) ∈ LS M q"
      using language_prefix ‹τ i = (butlast (τ i)) @ [last (τ i)]›
      by metis 

    have "(fst (last (τ i)), snd (last (τ i))) ∈ list.set ((butlast (τ i)) @ [last (τ i)])"
      using ‹τ i = (butlast (τ i)) @ [last (τ i)]›
      using in_set_conv_decomp by fastforce
    then have "fst (last (τ i)) ∈ inputs M" 
          and "snd (last (τ i)) ∈ outputs M"
      using ‹τ i ∈ LS M q› ‹τ i = (butlast (τ i)) @ [last (τ i)]› language_io[of "(butlast (τ i)) @ [last (τ i)]" M q "fst (last (τ i))" "snd (last (τ i))"] 
      by auto
      
    then show "τ i ∈ 𝒳 q"
      unfolding 𝒳 
      using ‹length (butlast (τ i)) ≤ m - n› ‹τ i = (butlast (τ i)) @ [last (τ i)]›
            ‹butlast (τ i) ∈ LS M q›
      by (metis (mono_tags, lifting) mem_Collect_eq surjective_pairing)
  qed

  have "⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I"
  proof -
    fix i assume "i ≤ m-n+1"

    have "butlast τ' = τ i @ (drop i (butlast τ'))"
      unfolding τ_def by auto
    then have ‹(π @ τ i) @ (drop i (butlast τ')) ∈ L M ∩ L I›
      using ‹π @ (butlast τ') ∈ L M ∩ L I›
      by auto
    then show "π @ (τ i) ∈ L M ∩ L I"
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of M "initial M"]
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of I "initial I"]
      by blast
  qed

  have B_diff: "Π ∩ (λi . π @ (τ i)) ` {1 .. m-n+1} = {}"
  proof -
    have "⋀ io1 io2 . io1 ∈ Π ⟹ io2 ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹ io1 ≠ io2"
    proof (rule ccontr)
      fix io1 io2 assume "io1 ∈ Π" "io2 ∈ (λi . π @ (τ i)) ` {1 .. m-n+1}" "¬ io1 ≠ io2"

      then obtain i where "io2 = π @ (τ i)" and "i ≥ 1" and "i ≤ m - n + 1" and "π @ (τ i) ∈ Π"
        by auto
      then have "π @ (τ i) ∈ L M"
        using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› by auto
      
      obtain q where "q ∈ reachable_states M" and "V q = π @ (τ i)"
        using ‹π @ (τ i) ∈ Π› Π
        by auto 
      moreover have "(π @ (τ i))@(drop i τ') ∈ (L M - L I) ∪ (L I - L M)"
        using τ_def ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)› ‹length τ' > m - n + 1› ‹i ≤ m - n + 1›
        by (metis append_assoc append_take_drop_id le_iff_sup sup.strict_boundedE take_butlast) 
      ultimately have "length τ' ≤ length (drop i τ')"
        using ‹⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io›
        by presburger
      then show "False"
        using ‹length τ' > m - n + 1› ‹i ≥ 1›
        by (metis One_nat_def ‹i ≤ m - n + 1› diff_diff_cancel diff_is_0_eq' le_trans length_drop less_Suc_eq nat_less_le) 
    qed
    then show ?thesis 
      by blast
  qed


  have same_targets_in_I: "∃ α β . 
                    α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}
                    ∧ β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}
                    ∧ α ≠ β ∧ (after_initial I α = after_initial I β)"
  proof - 
    have "after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}) ⊆ states I"
    proof 
      fix q assume "q ∈ after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})"
      then obtain io where "io ∈ (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})" and "q = after_initial I io"
        by blast
      then have "io ∈ L I"
        using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› ‹Π ⊆ L I› by auto
      then show "q ∈ states I"
        unfolding ‹q = after_initial I io› 
        using observable_after_path[OF ‹observable I›, of io "initial I"] path_target_is_state[of I "initial I"]
        by metis 
    qed
    then have "card (after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})) ≤ m"
      using ‹size I ≤ m› fsm_states_finite[of I] unfolding FSM.size_def
      by (meson card_mono le_trans) 
    moreover have "card (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}) = m+1"
    proof -
      have *: "card Π = n"
        using state_cover_assignment_card[OF ‹is_state_cover_assignment M V› ‹observable M›] unfolding Π n .
      have **: "card ((λi . π @ (τ i)) ` {1 .. m-n+1}) = m-n+1"
      proof -
        have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
          by auto
        moreover have "inj_on (λi . π @ (τ i)) {1 .. m-n+1}" 
        proof 
          fix x y assume "x ∈ {1..m - n + 1}" "y ∈ {1..m - n + 1}" "π @ τ x = π @ τ y"

          then have "take x τ' = take y τ'"
            unfolding τ_def ‹length τ' > m - n + 1›
            by (metis (no_types, lifting) ‹m - n + 1 < length τ'› atLeastAtMost_iff diff_is_0_eq le_trans nat_less_le same_append_eq take_butlast zero_less_diff)
          moreover have "x ≤ length τ'"
            using ‹x ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
          moreover have "y ≤ length τ'"
            using ‹y ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
          ultimately show "x=y"
            by (metis length_take min.absorb2) 
        qed
        moreover have "card {1..m - n + 1} = m - n + 1"
          by auto
        ultimately show ?thesis
          by (simp add: card_image) 
      qed

      have ***: "n + (m - n + 1) = m+1"
        unfolding n using ‹m ≥ size_r M› by auto

      have "finite Π"
        unfolding Π using fsm_states_finite restrict_to_reachable_states_simps(2)
        by (metis finite_imageI) 
      have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
        by auto
      
      show ?thesis
        using card_Un_disjoint[OF ‹finite Π› ‹finite ((λi. π @ τ i) ` {1..m - n + 1})› ‹Π ∩ (λi . π @ (τ i)) ` {1 .. m-n+1} = {}›]
        unfolding * ** *** .
    qed
    ultimately have *: "card (after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})) < card (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})"
      by simp
    
    show ?thesis
      using pigeonhole[OF *] unfolding inj_on_def by blast
  qed

  (* covered converging traces in I must also converge in M *)
  have same_targets_in_M: "⋀ α β . 
                    α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹
                    β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹
                    α ≠ β ⟹ 
                    (after_initial I α = after_initial I β) ⟹
                    (after_initial M α = after_initial M β)"
  proof (rule ccontr)
    fix α β assume "α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "α ≠ β"
               and "(after_initial I α = after_initial I β)"
               and "(after_initial M α ≠ after_initial M β)"


    have *: "(λi . π @ (τ i)) ` {1 .. m-n+1} ⊆ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
      using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q› ‹q ∈ reachable_states M› ‹π = V q›
      by force

    have "α ∈ L M" and "β ∈ L M" and "α ∈ L I" and "β ∈ L I"
      using ‹α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}› 
            ‹β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
            ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› 
            ‹Π ⊆ L M› ‹Π ⊆ L I› 
      by auto
    then have "¬ converge M α β" and "converge I α β"
      using ‹after_initial M α ≠ after_initial M β› 
      using ‹minimal M› 
      using after_is_state[OF assms(1) ‹α ∈ L M›]
      using after_is_state[OF assms(1) ‹β ∈ L M›]
      unfolding converge.simps minimal.simps ‹after_initial I α = after_initial I β› by auto
    then have "¬ converge M β α" and "converge I β α"
      using converge_sym by blast+

    
    have split_helper: "⋀ (P :: nat ⇒ nat ⇒ bool) . (∃ i j . P i j ∧ i ≠ j) = ((∃ i j . P i j ∧ i < j) ∨ (∃ i j . P i j ∧ i > j))"
    proof 
      show "⋀ (P :: nat ⇒ nat ⇒ bool) . ∃i j. P i j ∧ i ≠ j ⟹ (∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i)" 
      proof -
        fix P :: "nat ⇒ nat ⇒ bool" 
        assume "∃i j. P i j ∧ i ≠ j"
        then obtain i j where "P i j" and "i ≠ j" by auto
        then have "i < j ∨ i > j" by auto
        then show "(∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i)" using ‹P i j› by auto
      qed
      show "⋀ (P :: nat ⇒ nat ⇒ bool) . (∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i) ⟹ ∃i j. P i j ∧ i ≠ j" by auto
    qed
    have split_scheme:"(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α = π @ (τ i) ∧ β = π @ (τ j))
          = ((∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i < j ∧ α = π @ (τ i) ∧ β = π @ (τ j))
              ∨ (∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i > j ∧ α = π @ (τ i) ∧ β = π @ (τ j)))"
      using ‹α ≠ β›  
      using split_helper[of "λ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α = π @ (τ i) ∧ β = π @ (τ j)"]
      by blast

    consider "(α ∈ Π ∧ β ∈ Π)" |
             "(∃ i . i ∈ {1 .. m-n+1} ∧ α ∈ Π ∧ β = π @ (τ i))" |
             "(∃ i . i ∈ {1 .. m-n+1} ∧ β ∈ Π ∧ α = π @ (τ i))" |
             "(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i < j ∧ α = π @ (τ i) ∧ β = π @ (τ j))" |
             "(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i > j ∧ α = π @ (τ i) ∧ β = π @ (τ j))"
      using ‹α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
            ‹β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
      using split_scheme 
      by blast

    then have "∃ α' β' . α' ∈ L M ∧ β' ∈ L M ∧ ¬converge M α' β' ∧ converge I α' β' ∧
            ( (α' ∈ Π ∧ β' ∈ Π) 
              ∨ (∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i))
              ∨ (∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j)))"
      using ‹α ∈ L M› ‹β ∈ L M› ‹¬ converge M α β› ‹converge I α β› ‹¬ converge M β α› ‹converge I β α› 
      by metis

    then obtain α' β' where "α' ∈ L M" and "β' ∈ L M" and "¬converge M α' β'" and "converge I α' β' "
                        and "(α' ∈ Π ∧ β' ∈ Π) 
                              ∨ (∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i))
                              ∨ (∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j))"
      by blast
    then consider "α' ∈ Π ∧ β' ∈ Π"
      | "∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i)"
      | "∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j)"
      by blast

    then show False proof cases
      case 1
      moreover have "preserves_divergence M I Π"
        using dist_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
      ultimately show ?thesis 
        using ‹¬converge M α' β'› ‹converge I α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        unfolding preserves_divergence.simps 
        by blast
    next
      case 2
      then obtain i where "i ∈ {1 .. m-n+1}" and "α' ∈ Π" and "β' = π @ (τ i)"
        by blast
      then have "τ i ∈ 𝒳 q" 
        using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q›
        by force 

      have "β' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ i))}"
        unfolding ‹β' = π @ (τ i)› ‹π = V q› prefixes_set by auto 
      then have "¬converge I α' β'"
        using ‹α' ∈ Π› ‹¬converge M α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        using dist_prop_𝒳[OF ‹q ∈ reachable_states M› ‹τ i ∈ 𝒳 q›]
        unfolding preserves_divergence.simps by blast
      then show False
        using ‹converge I α' β'› by blast
    next
      case 3
      then obtain i j where "i ∈ {1 .. m-n+1}" and "j ∈ {1 .. m-n+1}" and "α' = π @ (τ i)" and "β' = π @ (τ j)" and "i < j" by blast
      then have "τ j ∈ 𝒳 q" 
        using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q›
        by force 

      have "(τ i) = take i (τ j)"
        using ‹i < j› unfolding τ_def
        by simp
      then have "(τ i) ∈ list.set (prefixes (τ j))"
        unfolding prefixes_set
        by (metis (mono_tags) append_take_drop_id mem_Collect_eq)
      then have "α' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ j))}"
        unfolding ‹α' = π @ (τ i)› ‹π = V q›
        by simp
      moreover have "β' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ j))}"
        unfolding ‹β' = π @ (τ j)› ‹π = V q› prefixes_set by auto 
      ultimately have "¬converge I α' β'"
        using ‹¬converge M α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        using dist_prop_𝒳[OF ‹q ∈ reachable_states M› ‹τ j ∈ 𝒳 q›]
        unfolding preserves_divergence.simps by blast
      then show False
        using ‹converge I α' β'› by blast
    qed
  qed


  have case_helper: "⋀ A B P . (⋀ x y . P x y = P y x) ⟹ 
                                (∃ x y . x ∈ A ∪ B ∧ y ∈ A ∪ B ∧ P x y) =
                                          ((∃ x y . x ∈ A ∧ y ∈ A ∧ P x y)
                                            ∨ (∃ x y . x ∈ A ∧ y ∈ B ∧ P x y)
                                            ∨ (∃ x y . x ∈ B ∧ y ∈ B ∧ P x y))"
    by auto
  have *: "(⋀x y. (x ≠ y ∧ FSM.after I (FSM.initial I) x = FSM.after I (FSM.initial I) y) =
          (y ≠ x ∧ FSM.after I (FSM.initial I) y = FSM.after I (FSM.initial I) x))"
    by auto
    
  consider (a) "∃ α β . α ∈ Π ∧ β ∈ Π ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" | 
           (b) "∃ α β . α ∈ Π ∧ β ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" |
           (c) "∃ α β . α ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ β ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" 
    using same_targets_in_I
    unfolding case_helper[of "λ x y . x ≠ y ∧ (after_initial I x = after_initial I y)" Π "(λi . π @ (τ i)) ` {1 .. m-n+1}", OF *] 
    by blast
  then show "False" proof cases
    case a (* elements of the state cover cannot coincide *)
    then obtain α β  where "α ∈ Π" and "β ∈ Π" and "α ≠ β" and "(after_initial I α = after_initial I β)" by blast
    then have "(after_initial M α = after_initial M β)"
      using same_targets_in_M by blast

    obtain q1 q2 where "q1 ∈ reachable_states M" and "α = V q1"
                   and "q2 ∈ reachable_states M" and "β = V q2"
      using ‹α ∈ Π› ‹β ∈ Π› ‹α ≠ β›
      unfolding Π by blast
    then have "q1 ≠ q2"
      using ‹α ≠ β› by auto

    have "α ∈ L M" 
      using ‹Π ⊆ L M› ‹α ∈ Π› by blast
    have "q1 = after_initial M α"
      using ‹is_state_cover_assignment M V› ‹q1 ∈ reachable_states M› observable_io_targets[OF ‹observable M› ‹α ∈ L M›] 
      unfolding is_state_cover_assignment.simps ‹α = V q1›
      by (metis ‹is_state_cover_assignment M V› assms(1) is_state_cover_assignment_observable_after)

    have "β ∈ L M" 
      using ‹Π ⊆ L M› ‹β ∈ Π› by blast
    have "q2 = after_initial M β"
      using ‹is_state_cover_assignment M V› ‹q2 ∈ reachable_states M› observable_io_targets[OF ‹observable M› ‹β ∈ L M›] 
      unfolding is_state_cover_assignment.simps ‹β = V q2›
      by (metis ‹is_state_cover_assignment M V› assms(1) is_state_cover_assignment_observable_after)

    show "False"
      using ‹q1 ≠ q2› ‹(after_initial M α = after_initial M β)›
      unfolding ‹q1 = after_initial M α› ‹q2 = after_initial M β› 
      by simp
  next
    case b (* state cover and π@(τ i) cannot coincide due to minimality of π@τ' *)
    then obtain α β where "α ∈ Π"
                      and "β ∈ (λi. π @ τ i) ` {1..m - n + 1}"
                      and "α ≠ β" 
                      and "FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β"
      by blast
    then have "FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β"
      using same_targets_in_M by blast

    obtain i where "β = π@(τ i)" and "i ∈ {1..m - n + 1}"
      using ‹β ∈ (λi. π @ τ i) ` {1..m - n + 1}› by auto

    have "α ∈ L M" and "α ∈ L I" 
      using ‹Π ⊆ L M›  ‹Π ⊆ L I› ‹α ∈ Π› by blast+
    have "β ∈ L M" and "β ∈ L I" 
      using ‹β ∈ (λi. π @ τ i) ` {1..m - n + 1}› ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› 
      by auto

    let ?io = "drop i τ'"

    have "τ' = (τ i) @ ?io"
      using ‹i ∈ {1..m - n + 1}› ‹length τ' > m-n+1› 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "β@?io ∈ (L M - L I) ∪ (L I - L M)"
      using ‹β = π@(τ i)›  ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
      by auto
    then have "α@?io ∈ (L M - L I) ∪ (L I - L M)"
      using observable_after_eq[OF ‹observable M› ‹FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β› ‹α ∈ L M› ‹β ∈ L M›]
            observable_after_eq[OF ‹observable I› ‹FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β› ‹α ∈ L I› ‹β ∈ L I›]
      by blast
    then show "False"
      using τ'_min[OF ‹α ∈ Π›, of ?io] ‹length τ' > m - n + 1› ‹i ∈ {1..m - n + 1}›
      by (metis One_nat_def add_diff_cancel_left' atLeastAtMost_iff diff_diff_cancel diff_is_0_eq' length_drop less_Suc_eq nat_le_linear not_add_less2)
  next
    case c (* π@(τ i) and π@(τ j) cannot coincide due to minimality of π@τ' *)
    then have "∃ i j  . i ≠ j ∧ i ∈ {1..m - n + 1} ∧ j ∈ {1..m - n + 1} ∧ (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by force
    then have "∃ i j  . i < j ∧ i ∈ {1..m - n + 1} ∧ j ∈ {1..m - n + 1} ∧ (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by (metis linorder_neqE_nat)
    then obtain i j  where "i ∈ {1..m - n + 1}"
                       and "j ∈ {1..m - n + 1}"
                       and "i < j"
                       and "FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))"
      by force

    have "(π@(τ i)) ∈ (λi. π @ τ i) ` {1..m - n + 1}" and "(π@(τ j)) ∈ (λi. π @ τ i) ` {1..m - n + 1}"
      using ‹i ∈ {1..m - n + 1}› ‹j ∈ {1..m - n + 1}›
      by auto
    moreover have "(π@(τ i)) ≠ (π@(τ j))"
    proof -
      have "j ≤ length (butlast τ')"
        using ‹j ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
      moreover have "⋀ xs . j ≤ length xs ⟹ i < j ⟹ take j xs ≠ take i xs"
        by (metis dual_order.strict_implies_not_eq length_take min.absorb2 min_less_iff_conj)
      ultimately show ?thesis
        using ‹i < j› unfolding τ_def
        by fastforce 
    qed
    ultimately have "FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j))"
      using ‹FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))›
            same_targets_in_M 
      by blast

    have "(π@(τ i)) ∈ L M" and "(π@(τ i)) ∈ L I" and "(π@(τ j)) ∈ L M" and "(π@(τ j)) ∈ L I" 
      using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› ‹i ∈ {1..m - n + 1}› ‹j ∈ {1..m - n + 1}› 
      by auto

    let ?io = "drop j τ'"
    have "τ' = (τ j) @ ?io"
      using ‹j ∈ {1..m - n + 1}› ‹length τ' > m-n+1› 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "(π@(τ j))@?io ∈ (L M - L I) ∪ (L I - L M)"
      using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
      by (simp add: τ_def)
    then have "(π@(τ i))@?io ∈ (L M - L I) ∪ (L I - L M)"
      using observable_after_eq[OF ‹observable M› ‹FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j))› ‹(π@(τ i)) ∈ L M› ‹(π@(τ j)) ∈ L M›]
            observable_after_eq[OF ‹observable I› ‹FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))› ‹(π@(τ i)) ∈ L I› ‹(π@(τ j)) ∈ L I›]
      by blast
    then have "π@(τ i)@?io ∈ (L M - L I) ∪ (L I - L M)"
      by auto
    moreover have "length τ' > length (τ i @ drop j τ')"
      using ‹length τ' > m - n + 1› ‹j ∈ {1..m - n + 1}› ‹i < j› unfolding τ_def by force
    ultimately show "False"
      using τ'_min[OF ‹π ∈ Π›, of "(τ i) @ ?io"] 
      by simp
  qed
qed



lemma abstract_h_condition_soundness :
  assumes "observable M"
  and     "observable I"
  and     "is_state_cover_assignment M V"
  and     "L M = L I"
shows "satisfies_abstract_h_condition M I V m"
  using assms(3,4) equivalence_preserves_divergence[OF assms(1,2,4)]
  unfolding satisfies_abstract_h_condition_def Let_def by blast
  


lemma abstract_h_condition_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"
  and     "is_state_cover_assignment M V"
shows "satisfies_abstract_h_condition M I V m ⟷ (L M = L I)"
  using abstract_h_condition_soundness[OF assms(1,2,8)]
  using abstract_h_condition_exhaustiveness[OF assms]
  by blast


    
subsection ‹Definition of the Framework›


definition h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment) ⇒                        
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ (('b×'c) prefix_tree × 'd)) ⇒
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('a,'b,'c) transition list ⇒ ('a,'b,'c) transition list) ⇒                              
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒ nat ⇒ ('a,'b,'c) transition ⇒  ('a,'b,'c) transition list ⇒ ( ('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd)) ⇒ 
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 'a ⇒ 'b ⇒ 'c ⇒ (('b×'c) prefix_tree) × 'd) ⇒ 
                              (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
                              ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                              ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
                              ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
                              nat ⇒
                              ('b×'c) prefix_tree" 
  where
  "h_framework M 
               get_state_cover 
               handle_state_cover
               sort_transitions
               handle_unverified_transition
               handle_unverified_io_pair
               cg_initial
               cg_insert
               cg_lookup
               cg_merge
               m
  = (let
      rstates_set = reachable_states M;
      rstates     = reachable_states_as_list M;
      rstates_io  = List.product rstates (List.product (inputs_as_list M) (outputs_as_list M));
      undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M q x y = None) rstates_io;
      V           = get_state_cover M;
      TG1         = handle_state_cover M V cg_initial cg_insert cg_lookup;
      sc_covered_transitions = (⋃ q ∈ rstates_set . covered_transitions M V (V q));
      unverified_transitions = sort_transitions M V (filter (λt . t_source t ∈ rstates_set ∧ t ∉ sc_covered_transitions) (transitions_as_list M));
      verify_transition = (λ (X,T,G) t . handle_unverified_transition M V T G cg_insert cg_lookup cg_merge m t X);
      TG2         = snd (foldl verify_transition (unverified_transitions, TG1) unverified_transitions);
      verify_undefined_io_pair = (λ T (q,(x,y)) . fst (handle_unverified_io_pair M V T (snd TG2) cg_insert cg_lookup q x y))
    in
      foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs)"


subsection ‹Required Conditions on Procedural Parameters›

definition separates_state_cover :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ (('b×'c) prefix_tree × 'd)) ⇒
                                  ('a,'b,'c) fsm ⇒
                                  ('e,'b,'c) fsm ⇒
                                  (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                  bool"
  where 
  "separates_state_cover f M1 M2 cg_initial cg_insert cg_lookup = 
    (∀ V .
        (V ` reachable_states M1 ⊆ set (fst (f M1 V cg_initial cg_insert cg_lookup)))
        ∧ finite_tree (fst (f M1 V cg_initial cg_insert cg_lookup))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            convergence_graph_initial_invar M1 M2 cg_lookup cg_initial ⟶
            L M1 ∩ set (fst (f M1 V cg_initial cg_insert cg_lookup)) = L M2 ∩ set (fst (f M1 V cg_initial cg_insert cg_lookup)) ⟶
            (preserves_divergence M1 M2 (V ` reachable_states M1)
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V cg_initial cg_insert cg_lookup)))))"


definition handles_transition :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                    ('a,'b,'c) state_cover_assignment ⇒
                                    ('b×'c) prefix_tree ⇒ 
                                    'd ⇒
                                    ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                    ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
                                    ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒ 
                                    nat ⇒
                                    ('a,'b,'c) transition ⇒ 
                                    ('a,'b,'c) transition list ⇒   
                                    (('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd)) ⇒   
                                  ('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                  ('e,'b,'c) fsm ⇒
                                  ('a,'b,'c) state_cover_assignment ⇒    
                                  ('b×'c) prefix_tree ⇒
                                  ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  bool"
  where 
  "handles_transition f M1 M2 V T0 cg_insert cg_lookup cg_merge = 
    (∀ T G m t X .
        (set T ⊆ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
        ∧ (finite_tree T ⟶ finite_tree (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            size_r M1 ≤ m ⟶
            size M2 ≤ m ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            preserves_divergence M1 M2 (V ` reachable_states M1) ⟶
            V ` reachable_states M1 ⊆ set T ⟶
            t ∈ transitions M1 ⟶
            t_source t ∈ reachable_states M1 ⟶
            ((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t)) ⟶  
            convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            convergence_graph_merge_invar M1 M2 cg_lookup cg_merge ⟶
            L M1 ∩ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) = L M2 ∩ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) ⟶
            (set T0 ⊆ set T) ⟶
            (∀ γ . (length γ ≤ (m-size_r M1) ∧ list.set γ ⊆ inputs M1 × outputs M1 ∧ butlast γ ∈ LS M1 (t_target t))
                    ⟶ ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                          = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                         ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})))   
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X)))))"


definition handles_io_pair :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                            ('a,'b,'c) state_cover_assignment ⇒
                                            ('b×'c) prefix_tree ⇒ 
                                            'd ⇒
                                            ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ 
                                            ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                            'a ⇒ 'b ⇒ 'c ⇒  
                                            (('b×'c) prefix_tree × 'd)) ⇒
                                          ('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                          ('e,'b,'c) fsm ⇒
                                          ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                          ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒                                     
                                          bool"
  where 
  "handles_io_pair f M1 M2 cg_insert cg_lookup = 
    (∀ V T G q x y .
        (set T ⊆ set (fst (f M1 V T G cg_insert cg_lookup q x y)))
        ∧ (finite_tree T ⟶ finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y)))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            L M1 ∩ (V ` reachable_states M1) = L M2 ∩ V ` reachable_states M1 ⟶
            q ∈ reachable_states M1 ⟶
            x ∈ inputs M1 ⟶ 
            y ∈ outputs M1 ⟶ 
            convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶   
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) ⟶
            ( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))))"



subsection ‹Completeness and Finiteness of the Scheme›


lemma unverified_transitions_handle_all_transitions :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: "⋀ t γ . t ∈ transitions M1 ⟹
                                            t_source t ∈ reachable_states M1 ⟹
                                            length γ ≤ k ⟹ 
                                            list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
                                            butlast γ ∈ LS M1 (t_target t) ⟹
                                            (V (t_target t) ≠ (V (t_source t))@[(t_input t, t_output t)]) ⟹
                                            ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                                               = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                                             ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: "⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹ L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}"
  and     "t ∈ transitions M1"
  and     "t_source t ∈ reachable_states M1"
  and     "length γ ≤ k"
  and     "list.set γ ⊆ inputs M1 × outputs M1"
  and     "butlast γ ∈ LS M1 (t_target t)"
shows "(L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
         = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
        ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
proof (cases "V (t_target t) ≠ V (t_source t) @ [(t_input t, t_output t)]")
  case True
  then show ?thesis 
    using handles_unverified_transitions[OF assms(7-11)] 
    by blast
next
  case False
  then have "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
    by simp
  have "⋀ γ . length γ ≤ k ⟹
             list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
             butlast γ ∈ LS M1 (t_target t) ⟹
             L M1 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) =
               L M2 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ∧
             preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
  proof -
    fix γ assume "length γ ≤ k" and "list.set γ ⊆ inputs M1 × outputs M1" and "butlast γ ∈ LS M1 (t_target t)"
    then show "L M1 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) =
                 L M2 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ∧
               preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
      using ‹t ∈ transitions M1› ‹t_source t ∈ reachable_states M1› ‹V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)›
    proof (induction γ arbitrary: t)
      case Nil
      have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes [])} = {V (t_target t)}"
        unfolding Nil by auto
      then have *: "(V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes [])}) = V ` reachable_states M1"
        using reachable_states_next[OF Nil.prems(5,4)] by blast
      show ?case 
        unfolding *
        using assms(3,4) 
        by blast
    next
      case (Cons xy γ)
      then obtain x y where "xy = (x,y)" by auto
      then have "x ∈ inputs M1" and "y ∈ outputs M1"
        using Cons.prems(2) by auto

      have "t_target t ∈ reachable_states M1"
        using reachable_states_next[OF Cons.prems(5,4)] by blast
      then have "after_initial M1 (V (t_target t)) = t_target t"
        using ‹is_state_cover_assignment M1 V› 
        by (metis assms(1) is_state_cover_assignment_observable_after)

      show ?case proof (cases "[xy] ∈ LS M1 (t_target t)")
        case False
        then have "h_obs M1 (t_target t) x y = None"
          using Cons.prems(4,5) ‹x ∈ inputs M1› ‹y ∈ outputs M1› unfolding ‹xy = (x,y)›
          by (meson assms(1) h_obs_language_single_transition_iff) 
        then have "L M1 ∩ {V (t_target t) @ [(x, y)]} = L M2 ∩ {V (t_target t) @ [(x, y)]}"
          using handles_undefined_io_pairs[OF ‹t_target t ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›] by blast      
        
        have "V (t_target t) @ [(x, y)] ∉ L M1"
          using False ‹after_initial M1 (V (t_target t)) = t_target t› 
          unfolding ‹xy = (x,y)›
          by (metis assms(1) language_prefix observable_after_language_none) 
        then have "preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})"
          using assms(4)
          unfolding preserves_divergence.simps
          by blast 

        have "γ = []"
          using False Cons.prems(3) 
          by (metis (no_types, lifting) LS_single_transition ‹xy = (x, y)› butlast.simps(2) language_next_transition_ob)
        then have "list.set (prefixes (xy#γ)) = {[], [(x,y)]}"
          unfolding ‹xy = (x,y)›
          by force 
        then have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {V (t_target t), V (t_target t) @ [(x, y)]}"
          unfolding Cons by auto
        then have *:"(V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))}) = (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})"
          using reachable_states_next[OF Cons.prems(5,4)] by blast

        

        show ?thesis 
          unfolding *
          using assms(3)
                ‹L M1 ∩ {V (t_target t) @ [(x, y)]} = L M2 ∩ {V (t_target t) @ [(x, y)]}›
                ‹preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})›    
          by blast
      next
        case True

        then obtain t' where "t_source t' = t_target t" and "t_input t' = x" and "t_output t' = y" and "t' ∈ transitions M1"
          unfolding ‹xy = (x,y)›
          by auto 
        then have "t_target t' ∈ reachable_states M1" and "t_source t' ∈ reachable_states M1"
          using reachable_states_next[OF ‹t_target t ∈ reachable_states M1›, of t'] ‹t_target t ∈ reachable_states M1› by auto

        have *: "length γ ≤ k"
          using Cons.prems(1) by auto
        have **: "list.set γ ⊆ inputs M1 × outputs M1"
          using Cons.prems(2) by auto
        have ***: "butlast γ ∈ LS M1 (t_target t')"
          using Cons.prems(3)
          by (metis True ‹t' ∈ FSM.transitions M1› ‹t_input t' = x› ‹t_output t' = y› ‹t_source t' = t_target t› ‹xy = (x, y)› assms(1) butlast.simps(1) butlast.simps(2) observable_language_transition_target)                
        
        have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∪ {V (t_source t) @ [(t_input t, t_output t)]}"
          by (induction γ; auto) 
        moreover have "{((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}"
          unfolding ‹t_source t' = t_target t› ‹t_input t' = x› ‹t_output t' = y› ‹xy = (x,y)›[symmetric] Cons.prems(6)[symmetric] by simp
        ultimately have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∪ {V (t_target t)}"
          unfolding Cons by force
        then have ****: "V ` reachable_states M1 ∪ {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}
                          = V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))}"
          using ‹t_source t' = t_target t› ‹t_source t' ∈ reachable_states M1› by force

      

        show ?thesis proof (cases "V (t_source t') @ [(t_input t', t_output t')] = V (t_target t')")
          case True
          show ?thesis
            using Cons.IH[OF * ** *** ‹t' ∈ transitions M1› ‹t_source t' ∈ reachable_states M1› True]
            unfolding **** .
        next
          case False
          then show ?thesis
            using handles_unverified_transitions[OF ‹t' ∈ transitions M1› ‹t_source t' ∈ reachable_states M1› * ** ***]
            unfolding ****
            by presburger
        qed
      qed
    qed
  qed
  then show ?thesis
    using assms(9-11)
    by blast
qed

lemma abstract_h_condition_by_transition_and_io_pair_coverage :
  assumes "observable M1"