# 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

(* 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)"
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))"
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)"
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 ` ```