580 apply(erule PMatch.cases) |
580 apply(erule PMatch.cases) |
581 apply(simp_all)[7] |
581 apply(simp_all)[7] |
582 apply(clarify) |
582 apply(clarify) |
583 by (metis PMatch1(2)) |
583 by (metis PMatch1(2)) |
584 |
584 |
585 |
|
586 |
|
587 |
|
588 (* a proof that does not need proj *) |
585 (* a proof that does not need proj *) |
589 lemma PMatch2_roy_version: |
586 lemma PMatch2_roy_version: |
590 assumes "s \<in> (der c r) \<rightarrow> v" |
587 assumes "s \<in> (der c r) \<rightarrow> v" |
591 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
588 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
592 using assms |
589 using assms |
593 apply(induct r arbitrary: s v c rule: rexp.induct) |
590 proof(induct r arbitrary: s v rule: rexp.induct) |
594 apply(auto) |
591 case ZERO |
595 (* ZERO case *) |
592 have "s \<in> der c ZERO \<rightarrow> v" by fact |
596 apply(erule PMatch.cases) |
593 then have "s \<in> ZERO \<rightarrow> v" by simp |
597 apply(simp_all)[7] |
594 then have "False" by cases |
598 (* ONE case *) |
595 then show "(c#s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp |
599 apply(erule PMatch.cases) |
596 next |
600 apply(simp_all)[7] |
597 case ONE |
601 (* CHAR case *) |
598 have "s \<in> der c ONE \<rightarrow> v" by fact |
602 apply(case_tac "c = x") |
599 then have "s \<in> ZERO \<rightarrow> v" by simp |
603 apply(simp) |
600 then have "False" by cases |
604 apply(erule PMatch.cases) |
601 then show "(c#s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp |
605 apply(simp_all)[7] |
602 next |
606 apply (metis PMatch.intros(2)) |
603 case (CHAR d) |
607 apply(simp) |
604 consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast |
608 apply(erule PMatch.cases) |
605 then show "(c#s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)" |
609 apply(simp_all)[7] |
606 proof (cases) |
610 (* ALT case *) |
607 case eq |
611 prefer 2 |
608 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
612 apply(erule PMatch.cases) |
609 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
613 apply(simp_all)[7] |
610 then have eqs: "s = [] \<and> v = Void" by cases simp |
614 apply (metis PMatch.intros(3)) |
611 show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs by (auto intro: PMatch.intros) |
615 apply(clarify) |
612 next |
616 apply(rule PMatch.intros) |
613 case ineq |
617 apply metis |
614 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
618 apply(simp add: der_correctness Der_def) |
615 then have "s \<in> ZERO \<rightarrow> v" using ineq by simp |
619 (* SEQ case *) |
616 then have "False" by cases |
620 apply(case_tac "nullable x1") |
617 then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp |
621 apply(simp) |
618 qed |
622 prefer 2 |
619 next |
623 (* not-nullbale case *) |
620 case (ALT r1 r2) |
624 apply(simp) |
621 have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
625 apply(erule PMatch.cases) |
622 have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
626 apply(simp_all)[7] |
623 have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact |
627 apply(clarify) |
624 then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp |
628 apply(subst append.simps(2)[symmetric]) |
625 then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'" |
629 apply(rule PMatch.intros) |
626 | (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'" |
630 apply metis |
627 by cases auto |
631 apply metis |
628 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" |
632 apply(auto)[1] |
629 proof (cases) |
633 apply(simp add: der_correctness Der_def) |
630 case left |
634 apply(auto)[1] |
631 have "s \<in> der c r1 \<rightarrow> v'" by fact |
635 (* nullable case *) |
632 then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp |
636 apply(erule PMatch.cases) |
633 then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: PMatch.intros) |
637 apply(simp_all)[7] |
634 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp |
638 (* left case *) |
635 next |
639 apply(clarify) |
636 case right |
640 apply(erule PMatch.cases) |
637 have "s \<notin> L (der c r1)" by fact |
641 apply(simp_all)[4] |
638 then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def) |
642 prefer 2 |
639 moreover |
643 apply(clarify) |
640 have "s \<in> der c r2 \<rightarrow> v'" by fact |
644 prefer 2 |
641 then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp |
645 apply(clarify) |
642 ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')" |
646 apply(clarify) |
643 by (auto intro: PMatch.intros) |
647 apply(simp (no_asm)) |
644 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp |
648 apply(subst append.simps(2)[symmetric]) |
645 qed |
649 apply(rule PMatch.intros) |
646 next |
650 apply metis |
647 case (SEQ r1 r2) |
651 apply metis |
648 have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
652 apply(erule contrapos_nn) |
649 have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
653 apply(erule exE)+ |
650 have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact |
654 apply(auto)[1] |
651 then consider |
655 apply(simp add: der_correctness Der_def) |
652 (left_nullable) v1 v2 s1 s2 where |
656 apply metis |
653 "v = Left (Seq v1 v2)" "s = s1 @ s2" |
657 (* right interesting case *) |
654 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" |
658 apply(clarify) |
655 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" |
659 apply(subst append.simps(1)[symmetric]) |
656 | (right_nullable) v1 s1 s2 where |
660 apply(rule PMatch.intros) |
657 "v = Right v1" "s = s1 @ s2" |
661 apply (metis PMatch_mkeps) |
658 "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" |
662 apply metis |
659 | (not_nullable) v1 v2 s1 s2 where |
663 apply(rule notI) |
660 "v = Seq v1 v2" "s = s1 @ s2" |
664 apply(clarify) |
661 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" |
665 apply(simp) |
662 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" |
666 apply(simp add: der_correctness) |
663 apply(auto split: if_splits simp add: Sequ_def) apply(erule PMatch.cases) |
667 apply(simp only: Der_def Sequ_def) |
664 apply(auto elim: PMatch.cases simp add: Sequ_def der_correctness Der_def) |
668 apply(simp) |
665 by fastforce |
669 apply (metis Cons_eq_append_conv) |
666 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" |
670 (* Stars case *) |
667 proof (cases) |
671 apply(erule PMatch.cases) |
668 case left_nullable |
672 apply(simp_all)[7] |
669 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
673 apply(clarify) |
670 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
674 apply(rotate_tac 2) |
671 moreover |
675 apply(frule_tac PMatch1) |
672 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact |
676 apply(erule PMatch.cases) |
673 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def) |
677 apply(simp_all)[7] |
674 ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac PMatch.intros) |
678 apply(subst append.simps(2)[symmetric]) |
675 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp |
679 apply(rule PMatch.intros) |
676 next |
680 apply metis |
677 case right_nullable |
681 apply(auto)[1] |
678 have "nullable r1" by fact |
682 apply(rule PMatch.intros) |
679 then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule PMatch_mkeps) |
683 apply(simp) |
680 moreover |
684 apply(simp) |
681 have "s \<in> der c r2 \<rightarrow> v1" by fact |
685 apply(simp) |
682 then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp |
686 apply (metis L.simps(6)) |
683 moreover |
687 apply(subst Prf_injval_flat) |
684 have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact |
688 apply (metis PMatch1) |
685 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable |
689 apply(simp) |
686 by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def) |
690 apply(auto)[1] |
687 ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)" |
691 apply(drule_tac x="s\<^sub>3" in spec) |
688 by(rule PMatch.intros) |
692 apply(drule mp) |
689 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp |
693 defer |
690 next |
694 apply metis |
691 case not_nullable |
695 apply(clarify) |
692 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
696 apply(drule_tac x="s1" in meta_spec) |
693 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
697 apply(drule_tac x="v1" in meta_spec) |
694 moreover |
698 apply(drule_tac x="c" in meta_spec) |
695 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact |
699 apply(simp) |
696 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def) |
700 apply(rotate_tac 2) |
697 ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable |
701 apply(drule PMatch.intros(6)) |
698 by (rule_tac PMatch.intros) (simp_all) |
702 apply(rule PMatch.intros(7)) |
699 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp |
703 (* HERE *) |
700 qed |
704 apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat) |
701 next |
705 apply (metis Nil_is_append_conv) |
702 case (STAR r) |
706 apply(simp) |
703 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
707 apply(subst der_correctness) |
704 have "s \<in> der c (STAR r) \<rightarrow> v" by fact |
708 apply(simp add: Der_def) |
705 then consider |
709 done |
706 (cons) v1 vs s1 s2 where |
|
707 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
708 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
|
709 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" |
|
710 apply(erule_tac PMatch.cases) |
|
711 apply(auto) |
|
712 apply(rotate_tac 4) |
|
713 apply(erule_tac PMatch.cases) |
|
714 apply(auto) |
|
715 apply (simp add: PMatch.intros(6)) |
|
716 using PMatch.intros(7) by blast |
|
717 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
|
718 proof (cases) |
|
719 case cons |
|
720 have "s1 \<in> der c r \<rightarrow> v1" by fact |
|
721 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
722 moreover |
|
723 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact |
|
724 moreover |
|
725 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
|
726 then have "flat (injval r c v1) = (c # s1)" by (rule PMatch1) |
|
727 then have "flat (injval r c v1) \<noteq> []" by simp |
|
728 moreover |
|
729 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
|
730 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
|
731 by (simp add: der_correctness Der_def) |
|
732 ultimately |
|
733 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros) |
|
734 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
|
735 qed |
|
736 qed |
710 |
737 |
711 lemma lex_correct1: |
738 lemma lex_correct1: |
712 assumes "s \<notin> L r" |
739 assumes "s \<notin> L r" |
713 shows "matcher r s = None" |
740 shows "matcher r s = None" |
714 using assms |
741 using assms |