--- 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