section ‹Minimisation by OFSM Tables› text ‹This theory presents the classical algorithm for transforming observable FSMs into language-equivalent observable and minimal FSMs in analogy to the minimisation of finite automata.› theory Minimisation imports FSM begin subsection ‹OFSM Tables› text ‹OFSM tables partition the states of an FSM based on an initial partition and an iteration counter. States are in the same element of the 0th table iff they are in the same element of the initial partition. States q1, q2 are in the same element of the (k+1)-th table if they are in the same element of the k-th table and furthermore for each IO pair (x,y) either (x,y) is not in the language of both q1 and q2 or it is in the language of both states and the states q1', q2' reached via (x,y) from q1 and q2, respectively, are in the same element of the k-th table.› fun ofsm_table :: "('a,'b,'c) fsm ⇒ ('a ⇒ 'a set) ⇒ nat ⇒ 'a ⇒ 'a set" where "ofsm_table M f 0 q = (if q ∈ states M then f q else {})" | "ofsm_table M f (Suc k) q = (let prev_table = ofsm_table M f k in {q' ∈ prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ prev_table qT = prev_table qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) })" lemma ofsm_table_non_state : assumes "q ∉ states M" shows "ofsm_table M f k q = {}" using assms by (induction k; auto) lemma ofsm_table_subset: assumes "i ≤ j" shows "ofsm_table M f j q ⊆ ofsm_table M f i q" proof - have *: "⋀ k . ofsm_table M f (Suc k) q ⊆ ofsm_table M f k q" proof - fix k show "ofsm_table M f (Suc k) q ⊆ ofsm_table M f k q" proof (cases k) case 0 show ?thesis unfolding 0 ofsm_table.simps Let_def by blast next case (Suc k') show ?thesis unfolding Suc ofsm_table.simps Let_def by force qed qed show ?thesis using assms proof (induction j) case 0 then show ?case by auto next case (Suc x) then show ?case using *[of x] using le_SucE by blast qed qed lemma ofsm_table_case_helper : "(case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) = ((∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f k qT = ofsm_table M f k qT') ∨ (h_obs M q x y = None ∧ h_obs M q' x y = None))" proof - have *: "⋀ a b P . (case a of Some a' ⇒ (case b of Some b' ⇒ P a' b' | None ⇒ False) | None ⇒ b = None) = ((∃ a' b' . a = Some a' ∧ b = Some b' ∧ P a' b') ∨ (a = None ∧ b = None))" (is "⋀ a b P . ?P1 a b P = ?P2 a b P") proof fix a b P show "?P1 a b P ⟹ ?P2 a b P" using case_optionE[of "b = None" "λa' . (case b of Some b' ⇒ P a' b' | None ⇒ False)" a] by (metis case_optionE) show "?P2 a b P ⟹ ?P1 a b P" by auto qed show ?thesis using *[of "h_obs M q' x y" "λqT qT' . ofsm_table M f k qT = ofsm_table M f k qT'" "h_obs M q x y"] . qed lemma ofsm_table_case_helper_neg : "(¬ (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)) = ((∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f k qT ≠ ofsm_table M f k qT') ∨ (h_obs M q x y = None ⟷ h_obs M q' x y ≠ None))" unfolding ofsm_table_case_helper by force lemma ofsm_table_fixpoint : assumes "i ≤ j" and "⋀ q . q ∈ states M ⟹ ofsm_table M f (Suc i) q = ofsm_table M f i q" and "q ∈ states M" shows "ofsm_table M f j q = ofsm_table M f i q" proof - have *: "⋀ k . k ≥ i ⟹ (⋀ q . q ∈ states M ⟹ ofsm_table M f (Suc k) q = ofsm_table M f k q)" proof - fix k :: nat assume "k ≥ i" then show "⋀ q . q ∈ states M ⟹ ofsm_table M f (Suc k) q = ofsm_table M f k q" proof (induction k) case 0 then show ?case using assms(2) by auto next case (Suc k) show "ofsm_table M f (Suc (Suc k)) q = ofsm_table M f (Suc k) q" proof (cases "i = Suc k") case True then show ?thesis using assms(2)[OF ‹q ∈ states M›] by simp next case False then have "i ≤ k" using ‹i ≤ Suc k› by auto have h_obs_state: "⋀ q x y qT . h_obs M q x y = Some qT ⟹ qT ∈ states M" using h_obs_state by fastforce show ?thesis proof (rule ccontr) assume "ofsm_table M f (Suc (Suc k)) q ≠ ofsm_table M f (Suc k) q" moreover have "ofsm_table M f (Suc (Suc k)) q ⊆ ofsm_table M f (Suc k) q" using ofsm_table_subset by (metis (full_types) Suc_n_not_le_n nat_le_linear) ultimately obtain q' where "q' ∉ {q' ∈ ofsm_table M f (Suc k) q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) }" and "q' ∈ ofsm_table M f (Suc k) q" using ofsm_table.simps(2)[of M f "Suc k" q] unfolding Let_def by blast then have "¬(∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None))" by blast then obtain x y where "x ∈ inputs M" and "y ∈ outputs M" and "¬ (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" by blast then consider "∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f (Suc k) qT ≠ ofsm_table M f (Suc k) qT'" | "(h_obs M q x y = None ⟷ h_obs M q' x y ≠ None)" unfolding ofsm_table_case_helper_neg by blast then show False proof cases case 1 then obtain qT qT' where "h_obs M q x y = Some qT" and "h_obs M q' x y = Some qT'" and "ofsm_table M f (Suc k) qT ≠ ofsm_table M f (Suc k) qT'" by blast then have "ofsm_table M f k qT ≠ ofsm_table M f k qT'" using Suc.IH[OF h_obs_state[OF ‹h_obs M q x y = Some qT›] ‹i ≤ k›] Suc.IH[OF h_obs_state[OF ‹h_obs M q' x y = Some qT'›] ‹i ≤ k›] by fast moreover have "q' ∈ ofsm_table M f k q" using ofsm_table_subset[of k "Suc k"] ‹q' ∈ ofsm_table M f (Suc k) q› by force ultimately have "ofsm_table M f (Suc k) q ≠ ofsm_table M f k q" using ‹x ∈ inputs M› ‹y ∈ outputs M› ‹h_obs M q x y = Some qT› ‹h_obs M q' x y = Some qT'› unfolding ofsm_table.simps(2) Let_def by force then show ?thesis using Suc.IH[OF Suc.prems(1) ‹i ≤ k›] by simp next case 2 then have "¬ (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" unfolding ofsm_table_case_helper_neg by blast moreover have "q' ∈ ofsm_table M f k q" using ofsm_table_subset[of k "Suc k"] ‹q' ∈ ofsm_table M f (Suc k) q› by force ultimately have "ofsm_table M f (Suc k) q ≠ ofsm_table M f k q" using ‹x ∈ inputs M› ‹y ∈ outputs M› unfolding ofsm_table.simps(2) Let_def by force then show ?thesis using Suc.IH[OF Suc.prems(1) ‹i ≤ k›] by simp qed qed qed qed qed show ?thesis using assms(1) proof (induction "j") case 0 then show ?case by auto next case (Suc j) show ?case proof (cases "i = Suc j") case True then show ?thesis by simp next case False then have "i ≤ j" using Suc.prems(1) by auto then have "ofsm_table M f j q = ofsm_table M f i q" using Suc.IH by auto moreover have "ofsm_table M f (Suc j) q = ofsm_table M f j q" using *[OF ‹i≤j› ‹q∈states M›] by assumption ultimately show ?thesis by blast qed qed qed (* restricts the range of the supplied function to the states of the FSM - required for (easy) termination *) function ofsm_table_fix :: "('a,'b,'c) fsm ⇒ ('a ⇒ 'a set) ⇒ nat ⇒ 'a ⇒ 'a set" where "ofsm_table_fix M f k = (let cur_table = ofsm_table M (λq. f q ∩ states M) k; next_table = ofsm_table M (λq. f q ∩ states M) (Suc k) in if (∀ q ∈ states M . cur_table q = next_table q) then cur_table else ofsm_table_fix M f (Suc k))" by pat_completeness auto termination proof - { fix M :: "('a,'b,'c) fsm" and f :: "('a ⇒ 'a set)" and k :: nat define f' where f': "f' = (λq. f q ∩ states M)" assume "∃q∈FSM.states M. ofsm_table M (λq. f q ∩ states M) k q ≠ ofsm_table M (λq. f q ∩ states M) (Suc k) q" then obtain q where "q ∈ states M" and "ofsm_table M f' k q ≠ ofsm_table M f' (Suc k) q" unfolding f' by blast have *: "⋀ k . (∑q∈FSM.states M. card (ofsm_table M f' k q)) = card (ofsm_table M f' k q) + (∑q∈FSM.states M - {q}. card (ofsm_table M f' k q))" using ‹q ∈ states M› by (meson fsm_states_finite sum.remove) have "⋀ q . ofsm_table M f' (Suc k) q ⊆ ofsm_table M f' k q" using ofsm_table_subset[of k "Suc k" M ] by auto moreover have "⋀ q . finite (ofsm_table M f' k q)" proof - fix q have "ofsm_table M (λq. f q ∩ states M) k q ⊆ ofsm_table M (λq. f q ∩ states M) 0 q" using ofsm_table_subset[of 0 k M "(λq. f q ∩ FSM.states M)" q] by auto then have "ofsm_table M f' k q ⊆ states M" unfolding f' using ofsm_table_non_state[of q M "(λq. f q ∩ FSM.states M)" k] by force then show "finite (ofsm_table M f' k q)" using fsm_states_finite finite_subset by auto qed ultimately have "⋀ q . card (ofsm_table M f' (Suc k) q) ≤ card (ofsm_table M f' k q)" by (simp add: card_mono) then have "(∑q∈FSM.states M - {q}. card (ofsm_table M f' (Suc k) q)) ≤ (∑q∈FSM.states M - {q}. card (ofsm_table M f' k q))" by (simp add: sum_mono) moreover have "card (ofsm_table M f' (Suc k) q) < card (ofsm_table M f' k q)" using ‹ofsm_table M f' k q ≠ ofsm_table M f' (Suc k) q› ‹ofsm_table M f' (Suc k) q ⊆ ofsm_table M f' k q› ‹finite (ofsm_table M f' k q)› by (metis psubsetI psubset_card_mono) ultimately have "(∑q∈FSM.states M. card (ofsm_table M (λq. f q ∩ states M) (Suc k) q)) < (∑q∈FSM.states M. card (ofsm_table M (λq. f q ∩ states M) k q))" unfolding f'[symmetric] * by linarith } note t = this show ?thesis apply (relation "measure (λ (M, f, k) . ∑ q ∈ states M . card (ofsm_table M (λq. f q ∩ states M) k q))") apply (simp del: h_obs.simps ofsm_table.simps)+ by (erule t) qed lemma ofsm_table_restriction_to_states : assumes "⋀ q . q ∈ states M ⟹ f q ⊆ states M" and "q ∈ states M" shows "ofsm_table M f k q = ofsm_table M (λq . f q ∩ states M) k q" using assms(2) proof (induction k arbitrary: q) case 0 then show ?case using assms(1) by auto next case (Suc k) have "⋀ x y q q' . (case h_obs M q x y of None ⇒ h_obs M q' x y = None | Some qT ⇒ (case h_obs M q' x y of None ⇒ False | Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT')) = (case h_obs M q x y of None ⇒ h_obs M q' x y = None | Some qT ⇒ (case h_obs M q' x y of None ⇒ False | Some qT' ⇒ ofsm_table M (λq . f q ∩ states M) k qT = ofsm_table M (λq . f q ∩ states M) k qT'))" (is "⋀ x y q q' . ?C1 x y q q' = ?C2 x y q q' ") proof - fix x y q q' show "?C1 x y q q' = ?C2 x y q q'" using Suc.IH[OF h_obs_state, of q x y] using Suc.IH[OF h_obs_state, of q' x y] by (cases "h_obs M q x y"; cases "h_obs M q' x y"; auto) qed then show ?case unfolding ofsm_table.simps Let_def Suc.IH[OF Suc.prems] by blast qed lemma ofsm_table_fix_length : assumes "⋀ q . q ∈ states M ⟹ f q ⊆ states M" obtains k where "⋀ q . q ∈ states M ⟹ ofsm_table_fix M f 0 q = ofsm_table M f k q" and "⋀ q k' . q ∈ states M ⟹ k' ≥ k ⟹ ofsm_table M f k' q = ofsm_table M f k q" proof - have "∃ k . ∀ q ∈ states M . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q" proof - have "∃ fp . ∀ q k' . q ∈ states M ⟶ k' ≥ (fp q) ⟶ ofsm_table M f k' q = ofsm_table M f (fp q) q" proof fix q let ?assignK = "λ q . SOME k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q" have "⋀ q k' . q ∈ states M ⟹ k' ≥ ?assignK q ⟹ ofsm_table M f k' q = ofsm_table M f (?assignK q) q" proof - fix q k' assume "q ∈ states M" and "k' ≥ ?assignK q" then have p1: "finite (ofsm_table M f 0 q)" using fsm_states_finite assms(1) using infinite_super by fastforce have "∃ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q" using finite_subset_mapping_limit[of "λ k . ofsm_table M f k q", OF p1 ofsm_table_subset] by metis have "∀ k' ≥ (?assignK q) . ofsm_table M f k' q = ofsm_table M f (?assignK q) q" using someI_ex[of "λ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q", OF ‹∃ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q›] by assumption then show "ofsm_table M f k' q = ofsm_table M f (?assignK q) q" using ‹k' ≥ ?assignK q› by blast qed then show "∀q k'. q ∈ states M ⟶ ?assignK q ≤ k' ⟶ ofsm_table M f k' q = ofsm_table M f (?assignK q) q" by blast qed then obtain assignK where assignK_prop: "⋀ q k' . q ∈ states M ⟹ k' ≥ assignK q ⟹ ofsm_table M f k' q = ofsm_table M f (assignK q) q" by blast have "finite (assignK ` states M)" by (simp add: fsm_states_finite) moreover have "assignK ` FSM.states M ≠ {}" using fsm_initial by auto ultimately obtain k where "k ∈ (assignK ` states M)" and "⋀ k' . k' ∈ (assignK ` states M) ⟹ k' ≤ k" using Max_elem[OF ‹finite (assignK ` states M)› ‹assignK ` FSM.states M ≠ {}›] by (meson eq_Max_iff) have "⋀ q k' . q ∈ states M ⟹ k' ≥ k ⟹ ofsm_table M f k' q = ofsm_table M f k q" proof - fix q k' assume "k' ≥ k" and "q ∈ states M" then have "k' ≥ assignK q" using ‹⋀ k' . k' ∈ (assignK ` states M) ⟹ k' ≤ k› using dual_order.trans by auto then show "ofsm_table M f k' q = ofsm_table M f k q" using assignK_prop ‹⋀k'. k' ∈ assignK ` FSM.states M ⟹ k' ≤ k› ‹q ∈ FSM.states M› by blast qed then show ?thesis by blast qed then obtain k where k_prop: "⋀ q k' . q ∈ states M ⟹ k' ≥ k ⟹ ofsm_table M f k' q = ofsm_table M f k q" by blast then have "⋀ q . q ∈ states M ⟹ ofsm_table M f k q = ofsm_table M f (Suc k) q" by (metis (full_types) le_SucI order_refl) let ?ks = "(Set.filter (λ k . ∀ q ∈ states M . ofsm_table M f k q = ofsm_table M f (Suc k) q) {..k})" have f1: "finite ?ks" by simp moreover have f2: "?ks ≠ {}" using ‹⋀ q . q ∈ states M ⟹ ofsm_table M f k q = ofsm_table M f (Suc k) q› unfolding Set.filter_def by blast ultimately obtain kMin where "kMin ∈ ?ks" and "⋀ k' . k' ∈ ?ks ⟹ k' ≥ kMin" using Min_elem[OF f1 f2] by (meson eq_Min_iff) have k1: "⋀ q . q ∈ states M ⟹ ofsm_table M f (Suc kMin) q = ofsm_table M f kMin q" using ‹kMin ∈ ?ks› by (metis (mono_tags, lifting) member_filter) have k2: "⋀ k' . (⋀ q . q ∈ states M ⟹ ofsm_table M f k' q = ofsm_table M f (Suc k') q) ⟹ k' ≥ kMin" proof - fix k' assume "⋀ q . q ∈ states M ⟹ ofsm_table M f k' q = ofsm_table M f (Suc k') q" show "k' ≥ kMin" proof (cases "k' ∈ ?ks") case True then show ?thesis using ‹⋀ k' . k' ∈ ?ks ⟹ k' ≥ kMin› by blast next case False then have "k' > k" using ‹⋀ q . q ∈ states M ⟹ ofsm_table M f k' q = ofsm_table M f (Suc k') q› unfolding member_filter atMost_iff by (meson not_less) moreover have "kMin ≤ k" using ‹kMin ∈ ?ks› by auto ultimately show ?thesis by auto qed qed have "⋀ q . q ∈ states M ⟹ ofsm_table_fix M f 0 q = ofsm_table M (λ q . f q ∩ states M) kMin q" proof - fix q assume "q ∈ states M" show "ofsm_table_fix M f 0 q = ofsm_table M (λ q . f q ∩ states M) kMin q" proof (cases kMin) case 0 have "∀q∈FSM.states M. ofsm_table M (λq. f q ∩ FSM.states M) 0 q = ofsm_table M (λq. f q ∩ FSM.states M) (Suc 0) q" using k1 using ofsm_table_restriction_to_states[of M f _, OF assms(1) _ ] using "0" by blast then show ?thesis apply (subst ofsm_table_fix.simps) unfolding "0" Let_def by force next case (Suc kMin') have *: "⋀ i . i < kMin ⟹ ¬(∀ q ∈ states M . ofsm_table M f i q = ofsm_table M f (Suc i) q)" using k2 by (meson leD) have "⋀ i . i < kMin ⟹ ofsm_table_fix M f 0 = ofsm_table_fix M f (Suc i)" proof - fix i assume "i < kMin" then show "ofsm_table_fix M f 0 = ofsm_table_fix M f (Suc i)" proof (induction i) case 0 show ?case using *[OF 0] ofsm_table_restriction_to_states[of _ f, OF assms(1) _ ] unfolding ofsm_table_fix.simps[of M f 0] Let_def by (metis (no_types, lifting)) next case (Suc i) then have "i < kMin" by auto have "ofsm_table_fix M f (Suc i) = ofsm_table_fix M f (Suc (Suc i))" using *[OF ‹Suc i < kMin›] ofsm_table_restriction_to_states[of _ f, OF assms(1) _ ] unfolding ofsm_table_fix.simps[of M f "Suc i"] Let_def by metis then show ?case using Suc.IH[OF ‹i < kMin›] by presburger qed qed then have "ofsm_table_fix M f 0 = ofsm_table_fix M f kMin" using Suc by blast moreover have "ofsm_table_fix M f kMin q = ofsm_table M f kMin q" proof - have "∀q∈FSM.states M. ofsm_table M (λq. f q ∩ FSM.states M) kMin q = ofsm_table M (λq. f q ∩ FSM.states M) (Suc kMin) q" using ofsm_table_restriction_to_states[of _ f, OF assms(1) _ ] using k1 by blast then show ?thesis using ofsm_table_restriction_to_states[of _ f, OF assms(1) _ ] ‹q ∈ states M› unfolding ofsm_table_fix.simps[of M f kMin] Let_def by presburger qed ultimately show ?thesis using ofsm_table_restriction_to_states[of _ f, OF assms(1) ‹q ∈ states M›] by presburger qed qed moreover have "⋀ q k' . q ∈ states M ⟹ k' ≥ kMin ⟹ ofsm_table M f k' q = ofsm_table M f kMin q" using ofsm_table_fixpoint[OF _ k1 ] by blast ultimately show ?thesis using that[of kMin] using ofsm_table_restriction_to_states[of M f, OF assms(1) _ ] by blast qed lemma ofsm_table_containment : assumes "q ∈ states M" and "⋀ q . q ∈ states M ⟹ q ∈ f q" shows "q ∈ ofsm_table M f k q" proof (induction k) case 0 then show ?case using assms by auto next case (Suc k) then show ?case unfolding ofsm_table.simps Let_def option.case_eq_if by auto qed lemma ofsm_table_states : assumes "⋀ q . q ∈ states M ⟹ f q ⊆ states M" and "q ∈ states M" shows "ofsm_table M f k q ⊆ states M" proof - have "ofsm_table M f k q ⊆ ofsm_table M f 0 q" using ofsm_table_subset[OF le0] by metis moreover have "ofsm_table M f 0 q ⊆ states M" using assms unfolding ofsm_table.simps(1) by (metis (full_types)) ultimately show ?thesis by blast qed subsubsection ‹Properties of Initial Partitions› definition equivalence_relation_on_states :: "('a,'b,'c) fsm ⇒ ('a ⇒ 'a set) ⇒ bool" where "equivalence_relation_on_states M f = (equiv (states M) {(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ f q1} ∧ (∀ q ∈ states M . f q ⊆ states M))" lemma equivalence_relation_on_states_refl : assumes "equivalence_relation_on_states M f" and "q ∈ states M" shows "q ∈ f q" using assms unfolding equivalence_relation_on_states_def equiv_def refl_on_def by blast lemma equivalence_relation_on_states_sym : assumes "equivalence_relation_on_states M f" and "q1 ∈ states M" and "q2 ∈ f q1" shows "q1 ∈ f q2" using assms unfolding equivalence_relation_on_states_def equiv_def sym_def by blast lemma equivalence_relation_on_states_trans : assumes "equivalence_relation_on_states M f" and "q1 ∈ states M" and "q2 ∈ f q1" and "q3 ∈ f q2" shows "q3 ∈ f q1" proof - have "(q1,q2) ∈ {(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ f q1}" using assms(2,3) by blast then have "q2 ∈ states M" using assms(1) unfolding equivalence_relation_on_states_def by auto then have "(q2,q3) ∈ {(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ f q1}" using assms(4) by blast moreover have "trans {(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ f q1}" using assms(1) unfolding equivalence_relation_on_states_def equiv_def by auto ultimately show ?thesis using ‹(q1,q2) ∈ {(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ f q1}› unfolding trans_def by blast qed lemma equivalence_relation_on_states_ran : assumes "equivalence_relation_on_states M f" and "q ∈ states M" shows "f q ⊆ states M" using assms unfolding equivalence_relation_on_states_def by blast subsubsection ‹Properties of OFSM tables for initial partitions based on equivalence relations› lemma h_obs_io : assumes "h_obs M q x y = Some q'" shows "x ∈ inputs M" and "y ∈ outputs M" proof - have "snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x)) ≠ {}" using assms unfolding h_obs_simps Let_def by auto then show "x ∈ inputs M" and "y ∈ outputs M" unfolding h_simps using fsm_transition_input fsm_transition_output by fastforce+ qed lemma ofsm_table_language : assumes "q' ∈ ofsm_table M f k q" and "length io ≤ k" and "q ∈ states M" and "equivalence_relation_on_states M f" shows "is_in_language M q io ⟷ is_in_language M q' io" and "is_in_language M q io ⟹ (after M q' io) ∈ f (after M q io)" proof - have "(is_in_language M q io ⟷ is_in_language M q' io) ∧ (is_in_language M q io ⟶ (after M q' io) ∈ f (after M q io))" using assms(1,2,3) proof (induction k arbitrary: q q' io) case 0 then have "io = []" by auto then show ?case using "0.prems"(1,3) by auto next case (Suc k) show ?case proof (cases "length io ≤ k") case True have *: "q' ∈ ofsm_table M f k q" using ‹q' ∈ ofsm_table M f (Suc k) q› ofsm_table_subset by (metis (full_types) le_SucI order_refl subsetD) show ?thesis using Suc.IH[OF * True ‹q ∈ states M›] by assumption next case False then have "length io = Suc k" using ‹length io ≤ Suc k› by auto then obtain ioT ioP where "io = ioT#ioP" by (meson length_Suc_conv) then have "length ioP ≤ k" using ‹length io ≤ Suc k› by auto obtain x y where "io = (x,y)#ioP" using ‹io = ioT#ioP› prod.exhaust_sel by fastforce have "ofsm_table M f (Suc k) q = {q' ∈ ofsm_table M f k q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) }" unfolding ofsm_table.simps Let_def by blast then have "q' ∈ ofsm_table M f k q" and *: "⋀ x y . x ∈ inputs M ⟹ y ∈ outputs M ⟹ (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" using ‹q' ∈ ofsm_table M f (Suc k) q› by blast+ show ?thesis unfolding ‹io = (x,y)#ioP› proof - have "is_in_language M q ((x,y)#ioP) ⟹ is_in_language M q' ((x,y)#ioP) ∧ after M q' ((x,y)#ioP) ∈ f (after M q ((x,y)#ioP))" proof - assume "is_in_language M q ((x,y)#ioP)" then obtain qT where "h_obs M q x y = Some qT" and "is_in_language M qT ioP" by (metis case_optionE is_in_language.simps(2)) moreover have "(case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" using *[of x y, OF h_obs_io[OF ‹h_obs M q x y = Some qT›]] . ultimately obtain qT' where "h_obs M q' x y = Some qT'" and "ofsm_table M f k qT = ofsm_table M f k qT'" using ofsm_table_case_helper[of M q' x y f k q] unfolding ofsm_table.simps by force then have "qT' ∈ ofsm_table M f k qT" using ofsm_table_containment[OF h_obs_state equivalence_relation_on_states_refl[OF ‹equivalence_relation_on_states M f›]] by metis have "(is_in_language M qT ioP) = (is_in_language M qT' ioP)" "(is_in_language M qT ioP ⟶ after M qT' ioP ∈ f (after M qT ioP))" using Suc.IH[OF ‹qT' ∈ ofsm_table M f k qT› ‹length ioP ≤ k› h_obs_state[OF ‹h_obs M q x y = Some qT›]] by blast+ have "(is_in_language M qT' ioP)" using ‹(is_in_language M qT ioP) = (is_in_language M qT' ioP)› ‹is_in_language M qT ioP› by auto then have "is_in_language M q' ((x,y)#ioP)" unfolding is_in_language.simps ‹h_obs M q' x y = Some qT'› by auto moreover have "after M q' ((x,y)#ioP) ∈ f (after M q ((x,y)#ioP))" unfolding after.simps ‹h_obs M q' x y = Some qT'› ‹h_obs M q x y = Some qT› using ‹(is_in_language M qT ioP ⟶ after M qT' ioP ∈ f (after M qT ioP))› ‹is_in_language M qT ioP› by auto ultimately show "is_in_language M q' ((x,y)#ioP) ∧ after M q' ((x,y)#ioP) ∈ f (after M q ((x,y)#ioP))" by blast qed moreover have "is_in_language M q' ((x,y)#ioP) ⟹ is_in_language M q ((x,y)#ioP)" proof - assume "is_in_language M q' ((x,y)#ioP)" then obtain qT' where "h_obs M q' x y = Some qT'" and "is_in_language M qT' ioP" by (metis case_optionE is_in_language.simps(2)) moreover have "(case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" using *[of x y, OF h_obs_io[OF ‹h_obs M q' x y = Some qT'›]] . ultimately obtain qT where "h_obs M q x y = Some qT" and "ofsm_table M f k qT = ofsm_table M f k qT'" using ofsm_table_case_helper[of M q' x y f k q] unfolding ofsm_table.simps by force then have "qT ∈ ofsm_table M f k qT'" using ofsm_table_containment[OF h_obs_state equivalence_relation_on_states_refl[OF ‹equivalence_relation_on_states M f›]] by metis have "(is_in_language M qT ioP) = (is_in_language M qT' ioP)" using Suc.IH[OF ‹qT ∈ ofsm_table M f k qT'› ‹length ioP ≤ k› h_obs_state[OF ‹h_obs M q' x y = Some qT'›]] by blast then have "is_in_language M qT ioP" using ‹is_in_language M qT' ioP› by auto then show "is_in_language M q ((x,y)#ioP)" unfolding is_in_language.simps ‹h_obs M q x y = Some qT› by auto qed ultimately show "is_in_language M q ((x, y) # ioP) = is_in_language M q' ((x, y) # ioP) ∧ (is_in_language M q ((x, y) # ioP) ⟶ after M q' ((x, y) # ioP) ∈ f (after M q ((x, y) # ioP)))" by blast qed qed qed then show "is_in_language M q io = is_in_language M q' io" and "(is_in_language M q io ⟹ after M q' io ∈ f (after M q io))" by blast+ qed lemma after_is_state_is_in_language : assumes "q ∈ states M" and "is_in_language M q io" shows "FSM.after M q io ∈ states M" using assms proof (induction io arbitrary: q) case Nil then show ?case by auto next case (Cons a io) then obtain x y where "a = (x,y)" using prod.exhaust by metis show ?case using ‹is_in_language M q (a # io)› Cons.IH[OF h_obs_state[of M q x y]] unfolding ‹a = (x,y)› unfolding after.simps is_in_language.simps by (metis option.case_eq_if option.exhaust_sel) qed lemma ofsm_table_elem : assumes "q ∈ states M" and "q' ∈ states M" and "equivalence_relation_on_states M f" and "⋀ io . length io ≤ k ⟹ is_in_language M q io ⟷ is_in_language M q' io" and "⋀ io . length io ≤ k ⟹ is_in_language M q io ⟹ (after M q' io) ∈ f (after M q io)" shows "q' ∈ ofsm_table M f k q" using assms(1,2,4,5) proof (induction k arbitrary: q q') case 0 then show ?case by auto next case (Suc k) have "q' ∈ ofsm_table M f k q" using Suc.IH[OF Suc.prems(1,2)] Suc.prems(3,4) by auto moreover have "⋀ x y . x ∈ inputs M ⟹ y ∈ outputs M ⟹ (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" proof - fix x y assume "x ∈ inputs M" and "y ∈ outputs M" show "(case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" proof (cases "∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT'") case True then obtain qT qT' where "h_obs M q x y = Some qT" and "h_obs M q' x y = Some qT'" by blast have *: "⋀ io . length io ≤ k ⟹ is_in_language M qT io = is_in_language M qT' io" proof - fix io :: "('b × 'c) list " assume "length io ≤ k" have "is_in_language M qT io = is_in_language M q ([(x,y)]@io)" using ‹h_obs M q x y = Some qT› by auto moreover have "is_in_language M qT' io = is_in_language M q' ([(x,y)]@io)" using ‹h_obs M q' x y = Some qT'› by auto ultimately show "is_in_language M qT io = is_in_language M qT' io" using Suc.prems(3) ‹length io ≤ k› by (metis append.left_neutral append_Cons length_Cons not_less_eq_eq) qed have "ofsm_table M f k qT = ofsm_table M f k qT'" proof have "qT ∈ states M" using h_obs_state[OF ‹h_obs M q x y = Some qT›] . have "qT' ∈ states M" using h_obs_state[OF ‹h_obs M q' x y = Some qT'›] . show "ofsm_table M f k qT ⊆ ofsm_table M f k qT'" proof fix s assume "s ∈ ofsm_table M f k qT" then have "s ∈ states M" using ofsm_table_subset[of 0 k M f qT] equivalence_relation_on_states_ran[OF assms(3) ‹qT ∈ states M›] ‹qT ∈ states M› by auto have **: "(⋀io. length io ≤ k ⟹ is_in_language M qT' io = is_in_language M s io)" using ofsm_table_language(1)[OF ‹s ∈ ofsm_table M f k qT› _ ‹qT∈ states M› assms(3)] * by blast have ***: "(⋀io. length io ≤ k ⟹ is_in_language M qT' io ⟹ after M s io ∈ f (after M qT' io))" proof - fix io assume "length io ≤ k" and "is_in_language M qT' io" then have "is_in_language M qT io" using * by blast then have "after M s io ∈ f (after M qT io)" using ofsm_table_language(2)[OF ‹s ∈ ofsm_table M f k qT› ‹length io ≤ k› ‹qT∈ states M› assms(3)] by blast have "after M qT io = after M q ((x,y)#io)" using ‹h_obs M q x y = Some qT› by auto moreover have "after M qT' io = after M q' ((x,y)#io)" using ‹h_obs M q' x y = Some qT'› by auto moreover have "is_in_language M q ((x,y)#io)" using ‹h_obs M q x y = Some qT› ‹is_in_language M qT io› by auto ultimately have "after M qT' io ∈ f (after M qT io)" using Suc.prems(4) ‹length io ≤ k› by (metis Suc_le_mono length_Cons) show "after M s io ∈ f (after M qT' io)" using equivalence_relation_on_states_trans[OF ‹equivalence_relation_on_states M f› after_is_state_is_in_language[OF ‹qT' ∈ states M› ‹is_in_language M qT' io›] equivalence_relation_on_states_sym[OF ‹equivalence_relation_on_states M f› after_is_state_is_in_language[OF ‹qT ∈ states M› ‹is_in_language M qT io›] ‹after M qT' io ∈ f (after M qT io)›] ‹after M s io ∈ f (after M qT io)›] . qed show "s ∈ ofsm_table M f k qT'" using Suc.IH[OF ‹qT' ∈ states M› ‹s ∈ states M› ** ***] by blast qed show "ofsm_table M f k qT' ⊆ ofsm_table M f k qT" proof fix s assume "s ∈ ofsm_table M f k qT'" then have "s ∈ states M" using ofsm_table_subset[of 0 k M f qT'] equivalence_relation_on_states_ran[OF assms(3) ‹qT' ∈ states M›] ‹qT' ∈ states M› by auto have **: "(⋀io. length io ≤ k ⟹ is_in_language M qT io = is_in_language M s io)" using ofsm_table_language(1)[OF ‹s ∈ ofsm_table M f k qT'› _ ‹qT'∈ states M› assms(3)] * by blast have ***: "(⋀io. length io ≤ k ⟹ is_in_language M qT io ⟹ after M s io ∈ f (after M qT io))" proof - fix io assume "length io ≤ k" and "is_in_language M qT io" then have "is_in_language M qT' io" using * by blast then have "after M s io ∈ f (after M qT' io)" using ofsm_table_language(2)[OF ‹s ∈ ofsm_table M f k qT'› ‹length io ≤ k› ‹qT'∈ states M› assms(3)] by blast have "after M qT' io = after M q' ((x,y)#io)" using ‹h_obs M q' x y = Some qT'› by auto moreover have "after M qT io = after M q ((x,y)#io)" using ‹h_obs M q x y = Some qT› by auto moreover have "is_in_language M q' ((x,y)#io)" using ‹h_obs M q' x y = Some qT'› ‹is_in_language M qT' io› by auto ultimately have "after M qT io ∈ f (after M qT' io)" using Suc.prems(4) ‹length io ≤ k› by (metis Suc.prems(3) Suc_le_mono ‹is_in_language M qT io› ‹qT ∈ FSM.states M› after_is_state_is_in_language assms(3) equivalence_relation_on_states_sym length_Cons) show "after M s io ∈ f (after M qT io)" using equivalence_relation_on_states_trans[OF ‹equivalence_relation_on_states M f› after_is_state_is_in_language[OF ‹qT ∈ states M› ‹is_in_language M qT io›] equivalence_relation_on_states_sym[OF ‹equivalence_relation_on_states M f› after_is_state_is_in_language[OF ‹qT' ∈ states M› ‹is_in_language M qT' io›] ‹after M qT io ∈ f (after M qT' io)›] ‹after M s io ∈ f (after M qT' io)›] . qed show "s ∈ ofsm_table M f k qT" using Suc.IH[OF ‹qT ∈ states M› ‹s ∈ states M› ** ***] by blast qed qed then show ?thesis unfolding ‹h_obs M q x y = Some qT› ‹h_obs M q' x y = Some qT'› by auto next case False have "h_obs M q x y = None ∧ h_obs M q' x y = None" proof (rule ccontr) assume "¬ (h_obs M q x y = None ∧ h_obs M q' x y = None)" then have "is_in_language M q [(x,y)] ∨ is_in_language M q' [(x,y)]" unfolding is_in_language.simps using option.disc_eq_case(2) by blast moreover have "is_in_language M q [(x,y)] ≠ is_in_language M q' [(x,y)]" using False by (metis calculation case_optionE is_in_language.simps(2)) moreover have "length [(x,y)] ≤ Suc k" by auto ultimately show False using Suc.prems(3) by blast qed then show ?thesis unfolding ofsm_table_case_helper by blast qed qed ultimately show ?case unfolding Suc ofsm_table.simps Let_def by force qed lemma ofsm_table_set : assumes "q ∈ states M" and "equivalence_relation_on_states M f" shows "ofsm_table M f k q = {q' . q' ∈ states M ∧ (∀ io . length io ≤ k ⟶ (is_in_language M q io ⟷ is_in_language M q' io) ∧ (is_in_language M q io ⟶ after M q' io ∈ f (after M q io)))}" using ofsm_table_language[OF _ _ assms(1,2) ] ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(2)] assms(1)] ofsm_table_elem[OF assms(1) _ assms(2)] by blast lemma ofsm_table_set_observable : assumes "observable M" and "q ∈ states M" and "equivalence_relation_on_states M f" shows "ofsm_table M f k q = {q' . q' ∈ states M ∧ (∀ io . length io ≤ k ⟶ (io ∈ LS M q ⟷ io ∈ LS M q') ∧ (io ∈ LS M q ⟶ after M q' io ∈ f (after M q io)))}" unfolding ofsm_table_set[OF assms(2,3)] unfolding is_in_language_iff[OF assms(1,2)] using is_in_language_iff[OF assms(1)] by blast lemma ofsm_table_eq_if_elem : assumes "q1 ∈ states M" and "q2 ∈ states M" and "equivalence_relation_on_states M f" shows "(ofsm_table M f k q1 = ofsm_table M f k q2) = (q2 ∈ ofsm_table M f k q1)" proof show "ofsm_table M f k q1 = ofsm_table M f k q2 ⟹ q2 ∈ ofsm_table M f k q1" using ofsm_table_containment[OF assms(2) equivalence_relation_on_states_refl[OF ‹equivalence_relation_on_states M f›]] by blast show "q2 ∈ ofsm_table M f k q1 ⟹ ofsm_table M f k q1 = ofsm_table M f k q2" proof - assume *: "q2 ∈ ofsm_table M f k q1" have "ofsm_table M f k q1 = {q' ∈ FSM.states M. ∀io. length io ≤ k ⟶ (is_in_language M q1 io) = (is_in_language M q' io) ∧ (is_in_language M q1 io ⟶ after M q' io ∈ f (after M q1 io))}" using ofsm_table_set[OF assms(1,3)] by auto moreover have "ofsm_table M f k q2 = {q' ∈ FSM.states M. ∀io. length io ≤ k ⟶ (is_in_language M q1 io) = (is_in_language M q' io) ∧ (is_in_language M q1 io ⟶ after M q' io ∈ f (after M q1 io))}" proof - have "ofsm_table M f k q2 = {q' ∈ FSM.states M. ∀io. length io ≤ k ⟶ (is_in_language M q2 io) = (is_in_language M q' io) ∧ (is_in_language M q2 io ⟶ after M q' io ∈ f (after M q2 io))}" using ofsm_table_set[OF assms(2,3)] by auto moreover have "⋀ io . length io ≤ k ⟹ (is_in_language M q1 io) = (is_in_language M q2 io)" using ofsm_table_language(1)[OF * _ assms(1,3)] by blast moreover have "⋀ io q' . q' ∈ states M ⟹ length io ≤ k ⟹ (is_in_language M q2 io ⟶ after M q' io ∈ f (after M q2 io)) = (is_in_language M q1 io ⟶ after M q' io ∈ f (after M q1 io))" using ofsm_table_language(2)[OF * _ assms(1,3)] by (meson after_is_state_is_in_language assms(1) assms(2) assms(3) calculation(2) equivalence_relation_on_states_sym equivalence_relation_on_states_trans) ultimately show ?thesis by blast qed ultimately show ?thesis by blast qed qed lemma ofsm_table_fix_language : fixes M :: "('a,'b,'c) fsm" assumes "q' ∈ ofsm_table_fix M f 0 q" and "q ∈ states M" and "observable M" and "equivalence_relation_on_states M f" shows "LS M q = LS M q'" and "io ∈ LS M q ⟹ after M q' io ∈ f (after M q io)" proof - obtain k where *:"⋀ q . q ∈ states M ⟹ ofsm_table_fix M f 0 q = ofsm_table M f k q" and **: "⋀ q k' . q ∈ states M ⟹ k' ≥ k ⟹ ofsm_table M f k' q = ofsm_table M f k q" using ofsm_table_fix_length[of M f,OF equivalence_relation_on_states_ran[OF assms(4)]] by blast have "q' ∈ ofsm_table M f k q" using * assms(1,2) by blast then have "q' ∈ states M" by (metis assms(2) assms(4) equivalence_relation_on_states_ran le0 ofsm_table.simps(1) ofsm_table_subset subset_iff) have "⋀ k' . q' ∈ ofsm_table M f k' q" proof - fix k' show "q' ∈ ofsm_table M f k' q" proof (cases "k' ≤ k") case True show ?thesis using ofsm_table_subset[OF True, of M f q] ‹q' ∈ ofsm_table M f k q› by blast next case False then have "k ≤ k'" by auto show ?thesis unfolding **[OF assms(2) ‹k ≤ k'›] using ‹q' ∈ ofsm_table M f k q› by assumption qed qed have "⋀ io . io ∈ LS M q ⟷ io ∈ LS M q'" proof - fix io :: "('b × 'c) list" show "io ∈ LS M q ⟷ io ∈ LS M q'" using ofsm_table_language(1)[OF ‹q' ∈ ofsm_table M f (length io) q› _ assms(2,4), of io] using is_in_language_iff[OF assms(3,2)] is_in_language_iff[OF assms(3) ‹q' ∈ states M›] by blast qed then show "LS M q = LS M q'" by blast show "io ∈ LS M q ⟹ after M q' io ∈ f (after M q io)" using ofsm_table_language(2)[OF ‹q' ∈ ofsm_table M f (length io) q› _ assms(2,4), of io] using is_in_language_iff[OF assms(3,2)] is_in_language_iff[OF assms(3) ‹q' ∈ states M›] by blast qed lemma ofsm_table_same_language : assumes "LS M q = LS M q'" and "⋀ io . io ∈ LS M q ⟹ after M q' io ∈ f (after M q io)" and "observable M" and "q' ∈ states M" and "q ∈ states M" and "equivalence_relation_on_states M f" shows "ofsm_table M f k q = ofsm_table M f k q'" using assms(1,2,4,5) proof (induction k arbitrary: q q') case 0 then show ?case by (metis after.simps(1) assms(6) from_FSM_language language_contains_empty_sequence ofsm_table.simps(1) ofsm_table_eq_if_elem) next case (Suc k) have "ofsm_table M f (Suc k) q = {q'' ∈ ofsm_table M f k q' . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) }" using Suc.IH[OF Suc.prems] unfolding ofsm_table.simps Suc Let_def Suc by simp moreover have "ofsm_table M f (Suc k) q' = {q'' ∈ ofsm_table M f k q' . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q' x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) }" unfolding ofsm_table.simps Suc Let_def by auto moreover have "{q'' ∈ ofsm_table M f k q' . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) } = {q'' ∈ ofsm_table M f k q' . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q' x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) }" proof - have "⋀ q'' x y . q'' ∈ ofsm_table M f k q' ⟹ x ∈ inputs M ⟹ y ∈ outputs M ⟹ (case h_obs M q x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) = (case h_obs M q' x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None)" proof - fix q'' x y assume "q'' ∈ ofsm_table M f k q'" and "x ∈ inputs M" and "y ∈ outputs M" have *:"(∃ qT . h_obs M q x y = Some qT) = (∃ qT' . h_obs M q' x y = Some qT')" proof - have "([(x,y)] ∈ LS M q) = ([(x,y)] ∈ LS M q')" using ‹LS M q = LS M q'› by auto then have "(∃ qT . (q, x, y, qT) ∈ FSM.transitions M) = (∃ qT' . (q', x, y, qT') ∈ FSM.transitions M)" unfolding LS_single_transition by force then show "(∃ qT . h_obs M q x y = Some qT) = (∃ qT' . h_obs M q' x y = Some qT')" unfolding h_obs_Some[OF ‹observable M›] using ‹observable M› unfolding observable_alt_def by blast qed have **: "(case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None)" proof (cases "h_obs M q x y") case None then show ?thesis using * by auto next case (Some qT) show ?thesis proof (cases "h_obs M q' x y") case None then show ?thesis using * by auto next case (Some qT') have "(q,x,y,qT) ∈ transitions M" using ‹h_obs M q x y = Some qT› unfolding h_obs_Some[OF ‹observable M›] by blast have "(q',x,y,qT') ∈ transitions M" using ‹h_obs M q' x y = Some qT'› unfolding h_obs_Some[OF ‹observable M›] by blast have "LS M qT = LS M qT'" using observable_transition_target_language_eq[OF _ ‹(q,x,y,qT) ∈ transitions M› ‹(q',x,y,qT') ∈ transitions M› _ _ ‹observable M›] ‹LS M q = LS M q'› by auto moreover have "(⋀io. io ∈ LS M qT ⟹ after M qT' io ∈ f (after M qT io))" proof - fix io assume "io ∈ LS M qT" have "io ∈ LS M qT'" using ‹io ∈ LS M qT› calculation by auto have "after M qT io = after M q ((x,y)#io)" using after_h_obs_prepend[OF ‹observable M› ‹h_obs M q x y = Some qT› ‹io ∈ LS M qT›] by simp moreover have "after M qT' io = after M q' ((x,y)#io)" using after_h_obs_prepend[OF ‹observable M› ‹h_obs M q' x y = Some qT'› ‹io ∈ LS M qT'›] by simp moreover have "(x,y)#io ∈ LS M q" using ‹h_obs M q x y = Some qT› ‹io ∈ LS M qT› unfolding h_obs_language_iff[OF ‹observable M›] by blast ultimately show "after M qT' io ∈ f (after M qT io)" using Suc.prems(2) by presburger qed ultimately have "ofsm_table M f k qT = ofsm_table M f k qT'" using Suc.IH[OF _ _ fsm_transition_target[OF ‹(q',x,y,qT') ∈ transitions M›] fsm_transition_target[OF ‹(q,x,y,qT) ∈ transitions M›]] unfolding snd_conv by blast then show ?thesis using ‹h_obs M q x y = Some qT› ‹h_obs M q' x y = Some qT'› by auto qed qed show "(case h_obs M q x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None) = (case h_obs M q' x y of Some qT ⇒ (case h_obs M q'' x y of Some qT' ⇒ ofsm_table M f k qT = ofsm_table M f k qT' | None ⇒ False) | None ⇒ h_obs M q'' x y = None)" (is "?P") proof (cases "h_obs M q x y") case None then have "h_obs M q' x y = None" using * by auto show ?thesis unfolding None ‹h_obs M q' x y = None› by auto next case (Some qT) then obtain qT' where "h_obs M q' x y = Some qT'" using ‹(∃ qT . h_obs M q x y = Some qT) = (∃ qT' . h_obs M q' x y = Some qT')› by auto show ?thesis proof (cases "h_obs M q'' x y") case None then show ?thesis using * by (metis Some option.case_eq_if option.simps(5)) next case (Some qT'') show ?thesis using ** unfolding Some ‹h_obs M q x y = Some qT› ‹h_obs M q' x y = Some qT'› by auto qed qed qed then show ?thesis by blast qed ultimately show ?case by blast qed lemma ofsm_table_fix_set : assumes "q ∈ states M" and "observable M" and "equivalence_relation_on_states M f" shows "ofsm_table_fix M f 0 q = {q' ∈ states M . LS M q' = LS M q ∧ (∀ io ∈ LS M q . after M q' io ∈ f (after M q io))}" proof have "ofsm_table_fix M f 0 q ⊆ ofsm_table M f 0 q" using ofsm_table_fix_length[of M f] ofsm_table_subset[OF zero_le, of M f _ q] by (metis assms(1) assms(3) equivalence_relation_on_states_ran) then have "ofsm_table_fix M f 0 q ⊆ states M" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(3)] assms(1)] by blast then show "ofsm_table_fix M f 0 q ⊆ {q' ∈ states M . LS M q' = LS M q ∧ (∀ io ∈ LS M q . after M q' io ∈ f (after M q io))}" using ofsm_table_fix_language[OF _ assms] by blast show "{q' ∈ states M . LS M q' = LS M q ∧ (∀ io ∈ LS M q . after M q' io ∈ f (after M q io))} ⊆ ofsm_table_fix M f 0 q" proof fix q' assume "q' ∈ {q' ∈ states M . LS M q' = LS M q ∧ (∀ io ∈ LS M q . after M q' io ∈ f (after M q io))}" then have "q' ∈ states M" and "LS M q' = LS M q" and "⋀ io . io ∈ LS M q ⟹ after M q' io ∈ f (after M q io)" by blast+ then have "⋀ io . io ∈ LS M q' ⟹ after M q io ∈ f (after M q' io)" by (metis after_is_state assms(2) assms(3) equivalence_relation_on_states_sym) obtain k where "⋀ q . q ∈ states M ⟹ ofsm_table_fix M f 0 q = ofsm_table M f k q" and "⋀ q k' . q ∈ states M ⟹ k' ≥ k ⟹ ofsm_table M f k' q = ofsm_table M f k q" using ofsm_table_fix_length[of M f, OF equivalence_relation_on_states_ran[OF assms(3)]] by blast have "ofsm_table M f k q' = ofsm_table M f k q" using ofsm_table_same_language[OF ‹LS M q' = LS M q› ‹⋀ io . io ∈ LS M q' ⟹ after M q io ∈ f (after M q' io)› assms(2,1) ‹q' ∈ states M› assms(3)] by blast then show "q' ∈ ofsm_table_fix M f 0 q" using ofsm_table_containment[OF ‹q' ∈ states M›, of f k] using ‹⋀ q . q ∈ states M ⟹ ofsm_table_fix M f 0 q = ofsm_table M f k q› by (metis assms(1) assms(3) equivalence_relation_on_states_refl) qed qed lemma ofsm_table_fix_eq_if_elem : assumes "q1 ∈ states M" and "q2 ∈ states M" and "equivalence_relation_on_states M f" shows "(ofsm_table_fix M f 0 q1 = ofsm_table_fix M f 0 q2) = (q2 ∈ ofsm_table_fix M f 0 q1)" proof have "(⋀q. q ∈ FSM.states M ⟹ q ∈ f q)" using assms(3) by (meson equivalence_relation_on_states_refl) show "ofsm_table_fix M f 0 q1 = ofsm_table_fix M f 0 q2 ⟹ q2 ∈ ofsm_table_fix M f 0 q1" using ofsm_table_containment[of _ M f, OF assms(2) ‹(⋀q. q ∈ FSM.states M ⟹ q ∈ f q)›] using ofsm_table_fix_length[of M f] by (metis assms(2) assms(3) equivalence_relation_on_states_ran) show "q2 ∈ ofsm_table_fix M f 0 q1 ⟹ ofsm_table_fix M f 0 q1 = ofsm_table_fix M f 0 q2" using ofsm_table_eq_if_elem[OF assms(1,2,3)] using ofsm_table_fix_length[of M f] by (metis assms(1) assms(2) assms(3) equivalence_relation_on_states_ran) qed lemma ofsm_table_refinement_disjoint : assumes "q1 ∈ states M" and "q2 ∈ states M" and "equivalence_relation_on_states M f" and "ofsm_table M f k q1 ≠ ofsm_table M f k q2" shows "ofsm_table M f (Suc k) q1 ≠ ofsm_table M f (Suc k) q2" proof - have "ofsm_table M f (Suc k) q1 ⊆ ofsm_table M f k q1" and "ofsm_table M f (Suc k) q2 ⊆ ofsm_table M f k q2" using ofsm_table_subset[of k "Suc k" M f] by fastforce+ moreover have "ofsm_table M f k q1 ∩ ofsm_table M f k q2 = {}" proof (rule ccontr) assume "ofsm_table M f k q1 ∩ ofsm_table M f k q2 ≠ {}" then obtain q where "q ∈ ofsm_table M f k q1" and "q ∈ ofsm_table M f k q2" by blast then have "q ∈ states M" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(3)] assms(1)] by blast have "ofsm_table M f k q1 = ofsm_table M f k q2" using ‹q ∈ ofsm_table M f k q1› ‹q ∈ ofsm_table M f k q2› unfolding ofsm_table_eq_if_elem[OF assms(1) ‹q ∈ states M› assms(3), symmetric] unfolding ofsm_table_eq_if_elem[OF assms(2) ‹q ∈ states M› assms(3), symmetric] by blast then show False using assms(4) by simp qed ultimately show ?thesis by (metis Int_subset_iff all_not_in_conv assms(2) assms(3) ofsm_table_eq_if_elem subset_empty) qed lemma ofsm_table_partition_finite : assumes "equivalence_relation_on_states M f" shows "finite (ofsm_table M f k ` states M)" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms]] fsm_states_finite[of M] unfolding finite_Pow_iff[of "states M", symmetric] by simp lemma ofsm_table_refinement_card : assumes "equivalence_relation_on_states M f" and "A ⊆ states M" and "i ≤ j" shows "card (ofsm_table M f j ` A) ≥ card (ofsm_table M f i ` A)" proof - have "⋀ k . card (ofsm_table M f (Suc k) ` A) ≥ card (ofsm_table M f k ` A)" proof - fix k show "card (ofsm_table M f (Suc k) ` A) ≥ card (ofsm_table M f k ` A)" proof (rule ccontr) have "finite A" using fsm_states_finite[of M] assms(2) using finite_subset by blast assume "¬ card (ofsm_table M f k ` A) ≤ card (ofsm_table M f (Suc k) ` A)" then have "card (ofsm_table M f (Suc k) ` A) < card (ofsm_table M f k ` A)" by simp then obtain q1 q2 where "q1 ∈ A" and "q2 ∈ A" and "ofsm_table M f k q1 ≠ ofsm_table M f k q2" and "ofsm_table M f (Suc k) q1 = ofsm_table M f (Suc k) q2" using finite_card_less_witnesses[OF ‹finite A›] by blast then show False using ofsm_table_refinement_disjoint[OF _ _ assms(1), of q1 q2 k] using assms(2) by blast qed qed then show ?thesis using lift_Suc_mono_le[OF _ assms(3), where f="λ k . card (ofsm_table M f k ` A)"] by blast qed lemma ofsm_table_refinement_card_fix_Suc : assumes "equivalence_relation_on_states M f" and "card (ofsm_table M f (Suc k) ` states M) = card (ofsm_table M f k ` states M)" and "q ∈ states M" shows "ofsm_table M f (Suc k) q = ofsm_table M f k q" proof (rule ccontr) assume "ofsm_table M f (Suc k) q ≠ ofsm_table M f k q" then have "ofsm_table M f (Suc k) q ⊂ ofsm_table M f k q" using ofsm_table_subset by (metis Suc_leD order_refl psubsetI) then obtain q' where "q' ∈ ofsm_table M f k q" and "q' ∉ ofsm_table M f (Suc k) q" by blast then have "q' ∈ states M" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)] assms(3)] by blast have card_qq: "⋀ k . card (ofsm_table M f k ` states M) = card (ofsm_table M f k ` (states M - ⋃(ofsm_table M f k ` {q,q'}))) + card (ofsm_table M f k ` (⋃(ofsm_table M f k ` {q,q'})))" proof - fix k have "states M = (states M - ⋃(ofsm_table M f k ` {q,q'})) ∪ ⋃(ofsm_table M f k ` {q,q'})" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)] ‹q ∈ states M›] using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)] ‹q' ∈ states M›] by blast then have "finite (states M - ⋃(ofsm_table M f k ` {q,q'}))" and "finite (⋃(ofsm_table M f k ` {q,q'}))" using fsm_states_finite[of M] finite_Un[of "(states M - ⋃(ofsm_table M f k ` {q,q'}))" "⋃(ofsm_table M f k ` {q,q'})"] by force+ then have *:"finite (ofsm_table M f k ` (states M - ⋃(ofsm_table M f k ` {q,q'})))" and **:"finite (ofsm_table M f k ` ⋃(ofsm_table M f k ` {q,q'}))" by blast+ have ***:"(ofsm_table M f k ` (states M - ⋃(ofsm_table M f k ` {q,q'}))) ∩ (ofsm_table M f k ` ⋃(ofsm_table M f k ` {q,q'})) = {}" proof (rule ccontr) assume "ofsm_table M f k ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'})) ∩ ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'}) ≠ {}" then obtain Q where "Q ∈ ofsm_table M f k ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))" and "Q ∈ ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'})" by blast obtain q1 where "q1 ∈ (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))" and "Q = ofsm_table M f k q1" using ‹Q ∈ ofsm_table M f k ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))› by blast moreover obtain q2 where "q2 ∈ ⋃ (ofsm_table M f k ` {q, q'})" and "Q = ofsm_table M f k q2" using ‹Q ∈ ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'})› by blast ultimately have "ofsm_table M f k q1 = ofsm_table M f k q2" by auto have "q1 ∈ states M" and "q1 ∉ ⋃ (ofsm_table M f k ` {q, q'})" using ‹q1 ∈ (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))› by blast+ have "q2 ∈ states M" using ‹q2 ∈ ⋃ (ofsm_table M f k ` {q, q'})› ‹states M = (states M - ⋃(ofsm_table M f k ` {q,q'})) ∪ ⋃(ofsm_table M f k ` {q,q'})› by blast have "q1 ∈ ofsm_table M f k q2" using ‹ofsm_table M f k q1 = ofsm_table M f k q2› using ofsm_table_eq_if_elem[OF ‹q2 ∈ states M› ‹q1 ∈ states M› assms(1)] by blast moreover have "q2 ∈ ofsm_table M f k q ∨ q2 ∈ ofsm_table M f k q'" using ‹q2 ∈ ⋃ (ofsm_table M f k ` {q, q'})› by blast ultimately have "q1 ∈ ⋃ (ofsm_table M f k ` {q, q'})" unfolding ofsm_table_eq_if_elem[OF ‹q ∈ states M› ‹q2 ∈ states M› assms(1), symmetric] unfolding ofsm_table_eq_if_elem[OF ‹q' ∈ states M› ‹q2 ∈ states M› assms(1), symmetric] by blast then show False using ‹q1 ∉ ⋃ (ofsm_table M f k ` {q, q'})› by blast qed show "card (ofsm_table M f k ` states M) = card (ofsm_table M f k ` (states M - ⋃(ofsm_table M f k ` {q,q'}))) + card (ofsm_table M f k ` (⋃(ofsm_table M f k ` {q,q'})))" using card_Un_disjoint[OF * ** ***] using ‹states M = (states M - ⋃(ofsm_table M f k ` {q,q'})) ∪ ⋃(ofsm_table M f k ` {q,q'})› by (metis image_Un) qed have s1: "⋀ k . (states M - ⋃(ofsm_table M f k ` {q,q'})) ⊆ states M" and s2: "⋀ k . (⋃(ofsm_table M f k ` {q,q'})) ⊆ states M" using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)] ‹q ∈ states M›] using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)] ‹q' ∈ states M›] by blast+ have "card (ofsm_table M f (Suc k) ` states M) > card (ofsm_table M f k ` states M)" proof - have *: "⋃ (ofsm_table M f (Suc k) ` {q, q'}) ⊆ ⋃ (ofsm_table M f k ` {q, q'})" using ofsm_table_subset by (metis SUP_mono' lessI less_imp_le_nat) have "card (ofsm_table M f k ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))) ≤ card (ofsm_table M f (Suc k) ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'})))" using ofsm_table_refinement_card[OF assms(1), where i=k and j="Suc k", OF s1] using le_SucI by blast moreover have "card (ofsm_table M f (Suc k) ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))) ≤ card (ofsm_table M f (Suc k) ` (FSM.states M - ⋃ (ofsm_table M f (Suc k) ` {q, q'})))" using * using fsm_states_finite[of M] by (meson Diff_mono card_mono finite_Diff finite_imageI image_mono subset_refl) ultimately have "card (ofsm_table M f k ` (FSM.states M - ⋃ (ofsm_table M f k ` {q, q'}))) ≤ card (ofsm_table M f (Suc k) ` (FSM.states M - ⋃ (ofsm_table M f (Suc k) ` {q, q'})))" by presburger moreover have "card (ofsm_table M f k `