424 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')" |
424 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')" |
425 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
425 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
426 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
426 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
427 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
427 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
428 |
428 |
|
429 fun |
|
430 lex :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
431 where |
|
432 "lex r [] = (if nullable r then Some(mkeps r) else None)" |
|
433 | "lex r (c#s) = (case (lex (der c r) s) of |
|
434 None \<Rightarrow> None |
|
435 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
436 |
429 |
437 |
430 section {* Projection function *} |
438 section {* Projection function *} |
431 |
439 |
432 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
440 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
433 where |
441 where |
606 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
614 \<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)" |
615 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
608 |
616 |
609 lemma PMatch_mkeps: |
617 lemma PMatch_mkeps: |
610 assumes "nullable r" |
618 assumes "nullable r" |
611 shows " [] \<in> r \<rightarrow> mkeps r" |
619 shows "[] \<in> r \<rightarrow> mkeps r" |
612 using assms |
620 using assms |
613 apply(induct r) |
621 apply(induct r) |
614 apply(auto) |
622 apply(auto) |
615 apply (metis PMatch.intros(1)) |
623 apply (metis PMatch.intros(1)) |
616 apply(subst append.simps(1)[symmetric]) |
624 apply(subst append.simps(1)[symmetric]) |
739 apply (metis Prf.intros(1)) |
747 apply (metis Prf.intros(1)) |
740 apply(rule v3_proj) |
748 apply(rule v3_proj) |
741 apply(simp) |
749 apply(simp) |
742 by (metis Cons_eq_append_conv) |
750 by (metis Cons_eq_append_conv) |
743 |
751 |
744 |
752 lemma lex_correct: |
|
753 assumes "s \<in> L r" |
|
754 shows "\<exists>v. lex r s = Some(v) \<and> flat v = s" |
|
755 using assms |
|
756 apply(induct s arbitrary: r) |
|
757 apply(simp) |
|
758 apply (metis mkeps_flat nullable_correctness) |
|
759 apply(drule_tac x="der a r" in meta_spec) |
|
760 apply(drule meta_mp) |
|
761 defer |
|
762 apply(auto)[1] |
|
763 oops |
745 |
764 |
746 section {* Sulzmann's Ordering of values *} |
765 section {* Sulzmann's Ordering of values *} |
747 |
766 |
748 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
767 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
749 where |
768 where |
888 apply(simp_all)[8] |
907 apply(simp_all)[8] |
889 apply(erule ValOrd.cases) |
908 apply(erule ValOrd.cases) |
890 apply(simp_all)[8] |
909 apply(simp_all)[8] |
891 done |
910 done |
892 |
911 |
|
912 |
|
913 lemma ValOrd_PMatch: |
|
914 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s" |
|
915 shows "v1 \<succ>r v2" |
|
916 using assms |
|
917 apply(induct arbitrary: v2 rule: PMatch.induct) |
|
918 apply(erule Prf.cases) |
|
919 apply(simp_all)[5] |
|
920 apply (metis ValOrd.intros(7)) |
|
921 apply(erule Prf.cases) |
|
922 apply(simp_all)[5] |
|
923 apply (metis ValOrd.intros(8)) |
|
924 apply(erule Prf.cases) |
|
925 apply(simp_all)[5] |
|
926 apply(clarify) |
|
927 apply (metis ValOrd.intros(6)) |
|
928 apply(clarify) |
|
929 apply (metis PMatch1(2) ValOrd.intros(3) order_refl) |
|
930 apply(erule Prf.cases) |
|
931 apply(simp_all)[5] |
|
932 apply(clarify) |
|
933 apply (metis Prf_flat_L) |
|
934 apply (metis ValOrd.intros(5)) |
|
935 apply(erule Prf.cases) |
|
936 apply(simp_all)[5] |
|
937 apply(auto) |
|
938 apply(case_tac "v1 = v1a") |
|
939 apply(auto) |
|
940 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq) |
|
941 apply(rule ValOrd.intros(2)) |
|
942 apply(auto) |
|
943 thm L_flat_Prf |
|
944 apply(simp add: L_flat_Prf) |
|
945 thm append_eq_append_conv2 |
|
946 apply(simp add: append_eq_append_conv2) |
|
947 apply(auto) |
|
948 apply(drule_tac x="us" in spec) |
|
949 apply(drule mp) |
|
950 apply metis |
|
951 apply (metis append_Nil2) |
|
952 apply(case_tac "us = []") |
|
953 apply(auto) |
|
954 apply(drule_tac x="v1a" in meta_spec) |
|
955 apply(simp) |
|
956 |
893 lemma refl_on_ValOrd: |
957 lemma refl_on_ValOrd: |
894 "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}" |
958 "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}" |
895 unfolding refl_on_def |
959 unfolding refl_on_def |
896 apply(auto) |
960 apply(auto) |
897 apply(rule ValOrd_refl) |
961 apply(rule ValOrd_refl) |