diff -r a0bcf886b8ef -r 8c4b6fb43ebe Derivatives.thy
--- a/Derivatives.thy	Fri Jul 05 12:07:48 2013 +0100
+++ b/Derivatives.thy	Fri Jul 05 17:19:17 2013 +0100
@@ -8,83 +8,9 @@
 
 text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}
 
-subsection {* Left-Quotients of languages *}
-
-definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where "Deriv x A = { xs. x#xs \<in> A }"
-
-definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where "Derivs xs A = { ys. xs @ ys \<in> A }"
-
-abbreviation 
-  Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
-where
-  "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
-
-
-lemma Deriv_empty[simp]:   "Deriv a {} = {}"
-  and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
-  and Deriv_char[simp]:    "Deriv a {[b]} = (if a = b then {[]} else {})"
-  and Deriv_union[simp]:   "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
-by (auto simp: Deriv_def)
-
-lemma Deriv_conc_subset:
-"Deriv a A @@ B \<subseteq> Deriv a (A @@ B)" (is "?L \<subseteq> ?R")
-proof 
-  fix w assume "w \<in> ?L"
-  then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"
-    by (auto simp: Deriv_def)
-  then have "a # w \<in> A @@ B"
-    by (auto intro: concI[of "a # u", simplified])
-  thus "w \<in> ?R" by (auto simp: Deriv_def)
-qed
-
-lemma Der_conc [simp]:
-  shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
-unfolding Deriv_def conc_def
-by (auto simp add: Cons_eq_append_conv)
-
-lemma Deriv_star [simp]:
-  shows "Deriv c (star A) = (Deriv c A) @@ star A"
-proof -
-  have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
-    unfolding Deriv_def conc_def 
-    apply(auto simp add: Cons_eq_append_conv)
-    apply(drule star_decom)
-    apply(auto simp add: Cons_eq_append_conv)
-    done
-
-  have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
-    by (simp only: star_unfold_left[symmetric])
-  also have "... = Deriv c (A @@ star A)"
-    by (simp only: Deriv_union) (simp)
-  also have "... =  (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
-    by simp
-   also have "... =  (Deriv c A) @@ star A"
-    using incl by auto
-  finally show "Deriv c (star A) = (Deriv c A) @@ star A" . 
-qed
-
-lemma Derivs_simps [simp]:
-  shows "Derivs [] A = A"
-  and   "Derivs (c # s) A = Derivs s (Deriv c A)"
-  and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
-unfolding Derivs_def Deriv_def by auto
-
-
 subsection {* Brozowski's derivatives of regular expressions *}
 
 fun
-  nullable :: "'a rexp \<Rightarrow> bool"
-where
-  "nullable (Zero) = False"
-| "nullable (One) = True"
-| "nullable (Atom c) = False"
-| "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)"
-| "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)"
-| "nullable (Star r) = True"
-
-fun
   deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
   "deriv c (Zero) = Zero"
@@ -102,23 +28,26 @@
 | "derivs (c # s) r = derivs s (deriv c r)"
 
 
-lemma nullable_iff:
-  shows "nullable r \<longleftrightarrow> [] \<in> lang r"
-by (induct r) (auto simp add: conc_def split: if_splits)
-
-lemma Deriv_deriv:
-  shows "Deriv c (lang r) = lang (deriv c r)"
+lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
 by (induct r) (simp_all add: nullable_iff)
 
-lemma Derivs_derivs:
-  shows "Derivs s (lang r) = lang (derivs s r)"
-by (induct s arbitrary: r) (simp_all add: Deriv_deriv)
+lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)"
+by (induct s arbitrary: r) (simp_all add: lang_deriv)
+
+text {* A regular expression matcher: *}
+
+definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
+"matcher r s = nullable (derivs s r)"
+
+lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
+by (induct s arbitrary: r)
+   (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
 
 
 subsection {* Antimirov's partial derivatives *}
 
 abbreviation
-  "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
+  "Timess rs r \<equiv> (\<Union>r' \<in> rs. {Times r' r})"
 
 fun
   pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
@@ -135,20 +64,20 @@
   pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 where
   "pderivs [] r = {r}"
-| "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)"
+| "pderivs (c # s) r = \<Union> (pderivs s ` pderiv c r)"
 
 abbreviation
  pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
 where
-  "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs"
+  "pderiv_set c rs \<equiv> \<Union> (pderiv c ` rs)"
 
 abbreviation
   pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
 where
-  "pderivs_set s rs \<equiv> \<Union> (pderivs s) ` rs"
+  "pderivs_set s rs \<equiv> \<Union> (pderivs s ` rs)"
 
 lemma pderivs_append:
-  "pderivs (s1 @ s2) r = \<Union> (pderivs s2) ` (pderivs s1 r)"
+  "pderivs (s1 @ s2) r = \<Union> (pderivs s2 ` pderivs s1 r)"
 by (induct s1 arbitrary: r) (simp_all)
 
 lemma pderivs_snoc:
@@ -168,33 +97,33 @@
 subsection {* Relating left-quotients and partial derivatives *}
 
 lemma Deriv_pderiv:
-  shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)"
+  shows "Deriv c (lang r) = \<Union> (lang ` pderiv c r)"
 by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
 
 lemma Derivs_pderivs:
-  shows "Derivs s (lang r) = \<Union> lang ` (pderivs s r)"
+  shows "Derivs s (lang r) = \<Union> (lang ` pderivs s r)"
 proof (induct s arbitrary: r)
   case (Cons c s)
-  have ih: "\<And>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)" by fact
+  have ih: "\<And>r. Derivs s (lang r) = \<Union> (lang ` pderivs s r)" by fact
   have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
-  also have "\<dots> = Derivs s (\<Union> lang ` (pderiv c r))" by (simp add: Deriv_pderiv)
+  also have "\<dots> = Derivs s (\<Union> (lang ` pderiv c r))" by (simp add: Deriv_pderiv)
   also have "\<dots> = Derivss s (lang ` (pderiv c r))"
     by (auto simp add:  Derivs_def)
-  also have "\<dots> = \<Union> lang ` (pderivs_set s (pderiv c r))"
+  also have "\<dots> = \<Union> (lang ` (pderivs_set s (pderiv c r)))"
     using ih by auto
-  also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp
-  finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" .
+  also have "\<dots> = \<Union> (lang ` (pderivs (c # s) r))" by simp
+  finally show "Derivs (c # s) (lang r) = \<Union> (lang ` pderivs (c # s) r)" .
 qed (simp add: Derivs_def)
 
 subsection {* Relating derivatives and partial derivatives *}
 
 lemma deriv_pderiv:
-  shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)"
-unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp
+  shows "\<Union> (lang ` (pderiv c r)) = lang (deriv c r)"
+unfolding lang_deriv Deriv_pderiv by simp
 
 lemma derivs_pderivs:
-  shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)"
-unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp
+  shows "\<Union> (lang ` (pderivs s r)) = lang (derivs s r)"
+unfolding lang_derivs Derivs_pderivs by simp
 
 
 subsection {* Finiteness property of partial derivatives *}
@@ -272,7 +201,7 @@
   have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))" 
     by (simp add: pderivs_snoc)
   also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
-    using ih by (auto) (blast)
+    using ih by fast
   also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
     by (simp)
   also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
@@ -282,7 +211,7 @@
     by auto
   also 
   have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
-    by (auto simp add: if_splits) (blast)
+    by (auto simp add: if_splits)
   also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
     by (simp add: pderivs_snoc)
   also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2"
@@ -319,9 +248,9 @@
   { assume asm: "s \<noteq> []"
     have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
     also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
-      using ih[OF asm] by (auto) (blast)
+      using ih[OF asm] by fast
     also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
-      by (auto split: if_splits) (blast)+
+      by (auto split: if_splits)
     also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))"
       by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union)
          (auto simp add: pderivs_lang_def)
@@ -331,11 +260,7 @@
   }
   moreover
   { assume asm: "s = []"
-    then have ?case
-      apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
-      apply(rule_tac x = "[c]" in exI)
-      apply(auto)
-      done
+    then have ?case by (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
   }
   ultimately show ?case by blast
 qed (simp)
@@ -377,18 +302,4 @@
   shows "finite (pderivs_lang A r)"
 by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
 
-
-subsection {* A regular expression matcher based on Brozowski's derivatives *}
-
-fun
-  matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "matcher r s = nullable (derivs s r)"
-
-lemma matcher_correctness:
-  shows "matcher r s \<longleftrightarrow> s \<in> lang r"
-by (induct s arbitrary: r)
-   (simp_all add: nullable_iff Deriv_deriv[symmetric] Deriv_def)
-
-
 end
\ No newline at end of file