theory Myhill

  imports Myhill_2 "Derivatives"

begin

section {* The theorem *}

theorem Myhill_Nerode:

  fixes A::"('a::finite) lang"

  shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>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 \<approx>A y \<longleftrightarrow> Derivs x A = Derivs y A"

unfolding Derivs_def str_eq_def

by auto

lemma Myhill_Nerode3:

  fixes r::"'a rexp"

  shows "finite (UNIV // \<approx>(lang r))"

proof -

  have "finite (UNIV // =(\<lambda>x. pderivs x r)=)"

  proof - 

    have "range (\<lambda>x. pderivs x r) \<subseteq> 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 (\<lambda>x. pderivs x r))"

      by (simp add: finite_subset)

    then show "finite (UNIV // =(\<lambda>x. pderivs x r)=)" 

      by (rule finite_eq_tag_rel)

  qed

  moreover 

  have "=(\<lambda>x. pderivs x r)= \<subseteq> \<approx>(lang r)"

    unfolding tag_eq_def

    by (auto simp add: MN_Rel_Derivs Derivs_pderivs)

  moreover 

  have "equiv UNIV =(\<lambda>x. pderivs x r)="

  and  "equiv UNIV (\<approx>(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 // \<approx>(lang r))" 

    by (rule refined_partition_finite)

qed

end