1022 unfolding CPT_def by (auto elim: CPrf.cases) |
1022 unfolding CPT_def by (auto elim: CPrf.cases) |
1023 then show "Stars [] :\<sqsubseteq>val v2" |
1023 then show "Stars [] :\<sqsubseteq>val v2" |
1024 by (simp add: PosOrd_ex1_def) |
1024 by (simp add: PosOrd_ex1_def) |
1025 qed |
1025 qed |
1026 |
1026 |
|
1027 lemma Posix_PosOrd_stronger: |
|
1028 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
|
1029 shows "v1 :\<sqsubseteq>val v2" |
|
1030 proof - |
|
1031 from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s" |
|
1032 unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto |
|
1033 moreover |
|
1034 { assume "v2 \<in> CPT r s" |
|
1035 with assms(1) have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd) |
|
1036 } |
|
1037 moreover |
|
1038 { assume "flat v2 \<sqsubset>spre s" |
|
1039 then have "flat v2 \<sqsubset>spre flat v1" using assms(1) |
|
1040 using Posix1(2) by blast |
|
1041 then have "v1 :\<sqsubseteq>val v2" |
|
1042 by (simp add: PosOrd_ex1_def PosOrd_spreI) |
|
1043 } |
|
1044 ultimately show "v1 :\<sqsubseteq>val v2" by blast |
|
1045 qed |
|
1046 |
1027 lemma Posix_PosOrd_reverse: |
1047 lemma Posix_PosOrd_reverse: |
1028 assumes "s \<in> r \<rightarrow> v1" |
1048 assumes "s \<in> r \<rightarrow> v1" |
1029 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1049 shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)" |
1030 using assms |
1050 using assms |
1031 by (metis Posix_PosOrd less_irrefl PosOrd_def |
1051 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def |
1032 PosOrd_ex1_def PosOrd_ex_def PosOrd_trans) |
1052 PosOrd_ex1_def PosOrd_ex_def PosOrd_trans) |
1033 |
1053 |
1034 |
1054 |
1035 lemma PosOrd_Posix_Stars: |
1055 lemma PosOrd_Posix_Stars: |
1036 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
1056 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |