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› (* two traces converge if they are both in the language of the FSM and reach the same state *) 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 (* we can partition states of M2 via the Q-classes they belong to (using a single separate class for all states not contained in any Q-class *) 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 (* the partitioning results in at most n+1 classes *) 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 (* if γ is not contained in the language of s1, then by application of the SC it is also not contained in the languages of q1 or q2 *) 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 τ)