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