--- a/Closures.thy	Tue Aug 09 22:15:11 2011 +0000
+++ b/Closures.thy	Thu Aug 11 10:26:19 2011 +0000
@@ -153,7 +153,7 @@
   have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
   
   have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
-    by (simp add: Ders_pders)
+    by (simp add: Ders_pders pders_lang_def)
   also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
   finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
     by simp

--- a/Derivatives.thy	Tue Aug 09 22:15:11 2011 +0000
+++ b/Derivatives.thy	Thu Aug 11 10:26:19 2011 +0000
@@ -184,10 +184,39 @@
 
 subsection {* There are only finitely many partial derivatives for a language *}
 
-abbreviation
+definition
   "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r"
 
-text {* Non-empty suffixes of a string *}
+lemma pders_lang_subsetI [intro]:
+  assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
+  shows "pders_lang A r \<subseteq> C"
+using assms unfolding pders_lang_def by (rule UN_least)
+
+lemma pders_lang_union:
+  shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
+by (simp add: pders_lang_def)
+
+definition
+  "UNIV1 \<equiv> UNIV - {[]}"
+
+lemma pders_lang_Zero [simp]:
+  shows "pders_lang UNIV1 Zero = {Zero}"
+unfolding UNIV1_def pders_lang_def by auto
+
+lemma pders_lang_One [simp]:
+  shows "pders_lang UNIV1 One = {Zero}"
+unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
+
+lemma pders_lang_Atom:
+  shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
+unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
+
+lemma pders_lang_Plus [simp]:
+  shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
+unfolding UNIV1_def pders_lang_def by auto
+
+
+text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *}
 
 definition
   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
@@ -203,6 +232,7 @@
 
 lemma pders_lang_snoc:
   shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
+unfolding pders_lang_def
 by (simp add: Suf_Union pders_snoc)
 
 lemma pders_Times:
@@ -226,10 +256,29 @@
   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
     by (simp add: pders_snoc)
   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
-    by (auto simp add: Suf_snoc)  
+    unfolding pders_lang_def by (auto simp add: Suf_snoc)  
   finally show ?case .
 qed (simp) 
 
+lemma pders_lang_Times_aux1:
+  assumes a: "s \<in> UNIV1"
+  shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
+using a unfolding UNIV1_def Suf_def pders_lang_def by auto
+
+lemma pders_lang_Times_aux2:
+  assumes a: "s \<in> UNIV1"
+  shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2"
+using a unfolding pders_lang_def by auto
+
+lemma pders_lang_Times [intro]:
+  shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
+apply(rule pders_lang_subsetI)
+apply(rule subset_trans)
+apply(rule pders_Times)
+using pders_lang_Times_aux1 pders_lang_Times_aux2
+apply(blast)
+done
+
 lemma pders_Star:
   assumes a: "s \<noteq> []"
   shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
@@ -244,15 +293,16 @@
     also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
       by (auto split: if_splits) (blast)+
     also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
-      by (auto simp add: Suf_snoc pders_lang_snoc)
+      by (simp only: Suf_snoc pders_lang_snoc pders_lang_union)
+         (auto simp add: pders_lang_def)
     also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
-      by (auto simp add: Suf_snoc Suf_Union pders_snoc)
+      by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def)
     finally have ?case .
   }
   moreover
   { assume asm: "s = []"
     then have ?case
-      apply (auto simp add: pders_snoc Suf_def)
+      apply (auto simp add: pders_lang_def pders_snoc Suf_def)
       apply(rule_tac x = "[c]" in exI)
       apply(auto)
       done
@@ -260,56 +310,17 @@
   ultimately show ?case by blast
 qed (simp)
 
-definition
-  "UNIV1 \<equiv> UNIV - {[]}"
-
-lemma pders_lang_Zero [simp]:
-  shows "pders_lang UNIV1 Zero = {Zero}"
-unfolding UNIV1_def by auto
-
-lemma pders_lang_One [simp]:
-  shows "pders_lang UNIV1 One = {Zero}"
-unfolding UNIV1_def by (auto split: if_splits)
-
-lemma pders_lang_Atom:
-  shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
-unfolding UNIV1_def by (auto split: if_splits)
-
-lemma pders_lang_Plus:
-  shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
-unfolding UNIV1_def by auto
-
-lemma pders_lang_Times_aux:
-  assumes a: "s \<in> UNIV1"
-  shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
-using a unfolding UNIV1_def Suf_def by auto
-
-lemma pders_lang_Times [intro]:
-  shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
-unfolding UNIV1_def
-apply(rule UN_least)
+lemma pders_lang_Star [intro]:
+  shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
+apply(rule pders_lang_subsetI)
 apply(rule subset_trans)
-apply(rule pders_Times)
-apply(simp)
-apply(rule conjI) 
-apply(auto)[1]
-apply(rule subset_trans)
-apply(rule pders_lang_Times_aux)
-apply(auto simp add: UNIV1_def)
+apply(rule pders_Star)
+apply(simp add: UNIV1_def)
+apply(simp add: UNIV1_def Suf_def)
+apply(auto simp add: pders_lang_def)
 done
 
-lemma pders_lang_Star [intro]:
-  shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
-unfolding UNIV1_def
-apply(rule UN_least)
-apply(rule subset_trans)
-apply(rule pders_Star)
-apply(simp)
-apply(simp add: Suf_def)
-apply(auto)
-done
-
-lemma finite_Timess:
+lemma finite_Timess [simp]:
   assumes a: "finite A"
   shows "finite (Timess A r)"
 using a by auto
@@ -318,60 +329,33 @@
   shows "finite (pders_lang UNIV1 r)"
 apply(induct r)
 apply(simp)
-apply(simp only: pders_lang_One)
 apply(simp)
-apply(rule finite_subset)
-apply(rule pders_lang_Atom)
+apply(rule finite_subset[OF pders_lang_Atom])
 apply(simp)
-apply(simp only: pders_lang_Plus)
 apply(simp)
-apply(rule finite_subset)
-apply(rule pders_lang_Times)
-apply(simp only: finite_Timess finite_Un)
+apply(rule finite_subset[OF pders_lang_Times])
 apply(simp)
-apply(rule finite_subset)
-apply(rule pders_lang_Star)
-apply(simp only: finite_Timess)
+apply(rule finite_subset[OF pders_lang_Star])
+apply(simp)
 done
     
-lemma pders_lang_UNIV_UNIV1:
+lemma pders_lang_UNIV:
   shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
-unfolding UNIV1_def
-apply(auto)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-done
+unfolding UNIV1_def pders_lang_def
+by blast
 
 lemma finite_pders_lang_UNIV:
   shows "finite (pders_lang UNIV r)"
-unfolding pders_lang_UNIV_UNIV1
+unfolding pders_lang_UNIV
 by (simp add: finite_pders_lang_UNIV1)
 
 lemma finite_pders_lang:
   shows "finite (pders_lang A r)"
 apply(rule rev_finite_subset)
 apply(rule_tac r="r" in finite_pders_lang_UNIV)
-apply(auto)
+apply(auto simp add: pders_lang_def)
 done
 
-lemma finite_pders:
-  shows "finite (pders s r)"
-using finite_pders_lang[where A="{s}" and r="r"]
-by simp
-
-lemma finite_pders2:
-  shows "finite {pders s r | s. s \<in> A}"
-proof -
-  have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_lang A r)" by auto
-  moreover
-  have "finite (Pow (pders_lang A r))"
-    using finite_pders_lang by simp
-  ultimately 
-  show "finite {pders s r | s. s \<in> A}"
-    by(rule finite_subset)
-qed
-
-
 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
 lemma MN_Rel_Ders:
@@ -390,12 +374,13 @@
 proof -
   have "finite (UNIV // =(\<lambda>x. pders x r)=)"
   proof - 
-    have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto
+    have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)"
+      unfolding pders_lang_def by auto
     moreover 
-    have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)
+    have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang)
     ultimately
     have "finite (range (\<lambda>x. pders x r))"
-      by simp
+      by (simp add: finite_subset)
     then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 
       by (rule finite_eq_tag_rel)
   qed