722 by (metis list.inject v4_proj) |
722 by (metis list.inject v4_proj) |
723 |
723 |
724 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
724 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
725 by (metis list.sel(3)) |
725 by (metis list.sel(3)) |
726 |
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: |
727 lemma Prf_inj: |
904 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" |
728 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)" |
729 shows "(injval r c v1) \<succ>r (injval r c v2)" |
906 using assms |
730 using assms |
907 apply(induct arbitrary: v1 v2 rule: der.induct) |
731 apply(induct arbitrary: v1 v2 rule: der.induct) |
|
732 (* NULL case *) |
908 apply(simp) |
733 apply(simp) |
909 apply(erule ValOrd.cases) |
734 apply(erule ValOrd.cases) |
910 apply(simp_all)[8] |
735 apply(simp_all)[8] |
|
736 (* EMPTY case *) |
911 apply(erule ValOrd.cases) |
737 apply(erule ValOrd.cases) |
912 apply(simp_all)[8] |
738 apply(simp_all)[8] |
|
739 (* CHAR case *) |
913 apply(case_tac "c = c'") |
740 apply(case_tac "c = c'") |
914 apply(simp) |
741 apply(simp) |
915 apply(erule ValOrd.cases) |
742 apply(erule ValOrd.cases) |
916 apply(simp_all)[8] |
743 apply(simp_all)[8] |
917 apply(rule ValOrd.intros) |
744 apply(rule ValOrd.intros) |
918 apply(simp) |
745 apply(simp) |
919 apply(erule ValOrd.cases) |
746 apply(erule ValOrd.cases) |
920 apply(simp_all)[8] |
747 apply(simp_all)[8] |
|
748 (* ALT case *) |
921 apply(simp) |
749 apply(simp) |
922 apply(erule ValOrd.cases) |
750 apply(erule ValOrd.cases) |
923 apply(simp_all)[8] |
751 apply(simp_all)[8] |
924 apply(rule ValOrd.intros) |
752 apply(rule ValOrd.intros) |
925 apply(subst v4) |
753 apply(subst v4) |
992 apply(case_tac "injval r1 c v1 = mkeps r1") |
823 apply(case_tac "injval r1 c v1 = mkeps r1") |
993 apply(rule ValOrd.intros(1)) |
824 apply(rule ValOrd.intros(1)) |
994 apply(simp) |
825 apply(simp) |
995 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4) |
826 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4) |
996 apply(rule ValOrd.intros(2)) |
827 apply(rule ValOrd.intros(2)) |
997 |
828 apply(drule_tac x="proj r1 c" in spec) |
998 apply(rotate_tac 1) |
829 oops |
999 apply(drule meta_mp) |
|
1000 apply(rule |
|
1001 |
830 |
1002 lemma POSIX_der: |
831 lemma POSIX_der: |
1003 assumes "POSIX v (der c r)" "\<turnstile> v : der c r" |
832 assumes "POSIX v (der c r)" "\<turnstile> v : der c r" |
1004 shows "POSIX (injval r c v) r" |
833 shows "POSIX (injval r c v) r" |
1005 using assms |
834 using assms |
1006 unfolding POSIX_def |
835 unfolding POSIX_def |
1007 apply(auto) |
836 apply(auto) |
|
837 thm v4 |
1008 apply(subst (asm) v4) |
838 apply(subst (asm) v4) |
1009 apply(assumption) |
839 apply(assumption) |
1010 apply(drule_tac x="projval r c v'" in spec) |
840 apply(drule_tac x="projval r c v'" in spec) |
1011 apply(drule mp) |
|
1012 apply(auto) |
841 apply(auto) |
1013 apply(rule v3_proj) |
842 apply(rule v3_proj) |
1014 apply(simp) |
843 apply(simp) |
1015 apply(rule_tac x="flat v" in exI) |
844 apply(rule_tac x="flat v" in exI) |
1016 apply(simp) |
845 apply(simp) |