73 "flat(Void) = []" |
73 "flat(Void) = []" |
74 | "flat(Char c) = [c]" |
74 | "flat(Char c) = [c]" |
75 | "flat(Left v) = flat(v)" |
75 | "flat(Left v) = flat(v)" |
76 | "flat(Right v) = flat(v)" |
76 | "flat(Right v) = flat(v)" |
77 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
77 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
|
78 |
|
79 fun head :: "val \<Rightarrow> string" |
|
80 where |
|
81 "head(Void) = []" |
|
82 | "head(Char c) = [c]" |
|
83 | "head(Left v) = head(v)" |
|
84 | "head(Right v) = head(v)" |
|
85 | "head(Seq v1 v2) = head v1" |
78 |
86 |
79 fun flats :: "val \<Rightarrow> string list" |
87 fun flats :: "val \<Rightarrow> string list" |
80 where |
88 where |
81 "flats(Void) = [[]]" |
89 "flats(Void) = [[]]" |
82 | "flats(Char c) = [[c]]" |
90 | "flats(Char c) = [[c]]" |
376 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
384 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
377 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
385 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
378 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
386 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
379 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
387 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
380 |
388 |
|
389 |
381 section {* Projection function *} |
390 section {* Projection function *} |
382 |
391 |
383 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
392 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
384 where |
393 where |
385 "projval (CHAR d) c _ = Void" |
394 "projval (CHAR d) c _ = Void" |
527 assumes "\<turnstile> v : r" and "(flat v) = c # s" |
536 assumes "\<turnstile> v : r" and "(flat v) = c # s" |
528 shows "flat (projval r c v) = s" |
537 shows "flat (projval r c v) = s" |
529 using assms |
538 using assms |
530 by (metis list.inject v4_proj) |
539 by (metis list.inject v4_proj) |
531 |
540 |
|
541 lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}" |
|
542 apply(induct c r rule: der.induct) |
|
543 unfolding inj_on_def |
|
544 apply(auto)[1] |
|
545 apply(erule Prf.cases) |
|
546 apply(simp_all)[5] |
|
547 apply(auto)[1] |
|
548 apply(erule Prf.cases) |
|
549 apply(simp_all)[5] |
|
550 apply(auto)[1] |
|
551 apply(erule Prf.cases) |
|
552 apply(simp_all)[5] |
|
553 apply(erule Prf.cases) |
|
554 apply(simp_all)[5] |
|
555 apply(erule Prf.cases) |
|
556 apply(simp_all)[5] |
|
557 apply(auto)[1] |
|
558 apply(erule Prf.cases) |
|
559 apply(simp_all)[5] |
|
560 apply(erule Prf.cases) |
|
561 apply(simp_all)[5] |
|
562 apply(erule Prf.cases) |
|
563 apply(simp_all)[5] |
|
564 apply(auto)[1] |
|
565 apply(erule Prf.cases) |
|
566 apply(simp_all)[5] |
|
567 apply(erule Prf.cases) |
|
568 apply(simp_all)[5] |
|
569 apply(clarify) |
|
570 apply(erule Prf.cases) |
|
571 apply(simp_all)[5] |
|
572 apply(erule Prf.cases) |
|
573 apply(simp_all)[5] |
|
574 apply(clarify) |
|
575 apply(erule Prf.cases) |
|
576 apply(simp_all)[5] |
|
577 apply(clarify) |
|
578 apply (metis list.distinct(1) mkeps_flat v4) |
|
579 apply(erule Prf.cases) |
|
580 apply(simp_all)[5] |
|
581 apply(clarify) |
|
582 apply(rotate_tac 6) |
|
583 apply(erule Prf.cases) |
|
584 apply(simp_all)[5] |
|
585 apply (metis list.distinct(1) mkeps_flat v4) |
|
586 apply(erule Prf.cases) |
|
587 apply(simp_all)[5] |
|
588 apply(erule Prf.cases) |
|
589 apply(simp_all)[5] |
|
590 done |
|
591 |
532 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
592 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
533 by (metis list.sel(3)) |
593 by (metis list.sel(3)) |
534 |
594 |
535 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)" |
595 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)" |
536 by (metis) |
596 by (metis) |
543 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)" |
603 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)" |
544 |
604 |
545 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])" |
605 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])" |
546 by (metis Prf_flat_L nullable_correctness) |
606 by (metis Prf_flat_L nullable_correctness) |
547 |
607 |
|
608 lemma proj_inj_id: |
|
609 assumes "\<turnstile> v : der c r" |
|
610 shows "projval r c (injval r c v) = v" |
|
611 using assms |
|
612 apply(induct c r arbitrary: v rule: der.induct) |
|
613 apply(simp) |
|
614 apply(erule Prf.cases) |
|
615 apply(simp_all)[5] |
|
616 apply(simp) |
|
617 apply(erule Prf.cases) |
|
618 apply(simp_all)[5] |
|
619 apply(simp) |
|
620 apply(case_tac "c = c'") |
|
621 apply(simp) |
|
622 apply(erule Prf.cases) |
|
623 apply(simp_all)[5] |
|
624 apply(simp) |
|
625 apply(erule Prf.cases) |
|
626 apply(simp_all)[5] |
|
627 apply(simp) |
|
628 apply(erule Prf.cases) |
|
629 apply(simp_all)[5] |
|
630 apply(simp) |
|
631 apply(case_tac "nullable r1") |
|
632 apply(simp) |
|
633 apply(erule Prf.cases) |
|
634 apply(simp_all)[5] |
|
635 apply(auto)[1] |
|
636 apply(erule Prf.cases) |
|
637 apply(simp_all)[5] |
|
638 apply(auto)[1] |
|
639 apply (metis list.distinct(1) v4) |
|
640 apply(auto)[1] |
|
641 apply (metis mkeps_flat) |
|
642 apply(auto) |
|
643 apply(erule Prf.cases) |
|
644 apply(simp_all)[5] |
|
645 apply(auto)[1] |
|
646 apply(simp add: v4) |
|
647 done |
|
648 |
|
649 (* |
|
650 lemma |
|
651 assumes "\<turnstile> v : der c r" "flat v \<noteq> []" |
|
652 shows "injval r c v \<succ>r mkeps r" |
|
653 using assms |
|
654 apply(induct c r arbitrary: v rule: der.induct) |
|
655 apply(simp_all) |
|
656 apply(erule Prf.cases) |
|
657 apply(simp_all)[5] |
|
658 apply(erule Prf.cases) |
|
659 apply(simp_all)[5] |
|
660 apply(case_tac "c = c'") |
|
661 apply(simp) |
|
662 apply(erule Prf.cases) |
|
663 apply(simp_all)[5] |
|
664 apply(simp) |
|
665 apply(erule Prf.cases) |
|
666 apply(simp_all)[5] |
|
667 apply(auto)[1] |
|
668 apply(erule Prf.cases) |
|
669 apply(simp_all)[5] |
|
670 apply(clarify) |
|
671 apply (metis ValOrd.intros(6)) |
|
672 apply(clarify) |
|
673 apply (metis ValOrd.intros(4) drop_0 drop_all le_add2 list.distinct(1) list.size(3) mkeps_flat monoid_add_class.add.right_neutral nat_less_le v4) |
|
674 apply(erule Prf.cases) |
|
675 apply(simp_all)[5] |
|
676 apply(clarify) |
|
677 apply(rule ValOrd.intros) |
|
678 apply(simp) |
|
679 defer |
|
680 apply(rule ValOrd.intros) |
|
681 apply metis |
|
682 apply(case_tac "nullable r1") |
|
683 apply(simp) |
|
684 apply(erule Prf.cases) |
|
685 apply(simp_all)[5] |
|
686 apply(clarify) |
|
687 apply(erule Prf.cases) |
|
688 apply(simp_all)[5] |
|
689 apply(clarify) |
|
690 defer |
|
691 apply(clarify) |
|
692 apply(rule ValOrd.intros) |
|
693 apply metis |
|
694 apply(simp) |
|
695 apply(erule Prf.cases) |
|
696 apply(simp_all)[5] |
|
697 apply(clarify) |
|
698 defer |
|
699 apply(subst mkeps_flat) |
|
700 oops |
|
701 *) |
|
702 |
548 lemma Prf_inj: |
703 lemma Prf_inj: |
549 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
704 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
550 shows "(injval r c v1) \<succ>r (injval r c v2)" |
705 shows "(injval r c v1) \<succ>r (injval r c v2)" |
551 using assms |
706 using assms |
552 apply(induct arbitrary: v1 v2 rule: der.induct) |
707 apply(induct arbitrary: v1 v2 rule: der.induct) |
625 apply(rule ValOrd.intros) |
780 apply(rule ValOrd.intros) |
626 apply(simp) |
781 apply(simp) |
627 apply(clarify) |
782 apply(clarify) |
628 apply(rule ValOrd.intros(2)) |
783 apply(rule ValOrd.intros(2)) |
629 apply metis |
784 apply metis |
630 |
785 using injval_inj |
631 apply(erule Prf.cases) |
786 apply(simp add: inj_on_def) |
632 apply(simp_all)[5] |
787 apply metis |
633 apply(erule Prf.cases) |
788 (* SEQ nullable case *) |
634 apply(simp_all)[5] |
789 apply(erule Prf.cases) |
635 apply(clarify) |
790 apply(simp_all)[5] |
|
791 apply(clarify) |
|
792 apply(erule Prf.cases) |
|
793 apply(simp_all)[5] |
|
794 apply(clarify) |
|
795 apply(erule Prf.cases) |
|
796 apply(simp_all)[5] |
|
797 apply(clarify) |
|
798 apply(erule Prf.cases) |
|
799 apply(simp_all)[5] |
|
800 apply(clarify) |
|
801 apply(erule ValOrd.cases) |
|
802 apply(simp_all)[8] |
|
803 apply(clarify) |
|
804 apply(erule ValOrd.cases) |
|
805 apply(simp_all)[8] |
|
806 apply(clarify) |
|
807 apply(rule ValOrd.intros(1)) |
|
808 apply(simp) |
|
809 apply(rule ValOrd.intros(2)) |
|
810 apply metis |
|
811 using injval_inj |
|
812 apply(simp add: inj_on_def) |
|
813 apply metis |
|
814 apply(clarify) |
|
815 apply(erule Prf.cases) |
|
816 apply(simp_all)[5] |
|
817 apply(clarify) |
|
818 apply(erule ValOrd.cases) |
|
819 apply(simp_all)[8] |
|
820 apply(clarify) |
|
821 apply(simp) |
|
822 apply(rule ValOrd.intros(2)) |
|
823 prefer 2 |
|
824 apply (metis list.distinct(1) mkeps_flat v4) |
|
825 defer |
|
826 apply(clarify) |
|
827 apply(erule Prf.cases) |
|
828 apply(simp_all)[5] |
|
829 apply(clarify) |
|
830 apply(rotate_tac 6) |
|
831 apply(erule Prf.cases) |
|
832 apply(simp_all)[5] |
|
833 apply(clarify) |
|
834 apply(erule ValOrd.cases) |
|
835 apply(simp_all)[8] |
|
836 apply(clarify) |
|
837 apply(simp) |
|
838 apply(rule ValOrd.intros(2)) |
|
839 prefer 2 |
|
840 apply (metis list.distinct(1) mkeps_flat v4) |
|
841 defer |
|
842 apply(clarify) |
|
843 apply(erule ValOrd.cases) |
|
844 apply(simp_all)[8] |
|
845 apply(clarify) |
|
846 apply(rule ValOrd.intros(1)) |
|
847 apply(metis) |
|
848 apply(drule_tac x="v1" in meta_spec) |
|
849 apply(rotate_tac 7) |
|
850 apply(drule_tac x="projval r1 c (mkeps r1)" in meta_spec) |
|
851 apply(drule meta_mp) |
|
852 |
636 defer |
853 defer |
637 apply(erule ValOrd.cases) |
854 apply(erule ValOrd.cases) |
638 apply(simp_all del: injval.simps)[8] |
855 apply(simp_all del: injval.simps)[8] |
639 apply(simp) |
856 apply(simp) |
640 apply(clarify) |
857 apply(clarify) |