--- a/Derivatives.thy Thu Jul 28 11:56:25 2011 +0000
+++ b/Derivatives.thy Thu Jul 28 14:22:10 2011 +0000
@@ -14,7 +14,7 @@
definition
Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
where
- "Der c A \<equiv> {s. [c] @ s \<in> A}"
+ "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
definition
Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
@@ -77,25 +77,19 @@
finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
qed
+lemma Ders_nil [simp]:
+ shows "Ders [] A = A"
+unfolding Ders_def by simp
-lemma Ders_singleton:
- shows "Ders [c] A = Der c A"
-unfolding Der_def Ders_def
-by simp
+lemma Ders_cons [simp]:
+ shows "Ders (c # s) A = Ders s (Der c A)"
+unfolding Ders_def Der_def by auto
-lemma Ders_append:
+lemma Ders_append [simp]:
shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
unfolding Ders_def by simp
-text {* Relating the Myhill-Nerode relation with left-quotients. *}
-
-lemma MN_Rel_Ders:
- shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
-unfolding Ders_def str_eq_def str_eq_rel_def
-by auto
-
-
subsection {* Brozowsky's derivatives of regular expressions *}
fun
@@ -119,15 +113,12 @@
(if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
| "der c (Star r) = Times (der c r) (Star r)"
-function
+fun
ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
"ders [] r = r"
-| "ders (s @ [c]) r = der c (ders s r)"
-by (auto) (metis rev_cases)
+| "ders (c # s) r = ders s (der c r)"
-termination
- by (relation "measure (length o fst)") (auto)
lemma Delta_nullable:
shows "Delta (lang r) = (if nullable r then {[]} else {})"
@@ -140,13 +131,7 @@
lemma Ders_ders:
shows "Ders s (lang r) = lang (ders s r)"
-apply(induct s rule: rev_induct)
-apply(simp add: Ders_def)
-apply(simp only: ders.simps)
-apply(simp only: Ders_append)
-apply(simp only: Ders_singleton)
-apply(simp only: Der_der)
-done
+by (induct s arbitrary: r) (simp_all add: Der_der)
subsection {* Antimirov's Partial Derivatives *}
@@ -161,40 +146,29 @@
| "pder c One = {Zero}"
| "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) = Times_set (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
+| "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)"
abbreviation
"pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
-function
+fun
pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
where
"pders [] r = {r}"
-| "pders (s @ [c]) r = pder_set c (pders s r)"
-by (auto) (metis rev_cases)
-
-termination
- by (relation "measure (length o fst)") (auto)
+| "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))"
abbreviation
"pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
lemma pders_append:
"pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
-apply(induct s2 arbitrary: s1 r rule: rev_induct)
-apply(simp)
-apply(subst append_assoc[symmetric])
-apply(simp only: pders.simps)
-apply(auto)
-done
+by (induct s1 arbitrary: r) (simp_all)
-lemma pders_singleton:
- "pders [c] r = pder c r"
-apply(subst append_Nil[symmetric])
-apply(simp only: pders.simps)
-apply(simp)
-done
+lemma pders_snoc:
+ 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)))"
@@ -203,19 +177,19 @@
lemma pders_Zero [simp]:
shows "pders s Zero = {Zero}"
-by (induct s rule: rev_induct) (simp_all)
+by (induct s) (simp_all)
lemma pders_One [simp]:
shows "pders s One = (if s = [] then {One} else {Zero})"
-by (induct s rule: rev_induct) (auto)
+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 rule: rev_induct) (auto)
+by (induct s) (auto)
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 rule: rev_induct) (auto)
+by (induct s) (auto)
text {* Non-empty suffixes of a string *}
@@ -237,7 +211,8 @@
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)"
by fact
- have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp
+ 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))"
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)"
@@ -245,15 +220,11 @@
also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v 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)
+ 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)"
- apply(subst (2) pders.simps)
- apply(simp only: Suf)
- apply(simp add: Suf_Union pders_singleton)
- apply(auto)
- done
+ by (auto simp add: pders_snoc Suf Suf_Union)
finally show ?case .
qed (simp)
@@ -265,7 +236,7 @@
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
{ assume asm: "s \<noteq> []"
- have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by simp
+ 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)))"
@@ -275,52 +246,46 @@
also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (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))"
- by simp
+ by (simp add: pders_snoc)
also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
- apply(simp only: Suf)
- apply(simp add: Suf_Union pders_singleton)
- apply(auto)
- done
+ by (auto simp add: Suf Suf_Union pders_snoc)
finally have ?case .
}
moreover
{ assume asm: "s = []"
then have ?case
- apply(simp add: pders_singleton Suf_def)
- apply(auto)
- apply(rule_tac x="[c]" in exI)
- apply(simp add: pders_singleton)
- done
+ by (auto simp add: pders_snoc Suf_def)
}
ultimately show ?case by blast
qed (simp)
-abbreviation
+definition
"UNIV1 \<equiv> UNIV - {[]}"
lemma pders_set_Zero:
shows "pders_set UNIV1 Zero = {Zero}"
-by auto
+unfolding UNIV1_def by auto
lemma pders_set_One:
shows "pders_set UNIV1 One = {Zero}"
-by (auto split: if_splits)
+unfolding UNIV1_def by (auto split: if_splits)
lemma pders_set_Atom:
shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
-by (auto split: if_splits)
+unfolding UNIV1_def by (auto split: if_splits)
lemma pders_set_Plus:
shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
-by auto
+unfolding UNIV1_def by auto
lemma pders_set_Times_aux:
assumes a: "s \<in> UNIV1"
shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
-using a by (auto simp add: Suf_def)
+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"
+unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
apply(rule pders_Times)
@@ -329,11 +294,12 @@
apply(auto)[1]
apply(rule subset_trans)
apply(rule pders_set_Times_aux)
-apply(auto)
+apply(auto simp add: UNIV1_def)
done
lemma pders_set_Star:
shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
+unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
apply(rule pders_Star)
@@ -369,6 +335,7 @@
lemma pders_set_UNIV_UNIV1:
shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
+unfolding UNIV1_def
apply(auto)
apply(rule_tac x="[]" in exI)
apply(simp)
@@ -418,7 +385,7 @@
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 add: Ders_singleton)
+ 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)))"
@@ -426,7 +393,7 @@
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
+ by (simp add: pders_snoc)
finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
qed (simp add: Ders_def)
@@ -446,6 +413,12 @@
unfolding Ders_ders[symmetric] Ders_pders by simp
+text {* Relating the Myhill-Nerode relation with left-quotients. *}
+
+lemma MN_Rel_Ders:
+ shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
+unfolding Ders_def str_eq_def str_eq_rel_def
+by auto
subsection {*
The second direction of the Myhill-Nerode theorem using
@@ -488,4 +461,5 @@
by (rule refined_partition_finite)
qed
+
end
\ No newline at end of file