# 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›

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
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}›
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)›
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"
```