432 "lex r [] = (if nullable r then Some(mkeps r) else None)" |
432 "lex r [] = (if nullable r then Some(mkeps r) else None)" |
433 | "lex r (c#s) = (case (lex (der c r) s) of |
433 | "lex r (c#s) = (case (lex (der c r) s) of |
434 None \<Rightarrow> None |
434 None \<Rightarrow> None |
435 | Some(v) \<Rightarrow> Some(injval r c v))" |
435 | Some(v) \<Rightarrow> Some(injval r c v))" |
436 |
436 |
|
437 fun |
|
438 lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val" |
|
439 where |
|
440 "lex2 r [] = mkeps r" |
|
441 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)" |
|
442 |
437 |
443 |
438 section {* Projection function *} |
444 section {* Projection function *} |
439 |
445 |
440 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
446 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
441 where |
447 where |
612 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
618 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
613 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
619 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
614 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
620 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
615 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
621 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
616 |
622 |
|
623 |
617 lemma PMatch_mkeps: |
624 lemma PMatch_mkeps: |
618 assumes "nullable r" |
625 assumes "nullable r" |
619 shows "[] \<in> r \<rightarrow> mkeps r" |
626 shows "[] \<in> r \<rightarrow> mkeps r" |
620 using assms |
627 using assms |
621 apply(induct r) |
628 apply(induct r) |
646 apply (metis Prf.intros(2)) |
653 apply (metis Prf.intros(2)) |
647 apply (metis Prf.intros(3)) |
654 apply (metis Prf.intros(3)) |
648 apply (metis Prf.intros(1)) |
655 apply (metis Prf.intros(1)) |
649 done |
656 done |
650 |
657 |
651 lemma PMAtch2: |
658 lemma PMatch_Values: |
|
659 assumes "s \<in> r \<rightarrow> v" |
|
660 shows "v \<in> Values r s" |
|
661 using assms |
|
662 apply(simp add: Values_def PMatch1) |
|
663 by (metis append_Nil2 prefix_def) |
|
664 |
|
665 lemma PMatch2: |
652 assumes "s \<in> (der c r) \<rightarrow> v" |
666 assumes "s \<in> (der c r) \<rightarrow> v" |
653 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
667 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
654 using assms |
668 using assms |
655 apply(induct c r arbitrary: s v rule: der.induct) |
669 apply(induct c r arbitrary: s v rule: der.induct) |
656 apply(auto) |
670 apply(auto) |
747 apply (metis Prf.intros(1)) |
761 apply (metis Prf.intros(1)) |
748 apply(rule v3_proj) |
762 apply(rule v3_proj) |
749 apply(simp) |
763 apply(simp) |
750 by (metis Cons_eq_append_conv) |
764 by (metis Cons_eq_append_conv) |
751 |
765 |
752 lemma lex_correct: |
766 lemma lex_correct1: |
753 assumes "s \<in> L r" |
767 assumes "s \<notin> L r" |
754 shows "\<exists>v. lex r s = Some(v) \<and> flat v = s" |
768 shows "lex r s = None" |
755 using assms |
769 using assms |
756 apply(induct s arbitrary: r) |
770 apply(induct s arbitrary: r) |
757 apply(simp) |
771 apply(simp) |
758 apply (metis mkeps_flat nullable_correctness) |
772 apply (metis nullable_correctness) |
|
773 apply(auto) |
759 apply(drule_tac x="der a r" in meta_spec) |
774 apply(drule_tac x="der a r" in meta_spec) |
760 apply(drule meta_mp) |
775 apply(drule meta_mp) |
761 defer |
776 apply(auto) |
762 apply(auto)[1] |
777 apply(simp add: L_flat_Prf) |
763 oops |
778 by (metis v3 v4) |
|
779 |
|
780 |
|
781 lemma lex_correct2: |
|
782 assumes "s \<in> L r" |
|
783 shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
|
784 using assms |
|
785 apply(induct s arbitrary: r) |
|
786 apply(simp) |
|
787 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
|
788 apply(drule_tac x="der a r" in meta_spec) |
|
789 apply(drule meta_mp) |
|
790 apply(simp add: L_flat_Prf) |
|
791 apply(auto) |
|
792 apply (metis v3_proj v4_proj2) |
|
793 apply (metis v3) |
|
794 apply(rule v4) |
|
795 by metis |
|
796 |
|
797 lemma lex_correct3: |
|
798 assumes "s \<in> L r" |
|
799 shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v" |
|
800 using assms |
|
801 apply(induct s arbitrary: r) |
|
802 apply(simp) |
|
803 apply (metis PMatch_mkeps nullable_correctness) |
|
804 apply(drule_tac x="der a r" in meta_spec) |
|
805 apply(drule meta_mp) |
|
806 apply(simp add: L_flat_Prf) |
|
807 apply(auto) |
|
808 apply (metis v3_proj v4_proj2) |
|
809 apply(rule PMatch2) |
|
810 apply(simp) |
|
811 done |
|
812 |
|
813 lemma lex_correct4: |
|
814 assumes "s \<in> L r" |
|
815 shows "s \<in> r \<rightarrow> (lex2 r s)" |
|
816 using assms |
|
817 apply(induct s arbitrary: r) |
|
818 apply(simp) |
|
819 apply (metis PMatch_mkeps nullable_correctness) |
|
820 apply(simp) |
|
821 apply(rule PMatch2) |
|
822 apply(drule_tac x="der a r" in meta_spec) |
|
823 apply(drule meta_mp) |
|
824 apply(simp add: L_flat_Prf) |
|
825 apply(auto) |
|
826 apply (metis v3_proj v4_proj2) |
|
827 done |
764 |
828 |
765 section {* Sulzmann's Ordering of values *} |
829 section {* Sulzmann's Ordering of values *} |
|
830 |
|
831 thm PMatch.intros |
766 |
832 |
767 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
833 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
768 where |
834 where |
769 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
835 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
770 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
836 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |