239 | "L (NTIMES r n) = (L r) \<up> n" |
242 | "L (NTIMES r n) = (L r) \<up> n" |
240 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
243 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
241 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
244 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
242 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)" |
245 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)" |
243 | "L (AND r1 r2) = (L r1) \<inter> (L r2)" |
246 | "L (AND r1 r2) = (L r1) \<inter> (L r2)" |
|
247 | "L (NOT r) = UNIV - (L r)" |
|
248 | "L (ALLL) = UNIV" |
|
249 | "L (ALLBUT) = UNIV - {[]}" |
244 |
250 |
245 section {* Nullable, Derivatives *} |
251 section {* Nullable, Derivatives *} |
246 |
252 |
247 fun |
253 fun |
248 nullable :: "rexp \<Rightarrow> bool" |
254 nullable :: "rexp \<Rightarrow> bool" |
257 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
263 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
258 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
264 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
259 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
265 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
260 | "nullable (PLUS r) = (nullable r)" |
266 | "nullable (PLUS r) = (nullable r)" |
261 | "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)" |
267 | "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)" |
|
268 | "nullable (NOT r) = (\<not>nullable r)" |
|
269 | "nullable (ALLL) = True" |
|
270 | "nullable (ALLBUT) = False" |
|
271 |
262 |
272 |
263 fun |
273 fun |
264 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
274 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
265 where |
275 where |
266 "der c (ZERO) = ZERO" |
276 "der c (ZERO) = ZERO" |
283 else (if n = 0 then (if m = 0 then ZERO else |
293 else (if n = 0 then (if m = 0 then ZERO else |
284 SEQ (der c r) (UPNTIMES r (m - 1))) else |
294 SEQ (der c r) (UPNTIMES r (m - 1))) else |
285 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
295 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
286 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
296 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
287 | "der c (AND r1 r2) = AND (der c r1) (der c r2)" |
297 | "der c (AND r1 r2) = AND (der c r1) (der c r2)" |
|
298 | "der c (NOT r) = NOT (der c r)" |
|
299 | "der c (ALLL) = ALLL" |
|
300 | "der c (ALLBUT) = ALLL" |
|
301 |
288 |
302 |
289 fun |
303 fun |
290 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
304 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
291 where |
305 where |
292 "ders [] r = r" |
306 "ders [] r = r" |
337 apply(case_tac "n \<le> m") |
351 apply(case_tac "n \<le> m") |
338 prefer 2 |
352 prefer 2 |
339 apply(simp only: der.simps if_True) |
353 apply(simp only: der.simps if_True) |
340 apply(simp only: L.simps) |
354 apply(simp only: L.simps) |
341 apply(simp) |
355 apply(simp) |
342 apply(auto) |
356 apply(auto)[3] |
343 apply(subst (asm) Sequ_UNION[symmetric]) |
357 apply(subst (asm) Sequ_UNION[symmetric]) |
344 apply(subst (asm) test[symmetric]) |
358 apply(subst (asm) test[symmetric]) |
345 apply(auto simp add: Der_UNION)[1] |
359 apply(auto simp add: Der_UNION)[1] |
346 apply(auto simp add: Der_UNION)[1] |
360 apply(auto simp add: Der_UNION)[1] |
347 apply(subst Sequ_UNION[symmetric]) |
361 apply(subst Sequ_UNION[symmetric]) |
362 apply(simp add: Der_UNION) |
376 apply(simp add: Der_UNION) |
363 apply(erule_tac bexE) |
377 apply(erule_tac bexE) |
364 apply(case_tac xa) |
378 apply(case_tac xa) |
365 apply(simp) |
379 apply(simp) |
366 apply(simp) |
380 apply(simp) |
367 apply(auto) |
381 apply(auto)[1] |
368 apply(auto simp add: Sequ_def Der_def)[1] |
382 apply(auto simp add: Sequ_def Der_def)[1] |
369 using Star_def apply auto[1] |
383 using Star_def apply auto[1] |
370 apply(case_tac "[] \<in> L r") |
384 apply(case_tac "[] \<in> L r") |
371 apply(auto) |
385 apply(auto)[1] |
372 using Der_UNION Der_star Star_def by fastforce |
386 using Der_UNION Der_star Star_def apply fastforce |
|
387 apply(simp) |
|
388 apply(simp) |
|
389 apply(simp add: Der_def) |
|
390 apply(blast) |
|
391 (* ALLL*) |
|
392 apply(simp add: Der_def) |
|
393 apply(simp add: Der_def) |
|
394 done |
373 |
395 |
374 lemma ders_correctness: |
396 lemma ders_correctness: |
375 shows "L (ders s r) = Ders s (L r)" |
397 shows "L (ders s r) = Ders s (L r)" |
376 apply(induct s arbitrary: r) |
398 apply(induct s arbitrary: r) |
377 apply(simp_all add: Ders_def der_correctness Der_def) |
399 apply(simp_all add: Ders_def der_correctness Der_def) |
424 | "flat (Right v) = flat v" |
449 | "flat (Right v) = flat v" |
425 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
450 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
426 | "flat (Stars []) = []" |
451 | "flat (Stars []) = []" |
427 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
452 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
428 | "flat (And v1 v2) = flat v1" |
453 | "flat (And v1 v2) = flat v1" |
|
454 | "flat (Not v) = flat v" |
|
455 | "flat Allbut = []" |
|
456 |
429 |
457 |
430 lemma flat_Stars [simp]: |
458 lemma flat_Stars [simp]: |
431 "flat (Stars vs) = concat (map flat vs)" |
459 "flat (Stars vs) = concat (map flat vs)" |
432 by (induct vs) (auto) |
460 by (induct vs) (auto) |
433 |
461 |
434 |
|
435 section {* Relation between values and regular expressions *} |
|
436 |
|
437 inductive |
|
438 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
439 where |
|
440 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
441 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
442 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
443 | "\<turnstile> Void : ONE" |
|
444 | "\<turnstile> Char c : CHAR c" |
|
445 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
|
446 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
|
447 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
|
448 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
|
449 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m" |
|
450 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r" |
|
451 | "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2; flat v1 = flat v2\<rbrakk> \<Longrightarrow> \<turnstile> And v1 v2: AND r1 r2" |
|
452 |
|
453 |
|
454 inductive_cases Prf_elims: |
|
455 "\<turnstile> v : ZERO" |
|
456 "\<turnstile> v : SEQ r1 r2" |
|
457 "\<turnstile> v : ALT r1 r2" |
|
458 "\<turnstile> v : ONE" |
|
459 "\<turnstile> v : CHAR c" |
|
460 (* "\<turnstile> vs : STAR r"*) |
|
461 |
|
462 lemma Prf_STAR: |
|
463 assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" |
|
464 shows "concat (map flat vs) \<in> L r\<star>" |
|
465 using assms |
|
466 apply(induct vs) |
|
467 apply(auto) |
|
468 done |
|
469 |
|
470 lemma Prf_Pow: |
|
471 assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" |
|
472 shows "concat (map flat vs) \<in> L r \<up> length vs" |
|
473 using assms |
|
474 apply(induct vs) |
|
475 apply(auto simp add: Sequ_def) |
|
476 done |
|
477 |
|
478 lemma Prf_flat_L: |
|
479 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
|
480 using assms |
|
481 apply(induct v r rule: Prf.induct) |
|
482 apply(auto simp add: Sequ_def) |
|
483 apply(rule Prf_STAR) |
|
484 apply(simp) |
|
485 apply(rule_tac x="length vs" in bexI) |
|
486 apply(rule Prf_Pow) |
|
487 apply(simp) |
|
488 apply(simp) |
|
489 apply(rule Prf_Pow) |
|
490 apply(simp) |
|
491 apply(rule_tac x="length vs" in bexI) |
|
492 apply(rule Prf_Pow) |
|
493 apply(simp) |
|
494 apply(simp) |
|
495 apply(rule_tac x="length vs" in bexI) |
|
496 apply(rule Prf_Pow) |
|
497 apply(simp) |
|
498 apply(simp) |
|
499 using Prf_Pow by blast |
|
500 |
|
501 lemma Star_Pow: |
462 lemma Star_Pow: |
502 assumes "s \<in> A \<up> n" |
463 assumes "s \<in> A \<up> n" |
503 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)" |
464 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)" |
504 using assms |
465 using assms |
505 apply(induct n arbitrary: s) |
466 apply(induct n arbitrary: s) |
514 assumes "s \<in> A\<star>" |
475 assumes "s \<in> A\<star>" |
515 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
476 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
516 using assms |
477 using assms |
517 apply(auto simp add: Star_def) |
478 apply(auto simp add: Star_def) |
518 using Star_Pow by blast |
479 using Star_Pow by blast |
519 |
|
520 |
|
521 lemma Star_val: |
|
522 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
523 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
524 using assms |
|
525 apply(induct ss) |
|
526 apply(auto) |
|
527 apply (metis empty_iff list.set(1)) |
|
528 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
529 |
|
530 lemma Star_val_length: |
|
531 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
532 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r) \<and> (length vs) = (length ss)" |
|
533 using assms |
|
534 apply(induct ss) |
|
535 apply(auto) |
|
536 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD) |
|
537 |
|
538 |
|
539 |
|
540 |
|
541 |
|
542 lemma L_flat_Prf2: |
|
543 assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
|
544 using assms |
|
545 apply(induct r arbitrary: s) |
|
546 apply(auto simp add: Sequ_def intro: Prf.intros) |
|
547 using Prf.intros(1) flat.simps(5) apply blast |
|
548 using Prf.intros(2) flat.simps(3) apply blast |
|
549 using Prf.intros(3) flat.simps(4) apply blast |
|
550 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
|
551 apply(auto)[1] |
|
552 apply(rule_tac x="Stars vs" in exI) |
|
553 apply(simp) |
|
554 apply(rule Prf.intros) |
|
555 apply(simp) |
|
556 using Star_string Star_val apply force |
|
557 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
558 apply(auto)[1] |
|
559 apply(rule_tac x="Stars vs" in exI) |
|
560 apply(simp) |
|
561 apply(rule Prf.intros) |
|
562 apply(simp) |
|
563 apply(simp) |
|
564 using Star_Pow Star_val_length apply blast |
|
565 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)") |
|
566 apply(auto)[1] |
|
567 apply(rule_tac x="Stars vs" in exI) |
|
568 apply(simp) |
|
569 apply(rule Prf.intros) |
|
570 apply(simp) |
|
571 apply(simp) |
|
572 using Star_Pow Star_val_length apply blast |
|
573 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
574 apply(auto)[1] |
|
575 apply(rule_tac x="Stars vs" in exI) |
|
576 apply(simp) |
|
577 apply(rule Prf.intros) |
|
578 apply(simp) |
|
579 apply(simp) |
|
580 using Star_Pow Star_val_length apply blast |
|
581 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
582 apply(auto)[1] |
|
583 apply(rule_tac x="Stars vs" in exI) |
|
584 apply(simp) |
|
585 apply(rule Prf.intros) |
|
586 apply(simp) |
|
587 apply(simp) |
|
588 apply(simp) |
|
589 using Star_Pow Star_val_length apply blast |
|
590 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
591 apply(auto)[1] |
|
592 apply(rule_tac x="Stars vs" in exI) |
|
593 apply(simp) |
|
594 apply(rule Prf.intros) |
|
595 apply(simp) |
|
596 apply(simp) |
|
597 using Star_Pow Star_val_length apply blast |
|
598 (* AND *) |
|
599 using Prf.intros(12) by fastforce |
|
600 |
|
601 lemma L_flat_Prf: |
|
602 "L(r) = {flat v | v. \<turnstile> v : r}" |
|
603 using Prf_flat_L L_flat_Prf2 by blast |
|
604 |
480 |
605 |
481 |
606 section {* Sulzmann and Lu functions *} |
482 section {* Sulzmann and Lu functions *} |
607 |
483 |
608 fun |
484 fun |
616 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
492 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
617 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
493 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
618 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
494 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
619 | "mkeps(PLUS r) = Stars ([mkeps r])" |
495 | "mkeps(PLUS r) = Stars ([mkeps r])" |
620 | "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)" |
496 | "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)" |
|
497 | "mkeps(NOT r) = Not (Allbut)" |
|
498 | "mkeps(ALLL) = Void" |
621 |
499 |
622 |
500 |
623 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
501 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
624 where |
502 where |
625 "injval (CHAR d) c Void = Char d" |
503 "injval (CHAR d) c Void = Char d" |
634 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
512 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
635 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
513 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
636 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
514 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
637 | "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)" |
515 | "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)" |
638 |
516 |
|
517 |
639 section {* Mkeps, injval *} |
518 section {* Mkeps, injval *} |
640 |
519 |
641 lemma mkeps_flat: |
520 lemma mkeps_flat: |
642 assumes "nullable(r)" |
521 assumes "nullable(r)" |
643 shows "flat (mkeps r) = []" |
522 shows "flat (mkeps r) = []" |
644 using assms |
523 using assms |
645 apply (induct rule: nullable.induct) |
524 apply (induct r) |
646 apply(auto) |
525 apply(auto)[15] |
647 by meson |
526 apply(case_tac "x3a < x2") |
648 |
527 apply(auto)[2] |
649 lemma mkeps_nullable: |
|
650 assumes "nullable(r)" |
|
651 shows "\<turnstile> mkeps r : r" |
|
652 using assms |
|
653 apply(induct r rule: mkeps.induct) |
|
654 apply(auto intro: Prf.intros) |
|
655 apply(metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl) |
|
656 apply(rule Prf.intros) |
|
657 apply(simp_all add: mkeps_flat) |
|
658 done |
528 done |
659 |
529 |
660 lemma Prf_injval_flat: |
530 lemma Prf_injval_flat: |
661 assumes "\<turnstile> v : der c r" |
531 assumes "flat v \<in> L (der c r)" |
662 shows "flat (injval r c v) = c # (flat v)" |
532 shows "flat (injval r c v) = c # (flat v)" |
663 using assms |
533 using assms |
664 apply(induct arbitrary: v rule: der.induct) |
534 apply(induct arbitrary: v rule: der.induct) |
|
535 apply(simp_all) |
|
536 apply(case_tac "c = d") |
|
537 prefer 2 |
|
538 apply(simp) |
|
539 apply(simp) |
665 apply(auto elim!: Prf_elims split: if_splits) |
540 apply(auto elim!: Prf_elims split: if_splits) |
666 apply(metis mkeps_flat) |
541 apply(metis mkeps_flat) |
667 apply(rotate_tac 2) |
542 apply(rotate_tac 2) |
668 apply(erule Prf.cases) |
543 apply(erule Prf.cases) |
669 apply(simp_all) |
544 apply(simp_all) |