diff -r 07a269d9642b -r 9f46a9571e37 Derivatives.thy
--- a/Derivatives.thy	Wed Aug 03 17:08:31 2011 +0000
+++ b/Derivatives.thy	Fri Aug 05 05:34:11 2011 +0000
@@ -21,35 +21,15 @@
 where
   "Ders s A \<equiv> {s'. s @ s' \<in> A}"
 
-definition
-  Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
-  "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"
-
-lemma Ders_set_Ders:
-  shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"
-unfolding Ders_set_def Ders_def
-by auto
-
-lemma Der_zero [simp]:
-  shows "Der c {} = {}"
-unfolding Der_def
-by auto
+abbreviation 
+  "Derss s A \<equiv> \<Union> (Ders s) ` A"
 
-lemma Der_one [simp]:
-  shows "Der c {[]} = {}"
-unfolding Der_def
-by auto
-
-lemma Der_atom [simp]:
-  shows "Der c {[d]} = (if c = d then {[]} else {})"
-unfolding Der_def
-by auto
-
-lemma Der_union [simp]:
-  shows "Der c (A \<union> B) = Der c A \<union> Der c B"
-unfolding Der_def
-by auto
+lemma Der_simps [simp]:
+  shows "Der c {} = {}"
+  and   "Der c {[]} = {}"
+  and   "Der c {[d]} = (if c = d then {[]} else {})"
+  and   "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def by auto
 
 lemma Der_conc [simp]:
   shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
@@ -60,7 +40,7 @@
   shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
 proof -
   have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
-    unfolding Der_def Delta_def 
+    unfolding Der_def Delta_def conc_def 
     apply(auto)
     apply(drule star_decom)
     apply(auto simp add: Cons_eq_append_conv)
@@ -69,7 +49,7 @@
   have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
     by (simp only: star_unfold_left[symmetric])
   also have "... = Der c (A \<cdot> A\<star>)"
-    by (simp only: Der_union Der_one) (simp)
+    by (simp only: Der_simps) (simp)
   also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
     by simp
   also have "... =  (Der c A) \<cdot> A\<star>"
@@ -77,19 +57,12 @@
   finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 
 qed
 
-lemma Ders_nil [simp]:
+lemma Ders_simps [simp]:
   shows "Ders [] A = A"
-unfolding Ders_def by simp
-
-lemma Ders_cons [simp]:
-  shows "Ders (c # s) A = Ders s (Der c A)"
+  and   "Ders (c # s) A = Ders s (Der c A)"
+  and   "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
 unfolding Ders_def Der_def by auto
 
-lemma Ders_append [simp]:
-  shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
-unfolding Ders_def by simp 
-
-
 subsection {* Brozowsky's derivatives of regular expressions *}
 
 fun
@@ -137,7 +110,7 @@
 subsection {* Antimirov's Partial Derivatives *}
 
 abbreviation
-  "Times_set rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
+  "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
 
 fun
   pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
@@ -147,11 +120,11 @@
 | "pder c (Atom c') = (if c = c' then {One} else {Zero})"
 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
 | "pder c (Times r1 r2) = 
-    (if nullable r1 then Times_set (pder c r1) r2 \<union>  pder c r2 else Times_set (pder c r1) r2)"
-| "pder c (Star r) = Times_set (pder c r) (Star r)"
+    (if nullable r1 then Timess (pder c r1) r2 \<union>  pder c r2 else Timess (pder c r1) r2)"
+| "pder c (Star r) = Timess (pder c r) (Star r)"
 
 abbreviation
-  "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
+  "pder_set c rs \<equiv> \<Union> pder c ` rs"
 
 fun
   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
@@ -160,7 +133,7 @@
 | "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
 
 abbreviation
-  "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
+  "pderss s A \<equiv> \<Union> (pders s) ` A"
 
 lemma pders_append:
   "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
@@ -170,85 +143,113 @@
   shows "pders (s @ [c]) r = pder_set c (pders s r)"
 by (simp add: pders_append)
 
-lemma pders_set_lang:
-  shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
-unfolding image_def 
-by auto
-
-lemma pders_Zero [simp]:
+lemma pders_simps [simp]:
   shows "pders s Zero = {Zero}"
-by (induct s) (simp_all)
-
-lemma pders_One [simp]:
-  shows "pders s One = (if s = [] then {One} else {Zero})"
+  and   "pders s One = (if s = [] then {One} else {Zero})"
+  and   "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
+  and   "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
 by (induct s) (auto)
 
-lemma pders_Atom [simp]:
-  shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
-by (induct s) (auto)
+subsection {* Relating left-quotients and partial derivatives *}
+
+lemma Der_pder:
+  shows "Der c (lang r) = \<Union> lang ` (pder c r)"
+by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
 
-lemma pders_Plus [simp]:
-  shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
-by (induct s) (auto)
+lemma Ders_pders:
+  shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
+proof (induct s arbitrary: r)
+  case (Cons c s)
+  have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
+  have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp
+  also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder)
+  also have "\<dots> = Derss s (lang ` (pder c r))"
+    by (auto simp add:  Ders_def)
+  also have "\<dots> = \<Union> lang ` (pderss s (pder c r))"
+    using ih by auto
+  also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp
+  finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
+qed (simp add: Ders_def)
+
+subsection {* Relating derivatives and partial derivatives *}
+
+lemma
+  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+subsection {* There are only finitely many partial derivatives for a language *}
+
+abbreviation
+  "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
 
 text {* Non-empty suffixes of a string *}
 
 definition
   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
-lemma Suf:
+lemma Suf_snoc:
   shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
 unfolding Suf_def conc_def
 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
 
 lemma Suf_Union:
-  shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+  shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
 by (auto simp add: conc_def)
 
+lemma pders_set_snoc:
+  shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))"
+by (simp add: Suf_Union pders_snoc)
+
 lemma pders_Times:
-  shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+  shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)"
 proof (induct s rule: rev_induct)
   case (snoc c s)
-  have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 
+  have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)" 
     by fact
   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 
     by (simp add: pders_snoc)
-  also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
+  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2))"
     using ih by (auto) (blast)
-  also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
-    by (simp)
-  also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
+  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)"
     by (simp)
-  also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
-    by (auto simp add: pders_snoc)
-  also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
-    by (auto simp add: if_splits) (blast)
-  also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
-    by (auto simp add: pders_snoc Suf Suf_Union)
+  also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+    by (simp add: pders_set_snoc)
+  also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+    by auto
+  also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+    by (auto simp add: if_splits pders_snoc) (blast)
+  also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2"
+    by (auto simp add: Suf_snoc)  
   finally show ?case .
-qed (simp)
+qed (simp) 
+
 
 lemma pders_Star:
   assumes a: "s \<noteq> []"
-  shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Times_set (pders v r) (Star r))"
+  shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))"
 using a
 proof (induct s rule: rev_induct)
   case (snoc c s)
-  have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact
+  have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Timess (pders v r) (Star r))" by fact
   { assume asm: "s \<noteq> []"
     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
-    also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"
-      using ih[OF asm] by blast
-    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
+    also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Timess (pders v r) (Star r)))"
+      using ih[OF asm] by (auto) (blast)
+    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))"
       by simp
-    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
+    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
       by (auto split: if_splits) 
-    also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
+    also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
       using asm by (auto simp add: Suf_def)
-    also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
+    also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))"
       by (simp add: pders_snoc)
-    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
-      by (auto simp add: Suf Suf_Union pders_snoc)
+    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))"
+      by (auto simp add: Suf_snoc Suf_Union pders_snoc)
     finally have ?case .
   }
   moreover
@@ -284,7 +285,7 @@
 using a unfolding UNIV1_def Suf_def by (auto)
 
 lemma pders_set_Times:
-  shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+  shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Timess (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
 unfolding UNIV1_def
 apply(rule UN_least)
 apply(rule subset_trans)
@@ -298,7 +299,7 @@
 done
 
 lemma pders_set_Star:
-  shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
+  shows "pders_set UNIV1 (Star r) \<subseteq> Timess (pders_set UNIV1 r) (Star r)"
 unfolding UNIV1_def
 apply(rule UN_least)
 apply(rule subset_trans)
@@ -308,9 +309,9 @@
 apply(auto)
 done
 
-lemma finite_Times_set:
+lemma finite_Timess:
   assumes a: "finite A"
-  shows "finite (Times_set A r)"
+  shows "finite (Timess A r)"
 using a by (auto)
 
 lemma finite_pders_set_UNIV1:
@@ -326,11 +327,11 @@
 apply(simp)
 apply(rule finite_subset)
 apply(rule pders_set_Times)
-apply(simp only: finite_Times_set finite_Un)
+apply(simp only: finite_Timess finite_Un)
 apply(simp)
 apply(rule finite_subset)
 apply(rule pders_set_Star)
-apply(simp only: finite_Times_set)
+apply(simp only: finite_Timess)
 done
     
 lemma pders_set_UNIV_UNIV1:
@@ -371,48 +372,6 @@
 qed
 
 
-subsection {* Relating left-quotients and partial derivatives *}
-
-lemma Der_pder:
-  shows "Der c (lang r) = \<Union> lang ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
-
-lemma Ders_pders:
-  shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
-proof (induct s rule: rev_induct)
-  case (snoc c s)
-  have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
-  have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
-    by (simp add: Ders_append)
-  also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
-    by (simp)
-  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" 
-    unfolding Der_def image_def by auto
-  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang `  (pder c r)))"
-    by (simp add: Der_pder)
-  also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
-    by (simp add: pders_set_lang)
-  also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
-    by (simp add: pders_snoc)
-  finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
-qed (simp add: Ders_def)
-
-lemma Ders_set_pders_set:
-  shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"
-by (simp add: Ders_set_Ders Ders_pders)
-
-
-subsection {* Relating derivatives and partial derivatives *}
-
-lemma
-  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
-
-lemma
-  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
-
-
 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
 lemma MN_Rel_Ders: