equal
deleted
inserted
replaced
269 subsubsection \<open>Equational laws\<close> |
269 subsubsection \<open>Equational laws\<close> |
270 |
270 |
271 context semilattice_inf |
271 context semilattice_inf |
272 begin |
272 begin |
273 |
273 |
274 sublocale inf!: semilattice inf |
274 sublocale inf: semilattice inf |
275 proof |
275 proof |
276 fix a b c |
276 fix a b c |
277 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
277 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
278 by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff) |
278 by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff) |
279 show "a \<sqinter> b = b \<sqinter> a" |
279 show "a \<sqinter> b = b \<sqinter> a" |
280 by (rule antisym) (auto simp add: le_inf_iff) |
280 by (rule antisym) (auto simp add: le_inf_iff) |
281 show "a \<sqinter> a = a" |
281 show "a \<sqinter> a = a" |
282 by (rule antisym) (auto simp add: le_inf_iff) |
282 by (rule antisym) (auto simp add: le_inf_iff) |
283 qed |
283 qed |
284 |
284 |
285 sublocale inf!: semilattice_order inf less_eq less |
285 sublocale inf: semilattice_order inf less_eq less |
286 by standard (auto simp add: le_iff_inf less_le) |
286 by standard (auto simp add: le_iff_inf less_le) |
287 |
287 |
288 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
288 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
289 by (fact inf.assoc) |
289 by (fact inf.assoc) |
290 |
290 |
314 end |
314 end |
315 |
315 |
316 context semilattice_sup |
316 context semilattice_sup |
317 begin |
317 begin |
318 |
318 |
319 sublocale sup!: semilattice sup |
319 sublocale sup: semilattice sup |
320 proof |
320 proof |
321 fix a b c |
321 fix a b c |
322 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
322 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
323 by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
323 by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
324 show "a \<squnion> b = b \<squnion> a" |
324 show "a \<squnion> b = b \<squnion> a" |
325 by (rule antisym) (auto simp add: le_sup_iff) |
325 by (rule antisym) (auto simp add: le_sup_iff) |
326 show "a \<squnion> a = a" |
326 show "a \<squnion> a = a" |
327 by (rule antisym) (auto simp add: le_sup_iff) |
327 by (rule antisym) (auto simp add: le_sup_iff) |
328 qed |
328 qed |
329 |
329 |
330 sublocale sup!: semilattice_order sup greater_eq greater |
330 sublocale sup: semilattice_order sup greater_eq greater |
331 by standard (auto simp add: le_iff_sup sup.commute less_le) |
331 by standard (auto simp add: le_iff_sup sup.commute less_le) |
332 |
332 |
333 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
333 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
334 by (fact sup.assoc) |
334 by (fact sup.assoc) |
335 |
335 |
482 subsection \<open>Bounded lattices and boolean algebras\<close> |
482 subsection \<open>Bounded lattices and boolean algebras\<close> |
483 |
483 |
484 class bounded_semilattice_inf_top = semilattice_inf + order_top |
484 class bounded_semilattice_inf_top = semilattice_inf + order_top |
485 begin |
485 begin |
486 |
486 |
487 sublocale inf_top!: semilattice_neutr inf top |
487 sublocale inf_top: semilattice_neutr inf top |
488 + inf_top!: semilattice_neutr_order inf top less_eq less |
488 + inf_top: semilattice_neutr_order inf top less_eq less |
489 proof |
489 proof |
490 fix x |
490 fix x |
491 show "x \<sqinter> \<top> = x" |
491 show "x \<sqinter> \<top> = x" |
492 by (rule inf_absorb1) simp |
492 by (rule inf_absorb1) simp |
493 qed |
493 qed |
495 end |
495 end |
496 |
496 |
497 class bounded_semilattice_sup_bot = semilattice_sup + order_bot |
497 class bounded_semilattice_sup_bot = semilattice_sup + order_bot |
498 begin |
498 begin |
499 |
499 |
500 sublocale sup_bot!: semilattice_neutr sup bot |
500 sublocale sup_bot: semilattice_neutr sup bot |
501 + sup_bot!: semilattice_neutr_order sup bot greater_eq greater |
501 + sup_bot: semilattice_neutr_order sup bot greater_eq greater |
502 proof |
502 proof |
503 fix x |
503 fix x |
504 show "x \<squnion> \<bottom> = x" |
504 show "x \<squnion> \<bottom> = x" |
505 by (rule sup_absorb1) simp |
505 by (rule sup_absorb1) simp |
506 qed |
506 qed |
713 subsection \<open>@{text "min/max"} as special case of lattice\<close> |
713 subsection \<open>@{text "min/max"} as special case of lattice\<close> |
714 |
714 |
715 context linorder |
715 context linorder |
716 begin |
716 begin |
717 |
717 |
718 sublocale min!: semilattice_order min less_eq less |
718 sublocale min: semilattice_order min less_eq less |
719 + max!: semilattice_order max greater_eq greater |
719 + max: semilattice_order max greater_eq greater |
720 by standard (auto simp add: min_def max_def) |
720 by standard (auto simp add: min_def max_def) |
721 |
721 |
722 lemma min_le_iff_disj: |
722 lemma min_le_iff_disj: |
723 "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
723 "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
724 unfolding min_def using linear by (auto intro: order_trans) |
724 unfolding min_def using linear by (auto intro: order_trans) |