# Theory Myhill

```(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)

theory Myhill
imports Myhill_2 "Regular-Sets.Derivatives"
begin

section ‹The theorem›

theorem Myhill_Nerode:
fixes A::"('a::finite) lang"
shows "(∃r. A = lang r) ⟷ finite (UNIV // ≈A)"
using Myhill_Nerode1 Myhill_Nerode2 by auto

subsection ‹Second direction proved using partial derivatives›

text ‹
An alternaive proof using the notion of partial derivatives for regular
expressions due to Antimirov \<^cite>‹"Antimirov95"›.
›

lemma MN_Rel_Derivs:
shows "x ≈A y ⟷ Derivs x A = Derivs y A"
unfolding Derivs_def str_eq_def
by auto

lemma Myhill_Nerode3:
fixes r::"'a rexp"
shows "finite (UNIV // ≈(lang r))"
proof -
have "finite (UNIV // =(λx. pderivs x r)=)"
proof -
have "range (λx. pderivs x r) ⊆ Pow (pderivs_lang UNIV r)"
unfolding pderivs_lang_def by auto
moreover
have "finite (Pow (pderivs_lang UNIV r))" by (simp add: finite_pderivs_lang)
ultimately
have "finite (range (λx. pderivs x r))"
by (simp add: finite_subset)
then show "finite (UNIV // =(λx. pderivs x r)=)"
by (rule finite_eq_tag_rel)
qed
moreover
have "=(λx. pderivs x r)= ⊆ ≈(lang r)"
unfolding tag_eq_def
by (auto simp add: MN_Rel_Derivs Derivs_pderivs)
moreover
have "equiv UNIV =(λx. pderivs x r)="
and  "equiv UNIV (≈(lang r))"
unfolding equiv_def refl_on_def sym_def trans_def
unfolding tag_eq_def str_eq_def
by auto
ultimately show "finite (UNIV // ≈(lang r))"
by (rule refined_partition_finite)
qed

end
```