1 theory Matcher |
1 theory Matcher |
2 imports "Main" |
2 imports "Main" |
3 begin |
3 begin |
4 |
4 |
|
5 term "TYPE (nat * int)" |
|
6 term "TYPE ('a)" |
|
7 |
|
8 definition |
|
9 P:: "'a itself \<Rightarrow> bool" |
|
10 where |
|
11 "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))" |
|
12 |
5 |
13 |
6 section {* Sequential Composition of Sets *} |
14 section {* Sequential Composition of Sets *} |
7 |
15 |
8 fun |
16 definition |
9 lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
17 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
10 where |
18 where |
11 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
19 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
|
20 |
|
21 |
|
22 text {* Two Simple Properties about Sequential Composition *} |
|
23 |
|
24 lemma seq_empty [simp]: |
|
25 shows "A ;; {[]} = A" |
|
26 and "{[]} ;; A = A" |
|
27 by (simp_all add: Seq_def) |
|
28 |
|
29 lemma seq_null [simp]: |
|
30 shows "A ;; {} = {}" |
|
31 and "{} ;; A = {}" |
|
32 by (simp_all add: Seq_def) |
12 |
33 |
13 |
34 |
14 section {* Kleene Star for Sets *} |
35 section {* Kleene Star for Sets *} |
15 |
36 |
16 inductive_set |
37 inductive_set |
17 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
38 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
18 for L :: "string set" |
39 for A :: "string set" |
19 where |
40 where |
20 start[intro]: "[] \<in> L\<star>" |
41 start[intro]: "[] \<in> A\<star>" |
21 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>" |
42 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
22 |
43 |
23 |
44 |
24 text {* A standard property of Star *} |
45 text {* A Standard Property of Star *} |
25 |
46 |
26 lemma lang_star_cases: |
47 lemma star_cases: |
27 shows "L\<star> = {[]} \<union> L ;; L\<star>" |
48 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
49 unfolding Seq_def |
28 by (auto) (metis Star.simps) |
50 by (auto) (metis Star.simps) |
|
51 |
|
52 lemma star_decomp: |
|
53 assumes a: "c # x \<in> A\<star>" |
|
54 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
|
55 using a |
|
56 by (induct x\<equiv>"c # x" rule: Star.induct) |
|
57 (auto simp add: append_eq_Cons_conv) |
|
58 |
|
59 section {* Left-Quotient of a Set *} |
|
60 |
|
61 definition |
|
62 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
63 where |
|
64 "Der c A \<equiv> {s. [c] @ s \<in> A}" |
|
65 |
|
66 lemma Der_null [simp]: |
|
67 shows "Der c {} = {}" |
|
68 unfolding Der_def |
|
69 by auto |
|
70 |
|
71 lemma Der_empty [simp]: |
|
72 shows "Der c {[]} = {}" |
|
73 unfolding Der_def |
|
74 by auto |
|
75 |
|
76 lemma Der_char [simp]: |
|
77 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
78 unfolding Der_def |
|
79 by auto |
|
80 |
|
81 lemma Der_union [simp]: |
|
82 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
83 unfolding Der_def |
|
84 by auto |
|
85 |
|
86 lemma Der_seq [simp]: |
|
87 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
88 unfolding Der_def Seq_def |
|
89 by (auto simp add: Cons_eq_append_conv) |
|
90 |
|
91 lemma Der_star [simp]: |
|
92 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
93 proof - |
|
94 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
95 by (simp only: star_cases[symmetric]) |
|
96 also have "... = Der c (A ;; A\<star>)" |
|
97 by (simp only: Der_union Der_empty) (simp) |
|
98 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
99 by simp |
|
100 also have "... = (Der c A) ;; A\<star>" |
|
101 unfolding Seq_def Der_def |
|
102 by (auto dest: star_decomp) |
|
103 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
104 qed |
|
105 |
29 |
106 |
30 section {* Regular Expressions *} |
107 section {* Regular Expressions *} |
31 |
108 |
32 datatype rexp = |
109 datatype rexp = |
33 NULL |
110 NULL |
35 | CHAR char |
112 | CHAR char |
36 | SEQ rexp rexp |
113 | SEQ rexp rexp |
37 | ALT rexp rexp |
114 | ALT rexp rexp |
38 | STAR rexp |
115 | STAR rexp |
39 |
116 |
40 types lang = "string set" |
|
41 |
|
42 definition |
|
43 DERIV :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
44 where |
|
45 "DERIV s A \<equiv> {s'. s @ s' \<in> A}" |
|
46 |
|
47 definition |
|
48 delta :: "lang \<Rightarrow> lang" |
|
49 where |
|
50 "delta A = (if [] \<in> A then {[]} else {})" |
|
51 |
|
52 lemma |
|
53 "DERIV s (P ; Q) = \<Union>{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}" |
|
54 apply(auto) |
|
55 |
|
56 fun |
|
57 D1 :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
58 where |
|
59 "D1 [] A = A" |
|
60 | "D1 (c # s) A = DERIV [c] (D1 s A)" |
|
61 |
|
62 fun |
|
63 D2 :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
64 where |
|
65 "D2 [] A = A" |
|
66 | "D2 (c # s) A = DERIV [c] (D1 s A)" |
|
67 |
|
68 function |
|
69 D |
|
70 where |
|
71 "D s P Q = P ;; Q" |
|
72 | "D (c#s) = |
|
73 |
117 |
74 section {* Semantics of Regular Expressions *} |
118 section {* Semantics of Regular Expressions *} |
75 |
119 |
76 fun |
120 fun |
77 L :: "rexp \<Rightarrow> string set" |
121 L :: "rexp \<Rightarrow> string set" |
78 where |
122 where |
79 "L (NULL) = {}" |
123 "L (NULL) = {}" |
80 | "L (EMPTY) = {[]}" |
124 | "L (EMPTY) = {[]}" |
81 | "L (CHAR c) = {[c]}" |
125 | "L (CHAR c) = {[c]}" |
82 | "L (SEQ r1 r2) = (L r1) ; (L r2)" |
126 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
83 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
127 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
84 | "L (STAR r) = (L r)\<star>" |
128 | "L (STAR r) = (L r)\<star>" |
85 |
|
86 |
129 |
87 section {* The Matcher *} |
130 section {* The Matcher *} |
88 |
131 |
89 fun |
132 fun |
90 nullable :: "rexp \<Rightarrow> bool" |
133 nullable :: "rexp \<Rightarrow> bool" |
111 where |
154 where |
112 "derivative [] r = r" |
155 "derivative [] r = r" |
113 | "derivative (c # s) r = derivative s (der c r)" |
156 | "derivative (c # s) r = derivative s (der c r)" |
114 |
157 |
115 fun |
158 fun |
116 matches :: "rexp \<Rightarrow> string \<Rightarrow> bool" |
159 matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool" |
117 where |
160 where |
118 "matches r s = nullable (derivative s r)" |
161 "matcher r s = nullable (derivative s r)" |
119 |
162 |
120 |
163 |
121 section {* Correctness Proof of the Matcher *} |
164 section {* Correctness Proof of the Matcher *} |
122 |
165 |
123 lemma nullable_correctness: |
166 lemma nullable_correctness: |
124 shows "nullable r \<longleftrightarrow> [] \<in> L r" |
167 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
125 by (induct r) (auto) |
168 by (induct r) (auto simp add: Seq_def) |
|
169 |
126 |
170 |
127 lemma der_correctness: |
171 lemma der_correctness: |
128 shows "s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" |
172 shows "L (der c r) = Der c (L r)" |
129 proof (induct r arbitrary: s) |
173 by (induct r) |
130 case (SEQ r1 r2 s) |
174 (simp_all add: nullable_correctness) |
131 have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c # s \<in> L r1" by fact |
175 |
132 have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c # s \<in> L r2" by fact |
176 lemma matcher_correctness: |
133 show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c # s \<in> L (SEQ r1 r2)" |
177 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
134 using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv) |
|
135 next |
|
136 case (STAR r s) |
|
137 have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" by fact |
|
138 show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c # s \<in> L (STAR r)" |
|
139 proof |
|
140 assume "s \<in> L (der c (STAR r))" |
|
141 then have "s \<in> L (der c r) ; L r\<star>" by simp |
|
142 then have "c # s \<in> L r ; (L r)\<star>" |
|
143 by (auto simp add: ih Cons_eq_append_conv) |
|
144 then have "c # s \<in> (L r)\<star>" using lang_star_cases by auto |
|
145 then show "c # s \<in> L (STAR r)" by simp |
|
146 next |
|
147 assume "c # s \<in> L (STAR r)" |
|
148 then have "c # s \<in> (L r)\<star>" by simp |
|
149 then have "s \<in> L (der c r); (L r)\<star>" |
|
150 by (induct x\<equiv>"c # s" rule: Star.induct) |
|
151 (auto simp add: ih append_eq_Cons_conv) |
|
152 then show "s \<in> L (der c (STAR r))" by simp |
|
153 qed |
|
154 qed (simp_all) |
|
155 |
|
156 lemma matches_correctness: |
|
157 shows "matches r s \<longleftrightarrow> s \<in> L r" |
|
158 by (induct s arbitrary: r) |
178 by (induct s arbitrary: r) |
159 (simp_all add: nullable_correctness der_correctness) |
179 (simp_all add: nullable_correctness der_correctness Der_def) |
160 |
180 |
161 section {* Examples *} |
181 section {* Examples *} |
162 |
182 |
163 value "matches NULL []" |
183 value "matcher NULL []" |
164 value "matches (CHAR (CHR ''a'')) [CHR ''a'']" |
184 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']" |
165 value "matches (CHAR a) [a,a]" |
185 value "matcher (CHAR a) [a,a]" |
166 value "matches (STAR (CHAR a)) []" |
186 value "matcher (STAR (CHAR a)) []" |
167 value "matches (STAR (CHAR a)) [a,a]" |
187 value "matcher (STAR (CHAR a)) [a,a]" |
168 value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''" |
188 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''" |
169 value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''" |
189 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''" |
170 |
190 |
171 section {* Incorrect Matcher - fun-definition rejected *} |
191 section {* Incorrect Matcher - fun-definition rejected *} |
172 |
192 |
173 function |
193 fun |
174 match :: "rexp list \<Rightarrow> string \<Rightarrow> bool" |
194 match :: "rexp list \<Rightarrow> string \<Rightarrow> bool" |
175 where |
195 where |
176 "match [] [] = True" |
196 "match [] [] = True" |
177 | "match [] (c # s) = False" |
197 | "match [] (c # s) = False" |
178 | "match (NULL # rs) s = False" |
198 | "match (NULL # rs) s = False" |