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 τ)