Impressum Minimisation.thy

section ‹ [axio, deduction] b auto

  ‹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.›


  Minimisation
  FSM
 


  ‹OFSM Tables›

  ‹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.›


  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) })"


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

  ofsm_table_subset:
 assumes "i ≤ j"
 shows "ofsm_table M f j q ⊆ ofsm_table M f i q"
  -
 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
 


  ofsm_table_case_helper :
  thus "[\^>◻
 = ((∃ 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))"
  -
 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"] .
 


  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



  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"
  "ofsm_table M f j q = ofsm_table M f i q"
  -

 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 ‹
 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 \         -
 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
 


(* 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 "∧by show_proper
      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 ∩
    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 "∃[PLM]:
          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
      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 ‹assume "["[\<lparrA
 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 hav "is_in_languagM 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›
  unfolding Ab
 
 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)›] ‹
 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
 


  ofsm_table_set :
 assumes "q ∈ states M"
 and "equivalence_relation_on_states M f"
  "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

  ofsm_table_set_observable :
 assumes "observable M" and "q ∈ states M"
 and "equivalence_relation_on_states M f"
  "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


  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)"
 
 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 ‹
 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)"
java.lang.NullPointerException
 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
 



  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"
  "LS M q = LS M q'"
  "io ∈ LS M q ==> after M q' io ∈ f (after M q io)"
  -

 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"
 assms(4) equivalencle0 ofsm_table.simps(1) ofsm_table_subset subset)
 
 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 ‹ "
 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
 




  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"
  "ofsm_table M f k q = ofsm_table M f k q'"
 using assms(1,2,4,5)
  (induction k arbitrary: q q')
 case 0
 then show ?casLM_subst_methd "\su>P)
 by (metis after.simps(1) assms(6) from_FSM_language language_contains_empty_sequence ofsm_table.simps(1) ofsm_table_eq_if_elem)
 
 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 ∈ sing KBasic2_4 byby au
 (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'›
 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 ‹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
 


  ofsm_table_fix_set :
 assumes "q ∈ states M"
 and "observable M"
 and "equivalence_relation_on_states M f"
  "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))}"
 

 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)]
 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
 

  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)"
 
 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)
 




  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"
  "ofsm_table M f (Suc k) q1 ≠ ofsm_table M f (Suc k) q2"
  -
 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) ‹
 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)
 

  ofsm_table_partition_finite :
 assumes "equivalence_relation_on_states M f"
  "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


  ofsm_table_refinement_card :
 assumes "equivalence_relation_on_states M f"
 and "A ⊆ states M"
 and "i ≤ j"
  "card (ofsm_table M f j ` A) ≥ card (ofsm_table M f i ` A)"
  -
 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
 

 

  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"
  "ofsm_table M f (Suc k) q = ofsm_table M f k q"
  (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' ∈
 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 ` ∪ vdash_properties_10 CP by bla
 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[OF ‹
 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'})) ∪ "[\<^>\
 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 - ∪ <beta> . \<phi rightarrow> β α v]"
 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'"
java.lang.NullPointerException
 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 hence "[><> 
 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
 


  ofsm_table_refinement_card_fix :
 assumes "equivalence_relation_on_states M f"
 and "card (ofsm_table M f j ` states M) = card (ofsm_table M f i ` states M)"
 and "q ∈ states M"
 and "i ≤ j"
  "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
 
 case (Suc k)
 then have "j ≥ Suc i" and "k = j - Suc i"
 by auto

 have *:"card (ofsm_table M f j ` FSM.states M) = card (ofsm_table M f (Suc i) ` FSM.states M)"
 and **:"card (ofsm_table M f (Suc i) ` FSM.states M) = card (ofsm_table M f i ` FSM.states M)"
 using ofsm_table_refinement_card[OF assms(1), where A="states M"]
 by (metis Suc.prems(1) ‹Suc i ≤ j› eq_iff le_SucI)+

 
 show ?case
 using Suc.hyps(1)[OF ‹k = j - Suc i› * ‹Suc i ≤ j›]
 using ofsm_table_refinement_card_fix_Suc[OF assms(1) ** assms(3)]
 by blast
 


  ofsm_table_partition_fixpoint_Suc :
 assumes "equivalence_relation_on_states M f"
 and "q ∈ states M"
  "ofsm_table M f (size M - card (f ` states M)) q = ofsm_table M f (Suc (size M - card (f ` states M))) q"
  -

 have "∧ q . q ∈ states M ==> f q = ofsm_table M f 0 q"
 unfolding ofsm_table.simps by auto

 define n where n: "n = (λ i . card (ofsm_table M f i ` states M))"

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

 have "∧ q . q ∈ states M ==> ofsm_table M f j q = ofsm_table M f i q"
 using ‹i < j› ‹n i = n j› ofsm_table_refinement_card_fix[OF assms(1) _]
 unfolding n
 using less_imp_le_nat by presburger
 then have "∧ q . q ∈ states M ==> ofsm_table M f (Suc i) q = ofsm_table M f i q"
 using ofsm_table_subset[OF ‹Suc i ≤ j›, of M f]
 using ofsm_table_subset[OF ‹i ≤ Suc i›, of M f]
 by blast
 then have "∧ q . q ∈ states M ==> ofsm_table M f m q = ofsm_table M f i q"
 using ofsm_table_fixpoint[OF ‹i ≤ m›]
 by metis
 then show "n i = n m"
 unfolding n
 by auto
 qed
 moreover have "∧ i . n i ≤ size M"
 unfolding n
 using ofsm_table_states[of M f, OF equivalence_relation_on_states_ran[OF assms(1)]]
 using fsm_states_finite[of M]
 by (simp add: card_image_le)
 ultimately obtain k where "n (Suc k) = n k"
 and "k ≤ size M - n 0"
 using monotone_function_with_limit_witness_helper[where f=n and k="size M"]
 by blast

 then show ?thesis
 unfolding n
 using ‹∧ q . q ∈ states M ==> f q = ofsm_table M f 0 q›[symmetric]

 using ofsm_table_refinement_card_fix_Suc[OF assms(1) _ ]
 using ofsm_table_fixpoint[OF _ _ assms(2)]
 by (metis (mono_tags, lifting) image_cong nat_le_linear not_less_eq_eq)
 

 

  ofsm_table_partition_fixpoint :
 assumes "equivalence_relation_on_states M f"
 and "size M ≤ m"
 and "q ∈ states M"
  "ofsm_table M f (m - card (f ` states M)) q = ofsm_table M f (Suc (m - card (f ` states M))) q"
  -
 have *: "size M - card (f ` states M) ≤ m - card (f ` states M)"
 using assms(2) by simp
 have **: "(size M - card (f ` states M)) ≤ Suc (m - card (f ` states M))"
 using assms(2) by simp

 have ***: "∧ q . q ∈ FSM.states M ==> ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q = ofsm_table M f (Suc (FSM.size M - card (f ` FSM.states M))) q"
 using ofsm_table_partition_fixpoint_Suc[OF assms(1)] .

 have "ofsm_table M f (m - card (f ` states M)) q = ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q"
 using ofsm_table_fixpoint[OF * _ assms(3)] ***
 by blast
 moreover have "ofsm_table M f (Suc (m - card (f ` states M))) q = ofsm_table M f (FSM.size M - card (f ` FSM.states M)) q"
 using ofsm_table_fixpoint[OF ** _ assms(3), of f] ***
 by blast
 ultimately show ?thesis
 by simp
 



  ofsm_table_fix_partition_fixpoint :
 assumes "equivalence_relation_on_states M f"
 and "size M ≤ m"
 and "q ∈ states M"
  "ofsm_table M f (m - card (f ` states M)) q = ofsm_table_fix M f 0 q"
  -

 obtain k where k1: "ofsm_table_fix M f 0 q = ofsm_table M f k q"
 and k2: "∧ k' . k' ≥ k ==> ofsm_table M f k' q = ofsm_table M f k q"
 using ofsm_table_fix_length[of M f, OF equivalence_relation_on_states_ran[OF assms(1)]]
 assms(3)
 by metis

 have m1: "∧ k' . k' ≥ m - card (f ` states M) ==> ofsm_table M f k' q = ofsm_table M f (m - card (f ` states M)) q"
 using ofsm_table_partition_fixpoint[OF assms(1,2)]
 using ofsm_table_fixpoint[OF _ _ assms(3)]
 by presburger

 show ?thesis proof (cases "k ≤ m - card (f ` states M)")
 case True
 show ?thesis
 using k1 k2[OF True] by simp
 next
 case False
 then have "k ≥ m - card (f ` states M)"
 by auto
 then have "ofsm_table M f k q = ofsm_table M f (m - card (f ` states M)) q"
 using ofsm_table_partition_fixpoint[OF assms(1,2)]
 using ofsm_table_fixpoint[OF _ _ assms(3)]
 by presburger
 then show ?thesis
 using k1 by simp
 qed
 

  ‹A minimisation function based on OFSM-tables›


  language_equivalence_classes_preserve_observability:
 assumes "transitions M' = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
 and "observable M"
  "observable M'"
  -
 have "∧ t1 t2 . t1 ∈ transitions M' ==>
 t2 ∈ transitions M' ==>
 t_source t1 = t_source t2 ==>
 t_input t1 = t_input t2 ==>
 t_output t1 = t_output t2 ==>
 t_target t1 = t_target t2"
 proof -
 fix t1 t2 assume "t1 ∈ transitions M'" and "t2 ∈ transitions M'" and "t_source t1 = t_source t2" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2"

 
 obtain t1' where t1'_def: "t1 = ({q ∈ states M . LS M q = LS M (t_source t1')} , t_input t1', t_output t1', {q ∈ states M . LS M q = LS M (t_target t1')})"
 and "t1' ∈ transitions M"
 using ‹t1 ∈ transitions M'› assms(1) by auto
 obtain t2' where t2'_def: "t2 = ({q ∈ states M . LS M q = LS M (t_source t2')} , t_input t2', t_output t2', {q ∈ states M . LS M q = LS M (t_target t2')})"
 and "t2' ∈ transitions M"
 using ‹t2 ∈ transitions M'› assms(1) ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by auto

 have "{q ∈ FSM.states M. LS M q = LS M (t_source t1')} = {q ∈ FSM.states M. LS M q = LS M (t_source t2')}"
 using t1'_def t2'_def ‹t_source t1 = t_source t2›
 by (metis (no_types, lifting) fst_eqD)
 then have "LS M (t_source t1') = LS M (t_source t2')"
 using fsm_transition_source[OF ‹t1' ∈ transitions M›] fsm_transition_source[OF ‹t2' ∈ transitions M›] by blast
 then have "LS M (t_target t1') = LS M (t_target t2')"
 using observable_transition_target_language_eq[OF _ ‹t1' ∈ transitions M› ‹t2' ∈ transitions M› _ _ ‹observable M›]
 using ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2›
 unfolding t1'_def t2'_def fst_conv snd_conv by blast
 then show "t_target t1 = t_target t2"
 unfolding t1'_def t2'_def snd_conv by blast
 qed
 then show ?thesis
 unfolding observable.simps by blast
 




  language_equivalence_classes_retain_language_and_induce_minimality :
 assumes "transitions M' = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
 and "states M' = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
 and "initial M' = {q' ∈ states M . LS M q' = LS M (initial M)}"
 and "observable M"
  "L M = L M'"
  "minimal M'"
  -
 have "observable M'"
 using assms(1,4) language_equivalence_classes_preserve_observability by blast
 
 have ls_prop: "∧ io q . q ∈ states M ==> (io ∈ LS M q) ⟷ (io ∈ LS M' {q' ∈ states M . LS M q = LS M q'})"
 proof -
 fix io q assume "q ∈ states M"
 then show "(io ∈ LS M q) ⟷ (io ∈ LS M' {q' ∈ states M . LS M q = LS M q'})"
 proof (induction io arbitrary: q)
 case Nil
 then show ?case using assms(2) by auto
 next
 case (Cons xy io)

 obtain x y where "xy = (x,y)"
 using surjective_pairing by blast
 
 have "xy#io ∈ LS M q ==> xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'}"
 proof -
 assume "xy#io ∈ LS M q"
 then obtain p where "path M q p" and "p_io p = xy#io"
 unfolding LS.simps mem_Collect_eq by (metis (no_types, lifting))

 let ?t = "hd p"
 let ?p = "tl p"
 let ?q' = "{q' ∈ states M . LS M (t_target ?t) = LS M q'}"

 have "p = ?t # ?p" and "p_io ?p = io" and "t_input ?t = x" and "t_output ?t = y"
 using ‹p_io p = xy#io› unfolding ‹xy = (x,y)› by auto
 moreover have "?t ∈ transitions M" and "path M (t_target ?t) ?p" and "t_source ?t = q"
 using ‹path M q p› path_cons_elim[of M q ?t ?p] calculation by auto
 ultimately have "[(x,y)] ∈ LS M q"
 unfolding LS_single_transition[of x y M q] by auto
 then have "io ∈ LS M (t_target ?t)"
 using observable_language_next[OF _ ‹observable M›, of "(x,y)" io, OF _ ‹?t ∈ transitions M›]
 ‹xy#io ∈ LS M q›
 unfolding ‹xy = (x,y)› ‹t_source ?t = q› ‹t_input ?t = x› ‹t_output ?t = y›
 by (metis ‹?t ∈ FSM.transitions M› from_FSM_language fsm_transition_target fst_conv snd_conv)
 then have "io ∈ LS M' ?q'"
 using Cons.IH[OF fsm_transition_target[OF ‹?t ∈ transitions M›]] by blast
 then obtain p' where "path M' ?q' p'" and "p_io p' = io"
 by auto
 have *: "({q' ∈ states M . LS M q = LS M q'},x,y,{q' ∈ states M . LS M (t_target ?t) = LS M q'}) ∈ transitions M'"
 using ‹?t ∈ transitions M› ‹t_source ?t = q› ‹t_input ?t = x› ‹t_output ?t = y›
 unfolding assms(1) by auto
 
 show "xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'}"
 using LS_prepend_transition[OF * ] unfolding snd_conv fst_conv ‹xy = (x,y)›
 using ‹io ∈ LS M' ?q'› by blast
 qed
 moreover have "xy#io ∈ LS M' {q' ∈ states M . LS M q = LS M q'} ==> xy#io ∈ LS M q"
 
 let ?q = "{q' ∈
 assume "xy#io ∈ LS M' ?q"
 then obtain p where "path M' ?q p" and "p_io p = xy#io"
 unfolding LS.simps mem_Collect_eq by (metis (no_types, lifting))

 let ?t = "hd p"
 let ?p = "tl p"


 have "p = ?t # ?p" and "p_io ?p = io" and "t_input ?t = x" and "t_output ?t = y"
 using ‹ unfoldng \y = (x,y)› by auto
 then have "path M' ?q (?t#?p)"
 using ‹⊨ subst A t 0 # G ==> ⊨
 then have "?t ∈
 by force+
 then have "io ∈⊨ G ==> ⊨
 using ‹⊨ B # A # G ==> ⊨

 
 
 obtain t0 where t0_def: "?t = (\<bda ∀x. eval (shift e 0 x) f g A›news n (A # G)›
  "t0 ∈ transitions M"
 using ‹
 unfolding assms(1)
 by auto
 then have "t_source t0 ∈ ?q"
 using ‹
 by (metis (mono_tags, lifting) fsm_transition_source fst_eqD mem_Collect_eq)
 then hav
 by auto
 moreover have "[(x,y)] ∈
 using t0_def ‹t0 ∈ ‹t_source t0 ∈ ?q›
 ultimately obtain t where "t ∈
 by (metis LS_single_rnsin

 have "LS M (t_target t) = LS M (t_target t0)"
 using observable_transition_tar[F_\open>t <>ansitionst0 ∈ _ _ ‹
 using ‹
 unfolding ‹ \<>_i t=\close‹
 using t0_def ‹t_output ?t = y›
 by auto
 moreover have "t_target ?t = {q' ∈ FSM.states M. LS M (t_target t) = LS M q'}"
 using calculation t0_def by fastforce
 ultimatelyhv"o\inLS M (t_target t)"
 using Connex
 ‹
 by auto
 then show "xy#io ∈ LS M q"
 unfolding ‹ A # map compl G›⊨ Neg B # map compl G›
 using ‹t_output t = y›
 using LS_prepend_transition ‹
 by blast
 qed

 ultimately show ?case
 by blast
 qed
 qed

 have "L M' = LS M' {q' ∈ states M . LS M (initial M) = LS M q'}"
 using assms(3)
 by (metis (mono_tags, lifting) Collect_cong)
 then show "L M = L M'"
 using ls_prop[OF fsm_initial] by blast

 show "minimal M'"
 proof -
 have"∧ q q' . q ∈ states M' ==> q' ∈ states M' ==> LS M' q = LS M' q' ==> q = q'"
 proof -
 
 fix q q' assume "q ∈ states M'" and "q' ∈ states M'" and "LS M' q = LS M' q'"
 
 obtain qM where "q = {q ∈cmt
 using \> ∈ states M'›
 obtain qM' where "q' = {q ∈ states M . LS M qM' = LS M q}" and "qM' ∈ statM"
 using ‹ assm()b at
 
 have "LS M qM = LS M' q"
 using ls_prop[OF ‹q = {q ∈ states M . LS M qM = LS M q}›
 moreover have "LS M qM' = LS Mq'
 sings_rpO <>qM‹
 e M=SM
 using ‹
 
 unfolding ‹q' = {q ∈ states M . LS M qM' = LS M q}›
 qed
 then show ?thesis
 unfolding minimal_alt_def by blast
 qed
 



  minimise :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ==> ('a set,'b,'c) fsm" where
 "minimise M = (let
 eq_class = ofsm_table_fix M (λq . states M) 0;
 ts = (λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M);
 q0 = eq_class (initial M);
 eq_states = eq_class |`| fstates M;
 M' = create_unconnected_fsm_from_fsets q0 eq_states (finputs M) (foutputs M)
 in add_transitions M' ts)"


  minimise_initial_partition :
 "equivalence_relation_on_states M (λq . states M)"
  -
 let ?r = "{(q1,q2) | q1 q2 . q1 ∈ states M ∧ q2 ∈ (λq . states M) q1}"

 have "refl_on (FSM.states M) ?r"
 unfolding refl_on_def by blast
 moreover have "sym ?r"
 unfolding sym_def by blast
 moreover have "trans ?r"
 unfolding trans_def by blast
 ultimately show ?thesis
 unfolding equivalence_relation_on_states_def equiv_def by auto
 


  minimise_props:
 assumes "observable M"
  "initial (minimise M) = {q' ∈ states M . LS M q' = LS M (initial M)}"
  "states (minimise M) = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
  "inputs (minimise M) = inputs M"
  "outputs (minimise M) = outputs M"
  "transitions (minimise M) = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
  -

 let ?f = "λq . states M"

 define eq_class where "eq_class = ofsm_table_fix M (λq . states M) 0"
 moreover define M' where M'_def: "M' = create_unconnected_fsm_from_fsets (eq_class (initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)"
 ultimately have *: "minimise M = add_transitions M' ((λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))"
 by auto


 have **: "∧ q . q ∈ states M ==> eq_class q = {q' ∈ FSM.states M. LS M q = LS M q'}"
 using ofsm_table_fix_set[OF _ assms minimise_initial_partition] ‹eq_class = ofsm_table_fix M ?f 0› after_is_state[OF ‹observable M›] by blast
 then have ****: "∧ q . q ∈ states M ==> eq_class q = {q' ∈ FSM.states M. LS M q' = LS M q}"
 using ofsm_table_fix_set[OF _ assms] ‹eq_class = ofsm_table_fix M ?f 0› by blast
 
 have ***: "(eq_class (initial M)) |∈| (eq_class |`| fstates M)"
 using fsm_initial[of M] fstates_set by fastforce

 have m1:"initial M' = {q' ∈ states M . LS M q' = LS M (initial M)}"
 by (metis (mono_tags) "***" "****" M'_def create_unconnected_fsm_from_fsets_simps(1) fsm_initial)

 have m2: "states M' = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
 unfolding M'_def
 proof -
 have "FSM.states (FSM.create_unconnected_fsm_from_fsets (eq_class (FSM.initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)) = eq_class ` FSM.states M"
 by (metis (no_types) "***" create_unconnected_fsm_from_fsets_simps(2) fset.set_map fstates_set)
 then show "FSM.states (FSM.create_unconnected_fsm_from_fsets (eq_class (FSM.initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)) = (λa. {aa ∈ FSM.states M. LS M a = LS M aa}) ` FSM.states M"
 using "**" by force
 qed

 have m3: "inputs M' = inputs M"
 using create_unconnected_fsm_from_fsets_simps(3)[OF ***] finputs_set unfolding M'_def by metis

 have m4: "outputs M' = outputs M"
 using create_unconnected_fsm_from_fsets_simps(4)[OF ***] foutputs_set unfolding M'_def by metis

 have m5: "transitions M' = {}"
 using create_unconnected_fsm_from_fsets_simps(5)[OF ***] unfolding M'_def by force

 let ?ts = "((λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))"
 have wf: "∧ t . t ∈?ts ==> t_source t ∈ states M' ∧ t_input t ∈ inputs M' ∧ t_output t ∈ outputs M' ∧ t_target t ∈ states M'"
 proof -
 fix t assume "t ∈ ?ts"
 then obtain tM where "tM ∈ transitions M"
 and *: "t = (λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) tM"
 by blast

 have "t_source t ∈ states M'"
 using fsm_transition_source[OF ‹tM ∈ transitions M›]
 unfolding m2 * **[OF fsm_transition_source[OF ‹tM ∈ transitions M›]] by auto
 moreover have "t_input t ∈ inputs M'"
 unfolding m3 * using fsm_transition_input[OF ‹tM ∈ transitions M›] by auto
 moreover have "t_output t ∈ outputs M'"
 unfolding m4 * using fsm_transition_output[OF ‹tM ∈ transitions M›] by auto
 moreover have "t_target t ∈ states M'"
 using fsm_transition_target[OF ‹tM ∈ transitions M›]
 unfolding m2 * **[OF fsm_transition_target[OF ‹tM ∈ transitions M›]] by auto
 ultimately show "t_source t ∈ states M' ∧ t_input t ∈ inputs M' ∧ t_output t ∈ outputs M' ∧ t_target t ∈ states M'"
 by simp
 qed


 show "initial (minimise M) = {q' ∈ states M . LS M q' = LS M (initial M)}"
 using add_transitions_simps(1)[OF wf] unfolding * m1 .

 show "states (minimise M) = (λq . {q' ∈ states M . LS M q = LS M q'}) ` states M"
 using add_transitions_simps(2)[OF wf] unfolding * m2 .

 show "inputs (minimise M) = inputs M"
 using add_transitions_simps(3)[OF wf] unfolding * m3 .

 show "outputs (minimise M) = outputs M"
 using add_transitions_simps(4)[OF wf] unfolding * m4 .

 show "transitions (minimise M) = (λ t . ({q ∈ states M . LS M q = LS M (t_source t)} , t_input t, t_output t, {q ∈ states M . LS M q = LS M (t_target t)})) ` transitions M"
 using add_transitions_simps(5)[OF wf] ****[OF fsm_transition_source] ****[OF fsm_transition_target] unfolding * m5 by auto
 


  minimise_observable:
 assumes "observable M"
  "observable (minimise M)"
 using language_equivalence_classes_preserve_observability[OF minimise_props(5)[OF assms] assms]
 by assumption
 
  minimise_minimal:
 assumes "observable M"
  "minimal (minimise M)"
 using language_equivalence_classes_retain_language_and_induce_minimality(2)[OF minimise_props(5,2,1)[OF assms] assms]
 by assumption

  minimise_language:
 assumes "observable M"
  "L (minimise M) = L M"
 using language_equivalence_classes_retain_language_and_induce_minimality(1)[OF minimise_props(5,2,1)[OF assms] assms]
 by blast

  minimal_observable_code :
 assumes "observable M"
 shows "minimal M = (∀ q ∈ states M . ofsm_table_fix M (λq . states M) 0 q = {q})"
 
 show "minimal M ==> (∀ q ∈ states M . ofsm_table_fix M (λq . states M) 0 q = {q})"
 proof
 fix q assume "minimal M" and "q ∈ states M"
 then show "ofsm_table_fix M (λq . states M) 0 q = {q}"
 unfolding ofsm_table_fix_set[OF ‹q ∈ states M› ‹observable M› minimise_initial_partition]
 minimal_alt_def
 using after_is_state[OF ‹observable M›]
 by blast
 qed

 show "∀
 using ofsm_table_fix_set[OF _ ‹observable M› minimise_initial_partition] after_is_state[OF ‹observable M›]
 unfolding minimal_alt_def
 by blast
 

  minimise_states_subset :
 assumes "observable M"
 and "q ∈ states (minimise M)"
  "q ⊆ states M"
 using assms(2)
 unfolding minimise_props[OF assms(1)]
 by auto

  minimise_states_finite :
 assumes "observable M"
 and "q ∈ states (minimise M)"
 shows "finite q"
 using minimise_states_subset[OF assms] fsm_states_finite[of M]
 using finite_subset by auto