28 | "M (NOT r) = Suc (M r)" |
38 | "M (NOT r) = Suc (M r)" |
29 | "M (PLUS r) = Suc (M r)" |
39 | "M (PLUS r) = Suc (M r)" |
30 | "M (OPT r) = Suc (M r)" |
40 | "M (OPT r) = Suc (M r)" |
31 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
41 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
32 | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)" |
42 | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)" |
|
43 | "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc n + Suc m)" |
33 |
44 |
34 section {* Sequential Composition of Sets *} |
45 section {* Sequential Composition of Sets *} |
35 |
46 |
36 definition |
47 definition |
37 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
48 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
149 | "L (NOT r) = UNIV - (L r)" |
160 | "L (NOT r) = UNIV - (L r)" |
150 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
161 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
151 | "L (OPT r) = (L r) \<union> {[]}" |
162 | "L (OPT r) = (L r) \<union> {[]}" |
152 | "L (NTIMES r n) = (L r) \<up> n" |
163 | "L (NTIMES r n) = (L r) \<up> n" |
153 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" |
164 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" |
|
165 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" |
|
166 |
154 |
167 |
155 lemma "L (NOT NULL) = UNIV" |
168 lemma "L (NOT NULL) = UNIV" |
156 apply(simp) |
169 apply(simp) |
157 done |
170 done |
158 |
171 |
|
172 lemma "L (NMTIMES r (Suc n) m) = L (SEQ r (NMTIMES r n m))" |
|
173 apply(simp add: Suc_reduce_Union Seq_def) |
|
174 apply(auto) |
|
175 done |
|
176 |
|
177 lemma "L (NMTIMES2 r (Suc n) (Suc m)) = L (SEQ r (NMTIMES2 r n m))" |
|
178 apply(simp add: Suc_reduce_Union Seq_def) |
|
179 apply(auto) |
|
180 done |
|
181 |
|
182 lemma "L (NMTIMES2 r 0 0) = {[]}" |
|
183 apply(simp add: Suc_reduce_Union Seq_def) |
|
184 done |
|
185 |
|
186 lemma t: "\<lbrakk>n \<le> i; i \<le> m\<rbrakk> \<Longrightarrow> L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \<union> L (NMTIMES2 r i m)" |
|
187 apply(auto) |
|
188 apply (metis atLeastAtMost_iff nat_le_linear) |
|
189 apply (metis atLeastAtMost_iff le_trans) |
|
190 by (metis atLeastAtMost_iff le_trans) |
|
191 |
|
192 |
|
193 lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))" |
|
194 apply(rule t) |
|
195 apply(auto) |
|
196 done |
|
197 |
|
198 lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))" |
|
199 apply(rule t) |
|
200 apply(auto) |
|
201 done |
|
202 |
|
203 lemma "L (NMTIMES2 r 0 1) = {[]} \<union> L r" |
|
204 apply(simp) |
|
205 apply(auto) |
|
206 apply(case_tac xa) |
|
207 apply(auto) |
|
208 done |
|
209 |
|
210 |
|
211 lemma "L (NMTIMES2 r n n) = L (NTIMES r n)" |
|
212 apply(simp) |
|
213 done |
|
214 |
|
215 lemma "n < m \<Longrightarrow> L (NMTIMES2 r n m) = L (NTIMES r n) \<union> L (NMTIMES2 r (Suc n) m)" |
|
216 apply(simp) |
|
217 apply(auto) |
|
218 apply (metis Suc_leI atLeastAtMost_iff le_eq_less_or_eq) |
|
219 apply (metis atLeastAtMost_iff le_eq_less_or_eq) |
|
220 by (metis Suc_leD atLeastAtMost_iff) |
159 |
221 |
160 section {* The Matcher *} |
222 section {* The Matcher *} |
161 |
223 |
162 fun |
224 fun |
163 nullable :: "rexp \<Rightarrow> bool" |
225 nullable :: "rexp \<Rightarrow> bool" |
171 | "nullable (NOT r) = (\<not>(nullable r))" |
233 | "nullable (NOT r) = (\<not>(nullable r))" |
172 | "nullable (PLUS r) = (nullable r)" |
234 | "nullable (PLUS r) = (nullable r)" |
173 | "nullable (OPT r) = True" |
235 | "nullable (OPT r) = True" |
174 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
236 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
175 | "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)" |
237 | "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)" |
|
238 | "nullable (NMTIMES2 r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
176 |
239 |
177 function |
240 function |
178 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
241 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
179 where |
242 where |
180 "der c (NULL) = NULL" |
243 "der c (NULL) = NULL" |
189 | "der c (NTIMES r 0) = NULL" |
252 | "der c (NTIMES r 0) = NULL" |
190 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
253 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
191 | "der c (NMTIMES r 0 0) = NULL" |
254 | "der c (NMTIMES r 0 0) = NULL" |
192 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" |
255 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" |
193 | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" |
256 | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" |
|
257 | "der c (NMTIMES2 r n m) = (if m < n then NULL else |
|
258 (if n = m then der c (NTIMES r n) else |
|
259 ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))" |
194 by pat_completeness auto |
260 by pat_completeness auto |
195 |
261 |
196 termination der |
262 termination der |
197 by (relation "measure (\<lambda>(c, r). M r)") (simp_all) |
263 sorry |
|
264 (*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*) |
198 |
265 |
199 |
266 |
200 fun |
267 fun |
201 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
268 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
202 where |
269 where |
211 |
278 |
212 section {* Correctness Proof of the Matcher *} |
279 section {* Correctness Proof of the Matcher *} |
213 |
280 |
214 lemma nullable_correctness: |
281 lemma nullable_correctness: |
215 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
282 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
216 by(induct r) (auto simp add: Seq_def) |
283 apply(induct r) |
217 |
284 apply(auto simp add: Seq_def) |
|
285 done |
218 |
286 |
219 section {* Left-Quotient of a Set *} |
287 section {* Left-Quotient of a Set *} |
220 |
288 |
221 definition |
289 definition |
222 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
290 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
280 |
348 |
281 lemma Der_UNION [simp]: |
349 lemma Der_UNION [simp]: |
282 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
350 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
283 by (auto simp add: Der_def) |
351 by (auto simp add: Der_def) |
284 |
352 |
285 lemma Suc_Union: |
|
286 "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))" |
|
287 by (metis UN_insert atMost_Suc) |
|
288 |
|
289 lemma Suc_reduce_Union: |
|
290 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
|
291 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
|
292 |
353 |
293 |
354 |
294 lemma der_correctness: |
355 lemma der_correctness: |
295 shows "L (der c r) = Der c (L r)" |
356 shows "L (der c r) = Der c (L r)" |
296 by (induct rule: der.induct) |
357 apply(induct rule: der.induct) |
297 (simp_all add: nullable_correctness |
358 apply(simp_all add: nullable_correctness |
298 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
359 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
|
360 apply(case_tac m) |
|
361 apply(simp) |
|
362 apply(simp) |
|
363 apply(auto) |
|
364 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
|
365 apply (metis Suc_leD atLeastAtMost_iff) |
|
366 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
299 |
367 |
300 |
368 |
301 lemma matcher_correctness: |
369 lemma matcher_correctness: |
302 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
370 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
303 by (induct s arbitrary: r) |
371 by (induct s arbitrary: r) |