Theory Convergence
section ‹Convergence of Traces›
text ‹This theory defines convergence of traces in observable FSMs and provides results on
sufficient conditions to establish that two traces converge.
Furthermore it is shown how convergence can be employed in proving language equivalence.›
theory Convergence
imports "../Minimisation" "../Distinguishability" "../State_Cover" "HOL-Library.List_Lexorder"
begin
subsection ‹Basic Definitions›
fun converge :: "('a,'b,'c) fsm ⇒ ('b × 'c) list ⇒ ('b × 'c) list ⇒ bool" where
"converge M π τ = (π ∈ L M ∧ τ ∈ L M ∧ (LS M (after_initial M π) = LS M (after_initial M τ)))"
fun preserves_divergence :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
"preserves_divergence M1 M2 A = (∀ α ∈ L M1 ∩ A . ∀ β ∈ L M1 ∩ A . ¬ converge M1 α β ⟶ ¬ converge M2 α β)"
fun preserves_convergence :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
"preserves_convergence M1 M2 A = (∀ α ∈ L M1 ∩ A . ∀ β ∈ L M1 ∩ A . converge M1 α β ⟶ converge M2 α β)"
lemma converge_refl :
assumes "α ∈ L M"
shows "converge M α α"
using assms by auto
lemma convergence_minimal :
assumes "minimal M"
and "observable M"
and "α ∈ L M"
and "β ∈ L M"
shows "converge M α β = ((after_initial M α) = (after_initial M β))"
proof
have *:"(after_initial M α) ∈ states M"
using ‹α ∈ L M› by (meson after_is_state assms(2))
have **:"(after_initial M β) ∈ states M"
using ‹β ∈ L M› by (meson after_is_state assms(2))
show "converge M α β ⟹ ((after_initial M α) = (after_initial M β))"
using * ** ‹minimal M› unfolding minimal.simps converge.simps
by blast
show "((after_initial M α) = (after_initial M β)) ⟹ converge M α β"
unfolding converge.simps using assms(3,4) by simp
qed
lemma state_cover_assignment_diverges :
assumes "observable M"
and "minimal M"
and "is_state_cover_assignment M f"
and "q1 ∈ reachable_states M"
and "q2 ∈ reachable_states M"
and "q1 ≠ q2"
shows "¬ converge M (f q1) (f q2)"
proof -
have "f q1 ∈ L M"
using assms(3,4)
by (metis from_FSM_language is_state_cover_assignment.simps language_contains_empty_sequence language_io_target_append language_prefix reachable_state_is_state)
moreover have "q1 ∈ io_targets M (f q1) (initial M)"
using assms(3,4) unfolding is_state_cover_assignment.simps by blast
ultimately have "(after_initial M (f q1)) = q1"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)
have "f q2 ∈ L M"
using assms(3,5)
by (metis from_FSM_language is_state_cover_assignment.simps language_contains_empty_sequence language_io_target_append language_prefix reachable_state_is_state)
moreover have "q2 ∈ io_targets M (f q2) (initial M)"
using assms(3,5) unfolding is_state_cover_assignment.simps by blast
ultimately have "(after_initial M (f q2)) = q2"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)
show ?thesis
using convergence_minimal[OF assms(2,1) ‹f q1 ∈ L M› ‹f q2 ∈ L M›] ‹q1 ≠ q2›
unfolding ‹(after_initial M (f q1)) = q1› ‹(after_initial M (f q2)) = q2›
by simp
qed
lemma converge_extend :
assumes "observable M"
and "converge M α β"
and "α@γ ∈ L M"
and "β ∈ L M"
shows "β@γ ∈ L M"
by (metis after_io_targets assms(1) assms(2) assms(3) assms(4) converge.simps language_io_target_append language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)
lemma converge_append :
assumes "observable M"
and "converge M α β"
and "α@γ ∈ L M"
and "β ∈ L M"
shows "converge M (α@γ) (β@γ)"
using after_language_append_iff[OF assms(1,3)]
using after_language_append_iff[OF assms(1) converge_extend[OF assms]]
using assms converge_extend
unfolding converge.simps
by blast
lemma non_initialized_state_cover_assignment_diverges :
assumes "observable M"
and "minimal M"
and "⋀ q . q ∈ reachable_states M ⟹ q ∈ io_targets M (f q) (initial M)"
and "⋀ q . q ∈ reachable_states M ⟹ f q ∈ L M ∩ SC"
and "q1 ∈ reachable_states M"
and "q2 ∈ reachable_states M"
and "q1 ≠ q2"
shows "¬ converge M (f q1) (f q2)"
proof -
have "f q1 ∈ L M"
using assms(4,5) by blast
moreover have "q1 ∈ io_targets M (f q1) (initial M)"
using assms(3,5) by blast
ultimately have "(after_initial M (f q1)) = q1"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)
have "f q2 ∈ L M"
using assms(4,6) by blast
moreover have "q2 ∈ io_targets M (f q2) (initial M)"
using assms(3,6) by blast
ultimately have "(after_initial M (f q2)) = q2"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)
show ?thesis
using convergence_minimal[OF assms(2,1) ‹f q1 ∈ L M› ‹f q2 ∈ L M›] ‹q1 ≠ q2›
unfolding ‹(after_initial M (f q1)) = q1› ‹(after_initial M (f q2)) = q2›
by simp
qed
lemma converge_trans_2 :
assumes "observable M" and "minimal M" and "converge M u v"
shows "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
proof -
have "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2) ∧ converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2) ∧ converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
proof (cases "u@w1 ∈ L M ∧ u@w2 ∈ L M")
case False
then consider "u@w1 ∉ L M" | "u@w2 ∉ L M"
by blast
then have "v@w1 ∉ L M ∨ v@w2 ∉ L M"
using after_language_iff[OF assms(1), of u "initial M" w1]
after_language_iff[OF assms(1), of u "initial M" w2]
after_language_iff[OF assms(1), of v "initial M" w1]
after_language_iff[OF assms(1), of v "initial M" w2]
by (metis assms(3) converge.elims(2))
then show ?thesis
by (meson assms(1) assms(3) converge.elims(2) converge_extend)
next
case True
then have "u@w1 ∈ L M" and "u@w2 ∈ L M" by auto
then have "v@w1 ∈ L M" and "v@w2 ∈ L M"
by (meson assms(1) assms(3) converge.simps converge_extend)+
have "u ∈ L M" using ‹u@w1 ∈ L M› language_prefix by metis
have "v ∈ L M" using ‹v@w1 ∈ L M› language_prefix by metis
have "after_initial M u = after_initial M v"
using ‹u ∈ L M› ‹v ∈ L M› assms(1) assms(2) assms(3) convergence_minimal by blast
moreover have "after_initial M (u @ w1) = after_initial M (v @ w1)"
by (metis calculation True ‹v @ w1 ∈ L M› after_split assms(1))
ultimately have "after_initial M (u @ w2) = after_initial M (v @ w2)"
by (metis (no_types) True ‹v @ w2 ∈ L M› after_split assms(1))
have "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
using True ‹after_initial M (u @ w1) = after_initial M (v @ w1)› ‹after_initial M (u @ w2) = after_initial M (v @ w2)› ‹v @ w1 ∈ L M› ‹v @ w2 ∈ L M›
by auto
moreover have "converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
using True ‹after_initial M (u @ w2) = after_initial M (v @ w2)› ‹v @ w2 ∈ L M› by auto
moreover have "converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
using True ‹after_initial M (u @ w1) = after_initial M (v @ w1)› ‹v @ w1 ∈ L M› by auto
ultimately show ?thesis
by blast
qed
then show "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
by blast+
qed
lemma preserves_divergence_converge_insert :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
and "preserves_divergence M1 M2 X"
and "u ∈ X"
shows "preserves_divergence M1 M2 (Set.insert v X)"
proof -
have "⋀ w . w ∈ L M1 ∩ X ⟹ ¬converge M1 v w ⟹ ¬converge M2 v w"
proof -
fix w
assume "w ∈ L M1 ∩ X" and "¬converge M1 v w"
then have "¬converge M1 u w"
using assms(5)
using converge.simps by blast
then have "¬converge M2 u w"
using assms(5-8)
by (meson IntI ‹w ∈ L M1 ∩ X› converge.elims(2) preserves_divergence.simps)
then show "¬converge M2 v w"
using assms(6) converge.simps by blast
qed
then show ?thesis
using assms(7)
unfolding preserves_divergence.simps
by (metis (no_types, lifting) Int_insert_right_if1 assms(1) assms(2) assms(3) assms(4) assms(5) converge.elims(2) convergence_minimal insert_iff)
qed
lemma preserves_divergence_converge_replace :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
and "preserves_divergence M1 M2 (Set.insert u X)"
shows "preserves_divergence M1 M2 (Set.insert v X)"
proof -
have "u ∈ L M1" and "v ∈ L M1"
using assms(5) by auto
then have "after_initial M1 u = after_initial M1 v"
using assms(1) assms(3) assms(5) convergence_minimal by blast
have "⋀ w . w ∈ L M1 ∩ X ⟹ ¬converge M1 v w ⟹ ¬converge M2 v w"
proof -
fix w
assume "w ∈ L M1 ∩ X" and "¬converge M1 v w"
then have "¬converge M1 u w"
using assms(5)
using converge.simps by blast
then have "¬converge M2 u w"
using assms(5-7)
by (meson IntD1 IntD2 IntI ‹w ∈ L M1 ∩ X› converge.elims(2) insertCI preserves_divergence.elims(1))
then show "¬converge M2 v w"
using assms(6) converge.simps by blast
qed
have "⋀ α β . α ∈ L M1 ⟹ α ∈ insert v X ⟹ β ∈ L M1 ⟹ β ∈ insert v X ⟹ ¬ converge M1 α β ⟹ ¬ converge M2 α β"
proof -
fix α β assume "α ∈ L M1" "α ∈ insert v X" "β ∈ L M1" "β ∈ insert v X" "¬ converge M1 α β"
then consider "α = v ∧ β = v" |
"α = v ∧ β ∈ X" |
"α ∈ X ∧ β = v" |
"α ∈ X ∧ β ∈ X"
by blast
then show "¬ converge M2 α β"
proof cases
case 1
then show ?thesis
using ‹α ∈ L M1› ‹β ∈ L M1› ‹¬ converge M1 α β› by auto
next
case 2
then show ?thesis
by (metis IntI ‹⋀w. ⟦w ∈ L M1 ∩ X; ¬ converge M1 v w⟧ ⟹ ¬ converge M2 v w› ‹β ∈ L M1› ‹¬ converge M1 α β›)
next
case 3
then show ?thesis
by (metis IntI ‹⋀w. ⟦w ∈ L M1 ∩ X; ¬ converge M1 v w⟧ ⟹ ¬ converge M2 v w› ‹α ∈ L M1› ‹¬ converge M1 α β› converge.simps)
next
case 4
then show ?thesis
using assms(7) unfolding preserves_divergence.simps
using ‹α ∈ L M1› ‹β ∈ L M1› ‹¬ converge M1 α β› by blast
qed
qed
then show ?thesis
unfolding preserves_divergence.simps by blast
qed
lemma preserves_divergence_converge_replace_iff :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
shows "preserves_divergence M1 M2 (Set.insert u X) = preserves_divergence M1 M2 (Set.insert v X)"
proof -
have *: "converge M1 v u" using assms(5) by auto
have **: "converge M2 v u" using assms(6) by auto
show ?thesis
using preserves_divergence_converge_replace[OF assms]
preserves_divergence_converge_replace[OF assms(1-4) * **]
by blast
qed
lemma preserves_divergence_subset :
assumes "preserves_divergence M1 M2 B"
and "A ⊆ B"
shows "preserves_divergence M1 M2 A"
using assms unfolding preserves_divergence.simps by blast
lemma preserves_divergence_insertI :
assumes "preserves_divergence M1 M2 X"
and "⋀ α . α ∈ L M1 ∩ X ⟹ β ∈ L M1 ⟹ ¬converge M1 α β ⟹ ¬converge M2 α β"
shows "preserves_divergence M1 M2 (Set.insert β X)"
using assms unfolding preserves_divergence.simps
by (metis Int_insert_right converge.elims(2) converge.elims(3) insertE)
lemma preserves_divergence_insertE :
assumes "preserves_divergence M1 M2 (Set.insert β X)"
shows "preserves_divergence M1 M2 X"
and "⋀ α . α ∈ L M1 ∩ X ⟹ β ∈ L M1 ⟹ ¬converge M1 α β ⟹ ¬converge M2 α β"
using assms unfolding preserves_divergence.simps
by blast+
lemma distinguishes_diverge_prefix :
assumes "observable M"
and "distinguishes M (after_initial M u) (after_initial M v) w"
and "u ∈ L M"
and "v ∈ L M"
and "w' ∈ set (prefixes w)"
and "w' ∈ LS M (after_initial M u)"
and "w' ∈ LS M (after_initial M v)"
shows "¬converge M (u@w') (v@w')"
proof
assume "converge M (u @ w') (v @ w')"
obtain w'' where "w = w'@w''"
using assms(5)
using prefixes_set_ob by auto
have "u@w' ∈ L M"
using assms(3,6) after_language_iff[OF assms(1)]
by blast
then have *:"(w ∈ LS M (after_initial M u)) = (w'' ∈ LS M (after_initial M (u@w')))"
using after_language_append_iff[OF assms(1)]
unfolding ‹w = w'@w''›
by blast
have "v@w' ∈ L M"
using assms(4,7) after_language_iff[OF assms(1)]
by blast
then have **:"(w ∈ LS M (after_initial M v)) = (w'' ∈ LS M (after_initial M (v@w')))"
using after_language_append_iff[OF assms(1)]
unfolding ‹w = w'@w''›
by blast
have "(w ∈ LS M (after_initial M u)) = (w ∈ LS M (after_initial M v))"
unfolding * **
using ‹converge M (u @ w') (v @ w')›
by (metis converge.elims(2))
then show False
using ‹distinguishes M (after_initial M u) (after_initial M v) w›
unfolding distinguishes_def
by blast
qed
lemma converge_distinguishable_helper :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
and "distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v"
and "L M1 ∩ {α@v,β@v} = L M2 ∩ {α@v,β@v}"
shows "(after_initial M1 π) ≠ (after_initial M1 τ)"
proof -
have "LS M1 (after_initial M1 π) = LS M1 (after_initial M1 α)"
by (meson assms(5) converge.elims(2))
have "LS M1 (after_initial M1 τ) = LS M1 (after_initial M1 β)"
by (meson assms(7) converge.elims(2))
have "LS M2 (after_initial M2 π) = LS M2 (after_initial M2 α)"
by (meson assms(6) converge.elims(2))
have "LS M2 (after_initial M2 τ) = LS M2 (after_initial M2 β)"
by (meson assms(8) converge.elims(2))
have "v ∈ LS M2 (after_initial M2 π) ⟷ v ∉ LS M2 (after_initial M2 τ)"
using assms(9) unfolding distinguishes_def by blast
then have "v ∈ LS M2 (after_initial M2 α) ⟷ v ∉ LS M2 (after_initial M2 β)"
using ‹LS M2 (after_initial M2 π) = LS M2 (after_initial M2 α)› ‹LS M2 (after_initial M2 τ) = LS M2 (after_initial M2 β)› by blast
then have "α@v ∈ L M2 ⟷ β@v ∉ L M2"
by (meson after_language_iff assms(2) assms(6) assms(8) converge.elims(2))
then have "α@v ∈ L M1 ⟷ β@v ∉ L M1"
using assms(10)
by (metis (no_types, lifting) Int_insert_right inf_sup_ord(1) insert_subset)
then have "v ∈ LS M1 (after_initial M1 α) ⟷ v ∉ LS M1 (after_initial M1 β)"
by (meson after_language_iff assms(1) assms(5) assms(7) converge.elims(2))
then have "v ∈ LS M1 (after_initial M1 π) ⟷ v ∉ LS M1 (after_initial M1 τ)"
using ‹LS M1 (after_initial M1 π) = LS M1 (after_initial M1 α)› ‹LS M1 (after_initial M1 τ) = LS M1 (after_initial M1 β)› by blast
then show ?thesis
by metis
qed
lemma converge_append_language_iff :
assumes "observable M"
and "converge M α β"
shows "(α@γ ∈ L M) = (β@γ ∈ L M)"
by (metis (no_types) assms(1) assms(2) converge.simps converge_extend)
lemma converge_append_iff :
assumes "observable M"
and "converge M α β"
shows "converge M γ (α@ω) = converge M γ (β@ω)"
proof (cases "(α@ω) ∈ L M")
case True
then show ?thesis
using converge_append_language_iff[OF assms] language_prefix[of β ω M "initial M"]
using converge_append[OF assms True]
by auto
next
case False
then show ?thesis
using converge_append_language_iff[OF assms]
using converge.simps by blast
qed
lemma after_distinguishes_language :
assumes "observable M1"
and "α ∈ L M1"
and "β ∈ L M1"
and "distinguishes M1 (after_initial M1 α) (after_initial M1 β) γ"
shows "(α@γ ∈ L M1) ≠ (β@γ ∈ L M1)"
unfolding after_language_iff[OF assms(1,2),symmetric]
after_language_iff[OF assms(1,3),symmetric]
using assms(4)
unfolding distinguishes_def
by blast
lemma distinguish_diverge :
assumes "observable M1"
and "observable M2"
and "distinguishes M1 (after_initial M1 u) (after_initial M1 v) γ"
and "u @ γ ∈ T"
and "v @ γ ∈ T"
and "u ∈ L M1"
and "v ∈ L M1"
and "L M1 ∩ T = L M2 ∩ T"
shows "¬ converge M2 u v"
proof
assume "converge M2 u v"
then have "u@γ ∈ L M2 ⟷ v@γ ∈ L M2"
using assms(2) converge_append_language_iff by blast
moreover have "u@γ ∈ L M1 ⟷ v@γ ∉ L M1"
using assms(1,3,6,7)
using after_distinguishes_language
by blast
ultimately show False
using assms(4,5,8) by blast
qed
lemma distinguish_converge_diverge :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "u' ∈ L M1"
and "v' ∈ L M1"
and "converge M1 u u'"
and "converge M1 v v'"
and "converge M2 u u'"
and "converge M2 v v'"
and "distinguishes M1 (after_initial M1 u) (after_initial M1 v) γ"
and "u' @ γ ∈ T"
and "v' @ γ ∈ T"
and "L M1 ∩ T = L M2 ∩ T"
shows "¬ converge M2 u v"
proof -
have *:"distinguishes M1 (after_initial M1 u') (after_initial M1 v') γ"
by (metis (mono_tags, opaque_lifting) assms(1) assms(10) assms(3) assms(6) assms(7) converge.simps convergence_minimal)
show ?thesis
using distinguish_diverge[OF assms(1-2) *]
by (metis (mono_tags, lifting) assms(9) assms(11) assms(12) assms(13) assms(4) assms(5) assms(8) converge.simps)
qed
lemma diverge_prefix :
assumes "observable M"
and "α@γ ∈ L M"
and "β@γ ∈ L M"
and "¬ converge M (α@γ) (β@γ)"
shows "¬ converge M α β"
by (meson assms converge_append language_prefix)
lemma converge_sym: "converge M u v = converge M v u"
by auto
lemma state_cover_transition_converges :
assumes "observable M"
and "is_state_cover_assignment M V"
and "t ∈ transitions M"
and "t_source t ∈ reachable_states M"
shows "converge M ((V (t_source t)) @ [(t_input t,t_output t)]) (V (t_target t))"
proof -
have "t_target t ∈ reachable_states M"
using assms(3,4) reachable_states_next
by metis
have "V (t_source t) ∈ L M" and "after_initial M (V (t_source t)) = (t_source t)"
using state_cover_assignment_after[OF assms(1,2,4)]
by simp+
have "((V (t_source t)) @ [(t_input t,t_output t)]) ∈ L M"
using after_language_iff[OF assms(1) ‹V (t_source t) ∈ L M›, of "[(t_input t,t_output t)]"]
assms(3)
unfolding LS_single_transition ‹after_initial M (V (t_source t)) = (t_source t)›
by force
have "FSM.after M (t_source t) [(t_input t, t_output t)] = t_target t"
using after_transition[OF assms(1)] assms(3)
by auto
then have "after_initial M ((V (t_source t)) @ [(t_input t,t_output t)]) = t_target t"
using ‹after_initial M (V (t_source t)) = (t_source t)›
using after_split[OF assms(1) ‹((V (t_source t)) @ [(t_input t,t_output t)]) ∈ L M›]
by force
then show ?thesis
using ‹((V (t_source t)) @ [(t_input t,t_output t)]) ∈ L M›
using state_cover_assignment_after[OF assms(1,2) ‹t_target t ∈ reachable_states M›]
by auto
qed
lemma equivalence_preserves_divergence :
assumes "observable M"
and "observable I"
and "L M = L I"
shows "preserves_divergence M I A"
proof -
have "⋀ α β . α ∈ L M ∩ A ⟹ β ∈ L M ∩ A ⟹ ¬ converge M α β ⟹ ¬ converge I α β"
proof -
fix α β assume "α ∈ L M ∩ A" and "β ∈ L M ∩ A" and "¬ converge M α β"
then have "after_initial M α ∈ states M" and "after_initial M β ∈ states M" and "LS M (after_initial M α) ≠ LS M (after_initial M β)"
using after_is_state[OF assms(1)] unfolding converge.simps
by auto
then obtain γ where "(γ ∈ LS M (after_initial M α)) ≠ (γ ∈ LS M (after_initial M β))"
by blast
then have "(α@γ ∈ L M) ≠ (β@γ ∈ L M)"
using after_language_iff[OF assms(1)] ‹α ∈ L M ∩ A› ‹β ∈ L M ∩ A› by blast
then have "(α@γ ∈ L I) ≠ (β@γ ∈ L I)"
using assms(3) by blast
then show "¬ converge I α β"
using assms(2) converge_append_language_iff by blast
qed
then show ?thesis
unfolding preserves_divergence.simps by blast
qed
subsection ‹Sufficient Conditions for Convergence›
text ‹The following lemma provides a condition for convergence that assumes the existence
of a single state cover covering all extensions of length up to (m - |M1|).
This is too restrictive for the SPYH method but could be used in the SPY method.
The proof idea has been developed by Wen-ling Huang and adapted by the author to
avoid requiring the SC to cover traces that contain a proper prefix already not
in the language of FSM M1.›
lemma sufficient_condition_for_convergence_in_SPY_method :
fixes M1 :: "('a,'b,'c) 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 "L M1 ∩ T = L M2 ∩ T"
and "π ∈ L M1 ∩ T"
and "τ ∈ L M1 ∩ T"
and "converge M1 π τ"
and "SC ⊆ T"
and "⋀ q . q ∈ reachable_states M1 ⟹ ∃ io ∈ L M1 ∩ SC . q ∈ io_targets M1 io (initial M1)"
and "preserves_divergence M1 M2 SC"
and "⋀ γ x y . length γ < m - size_r M1 ⟹
γ ∈ LS M1 (after_initial M1 π) ⟹
x ∈ inputs M1 ⟹
y ∈ outputs M1 ⟹
∃ α β . converge M1 α (π@γ) ∧
converge M2 α (π@γ) ∧
converge M1 β (τ@γ) ∧
converge M2 β (τ@γ) ∧
α ∈ SC ∧
α@[(x,y)] ∈ SC ∧
β ∈ SC ∧
β@[(x,y)] ∈ SC"
and "∃ α β . converge M1 α π ∧
converge M2 α π ∧
converge M1 β τ ∧
converge M2 β τ ∧
α ∈ SC ∧
β ∈ SC"
and "inputs M2 = inputs M1"
and "outputs M2 = outputs M1"
shows "converge M2 π τ"
proof -
obtain f where f1: "⋀ q . q ∈ reachable_states M1 ⟹ q ∈ io_targets M1 (f q) (initial M1)"
and f2: "⋀ q . q ∈ reachable_states M1 ⟹ f q ∈ L M1 ∩ SC"
using non_initialized_state_cover_assignment_from_non_initialized_state_cover[OF ‹⋀ q . q ∈ reachable_states M1 ⟹ ∃ io ∈ L M1 ∩ SC . q ∈ io_targets M1 io (initial M1)›]
by blast
define A where A: "A = (λ q . Set.filter (converge M1 (f q)) (L M1 ∩ SC))"
define Q where Q: "Q = (λ q . ⋃ α ∈ A q . io_targets M2 α (initial M2))"
have "⋀ q . q ∈ reachable_states M1 ⟹ Q q ≠ {}"
proof -
fix q assume "q ∈ reachable_states M1"
then have "f q ∈ A q"
using A
using f2 by auto
moreover have "f q ∈ L M2"
proof -
have "f q ∈ L M1 ∩ SC"
using ‹q ∈ reachable_states M1› f2 by blast
then show ?thesis
using ‹SC ⊆ T› ‹L M1 ∩ T = L M2 ∩ T› by blast
qed
ultimately show "Q q ≠ {}"
unfolding Q
by auto
qed
have "states M2 = (⋃ q ∈ reachable_states M1 . Q q) ∪ (states M2 - (⋃ q ∈ reachable_states M1 . Q q))"
proof -
have "(⋃ q ∈ reachable_states M1 . Q q) ⊆ reachable_states M2"
proof
fix q assume "q ∈ (⋃ q ∈ reachable_states M1 . Q q)"
then obtain α where "q ∈ io_targets M2 α (initial M2)"
unfolding Q by blast
then show "q ∈ reachable_states M2"
unfolding io_targets.simps reachable_states_def by blast
qed
then show ?thesis
by (metis Diff_partition reachable_state_is_state subset_iff)
qed
have "⋀ q1 q2 . q1 ∈ reachable_states M1 ⟹ q2 ∈ reachable_states M1 ⟹ q1 ≠ q2 ⟹ Q q1 ∩ Q q2 = {}"
proof -
fix q1 q2
assume "q1 ∈ reachable_states M1" and "q2 ∈ reachable_states M1" and "q1 ≠ q2"
have "⋀ α β . α ∈ A q1 ⟹ β ∈ A q2 ⟹ io_targets M2 α (initial M2) ∩ io_targets M2 β (initial M2) = {}"
proof -
fix α β assume "α ∈ A q1" and "β ∈ A q2"
then have "converge M1 (f q1) α" and "converge M1 (f q2) β"
unfolding A
by (meson member_filter)+
moreover have "¬ converge M1 (f q1) (f q2)"
using non_initialized_state_cover_assignment_diverges[OF assms(1,3) f1 f2 ‹q1 ∈ reachable_states M1› ‹q2 ∈ reachable_states M1› ‹q1 ≠ q2›] .
ultimately have "¬ converge M1 α β"
unfolding converge.simps by blast
moreover have "α∈L M1 ∩ SC"
using ‹α ∈ A q1› unfolding A
by (meson member_filter)
moreover have "β∈L M1 ∩ SC"
using ‹β ∈ A q2› unfolding A
by (meson member_filter)
ultimately have "¬ converge M2 α β"
using ‹preserves_divergence M1 M2 SC›
unfolding preserves_divergence.simps
by blast
have "α ∈ L M2" and "β ∈ L M2"
using ‹α∈L M1 ∩ SC› ‹β∈L M1 ∩ SC› ‹SC ⊆ T› ‹L M1 ∩ T = L M2 ∩ T› by blast+
have "io_targets M2 α (initial M2) = {after_initial M2 α}"
using observable_io_targets[OF ‹observable M2› ‹α ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹α ∈ L M2›]
by (metis the_elem_eq)
moreover have "io_targets M2 β (initial M2) = {after_initial M2 β}"
using observable_io_targets[OF ‹observable M2› ‹β ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹β ∈ L M2›]
by (metis the_elem_eq)
ultimately show "io_targets M2 α (initial M2) ∩ io_targets M2 β (initial M2) = {}"
using ‹¬ converge M2 α β› unfolding convergence_minimal[OF assms(4,2) ‹α ∈ L M2› ‹β ∈ L M2›]
by (metis Int_insert_right_if0 inf_bot_right singletonD)
qed
then show "Q q1 ∩ Q q2 = {}"
unfolding Q by blast
qed
then have "⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')"
unfolding Uniq_def
by blast
define partition where partition: "partition = (λ q . if ∃ q' ∈ reachable_states M1 . q ∈ Q q'
then Q (THE q' . q' ∈ reachable_states M1 ∧ q ∈ Q q')
else (states M2 - (⋃ q ∈ reachable_states M1 . Q q)))"
have is_eq: "equivalence_relation_on_states M2 partition"
proof-
let ?r = "{(q1,q2) | q1 q2 . q1 ∈ states M2 ∧ q2 ∈ partition q1}"
have "⋀ q .partition q ⊆ states M2"
proof -
fix q show "partition q ⊆ states M2"
proof (cases "∃ q' ∈ reachable_states M1 . q ∈ Q q'")
case True
then have "partition q = Q (THE q' . q' ∈ reachable_states M1 ∧ q ∈ Q q')"
unfolding partition by simp
then show ?thesis
using True ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›
by (metis (no_types, lifting) Q SUP_least io_targets_states)
next
case False
then show ?thesis unfolding partition
by auto
qed
qed
have "⋀ q . q ∈ states M2 ⟹ q ∈ partition q"
proof -
fix q assume "q ∈ states M2"
show "q ∈ partition q"
proof (cases "∃ q' ∈ reachable_states M1 . q ∈ Q q'")
case True
then have "partition q = Q (THE q' . q' ∈ reachable_states M1 ∧ q ∈ Q q')"
unfolding partition by simp
then show ?thesis
using True ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›
using the1_equality' by fastforce
next
case False
then show ?thesis unfolding partition
using ‹q ∈ states M2›
by simp
qed
qed
have "⋀ q q' . q ∈ states M2 ⟹ q' ∈ partition q ⟹ q ∈ partition q'"
proof -
fix q q' assume "q ∈ states M2" and "q' ∈ partition q"
show "q ∈ partition q'"
proof (cases "∃ q' ∈ reachable_states M1 . q ∈ Q q'")
case True
then have "partition q = Q (THE q' . q' ∈ reachable_states M1 ∧ q ∈ Q q')"
unfolding partition by simp
then obtain q1 where "partition q = Q q1" and "q1 ∈ reachable_states M1" and "q ∈ Q q1"
using True ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›
using the1_equality' by fastforce
then have "q' ∈ Q q1"
using ‹q' ∈ partition q› by auto
then have "partition q' = Q q1"
using ‹q1 ∈ reachable_states M1›
using the1_equality'[OF ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›]
unfolding partition
by auto
then show ?thesis
using ‹q ∈ Q q1› ‹q' ∈ partition q› ‹partition q = Q q1› by blast
next
case False
then show ?thesis
using ‹q ∈ states M2› ‹q' ∈ partition q›
by (simp add: partition)
qed
qed
have "⋀ q q' q'' . q ∈ states M2 ⟹ q' ∈ partition q ⟹ q'' ∈ partition q' ⟹ q'' ∈ partition q"
proof -
fix q q' q''
assume "q ∈ states M2" and "q' ∈ partition q" and "q'' ∈ partition q'"
show "q'' ∈ partition q"
proof (cases "∃ q' ∈ reachable_states M1 . q ∈ Q q'")
case True
then have "partition q = Q (THE q' . q' ∈ reachable_states M1 ∧ q ∈ Q q')"
unfolding partition by simp
then obtain q1 where "partition q = Q q1" and "q1 ∈ reachable_states M1" and "q ∈ Q q1"
using True ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›
using the1_equality' by fastforce
then have "q' ∈ Q q1"
using ‹q' ∈ partition q› by auto
then have "partition q' = Q q1"
using ‹q1 ∈ reachable_states M1›
using the1_equality'[OF ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›]
unfolding partition
by auto
then have "q'' ∈ Q q1"
using ‹q'' ∈ partition q'› by auto
then have "partition q'' = Q q1"
using ‹q1 ∈ reachable_states M1›
using the1_equality'[OF ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›]
unfolding partition
by auto
then show ?thesis
unfolding ‹partition q = Q q1›
using ‹q'' ∈ Q q1› by blast
next
case False
then show ?thesis
using ‹q ∈ states M2› ‹q' ∈ partition q› ‹q'' ∈ partition q'›
by (simp add: partition)
qed
qed
have "refl_on (states M2) ?r" unfolding refl_on_def
proof
show "{(q1, q2) |q1 q2. q1 ∈ FSM.states M2 ∧ q2 ∈ partition q1} ⊆ FSM.states M2 × FSM.states M2"
using ‹⋀ q .partition q ⊆ states M2› by blast
show "∀x∈FSM.states M2. (x, x) ∈ {(q1, q2) |q1 q2. q1 ∈ FSM.states M2 ∧ q2 ∈ partition q1}"
proof
fix q assume "q ∈ states M2"
then show "(q,q) ∈ {(q1, q2) |q1 q2. q1 ∈ FSM.states M2 ∧ q2 ∈ partition q1}"
using ‹⋀ q . q ∈ states M2 ⟹ q ∈ partition q›
by blast
qed
qed
moreover have "sym ?r"
unfolding sym_def
using ‹⋀ q q' . q ∈ states M2 ⟹ q' ∈ partition q ⟹ q ∈ partition q'› ‹⋀ q .partition q ⊆ states M2›
by blast
moreover have "trans ?r"
unfolding trans_def
using ‹⋀ q q' q'' . q ∈ states M2 ⟹ q' ∈ partition q ⟹ q'' ∈ partition q' ⟹ q'' ∈ partition q›
by blast
ultimately show ?thesis
unfolding equivalence_relation_on_states_def equiv_def
using ‹⋀ q .partition q ⊆ states M2› by blast
qed
define n0 where n0: "n0 = card (partition ` states M2)"
have "n0 ≤ Suc (size_r M1)" and "n0 ≥ size_r M1"
proof -
have "partition ` states M2 ⊆ insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)"
proof
fix X assume "X ∈ partition ` states M2"
then obtain q where "q ∈ states M2" and "X = partition q"
by blast
show "X ∈ insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)"
proof (cases "∃q'∈reachable_states M1. q ∈ Q q'")
case True
then show ?thesis
unfolding ‹X = partition q› partition
using the1_equality'[OF ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›]
by auto
next
case False
then show ?thesis
unfolding ‹X = partition q› partition
by auto
qed
qed
moreover have "card (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)) ≤ Suc (size_r M1)"
and "finite (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1))"
and "card (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)) ≥ size_r M1"
proof -
have "finite (Q ` reachable_states M1)"
using fsm_states_finite[of M1]
by (metis finite_imageI fsm_states_finite restrict_to_reachable_states_simps(2))
moreover have "card (Q ` reachable_states M1) = size_r M1"
proof -
have "card (Q ` reachable_states M1) ≤ size_r M1"
by (metis card_image_le fsm_states_finite restrict_to_reachable_states_simps(2))
moreover have "card (Q ` reachable_states M1) ≥ size_r M1"
using ‹finite (Q ` reachable_states M1)›
by (metis (full_types) ‹⋀q. q ∈ reachable_states M1 ⟹ Q q ≠ {}› ‹⋀q2 q1. ⟦q1 ∈ reachable_states M1; q2 ∈ reachable_states M1; q1 ≠ q2⟧ ⟹ Q q1 ∩ Q q2 = {}› calculation card_eq_0_iff card_union_of_distinct le_0_eq)
ultimately show ?thesis
by simp
qed
ultimately show "card (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)) ≤ Suc (size_r M1)"
and "card (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1)) ≥ size_r M1"
by (simp add: card_insert_if)+
show "finite (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1))"
using ‹finite (Q ` reachable_states M1)›
by blast
qed
ultimately show "n0 ≤ Suc (size_r M1)" unfolding n0
by (meson card_mono le_trans)
have "(Q ` reachable_states M1) ⊆ partition ` states M2"
proof
fix x assume "x ∈ (Q ` reachable_states M1)"
then obtain q' where "q' ∈ reachable_states M1" and "x = Q q'"
by blast
then obtain q where "q ∈ Q q'"
using ‹⋀ q . q ∈ reachable_states M1 ⟹ Q q ≠ {}› by blast
then obtain α where "α ∈ A q'" and "q ∈ io_targets M2 α (initial M2)"
unfolding Q by blast
then have "q ∈ states M2"
by (meson io_targets_states subset_iff)
have "∃q'∈reachable_states M1. q ∈ Q q'"
using ‹q' ∈ reachable_states M1› ‹q ∈ Q q'› by blast
then have "partition q = Q q'"
unfolding partition
using the1_equality'[OF ‹⋀ q . Uniq (λq' . q' ∈ reachable_states M1 ∧ q ∈ Q q')›, of q' q] ‹q ∈ Q q'› ‹q' ∈ reachable_states M1›
by auto
then show "x ∈ partition ` states M2"
using ‹q ∈ states M2› ‹x = Q q'›
by blast
qed
then show "n0 ≥ size_r M1"
unfolding n0
using ‹finite (insert (states M2 - (⋃ q ∈ reachable_states M1 . Q q)) (Q ` reachable_states M1))›
by (metis (full_types) ‹⋀q. q ∈ reachable_states M1 ⟹ Q q ≠ {}› ‹⋀q2 q1. ⟦q1 ∈ reachable_states M1; q2 ∈ reachable_states M1; q1 ≠ q2⟧ ⟹ Q q1 ∩ Q q2 = {}› ‹partition ` FSM.states M2 ⊆ insert (FSM.states M2 - ⋃ (Q ` reachable_states M1)) (Q ` reachable_states M1)› card_mono card_union_of_distinct finite_subset fsm_states_finite restrict_to_reachable_states_simps(2))
qed
moreover have "after_initial M2 τ ∈ ofsm_table M2 partition (m - size_r M1) (after_initial M2 π)"
proof -
define q1 where q1: "q1 = (after_initial M2 π)"
define q2 where q2: "q2 = (after_initial M2 τ)"
have "π ∈ L M2" and "τ ∈ L M2"
using assms(7,8,9) by blast+
have "q1 ∈ states M2"
using ‹π ∈ L M2› after_is_state[OF ‹observable M2›] unfolding q1 by blast
have "q2 ∈ states M2"
using ‹τ ∈ L M2› after_is_state[OF ‹observable M2›] unfolding q2 by blast
moreover have "⋀ γ . length γ ≤ m - size_r M1 ⟹ (γ ∈ LS M2 q1) = (γ ∈ LS M2 q2) ∧ (γ ∈ LS M2 q1 ⟶ after M2 q2 γ ∈ partition (after M2 q1 γ))"
proof -
fix γ :: "('b×'c) list"
assume "length γ ≤ m - size_r M1"
then show "((γ ∈ LS M2 q1) = (γ ∈ LS M2 q2)) ∧ (γ ∈ LS M2 q1 ⟶ after M2 q2 γ ∈ partition (after M2 q1 γ))"
proof (induction γ rule: rev_induct)
case Nil
show ?case
proof
have "([] ∈ LS M2 q1)" and "([] ∈ LS M2 q2)"
using ‹q1 ∈ states M2› ‹q2 ∈ states M2›
by auto
then have "after M2 q1 [] = q1" and "after M2 q2 [] = q2"
unfolding Nil
by auto
obtain α β where "converge M1 α π"
"converge M2 α π"
"converge M1 β τ"
"converge M2 β τ"
"α ∈ SC"
"β ∈ SC"
using assms(15) by blast
then have "α ∈ L M1" and "β ∈ L M1"
by auto
have "α ∈ L M2"
using ‹α ∈ L M1› ‹α ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "β ∈ L M2"
using ‹β ∈ L M1› ‹β ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "([] ∈ LS M2 q1) = ([] ∈ LS M2 (after_initial M2 α))"
using ‹converge M2 α π› unfolding q1 converge.simps by simp
also have "… = ([] ∈ LS M1 (after_initial M1 α))"
using ‹α ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
unfolding after_language_iff[OF ‹observable M1› ‹α ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹α ∈ L M2›]
unfolding Nil
by auto
also have "… = ([] ∈ LS M1 (after_initial M1 β))"
using ‹converge M1 π τ› ‹converge M1 α π› ‹converge M1 β τ›
unfolding converge.simps by blast
also have "… = ([] ∈ LS M2 (after_initial M2 β))"
using ‹β ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
unfolding after_language_iff[OF ‹observable M1› ‹β ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹β ∈ L M2›]
unfolding Nil
by auto
also have "… = ([] ∈ LS M2 q2)"
using ‹converge M2 β τ› unfolding q2 converge.simps by simp
finally show "([] ∈ LS M2 q1) = ([] ∈ LS M2 q2)" .
show "([] ∈ LS M2 q1 ⟶ after M2 q2 [] ∈ partition (after M2 q1 []))"
proof
assume "[] ∈ LS M2 q1"
then have "[] ∈ LS M1 (after_initial M1 α)"
and "[] ∈ LS M1 (after_initial M1 β)"
unfolding ‹([] ∈ LS M2 q1) = ([] ∈ LS M2 (after_initial M2 α))›
‹([] ∈ LS M2 (after M2 (FSM.initial M2) α)) = ([] ∈ LS M1 (after M1 (FSM.initial M1) α))›
‹([] ∈ LS M1 (after M1 (FSM.initial M1) α)) = ([] ∈ LS M1 (after M1 (FSM.initial M1) β))›
by simp+
have "α@[] ∈ L M1"
using ‹[] ∈ LS M1 (after_initial M1 α)› unfolding after_language_iff[OF ‹observable M1› ‹α ∈ L M1›] .
moreover have "β@[] ∈ L M1"
using ‹[] ∈ LS M1 (after_initial M1 β)› unfolding after_language_iff[OF ‹observable M1› ‹β ∈ L M1›] .
moreover have "converge M1 α β"
using ‹converge M1 π τ› ‹converge M1 α π› ‹converge M1 β τ›
unfolding converge.simps by blast
ultimately have "converge M1 (α@[]) (β@[])"
using converge_append[OF ‹observable M1›] language_prefix[of β "[]" M1 "initial M1"] by blast
have "(α @ []) ∈ L M2" and "(β @ []) ∈ L M2"
using ‹α@[] ∈ L M1› ‹α ∈ SC› ‹β@[] ∈ L M1› ‹β ∈ SC ›‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by auto
have "after_initial M1 (α@[]) ∈ reachable_states M1"
using observable_after_path[OF ‹observable M1› ]
unfolding reachable_states_def
proof -
have "∃ps. after M1 (FSM.initial M1) α = target (FSM.initial M1) ps ∧ path M1 (FSM.initial M1) ps"
by (metis (no_types) ‹⋀thesis q io. ⟦io ∈ LS M1 q; ⋀p. ⟦path M1 q p; p_io p = io; target q p = after M1 q io⟧ ⟹ thesis⟧ ⟹ thesis› ‹α ∈ L M1›)
then show "after M1 (FSM.initial M1) (α @ []) ∈ {target (FSM.initial M1) ps |ps. path M1 (FSM.initial M1) ps}"
by auto
qed
have "(α@[]) ∈ A (after_initial M1 (α@[]))"
unfolding A
using convergence_minimal[OF assms(3,1) _ ‹α@[] ∈ L M1›, of "f (after_initial M1 (α@[]))"]
using f2[OF ‹after_initial M1 (α@[]) ∈ reachable_states M1›]
using ‹α ∈ SC›
unfolding Nil
by (metis (no_types, lifting) Int_iff ‹α ∈ L M1› ‹after M1 (FSM.initial M1) (α @ []) ∈ reachable_states M1› append_Nil2 assms(1) f1 member_filter observable_after_path observable_path_io_target singletonD)
then have "after M2 (FSM.initial M2) (α @ []) ∈ Q (after_initial M1 (α@[]))"
unfolding Q
using observable_io_targets[OF ‹observable M2› ‹(α @ []) ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹(α @ []) ∈ L M2›]
by (metis UN_iff insertCI the_elem_eq)
then have "∃q'∈reachable_states M1. after M2 (FSM.initial M2) (α @ []) ∈ Q q'"
using ‹after_initial M1 (α@[]) ∈ reachable_states M1› by blast
moreover have "(THE q'. q' ∈ reachable_states M1 ∧ after M2 (FSM.initial M2) (α @ []) ∈ Q q') = (after_initial M1 (α@[]))"
using ‹after_initial M1 (α@[]) ∈ reachable_states M1›
using ‹after M2 (FSM.initial M2) (α @ []) ∈ Q (after_initial M1 (α@[]))›
by (simp add: ‹⋀q. ∃⇩≤⇩1 q'. q' ∈ reachable_states M1 ∧ q ∈ Q q'› the1_equality')
moreover have "after M2 (FSM.initial M2) (β @ []) ∈ Q (after_initial M1 (α@[]))"
proof -
have "(β@[]) ∈ A (after_initial M1 (α@[]))"
using A ‹α @ [] ∈ A (after M1 (FSM.initial M1) (α @ []))› ‹β @ [] ∈ L M1› ‹β ∈ SC› ‹converge M1 (α @ []) (β @ [])› unfolding Nil by auto
then show ?thesis
unfolding Q
using observable_io_targets[OF ‹observable M2› ‹(β @ []) ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹(β @ []) ∈ L M2›]
by (metis UN_iff insertCI the_elem_eq)
qed
ultimately have "after_initial M2 (β@[]) ∈ partition (after_initial M2 (α@[]))"
unfolding partition
by presburger
moreover have "after_initial M2 (α@[]) = after_initial M2 (π@[])"
using converge_append[OF assms(2) ‹converge M2 α π› ‹(α @ []) ∈ L M2› ‹π ∈ L M2›]
unfolding convergence_minimal[OF assms(4,2) ‹(α @ []) ∈ L M2› converge_extend[OF assms(2) ‹converge M2 α π› ‹(α @ []) ∈ L M2› ‹π ∈ L M2›]]
.
moreover have "after_initial M2 (β@[]) = after_initial M2 (τ@[])"
using converge_append[OF assms(2) ‹converge M2 β τ› ‹(β @ []) ∈ L M2› ‹τ ∈ L M2›]
unfolding convergence_minimal[OF assms(4,2) ‹(β @ []) ∈ L M2› converge_extend[OF assms(2) ‹converge M2 β τ› ‹(β @ []) ∈ L M2› ‹τ ∈ L M2›]]
.
ultimately show "after M2 q2 [] ∈ partition (after M2 q1 [])"
unfolding q1 q2
unfolding after_split[OF assms(2) converge_extend[OF assms(2) ‹converge M2 α π› ‹(α @ []) ∈ L M2› ‹π ∈ L M2›]]
unfolding after_split[OF assms(2) converge_extend[OF assms(2) ‹converge M2 β τ› ‹(β @ []) ∈ L M2› ‹τ ∈ L M2›]]
by simp
qed
qed
next
case (snoc xy γ)
obtain x y where "xy = (x,y)"
by fastforce
show ?case proof (cases "∀ x' y' . (x',y') ∈ set (γ@[(x,y)]) ⟶ x' ∈ inputs M1 ∧ y' ∈ outputs M1")
case False
have "γ@[(x,y)] ∉ LS M2 q1" and "γ@[(x,y)] ∉ LS M2 q2"
using language_io[of "γ@[(x,y)]" M2 _ ] False
unfolding ‹inputs M2 = inputs M1› ‹outputs M2 = outputs M1›
by blast+
then show ?thesis
unfolding ‹xy = (x,y)›
by blast
next
case True
define s1 where s1: "s1 = (after_initial M1 π)"
define s2 where s2: "s2 = (after_initial M1 τ)"
have "s1 ∈ states M1"
using ‹π ∈ L M1 ∩ T› after_is_state[OF ‹observable M1›] unfolding s1 by blast
have "s2 ∈ states M1"
using ‹τ ∈ L M1 ∩ T› after_is_state[OF ‹observable M1›] unfolding s2 by blast
show ?thesis proof (cases "γ ∈ LS M1 s1")
case False
obtain io' x' y' io'' where "γ = io' @ [(x', y')] @ io''"
and "io' ∈ LS M1 s1"
and "io' @ [(x', y')] ∉ LS M1 s1"
using language_maximal_contained_prefix_ob[OF False ‹s1 ∈ states M1› ‹observable M1›]
by blast
have *: "length io' < m - size_r M1"
using ‹length (γ @ [xy]) ≤ m - size_r M1›
unfolding ‹γ = io' @ [(x', y')] @ io''›
by auto
have **: "io' ∈ LS M1 (after M1 (FSM.initial M1) π)"
using ‹io' ∈ LS M1 s1› unfolding s1 .
have "x' ∈ inputs M1" and "y' ∈ outputs M1"
using True
unfolding ‹γ = io' @ [(x', y')] @ io''›
by auto
obtain α β where "converge M1 α (π @ io')"
"converge M2 α (π @ io')"
"converge M1 β (τ @ io')"
"converge M2 β (τ @ io')"
"α ∈ SC"
"α @ [(x', y')] ∈ SC"
"β ∈ SC"
"β @ [(x', y')] ∈ SC"
using assms(14)[OF * ** ‹x' ∈ inputs M1› ‹y' ∈ outputs M1›]
by blast
then have "α ∈ L M1" and "β ∈ L M1"
by auto
have "π@io' ∈ L M1"
using ‹io' ∈ LS M1 s1› ‹π ∈ L M1 ∩ T›
using after_language_iff[OF ‹observable M1›, of π "initial M1" io']
unfolding s1
by blast
have "converge M1 (π @ io') (τ @ io')"
using converge_append[OF ‹observable M1› ‹converge M1 π τ› ‹π@io' ∈ L M1› ]
using ‹τ ∈ L M1 ∩ T›
by blast
have "(π @ io') @ [(x', y')] ∉ L M1"
using ‹io' @ [(x', y')] ∉ LS M1 s1›
using ‹π ∈ L M1 ∩ T›
using after_language_iff[OF ‹observable M1›, of π "initial M1" "io'@[(x',y')]"]
unfolding s1
by auto
then have "[(x',y')] ∉ LS M1 (after_initial M1 α)"
using after_language_iff[OF ‹observable M1› ‹π@io' ∈ L M1›, of "[(x',y')]"]
using ‹converge M1 α (π @ io')›
unfolding converge.simps
by blast
then have "[(x',y')] ∉ LS M1 (after_initial M1 β)"
using ‹converge M1 (π @ io') (τ @ io')› ‹converge M1 α (π @ io')› ‹converge M1 β (τ @ io')›
unfolding converge.simps
by blast
have "α ∈ L M2"
using ‹α ∈ L M1› ‹α ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "β ∈ L M2"
using ‹β ∈ L M1› ‹β ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "[(x',y')] ∉ LS M2 (after_initial M2 α)"
using ‹α @ [(x', y')] ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
‹[(x',y')] ∉ LS M1 (after_initial M1 α)›
unfolding after_language_iff[OF ‹observable M1› ‹α ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹α ∈ L M2›]
by blast
then have "io'@[(x',y')] ∉ LS M2 q1"
using ‹converge M2 α (π @ io')›
unfolding q1 converge.simps
using after_language_append_iff assms(2) by blast
then have "γ@[xy] ∉ LS M2 q1"
unfolding ‹γ = io' @ [(x', y')] @ io''›
using language_prefix
by (metis append_assoc)
have "[(x',y')] ∉ LS M2 (after_initial M2 β)"
using ‹β @ [(x', y')] ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
‹[(x',y')] ∉ LS M1 (after_initial M1 β)›
unfolding after_language_iff[OF ‹observable M1› ‹β ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹β ∈ L M2›]
by blast
then have "io'@[(x',y')] ∉ LS M2 q2"
using ‹converge M2 β (τ @ io')›
unfolding q2 converge.simps
using after_language_append_iff assms(2) by blast
then have "γ@[xy] ∉ LS M2 q2"
unfolding ‹γ = io' @ [(x', y')] @ io''›
using language_prefix
by (metis append_assoc)
then show ?thesis
using ‹γ@[xy] ∉ LS M2 q1›
by blast
next
case True
have *: "length γ < m - size_r M1"
using ‹length (γ @ [xy]) ≤ m - size_r M1›
by auto
have **: "γ ∈ LS M1 (after M1 (FSM.initial M1) π)"
using True unfolding s1 .
have "x ∈ inputs M1" and "y ∈ outputs M1"
using ‹∀ x' y' . (x',y') ∈ set (γ@[(x,y)]) ⟶ x' ∈ inputs M1 ∧ y' ∈ outputs M1›
by auto
obtain α β where "converge M1 α (π @ γ)"
"converge M2 α (π @ γ)"
"converge M1 β (τ @ γ)"
"converge M2 β (τ @ γ)"
"α ∈ SC"
"α @ [xy] ∈ SC"
"β ∈ SC"
"β @ [xy] ∈ SC"
using assms(14)[OF * ** ‹x ∈ inputs M1› ‹y ∈ outputs M1›]
unfolding ‹xy = (x,y)›
by blast
then have "α ∈ L M1" and "β ∈ L M1"
by auto
have "α ∈ L M2"
using ‹α ∈ L M1› ‹α ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "β ∈ L M2"
using ‹β ∈ L M1› ‹β ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast
have "(π @ γ) ∈ L M2"
using ‹converge M2 α (π @ γ)› by auto
have "(τ @ γ) ∈ L M2"
using ‹converge M2 β (τ @ γ)› by auto
have "converge M1 (π @ γ) (τ @ γ)"
using converge_append[OF ‹observable M1› ‹converge M1 π τ›, of γ]
using ‹converge M1 α (π @ γ)› ‹τ ∈ L M1 ∩ T›
by auto
have "(γ@[xy] ∈ LS M2 q1) = ([xy] ∈ LS M2 (after_initial M2 (π@γ)))"
unfolding q1
using after_language_append_iff[OF ‹observable M2› ‹(π @ γ) ∈ L M2›] by auto
also have "… = ([xy] ∈ LS M2 (after_initial M2 α))"
using ‹converge M2 α (π @ γ)› unfolding q1 converge.simps
by blast
also have "… = ([xy] ∈ LS M1 (after_initial M1 α))"
using ‹α@[xy] ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
unfolding after_language_iff[OF ‹observable M1› ‹α ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹α ∈ L M2›]
by blast
also have "… = ([xy] ∈ LS M1 (after_initial M1 β))"
using ‹converge M1 (π @ γ) (τ @ γ)› ‹converge M1 α (π @ γ)› ‹converge M1 β (τ @ γ)›
unfolding converge.simps
by blast
also have "… = ([xy] ∈ LS M2 (after_initial M2 β))"
using ‹β@[xy] ∈ SC› ‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T›
unfolding after_language_iff[OF ‹observable M1› ‹β ∈ L M1›]
unfolding after_language_iff[OF ‹observable M2› ‹β ∈ L M2›]
by blast
also have "… = ([xy] ∈ LS M2 (after_initial M2 (τ@γ)))"
using ‹converge M2 β (τ @ γ)› unfolding q1 converge.simps
by blast
also have "… = (γ@[xy] ∈ LS M2 q2)"
unfolding q2
using after_language_append_iff[OF ‹observable M2› ‹(τ @ γ) ∈ L M2›] by auto
finally have p1: "(γ@[xy] ∈ LS M2 q1) = (γ@[xy] ∈ LS M2 q2)"
.
moreover have "(γ@[xy] ∈ LS M2 q1 ⟶ after M2 q2 (γ@[xy]) ∈ partition (after M2 q1 (γ@[xy])))"
proof
assume "γ@[xy] ∈ LS M2 q1"
then have "[xy] ∈ LS M1 (after_initial M1 α)"
and "[xy] ∈ LS M1 (after_initial M1 β)"
unfolding ‹(γ@[xy] ∈ LS M2 q1) = ([xy] ∈ LS M2 (after_initial M2 (π@γ)))›
‹([xy] ∈ LS M2 (after_initial M2 (π@γ))) = ([xy] ∈ LS M2 (after_initial M2 α))›
‹([xy] ∈ LS M2 (after M2 (FSM.initial M2) α)) = ([xy] ∈ LS M1 (after M1 (FSM.initial M1) α))›
‹([xy] ∈ LS M1 (after M1 (FSM.initial M1) α)) = ([xy] ∈ LS M1 (after M1 (FSM.initial M1) β))›
by simp+
have "α@[xy] ∈ L M1"
using ‹[xy] ∈ LS M1 (after_initial M1 α)› unfolding after_language_iff[OF ‹observable M1› ‹α ∈ L M1›] .
moreover have "β@[xy] ∈ L M1"
using ‹[xy] ∈ LS M1 (after_initial M1 β)› unfolding after_language_iff[OF ‹observable M1› ‹β ∈ L M1›] .
moreover have "converge M1 α β"
using ‹converge M1 (π @ γ) (τ @ γ)› ‹converge M1 α (π @ γ)› ‹converge M1 β (τ @ γ)›
unfolding converge.simps
by blast
ultimately have "converge M1 (α@[xy]) (β@[xy])"
using converge_append[OF ‹observable M1›] language_prefix[of β "[xy]" M1 "initial M1"] by blast
have "(α @ [xy]) ∈ L M2" and "(β @ [xy]) ∈ L M2"
using ‹α@[xy] ∈ L M1› ‹α@[xy] ∈ SC› ‹β@[xy] ∈ L M1› ‹β@[xy] ∈ SC ›‹L M1 ∩ T = L M2 ∩ T› ‹SC ⊆ T› by blast+
have "after_initial M1 (α@[xy]) ∈ reachable_states M1"
using observable_after_path[OF ‹observable M1› ‹α@[xy] ∈ L M1›]
unfolding reachable_states_def
by (metis (mono_tags, lifting) mem_Collect_eq)
have "(α@[xy]) ∈ A (after_initial M1 (α@[xy]))"
unfolding A
using convergence_minimal[OF assms(3,1) _ ‹α@[xy] ∈ L M1›, of "f (after_initial M1 (α@[xy]))"]
using f2[OF ‹after_initial M1 (α@[xy]) ∈ reachable_states M1›]
using ‹α@[xy] ∈ SC›
by (metis (no_types, lifting) Int_iff ‹α @ [xy] ∈ L M1› ‹after M1 (FSM.initial M1) (α @ [xy]) ∈ reachable_states M1› assms(1) f1 member_filter observable_after_path observable_path_io_target singletonD)
then have "after M2 (FSM.initial M2) (α @ [xy]) ∈ Q (after_initial M1 (α@[xy]))"
unfolding Q
using observable_io_targets[OF ‹observable M2› ‹(α @ [xy]) ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹(α @ [xy]) ∈ L M2›]
by (metis UN_iff insertCI the_elem_eq)
then have "∃q'∈reachable_states M1. after M2 (FSM.initial M2) (α @ [xy]) ∈ Q q'"
using ‹after_initial M1 (α@[xy]) ∈ reachable_states M1› by blast
moreover have "(THE q'. q' ∈ reachable_states M1 ∧ after M2 (FSM.initial M2) (α @ [xy]) ∈ Q q') = (after_initial M1 (α@[xy]))"
using ‹after_initial M1 (α@[xy]) ∈ reachable_states M1›
using ‹after M2 (FSM.initial M2) (α @ [xy]) ∈ Q (after_initial M1 (α@[xy]))›
by (simp add: ‹⋀q. ∃⇩≤⇩1 q'. q' ∈ reachable_states M1 ∧ q ∈ Q q'› the1_equality')
moreover have "after M2 (FSM.initial M2) (β @ [xy]) ∈ Q (after_initial M1 (α@[xy]))"
proof -
have "(β@[xy]) ∈ A (after_initial M1 (α@[xy]))"
using A ‹α @ [xy] ∈ A (after M1 (FSM.initial M1) (α @ [xy]))› ‹β @ [xy] ∈ L M1› ‹β @ [xy] ∈ SC› ‹converge M1 (α @ [xy]) (β @ [xy])› by auto
then show ?thesis
unfolding Q
using observable_io_targets[OF ‹observable M2› ‹(β @ [xy]) ∈ L M2›]
unfolding after_io_targets[OF ‹observable M2› ‹(β @ [xy]) ∈ L M2›]
by (metis UN_iff insertCI the_elem_eq)
qed
ultimately have "after_initial M2 (β@[xy]) ∈ partition (after_initial M2 (α@[xy]))"
unfolding partition
by presburger
moreover have "after_initial M2 (α@[xy]) = after_initial M2 ((π@γ)@[xy])"
using converge_append[OF assms(2) ‹converge M2 α (π@γ)› ‹(α @ [xy]) ∈ L M2› ‹(π@γ) ∈ L M2›]
unfolding convergence_minimal[OF assms(4,2) ‹(α @ [xy]) ∈ L M2› converge_extend[OF assms(2) ‹converge M2 α (π@γ)› ‹(α @ [xy]) ∈ L M2› ‹(π@γ) ∈ L M2›]]
.
moreover have "after_initial M2 (β@[xy]) = after_initial M2 ((τ@γ)@[xy])"
using converge_append[OF assms(2) ‹converge M2 β (τ@γ)› ‹(β @ [xy]) ∈ L M2› ‹(τ@γ) ∈ L M2›]
unfolding convergence_minimal[OF assms(4,2) ‹(β @ [xy]) ∈ L M2› converge_extend[OF assms(2) ‹converge M2 β (τ@γ)› ‹(β @ [xy]) ∈ L M2› ‹(τ@γ) ∈ L M2›]]
.
ultimately show "after M2 q2 (γ@[xy]) ∈ partition (after M2 q1 (γ@[xy]))"
unfolding q1 q2
unfolding after_split[OF assms(2) converge_extend[OF assms(2) ‹converge M2 α (π@γ)› ‹(α @ [xy]) ∈ L M2› ‹(π@γ) ∈ L M2›]]
unfolding after_split[OF assms(2) converge_extend[OF assms(2) ‹converge M2 β (τ@γ)› ‹(β @ [xy]) ∈ L M2› ‹(τ@γ) ∈ L M2›]]
by (metis ‹γ @ [xy] ∈ LS M2 q1› ‹π @ γ ∈ L M2› ‹τ @ γ ∈ L M2› ‹after M2 (after M2 (FSM.initial M2) (π @ γ)) [xy] = after M2 (FSM.initial M2) ((π @ γ) @ [xy])› ‹after M2 (after M2 (FSM.initial M2) (τ @ γ)) [xy] = after M2 (FSM.initial M2) ((τ @ γ) @ [xy])› after_split assms(2) p1 q1 q2)
qed
ultimately show ?thesis
by blast
qed
qed
qed
qed
ultimately show ?thesis
using ofsm_table_set_observable[OF ‹observable M2› ‹q1 ∈ states M2› is_eq, of "m - size_r M1"]
unfolding q1 q2
by blast
qed
ultimately have "after M2 (FSM.initial M2) τ ∈ ofsm_table M2 partition (m - n0) (after M2 (FSM.initial M2) π)"
using ofsm_table_subset[OF ‹size_r M1 ≤ n0›, of M2 partition "initial M2"]
by (meson diff_le_mono2 in_mono ofsm_table_subset)
moreover have "after M2 (FSM.initial M2) π ∈ states M2"
by (metis IntD1 after_is_state assms(2) assms(7) assms(8))
ultimately have "after M2 (FSM.initial M2) τ ∈ ofsm_table_fix M2 partition 0 (after M2 (FSM.initial M2) π)"
using ofsm_table_fix_partition_fixpoint[OF ‹equivalence_relation_on_states M2 partition› ‹size M2 ≤ m›, of "after M2 (FSM.initial M2) π"]
unfolding n0
by blast
then have "LS M2 (after_initial M2 τ) = LS M2 (after_initial M2 π)"
unfolding ofsm_table_fix_set[OF ‹after M2 (FSM.initial M2) π ∈ states M2› ‹observable M2› ‹equivalence_relation_on_states M2 partition›]
by blast
then show ?thesis
unfolding converge.simps
by (metis assms(15) converge.elims(2))
qed
lemma preserves_divergence_minimally_distinguishing_prefixes_lower_bound :
fixes M1 :: "('a,'b,'c) fsm"
fixes M2 :: "('d,'b,'c) fsm"
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "¬converge M2 u v"
and "u ∈ L M2"
and "v ∈ L M2"
and "minimally_distinguishes M2 (after_initial M2 u) (after_initial M2 v) w"
and "wp ∈ list.set (prefixes w)"
and "wp ≠ w"
and "wp ∈ LS M1 (after_initial M1 u) ∩ LS M1 (after_initial M1 v)"
and "preserves_divergence M1 M2 {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes wp)}"
and "L M1 ∩ {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes wp)} = L M2 ∩ {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes wp)}"
shows "card (after_initial M2 ` {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes wp)}) ≥ length wp + (card (FSM.after M1 (after_initial M1 u) ` (list.set (prefixes wp)))) + 1"
proof -
define k where "k = length wp"
then show ?thesis
using assms(10,11,12,13,14)
proof (induction k arbitrary: wp rule: less_induct)
case (less k)
show ?case proof (cases k)
case 0
then have "wp = []"
using less.prems by auto
have "{α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes [])} = {u,v}"
by auto
moreover have "(after_initial M2 u) ≠ (after_initial M2 v)"
using assms(9) assms(2) assms(4) assms(6) assms(7) assms(8) convergence_minimal by blast
ultimately have "card (after_initial M2 ` {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes [])}) = 2"
by auto
have "FSM.after M1 (after_initial M1 u) ` (list.set (prefixes [])) = {after_initial M1 u}"
unfolding prefixes_set by auto
then have "length [] + (card (FSM.after M1 (after_initial M1 u) ` (list.set (prefixes [])))) + 1 = 2"
by auto
then show ?thesis
unfolding ‹wp = []›
using ‹card (after_initial M2 ` {α@γ | α γ . α ∈ {u,v} ∧ γ ∈ list.set (prefixes [])}) = 2›
by simp
next
case (Suc k')
have "⋀ w''. w'' ∈ set (prefixes wp) ⟹ u@w'' ∈ L M1"
by (metis after_language_iff assms(1) assms(5) converge.elims(2) inf_idem language_prefix less.prems(4) prefixes_set_ob)
then have "⋀ w''. w'' ∈ set (prefixes wp) ⟹ v@w'' ∈ L M1"
by (meson assms(1) assms(5) converge.elims(2) converge_extend)
have "⋀ w'' . w'' ∈ set (prefixes wp) ⟹ converge M1 (u@w'') (v@w'')"
using ‹⋀w''. w'' ∈ set (prefixes wp) ⟹ u @ w'' ∈ L M1› assms(1) assms(5) converge.simps converge_append by blast
have "⋀ w' . w' ∈ set (prefixes wp) ⟹ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes w')} ⊆ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)}"
using prefixes_prefix_subset[of _ wp]
by blast
have "⋀ w' . {u @ γ | γ. γ ∈ set (prefixes w')} ⊆ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes w')}"
using prefixes_set_subset by blast
have "⋀ w' . {v @ γ | γ. γ ∈ set (prefixes w')} ⊆ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes w')}"
using prefixes_set_subset by blast
have "u@wp ∈ L M1"
by (metis Int_absorb after_language_iff assms(1) assms(5) converge.simps less.prems(4))
moreover have "u@wp ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)}"
unfolding prefixes_set by blast
ultimately have "u@wp ∈ L M2"
using less.prems(6) by blast
then have "wp ∈ LS M2 (after_initial M2 u)"
by (meson after_language_iff assms(2) language_prefix)
have "v@wp ∈ L M1"
by (meson ‹u @ wp ∈ L M1› assms(1) assms(5) converge.simps converge_extend)
moreover have "v@wp ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)}"
unfolding prefixes_set by blast
ultimately have "v@wp ∈ L M2"
using less.prems(6) by blast
then have "wp ∈ LS M2 (after_initial M2 v)"
by (meson after_language_iff assms(2) language_prefix)
have no_conv_2: "⋀ w'' . w'' ∈ set (prefixes wp) ⟹ ¬converge M2 (u@w'') (v@w'') ∧ u@w'' ∈ L M1 ∧ v@w'' ∈ L M1 ∧ u@w'' ∈ L M2 ∧ v@w'' ∈ L M2"
proof -
fix w'' assume *: "w'' ∈ set (prefixes wp)"
then have "w'' ∈ set (prefixes w)"
using less.prems
by (metis (no_types, lifting) insert_subset mk_disjoint_insert prefixes_set_ob prefixes_set_subset)
have "u@w'' ∈ L M1"
using ‹⋀w''. w'' ∈ set (prefixes wp) ⟹ u @ w'' ∈ L M1› * by auto
then have "u@w'' ∈ L M2"
using assms(14) less.prems *
by (metis (no_types, lifting) ‹wp ∈ LS M2 (after_initial M2 u)› after_language_iff assms(2) assms(7) language_prefix prefixes_set_ob)
then have "w'' ∈ LS M2 (after_initial M2 u)"
by (meson after_language_iff assms(2) language_prefix)
have "v@w'' ∈ L M1"
using ‹⋀w''. w'' ∈ set (prefixes wp) ⟹ v @ w'' ∈ L M1› * by auto
then have "v@w'' ∈ L M2"
using assms(14) less.prems(1) *
by (metis (no_types, lifting) ‹wp ∈ LS M2 (after_initial M2 v)› after_language_iff assms(2) assms(8) language_prefix prefixes_set_ob)
then have "w'' ∈ LS M2 (after_initial M2 v)"
by (meson after_language_iff assms(2) language_prefix)
have "distinguishes M2 (after_initial M2 u) (after_initial M2 v) w"
using assms(9) unfolding minimally_distinguishes_def by auto
show "¬converge M2 (u@w'') (v@w'') ∧ u@w'' ∈ L M1 ∧ v@w'' ∈ L M1 ∧ u@w'' ∈ L M2 ∧ v@w'' ∈ L M2"
using distinguishes_diverge_prefix[OF assms(2) ‹distinguishes M2 (after_initial M2 u) (after_initial M2 v) w› assms(7,8) ‹w'' ∈ set (prefixes w)› ‹w'' ∈ LS M2 (after_initial M2 u)› ‹w'' ∈ LS M2 (after_initial M2 v)›]
‹u@w'' ∈ L M1› ‹v@w'' ∈ L M1› ‹u@w'' ∈ L M2› ‹v@w'' ∈ L M2›
by blast
qed
have div_on_prefixes : "⋀ w'' . w'' ∈ set (prefixes wp) ⟹ after_initial M2 (u@w'') ≠ after_initial M2 (v@w'')"
using no_conv_2
using assms(2) assms(4) convergence_minimal by blast
then have div_on_proper_prefixes : "⋀ w' w'' . w' ∈ set (prefixes wp) ⟹ w'' ∈ set (prefixes w') ⟹ after_initial M2 (u@w'') ≠ after_initial M2 (v@w'')"
using prefixes_prefix_subset by blast
have "wp = (butlast wp)@[last wp]"
using Suc less.prems(1)
by (metis append_butlast_last_id length_greater_0_conv zero_less_Suc)
then have "(FSM.after M1 (after_initial M1 u) ` (list.set (prefixes wp))) = Set.insert (FSM.after M1 (after_initial M1 u) wp) (FSM.after M1 (after_initial M1 u) ` (list.set (prefixes (butlast wp))))"
using prefixes_set_Cons_insert
by (metis image_insert)
consider "(FSM.after M1 (after_initial M1 u) wp) ∉ (FSM.after M1 (after_initial M1 u) ` (list.set (prefixes (butlast wp))))" |
"(FSM.after M1 (after_initial M1 u) wp) ∈ (FSM.after M1 (after_initial M1 u) ` (list.set (prefixes (butlast wp))))"
by blast
obtain w_suffix where "w = (wp)@w_suffix"
using less.prems(2)
using prefixes_set_ob by blast
define wk where wk: "wk = (λ i . take i wp)"
define wk' where wk': "wk' = (λ i . drop i wp)"
have "⋀ i . (wk i)@(wk' i) = wp"
unfolding wk wk' by auto
then have "⋀ i . wk i ∈ set (prefixes wp)"
unfolding prefixes_set
by auto
then have "⋀ i . set (prefixes (wk i)) ⊆ set (prefixes wp)"
by (simp add: prefixes_prefix_subset)
have "⋀ i . i < k ⟹ wk' i ≠ []"
using less.prems(1)
by (simp add: wk')
have "wk k = wp"
using less.prems(1)
by (simp add: wk)
have "⋀ i . ¬ converge M2 (u @ wk i) (v @ wk i)"
using no_conv_2[OF ‹⋀ i . wk i ∈ set (prefixes wp)›] by blast
have "⋀ i . u@wk i ∈ L M1"
using no_conv_2[OF ‹⋀ i . wk i ∈ set (prefixes wp)›] by blast
have "⋀ i . u@wk i ∈ L M2"
using no_conv_2[OF ‹⋀ i . wk i ∈ set (prefixes wp)›] by blast
have "⋀ i . v@wk i ∈ L M1"
using no_conv_2[OF ‹⋀ i . wk i ∈ set (prefixes wp)›] by blast
have "⋀ i . v@wk i ∈ L M2"
using no_conv_2[OF ‹⋀ i . wk i ∈ set (prefixes wp)›] by blast
have "⋀ w'' . w'' ∈ set (prefixes wp) ⟹ w'' = wk (length w'')"
unfolding prefixes_take_iff unfolding wk
by auto
then have "⋀ i w'' . w'' ∈ set (prefixes (wk i)) ⟹ ∃ j . w'' = wk j ∧ j ≤ i"
by (metis min_def order_refl prefixes_take_iff take_take wk)
have prefixes_same_reaction: "⋀ j . j < k ⟹ w_suffix ∈ LS M2 (after_initial M2 (u@wk j)) = (w_suffix ∈ LS M2 (after_initial M2 (v@wk j)))"
proof -
fix j assume "j < k"
then have "wp = (wk j)@(wk' j)" and "(wk' j) ≠ []"
using ‹⋀ i . (wk i)@(wk' i) = wp› ‹⋀ i . i < k ⟹ wk' i ≠ []› by auto
have "distinguishes M2 (after_initial M2 u) (after_initial M2 v) ((wk j)@(wk' j)@w_suffix)"
using assms(9)
unfolding ‹w = (wp)@w_suffix› ‹wp = (wk j)@(wk' j)› minimally_distinguishes_def
by (metis append.assoc)
have "u@wk j ∈ L M2"
using ‹⋀i. u @ wk i ∈ L M2› by blast
have "v@wk j ∈ L M2"
using ‹⋀i. v @ wk i ∈ L M2› by blast
have *: "minimally_distinguishes M2 (after_initial M2 (u @ wk j)) (after_initial M2 (v @ wk j)) ((wk' j)@w_suffix)"
using assms(9) minimally_distinguishes_after_append_initial[OF assms(2,4) ‹u ∈ L M2› ‹v ∈ L M2›, of "wk j"]
using ‹w = wp @ w_suffix› ‹wk' j ≠ []› ‹wp = wk j @ wk' j› by auto
then have "¬distinguishes M2 (after_initial M2 (u@wk j)) (after_initial M2 (v@wk j)) w_suffix"
unfolding minimally_distinguishes_def
by (metis "*" ‹u @ wk j ∈ L M2› ‹v @ wk j ∈ L M2› ‹wk' j ≠ []› append.left_neutral append.right_neutral assms(2) minimally_distinguishes_no_prefix)
then show "w_suffix ∈ LS M2 (after_initial M2 (u@wk j)) = (w_suffix ∈ LS M2 (after_initial M2 (v@wk j)))"
unfolding distinguishes_def by blast
qed
have "⋀ i . u@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}"
using ‹⋀i. wk i ∈ set (prefixes wp)› by blast
have "⋀ i . v@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}"
using ‹⋀i. wk i ∈ set (prefixes wp)› by blast
have "u@(wp) ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}"
using prefixes_set by blast
have "v@(wp) ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}"
using prefixes_set by blast
define q where q: "q = (λ i . after_initial M1 (u@(wk i)))"
define a where a: "a = (λ i . after_initial M2 (u@(wk i)))"
define b where b: "b = (λ i . after_initial M2 (v@(wk i)))"
define I' where I': "I' = (λ i . {j . j ≤ Suc k' ∧ q i = q j})"
define l where l: "l = card (q ` (⋃ i ∈ {..Suc k'} . I' i))"
have q_v: "⋀ i . q i = after_initial M1 (v@(wk i))"
unfolding q
by (meson ‹⋀i. wk i ∈ set (prefixes wp)› ‹⋀w''. w'' ∈ set (prefixes wp) ⟹ converge M1 (u @ w'') (v @ w'')› assms(1) assms(3) converge.simps convergence_minimal)
have q_divergence: "⋀ i j . q i ≠ q j ⟹ a i ≠ a j ∧ a i ≠ b j ∧ b i ≠ a j ∧ b i ≠ b j"
proof -
fix i j assume "q i ≠ q j"
then have "¬ converge M1 (u@(wk i)) (u@(wk j))"
unfolding q
using assms(1) assms(3) converge.simps convergence_minimal by blast
then have "¬ converge M1 (u@(wk i)) (v@(wk j))"
"¬ converge M1 (v@(wk i)) (u@(wk j))"
"¬ converge M1 (v@(wk i)) (v@(wk j))"
using assms(1) assms(3) assms(5) converge_trans_2 by blast+
have "¬ converge M2 (u@(wk i)) (u@(wk j))"
using ‹¬ converge M1 (u@(wk i)) (u@(wk j))›
using less.prems(5) unfolding preserves_divergence.simps
using ‹⋀i. u @ wk i ∈ L M1› [of i] ‹⋀ i . u@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of i]
using ‹⋀i. u @ wk i ∈ L M1› [of j] ‹⋀ i . u@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of j]
by blast
then have "a i ≠ a j"
unfolding a
using ‹⋀i. u @ wk i ∈ L M2›
using assms(2) assms(4) convergence_minimal by blast
have "¬ converge M2 (v@(wk i)) (v@(wk j))"
using ‹¬ converge M1 (v@(wk i)) (v@(wk j))›
using less.prems(5) unfolding preserves_divergence.simps
using ‹⋀i. v @ wk i ∈ L M1› [of i] ‹⋀ i . v@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of i]
using ‹⋀i. v @ wk i ∈ L M1› [of j] ‹⋀ i . v@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of j]
by blast
then have "b i ≠ b j"
unfolding b
using ‹⋀i. v @ wk i ∈ L M2›
using assms(2) assms(4) convergence_minimal by blast
have "¬ converge M2 (u@(wk i)) (v@(wk j))"
using ‹¬ converge M1 (u@(wk i)) (v@(wk j))›
using less.prems(5) unfolding preserves_divergence.simps
using ‹⋀i. u @ wk i ∈ L M1› [of i] ‹⋀ i . u@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of i]
using ‹⋀i. v @ wk i ∈ L M1› [of j] ‹⋀ i . v@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of j]
by blast
then have "a i ≠ b j"
unfolding a b
using ‹⋀i. u @ wk i ∈ L M2› ‹⋀i. v @ wk i ∈ L M2›
using assms(2) assms(4) convergence_minimal by blast
have "¬ converge M2 (v@(wk i)) (u@(wk j))"
using ‹¬ converge M1 (v@(wk i)) (u@(wk j))›
using less.prems(5) unfolding preserves_divergence.simps
using ‹⋀i. v @ wk i ∈ L M1› [of i] ‹⋀ i . v@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of i]
using ‹⋀i. u @ wk i ∈ L M1› [of j] ‹⋀ i . u@wk i ∈ {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes (wp))}›[of j]
by blast
then have "b i ≠ a j"
unfolding b a
using ‹⋀i. v @ wk i ∈ L M2› ‹⋀i. u @ wk i ∈ L M2›
using assms(2) assms(4) convergence_minimal by blast
show "a i ≠ a j ∧ a i ≠ b j ∧ b i ≠ a j ∧ b i ≠ b j"
using ‹a i ≠ a j› ‹a i ≠ b j› ‹b i ≠ a j› ‹b i ≠ b j› by auto
qed
have "⋀ i . a i ∈ states M2"
by (metis ‹⋀i. u @ wk i ∈ L M2› a after_is_state assms(2))
have "⋀ i . b i ∈ states M2"
by (metis ‹⋀i. v @ wk i ∈ L M2› b after_is_state assms(2))
have "⋀ i j . i ≤ Suc k' ⟹ j ≤ Suc k' ⟹ q i = q j ⟹ I' i = I' j"
unfolding q I' by force
have "⋀ i . i ≤ Suc k' ⟹ i ∈ I' i"
unfolding I' q by force
moreover have "⋀ i . I' i ⊆ {..Suc k'}"
unfolding I' by force
ultimately have "(⋃ i ∈ {..Suc k'} . I' i) = {..Suc k'}"
by blast
then have "card (⋃ i ∈ {..Suc k'} . I' i) = k'+2"
by auto
have pt1: "finite {..Suc k'}"
by auto
have pt2: "{..Suc k'} ≠ {}"
by auto
have pt3: "(⋀x. x ∈ {..Suc k'} ⟹ I' x ⊆ {..Suc k'})"
using ‹⋀i. I' i ⊆ {..Suc k'}› atMost_atLeast0 by blast
have pt4: "(⋀x. x ∈ {..Suc k'} ⟹ I' x ≠ {})"
using ‹⋀i. i ≤ Suc k' ⟹ i ∈ I' i› by auto
have pt5: "(⋀x y. x ∈ {..Suc k'} ⟹ y ∈ {..Suc k'} ⟹ I' x = I' y ∨ I' x ∩ I' y = {})"
using I' by force
have pt6: "⋃ (I' ` {..Suc k'}) = {..Suc k'}"
using ‹⋃ (I' ` {..Suc k'}) = {..Suc k'}› by linarith
obtain l I where "I ` {..l} = I' ` {..Suc k'}"
and "⋀i j. i ≤ l ⟹ j ≤ l ⟹ i ≠ j ⟹ I i ∩ I j = {}"
and "card (I' ` {..Suc k'}) = Suc l"
using partition_helper[of "{..Suc k'}" I', OF pt1 pt2 pt3 pt4 pt5 pt6]
by metis
have "⋀ i . i ≤ l ⟹ ∃ j . j ≤ Suc k' ∧ I i = I' j"
using ‹I ` {..l} = I' ` {..Suc k'}›
by blast
define S where S: "S = (λ i . ⋃ j ∈ I i . {a j, b j})"
have "(⋃ i ∈ {..l} . S i) = (⋃ i ∈ {..Suc k'} . {a i, b i})"
unfolding S using ‹I ` {..l} = I' ` {..Suc k'}›
by (metis (no_types, lifting) Sup.SUP_cong UN_UN_flatten ‹⋃ (I' ` {..Suc k'}) = {..Suc k'}›)
then have "card (⋃ i ∈ {..l} . S i) = card (⋃ i ∈ {..Suc k'} . {a i, b i})"
by presburger
moreover have "⋀ i j. i ≤ l ⟹ j ≤ l ⟹ i ≠ j ⟹ S i ∩ S j = {}"
proof (rule ccontr)
fix i j assume "i ≤ l" and "j ≤ l" and "i ≠ j" and "S i ∩ S j ≠ {}"
then obtain ii jj where "ii ∈ I i" and "jj ∈ I j" and "{a ii, b ii} ∩ {a jj, b jj} ≠ {}"
unfolding S by blast
obtain i' j' where "i' ≤ Suc k'" and "j' ≤ Suc k'" and "I i = I' i'" and "I j = I' j'"
using ‹i ≤ l› ‹j ≤ l› ‹⋀ i . i ≤ l ⟹ ∃ j . j ≤ Suc k' ∧ I i = I' j›
by meson
moreover have "I i ∩ I j = {}"
by (meson ‹⋀j i. ⟦i ≤ l; j ≤ l; i ≠ j⟧ ⟹ I i ∩ I j = {}› ‹i ≤ l› ‹i ≠ j› ‹j ≤ l›)
ultimately have "I' i' ∩ I' j' = {}"
by blast
then have "q i' ≠ q j'"
unfolding I'
by (metis I' ‹I i = I' i'› ‹⋀i. i ≤ Suc k' ⟹ i ∈ I' i› ‹⋀thesis. (⋀i' j'. ⟦i' ≤ Suc k'; j' ≤ Suc k'; I i = I' i'; I j = I' j'⟧ ⟹ thesis) ⟹ thesis› empty_iff inf.idem)
then have "q ii ≠ q jj"
using I' ‹I i = I' i'› ‹I j = I' j'› ‹ii ∈ I i› ‹jj ∈ I j› by force
then have "a ii ≠ a jj" "a ii ≠ b jj" "b ii ≠ a jj" "b ii ≠ b jj"
using q_divergence
by blast+
then show False
using ‹{a ii, b ii} ∩ {a jj, b jj} ≠ {}›
by blast
qed
moreover have "∀ i ∈ {..l} . finite (S i)"
unfolding S
by (metis (no_types, lifting) ‹I ` {..l} = I' ` {..Suc k'}› ‹⋃ (I' ` {..Suc k'}) = {..Suc k'}› finite.emptyI finite.insertI finite_UN finite_atMost)
ultimately have "card (⋃ i ∈ {..l} . S i) = (∑ i ∈ {..l} . card (S i))"
using atMost_iff
using card_UN_disjoint[OF finite_atMost[of l], of S]
by blast
have eq7: "card (⋃ i ∈ {..Suc k'} . {a i, b i}) = (∑ i ∈ {..l} . card (S i))"
unfolding ‹card (⋃ i ∈ {..l} . S i) = card (⋃ i ∈ {..Suc k'} . {a i, b i})›[symmetric]
unfolding ‹card (⋃ i ∈ {..l} . S i) = (∑ i ∈ {..l} . card (S i))›
by blast
have eq8: "⋀ i . i ≤ l ⟹ card (S i) ≥ Suc (card (I i))"
proof -
fix i assume "i ≤ l"
have "S i ⊆ states M2"
unfolding S using ‹⋀ i . a i ∈ states M2› ‹⋀ i . b i ∈ states M2›
by blast
define W where W: "W = {w' ∈ set (prefixes w).
w' ≠ w ∧
after M2 (after_initial M2 u) w' ∈ S i ∧ after M2 (after_initial M2 v) w' ∈ S i}"
have "wk ` I i ⊆ W"
proof
fix x assume "x ∈ wk ` I i"
then obtain i' where "x = wk i'" and "i' ∈ I i"
by blast
then have "a i' ∈ S i" and "b i' ∈ S i"
unfolding S by blast+
then have "after M2 (after_initial M2 u) (wk i') ∈ S i"
"after M2 (after_initial M2 v) (wk i') ∈ S i"
unfolding a b
using ‹⋀i. u @ wk i ∈ L M2› ‹⋀i. v @ wk i ∈ L M2›
by (metis after_split assms(2))+
moreover have "wk i' ≠ w"
by (metis (no_types) ‹⋀i. wk i ∈ set (prefixes wp)› less.prems(2) less.prems(3) nat_le_linear prefixes_take_iff take_all_iff)
moreover have "wk i' ∈ set (prefixes w)"
using ‹⋀i. wk i ∈ set (prefixes wp)› less.prems(2) prefixes_prefix_subset by blast
ultimately show "x ∈ W"
unfolding ‹x = wk i'› W
by blast
qed
moreover have "finite W"
proof -
have "W ⊆ (set (prefixes w))"
unfolding W by blast
then show ?thesis
by (meson List.finite_set rev_finite_subset)
qed
ultimately have "card (wk ` I i) ≤ card W"
by (meson card_mono)
moreover have "card (wk ` I i) = card (I i)"
proof -
have "⋀ x y . x ∈ I i ⟹ y ∈ I i ⟹ x ≠ y ⟹ wk x ≠ wk y"
proof -
fix x y assume "x ∈ I i" "y ∈ I i" "x ≠ y"
then have "x ≤ Suc k'" "y ≤ Suc k'"
by (metis UN_I ‹I ` {..l} = I' ` {..Suc k'}› ‹⋃ (I' ` {..Suc k'}) = {..Suc k'}› ‹i ≤ l› atMost_iff)+
then show "wk x ≠ wk y"
using ‹x ≠ y› ‹k = length wp›
unfolding wk Suc
using take_diff by metis
qed
moreover have "finite (I i)"
by (metis ‹I ` {..l} = I' ` {..Suc k'}› ‹i ≤ l› atMost_iff finite_UN finite_atMost pt6)
ultimately show ?thesis
using image_inj_card_helper by metis
qed
ultimately have "card (I i) ≤ card W"
by simp
then have "card (I i) ≤ card (S i) - 1"
using minimally_distinguishes_proper_prefixes_card[OF assms(2,4) after_is_state[OF assms(2) ‹u ∈ L M2›] after_is_state[OF assms(2) ‹v ∈ L M2›] ‹minimally_distinguishes M2 (after_initial M2 u) (after_initial M2 v) w› ‹S i ⊆ states M2›]
unfolding W[symmetric]
by simp
moreover have "card (S i) > 0"
proof -
have "card (I i) > 0"
by (metis ‹⋀i. i ≤ l ⟹ ∃j≤Suc k'. I i = I' j› ‹card (wk ` I i) = card (I i)› ‹finite W› ‹i ≤ l› ‹wk ` I i ⊆ W› atMost_iff card_0_eq gr0I image_is_empty pt4 rev_finite_subset)
then show ?thesis
unfolding S
by (metis S calculation diff_le_self le_0_eq not_gr_zero)
qed
ultimately show "card (S i) ≥ Suc (card (I i))"
by linarith
qed
have "(∑ i ∈ {..l} . card (S i)) ≥ (∑ i ∈ {..l} . (Suc (card (I i))))"
using eq8
by (meson atMost_iff sum_mono)
moreover have "(∑ i ∈ {..l} . (Suc (card (I i)))) = (Suc l) + k' + 2"
proof -
have "(∑ i ∈ {..l} . (Suc (card (I i)))) = (Suc l) + (∑ i ∈ {..l} . (card (I i)))"
by (simp add: sum_Suc)
moreover have "(∑ i ∈ {..l} . (card (I i))) = k' + 2"
proof -
have "card (⋃ i ∈ {..l} . I i) = k' + 2"
using ‹card (⋃ i ∈ {..Suc k'} . I' i) = k'+2›
using ‹I ` {..l} = I' ` {..Suc k'}› by presburger
moreover have "(∑ i ∈ {..l} . (card (I i))) = card (⋃ i ∈ {..l} . I i)"
using sum_image_inj_card_helper[of l I]
by (metis ‹I ` {..l} = I' ` {..Suc k'}› ‹⋀j i. ⟦i ≤ l; j ≤ l; i ≠ j⟧ ⟹ I i ∩ I j = {}› ‹⋃ (I' ` {..Suc k'}) = {..Suc k'}› atMost_iff finite_UN finite_atMost)
ultimately show ?thesis
by auto
qed
ultimately show ?thesis
by linarith
qed
ultimately have "(∑ i ∈ {..l} . card (S i)) ≥ k' + l + 3"
by auto
moreover have "card (after_initial M2 ` {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)}) = (∑ i ∈ {..l} . card (S i))"
proof -
have "after_initial M2 ` {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)} = (⋃ i ∈ {..l} . S i)"
proof -
have "set (prefixes wp) = {wk i | i . i ≤ k}"
using less.prems(1) unfolding wk prefixes_set
by (metis ‹⋀i. wk i ∈ set (prefixes wp)› append_eq_conv_conj le_cases prefixes_set_ob take_all wk)
then have *:"{α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)} = (⋃ i ∈ {..Suc k'} . {u@wk i, v@wk i})"
unfolding Suc by auto
have **: "(⋃ i ∈ {..Suc k'} . {a i, b i}) = after_initial M2 ` (⋃ i ∈ {..Suc k'} . {u@wk i, v@wk i})"
unfolding a b by blast
show ?thesis
unfolding ‹(⋃ i ∈ {..l} . S i) = (⋃ i ∈ {..Suc k'} . {a i, b i})› ** *
by simp
qed
then show ?thesis
by (simp add: ‹card (⋃ (S ` {..l})) = (∑i≤l. card (S i))›)
qed
ultimately have bound_l: "card (after_initial M2 ` {α @ γ |α γ. α ∈ {u, v} ∧ γ ∈ set (prefixes wp)}) ≥ k + l + 2"
unfolding Suc by simp
have bound_r: "length wp + card (after M1 (after_initial M1 u) ` set (prefixes wp)) + 1 = k + l + 2"
proof -
have "set (prefixes wp) = {wk i | i . i ≤ k}"
using less.prems(1) unfolding wk prefixes_set
by (metis ‹⋀i. wk i ∈ set (prefixes wp)› append_eq_conv_conj le_cases prefixes_set_ob take_all wk)
let ?witness = "λi . SOME j . j ∈ i"
have "⋀ i . i ∈ (I' ` {..Suc k'}) ⟹ ?witness i ∈ i"
using ‹⋀i. i ≤ Suc k' ⟹ i ∈ I' i› some_in_eq by auto
have **:"⋀ Ii Ij . Ii ∈ (I' ` {..Suc k'}) ⟹ Ij ∈ (I' ` {..Suc k'}) ⟹ Ii ≠ Ij ⟹ ?witness Ii ≠ ?witness Ij"
proof -
fix Ii Ij assume "Ii ∈ (I' ` {..Suc k'})" and "Ij ∈ (I' ` {..Suc k'})" and "Ii ≠ Ij"
then have "Ii ∩ Ij = {}"
using pt5 by auto
moreover have "?witness Ii ∈ Ii"
using ‹⋀ i . i ∈ (I' ` {..Suc k'}) ⟹ ?witness i ∈ i› ‹Ii ∈ (I' ` {..Suc k'})›
by blast
moreover have "?witness Ij ∈ Ij"
using ‹⋀ i . i ∈ (I' ` {..Suc k'}) ⟹ ?witness i ∈ i› ‹Ij ∈ (I' ` {..Suc k'})›
by blast
ultimately show "?witness Ii ≠ ?witness Ij"
by fastforce
qed
have *: "finite (I' ` {..Suc k'})"
by auto
have c1: "card (I' ` {..Suc k'}) = card (?witness ` (I' ` {..Suc k'}))"
using image_inj_card_helper[of "I' ` {..Suc k'}" ?witness, OF * **]
by auto
have *: "finite (?witness ` (I' ` {..Suc k'}))"
by auto
have **:"⋀ i j . i ∈ (?witness ` (I' ` {..Suc k'})) ⟹ j ∈ (?witness ` (I' ` {..Suc k'})) ⟹ i ≠ j ⟹ q i ≠ q j"
proof -
fix i j assume "i ∈ (?witness ` (I' ` {..Suc k'}))" and "j ∈ (?witness ` (I' ` {..Suc k'}))" and "i ≠ j"
obtain i' where "i = ?witness (I' i')" and "i ∈ I' i'" and "i' ∈ {..Suc k'}"
using ‹i ∈ (?witness ` (I' ` {..Suc k'}))›
using ‹⋀i. i ∈ I' ` {..Suc k'} ⟹ (SOME j. j ∈ i) ∈ i› by blast
obtain j' where "j = ?witness (I' j')" and "j ∈ I' j'" and "j' ∈ {..Suc k'}"
using ‹j ∈ (?witness ` (I' ` {..Suc k'}))›
using ‹⋀i. i ∈ I' ` {..Suc k'} ⟹ (SOME j. j ∈ i) ∈ i› by blast
have "I' i' ≠ I' j'"
using ‹i ≠ j›
using ‹i = (SOME j. j ∈ I' i')› ‹j = (SOME j. j ∈ I' j')› by fastforce
then show "q i ≠ q j"
using ‹i ∈ I' i'› ‹j ∈ I' j'›
unfolding q I'
by force
qed
have c2: "card (I' ` {..Suc k'}) = card (q ` (?witness ` (I' ` {..Suc k'})))"
using image_inj_card_helper[of "(?witness ` (I' ` {..Suc k'}))" q, OF * **] c1
by force
have "q ` (?witness ` (I' ` {..Suc k'})) = q ` (⋃ i ∈ {..Suc k'} . I' i)"
proof
show "q ` ?witness ` I' ` {..Suc k'} ⊆ q ` ⋃ (I' ` {..Suc k'})"
proof
fix s assume "s ∈ q ` ?witness ` I' ` {..Suc k'}"
then obtain Ii where "Ii ∈ I' ` {..Suc k'}" and "s = q (?witness Ii)"
by blast
then have "s ∈ q ` Ii"
using ‹⋀i. i ∈ I' ` {..Suc k'} ⟹ (SOME j. j ∈ i) ∈ i› by blast
then show "s ∈ q ` ⋃ (I' ` {..Suc k'})"
using ‹Ii ∈ I' ` {..Suc k'}› by blast
qed
show "q ` ⋃ (I' ` {..Suc k'}) ⊆ q ` ?witness ` I' ` {..Suc k'}"
proof
fix s assume "s ∈ q ` ⋃ (I' ` {..Suc k'})"
then obtain i where "s ∈ q ` (I' i)" and "i ∈ {..Suc k'}"
by blast
have "?witness (I' i) ∈ I' i"
using ‹⋀i. i ∈ I' ` {..Suc k'} ⟹ (SOME j. j ∈ i) ∈ i› ‹i ∈ {..Suc k'}› by blast
then have "q ` (I' i) = {q (?witness (I' i))}"
unfolding q I'
by fastforce
then have "s = q (?witness (I' i))"
using ‹s ∈ q ` (I' i)› by blast
then show "s ∈ q ` ?witness ` I' ` {..Suc k'}"
using ‹i ∈ {..Suc k'}› by blast
qed
qed
then have c3: "card (I' ` {..Suc k'}) = card (q ` (⋃ i ∈ {..Suc k'} . I' i))"
using c2 by auto
have "q ` (⋃ i ∈ {..Suc k'} . I' i) = after M1 (after_initial M1 u) ` set (prefixes wp)"
proof -
have "set (prefixes wp) = {wk i | i . i ≤ k}"
using less.prems(1) unfolding wk prefixes_set
by (metis ‹⋀i. wk i ∈ set (prefixes wp)› append_eq_conv_conj le_cases prefixes_set_ob take_all wk)
also have "… = wk ` {..Suc k'}"
unfolding Suc
by (simp add: atMost_def setcompr_eq_image)
finally have *:"set (prefixes wp) = wk ` {..Suc k'}" .
have "⋀ i . after_initial M1 (u @ wk i) = after M1 (after_initial M1 u) (wk i)"
by (metis ‹⋀i. u @ wk i ∈ L M1› after_split assms(1))
then have **: "⋀ X . q ` X = after M1 (after_initial M1 u) ` wk ` X"
unfolding q
by fastforce
show ?thesis
unfolding * **
unfolding ‹(⋃ i ∈ {..Suc k'} . I' i) = {..Suc k'}›
by simp
qed
then have "card (I' ` {..Suc k'}) = card (after M1 (after_initial M1 u) ` set (prefixes wp))"
using c3 by auto
then have "card (after M1 (after_initial M1 u) ` set (prefixes wp)) = Suc l"
using ‹card (I' ` {..Suc k'}) = Suc l›
by auto
then show ?thesis
unfolding ‹k = length wp›[symmetric] by auto
qed
show ?thesis
using bound_l
unfolding bound_r .
qed
qed
qed
lemma sufficient_condition_for_convergence :
fixes M1 :: "('a,'b,'c) 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"
and "converge M1 π τ"
and "L M1 ∩ T = L M2 ∩ T"
and "⋀ γ x y . length (γ@[(x,y)]) ≤ m - size_r M1 ⟹
γ ∈ LS M1 (after_initial M1 π) ⟹
x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹
∃ SC α β . SC ⊆ T
∧ is_state_cover M1 SC
∧ {ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (γ@[(x,y)]))} ⊆ SC
∧ converge M1 π α
∧ converge M2 π α
∧ converge M1 τ β
∧ converge M2 τ β
∧ preserves_divergence M1 M2 SC"
and "∃ SC α β . SC ⊆ T
∧ is_state_cover M1 SC
∧ α ∈ SC ∧ β ∈ SC
∧ converge M1 π α
∧ converge M2 π α
∧ converge M1 τ β
∧ converge M2 τ β
∧ preserves_divergence M1 M2 SC"
shows "converge M2 π τ"
proof (cases "inputs M1 = {} ∨ outputs M1 = {}")
case True
then have "L M1 = {[]}"
using language_empty_IO by blast
then have "π = []" and "τ = []"
using assms(9) by auto
then show ?thesis
by auto
next
case False
define n where n: "n = size_r M1"
have "n ≤ m"
using assms(5) n by auto
show ?thesis proof (rule ccontr)
assume "¬ converge M2 π τ"
moreover have "π ∈ L M2" and "τ ∈ L M2"
using assms(12) by auto
ultimately have "after_initial M2 π ≠ after_initial M2 τ"
using assms(2) assms(4) convergence_minimal by blast
then obtain v where "minimally_distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v"
using minimally_distinguishes_ex
by (metis ‹¬ converge M2 π τ› ‹π ∈ L M2› ‹τ ∈ L M2› after_is_state assms(2) converge.simps)
then have "distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v"
unfolding minimally_distinguishes_def by auto
then have "v ≠ []"
by (meson ‹π ∈ L M2› ‹τ ∈ L M2› after_is_state assms(2) distinguishes_not_Nil)
have "length v > m - n"
proof (rule ccontr)
assume "¬ m - n < length v"
have ‹v ∈ set (prefixes v)›
unfolding prefixes_set by auto
show False proof (cases "v ∈ LS M1 (after_initial M1 π)")
case True
have "v = (butlast v)@[last v]"
using ‹v ≠ []› by fastforce
then obtain x y where "v = (butlast v)@[(x,y)]"
using prod.exhaust by metis
then have "(x,y) ∈ set v"
using in_set_conv_decomp by force
then have "x ∈ inputs M1" and "y ∈ outputs M1"
using language_io[OF True, of x y] by auto
moreover have "length (butlast v @ [(x, y)]) ≤ m - size_r M1"
using ‹¬ m - n < length v› ‹v = (butlast v)@[(x,y)]›
unfolding n by auto
moreover have "butlast v ∈ LS M1 (after_initial M1 π)"
using True language_prefix[of "butlast v" "[(x,y)]"]
unfolding ‹v = (butlast v)@[(x,y)]›[symmetric]
by metis
ultimately obtain SC α β where "SC ⊆ T"
and "{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes v)} ⊆ SC"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
using assms(11)[of "(butlast v)" x y]
unfolding ‹v = (butlast v)@[(x,y)]›[symmetric]
by meson
then have "α@v ∈ T" and "β@v ∈ T"
using ‹SC ⊆ T› ‹{ω@γ | ω γ . ω ∈ {α,β} ∧ γ ∈ list.set (prefixes v)} ⊆ SC› ‹v ∈ set (prefixes v)›
by auto
then have "L M1 ∩ {α@v,β@v} = L M2 ∩ {α@v,β@v}"
using assms(10) by blast
have "after_initial M1 π ≠ after_initial M1 τ"
using converge_distinguishable_helper[OF assms(1-4) ‹converge M1 π α› ‹converge M2 π α› ‹converge M1 τ β› ‹converge M2 τ β› ‹distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v› ‹L M1 ∩ {α@v,β@v} = L M2 ∩ {α@v,β@v}›] .
then show False
using ‹converge M1 π τ›
by (meson assms(1) assms(3) converge.elims(2) convergence_minimal)
next
case False
obtain io' x' y' io'' where "v = io'@[(x',y')]@io''"
and "io' ∈ LS M1 (after_initial M1 π)"
and "io'@[(x',y')] ∉ LS M1 (after_initial M1 π)"
using language_maximal_contained_prefix_ob[OF False _ assms(1)]
by (metis after_is_state assms(1) assms(9) converge.simps)
have "length io' < m - size_r M1"
using ‹¬ m - n < length v› unfolding ‹v = io'@[(x',y')]@io''› n by auto
then have "length (io'@[(x',y')]) ≤ m - size_r M1"
by auto
have "x' ∈ inputs M1" and "y' ∈ outputs M1"
proof -
have "x' ∈ inputs M1 ∧ y' ∈ outputs M1"
proof -
have "(x',y') ∈ set v"
unfolding ‹v = io'@[(x',y')]@io''› by auto
then have "(x', y') ∈ set (π @ v)" and "(x', y') ∈ set (τ @ v)"
by auto
have "π@v ∈ L M2 ∨ τ@v ∈ L M2"
using ‹distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v›
unfolding distinguishes_def
by (metis Un_iff ‹π ∈ L M2› ‹τ ∈ L M2› after_language_iff assms(2))
then show ?thesis
using language_io[of "π@v" M2 "initial M2", OF _ ‹(x', y') ∈ set (π @ v)›]
language_io[of "τ@v" M2 "initial M2", OF _ ‹(x', y') ∈ set (τ @ v)›]
by (metis assms(7) assms(8))
qed
then show "x' ∈ inputs M1" and "y' ∈ outputs M1"
by auto
qed
obtain SC α β where "SC ⊆ T"
and "{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (io'@[(x',y')]))} ⊆ SC"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
using assms(11)[of io' x' y', OF ‹length (io'@[(x',y')]) ≤ m - size_r M1› ‹io' ∈ LS M1 (after_initial M1 π)› ‹x' ∈ inputs M1› ‹y' ∈ outputs M1›]
by meson
show False proof (cases "v ∈ set (prefixes (io'@[(x',y')]))")
case True
then have "α@v ∈ T" and "β@v ∈ T"
using ‹SC ⊆ T› ‹{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (io'@[(x',y')]))} ⊆ SC›
by auto
then have "L M1 ∩ {α@v,β@v} = L M2 ∩ {α@v,β@v}"
using assms(10) by blast
have "after_initial M1 π ≠ after_initial M1 τ"
using converge_distinguishable_helper[OF assms(1-4) ‹converge M1 π α› ‹converge M2 π α› ‹converge M1 τ β› ‹converge M2 τ β› ‹distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v› ‹L M1 ∩ {α@v,β@v} = L M2 ∩ {α@v,β@v}›] .
then show False
using ‹converge M1 π τ›
by (meson assms(1) assms(3) converge.elims(2) convergence_minimal)
next
case False
then obtain io''' io'''' where "io'' = io'''@io''''"
and "v = io'@[(x',y')]@io'''"
and "io''' ≠ []"
using prefixes_prefix_suffix_ob[of v "io'@[(x',y')]" io'']
using ‹v ∈ set (prefixes v)›
unfolding ‹v = io'@[(x',y')]@io''›
by auto
then have "io'@[(x',y')] ∈ set (prefixes v)" and "io'@[(x',y')] ≠ v"
unfolding prefixes_set by auto
then have "io'@[(x',y')] ∈ LS M2 (after_initial M2 π)"
using minimally_distinguishes_proper_prefix_in_language[OF ‹minimally_distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v›, of "io'@[(x',y')]"]
by blast
then have "io'@[(x',y')] ∈ LS M2 (after_initial M2 α)"
using ‹converge M2 π α› converge.simps by blast
then have "α@(io'@[(x',y')]) ∈ L M2"
by (meson ‹converge M2 π α› after_language_iff assms(2) converge.elims(2))
moreover have "α@(io'@[(x',y')]) ∈ T"
using ‹{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (io'@[(x',y')]))} ⊆ SC› ‹SC ⊆ T›
unfolding prefixes_set by force
moreover have "α@(io'@[(x',y')]) ∉ L M1"
by (metis ‹converge M1 π α› ‹io' @ [(x', y')] ∉ LS M1 (after_initial M1 π)› after_language_iff assms(1) converge.elims(2))
ultimately show False
using assms(10) by blast
qed
qed
qed
define vm where vm: "vm = take (m-n) v"
define v_suffix where v_suffix: "v_suffix = drop (m-n) v"
have "length vm = m-n" and "vm ≠ v"
using ‹m - n < length v› unfolding vm by auto
have "v = vm@v_suffix"
unfolding vm v_suffix by auto
then have "vm ∈ set (prefixes v)"
unfolding prefixes_set by auto
have "vm ∈ LS M2 (after_initial M2 π)" and "vm ∈ LS M2 (after_initial M2 τ)"
using minimally_distinguishes_proper_prefix_in_language[OF ‹minimally_distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v› ‹vm ∈ set (prefixes v)› ‹vm ≠ v›]
by auto
have "vm ∈ LS M1 (after_initial M1 π)"
proof (rule ccontr)
assume False: "vm ∉ LS M1 (after_initial M1 π)"
obtain io' x' y' io'' where "vm = io'@[(x',y')]@io''"
and "io' ∈ LS M1 (after_initial M1 π)"
and "io'@[(x',y')] ∉ LS M1 (after_initial M1 π)"
using language_maximal_contained_prefix_ob[OF False _ assms(1)]
by (metis after_is_state assms(1) assms(9) converge.simps)
have "length io' < m - size_r M1"
using ‹length vm = m - n› unfolding ‹vm = io'@[(x',y')]@io''› n by auto
then have "length (io'@[(x',y')]) ≤ m - size_r M1"
by auto
have "x' ∈ inputs M1"
using ‹vm ∈ LS M2 (after_initial M2 π)›
unfolding ‹vm = io'@[(x',y')]@io''›
using language_io[of "io' @ [(x', y')] @ io''" M2 "initial M2" x' y']
by (metis append_Cons assms(7) in_set_conv_decomp language_io(1))
have "y' ∈ outputs M1"
using ‹vm ∈ LS M2 (after_initial M2 π)›
unfolding ‹vm = io'@[(x',y')]@io''›
using language_io[of "io' @ [(x', y')] @ io''" M2 "initial M2" x' y']
by (metis append_Cons assms(8) in_set_conv_decomp language_io(2))
obtain SC α β where "SC ⊆ T"
and "{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (io'@[(x',y')]))} ⊆ SC"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
using assms(11)[of io' x' y', OF ‹length (io'@[(x',y')]) ≤ m - size_r M1› ‹io' ∈ LS M1 (after_initial M1 π)› ‹x' ∈ inputs M1› ‹y' ∈ outputs M1›]
by meson
have "io'@[(x',y')] ∈ LS M2 (after_initial M2 π)"
using ‹vm ∈ LS M2 (after_initial M2 π)› language_prefix unfolding ‹vm = io'@[(x',y')]@io''›
by (metis append_assoc)
then have "α@(io'@[(x',y')]) ∈ L M2"
by (metis ‹converge M2 π α› after_language_iff assms(2) converge.simps)
moreover have "α@(io'@[(x',y')]) ∈ T"
using ‹{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes (io'@[(x',y')]))} ⊆ SC› ‹SC ⊆ T›
unfolding prefixes_set by force
moreover have "α@(io'@[(x',y')]) ∉ L M1"
by (metis ‹converge M1 π α› ‹io' @ [(x', y')] ∉ LS M1 (after_initial M1 π)› after_language_iff assms(1) converge.elims(2))
ultimately show False
using assms(10) by blast
qed
obtain SC α β where "SC ⊆ T"
and "is_state_cover M1 SC"
and "{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)} ⊆ SC"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
and "preserves_divergence M1 M2 SC"
proof (cases vm rule: rev_cases)
case Nil
then have "list.set (prefixes vm) = {[]}"
by auto
then have "⋀ α β . {ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)} = {α,β}"
by blast
then show ?thesis using assms(12) that
by force
next
case (snoc blvm lvm)
then obtain x y where "vm = blvm@[(x,y)]"
using prod.exhaust by metis
have *:"length (blvm@[(x,y)]) ≤ m - size_r M1"
using ‹length vm = m - n› ‹vm = blvm @ [(x, y)]› n by fastforce
have **:"blvm ∈ LS M1 (after_initial M1 π)"
using ‹vm = blvm @ [(x, y)]› language_prefix ‹vm ∈ LS M1 (after_initial M1 π)›
by metis
have ***:"x ∈ inputs M1" and ****:"y ∈ outputs M1"
using language_io[OF ‹vm ∈ LS M1 (after_initial M1 π)›, of x y]
unfolding ‹vm = blvm @ [(x, y)]› by auto
show ?thesis
using assms(11)[OF * ** *** ****] that
unfolding ‹vm = blvm @ [(x, y)]›[symmetric] by force
qed
have "vm ∈ LS M1 (after_initial M1 α) ∩ LS M1 (after_initial M1 β)"
using ‹converge M1 π α› ‹converge M1 π τ› ‹converge M1 τ β› ‹vm ∈ LS M1 (after_initial M1 π)› by auto
then have "vm ∈ LS M1 (after_initial M1 α)" by blast
have "α ∈ L M2"
using ‹converge M2 π α› by auto
have "β ∈ L M2"
using ‹converge M2 τ β› by auto
have "minimally_distinguishes M2 (after_initial M2 α) (after_initial M2 β) v"
using ‹minimally_distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v›
by (metis ‹α ∈ L M2› ‹β ∈ L M2› ‹π ∈ L M2› ‹τ ∈ L M2› ‹converge M2 π α› ‹converge M2 τ β› assms(2) assms(4) convergence_minimal)
have "converge M1 α β"
using ‹converge M1 π α› ‹converge M1 τ β› assms(9) by auto
have "¬converge M2 α β"
using ‹converge M2 π α› ‹converge M2 τ β› ‹¬converge M2 π τ› by auto
have "preserves_divergence M1 M2 {ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)}"
using ‹{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)} ⊆ SC› ‹preserves_divergence M1 M2 SC›
unfolding preserves_divergence.simps by blast
have "L M1 ∩ {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)} = L M2 ∩ {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}"
using ‹{ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)} ⊆ SC› ‹SC ⊆ T› assms(10)
by blast
have card_geq: "card (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) ≥ (m-n) + card (after M1 (after_initial M1 α) ` set (prefixes vm)) + 1"
using preserves_divergence_minimally_distinguishing_prefixes_lower_bound[OF assms(1-4) ‹converge M1 α β› ‹¬converge M2 α β› ‹α ∈ L M2› ‹β ∈ L M2› ‹minimally_distinguishes M2 (after_initial M2 α) (after_initial M2 β) v› ‹vm ∈ set (prefixes v)› ‹vm ≠ v› ‹vm ∈ LS M1 (after_initial M1 α) ∩ LS M1 (after_initial M1 β)› ‹preserves_divergence M1 M2 {ω@ω' | ω ω' . ω ∈ {α,β} ∧ ω' ∈ list.set (prefixes vm)}› ‹L M1 ∩ {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)} = L M2 ∩ {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}›]
unfolding ‹length vm = m-n› .
have "after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)} ⊆ states M2"
proof
fix q assume "q ∈ after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}"
then obtain w1 w2 where "q = after_initial M2 (w1@w2)"
and "w1 ∈ {α,β}"
and "w2 ∈ set (prefixes vm)"
by blast
have "w2 ∈ LS M2 (after_initial M2 α)"
using ‹w2 ∈ set (prefixes vm)› unfolding prefixes_set
by (metis ‹converge M2 π α› ‹vm ∈ LS M2 (after_initial M2 π)› ‹w2 ∈ set (prefixes vm)› converge.elims(2) language_prefix prefixes_set_ob)
then have "after_initial M2 (α@w2) ∈ states M2"
by (meson ‹α ∈ L M2› after_is_state after_language_iff assms(2))
have "w2 ∈ LS M2 (after_initial M2 β)"
using ‹w2 ∈ set (prefixes vm)› unfolding prefixes_set
by (metis ‹converge M2 τ β› ‹vm ∈ LS M2 (after_initial M2 τ)› ‹w2 ∈ set (prefixes vm)› converge.elims(2) language_prefix prefixes_set_ob)
then have "after_initial M2 (β@w2) ∈ states M2"
by (meson ‹β ∈ L M2› after_is_state after_language_iff assms(2))
show "q ∈ states M2"
unfolding ‹q = after_initial M2 (w1@w2)›
using ‹w1 ∈ {α,β}› ‹after_initial M2 (α@w2) ∈ states M2› ‹after_initial M2 (β@w2) ∈ states M2›
by blast
qed
have upper_bound: "card (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) ≤ m"
proof -
have "card (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) ≤ size M2"
using ‹after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)} ⊆ states M2›
using fsm_states_finite[of M2] unfolding FSM.size_def
by (simp add: card_mono)
then show ?thesis
using ‹size M2 ≤ m› by linarith
qed
have "after M1 (after_initial M1 α) ` set (prefixes vm) ⊆ reachable_states M1"
proof
fix q assume "q ∈ after M1 (after_initial M1 α) ` set (prefixes vm)"
then obtain vm' where "q = after M1 (after_initial M1 α) vm'" and "vm' ∈ set (prefixes vm)"
by auto
have "vm' ∈ LS M1 (after_initial M1 α)"
using ‹vm' ∈ set (prefixes vm)› unfolding prefixes_set
by (metis ‹vm ∈ LS M1 (after_initial M1 α)› ‹vm' ∈ set (prefixes vm)› language_prefix prefixes_set_ob)
then have "α@vm' ∈ L M1"
by (meson ‹converge M1 π α› after_language_iff assms(1) converge.simps)
moreover have "q = after_initial M1 (α@vm')"
unfolding ‹q = after M1 (after_initial M1 α) vm'›
by (meson after_split assms(1) calculation)
ultimately show "q ∈ reachable_states M1"
using after_reachable_initial[OF assms(1)] by auto
qed
moreover have "finite (reachable_states M1)"
using fsm_states_finite[of M1] reachable_state_is_state[of _ M1]
by (metis fsm_states_finite restrict_to_reachable_states_simps(2))
ultimately have "card (after M1 (after_initial M1 α) ` set (prefixes vm)) ≤ n"
unfolding n
by (metis card_mono)
have "⋀ q . q ∈ reachable_states M1 ⟹ ∃ io ∈ SC. q ∈ io_targets M1 io (FSM.initial M1)"
using ‹is_state_cover M1 SC›
by auto
obtain V where "is_state_cover_assignment M1 V"
and "⋀q. q ∈ reachable_states M1 ⟹ V q ∈ SC"
using state_cover_assignment_from_state_cover[OF ‹is_state_cover M1 SC›]
by blast
define unreached_states where unreached_states: "unreached_states = reachable_states M1 - (after M1 (after_initial M1 α) ` set (prefixes vm))"
have "size_r M1 = card (after M1 (after_initial M1 α) ` set (prefixes vm)) + card unreached_states"
by (metis ‹after M1 (after_initial M1 α) ` set (prefixes vm) ⊆ reachable_states M1› ‹card (after M1 (after_initial M1 α) ` set (prefixes vm)) ≤ n› ‹finite (reachable_states M1)› card_Diff_subset le_add_diff_inverse n rev_finite_subset unreached_states)
have unreached_V: "⋀ q . q ∈ unreached_states ⟹ V q ∈ L M1 ∧ V q ∈ L M2 ∧ V q ∈ SC"
proof -
fix q assume "q ∈ unreached_states"
then have "q ∈ reachable_states M1"
unfolding unreached_states by auto
then have "after_initial M1 (V q) = q"
using is_state_cover_assignment_observable_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by auto
have "V q ∈ L M1"
using is_state_cover_assignment_language[OF ‹is_state_cover_assignment M1 V›] ‹q ∈ reachable_states M1›
by auto
moreover have "V q ∈ T" and "V q ∈ SC"
using ‹⋀q. q ∈ reachable_states M1 ⟹ V q ∈ SC› ‹q ∈ reachable_states M1› ‹SC ⊆ T›
by auto
ultimately have "V q ∈ L M2"
by (metis Int_iff assms(10))
show "V q ∈ L M1 ∧ V q ∈ L M2 ∧ V q ∈ SC"
using ‹V q ∈ L M1› ‹V q ∈ L M2› ‹V q ∈ SC› by auto
qed
have "⋀ q1 q2 . q1 ∈ unreached_states ⟹ q2 ∈ unreached_states ⟹ q1 ≠ q2 ⟹ after_initial M2 (V q1) ≠ after_initial M2 (V q2)"
proof -
fix q1 q2 assume "q1 ∈ unreached_states" and "q2 ∈ unreached_states" and "q1 ≠ q2"
then have "q1 ∈ reachable_states M1" and "q2 ∈ reachable_states M1"
unfolding unreached_states by auto
then have "after_initial M1 (V q1) = q1" and "after_initial M1 (V q2) = q2"
using is_state_cover_assignment_observable_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
by auto
then have "V q1 ≠ V q2"
using ‹q1 ≠ q2›
by metis
have "V q1 ∈ L M1" and "V q2 ∈ L M1"
using is_state_cover_assignment_language[OF ‹is_state_cover_assignment M1 V›] ‹q1 ∈ reachable_states M1› ‹q2 ∈ reachable_states M1›
by auto
moreover have "V q1 ∈ T" and "V q2 ∈ T" and "V q1 ∈ SC" and "V q2 ∈ SC"
using ‹⋀q. q ∈ reachable_states M1 ⟹ V q ∈ SC› ‹q1 ∈ reachable_states M1› ‹q2 ∈ reachable_states M1› ‹SC ⊆ T›
by auto
ultimately have "V q1 ∈ L M2" and "V q2 ∈ L M2"
by (metis Int_iff assms(10))+
have "¬converge M1 (V q1) (V q2)"
by (meson ‹is_state_cover_assignment M1 V› ‹q1 ∈ reachable_states M1› ‹q1 ≠ q2› ‹q2 ∈ reachable_states M1› assms(1) assms(3) state_cover_assignment_diverges)
then have "¬converge M2 (V q1) (V q2)"
using ‹V q1 ∈ L M1› ‹V q2 ∈ L M1› ‹V q1 ∈ SC› ‹V q2 ∈ SC› ‹preserves_divergence M1 M2 SC›
unfolding preserves_divergence.simps by blast
then have "after_initial M2 (V q1) ≠ after_initial M2 (V q2)"
using ‹V q1 ∈ L M2› ‹V q2 ∈ L M2›
using assms(2) assms(4) convergence_minimal by blast
then show "after_initial M2 (V q1) ≠ after_initial M2 (V q2)"
by auto
qed
have lower_bound: "size M2 ≥ card (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) + card unreached_states"
proof -
have "finite unreached_states"
by (simp add: ‹finite (reachable_states M1)› unreached_states)
then have "finite ((λ q . after_initial M2 (V q)) ` unreached_states)"
by simp
have "card unreached_states = card ((λ q . after_initial M2 (V q)) ` unreached_states)"
using image_inj_card_helper[of unreached_states "(λ q . after_initial M2 (V q))", OF ‹finite unreached_states› ‹⋀ q1 q2 . q1 ∈ unreached_states ⟹ q2 ∈ unreached_states ⟹ q1 ≠ q2 ⟹ after_initial M2 (V q1) ≠ after_initial M2 (V q2)›]
by auto
have card_helper: "⋀ A B C . A ∩ B = {} ⟹ A ⊆ C ⟹ B ⊆ C ⟹ finite C ⟹ card C ≥ card A + card B"
by (metis Int_Un_distrib card_Un_disjoint card_mono finite_subset inf.absorb_iff2)
have "⋀ q . q ∈ unreached_states ⟹ after_initial M2 (V q) ∉ (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)})"
proof
fix q assume "q ∈ unreached_states"
and "after_initial M2 (V q) ∈ after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}"
then obtain w1 w2 where "after_initial M2 (V q) = after_initial M2 (w1@w2)"
and "w1 ∈ {α,β}"
and "w2 ∈ set (prefixes vm)"
by blast
then have "(w1@w2) ∈ SC"
using ‹{ω @ ω' |ω ω'. ω ∈ {α, β} ∧ ω' ∈ set (prefixes vm)} ⊆ SC› by blast
have "w2 ∈ LS M2 (after_initial M2 α)"
using ‹w2 ∈ set (prefixes vm)› unfolding prefixes_set
by (metis ‹converge M2 π α› ‹vm ∈ LS M2 (after_initial M2 π)› ‹w2 ∈ set (prefixes vm)› converge.elims(2) language_prefix prefixes_set_ob)
moreover have "w2 ∈ LS M2 (after_initial M2 β)"
using ‹w2 ∈ set (prefixes vm)› unfolding prefixes_set
by (metis ‹converge M2 τ β› ‹vm ∈ LS M2 (after_initial M2 τ)› ‹w2 ∈ set (prefixes vm)› converge.elims(2) language_prefix prefixes_set_ob)
ultimately have "w1@w2 ∈ L M2"
using ‹w1 ∈ {α,β}›
by (metis ‹converge M2 π α› ‹converge M2 τ β› after_language_iff assms(2) converge.simps empty_iff insert_iff)
then have "converge M2 (V q) (w1@w2)"
using unreached_V[OF ‹q ∈ unreached_states›]
using ‹after_initial M2 (V q) = after_initial M2 (w1 @ w2)› assms(2) assms(4) convergence_minimal by blast
moreover have "¬converge M1 (V q) (w1@w2)"
proof -
have "after M1 (after_initial M1 α) w2 = after M1 (after_initial M1 β) w2"
by (metis ‹converge M1 α β› assms(1) assms(3) converge.simps convergence_minimal)
then have "q ≠ (after M1 (after_initial M1 w1) w2)"
using ‹q ∈ unreached_states› ‹w1 ∈ {α,β}›
unfolding unreached_states
by (metis DiffD2 ‹w2 ∈ set (prefixes vm)› image_eqI insert_iff singletonD)
moreover have "(after M1 (after_initial M1 w1) w2) = (after_initial M1 (w1@w2))"
by (metis (no_types, lifting) Int_iff ‹SC ⊆ T› ‹w1 @ w2 ∈ L M2› ‹w1 @ w2 ∈ SC› after_split assms(1) assms(10) in_mono)
moreover have "q = after_initial M1 (V q)"
using is_state_cover_assignment_observable_after[OF assms(1) ‹is_state_cover_assignment M1 V›] ‹q ∈ unreached_states›
unfolding unreached_states
by (metis Diff_iff)
ultimately show ?thesis
by (metis assms(1) assms(3) converge.elims(2) convergence_minimal)
qed
moreover have "V q ∈ L M1 ∩ SC"
using unreached_V[OF ‹q ∈ unreached_states›] by auto
moreover have "w1@w2 ∈ L M1 ∩ SC"
using ‹SC ⊆ T› ‹w1 @ w2 ∈ L M2› ‹w1 @ w2 ∈ SC› assms(10) by auto
ultimately show False
using ‹preserves_divergence M1 M2 SC›
unfolding preserves_divergence.simps
by blast
qed
then have *: "((λ q . after_initial M2 (V q)) ` unreached_states) ∩ (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) = {}"
by blast
have **: "((λ q . after_initial M2 (V q)) ` unreached_states) ⊆ states M2"
using unreached_V
by (meson after_is_state assms(2) image_subset_iff)
moreover note ‹(after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) ⊆ states M2›
show ?thesis
unfolding ‹card unreached_states = card ((λ q . after_initial M2 (V q)) ` unreached_states)› FSM.size_def
using card_helper[OF * ** ‹(after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) ⊆ states M2› fsm_states_finite[of M2] ]
by linarith
qed
moreover have card_geq_unreached: "card (after_initial M2 ` {α' @ γ |α' γ. α' ∈ {α, β} ∧ γ ∈ set (prefixes vm)}) + card unreached_states ≥ m + 1"
using card_geq
using ‹size_r M1 ≤ m›
unfolding n
unfolding ‹size_r M1 = card (after M1 (after_initial M1 α) ` set (prefixes vm)) + card unreached_states›
by linarith
ultimately have "size M2 ≥ m + 1"
by linarith
then show False
using ‹size M2 ≤ m›
by linarith
qed
qed
lemma establish_convergence_from_pass :
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"
and "is_state_cover_assignment M1 V"
and "L M1 ∩ (V ` reachable_states M1) = L M2 ∩ V ` reachable_states M1"
and "converge M1 u v"
and "u ∈ L M2"
and "v ∈ L M2"
and prop1: "⋀γ x y.
length (γ @ [(x, y)]) ≤ (m - size_r M1) ⟹
γ ∈ LS M1 (after_initial M1 u) ⟹
x ∈ FSM.inputs M1 ⟹
y ∈ FSM.outputs M1 ⟹
L M1 ∩ ((V ` reachable_states M1) ∪ {ω @ ω' |ω ω'. ω ∈ {u, v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))}) =
L M2 ∩ ((V ` reachable_states M1) ∪ {ω @ ω' |ω ω'. ω ∈ {u, v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))}) ∧
preserves_divergence M1 M2 ((V ` reachable_states M1) ∪ {ω @ ω' |ω ω'. ω ∈ {u, v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))})"
and prop2: "preserves_divergence M1 M2 ((V ` reachable_states M1) ∪ {u, v})"
shows "converge M2 u v"
proof -
define language_up_to_depth where language_up_to_depth: "language_up_to_depth = {γ . γ ∈ LS M1 (after_initial M1 u) ∧ length γ < (m - size_r M1)}"
define T1 where T1: "T1 = ⋃{((V ` reachable_states M1) ∪ {ω @ ω' |ω ω'. ω ∈ {u, v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))}) | γ x y . length (γ @ [(x, y)]) ≤ (m - size_r M1) ∧ γ ∈ LS M1 (after_initial M1 u) ∧ x ∈ inputs M1 ∧ y ∈ outputs M1}"
define T2 where T2: "T2 = ((V ` reachable_states M1) ∪ {u, v})"
define T where T: "T = T1 ∪ T2"
have union_intersection_helper: "⋀ A B C . (A ∩ ⋃C = B ∩ ⋃C) = (∀C' ∈ C . A ∩ C' = B ∩ C')"
by blast
have "L M1 ∩ T = L M2 ∩ T"
proof -
have "(L M1 ∩ T1 = L M2 ∩ T1)"
unfolding T1 union_intersection_helper
using prop1 by blast
moreover have "L M1 ∩ T2 = L M2 ∩ T2"
proof-
have "u ∈ L M1" and "v ∈ L M1"
using ‹converge M1 u v› by auto
moreover note ‹L M1 ∩ (V ` reachable_states M1) = L M2 ∩ V ` reachable_states M1› ‹u ∈ L M2› ‹v ∈ L M2›
ultimately show ?thesis
unfolding T2 by blast
qed
ultimately show ?thesis
unfolding T by blast
qed
have prop1': "(⋀γ x y.
length (γ @ [(x, y)]) ≤ m - size_r M1 ⟹
γ ∈ LS M1 (after_initial M1 u) ⟹
x ∈ FSM.inputs M1 ⟹
y ∈ FSM.outputs M1 ⟹
∃SC α β.
SC ⊆ T ∧
is_state_cover M1 SC ∧
{ω @ ω' |ω ω'. ω ∈ {α, β} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))} ⊆ SC ∧
converge M1 u α ∧ converge M2 u α ∧ converge M1 v β ∧ converge M2 v β ∧ preserves_divergence M1 M2 SC)"
proof -
fix γ x y
define SC where SC: "SC = ((V ` reachable_states M1) ∪ {ω @ ω' |ω ω'. ω ∈ {u, v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))})"
assume "length (γ @ [(x, y)]) ≤ m - size_r M1"
"γ ∈ LS M1 (after_initial M1 u)"
"x ∈ FSM.inputs M1"
"y ∈ FSM.outputs M1"
then have "L M1 ∩ SC = L M2 ∩ SC"
"preserves_divergence M1 M2 SC"
using prop1[of γ x y]
unfolding SC
by blast+
have "SC ⊆ T"
unfolding T T1 SC
using ‹length (γ @ [(x, y)]) ≤ m - size_r M1› ‹γ ∈ LS M1 (after_initial M1 u)› ‹x ∈ FSM.inputs M1› ‹y ∈ FSM.outputs M1›
by blast
moreover have "is_state_cover M1 SC"
proof -
have "is_state_cover M1 (V ` reachable_states M1)"
using ‹is_state_cover_assignment M1 V›
by (metis is_minimal_state_cover.simps minimal_state_cover_is_state_cover)
moreover have "(V ` reachable_states M1) ⊆ SC"
unfolding SC
by blast
ultimately show ?thesis
unfolding is_state_cover.simps by blast
qed
moreover have "{ω @ ω' |ω ω'. ω ∈ {u,v} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))} ⊆ SC"
unfolding SC by auto
moreover have "converge M1 u u"
using ‹converge M1 u v› by auto
moreover have "converge M1 v v"
using ‹converge M1 u v› by auto
moreover have "converge M2 u u"
using ‹u ∈ L M2› by auto
moreover have "converge M2 v v"
using ‹v ∈ L M2› by auto
moreover note ‹preserves_divergence M1 M2 SC›
ultimately show "∃SC α β.
SC ⊆ T ∧
is_state_cover M1 SC ∧
{ω @ ω' |ω ω'. ω ∈ {α, β} ∧ ω' ∈ list.set (prefixes (γ @ [(x, y)]))} ⊆ SC ∧
converge M1 u α ∧ converge M2 u α ∧ converge M1 v β ∧ converge M2 v β ∧ preserves_divergence M1 M2 SC"
by blast
qed
have prop2': "∃SC α β.
SC ⊆ T ∧
is_state_cover M1 SC ∧
α ∈ SC ∧ β ∈ SC ∧ converge M1 u α ∧ converge M2 u α ∧ converge M1 v β ∧ converge M2 v β ∧ preserves_divergence M1 M2 SC"
proof -
define SC where SC: "SC = ((V ` reachable_states M1) ∪ {u, v})"
have "SC ⊆ T"
unfolding T T2 SC by auto
moreover have "is_state_cover M1 SC"
proof -
have "is_state_cover M1 (V ` reachable_states M1)"
using ‹is_state_cover_assignment M1 V›
by (metis is_minimal_state_cover.simps minimal_state_cover_is_state_cover)
moreover have "(V ` reachable_states M1) ⊆ SC"
unfolding SC
by blast
ultimately show ?thesis
unfolding is_state_cover.simps by blast
qed
moreover have "u ∈ SC" and "v ∈ SC"
unfolding SC by auto
moreover have "converge M1 u u"
using ‹converge M1 u v› by auto
moreover have "converge M1 v v"
using ‹converge M1 u v› by auto
moreover have "converge M2 u u"
using ‹u ∈ L M2› by auto
moreover have "converge M2 v v"
using ‹v ∈ L M2› by auto
moreover have ‹preserves_divergence M1 M2 SC›
using prop2 unfolding SC .
ultimately show ?thesis
by blast
qed
show "converge M2 u v"
using sufficient_condition_for_convergence[OF assms(1-8,11) ‹L M1 ∩ T = L M2 ∩ T› prop1' prop2']
by blast
qed
subsection ‹Proving Language Equivalence by Establishing a Convergence Preserving Initialised Transition Cover›
definition transition_cover :: "('a,'b,'c) fsm ⇒ ('b × 'c) list set ⇒ bool" where
"transition_cover M A = (∀ q ∈ reachable_states M . ∀ x ∈ inputs M . ∀ y ∈ outputs M . ∃ α. α ∈ A ∧ α@[(x,y)] ∈ A ∧ α ∈ L M ∧ after_initial M α = q)"
lemma initialised_convergence_preserving_transition_cover_is_complete :
fixes M1 :: "('a,'b,'c) fsm"
fixes M2 :: "('d,'b,'c) fsm"
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "inputs M2 = inputs M1"
and "outputs M2 = outputs M1"
and "L M1 ∩ T = L M2 ∩ T"
and "A ⊆ T"
and "transition_cover M1 A"
and "[] ∈ A"
and "preserves_convergence M1 M2 A"
shows "L M1 = L M2"
proof -
have convergence_right: "⋀ α β . α ∈ A ⟹ converge M1 α β ⟹ converge M2 α β"
proof -
fix α β
assume "α ∈ A" and "converge M1 α β"
then show "converge M2 α β"
proof (induction β arbitrary: α rule: rev_induct)
case Nil
then have "α ∈ L M1 ∩ A"
by auto
moreover have "[] ∈ L M1 ∩ A"
using ‹[] ∈ A›
by auto
ultimately show ?case
using ‹preserves_convergence M1 M2 A› ‹converge M1 α []›
unfolding preserves_convergence.simps
by blast
next
case (snoc xy β)
obtain x y where "xy = (x,y)"
by force
have "α ∈ L M1"
and "β @ [(x,y)] ∈ L M1"
and "LS M1 (after_initial M1 α) = LS M1 (after_initial M1 (β @ [(x,y)]))"
using snoc unfolding ‹xy = (x,y)›
by auto
then have "β ∈ L M1"
using language_prefix by metis
then have "after_initial M1 β ∈ reachable_states M1"
using after_reachable[OF ‹observable M1› _ reachable_states_initial]
by metis
moreover have "x ∈ inputs M1" and "y ∈ outputs M1"
using language_io[OF ‹β @ [(x,y)] ∈ L M1›] by auto
ultimately obtain γ where "γ ∈ A"
and "γ @ [(x, y)] ∈ A"
and "γ ∈ L M1"
and "after_initial M1 γ = after_initial M1 β"
using ‹transition_cover M1 A›
unfolding transition_cover_def
by blast
then have "converge M1 γ β"
using ‹β ∈ L M1›
by auto
then have "converge M2 γ β"
using snoc.IH[OF ‹γ ∈ A›]
by simp
then have "β ∈ L M2"
by auto
have "converge M1 β γ"
using ‹converge M1 γ β› by auto
then have "converge M1 (β @ [(x, y)]) (γ @ [(x, y)])"
using converge_append[OF assms(1) _ ‹β @ [(x,y)] ∈ L M1› ‹γ ∈ L M1›]
by auto
then have "γ @ [(x, y)] ∈ L M1"
by auto
then have "γ @ [(x, y)] ∈ L M2"
using ‹γ @ [(x, y)] ∈ A› assms(7,8)
by blast
then have "converge M2 (β @ [(x, y)]) (γ @ [(x, y)])"
using converge_append[OF assms(2) ‹converge M2 γ β› _ ‹β ∈ L M2›]
by auto
have "converge M1 α (γ @ [(x, y)])"
using ‹converge M1 (β @ [(x, y)]) (γ @ [(x, y)])›
using ‹converge M1 α (β @ [xy])›
unfolding ‹xy = (x,y)›
by auto
then have "converge M2 α (γ @ [(x, y)])"
using ‹α ∈ A› ‹γ @ [(x, y)] ∈ A› ‹preserves_convergence M1 M2 A›
unfolding preserves_convergence.simps
by auto
then show ?case
using ‹converge M2 (β @ [(x, y)]) (γ @ [(x, y)])›
unfolding ‹xy = (x,y)›
by auto
qed
qed
have reaching_sequence_ex : "⋀ q . q ∈ reachable_states M1 ⟹ ∃ α . α ∈ A ∧ α ∈ L M1 ∧ after_initial M1 α = q"
proof -
fix q assume "q ∈ reachable_states M1"
then show "∃ α . α ∈ A ∧ α ∈ L M1 ∧ after_initial M1 α = q"
proof (induction rule: reachable_states_cases)
case init
then show ?case
using ‹[] ∈ A›
using language_contains_empty_sequence
by (metis after.simps(1))
next
case (transition t)
obtain γ where "γ ∈ A" and "γ@[(t_input t,t_output t)] ∈ A" and "γ ∈ L M1" and "after_initial M1 γ = t_source t"
using ‹transition_cover M1 A›
‹t_source t ∈ reachable_states M1›
fsm_transition_input[OF ‹t ∈ transitions M1›]
fsm_transition_output[OF ‹t ∈ transitions M1›]
unfolding transition_cover_def
by blast
have "γ@[(t_input t,t_output t)] ∈ L M1"
using after_language_iff[OF assms(1) ‹γ ∈ L M1›, of "[(t_input t,t_output t)]"] ‹t ∈ transitions M1›
unfolding ‹after_initial M1 γ = t_source t› LS_single_transition
by auto
moreover have "after M1 (after_initial M1 γ) [(t_input t,t_output t)] = t_target t"
using after_transition[OF assms(1)] ‹t ∈ transitions M1›
unfolding ‹after_initial M1 γ = t_source t›
by auto
ultimately have "after_initial M1 (γ@[(t_input t,t_output t)]) = t_target t"
using after_split[OF assms(1)]
by metis
then show ?case
using ‹γ@[(t_input t,t_output t)] ∈ A› ‹γ@[(t_input t,t_output t)] ∈ L M1›
by blast
qed
qed
have arbitrary_convergence: "⋀ α β . converge M1 α β ⟹ converge M2 α β"
proof -
fix α β
assume "converge M1 α β"
then have "α ∈ L M1" and "β ∈ L M1"
by auto
then have "after_initial M1 α ∈ reachable_states M1"
using after_reachable[OF assms(1) _ reachable_states_initial]
by auto
then obtain γ where "γ ∈ A" and "γ ∈ L M1" and "after_initial M1 γ = after_initial M1 α"
using reaching_sequence_ex by blast
moreover have "after_initial M1 α = after_initial M1 β"
using convergence_minimal[OF assms(3,1) ‹α ∈ L M1› ‹β ∈ L M1›] ‹converge M1 α β›
by blast
ultimately have "converge M1 γ α" and "converge M1 γ β"
using ‹α ∈ L M1› ‹β ∈ L M1›
by auto
then have "converge M2 γ α" and "converge M2 γ β"
using convergence_right[OF ‹γ ∈ A›]
by auto
then show "converge M2 α β"
by auto
qed
have "L M1 ⊆ L M2"
proof
fix α assume "α ∈ L M1"
then have "converge M1 α α"
by auto
then have "converge M2 α α"
using arbitrary_convergence
by blast
then show "α ∈ L M2"
by auto
qed
moreover have "L M2 ⊆ L M1"
proof (rule ccontr)
assume "¬ L M2 ⊆ L M1"
then obtain α' where "α' ∈ L M2 - L M1"
by auto
obtain α xy β where "α' = α @ [xy] @ β" and "α ∈ L M2 ∩ L M1" and "α @ [xy] ∈ L M2 - L M1"
using minimal_failure_prefix_ob[OF assms(1,2) fsm_initial fsm_initial ‹α' ∈ L M2 - L M1›]
by blast
moreover obtain x y where "xy = (x,y)"
by force
ultimately have "α ∈ L M2" and "α ∈ L M1" and "α @ [(x,y)] ∈ L M2" and "α @ [(x,y)] ∉ L M1"
by auto
have "x ∈ inputs M1" and "y ∈ outputs M1"
using language_io[OF ‹α @ [(x,y)] ∈ L M2›]
unfolding ‹inputs M2 = inputs M1› ‹outputs M2 = outputs M1›
by auto
moreover have "after_initial M1 α ∈ reachable_states M1"
using after_reachable[OF assms(1) ‹α ∈ L M1› reachable_states_initial]
by auto
ultimately obtain γ where "γ ∈ A" and "γ@[(x,y)] ∈ A" and "γ ∈ L M1" and "after_initial M1 γ = after_initial M1 α"
using ‹transition_cover M1 A›
unfolding transition_cover_def
by blast
then have "converge M1 α γ"
using ‹α ∈ L M1›
by auto
then have "converge M2 α γ"
using arbitrary_convergence
by blast
have "γ ∈ L M2"
using ‹γ ∈ A› ‹γ ∈ L M1› assms(7,8)
by blast
have "γ @ [(x,y)] ∈ L M2"
using ‹α @ [(x,y)] ∈ L M2› ‹converge M2 α γ›
using after_language_iff[OF assms(2) ‹α ∈ L M2› ]
using after_language_iff[OF assms(2) ‹γ ∈ L M2› ]
unfolding convergence_minimal[OF assms(4,2) ‹α ∈ L M2› ‹γ ∈ L M2›]
by auto
have "γ @ [(x,y)] ∉ L M1"
using ‹α @ [(x,y)] ∉ L M1›
using after_language_iff[OF assms(1) ‹γ ∈ L M1› ]
using after_language_iff[OF assms(1) ‹α ∈ L M1› ]
unfolding ‹after_initial M1 γ = after_initial M1 α›
by auto
then have "γ @ [(x,y)] ∉ L M2"
using ‹γ@[(x,y)] ∈ A› assms(7,8)
by auto
then show False
using ‹γ @ [(x,y)] ∈ L M2›
by auto
qed
ultimately show ?thesis
by blast
qed
end