866 apply(rule CPrf.intros) |
866 apply(rule CPrf.intros) |
867 done |
867 done |
868 |
868 |
869 section {* The Posix Value is smaller than any other Value *} |
869 section {* The Posix Value is smaller than any other Value *} |
870 |
870 |
|
871 |
871 lemma Posix_PosOrd: |
872 lemma Posix_PosOrd: |
872 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
873 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
873 shows "v1 :\<sqsubseteq>val v2" |
874 shows "v1 :\<sqsubseteq>val v2" |
874 using assms |
875 using assms |
875 proof (induct arbitrary: v2 rule: Posix.induct) |
876 proof (induct arbitrary: v2 rule: Posix.induct) |
876 case (Posix_ONE v) |
877 case (Posix_ONE v) |
877 have "v \<in> CPTpre ONE []" by fact |
878 have "v \<in> CPT ONE []" by fact |
|
879 then have "v = Void" |
|
880 by (simp add: CPT_simps) |
878 then show "Void :\<sqsubseteq>val v" |
881 then show "Void :\<sqsubseteq>val v" |
879 by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases) |
882 by (simp add: PosOrd_ex1_def) |
880 next |
883 next |
881 case (Posix_CHAR c v) |
884 case (Posix_CHAR c v) |
882 have "v \<in> CPTpre (CHAR c) [c]" by fact |
885 have "v \<in> CPT (CHAR c) [c]" by fact |
|
886 then have "v = Char c" |
|
887 by (simp add: CPT_simps) |
883 then show "Char c :\<sqsubseteq>val v" |
888 then show "Char c :\<sqsubseteq>val v" |
884 by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases) |
889 by (simp add: PosOrd_ex1_def) |
885 next |
890 next |
886 case (Posix_ALT1 s r1 v r2 v2) |
891 case (Posix_ALT1 s r1 v r2 v2) |
887 have as1: "s \<in> r1 \<rightarrow> v" by fact |
892 have as1: "s \<in> r1 \<rightarrow> v" by fact |
888 have IH: "\<And>v2. v2 \<in> CPTpre r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
893 have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
889 have "v2 \<in> CPTpre (ALT r1 r2) s" by fact |
894 have "v2 \<in> CPT (ALT r1 r2) s" by fact |
890 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s" |
895 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
891 by(auto simp add: CPTpre_def prefix_list_def) |
896 by(auto simp add: CPT_def prefix_list_def) |
892 then consider |
897 then consider |
893 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" |
898 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
894 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s" |
899 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
895 by (auto elim: CPrf.cases) |
900 by (auto elim: CPrf.cases) |
896 then show "Left v :\<sqsubseteq>val v2" |
901 then show "Left v :\<sqsubseteq>val v2" |
897 proof(cases) |
902 proof(cases) |
898 case (Left v3) |
903 case (Left v3) |
899 have "v3 \<in> CPTpre r1 s" using Left(2,3) |
904 have "v3 \<in> CPT r1 s" using Left(2,3) |
900 by (auto simp add: CPTpre_def prefix_list_def) |
905 by (auto simp add: CPT_def prefix_list_def) |
901 with IH have "v :\<sqsubseteq>val v3" by simp |
906 with IH have "v :\<sqsubseteq>val v3" by simp |
902 moreover |
907 moreover |
903 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3) |
908 have "flat v3 = flat v" using as1 Left(3) |
904 by (simp add: Posix1(2) sprefix_list_def) |
909 by (simp add: Posix1(2)) |
905 ultimately have "Left v :\<sqsubseteq>val Left v3" |
910 ultimately have "Left v :\<sqsubseteq>val Left v3" |
906 by (auto simp add: PosOrd_ex1_def PosOrd_LeftI PosOrd_spreI) |
911 by (auto simp add: PosOrd_ex1_def PosOrd_LeftI) |
907 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
912 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
908 next |
913 next |
909 case (Right v3) |
914 case (Right v3) |
910 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3) |
915 have "flat v3 = flat v" using as1 Right(3) |
911 by (simp add: Posix1(2) sprefix_list_def) |
916 by (simp add: Posix1(2)) |
912 then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 |
917 then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 |
913 by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right PosOrd_spreI) |
918 by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right) |
914 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
919 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
915 qed |
920 qed |
916 next |
921 next |
917 case (Posix_ALT2 s r2 v r1 v2) |
922 case (Posix_ALT2 s r2 v r1 v2) |
918 have as1: "s \<in> r2 \<rightarrow> v" by fact |
923 have as1: "s \<in> r2 \<rightarrow> v" by fact |
919 have as2: "s \<notin> L r1" by fact |
924 have as2: "s \<notin> L r1" by fact |
920 have IH: "\<And>v2. v2 \<in> CPTpre r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
925 have IH: "\<And>v2. v2 \<in> CPT r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
921 have "v2 \<in> CPTpre (ALT r1 r2) s" by fact |
926 have "v2 \<in> CPT (ALT r1 r2) s" by fact |
922 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s" |
927 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
923 by(auto simp add: CPTpre_def prefix_list_def) |
928 by(auto simp add: CPT_def prefix_list_def) |
924 then consider |
929 then consider |
925 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" |
930 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
926 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s" |
931 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
927 by (auto elim: CPrf.cases) |
932 by (auto elim: CPrf.cases) |
928 then show "Right v :\<sqsubseteq>val v2" |
933 then show "Right v :\<sqsubseteq>val v2" |
929 proof (cases) |
934 proof (cases) |
930 case (Right v3) |
935 case (Right v3) |
931 have "v3 \<in> CPTpre r2 s" using Right(2,3) |
936 have "v3 \<in> CPT r2 s" using Right(2,3) |
932 by (auto simp add: CPTpre_def prefix_list_def) |
937 by (auto simp add: CPT_def prefix_list_def) |
933 with IH have "v :\<sqsubseteq>val v3" by simp |
938 with IH have "v :\<sqsubseteq>val v3" by simp |
934 moreover |
939 moreover |
935 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3) |
940 have "flat v3 = flat v" using as1 Right(3) |
936 by (simp add: Posix1(2) sprefix_list_def) |
941 by (simp add: Posix1(2)) |
937 ultimately have "Right v :\<sqsubseteq>val Right v3" |
942 ultimately have "Right v :\<sqsubseteq>val Right v3" |
938 by (auto simp add: PosOrd_ex1_def PosOrd_RightI PosOrd_spreI) |
943 by (auto simp add: PosOrd_ex1_def PosOrd_RightI) |
939 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
944 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
940 next |
945 next |
941 case (Left v3) |
946 case (Left v3) |
942 have w: "v3 \<in> CPTpre r1 s" using Left(2,3) as2 |
947 have "v3 \<in> CPT r1 s" using Left(2,3) as2 |
943 by (auto simp add: CPTpre_def prefix_list_def) |
948 by (auto simp add: CPT_def prefix_list_def) |
944 have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3) |
949 then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3) |
945 by (simp add: Posix1(2) sprefix_list_def) |
950 by (simp add: Posix1(2) CPT_def) |
946 then have "flat v3 \<sqsubset>spre flat v \<or> \<Turnstile> v3 : r1" using w |
951 then have "False" using as1 as2 Left |
947 by(auto simp add: CPTpre_def) |
952 by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf) |
948 then have "flat v3 \<sqsubset>spre flat v" using as1 as2 Left |
953 then show "Right v :\<sqsubseteq>val v2" by simp |
949 by (auto simp add: prefix_list_def sprefix_list_def Posix1(2) L_flat_Prf1 Prf_CPrf) |
|
950 then have "Right v :\<sqsubseteq>val Left v3" |
|
951 by (simp add: PosOrd_ex1_def PosOrd_spreI) |
|
952 then show "Right v :\<sqsubseteq>val v2" unfolding Left . |
|
953 qed |
954 qed |
954 next |
955 next |
955 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
956 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
956 have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
957 have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
957 have IH1: "\<And>v3. v3 \<in> CPTpre r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
958 have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
958 have IH2: "\<And>v3. v3 \<in> CPTpre r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
959 have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
959 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
960 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
960 have "v3 \<in> CPTpre (SEQ r1 r2) (s1 @ s2)" by fact |
961 have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact |
961 then obtain v3a v3b where eqs: |
962 then obtain v3a v3b where eqs: |
962 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
963 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
963 "flat v3a @ flat v3b \<sqsubseteq>pre s1 @ s2" |
964 "flat v3a @ flat v3b = s1 @ s2" |
964 by (force simp add: prefix_list_def CPTpre_def elim: CPrf.cases) |
965 by (force simp add: prefix_list_def CPT_def elim: CPrf.cases) |
965 then have "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2 \<or> flat v3a @ flat v3b = s1 @ s2" |
966 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
966 by (simp add: sprefix_list_def) |
967 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
967 moreover |
968 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
968 { assume "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2" |
969 by (simp add: sprefix_list_def append_eq_conv_conj) |
969 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using as1 |
970 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
970 by (auto simp add: PosOrd_ex1_def PosOrd_spreI Posix1(2)) |
971 using PosOrd_spreI Posix1(2) as1(1) eqs by blast |
971 } |
972 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3) |
972 moreover |
973 by (auto simp add: CPT_def) |
973 { assume q1: "flat v3a @ flat v3b = s1 @ s2" |
974 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
974 then have "flat v3a \<sqsubseteq>pre s1" using eqs(2,3) cond |
975 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
975 unfolding prefix_list_def |
976 unfolding PosOrd_ex1_def |
976 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
977 by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) |
977 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using q1 |
978 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
978 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
979 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
|
980 using PosOrd_spreI Posix1(2) as1(1) q1 by blast |
|
981 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r1 s1 \<and> v3b \<in> CPTpre r2 s2)" using eqs(2,3) |
|
982 by (auto simp add: CPTpre_def) |
|
983 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
|
984 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using q1 q2 as1 |
|
985 unfolding PosOrd_ex1_def |
|
986 by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) |
|
987 } |
|
988 ultimately show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
|
989 next |
979 next |
990 case (Posix_STAR1 s1 r v s2 vs v3) |
980 case (Posix_STAR1 s1 r v s2 vs v3) |
991 have as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
981 have as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
992 have IH1: "\<And>v3. v3 \<in> CPTpre r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
982 have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
993 have IH2: "\<And>v3. v3 \<in> CPTpre (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
983 have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
994 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
984 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
995 have cond2: "flat v \<noteq> []" by fact |
985 have cond2: "flat v \<noteq> []" by fact |
996 have "v3 \<in> CPTpre (STAR r) (s1 @ s2)" by fact |
986 have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact |
997 then consider |
987 then consider |
998 (NonEmpty) v3a vs3 where |
988 (NonEmpty) v3a vs3 where |
999 "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
989 "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
1000 "flat v3a @ flat (Stars vs3) \<sqsubseteq>pre s1 @ s2" |
990 "flat (Stars (v3a # vs3)) = s1 @ s2" |
1001 | (Empty) "v3 = Stars []" |
991 | (Empty) "v3 = Stars []" |
1002 by (force simp add: CPTpre_def prefix_list_def elim: CPrf.cases) |
992 by (force simp add: CPT_def elim: CPrf.cases) |
1003 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
993 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
1004 proof (cases) |
994 proof (cases) |
1005 case (NonEmpty v3a vs3) |
995 case (NonEmpty v3a vs3) |
1006 then have "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2 \<or> flat (Stars (v3a # vs3)) = s1 @ s2" |
996 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
1007 by (simp add: sprefix_list_def) |
997 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
1008 moreover |
998 unfolding prefix_list_def |
1009 { assume "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2" |
999 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
1010 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using as1 |
1000 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
1011 by (metis PosOrd_ex1_def PosOrd_spreI Posix1(2) flat.simps(7)) |
1001 by (simp add: sprefix_list_def append_eq_conv_conj) |
1012 } |
1002 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
1013 moreover |
1003 using PosOrd_spreI Posix1(2) as1(1) NonEmpty(4) by blast |
1014 { assume q1: "flat (Stars (v3a # vs3)) = s1 @ s2" |
1004 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" |
1015 then have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) cond |
1005 using NonEmpty(2,3) by (auto simp add: CPT_def) |
1016 unfolding prefix_list_def |
1006 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
1017 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
1007 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
1018 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using q1 |
1008 unfolding PosOrd_ex1_def |
1019 by (simp add: sprefix_list_def append_eq_conv_conj) |
1009 by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5)) |
1020 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
1010 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
1021 using PosOrd_spreI Posix1(2) as1(1) q1 by blast |
|
1022 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r s1 \<and> Stars vs3 \<in> CPTpre (STAR r) s2)" |
|
1023 using NonEmpty(2,3) by (auto simp add: CPTpre_def) |
|
1024 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
1025 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using q1 q2 as1 |
|
1026 unfolding PosOrd_ex1_def |
|
1027 by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5)) |
|
1028 } |
|
1029 ultimately show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
1030 next |
1011 next |
1031 case Empty |
1012 case Empty |
1032 have "v3 = Stars []" by fact |
1013 have "v3 = Stars []" by fact |
1033 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
1014 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
1034 unfolding PosOrd_ex1_def using cond2 |
1015 unfolding PosOrd_ex1_def using cond2 |
1035 by (simp add: PosOrd_shorterI) |
1016 by (simp add: PosOrd_shorterI) |
1036 qed |
1017 qed |
1037 next |
1018 next |
1038 case (Posix_STAR2 r v2) |
1019 case (Posix_STAR2 r v2) |
1039 have "v2 \<in> CPTpre (STAR r) []" by fact |
1020 have "v2 \<in> CPT (STAR r) []" by fact |
1040 then have "v2 = Stars []" using CPTpre_subsets by auto |
1021 then have "v2 = Stars []" |
|
1022 unfolding CPT_def by (auto elim: CPrf.cases) |
1041 then show "Stars [] :\<sqsubseteq>val v2" |
1023 then show "Stars [] :\<sqsubseteq>val v2" |
1042 by (simp add: PosOrd_ex1_def) |
1024 by (simp add: PosOrd_ex1_def) |
1043 qed |
1025 qed |
1044 |
1026 |
1045 |
|
1046 lemma Posix_PosOrd_stronger: |
|
1047 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
|
1048 shows "v1 :\<sqsubseteq>val v2" |
|
1049 using assms Posix_PosOrd |
|
1050 using CPT_CPTpre_subset by blast |
|
1051 |
|
1052 |
|
1053 lemma Posix_PosOrd_reverse: |
1027 lemma Posix_PosOrd_reverse: |
1054 assumes "s \<in> r \<rightarrow> v1" |
1028 assumes "s \<in> r \<rightarrow> v1" |
1055 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1029 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1056 using assms |
1030 using assms |
1057 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def |
1031 by (metis Posix_PosOrd less_irrefl PosOrd_def |
1058 PosOrd_ex1_def PosOrd_ex_def PosOrd_trans) |
1032 PosOrd_ex1_def PosOrd_ex_def PosOrd_trans) |
1059 |
1033 |
1060 |
1034 |
1061 lemma PosOrd_Posix_Stars: |
1035 lemma PosOrd_Posix_Stars: |
1062 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
1036 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |