24 | PLUS rexp |
24 | PLUS rexp |
25 | OPT rexp |
25 | OPT rexp |
26 | NTIMES rexp nat |
26 | NTIMES rexp nat |
27 | NMTIMES rexp nat nat |
27 | NMTIMES rexp nat nat |
28 |
28 |
29 fun M :: "rexp \<Rightarrow> nat" |
|
30 where |
|
31 "M (NULL) = 0" |
|
32 | "M (EMPTY) = 0" |
|
33 | "M (CHAR char) = 0" |
|
34 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))" |
|
35 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))" |
|
36 | "M (STAR r) = Suc (M r)" |
|
37 | "M (NOT r) = Suc (M r)" |
|
38 | "M (PLUS r) = Suc (M r)" |
|
39 | "M (OPT r) = Suc (M r)" |
|
40 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
|
41 | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc m - Suc n)" |
|
42 |
29 |
43 section {* Sequential Composition of Sets *} |
30 section {* Sequential Composition of Sets *} |
44 |
31 |
45 definition |
32 definition |
46 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
33 Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
180 | "nullable (NOT r) = (\<not>(nullable r))" |
167 | "nullable (NOT r) = (\<not>(nullable r))" |
181 | "nullable (PLUS r) = (nullable r)" |
168 | "nullable (PLUS r) = (nullable r)" |
182 | "nullable (OPT r) = True" |
169 | "nullable (OPT r) = True" |
183 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
170 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
184 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
171 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
|
172 |
|
173 fun M :: "rexp \<Rightarrow> nat" |
|
174 where |
|
175 "M (NULL) = 0" |
|
176 | "M (EMPTY) = 0" |
|
177 | "M (CHAR char) = 0" |
|
178 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))" |
|
179 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))" |
|
180 | "M (STAR r) = Suc (M r)" |
|
181 | "M (NOT r) = Suc (M r)" |
|
182 | "M (PLUS r) = Suc (M r)" |
|
183 | "M (OPT r) = Suc (M r)" |
|
184 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
|
185 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)" |
|
186 |
185 |
187 |
186 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
188 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
187 where |
189 where |
188 "der c (NULL) = NULL" |
190 "der c (NULL) = NULL" |
189 | "der c (EMPTY) = NULL" |
191 | "der c (EMPTY) = NULL" |
195 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
197 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
196 | "der c (OPT r) = der c r" |
198 | "der c (OPT r) = der c r" |
197 | "der c (NTIMES r 0) = NULL" |
199 | "der c (NTIMES r 0) = NULL" |
198 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
200 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
199 | "der c (NMTIMES r n m) = |
201 | "der c (NMTIMES r n m) = |
200 (if m < n then NULL else |
202 (if m < n then NULL else |
201 (if m = 0 then NULL else |
203 (if n = m then der c (NTIMES r n) else |
202 (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))" |
204 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))" |
203 (* |
|
204 |
|
205 (if m < n then NULL else |
|
206 (if n = m then der c (NTIMES r n) else |
|
207 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))" |
|
208 *) |
|
209 by pat_completeness auto |
205 by pat_completeness auto |
|
206 |
|
207 lemma bigger1: |
|
208 "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b" |
|
209 by (metis le0 mult_strict_mono') |
210 |
210 |
211 termination der |
211 termination der |
212 apply(relation "measure (\<lambda>(c, r). M r)") |
212 apply(relation "measure (\<lambda>(c, r). M r)") |
213 apply(simp_all) |
213 apply(simp) |
214 sorry |
214 apply(simp) |
215 |
215 apply(simp) |
216 |
216 apply(simp) |
|
217 apply(simp) |
|
218 apply(simp) |
|
219 apply(simp) |
|
220 apply(simp) |
|
221 apply(simp) |
|
222 apply(simp) |
|
223 apply(simp) |
|
224 apply(simp_all del: M.simps) |
|
225 apply(simp_all only: M.simps) |
|
226 defer |
|
227 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n") |
|
228 prefer 2 |
|
229 apply(auto)[1] |
|
230 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc) |
|
231 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)") |
|
232 prefer 2 |
|
233 apply(auto)[1] |
|
234 apply(subgoal_tac "Suc n < Suc m") |
|
235 prefer 2 |
|
236 apply(auto)[1] |
|
237 apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m") |
|
238 prefer 2 |
|
239 apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2") |
|
240 prefer 2 |
|
241 apply(auto)[1] |
|
242 apply(rule bigger1) |
|
243 apply(assumption) |
|
244 apply(simp) |
|
245 apply (metis zero_less_Suc) |
|
246 apply (metis mult_is_0 neq0_conv old.nat.distinct(2)) |
|
247 apply(rotate_tac 4) |
|
248 apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1) |
|
249 prefer 4 |
|
250 apply(simp) |
|
251 apply(simp) |
|
252 apply (metis zero_less_one) |
|
253 apply(simp) |
|
254 done |
217 |
255 |
218 fun |
256 fun |
219 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
257 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
220 where |
258 where |
221 "ders [] r = r" |
259 "ders [] r = r" |
304 lemma der_correctness: |
342 lemma der_correctness: |
305 shows "L (der c r) = Der c (L r)" |
343 shows "L (der c r) = Der c (L r)" |
306 apply(induct rule: der.induct) |
344 apply(induct rule: der.induct) |
307 apply(simp_all add: nullable_correctness |
345 apply(simp_all add: nullable_correctness |
308 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
346 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
309 apply(case_tac "[] \<in> L r") |
347 apply(rule impI)+ |
310 apply(simp) |
348 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}") |
311 apply(case_tac n) |
|
312 apply(auto)[1] |
|
313 apply(case_tac m) |
|
314 apply(simp) |
|
315 apply(auto simp add: )[1] |
|
316 apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq) |
|
317 |
|
318 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
|
319 apply (metis Suc_leD atLeastAtMost_iff) |
|
320 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
|
321 |
|
322 (* |
|
323 lemma der_correctness: |
|
324 shows "L (der c r) = Der c (L r)" |
|
325 apply(induct rule: der.induct) |
|
326 apply(simp_all add: nullable_correctness |
|
327 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
|
328 apply(case_tac m) |
|
329 apply(simp) |
|
330 apply(simp) |
|
331 apply(auto) |
349 apply(auto) |
332 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
350 done |
333 apply (metis Suc_leD atLeastAtMost_iff) |
|
334 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
|
335 *) |
|
336 |
351 |
337 lemma matcher_correctness: |
352 lemma matcher_correctness: |
338 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
353 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
339 by (induct s arbitrary: r) |
354 by (induct s arbitrary: r) |
340 (simp_all add: nullable_correctness der_correctness Der_def) |
355 (simp_all add: nullable_correctness der_correctness Der_def) |
341 |
356 |
342 |
|
343 lemma "L (der c (NMTIMES r n m)) = |
|
344 L ((if m < n then NULL else |
|
345 (if m = 0 then NULL else |
|
346 (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))" |
|
347 apply(subst der.simps(12)) |
|
348 apply(auto simp del: der.simps) |
|
349 apply(simp) |
|
350 apply(auto)[1] |
|
351 apply(case_tac m) |
|
352 apply(simp) |
|
353 apply(simp) |
|
354 apply(case_tac m) |
|
355 apply(simp) |
|
356 apply(simp) |
|
357 apply(simp) |
|
358 apply(subst (asm) der.simps(12)) |
|
359 apply(auto)[1] |
|
360 apply(case_tac m) |
|
361 apply(simp) |
|
362 apply(simp) |
|
363 apply(case_tac m) |
|
364 apply(simp) |
|
365 apply(simp) |
|
366 apply(auto)[1] |
|
367 apply(auto simp del: der.simps(12))[1] |
|
368 apply(subst (asm) der.simps(12)) |
|
369 apply(case_tac n) |
|
370 apply(simp) |
|
371 apply(simp) |
|
372 apply(case_tac m) |
|
373 apply(simp) |
|
374 apply(simp) |
|
375 apply(case_tac "Suc nat = nata") |
|
376 apply(simp) |
|
377 apply(auto simp del: der.simps(12))[1] |
|
378 apply(auto)[1] |
|
379 apply(case_tac n) |
|
380 apply(simp) |
|
381 apply(simp) |
|
382 apply(case_tac m) |
|
383 apply(simp) |
|
384 apply(simp) |
|
385 apply(simp add: Seq_def) |
|
386 apply(auto)[1] |
|
387 apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat) |
|
388 apply(simp (no_asm) del: der.simps(12)) |
|
389 apply(auto simp del: der.simps(12))[1] |
|
390 apply(case_tac "m = Suc n") |
|
391 apply(simp) |
|
392 apply(case_tac n) |
|
393 apply(simp) |
|
394 apply(simp) |
|
395 apply(auto simp add: Seq_def del: der.simps(12))[1] |
|
396 |
|
397 apply(case_tac n) |
|
398 apply(simp) |
|
399 apply(case_tac m) |
|
400 apply(simp) |
|
401 apply(simp) |
|
402 apply(simp add: Seq_def) |
|
403 apply(auto)[1] |
|
404 apply(case_tac "nat = 0") |
|
405 apply(simp) |
|
406 apply(simp) |
|
407 apply(auto)[1] |
|
408 apply(case_tac "Suc 0 = nat") |
|
409 apply(simp) |
|
410 apply(auto simp del: der.simps(12))[1] |
|
411 apply(simp) |
|
412 apply(case_tac "Suc 0 = nat") |
|
413 apply(simp) |
|
414 apply(auto simp add: Seq_def del: der.simps(12))[1] |
|
415 apply(rule_tac x="s1" in exI) |
|
416 apply(rule_tac x="s2" in exI) |
|
417 apply(simp) |
|
418 apply(rule_tac x="1" in bexI) |
|
419 apply(simp) |
|
420 apply(simp) |
|
421 apply(simp) |
|
422 apply(auto simp add: Seq_def)[1] |
|
423 apply(case_tac m) |
|
424 apply(simp) |
|
425 apply(simp) |
|
426 |
|
427 end |
357 end |