--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Myhill.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -0,0 +1,55 @@
+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
\ No newline at end of file