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