Quelle  Minimisation.thy

section ‹Minimisation by OFSM Tables›

text ‹This theory presents the classical algorithm for transforming observable FSMs into
 language-equivalent observable and minimal FSMs in analogy to the minimisation of
 finite automata.›


theory Minimisation
imports FSM 
begin


subsection ‹OFSM Tables›

text ‹OFSM tables partition the states of an FSM based on an initial partition and an iteration
 counter.
 States are in the same element of the 0th table iff they are in the same element of the
 initial partition.
 States q1, q2 are in the same element of the (k+1)-th table if they are in the same element of
 the k-th table and furthermore for each IO pair (x,y) either (x,y) is not in the language of
 both q1 and q2 or it is in the language of both states and the states q1', q2' reached via
 (x,y) from q1 and q2, respectively, are in the same element of the k-th table.›


fun ofsm_table :: "('a,'b,'c) fsm ==> ('a ==> 'a set) ==> nat ==> 'a ==> 'a set" where
  "ofsm_table M f 0 q = (if q ∈ states M then f q else {})" |
  "ofsm_table M f (Suc k) q = (let
      prev_table = ofsm_table M f k
    in {q' ∈ prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> prev_table qT = prev_table qT' | None ==> False) | None ==> h_obs M q' x y = None) })"


lemma ofsm_table_non_state :
  assumes "q ∉ states M"
  shows "ofsm_table M f k q = {}"
using assms by (induction k; auto)

lemma ofsm_table_subset: 
  assumes "i ≤ j"
  shows "ofsm_table M f j q ⊆ ofsm_table M f i q"
proof -
  have *: "∧ k . ofsm_table M f (Suc k) q ⊆ ofsm_table M f k q"
  proof -
    fix k show "ofsm_table M f (Suc k) q ⊆ ofsm_table M f k q"
    proof (cases k)
      case 0
      show ?thesis unfolding 0 ofsm_table.simps Let_def by blast
    next
      case (Suc k')
      
      show ?thesis 
        unfolding Suc ofsm_table.simps Let_def by force
    qed
  qed
  
  show ?thesis
    using assms 
  proof (induction j)
    case 0
    then show ?case by auto
  next
    case (Suc x)
    then show ?case using *[of x]
      using le_SucE by blast 
  qed
qed


lemma ofsm_table_case_helper :
  "(case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f k qT = ofsm_table M f k qT' | None ==> False) | None ==> h_obs M q' x y = None)
   = ((∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f k qT = ofsm_table M f k qT') ∨ (h_obs M q x y = None ∧ h_obs M q' x y = None))"
proof -
  have *: "∧ a b P . (case a of Some a' ==> (case b of Some b' ==> P a' b' | None ==> False) | None ==> b = None)
    = ((∃ a' b' . a = Some a' ∧ b = Some b' ∧ P a' b') ∨ (a = None ∧ b = None))"
    (is "∧ a b P . ?P1 a b P = ?P2 a b P")
  proof 
    fix a b P
    show "?P1 a b P ==> ?P2 a b P" using case_optionE[of "b = None" "λa' . (case b of Some b' ==> P a' b' | None ==> False)" a]
      by (metis case_optionE) 
    show "?P2 a b P ==> ?P1 a b P" by auto
  qed
  
  show ?thesis 
    using *[of "h_obs M q' x y" "λqT qT' . ofsm_table M f k qT = ofsm_table M f k qT'" "h_obs M q x y"] .
qed


lemma ofsm_table_case_helper_neg :
  "(¬ (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f k qT = ofsm_table M f k qT' | None ==> False) | None ==> h_obs M q' x y = None))
   = ((∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f k qT ≠ ofsm_table M f k qT') ∨ (h_obs M q x y = None ⟷ h_obs M q' x y ≠ None))"
  unfolding ofsm_table_case_helper by force 



lemma ofsm_table_fixpoint :
  assumes "i ≤ j"
  and     "∧ q . q ∈ states M ==> ofsm_table M f (Suc i) q = ofsm_table M f i q"
  and     "q ∈ states M"
shows "ofsm_table M f j q = ofsm_table M f i q"
proof -

  have *: "∧ k . k ≥ i ==> (∧ q . q ∈ states M ==> ofsm_table M f (Suc k) q = ofsm_table M f k q)"
  proof -
    
    fix k :: nat assume "k ≥ i" 
    then show "∧ q . q ∈ states M ==> ofsm_table M f (Suc k) q = ofsm_table M f k q"
    proof (induction k)
      case 0
      then show ?case using assms(2) by auto
    next
      case (Suc k)

      show "ofsm_table M f (Suc (Suc k)) q = ofsm_table M f (Suc k) q" 
      proof (cases "i = Suc k")
        case True
        then show ?thesis using assms(2)[OF ‹q ∈ states M›] by simp
      next
        case False
        then have "i ≤ k"
          using ‹i ≤ Suc k› by auto

        have h_obs_state: "∧ q x y qT . h_obs M q x y = Some qT ==> qT ∈ states M"
          using h_obs_state by fastforce

        show ?thesis 
        proof (rule ccontr) 
          assume "ofsm_table M f (Suc (Suc k)) q ≠ ofsm_table M f (Suc k) q"
          moreover have "ofsm_table M f (Suc (Suc k)) q ⊆ ofsm_table M f (Suc k) q"
            using ofsm_table_subset
            by (metis (full_types) Suc_n_not_le_n nat_le_linear) 
          ultimately obtain q' where "q' ∉ {q' ∈ ofsm_table M f (Suc k) q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ==> False) | None ==> h_obs M q' x y = None) }"
                                 and "q' ∈ ofsm_table M f (Suc k) q"
            using ofsm_table.simps(2)[of M f "Suc k" q] unfolding Let_def by blast
          then have "¬(∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ==> False) | None ==> h_obs M q' x y = None))"
            by blast
          then obtain x y where "x ∈ inputs M" and "y ∈ outputs M" and "¬ (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f (Suc k) qT = ofsm_table M f (Suc k) qT' | None ==> False) | None ==> h_obs M q' x y = None)"
            by blast            
          then consider "∃ qT qT' . h_obs M q x y = Some qT ∧ h_obs M q' x y = Some qT' ∧ ofsm_table M f (Suc k) qT ≠ ofsm_table M f (Suc k) qT'" |
                        "(h_obs M q x y = None ⟷ h_obs M q' x y ≠ None)"
            unfolding ofsm_table_case_helper_neg by blast 
          then show False proof cases
            case 1
            then obtain qT qT' where "h_obs M q x y = Some qT" and "h_obs M q' x y = Some qT'" and "ofsm_table M f (Suc k) qT ≠ ofsm_table M f (Suc k) qT'"
              by blast
            then have "ofsm_table M f k qT ≠ ofsm_table M f k qT'"
              using Suc.IH[OF h_obs_state[OF ‹h_obs M q x y = Some qT›] ‹i ≤ k›]
                    Suc.IH[OF h_obs_state[OF ‹h_obs M q' x y = Some qT'›] ‹i ≤ k›]
              by fast
            moreover have "q' ∈ ofsm_table M f k q"
              using ofsm_table_subset[of k "Suc k"] ‹q' ∈ ofsm_table M f (Suc k) q› by force
            ultimately have "ofsm_table M f (Suc k) q ≠ ofsm_table M f k q"
              using ‹x ∈ inputs M› ‹y ∈ outputs M› ‹h_obs M q x y = Some qT› ‹h_obs M q' x y = Some qT'›
              unfolding ofsm_table.simps(2) Let_def by force
            then show ?thesis 
              using Suc.IH[OF Suc.prems(1) ‹i ≤ k›] by simp 
          next
            case 2
            then have "¬ (case h_obs M q x y of Some qT ==> (case h_obs M q' x y of Some qT' ==> ofsm_table M f k qT = ofsm_table M f k qT' | None ==> False) | None ==> h_obs M q' x y = None)"
              unfolding ofsm_table_case_helper_neg by blast
            moreover have "q' ∈ ofsm_table M f k q"
              using ofsm_table_subset[of k "Suc k"] ‹q' ∈ ofsm_table M f (Suc k) q› by force
            ultimately have "ofsm_table M f (Suc k) q ≠ ofsm_table M f k q"
              using ‹x ∈ inputs M› ‹y ∈ outputs M›
              unfolding ofsm_table.simps(2) Let_def by force
            then show ?thesis 
              using Suc.IH[OF Suc.prems(1) ‹i ≤ k›] by simp
          qed
        qed
      qed
    qed
  qed
  
  show ?thesis
    using assms(1) proof (induction "j")
    case 0
    then show ?case by auto
  next
    case (Suc j) 
    
    show ?case proof (cases "i = Suc j")
      case True
      then show ?thesis by simp
    next
      case False
      then have "i ≤ j"
        using Suc.prems(1) by auto
      then have "ofsm_table M f j q = ofsm_table M f i q"
        using Suc.IH by auto
      moreover have "ofsm_table M f (Suc j) q = ofsm_table M f j q"
        using *[OF ‹i≤j› ‹q∈states M›] by assumption
      ultimately show ?thesis 
        by blast
    qed
  qed
qed


(* restricts the range of the supplied function to the states of the FSM - required for (easy) termination *)
function ofsm_table_fix :: "('a,'b,'c) fsm ==> ('a ==> 'a set) ==> nat ==> 'a ==> 'a set" where
  "ofsm_table_fix M f k = (let
    cur_table = ofsm_table M (λq. f q ∩ states M) k;
    next_table = ofsm_table M (λq. f q ∩ states M) (Suc k)
  in if (∀ q ∈ states M . cur_table q = next_table q)
    then cur_table
    else ofsm_table_fix M f (Suc k))"
  by pat_completeness auto
termination   
proof -
  {
    fix M :: "('a,'b,'c) fsm"
    and f :: "('a ==> 'a set)"
    and k :: nat 
  
    define f' where f': "f' = (λq. f q ∩ states M)"
    
    assume "∃q∈FSM.states M. ofsm_table M (λq. f q ∩ states M) k q ≠ ofsm_table M (λq. f q ∩ states M) (Suc k) q"
    then obtain q where "q ∈ states M"
                    and "ofsm_table M f' k q ≠ ofsm_table M f' (Suc k) q"
      unfolding f' by blast
  
    have *: "∧ k . (∑q∈FSM.states M. card (ofsm_table M f' k q)) = card (ofsm_table M f' k q) + (∑q∈FSM.states M - {q}. card (ofsm_table M f' k q))"
      using ‹q ∈ states M› by (meson fsm_states_finite sum.remove)
  
    have "∧ q . ofsm_table M f' (Suc k) q ⊆ ofsm_table M f' k q"
      using ofsm_table_subset[of k "Suc k" M ] by auto
    moreover have "∧ q . finite (ofsm_table M f' k q)"
    proof -
      fix q 
      have "ofsm_table M (λq. f q ∩ states M) k q ⊆ ofsm_table M (λq. f q ∩ states M) 0 q"
        using ofsm_table_subset[of 0 k M "(λq. f q ∩ FSM.states M)" q] by auto
      then have "ofsm_table M f' k q ⊆ states M"
        unfolding f'
        using ofsm_table_non_state[of q M "(λq. f q ∩ FSM.states M)" k]
        by force 
      then show "finite (ofsm_table M f' k q)"
        using fsm_states_finite finite_subset by auto 
    qed
    ultimately have "∧ q . card (ofsm_table M f' (Suc k) q) ≤ card (ofsm_table M f' k q)"
      by (simp add: card_mono)
    then have "(∑q∈FSM.states M - {q}. card (ofsm_table M f' (Suc k) q)) ≤ (∑q∈FSM.states M - {q}. card (ofsm_table M f' k q))"
      by (simp add: sum_mono)
    moreover have "card (ofsm_table M f' (Suc k) q) < card (ofsm_table M f' k q)"
      using ‹ofsm_table M f' k q ≠ ofsm_table M f' (Suc k) q› ‹ofsm_table M f' (Suc k) q ⊆ ofsm_table M f' k q› ‹finite (ofsm_table M f' k q)›
      by (metis psubsetI psubset_card_mono)    
    ultimately have "(∑q∈FSM.states M. card (ofsm_table M (λq. f q ∩ states M) (Suc k) q)) < (∑q∈FSM.states M. card (ofsm_table M (λq. f q ∩ states M) k q))"
      unfolding f'[symmetric] *
      by linarith 
  } note t = this

  show ?thesis
    apply (relation "measure (λ (M, f, k) . ∑ q ∈ states M . card (ofsm_table M (λq. f q ∩ states M) k q))")
    apply (simp del: h_obs.simps ofsm_table.simps)+
    by (erule t) 
qed


lemma ofsm_table_restriction_to_states :
  assumes "∧ q . q ∈ states M ==> f q ⊆ states M"
  and     "q ∈ states M"
shows "ofsm_table M f k q = ofsm_table M (λq . f q ∩ states M) k q"
using assms(2) proof (induction k arbitrary: q)
  case 0
  then show ?case using assms(1) by auto
next
  case (Suc k)

  have "∧ x y q q' . (case h_obs M q x y of None ==> h_obs M q' x y = None | Some qT ==> (case h_obs M q' x y of None ==> False | Some qT' ==> ofsm_table M f k qT = ofsm_table M f k qT'))
                      = (case h_obs M q x y of None ==> h_obs M q' x y = None | Some qT ==> (case h_obs M q' x y of None ==> False | Some qT' ==> ofsm_table M (λq . f q ∩ states M) k qT = ofsm_table M (λq . f q ∩ states M) k qT'))"
        (is "∧ x y q q' . ?C1 x y q q' = ?C2 x y q q' ")
  proof -
    fix x y q q'  
    show "?C1 x y q q' = ?C2 x y q q'"
      using Suc.IH[OF h_obs_state, of q x y]
      using Suc.IH[OF h_obs_state, of q' x y] 
      by (cases "h_obs M q x y"; cases "h_obs M q' x y"; auto)
  qed
  then show ?case
    unfolding ofsm_table.simps Let_def Suc.IH[OF Suc.prems] 
    by blast
qed


lemma ofsm_table_fix_length :
  assumes "∧ q . q ∈ states M ==> f q ⊆ states M"
  obtains k where "∧ q . q ∈ states M ==> ofsm_table_fix M f 0 q = ofsm_table M f k q" and "∧ q k' . q ∈ states M ==> k' ≥ k ==> ofsm_table M f k' q = ofsm_table M f k q"
proof -
  
  have "∃ k . ∀ q ∈ states M . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q"
  proof -

    have "∃ fp . ∀ q k' . q ∈ states M ⟶ k' ≥ (fp q) ⟶ ofsm_table M f k' q = ofsm_table M f (fp q) q"
    proof 
      fix q
      let ?assignK = "λ q . SOME k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q"

      have "∧ q k' . q ∈ states M ==> k' ≥ ?assignK q ==> ofsm_table M f k' q = ofsm_table M f (?assignK q) q"
      proof -
        fix q k' assume "q ∈ states M" and "k' ≥ ?assignK q"
        then have p1: "finite (ofsm_table M f 0 q)"
          using fsm_states_finite assms(1)
          using infinite_super by fastforce 
    
        have "∃ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q"
          using finite_subset_mapping_limit[of "λ k . ofsm_table M f k q", OF p1 ofsm_table_subset] by metis
        have "∀ k' ≥ (?assignK q) . ofsm_table M f k' q = ofsm_table M f (?assignK q) q" 
          using someI_ex[of "λ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q", OF ‹∃ k . ∀ k' ≥ k . ofsm_table M f k' q = ofsm_table M f k q›] by assumption
        then show "ofsm_table M f k' q = ofsm_table M f (?assignK q) q" 
          using ‹k' ≥ ?assignK q› by blast
      qed
      then show "∀q k'. q ∈ states M ⟶ ?assignK q ≤ k' ⟶ ofsm_table M f k' q = ofsm_table M f (?assignK q) q" 
        by blast
    qed
    then obtain assignK where assignK_prop: "∧ q k' . q ∈ states M ==> k' ≥ assignK q ==> ofsm_table M f k' q = ofsm_table M f (assignK q) q" 
      by blast

    have "finite (assignK ` states M)"
      by (simp add: fsm_states_finite) 
    moreover have "assignK ` FSM.states M ≠ {}"
      using fsm_initial by auto
    ultimately obtain k where "k ∈ (assignK ` states M)" and "∧ k' . k' ∈ (assignK ` states M) ==> k' ≤ k"
      using Max_elem[OF ‹finite (assignK ` states M)› ‹assignK ` FSM.states M ≠ {}›] by (meson eq_Max_iff)

    have "∧ q k' . q ∈ states M ==> k' ≥ k ==> ofsm_table M f k' q = ofsm_table M f k q"
    proof -
      fix q k' assume "k' ≥ k" and "q ∈ states M"
      then have "k' ≥ assignK q"
        using ‹∧ k' . k' ∈ (assignK ` states M) ==> k' ≤ k›
        using dual_order.trans by auto 
      then show "ofsm_table M f k' q = ofsm_table M f k q"
        using assignK_prop ‹∧k'. k' ∈ assignK ` FSM.states M ==> k' ≤ k› ‹q ∈ FSM.states M› by blast
    qed
    then show ?thesis 
      by blast
  qed
  then obtain k where k_prop: "∧ q k' . q ∈ states M ==> k' ≥ k ==> ofsm_table M f k' q = ofsm_table M f k q"
    by blast
  then have "∧ q . q ∈ states M ==> ofsm_table M f k q = ofsm_table M f (Suc k) q"
    by (metis (full_types) le_SucI order_refl)

  
  let ?ks = "(Set.filter (λ k . ∀ q ∈ states M . ofsm_table M f k q = ofsm_table M f (Suc k) q) {..k})"
  have f1: "finite ?ks"
    by simp
  moreover have f2: "?ks ≠ {}"
    apply (clarsimp simp only: Set.filter_eq simp flip: ex_in_conv)
    using ‹∧q. q ∈ states M ==> ofsm_table M f k q = ofsm_table M f (Suc k) q›
    apply blast
    done
  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) Set.filter_eq mem_Collect_eq) 

  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›
        by (smt (verit, best) Set.filter_eq atMost_iff dual_order.refl mem_Collect_eq nat_less_le
            nat_neq_iff) 
      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 by (auto simp add: Let_def card_1_singleton_iff split: if_splits)
  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 \<in> states M"
  and     "i \<le> 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 \<ge> 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) \<open>Suc i \<le> j\<close> eq_iff le_SucI)+

  
  show ?case
    using Suc.hyps(1)[OF \<open>k = j - Suc i\<close> * \<open>Suc i \<le> j\<close>]
    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 \<in> 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 "\<And> q . q \<in> states M \<Longrightarrow> f q = ofsm_table M f 0 q"
    unfolding ofsm_table.simps by auto

  define n where n: "n = (\<lambda> i . card (ofsm_table M f i ` states M))"

  have "\<And> i j . i \<le> j \<Longrightarrow> n i \<le> n j"
    unfolding n
    using ofsm_table_refinement_card[OF assms(1), where A="states M"]
    by blast
  moreover have "\<And> i j m . i < j \<Longrightarrow> n i = n j \<Longrightarrow> j \<le> m \<Longrightarrow> n i = n m"
  proof -
    fix i j m assume "i < j" and "n i = n j" and "j \<le> m"
    then have "Suc i \<le> j" and "i \<le> Suc i" and "i \<le> m"
      by auto

    have "\<And> q . q \<in> states M \<Longrightarrow> ofsm_table M f j q = ofsm_table M f i q"
      using \<open>i < j\<close> \<open>n i = n j\<close> ofsm_table_refinement_card_fix[OF assms(1) _]
      unfolding n
      using less_imp_le_nat by presburger
    then have "\<And> q . q \<in> states M \<Longrightarrow> ofsm_table M f (Suc i) q = ofsm_table M f i q"
      using ofsm_table_subset[OF \<open>Suc i \<le> j\<close>, of M f]
      using ofsm_table_subset[OF \<open>i \<le> Suc i\<close>, of M f]
      by blast
    then have "\<And> q . q \<in> states M \<Longrightarrow> ofsm_table M f m q = ofsm_table M f i q"
      using ofsm_table_fixpoint[OF \<open>i \<le> m\<close>] 
      by metis
    then show "n i = n m"
      unfolding n
      by auto 
  qed
  moreover have "\<And> i . n i \<le> 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 \<le> 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 \<open>\<And> q . q \<in> states M \<Longrightarrow> f q = ofsm_table M f 0 q\<close>[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 \<le> m"
  and     "q \<in> 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) \<le> m - card (f ` states M)"
    using assms(2) by simp
  have **: "(size M - card (f ` states M)) \<le> Suc (m - card (f ` states M))"
    using assms(2) by simp

  have ***: "\<And> q . q \<in> FSM.states M \<Longrightarrow> 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 \<le> m"
  and     "q \<in> 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: "\<And> k' . k' \<ge> k \<Longrightarrow> 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: "\<And> k' . k' \<ge> m - card (f ` states M) \<Longrightarrow> 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 \<le> m - card (f ` states M)")
    case True
    show ?thesis
      using k1 k2[OF True] by simp
  next
    case False
    then have "k \<ge> 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 \<open>A minimisation function based on OFSM-tables\<close>


lemma language_equivalence_classes_preserve_observability:
  assumes "transitions M' = (\<lambda> t . ({q \<in> states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q \<in> states M . LS M q = LS M (t_target t)})) ` transitions M"
  and     "observable M"
shows "observable M'"
proof -
  have "\<And> t1 t2 . t1 \<in> transitions M' \<Longrightarrow>
                   t2 \<in> transitions M' \<Longrightarrow>
                    t_source t1 = t_source t2 \<Longrightarrow> 
                    t_input t1 = t_input t2 \<Longrightarrow> 
                    t_output t1 = t_output t2 \<Longrightarrow>
                    t_target t1 = t_target t2"
  proof -
    fix t1 t2 assume "t1 \<in> transitions M'" and "t2 \<in> 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 \<in> states M . LS M q = LS M (t_source t1')} , t_input t1', t_output t1', {q \<in> states M . LS M q = LS M (t_target t1')})"
                 and          "t1' \<in> transitions M"
      using \<open>t1 \<in> transitions M'\<close> assms(1) by auto
    obtain t2' where t2'_def: "t2 = ({q \<in> states M . LS M q = LS M (t_source t2')} , t_input t2', t_output t2', {q \<in> states M . LS M q = LS M (t_target t2')})"
                 and          "t2' \<in> transitions M"
      using \<open>t2 \<in> transitions M'\<close> assms(1) \<open>t_input t1 = t_input t2\<close> \<open>t_output t1 = t_output t2\<close> by auto

    have "{q \<in> FSM.states M. LS M q = LS M (t_source t1')} = {q \<in> FSM.states M. LS M q = LS M (t_source t2')}"
      using t1'_def t2'_def \<open>t_source t1 = t_source t2\<close>
      by (metis (no_types, lifting) fst_eqD)
    then have "LS M (t_source t1') = LS M (t_source t2')"
      using fsm_transition_source[OF \<open>t1' \<in> transitions M\<close>] fsm_transition_source[OF \<open>t2' \<in> transitions M\<close>] by blast
    then have "LS M (t_target t1') = LS M (t_target t2')"
      using observable_transition_target_language_eq[OF _ \<open>t1' \<in> transitions M\<close>  \<open>t2' \<in> transitions M\<close> _ _ \<open>observable M\<close>] 
      using \<open>t_input t1 = t_input t2\<close> \<open>t_output t1 = t_output t2\<close>
      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' = (\<lambda> t . ({q \<in> states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q \<in> states M . LS M q = LS M (t_target t)})) ` transitions M"
  and     "states M' = (\<lambda>q . {q' \<in> states M . LS M q = LS M q'}) ` states M"
  and     "initial M' = {q' \<in> 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: "\<And> io q . q \<in> states M \<Longrightarrow> (io \<in> LS M q) \<longleftrightarrow> (io \<in> LS M' {q' \<in> states M . LS M q = LS M q'})"
  proof -
    fix io q assume "q \<in> states M" 
    then show "(io \<in> LS M q) \<longleftrightarrow> (io \<in> LS M' {q' \<in> 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 \<in> LS M q \<Longrightarrow> xy#io \<in> LS M' {q' \<in> states M . LS M q = LS M q'}"
      proof -
        assume "xy#io \<in> 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' \<in> 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 \<open>p_io p = xy#io\<close> unfolding \<open>xy = (x,y)\<close> by auto
        moreover have "?t \<in> transitions M" and "path M (t_target ?t) ?p" and "t_source ?t = q"
          using \<open>path M q p\<close> path_cons_elim[of M q ?t ?p] calculation by auto
        ultimately have "[(x,y)] \<in> LS M q"
          unfolding LS_single_transition[of x y M q] by auto
        then have "io \<in> LS M (t_target ?t)"
          using observable_language_next[OF _ \<open>observable M\<close>, of "(x,y)" io, OF _ \<open>?t \<in> transitions M\<close>]
                \<open>xy#io \<in> LS M q\<close> 
          unfolding \<open>xy = (x,y)\<close> \<open>t_source ?t = q\<close> \<open>t_input ?t = x\<close> \<open>t_output ?t = y\<close> 
          by (metis \<open>?t \<in> FSM.transitions M\<close> from_FSM_language fsm_transition_target fst_conv snd_conv) 
        then have "io \<in> LS M' ?q'"
          using Cons.IH[OF fsm_transition_target[OF \<open>?t \<in> transitions M\<close>]] by blast
        then obtain p' where "path M' ?q' p'" and "p_io p' = io"
          by auto
        have *: "({q' \<in> states M . LS M q = LS M q'},x,y,{q' \<in> states M . LS M (t_target ?t) = LS M q'}) \<in> transitions M'"
          using \<open>?t \<in> transitions M\<close> \<open>t_source ?t = q\<close> \<open>t_input ?t = x\<close> \<open>t_output ?t = y\<close> 
          unfolding assms(1) by auto
        
        show "xy#io \<in> LS M' {q' \<in> states M . LS M q = LS M q'}"
          using LS_prepend_transition[OF * ] unfolding snd_conv fst_conv \<open>xy = (x,y)\<close>
          using \<open>io \<in> LS M' ?q'\<close> by blast
      qed
      moreover have "xy#io \<in> LS M' {q' \<in> states M . LS M q = LS M q'} \<Longrightarrow> xy#io \<in> LS M q"
      proof -
        let ?q = "{q' \<in> states M . LS M q = LS M q'}"
        assume "xy#io \<in> 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 \<open>p_io p = xy#io\<close> unfolding \<open>xy = (x,y)\<close> by auto
        then have "path M' ?q (?t#?p)"
          using \<open>path M' ?q p\<close> by auto
        then have "?t \<in> transitions M'" and "path M' (t_target ?t) ?p" and "t_source ?t = ?q"
          by force+
        then have "io \<in> LS M' (t_target ?t)"
          using \<open>p_io ?p = io\<close> by auto

        
        
        obtain t0 where t0_def: "?t = (\<lambda> t . ({q \<in> states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q \<in> states M . LS M q = LS M (t_target t)})) t0"
                    and "t0 \<in> transitions M"
          using \<open>?t \<in> transitions M'\<close> 
          unfolding assms(1)
          by auto
        then have "t_source t0 \<in> ?q" 
          using \<open>t_source ?t = ?q\<close>
          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)] \<in> LS M (t_source t0)"
          using t0_def \<open>t_input ?t = x\<close> \<open>t0 \<in> transitions M\<close> \<open>t_output ?t = y\<close> \<open>t_source t0 \<in> ?q\<close> unfolding LS_single_transition by auto
        ultimately obtain t where "t \<in> 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 _\<open>t \<in> transitions M\<close> \<open>t0 \<in> transitions M\<close> _ _ \<open>observable M\<close>]
          using \<open>LS M q = LS M (t_source t0)\<close> 
          unfolding \<open>t_source t = q\<close> \<open>t_input t = x\<close> \<open>t_output t = y\<close> 
          using t0_def \<open>t_input ?t = x\<close> \<open>t_output ?t = y\<close> 
          by auto
        moreover have "t_target ?t = {q' \<in> FSM.states M. LS M (t_target t) = LS M q'}"
          using calculation t0_def by fastforce
        ultimately have "io \<in> LS M (t_target t)"
          using Cons.IH[OF fsm_transition_target[OF \<open>t \<in> transitions M\<close>]]
                \<open>io \<in> LS M' (t_target ?t)\<close> 
          by auto
        then show "xy#io \<in> LS M q"
          unfolding \<open>t_source t = q\<close>[symmetric] \<open>xy = (x,y)\<close> 
          using \<open>t_input t = x\<close> \<open>t_output t = y\<close>
          using LS_prepend_transition \<open>t \<in> FSM.transitions M\<close> 
          by blast 
      qed

      ultimately show ?case 
        by blast
    qed
  qed

  have "L M' = LS M' {q' \<in> 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"\<And> q q' . q \<in> states M' \<Longrightarrow> q' \<in> states M' \<Longrightarrow> LS M' q = LS M' q' \<Longrightarrow> q = q'"
    proof -
     
      fix q q' assume "q \<in> states M'" and "q' \<in> states M'" and "LS M' q = LS M' q'"
  
      obtain qM where "q = {q \<in> states M . LS M qM = LS M q}" and "qM \<in> states M"
        using \<open>q \<in> states M'\<close> assms(2) by auto
      obtain qM' where "q' = {q \<in> states M . LS M qM' = LS M q}" and "qM' \<in> states M"
        using \<open>q' \<in> states M'\<close> assms(2) by auto
  
      have "LS M qM = LS M' q"
        using ls_prop[OF \<open>qM \<in> states M\<close>] unfolding \<open>q = {q \<in> states M . LS M qM = LS M q}\<close> by blast
      moreover have "LS M qM' = LS M' q'"
        using ls_prop[OF \<open>qM' \<in> states M\<close>] unfolding \<open>q' = {q \<in> states M . LS M qM' = LS M q}\<close> by blast
      ultimately have "LS M qM = LS M qM'"
        using \<open>LS M' q = LS M' q'\<close> by blast
      then show "q = q'"
        unfolding \<open>q = {q \<in> states M . LS M qM = LS M q}\<close> \<open>q' = {q \<in> states M . LS M qM' = LS M q}\<close> by blast
    qed
    then show ?thesis
      unfolding minimal_alt_def by blast
  qed
qed



fun minimise :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm \<Rightarrow> ('a set,'b,'c) fsm" where
  "minimise M = (let
      eq_class = ofsm_table_fix M (\<lambda>q . states M) 0;
      ts = (\<lambda> 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 (\<lambda>q . states M)"
proof -
  let ?r = "{(q1,q2) | q1 q2 . q1 \<in> states M \<and> q2 \<in> (\<lambda>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' \<in> states M . LS M q' = LS M (initial M)}"
and   "states (minimise M) = (\<lambda>q . {q' \<in> 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) = (\<lambda> t . ({q \<in> states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q \<in> states M . LS M q = LS M (t_target t)})) ` transitions M"
proof -

  let ?f = "\<lambda>q . states M"

  define eq_class where "eq_class = ofsm_table_fix M (\<lambda>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' ((\<lambda> t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))"
    by auto


  have **: "\<And> q . q \<in> states M \<Longrightarrow> eq_class q = {q' \<in> FSM.states M. LS M q = LS M q'}"
    using ofsm_table_fix_set[OF _ assms minimise_initial_partition] \<open>eq_class = ofsm_table_fix M ?f 0\<close>  after_is_state[OF \<open>observable M\<close>] by blast
  then have ****: "\<And> q . q \<in> states M \<Longrightarrow> eq_class q = {q' \<in> FSM.states M. LS M q' = LS M q}"
    using ofsm_table_fix_set[OF _ assms] \<open>eq_class = ofsm_table_fix M ?f 0\<close> by blast
  
  have ***: "(eq_class (initial M)) |\<in>| (eq_class |`| fstates M)"
    using fsm_initial[of M] fstates_set by fastforce

  have m1:"initial M' = {q' \<in> 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' = (\<lambda>q . {q' \<in> 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)) = (\<lambda>a. {aa \<in> FSM.states M. LS M a = LS M aa}) ` FSM.states M"
      using "**" by force
  qed  

open Derive_Util
    using create_unconnected_fsm_from_fsets_simps(3)[OF ***] finputs_setjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0

have "utputs '=outputsM"
using()OF*]foutputs_set 'def  metis

  have m5: "transitionselse Freebname, btype)|
    using       TFree _) = conv_func inner_term |

 ts=(\lambda .eq_class(t_source),t_input, t_outputt eq_class( ))`(transitions )
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
   -
    fixifvarTname =prod_type_namejava.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 48
    then obtain tMremove_constraints if  thendest_TFreeT|  K\^sort>open>ypeclose)|  elseT
                   and ( (,))
byjava.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for length 14

    have "t_source t \<in> states java.lang.StringIndexOutOfBoundsException: Index 8 out of bounds for length 8
      using let
      m2* *[OF fsm_transition_source[OF \<>tM\in  M\close]]  auto
    moreovervaltnameTs) = dest_Type
                  define_modular_instance() ,rvs lvprvpprod_term opT
have  < outputsM"
unfolding  [\<open> \in>transitions \close]by auto
    moreover have "t_target t \<in> states M'"
using[ <>tM\intransitions\close]
      unfolding m2  =.  prod_def_name
    ultimately show  (,,,,lthy define_modular_sum_prod prod_vars_raw prod_opT lthy
       java.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 13
  qed


    Local_Defs lthy' prod_def_thmsum_def_thm]modular_folded_thm
    using add_transitions_simps(1)[OF wf                    list_combmodular_unfolded)

  show "states (minimise M) = (\<lambda>q ] []]
    using add_transitions_simps

show    define_operations_rec_aux ty (p::ps) lthy = define_operations_rec_aux
    using add_transitions_simps(3)[OF wf] unfolding * m3 ,strict }  from_name 

  val  binders-body
using()OFwf unfolding   .

  show 
using5 wf **[ fsm_transition_source **OFfsm_transition_target unfolding * m5by auto
qed


lemma minimise_observable:
  assumes "               x:xs   Const<const_name<>.all\<lose,))  Absx ,abstractxs           
shows "observable (   # ty_info
  using language_equivalence_classes_preserve_observability
  by assumption
        
lemma minimise_minimal   constr_names\const_name<>Tagged_Prod_Sum.\<> else\^>\<openSum_TypeInl\<closejava.lang.StringIndexOutOfBoundsException: Index 142 out of bounds for length 142
         (, str_optT-  - T1> T2->  (,))
shows "minimal (minimise M)"
  using language_equivalence_classes_retain_language_and_induce_minimality     T2   t2in
  by assumption

lemma
  assumes "observable M"
shows "L (minimise M) = L M"
  Const  ->T
  by blast

lemma minimal_observable_code :
 " Mjava.lang.StringIndexOutOfBoundsException: Index 24 out of bounds for length 24
  shows "minimal M   ifHOLogicis_unithd)
proofcase tail_ctrsofjava.lang.StringIndexOutOfBoundsException: Index 63 out of bounds for length 63
  show "minimal M \<Longrightarrow> (\<forall> q \<in> states M . ofsm_table_fix M (\<lambda>q . states M) 0 q = {q})"
  proof 
    fix q assume "  ( ("" Long_Namebase_nametyco) dummyT)  conv_dummy 
    then showc: >
new_prefix
                 
      using after_is_state @
      by blast
  qed

  show "\<forall>q\<in>FSM.states M. ofsm_table_fix M
usingofsm_table_fix_setOF _<> M<> minimise_initial_partitionafter_is_stateOF <>observable\close>]
    unfolding minimal_alt_def 
    by blast
qed

lemma minimise_states_subset :
  assumes "observable M"
  and     "q \<in> states (minimise M)"
 q\subseteq "
  using assms(2) 
  unfoldingjava.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for length 39
  by auto                                  else |

lemma minimise_states_finite :
  [=if  thenmk_tagged_tuple_dummy'  . xs_to |
  and     "q \<in> states (minimise M)"
  shows "finite q"
  using minimise_states_subset[OFcase tail_ctrs of 
  using finite_subset by auto

end