314 apply(erule Prf.cases) |
314 apply(erule Prf.cases) |
315 apply(simp_all)[5] |
315 apply(simp_all)[5] |
316 apply(auto) |
316 apply(auto) |
317 apply(rule ValOrd.intros) |
317 apply(rule ValOrd.intros) |
318 apply metis |
318 apply metis |
|
319 done |
|
320 |
|
321 |
|
322 lemma |
|
323 "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk> |
|
324 \<Longrightarrow> POSIX (val.Right (mkeps r2)) (ALT r1 r2)" |
|
325 apply(auto simp add: POSIX_def) |
|
326 apply(rule Prf.intros(3)) |
|
327 apply(auto) |
|
328 apply(rotate_tac 3) |
|
329 apply(erule Prf.cases) |
|
330 apply(simp_all)[5] |
|
331 apply(simp add: mkeps_flat) |
|
332 apply(auto)[1] |
|
333 apply (metis Prf_flat_L nullable_correctness) |
|
334 apply(rule ValOrd.intros) |
|
335 apply(auto) |
319 done |
336 done |
320 |
337 |
321 lemma mkeps_POSIX: |
338 lemma mkeps_POSIX: |
322 assumes "nullable r" |
339 assumes "nullable r" |
323 shows "POSIX (mkeps r) r" |
340 shows "POSIX (mkeps r) r" |
717 defer |
734 defer |
718 apply(subst mkeps_flat) |
735 apply(subst mkeps_flat) |
719 oops |
736 oops |
720 *) |
737 *) |
721 |
738 |
|
739 |
|
740 lemma LeftRight: |
|
741 assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)" |
|
742 and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" |
|
743 shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))" |
|
744 using assms |
|
745 apply(simp) |
|
746 apply(erule ValOrd.cases) |
|
747 apply(simp_all)[8] |
|
748 apply(rule ValOrd.intros) |
|
749 apply(clarify) |
|
750 apply(subst v4) |
|
751 apply(simp) |
|
752 apply(subst v4) |
|
753 apply(simp) |
|
754 apply(simp) |
|
755 done |
|
756 |
|
757 lemma RightLeft: |
|
758 assumes "(Right v1) \<succ>(der c (ALT r1 r2)) (Left v2)" |
|
759 and "\<turnstile> v1 : der c r2" "\<turnstile> v2 : der c r1" |
|
760 shows "(injval (ALT r1 r2) c (Right v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Left v2))" |
|
761 using assms |
|
762 apply(simp) |
|
763 apply(erule ValOrd.cases) |
|
764 apply(simp_all)[8] |
|
765 apply(rule ValOrd.intros) |
|
766 apply(clarify) |
|
767 apply(subst v4) |
|
768 apply(simp) |
|
769 apply(subst v4) |
|
770 apply(simp) |
|
771 apply(simp) |
|
772 done |
|
773 |
|
774 lemma h: |
|
775 assumes "nullable r1" "\<turnstile> v1 : der c r1" |
|
776 shows "injval r1 c v1 \<succ>r1 mkeps r1" |
|
777 using assms |
|
778 apply(induct r1 arbitrary: v1 rule: der.induct) |
|
779 apply(simp) |
|
780 apply(simp) |
|
781 apply(erule Prf.cases) |
|
782 apply(simp_all)[5] |
|
783 apply(simp) |
|
784 apply(simp) |
|
785 apply(erule Prf.cases) |
|
786 apply(simp_all)[5] |
|
787 apply(clarify) |
|
788 apply(auto)[1] |
|
789 apply (metis ValOrd.intros(6)) |
|
790 apply (metis ValOrd.intros(6)) |
|
791 apply (metis ValOrd.intros(3) le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral) |
|
792 apply(auto)[1] |
|
793 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4) |
|
794 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4) |
|
795 apply (metis ValOrd.intros(5)) |
|
796 apply(simp) |
|
797 apply(erule Prf.cases) |
|
798 apply(simp_all)[5] |
|
799 apply(clarify) |
|
800 apply(erule Prf.cases) |
|
801 apply(simp_all)[5] |
|
802 apply(clarify) |
|
803 apply (metis ValOrd.intros(2) list.distinct(1) mkeps_flat v4) |
|
804 apply(clarify) |
|
805 by (metis ValOrd.intros(1)) |
|
806 |
|
807 lemma LeftRightSeq: |
|
808 assumes "(Left (Seq v1 v2)) \<succ>(der c (SEQ r1 r2)) (Right v3)" |
|
809 and "nullable r1" "\<turnstile> v1 : der c r1" |
|
810 shows "(injval (SEQ r1 r2) c (Seq v1 v2)) \<succ>(SEQ r1 r2) (injval (SEQ r1 r2) c (Right v2))" |
|
811 using assms |
|
812 apply(simp) |
|
813 apply(erule ValOrd.cases) |
|
814 apply(simp_all)[8] |
|
815 apply(clarify) |
|
816 apply(simp) |
|
817 apply(rule ValOrd.intros(2)) |
|
818 prefer 2 |
|
819 apply (metis list.distinct(1) mkeps_flat v4) |
|
820 by (metis h) |
|
821 |
722 lemma Prf_inj: |
822 lemma Prf_inj: |
723 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
823 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
724 shows "(injval r c v1) \<succ>r (injval r c v2)" |
824 shows "(injval r c v1) \<succ>r (injval r c v2)" |
725 using assms |
825 using assms |
726 apply(induct arbitrary: v1 v2 rule: der.induct) |
826 apply(induct arbitrary: v1 v2 rule: der.induct) |
830 apply metis |
930 apply metis |
831 using injval_inj |
931 using injval_inj |
832 apply(simp add: inj_on_def) |
932 apply(simp add: inj_on_def) |
833 apply metis |
933 apply metis |
834 apply(clarify) |
934 apply(clarify) |
|
935 apply(simp) |
835 apply(erule Prf.cases) |
936 apply(erule Prf.cases) |
836 apply(simp_all)[5] |
937 apply(simp_all)[5] |
837 apply(clarify) |
938 apply(clarify) |
838 apply(erule ValOrd.cases) |
939 apply(erule ValOrd.cases) |
839 apply(simp_all)[8] |
940 apply(simp_all)[8] |
840 apply(clarify) |
941 apply(clarify) |
841 apply(simp) |
942 apply(simp) |
842 apply(rule ValOrd.intros(2)) |
943 apply(rule ValOrd.intros(2)) |
|
944 apply (metis h) |
|
945 apply (metis list.distinct(1) mkeps_flat v4) |
|
946 apply(clarify) |
|
947 apply(erule Prf.cases) |
|
948 apply(simp_all)[5] |
|
949 apply(clarify) |
|
950 apply(rotate_tac 6) |
|
951 apply(erule Prf.cases) |
|
952 apply(simp_all)[5] |
|
953 apply(clarify) |
|
954 apply(erule ValOrd.cases) |
|
955 apply(simp_all)[8] |
|
956 apply(clarify) |
|
957 apply(simp) |
843 prefer 2 |
958 prefer 2 |
844 apply (metis list.distinct(1) mkeps_flat v4) |
959 apply(clarify) |
845 defer |
960 apply(erule ValOrd.cases) |
846 apply(clarify) |
961 apply(simp_all)[8] |
847 apply(erule Prf.cases) |
962 apply(clarify) |
848 apply(simp_all)[5] |
963 apply(rule ValOrd.intros(1)) |
849 apply(clarify) |
964 apply(metis) |
850 apply(rotate_tac 6) |
965 thm mkeps_flat v4 |
851 apply(erule Prf.cases) |
|
852 apply(simp_all)[5] |
|
853 apply(clarify) |
|
854 apply(erule ValOrd.cases) |
|
855 apply(simp_all)[8] |
|
856 apply(clarify) |
|
857 apply(simp) |
|
858 apply(rule ValOrd.intros(2)) |
|
859 prefer 2 |
|
860 apply (metis list.distinct(1) mkeps_flat v4) |
966 apply (metis list.distinct(1) mkeps_flat v4) |
861 defer |
967 defer |
862 apply(clarify) |
968 apply(clarify) |
863 apply(erule ValOrd.cases) |
969 apply(erule ValOrd.cases) |
864 apply(simp_all)[8] |
970 apply(simp_all)[8] |