Theory Minimisation
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
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 ` ⋃ (ofsm_table M f k ` {q, q'})) < card (ofsm_table M f (Suc k) ` ⋃ (ofsm_table M f (Suc k) ` {q, q'}))"
proof -
have *: "⋀ k . ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'}) = {ofsm_table M f k q, ofsm_table M f k q'}"
proof -
fix k show "ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'}) = {ofsm_table M f k q, ofsm_table M f k q'}"
proof
show "ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'}) ⊆ {ofsm_table M f k q, ofsm_table M f k q'}"
proof
fix Q assume "Q ∈ ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'})"
then obtain qq where "Q = ofsm_table M f k qq"
and "qq ∈ ⋃ (ofsm_table M f k ` {q, q'})"
by blast
then have "qq ∈ ofsm_table M f k q ∨ qq ∈ ofsm_table M f k q'"
by blast
then have "qq ∈ states M"
using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)]] ‹q ∈ states M› ‹q' ∈ states M›
by blast
have "ofsm_table M f k qq = ofsm_table M f k q ∨ ofsm_table M f k qq = ofsm_table M f k q'"
using ‹qq ∈ ofsm_table M f k q ∨ qq ∈ ofsm_table M f k q'›
using ofsm_table_eq_if_elem[OF _ ‹qq ∈ states M› assms(1)] ‹q ∈ states M› ‹q' ∈ states M›
by blast
then show "Q ∈ {ofsm_table M f k q, ofsm_table M f k q'}"
using ‹Q = ofsm_table M f k qq›
by blast
qed
show "{ofsm_table M f k q, ofsm_table M f k q'} ⊆ ofsm_table M f k ` ⋃ (ofsm_table M f k ` {q, q'})"
using ofsm_table_containment[of _ M f, OF _ equivalence_relation_on_states_refl[OF assms(1)]] ‹q ∈ states M› ‹q' ∈ states M›
by blast
qed
qed
have "ofsm_table M f k q = ofsm_table M f k q'"
using ‹q' ∈ ofsm_table M f k q›
using ofsm_table_eq_if_elem[OF ‹q ∈ states M› ‹q' ∈ states M› assms(1)]
by blast
moreover have "ofsm_table M f (Suc k) q ≠ ofsm_table M f (Suc k) q'"
using ‹q' ∉ ofsm_table M f (Suc k) q›
using ofsm_table_eq_if_elem[OF ‹q ∈ states M› ‹q' ∈ states M› assms(1)]
by blast
ultimately show ?thesis
unfolding *
by (metis card_insert_if finite.emptyI finite.insertI insert_absorb insert_absorb2 insert_not_empty lessI singleton_insert_inj_eq)
qed
ultimately show ?thesis
unfolding card_qq by presburger
qed
then show False
using assms(2) by linarith
qed
lemma ofsm_table_refinement_card_fix :
assumes "equivalence_relation_on_states M f"
and "card (ofsm_table M f j ` states M) = card (ofsm_table M f i ` states M)"
and "q ∈ states M"
and "i ≤ j"
shows "ofsm_table M f j q = ofsm_table M f i q"
using assms (2,4) proof (induction "j-i" arbitrary: i j)
case 0
then have "i = j" by auto
then show ?case by auto
next
case (Suc k)
then have "j ≥ Suc i" and "k = j - Suc i"
by auto
have *:"card (ofsm_table M f j ` FSM.states M) = card (ofsm_table M f (Suc i) ` FSM.states M)"
and **:"card (ofsm_table M f (Suc i) ` FSM.states M) = card (ofsm_table M f i ` FSM.states M)"
using ofsm_table_refinement_card[OF assms(1), where A="states M"]
by (metis Suc.prems(1) ‹Suc i ≤ j› eq_iff le_SucI)+
show ?case
using Suc.hyps(1)[OF ‹k = j - Suc i› * ‹Suc i ≤ j›]
using ofsm_table_refinement_card_fix_Suc[OF assms(1) ** assms(3)]
by blast
qed
lemma ofsm_table_partition_fixpoint_Suc :
assumes "equivalence_relation_on_states M f"
and "q ∈ states M"
shows "ofsm_table M f (size M - card (f ` states M)) q = ofsm_table M f (Suc (size M - card (f ` states M))) q"
proof -
have "⋀ q . q ∈ states M ⟹ f q = ofsm_table M f 0 q"
unfolding ofsm_table.simps by auto
define n where n: "n = (λ i . card (ofsm_table M f i ` states M))"
have "⋀ i j . i ≤ j ⟹ n i ≤ n j"
unfolding n
using ofsm_table_refinement_card[OF assms(1), where A="states M"]
by blast
moreover have "⋀ i j m . i < j ⟹ n i = n j ⟹ j ≤ m ⟹ n i = n m"
proof -
fix i j m assume "i < j" and "n i = n j" and "j ≤ m"
then have "Suc i ≤ j" and "i ≤ Suc i" and "i ≤ m"
by auto
have "⋀ q . q ∈ states M ⟹ ofsm_table M f j q = ofsm_table M f i q"
using ‹i < j› ‹n i = n j› ofsm_table_refinement_card_fix[OF assms(1) _]
unfolding n
using less_imp_le_nat by presburger
then have "⋀ q . q ∈ states M ⟹ ofsm_table M f (Suc i) q = ofsm_table M f i q"
using ofsm_table_subset[OF ‹Suc i ≤ j›, of M f]
using ofsm_table_subset[OF ‹i ≤ Suc i›, of M f]
by blast
then have "⋀ q . q ∈ states M ⟹ ofsm_table M f m q = ofsm_table M f i q"
using ofsm_table_fixpoint[OF ‹i ≤ m›]
by metis
then show "n i = n m"
unfolding n
by auto
qed
moreover have "⋀ i . n i ≤ size M"
unfolding n
using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)]]
using fsm_states_finite[of M]
by (simp add: card_image_le)
ultimately obtain k where "n (Suc k) = n k"
and "k ≤ size M - n 0"
using monotone_function_with_limit_witness_helper[where f=n and k="size M"]
by blast
then show ?thesis
unfolding n
using ‹⋀ q . q ∈ states M ⟹ f q = ofsm_table M f 0 q›[symmetric]
using ofsm_table_refinement_card_fix_Suc[OF assms(1) _ ]
using ofsm_table_fixpoint[OF _ _ assms(2)]
by (metis (mono_tags, lifting) image_cong nat_le_linear not_less_eq_eq)
qed
lemma ofsm_table_partition_fixpoint :
assumes "equivalence_relation_on_states M f"
and "size M ≤ m"
and "q ∈ states M"
shows "ofsm_table M f (m - card (f ` states M)) q = ofsm_table M f (Suc (m - card (f ` states M))) q"
proof -
have *: "size M - card (f ` states M) ≤ m - card (f ` states M)"
using assms(2) by simp
have **: "(size M - card (f ` states M)) ≤ Suc (m - card (f ` states M))"
using assms(2) by simp
have ***: "⋀ q . q ∈ FSM.states M ⟹ ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q = ofsm_table M f (Suc (FSM.size M - card (f ` FSM.states M))) q"
using ofsm_table_partition_fixpoint_Suc[OF assms(1)] .
have "ofsm_table M f (m - card (f ` states M)) q = ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q"
using ofsm_table_fixpoint[OF * _ assms(3)] ***
by blast
moreover have "ofsm_table M f (Suc (m - card (f ` states M))) q = ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q"
using ofsm_table_fixpoint[OF ** _ assms(3), of f] ***
by blast
ultimately show ?thesis
by simp
qed
lemma ofsm_table_fix_partition_fixpoint :
assumes "equivalence_relation_on_states M f"
and "size M ≤ m"
and "q ∈ states M"
shows "ofsm_table M f (m - card (f ` states M)) q = ofsm_table_fix M f 0 q"
proof -
obtain k where k1: "ofsm_table_fix M f 0 q = ofsm_table M f k q"
and k2: "⋀ k' . 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(1)]]
assms(3)
by metis
have m1: "⋀ k' . k' ≥ m - card (f ` states M) ⟹ ofsm_table M f k' q = ofsm_table M f (m - card (f ` states M)) q"
using ofsm_table_partition_fixpoint[OF assms(1,2)]
using ofsm_table_fixpoint[OF _ _ assms(3)]
by presburger
show ?thesis proof (cases "k ≤ m - card (f ` states M)")
case True
show ?thesis
using k1 k2[OF True] by simp
next
case False
then have "k ≥ m - card (f ` states M)"
by auto
then have "ofsm_table M f k q = ofsm_table M f (m - card (f ` states M)) q"
using ofsm_table_partition_fixpoint[OF assms(1,2)]
using ofsm_table_fixpoint[OF _ _ assms(3)]
by presburger
then show ?thesis
using k1 by simp
qed
qed
subsection ‹A minimisation function based on OFSM-tables›
lemma language_equivalence_classes_preserve_observability:
assumes "transitions M' = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
and "observable M"
shows "observable M'"
proof -
have "⋀ t1 t2 . t1 ∈ transitions M' ⟹
t2 ∈ transitions M' ⟹
t_source t1 = t_source t2 ⟹
t_input t1 = t_input t2 ⟹
t_output t1 = t_output t2 ⟹
t_target t1 = t_target t2"
proof -
fix t1 t2 assume "t1 ∈ transitions M'" and "t2 ∈ transitions M'" and "t_source t1 = t_source t2" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2"
obtain t1' where t1'_def: "t1 = ({q ∈ states M . LS M q = LS M (t_source t1')} , t_input t1', t_output t1', {q ∈ states M . LS M q = LS M (t_target t1')})"
and "t1' ∈ transitions M"
using ‹t1 ∈ transitions M'› assms(1) by auto
obtain t2' where t2'_def: "t2 = ({q ∈ states M . LS M q = LS M (t_source t2')} , t_input t2', t_output t2', {q ∈ states M . LS M q = LS M (t_target t2')})"
and "t2' ∈ transitions M"
using ‹t2 ∈ transitions M'› assms(1) ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by auto
have "{q ∈ FSM.states M. LS M q = LS M (t_source t1')} = {q ∈ FSM.states M. LS M q = LS M (t_source t2')}"
using t1'_def t2'_def ‹t_source t1 = t_source t2›
by (metis (no_types, lifting) fst_eqD)
then have "LS M (t_source t1') = LS M (t_source t2')"
using fsm_transition_source[OF ‹t1' ∈ transitions M›] fsm_transition_source[OF ‹t2' ∈ transitions M›] by blast
then have "LS M (t_target t1') = LS M (t_target t2')"
using observable_transition_target_language_eq[OF _ ‹t1' ∈ transitions M› ‹t2' ∈ transitions M› _ _ ‹observable M›]
using ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2›
unfolding t1'_def t2'_def fst_conv snd_conv by blast
then show "t_target t1 = t_target t2"
unfolding t1'_def t2'_def snd_conv by blast
qed
then show ?thesis
unfolding observable.simps by blast
qed
lemma language_equivalence_classes_retain_language_and_induce_minimality :
assumes "transitions M' = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
and "states M' = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
and "initial M' = {q' ∈ states M . LS M q' = LS M (initial M)}"
and "observable M"
shows "L M = L M'"
and "minimal M'"
proof -
have "observable M'"
using assms(1,4) language_equivalence_classes_preserve_observability by blast
have ls_prop: "⋀ io q . q ∈ states M ⟹ (io ∈ LS M q) ⟷ (io ∈ LS M' {q' ∈ states M . LS M q = LS M q'})"
proof -
fix io q assume "q ∈ states M"
then show "(io ∈ LS M q) ⟷ (io ∈ LS M' {q' ∈ states M . LS M q = LS M q'})"
proof (induction io arbitrary: q)
case Nil
then show ?case using assms(2) by auto
next
case (Cons xy io)
obtain x y where "xy = (x,y)"
using surjective_pairing by blast
have "xy#io ∈ LS M q ⟹ xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'}"
proof -
assume "xy#io ∈ LS M q"
then obtain p where "path M q p" and "p_io p = xy#io"
unfolding LS.simps mem_Collect_eq by (metis (no_types, lifting))
let ?t = "hd p"
let ?p = "tl p"
let ?q' = "{q' ∈ states M . LS M (t_target ?t) = LS M q'}"
have "p = ?t # ?p" and "p_io ?p = io" and "t_input ?t = x" and "t_output ?t = y"
using ‹p_io p = xy#io› unfolding ‹xy = (x,y)› by auto
moreover have "?t ∈ transitions M" and "path M (t_target ?t) ?p" and "t_source ?t = q"
using ‹path M q p› path_cons_elim[of M q ?t ?p] calculation by auto
ultimately have "[(x,y)] ∈ LS M q"
unfolding LS_single_transition[of x y M q] by auto
then have "io ∈ LS M (t_target ?t)"
using observable_language_next[OF _ ‹observable M›, of "(x,y)" io, OF _ ‹?t ∈ transitions M›]
‹xy#io ∈ LS M q›
unfolding ‹xy = (x,y)› ‹t_source ?t = q› ‹t_input ?t = x› ‹t_output ?t = y›
by (metis ‹?t ∈ FSM.transitions M› from_FSM_language fsm_transition_target fst_conv snd_conv)
then have "io ∈ LS M' ?q'"
using Cons.IH[OF fsm_transition_target[OF ‹?t ∈ transitions M›]] by blast
then obtain p' where "path M' ?q' p'" and "p_io p' = io"
by auto
have *: "({q' ∈ states M . LS M q = LS M q'},x,y,{q' ∈ states M . LS M (t_target ?t) = LS M q'}) ∈ transitions M'"
using ‹?t ∈ transitions M› ‹t_source ?t = q› ‹t_input ?t = x› ‹t_output ?t = y›
unfolding assms(1) by auto
show "xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'}"
using LS_prepend_transition[OF * ] unfolding snd_conv fst_conv ‹xy = (x,y)›
using ‹io ∈ LS M' ?q'› by blast
qed
moreover have "xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'} ⟹ xy#io ∈ LS M q"
proof -
let ?q = "{q' ∈ states M . LS M q = LS M q'}"
assume "xy#io ∈ LS M' ?q"
then obtain p where "path M' ?q p" and "p_io p = xy#io"
unfolding LS.simps mem_Collect_eq by (metis (no_types, lifting))
let ?t = "hd p"
let ?p = "tl p"
have "p = ?t # ?p" and "p_io ?p = io" and "t_input ?t = x" and "t_output ?t = y"
using ‹p_io p = xy#io› unfolding ‹xy = (x,y)› by auto
then have "path M' ?q (?t#?p)"
using ‹path M' ?q p› by auto
then have "?t ∈ transitions M'" and "path M' (t_target ?t) ?p" and "t_source ?t = ?q"
by force+
then have "io ∈ LS M' (t_target ?t)"
using ‹p_io ?p = io› by auto
obtain t0 where t0_def: "?t = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) t0"
and "t0 ∈ transitions M"
using ‹?t ∈ transitions M'›
unfolding assms(1)
by auto
then have "t_source t0 ∈ ?q"
using ‹t_source ?t = ?q›
by (metis (mono_tags, lifting) fsm_transition_source fst_eqD mem_Collect_eq)
then have "LS M q = LS M (t_source t0)"
by auto
moreover have "[(x,y)] ∈ LS M (t_source t0)"
using t0_def ‹t_input ?t = x› ‹t0 ∈ transitions M› ‹t_output ?t = y› ‹t_source t0 ∈ ?q› unfolding LS_single_transition by auto
ultimately obtain t where "t ∈ transitions M" and "t_source t = q" and "t_input t = x" and "t_output t = y"
by (metis LS_single_transition)
have "LS M (t_target t) = LS M (t_target t0)"
using observable_transition_target_language_eq[OF _‹t ∈ transitions M› ‹t0 ∈ transitions M› _ _ ‹observable M›]
using ‹LS M q = LS M (t_source t0)›
unfolding ‹t_source t = q› ‹t_input t = x› ‹t_output t = y›
using t0_def ‹t_input ?t = x› ‹t_output ?t = y›
by auto
moreover have "t_target ?t = {q' ∈ FSM.states M. LS M (t_target t) = LS M q'}"
using calculation t0_def by fastforce
ultimately have "io ∈ LS M (t_target t)"
using Cons.IH[OF fsm_transition_target[OF ‹t ∈ transitions M›]]
‹io ∈ LS M' (t_target ?t)›
by auto
then show "xy#io ∈ LS M q"
unfolding ‹t_source t = q›[symmetric] ‹xy = (x,y)›
using ‹t_input t = x› ‹t_output t = y›
using LS_prepend_transition ‹t ∈ FSM.transitions M›
by blast
qed
ultimately show ?case
by blast
qed
qed
have "L M' = LS M' {q' ∈ states M . LS M (initial M) = LS M q'}"
using assms(3)
by (metis (mono_tags, lifting) Collect_cong)
then show "L M = L M'"
using ls_prop[OF fsm_initial] by blast
show "minimal M'"
proof -
have"⋀ q q' . q ∈ states M' ⟹ q' ∈ states M' ⟹ LS M' q = LS M' q' ⟹ q = q'"
proof -
fix q q' assume "q ∈ states M'" and "q' ∈ states M'" and "LS M' q = LS M' q'"
obtain qM where "q = {q ∈ states M . LS M qM = LS M q}" and "qM ∈ states M"
using ‹q ∈ states M'› assms(2) by auto
obtain qM' where "q' = {q ∈ states M . LS M qM' = LS M q}" and "qM' ∈ states M"
using ‹q' ∈ states M'› assms(2) by auto
have "LS M qM = LS M' q"
using ls_prop[OF ‹qM ∈ states M›] unfolding ‹q = {q ∈ states M . LS M qM = LS M q}› by blast
moreover have "LS M qM' = LS M' q'"
using ls_prop[OF ‹qM' ∈ states M›] unfolding ‹q' = {q ∈ states M . LS M qM' = LS M q}› by blast
ultimately have "LS M qM = LS M qM'"
using ‹LS M' q = LS M' q'› by blast
then show "q = q'"
unfolding ‹q = {q ∈ states M . LS M qM = LS M q}› ‹q' = {q ∈ states M . LS M qM' = LS M q}› by blast
qed
then show ?thesis
unfolding minimal_alt_def by blast
qed
qed
fun minimise :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ⇒ ('a set,'b,'c) fsm" where
"minimise M = (let
eq_class = ofsm_table_fix M (λq . states M) 0;
ts = (λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M);
q0 = eq_class (initial M);
eq_states = eq_class |`| fstates M;
M' = create_unconnected_fsm_from_fsets q0 eq_states (finputs M) (foutputs M)
in add_transitions M' ts)"
lemma minimise_initial_partition :
"equivalence_relation_on_states M (λq . states M)"
proof -
let ?r = "{(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ (λq . states M) q1}"
have "refl_on (FSM.states M) ?r"
unfolding refl_on_def by blast
moreover have "sym ?r"
unfolding sym_def by blast
moreover have "trans ?r"
unfolding trans_def by blast
ultimately show ?thesis
unfolding equivalence_relation_on_states_def equiv_def by auto
qed
lemma minimise_props:
assumes "observable M"
shows "initial (minimise M) = {q' ∈ states M . LS M q' = LS M (initial M)}"
and "states (minimise M) = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
and "inputs (minimise M) = inputs M"
and "outputs (minimise M) = outputs M"
and "transitions (minimise M) = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
proof -
let ?f = "λq . states M"
define eq_class where "eq_class = ofsm_table_fix M (λq . states M) 0"
moreover define M' where M'_def: "M' = create_unconnected_fsm_from_fsets (eq_class (initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)"
ultimately have *: "minimise M = add_transitions M' ((λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))"
by auto
have **: "⋀ q . q ∈ states M ⟹ eq_class q = {q' ∈ FSM.states M. LS M q = LS M q'}"
using ofsm_table_fix_set[OF _ assms minimise_initial_partition] ‹eq_class = ofsm_table_fix M ?f 0› after_is_state[OF ‹observable M›] by blast
then have ****: "⋀ q . q ∈ states M ⟹ eq_class q = {q' ∈ FSM.states M. LS M q' = LS M q}"
using ofsm_table_fix_set[OF _ assms] ‹eq_class = ofsm_table_fix M ?f 0› by blast
have ***: "(eq_class (initial M)) |∈| (eq_class |`| fstates M)"
using fsm_initial[of M] fstates_set by fastforce
have m1:"initial M' = {q' ∈ states M . LS M q' = LS M (initial M)}"
by (metis (mono_tags) "***" "****" M'_def create_unconnected_fsm_from_fsets_simps(1) fsm_initial)
have m2: "states M' = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
unfolding M'_def
proof -
have "FSM.states (FSM.create_unconnected_fsm_from_fsets (eq_class (FSM.initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)) = eq_class ` FSM.states M"
by (metis (no_types) "***" create_unconnected_fsm_from_fsets_simps(2) fset.set_map fstates_set)
then show "FSM.states (FSM.create_unconnected_fsm_from_fsets (eq_class (FSM.initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)) = (λa. {aa ∈ FSM.states M. LS M a = LS M aa}) ` FSM.states M"
using "**" by force
qed
have m3: "inputs M' = inputs M"
using create_unconnected_fsm_from_fsets_simps(3)[OF ***] finputs_set unfolding M'_def by metis
have m4: "outputs M' = outputs M"
using create_unconnected_fsm_from_fsets_simps(4)[OF ***] foutputs_set unfolding M'_def by metis
have m5: "transitions M' = {}"
using create_unconnected_fsm_from_fsets_simps(5)[OF ***] unfolding M'_def by force
let ?ts = "((λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))"
have wf: "⋀ t . t ∈?ts ⟹ t_source t ∈ states M' ∧ t_input t ∈ inputs M' ∧ t_output t ∈ outputs M' ∧ t_target t ∈ states M'"
proof -
fix t assume "t ∈ ?ts"
then obtain tM where "tM ∈ transitions M"
and *: "t = (λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) tM"
by blast
have "t_source t ∈ states M'"
using fsm_transition_source[OF ‹tM ∈ transitions M›]
unfolding m2 * **[OF fsm_transition_source[OF ‹tM ∈ transitions M›]] by auto
moreover have "t_input t ∈ inputs M'"
unfolding m3 * using fsm_transition_input[OF ‹tM ∈ transitions M›] by auto
moreover have "t_output t ∈ outputs M'"
unfolding m4 * using fsm_transition_output[OF ‹tM ∈ transitions M›] by auto
moreover have "t_target t ∈ states M'"
using fsm_transition_target[OF ‹tM ∈ transitions M›]
unfolding m2 * **[OF fsm_transition_target[OF ‹tM ∈ transitions M›]] by auto
ultimately show "t_source t ∈ states M' ∧ t_input t ∈ inputs M' ∧ t_output t ∈ outputs M' ∧ t_target t ∈ states M'"
by simp
qed
show "initial (minimise M) = {q' ∈ states M . LS M q' = LS M (initial M)}"
using add_transitions_simps(1)[OF wf] unfolding * m1 .
show "states (minimise M) = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
using add_transitions_simps(2)[OF wf] unfolding * m2 .
show "inputs (minimise M) = inputs M"
using add_transitions_simps(3)[OF wf] unfolding * m3 .
show "outputs (minimise M) = outputs M"
using add_transitions_simps(4)[OF wf] unfolding * m4 .
show "transitions (minimise M) = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
using add_transitions_simps(5)[OF wf] ****[OF fsm_transition_source] ****[OF fsm_transition_target] unfolding * m5 by auto
qed
lemma minimise_observable:
assumes "observable M"
shows "observable (minimise M)"
using language_equivalence_classes_preserve_observability[OF minimise_props(5)[OF assms] assms]
by assumption
lemma minimise_minimal:
assumes "observable M"
shows "minimal (minimise M)"
using language_equivalence_classes_retain_language_and_induce_minimality(2)[OF minimise_props(5,2,1)[OF assms] assms]
by assumption
lemma minimise_language:
assumes "observable M"
shows "L (minimise M) = L M"
using language_equivalence_classes_retain_language_and_induce_minimality(1)[OF minimise_props(5,2,1)[OF assms] assms]
by blast
lemma minimal_observable_code :
assumes "observable M"
shows "minimal M = (∀ q ∈ states M . ofsm_table_fix M (λq . states M) 0 q = {q})"
proof
show "minimal M ⟹ (∀ q ∈ states M . ofsm_table_fix M (λq . states M) 0 q = {q})"
proof
fix q assume "minimal M" and "q ∈ states M"
then show "ofsm_table_fix M (λq . states M) 0 q = {q}"
unfolding ofsm_table_fix_set[OF ‹q ∈ states M› ‹observable M› minimise_initial_partition]
minimal_alt_def
using after_is_state[OF ‹observable M›]
by blast
qed
show "∀q∈FSM.states M. ofsm_table_fix M (λq . states M) 0 q = {q} ⟹ minimal M"
using ofsm_table_fix_set[OF _ ‹observable M› minimise_initial_partition] after_is_state[OF ‹observable M›]
unfolding minimal_alt_def
by blast
qed
lemma minimise_states_subset :
assumes "observable M"
and "q ∈ states (minimise M)"
shows "q ⊆ states M"
using assms(2)
unfolding minimise_props[OF assms(1)]
by auto
lemma minimise_states_finite :
assumes "observable M"
and "q ∈ states (minimise M)"
shows "finite q"
using minimise_states_subset[OF assms] fsm_states_finite[of M]
using finite_subset by auto
end