equal
deleted
inserted
replaced
601 "[] \<in> EMPTY \<rightarrow> Void" |
601 "[] \<in> EMPTY \<rightarrow> Void" |
602 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
602 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
603 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
603 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
604 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
604 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
605 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
605 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
606 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s2) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
606 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
607 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
607 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
608 |
608 |
609 lemma PMatch_mkeps: |
609 lemma PMatch_mkeps: |
610 assumes "nullable r" |
610 assumes "nullable r" |
611 shows " [] \<in> r \<rightarrow> mkeps r" |
611 shows " [] \<in> r \<rightarrow> mkeps r" |
636 apply (metis Prf.intros(4)) |
636 apply (metis Prf.intros(4)) |
637 apply (metis Prf.intros(5)) |
637 apply (metis Prf.intros(5)) |
638 apply (metis Prf.intros(2)) |
638 apply (metis Prf.intros(2)) |
639 apply (metis Prf.intros(3)) |
639 apply (metis Prf.intros(3)) |
640 apply (metis Prf.intros(1)) |
640 apply (metis Prf.intros(1)) |
641 by (metis Prf.intros(1)) |
641 done |
642 |
642 |
643 lemma PMAtch2: |
643 lemma PMAtch2: |
644 assumes "s \<in> (der c r) \<rightarrow> v" |
644 assumes "s \<in> (der c r) \<rightarrow> v" |
645 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
645 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
646 using assms |
646 using assms |
687 apply(auto)[1] |
687 apply(auto)[1] |
688 apply(simp add: L_flat_Prf) |
688 apply(simp add: L_flat_Prf) |
689 apply(auto)[1] |
689 apply(auto)[1] |
690 apply(frule_tac c="c" in v3_proj) |
690 apply(frule_tac c="c" in v3_proj) |
691 apply metis |
691 apply metis |
692 apply(drule_tac x="projval r1 c v" in spec) |
692 apply(drule_tac x="s3" in spec) |
693 apply(drule mp) |
693 apply(drule mp) |
|
694 apply(rule_tac x="projval r1 c v" in exI) |
|
695 apply(rule conjI) |
694 apply (metis v4_proj2) |
696 apply (metis v4_proj2) |
695 apply(simp) |
697 apply(simp) |
|
698 apply metis |
696 (* nullable case *) |
699 (* nullable case *) |
697 apply(erule PMatch.cases) |
700 apply(erule PMatch.cases) |
698 apply(simp_all)[5] |
701 apply(simp_all)[5] |
699 apply(clarify) |
702 apply(clarify) |
700 apply(erule PMatch.cases) |
703 apply(erule PMatch.cases) |
707 apply(auto)[1] |
710 apply(auto)[1] |
708 apply(simp add: L_flat_Prf) |
711 apply(simp add: L_flat_Prf) |
709 apply(auto)[1] |
712 apply(auto)[1] |
710 apply(frule_tac c="c" in v3_proj) |
713 apply(frule_tac c="c" in v3_proj) |
711 apply metis |
714 apply metis |
712 apply(drule_tac x="projval r1 c v" in spec) |
715 apply(drule_tac x="s3" in spec) |
713 apply(drule mp) |
716 apply(drule mp) |
714 apply (metis v4_proj2) |
717 apply (metis v4_proj2) |
715 apply(simp) |
718 apply(simp) |
716 (* interesting case *) |
719 (* interesting case *) |
717 apply(clarify) |
720 apply(clarify) |
726 apply metis |
729 apply metis |
727 apply(auto) |
730 apply(auto) |
728 apply(simp only: L_flat_Prf) |
731 apply(simp only: L_flat_Prf) |
729 apply(simp) |
732 apply(simp) |
730 apply(auto) |
733 apply(auto) |
731 apply(drule_tac x="projval r1 c v" in spec) |
734 apply(drule_tac x="Seq (projval r1 c v) vb" in spec) |
732 apply(drule mp) |
735 apply(drule mp) |
733 apply (metis v4_proj2) |
736 apply(simp) |
734 apply(rotate_tac 1) |
737 apply (metis append_Cons butlast_snoc last_snoc neq_Nil_conv rotate1.simps(2) v4_proj2) |
735 apply(drule_tac x="sa" in meta_spec) |
738 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1") |
736 apply(drule_tac x="va" in meta_spec) |
739 apply (metis Prf.intros(1)) |
737 apply(simp) |
|
738 apply(rotate_tac 2) |
|
739 apply(drule_tac x="sa" in meta_spec) |
|
740 apply(drule_tac x="projval r1 c v" in meta_spec) |
|
741 apply(drule meta_mp) |
|
742 apply(frule_tac c="c" in v3_proj) |
|
743 apply metis |
|
744 |
|
745 apply(frule PMatch1(1)) |
|
746 apply(drule PMatch1(2)) |
|
747 apply(clarify) |
|
748 apply(subst (asm) (2) not_def) |
|
749 apply(drule mp) |
|
750 thm v3_proj |
|
751 apply(rule v3_proj) |
740 apply(rule v3_proj) |
752 apply(rule conjI) |
741 apply(simp) |
753 apply (metis v4_proj2) |
742 by (metis Cons_eq_append_conv) |
754 apply (metis v3_proj) |
|
755 v3_proj |
|
756 |
|
757 |
|
758 |
743 |
759 |
744 |
760 |
745 |
761 section {* Sulzmann's Ordering of values *} |
746 section {* Sulzmann's Ordering of values *} |
762 |
747 |