# Theory Myhill_1

```(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
theory Myhill_1
imports Folds
"HOL-Library.While_Combinator"
begin

section ‹First direction of MN: ‹finite partition ⇒ regular language››

notation
conc (infixr "⋅" 100) and
star ("_⋆" [101] 102)

lemma Pair_Collect [simp]:
shows "(x, y) ∈ {(x, y). P x y} ⟷ P x y"
by simp

text ‹Myhill-Nerode relation›

definition
str_eq :: "'a lang ⇒ ('a list × 'a list) set" ("≈_" [100] 100)
where
"≈A ≡ {(x, y).  (∀z. x @ z ∈ A ⟷ y @ z ∈ A)}"

abbreviation
str_eq_applied :: "'a list ⇒ 'a lang ⇒ 'a list ⇒ bool" ("_ ≈_ _")
where
"x ≈A y ≡ (x, y) ∈ ≈A"

lemma str_eq_conv_Derivs:
"str_eq A = {(u,v). Derivs u A = Derivs v A}"
by (auto simp: str_eq_def Derivs_def)

definition
finals :: "'a lang ⇒ 'a lang set"
where
"finals A ≡ {≈A `` {s} | s . s ∈ A}"

lemma lang_is_union_of_finals:
shows "A = ⋃(finals A)"
unfolding finals_def
unfolding Image_def
unfolding str_eq_def
by (auto) (metis append_Nil2)

lemma finals_in_partitions:
shows "finals A ⊆ (UNIV // ≈A)"
unfolding finals_def quotient_def
by auto

subsection ‹Equational systems›

text ‹The two kinds of terms in the rhs of equations.›

datatype 'a trm =
Lam "'a rexp"            (* Lambda-marker *)
| Trn "'a lang" "'a rexp"     (* Transition *)

fun
lang_trm::"'a trm ⇒ 'a lang"
where
"lang_trm (Lam r) = lang r"
| "lang_trm (Trn X r) = X ⋅ lang r"

fun
lang_rhs::"('a trm) set ⇒ 'a lang"
where
"lang_rhs rhs = ⋃ (lang_trm ` rhs)"

lemma lang_rhs_set:
shows "lang_rhs {Trn X r | r. P r} = ⋃{lang_trm (Trn X r) | r. P r}"
by (auto)

lemma lang_rhs_union_distrib:
shows "lang_rhs A ∪ lang_rhs B = lang_rhs (A ∪ B)"
by simp

text ‹Transitions between equivalence classes›

definition
transition :: "'a lang ⇒ 'a ⇒ 'a lang ⇒ bool" ("_ ⊨_⇒_" [100,100,100] 100)
where
"Y ⊨c⇒ X ≡ Y ⋅ {[c]} ⊆ X"

text ‹Initial equational system›

definition
"Init_rhs CS X ≡
if ([] ∈ X) then
{Lam One} ∪ {Trn Y (Atom c) | Y c. Y ∈ CS ∧ Y ⊨c⇒ X}
else
{Trn Y (Atom c)| Y c. Y ∈ CS ∧ Y ⊨c⇒ X}"

definition
"Init CS ≡ {(X, Init_rhs CS X) | X.  X ∈ CS}"

subsection ‹Arden Operation on equations›

fun
Append_rexp :: "'a rexp ⇒ 'a trm ⇒ 'a trm"
where
"Append_rexp r (Lam rexp)   = Lam (Times rexp r)"
| "Append_rexp r (Trn X rexp) = Trn X (Times rexp r)"

definition
"Append_rexp_rhs rhs rexp ≡ (Append_rexp rexp) ` rhs"

definition
"Arden X rhs ≡
Append_rexp_rhs (rhs - {Trn X r | r. Trn X r ∈ rhs}) (Star (⨄ {r. Trn X r ∈ rhs}))"

subsection ‹Substitution Operation on equations›

definition
"Subst rhs X xrhs ≡
(rhs - {Trn X r | r. Trn X r ∈ rhs}) ∪ (Append_rexp_rhs xrhs (⨄ {r. Trn X r ∈ rhs}))"

definition
Subst_all :: "('a lang × ('a trm) set) set ⇒ 'a lang ⇒ ('a trm) set ⇒ ('a lang × ('a trm) set) set"
where
"Subst_all ES X xrhs ≡ {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) ∈ ES}"

definition
"Remove ES X xrhs ≡
Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"

subsection ‹While-combinator and invariants›

definition
"Iter X ES ≡ (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) ∈ ES ∧ X ≠ Y
in Remove ES Y yrhs)"

lemma IterI2:
assumes "(Y, yrhs) ∈ ES"
and     "X ≠ Y"
and     "⋀Y yrhs. ⟦(Y, yrhs) ∈ ES; X ≠ Y⟧ ⟹ Q (Remove ES Y yrhs)"
shows "Q (Iter X ES)"
unfolding Iter_def using assms
by (rule_tac a="(Y, yrhs)" in someI2) (auto)

abbreviation
"Cond ES ≡ card ES ≠ 1"

definition
"Solve X ES ≡ while Cond (Iter X) ES"

definition
"distinctness ES ≡
∀ X rhs rhs'. (X, rhs) ∈ ES ∧ (X, rhs') ∈ ES ⟶ rhs = rhs'"

definition
"soundness ES ≡ ∀(X, rhs) ∈ ES. X = lang_rhs rhs"

definition
"ardenable rhs ≡ (∀ Y r. Trn Y r ∈ rhs ⟶ [] ∉ lang r)"

definition
"ardenable_all ES ≡ ∀(X, rhs) ∈ ES. ardenable rhs"

definition
"finite_rhs ES ≡ ∀(X, rhs) ∈ ES. finite rhs"

lemma finite_rhs_def2:
"finite_rhs ES = (∀ X rhs. (X, rhs) ∈ ES ⟶ finite rhs)"
unfolding finite_rhs_def by auto

definition
"rhss rhs ≡ {X | X r. Trn X r ∈ rhs}"

definition
"lhss ES ≡ {Y | Y yrhs. (Y, yrhs) ∈ ES}"

definition
"validity ES ≡ ∀(X, rhs) ∈ ES. rhss rhs ⊆ lhss ES"

lemma rhss_union_distrib:
shows "rhss (A ∪ B) = rhss A ∪ rhss B"

lemma lhss_union_distrib:
shows "lhss (A ∪ B) = lhss A ∪ lhss B"

definition
"invariant ES ≡ finite ES
∧ finite_rhs ES
∧ soundness ES
∧ distinctness ES
∧ ardenable_all ES
∧ validity ES"

lemma invariantI:
assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES"
"finite_rhs ES" "validity ES"
shows "invariant ES"
using assms by (simp add: invariant_def)

lemma finite_Trn:
assumes fin: "finite rhs"
shows "finite {r. Trn Y r ∈ rhs}"
using assms by (auto intro!: finite_vimageI simp add: inj_on_def)

lemma finite_Lam:
assumes fin: "finite rhs"
shows "finite {r. Lam r ∈ rhs}"
using assms by (auto intro!: finite_vimageI simp add: inj_on_def)

lemma trm_soundness:
assumes finite:"finite rhs"
shows "lang_rhs ({Trn X r| r. Trn X r ∈ rhs}) = X ⋅ (lang (⨄{r. Trn X r ∈ rhs}))"
proof -
have "finite {r. Trn X r ∈ rhs}"
by (rule finite_Trn[OF finite])
then show "lang_rhs ({Trn X r| r. Trn X r ∈ rhs}) = X ⋅ (lang (⨄{r. Trn X r ∈ rhs}))"
by (simp only: lang_rhs_set lang_trm.simps) (auto simp add: conc_def)
qed

lemma lang_of_append_rexp:
"lang_trm (Append_rexp r trm) = lang_trm trm ⋅ lang r"
by (induct rule: Append_rexp.induct)

lemma lang_of_append_rexp_rhs:
"lang_rhs (Append_rexp_rhs rhs r) = lang_rhs rhs ⋅ lang r"
unfolding Append_rexp_rhs_def
by (auto simp add: conc_def lang_of_append_rexp)

subsection ‹Intial Equational Systems›

lemma defined_by_str:
assumes "s ∈ X" "X ∈ UNIV // ≈A"
shows "X = ≈A `` {s}"
using assms
unfolding quotient_def Image_def str_eq_def
by auto

lemma every_eqclass_has_transition:
assumes has_str: "s @ [c] ∈ X"
and     in_CS:   "X ∈ UNIV // ≈A"
obtains Y where "Y ∈ UNIV // ≈A" and "Y ⋅ {[c]} ⊆ X" and "s ∈ Y"
proof -
define Y where "Y = ≈A `` {s}"
have "Y ∈ UNIV // ≈A"
unfolding Y_def quotient_def by auto
moreover
have "X = ≈A `` {s @ [c]}"
using has_str in_CS defined_by_str by blast
then have "Y ⋅ {[c]} ⊆ X"
unfolding Y_def Image_def conc_def
unfolding str_eq_def
by clarsimp
moreover
have "s ∈ Y" unfolding Y_def
unfolding Image_def str_eq_def by simp
ultimately show thesis using that by blast
qed

lemma l_eq_r_in_eqs:
assumes X_in_eqs: "(X, rhs) ∈ Init (UNIV // ≈A)"
shows "X = lang_rhs rhs"
proof
show "X ⊆ lang_rhs rhs"
proof
fix x
assume in_X: "x ∈ X"
{ assume empty: "x = []"
then have "x ∈ lang_rhs rhs" using X_in_eqs in_X
unfolding Init_def Init_rhs_def
by auto
}
moreover
{ assume not_empty: "x ≠ []"
then obtain s c where decom: "x = s @ [c]"
using rev_cases by blast
have "X ∈ UNIV // ≈A" using X_in_eqs unfolding Init_def by auto
then obtain Y where "Y ∈ UNIV // ≈A" "Y ⋅ {[c]} ⊆ X" "s ∈ Y"
using decom in_X every_eqclass_has_transition by metis
then have "x ∈ lang_rhs {Trn Y (Atom c)| Y c. Y ∈ UNIV // ≈A ∧ Y ⊨c⇒ X}"
unfolding transition_def
using decom by (force simp add: conc_def)
then have "x ∈ lang_rhs rhs" using X_in_eqs in_X
unfolding Init_def Init_rhs_def by simp
}
ultimately show "x ∈ lang_rhs rhs" by blast
qed
next
show "lang_rhs rhs ⊆ X" using X_in_eqs
unfolding Init_def Init_rhs_def transition_def
by auto
qed

lemma finite_Init_rhs:
fixes CS::"(('a::finite) lang) set"
assumes finite: "finite CS"
shows "finite (Init_rhs CS X)"
using assms unfolding Init_rhs_def transition_def by simp

lemma Init_ES_satisfies_invariant:
fixes A::"(('a::finite) lang)"
assumes finite_CS: "finite (UNIV // ≈A)"
shows "invariant (Init (UNIV // ≈A))"
proof (rule invariantI)
show "soundness (Init (UNIV // ≈A))"
unfolding soundness_def
using l_eq_r_in_eqs by auto
show "finite (Init (UNIV // ≈A))" using finite_CS
unfolding Init_def by simp
show "distinctness (Init (UNIV // ≈A))"
unfolding distinctness_def Init_def by simp
show "ardenable_all (Init (UNIV // ≈A))"
unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def
by auto
show "finite_rhs (Init (UNIV // ≈A))"
using finite_Init_rhs[OF finite_CS]
unfolding finite_rhs_def Init_def by auto
show "validity (Init (UNIV // ≈A))"
unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def
by auto
qed

subsection ‹Interations›

lemma Arden_preserves_soundness:
assumes l_eq_r: "X = lang_rhs rhs"
and not_empty: "ardenable rhs"
and finite: "finite rhs"
shows "X = lang_rhs (Arden X rhs)"
proof -
define A where "A = lang (⨄{r. Trn X r ∈ rhs})"
define b where "b = {Trn X r | r. Trn X r ∈ rhs}"
define B where "B = lang_rhs (rhs - b)"
have not_empty2: "[] ∉ A"
using finite_Trn[OF finite] not_empty
unfolding A_def ardenable_def by simp
have "X = lang_rhs rhs" using l_eq_r by simp
also have "… = lang_rhs (b ∪ (rhs - b))" unfolding b_def by auto
also have "… = lang_rhs b ∪ B" unfolding B_def by (simp only: lang_rhs_union_distrib)
also have "… = X ⋅ A ∪ B"
unfolding b_def
unfolding trm_soundness[OF finite]
unfolding A_def
by blast
finally have "X = X ⋅ A ∪ B" .
then have "X = B ⋅ A⋆"
also have "… = lang_rhs (Arden X rhs)"
unfolding Arden_def A_def B_def b_def
by (simp only: lang_of_append_rexp_rhs lang.simps)
finally show "X = lang_rhs (Arden X rhs)" by simp
qed

lemma Append_preserves_finite:
"finite rhs ⟹ finite (Append_rexp_rhs rhs r)"
by (auto simp: Append_rexp_rhs_def)

lemma Arden_preserves_finite:
"finite rhs ⟹ finite (Arden X rhs)"
by (auto simp: Arden_def Append_preserves_finite)

lemma Append_preserves_ardenable:
"ardenable rhs ⟹ ardenable (Append_rexp_rhs rhs r)"
apply (auto simp: ardenable_def Append_rexp_rhs_def)
by (case_tac x, auto simp: conc_def)

lemma ardenable_set_sub:
"ardenable rhs ⟹ ardenable (rhs - A)"
by (auto simp:ardenable_def)

lemma ardenable_set_union:
"⟦ardenable rhs; ardenable rhs'⟧ ⟹ ardenable (rhs ∪ rhs')"
by (auto simp:ardenable_def)

lemma Arden_preserves_ardenable:
"ardenable rhs ⟹ ardenable (Arden X rhs)"
by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub)

lemma Subst_preserves_ardenable:
"⟦ardenable rhs; ardenable xrhs⟧ ⟹ ardenable (Subst rhs X xrhs)"
by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub)

lemma Subst_preserves_soundness:
assumes substor: "X = lang_rhs xrhs"
and finite: "finite rhs"
shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right")
proof-
define A where "A = lang_rhs (rhs - {Trn X r | r. Trn X r ∈ rhs})"
have "?Left = A ∪ lang_rhs (Append_rexp_rhs xrhs (⨄{r. Trn X r ∈ rhs}))"
unfolding Subst_def
unfolding lang_rhs_union_distrib[symmetric]
moreover have "?Right = A ∪ lang_rhs {Trn X r | r. Trn X r ∈ rhs}"
proof-
have "rhs = (rhs - {Trn X r | r. Trn X r ∈ rhs}) ∪ ({Trn X r | r. Trn X r ∈ rhs})" by auto
thus ?thesis
unfolding A_def
unfolding lang_rhs_union_distrib
by simp
qed
moreover
have "lang_rhs (Append_rexp_rhs xrhs (⨄{r. Trn X r ∈ rhs})) = lang_rhs {Trn X r | r. Trn X r ∈ rhs}"
using finite substor by (simp only: lang_of_append_rexp_rhs trm_soundness)
ultimately show ?thesis by simp
qed

lemma Subst_preserves_finite_rhs:
"⟦finite rhs; finite yrhs⟧ ⟹ finite (Subst rhs Y yrhs)"
by (auto simp: Subst_def Append_preserves_finite)

lemma Subst_all_preserves_finite:
assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
using assms unfolding Subst_all_def by simp

declare [[simproc del: finite_Collect]]

lemma Subst_all_preserves_finite_rhs:
"⟦finite_rhs ES; finite yrhs⟧ ⟹ finite_rhs (Subst_all ES Y yrhs)"
by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def)

lemma append_rhs_preserves_cls:
"rhss (Append_rexp_rhs rhs r) = rhss rhs"
apply (auto simp: rhss_def Append_rexp_rhs_def)
apply (case_tac xa, auto simp: image_def)
by (rule_tac x = "Times ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)

lemma Arden_removes_cl:
"rhss (Arden Y yrhs) = rhss yrhs - {Y}"
by (auto simp: rhss_def)

lemma lhss_preserves_cls:
"lhss (Subst_all ES Y yrhs) = lhss ES"
by (auto simp: lhss_def Subst_all_def)

"X ∉ rhss xrhs ⟹
rhss (Subst rhs X xrhs) = rhss rhs ∪ rhss xrhs - {X}"
apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib)
by (auto simp: rhss_def)

lemma Subst_all_preserves_validity:
assumes sc: "validity (ES ∪ {(Y, yrhs)})"        (is "validity ?A")
shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
proof -
{ fix X xrhs'
assume "(X, xrhs') ∈ ?B"
then obtain xrhs
where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
and X_in: "(X, xrhs) ∈ ES" by (simp add:Subst_all_def, blast)
have "rhss xrhs' ⊆ lhss ?B"
proof-
have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
moreover have "rhss xrhs' ⊆ lhss ES"
proof-
have "rhss xrhs' ⊆  rhss xrhs ∪ rhss (Arden Y yrhs) - {Y}"
proof -
have "Y ∉ rhss (Arden Y yrhs)"
using Arden_removes_cl by auto
thus ?thesis using xrhs_xrhs' by (auto simp: Subst_updates_cls)
qed
moreover have "rhss xrhs ⊆ lhss ES ∪ {Y}" using X_in sc
apply (simp only:validity_def lhss_union_distrib)
by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
moreover have "rhss (Arden Y yrhs) ⊆ lhss ES ∪ {Y}"
using sc
by (auto simp add: Arden_removes_cl validity_def lhss_def)
ultimately show ?thesis by auto
qed
ultimately show ?thesis by simp
qed
} thus ?thesis by (auto simp only:Subst_all_def validity_def)
qed

lemma Subst_all_satisfies_invariant:
assumes invariant_ES: "invariant (ES ∪ {(Y, yrhs)})"
shows "invariant (Subst_all ES Y (Arden Y yrhs))"
proof (rule invariantI)
have Y_eq_yrhs: "Y = lang_rhs yrhs"
using invariant_ES by (simp only:invariant_def soundness_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
have ardenable_yrhs: "ardenable yrhs"
using invariant_ES by (auto simp:invariant_def ardenable_all_def)
show "soundness (Subst_all ES Y (Arden Y yrhs))"
proof -
have "Y = lang_rhs (Arden Y yrhs)"
using Y_eq_yrhs invariant_ES finite_yrhs
using finite_Trn[OF finite_yrhs]
apply(rule_tac Arden_preserves_soundness)
apply(simp_all)
unfolding invariant_def ardenable_all_def ardenable_def
apply(auto)
done
thus ?thesis using invariant_ES
unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps)
qed
show "finite (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite)
show "distinctness (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES
unfolding distinctness_def Subst_all_def invariant_def by auto
show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
proof -
{ fix X rhs
assume "(X, rhs) ∈ ES"
hence "ardenable rhs"  using invariant_ES
with ardenable_yrhs
have "ardenable (Subst rhs Y (Arden Y yrhs))"
Subst_preserves_ardenable Arden_preserves_ardenable)
} thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
qed
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
proof-
have "finite_rhs ES" using invariant_ES
moreover have "finite (Arden Y yrhs)"
proof -
have "finite yrhs" using invariant_ES
by (auto simp:invariant_def finite_rhs_def)
thus ?thesis using Arden_preserves_finite by auto
qed
ultimately show ?thesis
qed
show "validity (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def)
qed

lemma Remove_in_card_measure:
assumes finite: "finite ES"
and     in_ES: "(X, rhs) ∈ ES"
shows "(Remove ES X rhs, ES) ∈ measure card"
proof -
define f where "f x = ((fst x)::'a lang, Subst (snd x) X (Arden X rhs))" for x
define ES' where "ES' = ES - {(X, rhs)}"
have "Subst_all ES' X (Arden X rhs) = f ` ES'"
apply (auto simp: Subst_all_def f_def image_def)
by (rule_tac x = "(Y, yrhs)" in bexI, simp+)
then have "card (Subst_all ES' X (Arden X rhs)) ≤ card ES'"
unfolding ES'_def using finite by (auto intro: card_image_le)
also have "… < card ES" unfolding ES'_def
using in_ES finite by (rule_tac card_Diff1_less)
finally show "(Remove ES X rhs, ES) ∈ measure card"
unfolding Remove_def ES'_def by simp
qed

lemma Subst_all_cls_remains:
"(X, xrhs) ∈ ES ⟹ ∃ xrhs'. (X, xrhs') ∈ (Subst_all ES Y yrhs)"
by (auto simp: Subst_all_def)

lemma card_noteq_1_has_more:
assumes card:"Cond ES"
and e_in: "(X, xrhs) ∈ ES"
and finite: "finite ES"
shows "∃(Y, yrhs) ∈ ES. (X, xrhs) ≠ (Y, yrhs)"
proof-
have "card ES > 1" using card e_in finite
by (cases "card ES") (auto)
then have "card (ES - {(X, xrhs)}) > 0"
using finite e_in by auto
then have "(ES - {(X, xrhs)}) ≠ {}" using finite by (rule_tac notI, simp)
then show "∃(Y, yrhs) ∈ ES. (X, xrhs) ≠ (Y, yrhs)"
by auto
qed

lemma iteration_step_measure:
assumes Inv_ES: "invariant ES"
and    X_in_ES: "(X, xrhs) ∈ ES"
and    Cnd:     "Cond ES "
shows "(Iter X ES, ES) ∈ measure card"
proof -
have fin: "finite ES" using Inv_ES unfolding invariant_def by simp
then obtain Y yrhs
where Y_in_ES: "(Y, yrhs) ∈ ES" and not_eq: "(X, xrhs) ≠ (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) ∈ ES " "X ≠ Y"
using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "(Iter X ES, ES) ∈ measure card"
apply(rule IterI2)
apply(rule Remove_in_card_measure)
done
qed

lemma iteration_step_invariant:
assumes Inv_ES: "invariant ES"
and    X_in_ES: "(X, xrhs) ∈ ES"
and    Cnd: "Cond ES"
shows "invariant (Iter X ES)"
proof -
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
then obtain Y yrhs
where Y_in_ES: "(Y, yrhs) ∈ ES" and not_eq: "(X, xrhs) ≠ (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) ∈ ES" "X ≠ Y"
using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "invariant (Iter X ES)"
proof(rule IterI2)
fix Y yrhs
assume h: "(Y, yrhs) ∈ ES" "X ≠ Y"
then have "ES - {(Y, yrhs)} ∪ {(Y, yrhs)} = ES" by auto
then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
using Inv_ES
by (rule_tac Subst_all_satisfies_invariant) (simp)
qed
qed

lemma iteration_step_ex:
assumes Inv_ES: "invariant ES"
and    X_in_ES: "(X, xrhs) ∈ ES"
and    Cnd: "Cond ES"
shows "∃xrhs'. (X, xrhs') ∈ (Iter X ES)"
proof -
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
then obtain Y yrhs
where "(Y, yrhs) ∈ ES" "(X, xrhs) ≠ (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) ∈ ES " "X ≠ Y"
using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "∃xrhs'. (X, xrhs') ∈ (Iter X ES)"
apply(rule IterI2)
unfolding Remove_def
apply(rule Subst_all_cls_remains)
using X_in_ES
apply(auto)
done
qed

subsection ‹The conclusion of the first direction›

lemma Solve:
fixes A::"('a::finite) lang"
assumes fin: "finite (UNIV // ≈A)"
and     X_in: "X ∈ (UNIV // ≈A)"
shows "∃rhs. Solve X (Init (UNIV // ≈A)) = {(X, rhs)} ∧ invariant {(X, rhs)}"
proof -
define Inv where "Inv ES ⟷ invariant ES ∧ (∃rhs. (X, rhs) ∈ ES)" for ES
have "Inv (Init (UNIV // ≈A))" unfolding Inv_def
moreover
{ fix ES
assume inv: "Inv ES" and crd: "Cond ES"
then have "Inv (Iter X ES)"
unfolding Inv_def
by (auto simp add: iteration_step_invariant iteration_step_ex) }
moreover
{ fix ES
assume inv: "Inv ES" and not_crd: "¬Cond ES"
from inv obtain rhs where "(X, rhs) ∈ ES" unfolding Inv_def by auto
moreover
from not_crd have "card ES = 1" by simp
ultimately
have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq)
then have "∃rhs'. ES = {(X, rhs')} ∧ invariant {(X, rhs')}" using inv
unfolding Inv_def by auto }
moreover
have "wf (measure card)" by simp
moreover
{ fix ES
assume inv: "Inv ES" and crd: "Cond ES"
then have "(Iter X ES, ES) ∈ measure card"
unfolding Inv_def
apply(clarify)
apply(rule_tac iteration_step_measure)
apply(auto)
done }
ultimately
show "∃rhs. Solve X (Init (UNIV // ≈A)) = {(X, rhs)} ∧ invariant {(X, rhs)}"
unfolding Solve_def by (rule while_rule)
qed

lemma every_eqcl_has_reg:
fixes A::"('a::finite) lang"
assumes finite_CS: "finite (UNIV // ≈A)"
and X_in_CS: "X ∈ (UNIV // ≈A)"
shows "∃r. X = lang r"
proof -
from finite_CS X_in_CS
obtain xrhs where Inv_ES: "invariant {(X, xrhs)}"
using Solve by metis

define A where "A = Arden X xrhs"
have "rhss xrhs ⊆ {X}" using Inv_ES
unfolding validity_def invariant_def rhss_def lhss_def
by auto
then have "rhss A = {}" unfolding A_def
then have eq: "{Lam r | r. Lam r ∈ A} = A" unfolding rhss_def
by (auto, case_tac x, auto)

have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
using Arden_preserves_finite by auto
then have fin: "finite {r. Lam r ∈ A}" by (rule finite_Lam)

have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def
by simp
then have "X = lang_rhs A" using Inv_ES
unfolding A_def invariant_def ardenable_all_def finite_rhs_def
by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn)
then have "X = lang_rhs {Lam r | r. Lam r ∈ A}" using eq by simp
then have "X = lang (⨄{r. Lam r ∈ A})" using fin by auto
then show "∃r. X = lang r" by blast
qed

lemma bchoice_finite_set:
assumes a: "∀x ∈ S. ∃y. x = f y"
and     b: "finite S"
shows "∃ys. (⋃ S) = ⋃(f ` ys) ∧ finite ys"
using bchoice[OF a] b
apply(erule_tac exE)
apply(rule_tac x="fa ` S" in exI)
apply(auto)
done

theorem Myhill_Nerode1:
fixes A::"('a::finite) lang"
assumes finite_CS: "finite (UNIV // ≈A)"
shows   "∃r. A = lang r"
proof -
have fin: "finite (finals A)"
using finals_in_partitions finite_CS by (rule finite_subset)
have "∀X ∈ (UNIV // ≈A). ∃r. X = lang r"
using finite_CS every_eqcl_has_reg by blast
then have a: "∀X ∈ finals A. ∃r. X = lang r"
using finals_in_partitions by auto
then obtain rs::"('a rexp) set" where "⋃ (finals A) = ⋃(lang ` rs)" "finite rs"
using fin by (auto dest: bchoice_finite_set)
then have "A = lang (⨄rs)"
unfolding lang_is_union_of_finals[symmetric] by simp
then show "∃r. A = lang r" by blast
qed

end
```