204 |
204 |
205 lemma PosOrd_ordering: |
205 lemma PosOrd_ordering: |
206 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
206 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
207 unfolding ordering_def PosOrd_ex_eq_def |
207 unfolding ordering_def PosOrd_ex_eq_def |
208 apply(auto) |
208 apply(auto) |
209 using PosOrd_irrefl apply blast |
209 using PosOrd_trans partial_preordering_def apply blast |
210 using PosOrd_assym apply blast |
210 using PosOrd_assym ordering_axioms_def by blast |
211 using PosOrd_trans by blast |
|
212 |
211 |
213 lemma PosOrd_order: |
212 lemma PosOrd_order: |
214 shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
213 shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
215 using PosOrd_ordering |
214 using PosOrd_ordering |
216 apply(simp add: class.order_def class.preorder_def class.order_axioms_def) |
215 apply(simp add: class.order_def class.preorder_def class.order_axioms_def) |
217 unfolding ordering_def |
216 by (metis (full_types) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans) |
218 by blast |
|
219 |
217 |
220 |
218 |
221 lemma PosOrd_ex_eq2: |
219 lemma PosOrd_ex_eq2: |
222 shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)" |
220 shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)" |
223 using PosOrd_ordering |
221 using PosOrd_ordering |
224 unfolding ordering_def |
222 using PosOrd_ex_eq_def PosOrd_irrefl by blast |
225 by auto |
|
226 |
223 |
227 lemma PosOrdeq_trans: |
224 lemma PosOrdeq_trans: |
228 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3" |
225 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3" |
229 shows "v1 :\<sqsubseteq>val v3" |
226 shows "v1 :\<sqsubseteq>val v3" |
230 using assms PosOrd_ordering |
227 using assms PosOrd_ordering |
231 unfolding ordering_def |
228 unfolding ordering_def |
232 by blast |
229 by (metis partial_preordering.trans) |
233 |
230 |
234 lemma PosOrdeq_antisym: |
231 lemma PosOrdeq_antisym: |
235 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1" |
232 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1" |
236 shows "v1 = v2" |
233 shows "v1 = v2" |
237 using assms PosOrd_ordering |
234 using assms PosOrd_ordering |
238 unfolding ordering_def |
235 unfolding ordering_def |
239 by blast |
236 by (simp add: ordering_axioms_def) |
240 |
237 |
241 lemma PosOrdeq_refl: |
238 lemma PosOrdeq_refl: |
242 shows "v :\<sqsubseteq>val v" |
239 shows "v :\<sqsubseteq>val v" |
243 unfolding PosOrd_ex_eq_def |
240 unfolding PosOrd_ex_eq_def |
244 by auto |
241 by auto |