668 apply (metis mkeps_flat) |
696 apply (metis mkeps_flat) |
669 apply(simp) |
697 apply(simp) |
670 apply(erule Prf.cases) |
698 apply(erule Prf.cases) |
671 apply(simp_all)[5] |
699 apply(simp_all)[5] |
672 done |
700 done |
|
701 |
|
702 lemma v4_proj: |
|
703 assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s" |
|
704 shows "c # flat (projval r c v) = flat v" |
|
705 using assms |
|
706 apply(induct rule: Prf.induct) |
|
707 prefer 4 |
|
708 apply(simp) |
|
709 prefer 4 |
|
710 apply(simp) |
|
711 prefer 2 |
|
712 apply(simp) |
|
713 prefer 2 |
|
714 apply(simp) |
|
715 apply(auto) |
|
716 by (metis Cons_eq_append_conv) |
|
717 |
|
718 lemma v4_proj2: |
|
719 assumes "\<turnstile> v : r" and "(flat v) = c # s" |
|
720 shows "flat (projval r c v) = s" |
|
721 using assms |
|
722 by (metis list.inject v4_proj) |
|
723 |
|
724 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
|
725 by (metis list.sel(3)) |
|
726 |
|
727 lemma Prf_proj: |
|
728 assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<exists>s. (flat v1) = c # s" "\<exists>s. (flat v2) = c # s" |
|
729 shows "(projval r c v1) \<succ>(der c r) (projval r c v2)" |
|
730 using assms |
|
731 apply(induct arbitrary: v1 v2 rule: der.induct) |
|
732 apply(simp) |
|
733 apply(erule ValOrd.cases) |
|
734 apply(simp_all)[8] |
|
735 apply(erule ValOrd.cases) |
|
736 apply(simp_all)[8] |
|
737 apply(case_tac "c = c'") |
|
738 apply(simp) |
|
739 apply (metis ValOrd.intros(7)) |
|
740 apply(erule ValOrd.cases) |
|
741 apply(simp_all)[8] |
|
742 apply(simp) |
|
743 apply(erule ValOrd.cases) |
|
744 apply(simp_all)[8] |
|
745 apply(erule Prf.cases) |
|
746 apply(simp_all)[5] |
|
747 apply(erule Prf.cases) |
|
748 apply(simp_all)[5] |
|
749 apply(clarify) |
|
750 apply(rule ValOrd.intros) |
|
751 apply(subst v4_proj2) |
|
752 apply(simp) |
|
753 apply(simp) |
|
754 apply(subst v4_proj2) |
|
755 apply(simp) |
|
756 apply(simp) |
|
757 apply(simp) |
|
758 apply(clarify) |
|
759 apply(erule Prf.cases) |
|
760 apply(simp_all)[5] |
|
761 apply(erule Prf.cases) |
|
762 apply(simp_all)[5] |
|
763 apply(clarify) |
|
764 apply(rule ValOrd.intros) |
|
765 apply(subst v4_proj2) |
|
766 apply(simp) |
|
767 apply(simp) |
|
768 apply(subst v4_proj2) |
|
769 apply(simp) |
|
770 apply(simp) |
|
771 apply(simp) |
|
772 apply(clarify) |
|
773 apply(erule Prf.cases) |
|
774 apply(simp_all)[5] |
|
775 apply(erule Prf.cases) |
|
776 apply(simp_all)[5] |
|
777 apply(clarify) |
|
778 apply(rule ValOrd.intros) |
|
779 apply metis |
|
780 apply(clarify) |
|
781 apply(erule Prf.cases) |
|
782 apply(simp_all)[5] |
|
783 apply(erule Prf.cases) |
|
784 apply(simp_all)[5] |
|
785 apply(clarify) |
|
786 apply(rule ValOrd.intros) |
|
787 apply metis |
|
788 apply(clarify) |
|
789 apply(simp) |
|
790 apply(auto) |
|
791 defer |
|
792 apply(erule ValOrd.cases) |
|
793 apply(simp_all)[8] |
|
794 apply(auto)[1] |
|
795 apply(erule Prf.cases) |
|
796 apply(simp_all)[5] |
|
797 apply(erule Prf.cases) |
|
798 apply(simp_all)[5] |
|
799 apply(clarify) |
|
800 apply(simp) |
|
801 apply (metis Prf_flat_L nullable_correctness) |
|
802 apply(erule Prf.cases) |
|
803 apply(simp_all)[5] |
|
804 apply(erule Prf.cases) |
|
805 apply(simp_all)[5] |
|
806 apply(clarify) |
|
807 apply(rule ValOrd.intros) |
|
808 apply(simp) |
|
809 apply(simp) |
|
810 apply(auto)[1] |
|
811 apply(erule Prf.cases) |
|
812 apply(simp_all)[5] |
|
813 apply(erule Prf.cases) |
|
814 apply(simp_all)[5] |
|
815 apply(clarify) |
|
816 apply (metis Prf_flat_L nullable_correctness) |
|
817 apply(erule Prf.cases) |
|
818 apply(simp_all)[5] |
|
819 apply(erule Prf.cases) |
|
820 apply(simp_all)[5] |
|
821 apply(clarify) |
|
822 apply (metis Prf_flat_L nullable_correctness) |
|
823 apply(erule Prf.cases) |
|
824 apply(simp_all)[5] |
|
825 apply(erule Prf.cases) |
|
826 apply(simp_all)[5] |
|
827 apply(clarify) |
|
828 apply (metis Prf_flat_L nullable_correctness) |
|
829 apply(erule Prf.cases) |
|
830 apply(simp_all)[5] |
|
831 apply(erule Prf.cases) |
|
832 apply(simp_all)[5] |
|
833 apply(clarify) |
|
834 apply(rule ValOrd.intros(2)) |
|
835 apply (metis append_Cons list.inject neq_Nil_conv) |
|
836 apply(erule Prf.cases) |
|
837 apply(simp_all)[5] |
|
838 apply(erule Prf.cases) |
|
839 apply(simp_all)[5] |
|
840 apply(clarify) |
|
841 apply(auto) |
|
842 apply(erule ValOrd.cases) |
|
843 apply(simp_all)[8] |
|
844 apply(auto)[1] |
|
845 apply(rule ValOrd.intros) |
|
846 apply metis |
|
847 apply(clarify) |
|
848 apply(rule ValOrd.intros) |
|
849 |
|
850 apply(rule ValOrd.intros) |
|
851 apply(simp) |
|
852 apply(simp) |
|
853 apply(auto)[1] |
|
854 apply(erule Prf.cases) |
|
855 apply(simp_all)[5] |
|
856 apply(erule Prf.cases) |
|
857 apply(simp_all)[5] |
|
858 apply(clarify) |
|
859 apply(rule ValOrd.intros) |
|
860 defer |
|
861 apply(erule Prf.cases) |
|
862 apply(simp_all)[5] |
|
863 apply(erule Prf.cases) |
|
864 apply(simp_all)[5] |
|
865 apply(clarify) |
|
866 apply(simp add: append_eq_Cons_conv) |
|
867 apply(clarify) |
|
868 apply(rule ValOrd.intros) |
|
869 apply(simp) |
|
870 apply(subst v4_proj2) |
|
871 apply(simp) |
|
872 apply(simp) |
|
873 apply(subst v4_proj2) |
|
874 apply(simp) |
|
875 apply(simp) |
|
876 |
|
877 apply(simp) |
|
878 |
|
879 apply (metis Prf_flat_L nullable_correctness) |
|
880 |
|
881 |
|
882 |
|
883 |
|
884 apply(rule ValOrd.intros(2)) |
|
885 apply(erule Prf.cases) |
|
886 apply(simp_all)[5] |
|
887 apply(erule Prf.cases) |
|
888 apply(simp_all)[5] |
|
889 apply(simp) |
|
890 apply(erule ValOrd.cases) |
|
891 apply(simp_all)[8] |
|
892 apply(clarify) |
|
893 apply(erule Prf.cases) |
|
894 apply(simp_all)[5] |
|
895 apply(erule Prf.cases) |
|
896 apply(simp_all)[5] |
|
897 apply(clarify) |
|
898 apply(erule Prf.cases) |
|
899 apply(simp_all)[5] |
|
900 apply(clarify) |
|
901 apply(simp) |
|
902 |
|
903 lemma Prf_inj: |
|
904 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" |
|
905 shows "(injval r c v1) \<succ>r (injval r c v2)" |
|
906 using assms |
|
907 apply(induct arbitrary: v1 v2 rule: der.induct) |
|
908 apply(simp) |
|
909 apply(erule ValOrd.cases) |
|
910 apply(simp_all)[8] |
|
911 apply(erule ValOrd.cases) |
|
912 apply(simp_all)[8] |
|
913 apply(case_tac "c = c'") |
|
914 apply(simp) |
|
915 apply(erule ValOrd.cases) |
|
916 apply(simp_all)[8] |
|
917 apply(rule ValOrd.intros) |
|
918 apply(simp) |
|
919 apply(erule ValOrd.cases) |
|
920 apply(simp_all)[8] |
|
921 apply(simp) |
|
922 apply(erule ValOrd.cases) |
|
923 apply(simp_all)[8] |
|
924 apply(rule ValOrd.intros) |
|
925 apply(subst v4) |
|
926 apply(clarify) |
|
927 apply(rotate_tac 3) |
|
928 apply(erule Prf.cases) |
|
929 apply(simp_all)[5] |
|
930 apply(subst v4) |
|
931 apply(clarify) |
|
932 apply(rotate_tac 2) |
|
933 apply(erule Prf.cases) |
|
934 apply(simp_all)[5] |
|
935 apply(simp) |
|
936 apply(rule ValOrd.intros) |
|
937 apply(subst v4) |
|
938 apply(clarify) |
|
939 apply(rotate_tac 3) |
|
940 apply(erule Prf.cases) |
|
941 apply(simp_all)[5] |
|
942 apply(subst v4) |
|
943 apply(clarify) |
|
944 apply(erule Prf.cases) |
|
945 apply(simp_all)[5] |
|
946 apply(simp) |
|
947 apply(rule ValOrd.intros) |
|
948 apply(clarify) |
|
949 apply(erule Prf.cases) |
|
950 apply(simp_all)[5] |
|
951 apply(erule Prf.cases) |
|
952 apply(simp_all)[5] |
|
953 apply(rule ValOrd.intros) |
|
954 apply(clarify) |
|
955 apply(erule Prf.cases) |
|
956 apply(simp_all)[5] |
|
957 apply(erule Prf.cases) |
|
958 apply(simp_all)[5] |
|
959 apply(simp) |
|
960 apply(case_tac "nullable r1") |
|
961 defer |
|
962 apply(simp) |
|
963 apply(erule ValOrd.cases) |
|
964 apply(simp_all)[8] |
|
965 apply(clarify) |
|
966 apply(erule Prf.cases) |
|
967 apply(simp_all)[5] |
|
968 apply(erule Prf.cases) |
|
969 apply(simp_all)[5] |
|
970 apply(clarify) |
|
971 apply(rule ValOrd.intros) |
|
972 apply(simp) |
|
973 apply(simp) |
|
974 apply(rule ValOrd.intros(2)) |
|
975 apply(erule Prf.cases) |
|
976 apply(simp_all)[5] |
|
977 apply(erule Prf.cases) |
|
978 apply(simp_all)[5] |
|
979 apply(simp) |
|
980 apply(erule ValOrd.cases) |
|
981 apply(simp_all)[8] |
|
982 apply(clarify) |
|
983 apply(erule Prf.cases) |
|
984 apply(simp_all)[5] |
|
985 apply(erule Prf.cases) |
|
986 apply(simp_all)[5] |
|
987 apply(clarify) |
|
988 apply(erule Prf.cases) |
|
989 apply(simp_all)[5] |
|
990 apply(clarify) |
|
991 apply(simp) |
|
992 apply(case_tac "injval r1 c v1 = mkeps r1") |
|
993 apply(rule ValOrd.intros(1)) |
|
994 apply(simp) |
|
995 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4) |
|
996 apply(rule ValOrd.intros(2)) |
|
997 |
|
998 apply(rotate_tac 1) |
|
999 apply(drule meta_mp) |
|
1000 apply(rule |
|
1001 |
|
1002 lemma POSIX_der: |
|
1003 assumes "POSIX v (der c r)" "\<turnstile> v : der c r" |
|
1004 shows "POSIX (injval r c v) r" |
|
1005 using assms |
|
1006 unfolding POSIX_def |
|
1007 apply(auto) |
|
1008 apply(subst (asm) v4) |
|
1009 apply(assumption) |
|
1010 apply(drule_tac x="projval r c v'" in spec) |
|
1011 apply(drule mp) |
|
1012 apply(auto) |
|
1013 apply(rule v3_proj) |
|
1014 apply(simp) |
|
1015 apply(rule_tac x="flat v" in exI) |
|
1016 apply(simp) |
|
1017 apply(rule_tac c="c" in t) |
|
1018 apply(simp) |
|
1019 apply(subst v4_proj) |
|
1020 apply(simp) |
|
1021 apply(rule_tac x="flat v" in exI) |
|
1022 apply(simp) |
|
1023 apply(simp) |
|
1024 apply(simp add: Cons_eq_append_conv) |
|
1025 apply(auto)[1] |
673 |
1026 |
674 text {* |
1027 text {* |
675 Injection followed by projection is the identity. |
1028 Injection followed by projection is the identity. |
676 *} |
1029 *} |
677 |
1030 |
815 lemma v5: |
1168 lemma v5: |
816 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
1169 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
817 shows "POSIX (injval r c v) r" |
1170 shows "POSIX (injval r c v) r" |
818 using assms |
1171 using assms |
819 apply(induct arbitrary: v rule: der.induct) |
1172 apply(induct arbitrary: v rule: der.induct) |
820 apply(simp) |
1173 (* NULL case *) |
821 apply(erule Prf.cases) |
1174 apply(simp) |
822 apply(simp_all)[5] |
1175 apply(erule Prf.cases) |
823 apply(simp) |
1176 apply(simp_all)[5] |
824 apply(erule Prf.cases) |
1177 (* EMPTY case *) |
825 apply(simp_all)[5] |
1178 apply(simp) |
|
1179 apply(erule Prf.cases) |
|
1180 apply(simp_all)[5] |
|
1181 (* CHAR case *) |
826 apply(simp) |
1182 apply(simp) |
827 apply(case_tac "c = c'") |
1183 apply(case_tac "c = c'") |
828 apply(auto simp add: POSIX_def)[1] |
1184 apply(auto simp add: POSIX_def)[1] |
829 apply(erule Prf.cases) |
1185 apply(erule Prf.cases) |
830 apply(simp_all)[5] |
1186 apply(simp_all)[5] |
831 apply(erule Prf.cases) |
1187 apply(erule Prf.cases) |
832 apply(simp_all)[5] |
1188 apply(simp_all)[5] |
833 using ValOrd.simps apply blast |
1189 apply(rule ValOrd.intros) |
834 apply(auto) |
1190 apply(auto)[1] |
835 apply(erule Prf.cases) |
1191 apply(erule Prf.cases) |
836 apply(simp_all)[5] |
1192 apply(simp_all)[5] |
837 (* base cases done *) |
1193 (* base cases done *) |
838 (* ALT case *) |
1194 (* ALT case *) |
839 apply(erule Prf.cases) |
1195 apply(erule Prf.cases) |
840 apply(simp_all)[5] |
1196 apply(simp_all)[5] |
841 using POSIX_ALT POSIX_ALT_I1 apply blast |
1197 using POSIX_ALT POSIX_ALT_I1 apply blast |
842 apply(clarify) |
1198 apply(clarify) |
|
1199 apply(simp) |
|
1200 apply(rule POSIX_ALT_I2) |
|
1201 apply(drule POSIX_ALT1a) |
|
1202 apply metis |
|
1203 apply(auto)[1] |
|
1204 apply(subst v4) |
|
1205 apply(assumption) |
|
1206 apply(simp) |
|
1207 apply(drule POSIX_ALT1a) |
|
1208 apply(rotate_tac 1) |
|
1209 apply(drule_tac x="v2" in meta_spec) |
|
1210 apply(simp) |
|
1211 |
|
1212 apply(rotate_tac 4) |
|
1213 apply(erule Prf.cases) |
|
1214 apply(simp_all)[5] |
|
1215 apply(rule ValOrd.intros) |
|
1216 apply(simp) |
|
1217 apply(subst (asm) v4) |
|
1218 apply(assumption) |
|
1219 apply(clarify) |
|
1220 thm POSIX_ALT1a POSIX_ALT1b POSIX_ALT_I2 |
|
1221 apply(subst (asm) v4) |
|
1222 apply(auto simp add: POSIX_def)[1] |
843 apply(subgoal_tac "POSIX v2 (der c r2)") |
1223 apply(subgoal_tac "POSIX v2 (der c r2)") |
844 prefer 2 |
1224 prefer 2 |
845 apply(auto simp add: POSIX_def)[1] |
1225 apply(auto simp add: POSIX_def)[1] |
846 apply (metis POSIX_ALT1a POSIX_def flat.simps(4)) |
1226 apply (metis POSIX_ALT1a POSIX_def flat.simps(4)) |
847 apply(frule POSIX_ALT1a) |
1227 apply(frule POSIX_ALT1a) |