--- a/Theories/Derivs.thy	Wed Mar 23 13:33:55 2011 +0000
+++ b/Theories/Derivs.thy	Fri Mar 25 09:42:33 2011 +0000
@@ -166,6 +166,7 @@
 abbreviation
   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
 
+
 lemma pders_append:
   "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
 apply(induct s2 arbitrary: s1 r rule: rev_induct)
@@ -417,6 +418,55 @@
 using finite_pders_set[where A="{s}" and r="r"]
 by simp
 
+
+lemma test: 
+  shows "pders_set A r = (\<Union> {pders s r | s. s \<in> A})"
+by auto
+
+lemma finite_pow_pders:
+  shows "finite (Pow (\<Union> {pders s r | s. s \<in> A}))"
+using finite_pders_set
+by (simp add: test)
+
+lemma test2:
+  shows "{pders s r | s. s \<in> A} \<subseteq> Pow (\<Union> {pders s r | s. s \<in> A})"
+  by auto
+
+lemma test3:
+  shows "finite ({pders s r | s. s \<in> A})"
+apply(rule finite_subset)
+apply(rule test2)
+apply(rule finite_pow_pders)
+done
+
+lemma Myhill_Nerode_aux:
+  fixes r::"rexp"
+  shows "finite (UNIV // =(\<lambda>x. pders x r)=)"
+apply(rule finite_eq_tag_rel)
+apply(rule rev_finite_subset)
+apply(rule test3)
+apply(auto)
+done
+
+lemma Myhill_Nerode3:
+  fixes r::"rexp"
+  shows "finite (UNIV // \<approx>(L r))"
+apply(rule refined_partition_finite)
+apply(rule Myhill_Nerode_aux[where r="r"])
+apply(simp add: tag_eq_rel_def)
+apply(auto)[1]
+unfolding str_eq_def[symmetric]
+unfolding MN_Rel_Ders
+apply(simp add: Ders_pders)
+apply(rule equivI)
+apply(auto simp add: tag_eq_rel_def refl_on_def sym_def trans_def)
+apply(rule equivI)
+apply(auto simp add: str_eq_rel_def refl_on_def sym_def trans_def)
+done
+
+
+section {* Closure under Left-Quotients *}
+
 lemma closure_left_quotient:
   assumes "regular A"
   shows "regular (Ders_set B A)"
@@ -433,6 +483,29 @@
 qed
 
 
+section {* Relating standard and partial derivations *}
+
+lemma
+  shows "(\<Union> L ` (pder c r)) = L (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+  shows "(\<Union> L ` (pders s r)) = L (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+section {* attempt to prove MN *}
+(*
+lemma Myhill_Nerode3:
+  fixes r::"rexp"
+  shows "finite (UNIV // =(\<lambda>x. pders x r)=)"
+apply(rule finite_eq_tag_rel)
+apply(rule finite_pders_set)
+apply(simp add: Range_def)
+unfolding Quotien_def
+by (induct r) (auto)
+*)
+
 fun
   width :: "rexp \<Rightarrow> nat"
 where