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+
−