equal
deleted
inserted
replaced
124 done |
124 done |
125 |
125 |
126 |
126 |
127 |
127 |
128 |
128 |
129 section {* POSIX Ordering of Values According to Okui & Suzuki *} |
129 section {* POSIX Ordering of Values According to Okui \& Suzuki *} |
130 |
130 |
131 |
131 |
132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
133 where |
133 where |
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
194 assumes "v1 :\<sqsubset>val v2" |
194 assumes "v1 :\<sqsubset>val v2" |
195 shows "\<not>(v2 :\<sqsubset>val v1)" |
195 shows "\<not>(v2 :\<sqsubset>val v1)" |
196 using assms |
196 using assms |
197 using PosOrd_irrefl PosOrd_trans by blast |
197 using PosOrd_irrefl PosOrd_trans by blast |
198 |
198 |
199 text {* |
199 (* |
200 :\<sqsubseteq>val and :\<sqsubset>val are partial orders. |
200 :\<sqsubseteq>val and :\<sqsubset>val are partial orders. |
201 *} |
201 *) |
202 |
202 |
203 lemma PosOrd_ordering: |
203 lemma PosOrd_ordering: |
204 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
204 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
205 unfolding ordering_def PosOrd_ex_eq_def |
205 unfolding ordering_def PosOrd_ex_eq_def |
206 apply(auto) |
206 apply(auto) |