--- a/Matcher.thy Wed Apr 06 08:18:23 2011 +0000
+++ b/Matcher.thy Tue Apr 19 02:19:56 2011 +0000
@@ -2,30 +2,107 @@
imports "Main"
begin
+term "TYPE (nat * int)"
+term "TYPE ('a)"
+
+definition
+ P:: "'a itself \<Rightarrow> bool"
+where
+ "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))"
+
section {* Sequential Composition of Sets *}
-fun
- lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+definition
+ Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where
- "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+ "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
+
+
+text {* Two Simple Properties about Sequential Composition *}
+
+lemma seq_empty [simp]:
+ shows "A ;; {[]} = A"
+ and "{[]} ;; A = A"
+by (simp_all add: Seq_def)
+
+lemma seq_null [simp]:
+ shows "A ;; {} = {}"
+ and "{} ;; A = {}"
+by (simp_all add: Seq_def)
section {* Kleene Star for Sets *}
inductive_set
Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
- for L :: "string set"
+ for A :: "string set"
where
- start[intro]: "[] \<in> L\<star>"
-| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
+ start[intro]: "[] \<in> A\<star>"
+| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
-text {* A standard property of Star *}
+text {* A Standard Property of Star *}
+
+lemma star_cases:
+ shows "A\<star> = {[]} \<union> A ;; A\<star>"
+unfolding Seq_def
+by (auto) (metis Star.simps)
+
+lemma star_decomp:
+ assumes a: "c # x \<in> A\<star>"
+ shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
+using a
+by (induct x\<equiv>"c # x" rule: Star.induct)
+ (auto simp add: append_eq_Cons_conv)
+
+section {* Left-Quotient of a Set *}
+
+definition
+ Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
+where
+ "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+lemma Der_null [simp]:
+ shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_empty [simp]:
+ shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
-lemma lang_star_cases:
- shows "L\<star> = {[]} \<union> L ;; L\<star>"
-by (auto) (metis Star.simps)
+lemma Der_char [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_seq [simp]:
+ shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
+unfolding Der_def Seq_def
+by (auto simp add: Cons_eq_append_conv)
+
+lemma Der_star [simp]:
+ shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+proof -
+ have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+ by (simp only: star_cases[symmetric])
+ also have "... = Der c (A ;; A\<star>)"
+ by (simp only: Der_union Der_empty) (simp)
+ also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
+ by simp
+ also have "... = (Der c A) ;; A\<star>"
+ unfolding Seq_def Der_def
+ by (auto dest: star_decomp)
+ finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+qed
+
section {* Regular Expressions *}
@@ -37,39 +114,6 @@
| ALT rexp rexp
| STAR rexp
-types lang = "string set"
-
-definition
- DERIV :: "string \<Rightarrow> lang \<Rightarrow> lang"
-where
- "DERIV s A \<equiv> {s'. s @ s' \<in> A}"
-
-definition
- delta :: "lang \<Rightarrow> lang"
-where
- "delta A = (if [] \<in> A then {[]} else {})"
-
-lemma
- "DERIV s (P ; Q) = \<Union>{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}"
-apply(auto)
-
-fun
- D1 :: "string \<Rightarrow> lang \<Rightarrow> lang"
-where
- "D1 [] A = A"
-| "D1 (c # s) A = DERIV [c] (D1 s A)"
-
-fun
- D2 :: "string \<Rightarrow> lang \<Rightarrow> lang"
-where
- "D2 [] A = A"
-| "D2 (c # s) A = DERIV [c] (D1 s A)"
-
-function
- D
-where
- "D s P Q = P ;; Q"
-| "D (c#s) =
section {* Semantics of Regular Expressions *}
@@ -79,11 +123,10 @@
"L (NULL) = {}"
| "L (EMPTY) = {[]}"
| "L (CHAR c) = {[c]}"
-| "L (SEQ r1 r2) = (L r1) ; (L r2)"
+| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
| "L (STAR r) = (L r)\<star>"
-
section {* The Matcher *}
fun
@@ -113,64 +156,41 @@
| "derivative (c # s) r = derivative s (der c r)"
fun
- matches :: "rexp \<Rightarrow> string \<Rightarrow> bool"
+ matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"
where
- "matches r s = nullable (derivative s r)"
+ "matcher r s = nullable (derivative s r)"
section {* Correctness Proof of the Matcher *}
lemma nullable_correctness:
- shows "nullable r \<longleftrightarrow> [] \<in> L r"
-by (induct r) (auto)
+ shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
+by (induct r) (auto simp add: Seq_def)
+
lemma der_correctness:
- shows "s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r"
-proof (induct r arbitrary: s)
- case (SEQ r1 r2 s)
- have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c # s \<in> L r1" by fact
- have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c # s \<in> L r2" by fact
- show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c # s \<in> L (SEQ r1 r2)"
- using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv)
-next
- case (STAR r s)
- have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" by fact
- show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c # s \<in> L (STAR r)"
- proof
- assume "s \<in> L (der c (STAR r))"
- then have "s \<in> L (der c r) ; L r\<star>" by simp
- then have "c # s \<in> L r ; (L r)\<star>"
- by (auto simp add: ih Cons_eq_append_conv)
- then have "c # s \<in> (L r)\<star>" using lang_star_cases by auto
- then show "c # s \<in> L (STAR r)" by simp
- next
- assume "c # s \<in> L (STAR r)"
- then have "c # s \<in> (L r)\<star>" by simp
- then have "s \<in> L (der c r); (L r)\<star>"
- by (induct x\<equiv>"c # s" rule: Star.induct)
- (auto simp add: ih append_eq_Cons_conv)
- then show "s \<in> L (der c (STAR r))" by simp
- qed
-qed (simp_all)
+ shows "L (der c r) = Der c (L r)"
+by (induct r)
+ (simp_all add: nullable_correctness)
-lemma matches_correctness:
- shows "matches r s \<longleftrightarrow> s \<in> L r"
+lemma matcher_correctness:
+ shows "matcher r s \<longleftrightarrow> s \<in> L r"
by (induct s arbitrary: r)
- (simp_all add: nullable_correctness der_correctness)
+ (simp_all add: nullable_correctness der_correctness Der_def)
section {* Examples *}
-value "matches NULL []"
-value "matches (CHAR (CHR ''a'')) [CHR ''a'']"
-value "matches (CHAR a) [a,a]"
-value "matches (STAR (CHAR a)) []"
-value "matches (STAR (CHAR a)) [a,a]"
-value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
-value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
+value "matcher NULL []"
+value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
+value "matcher (CHAR a) [a,a]"
+value "matcher (STAR (CHAR a)) []"
+value "matcher (STAR (CHAR a)) [a,a]"
+value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
+value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
section {* Incorrect Matcher - fun-definition rejected *}
-function
+fun
match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
where
"match [] [] = True"
@@ -182,8 +202,6 @@
| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)"
| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
-apply(pat_completeness)
-apply(auto)
-done
+
end
\ No newline at end of file