411 |
411 |
412 |
412 |
413 subsection {* @{const min}/@{const max} on linear orders as |
413 subsection {* @{const min}/@{const max} on linear orders as |
414 special case of @{const inf}/@{const sup} *} |
414 special case of @{const inf}/@{const sup} *} |
415 |
415 |
416 lemma (in linorder) distrib_lattice_min_max: |
416 sublocale linorder < min_max!: distrib_lattice less_eq less "Orderings.ord.min less_eq" "Orderings.ord.max less_eq" |
417 "distrib_lattice (op \<le>) (op <) min max" |
|
418 proof |
417 proof |
419 have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" |
|
420 by (auto simp add: less_le antisym) |
|
421 fix x y z |
418 fix x y z |
422 show "max x (min y z) = min (max x y) (max x z)" |
419 show "Orderings.ord.max less_eq x (Orderings.ord.min less_eq y z) = |
423 unfolding min_def max_def |
420 Orderings.ord.min less_eq (Orderings.ord.max less_eq x y) (Orderings.ord.max less_eq x z)" |
424 by auto |
421 unfolding min_def max_def by auto |
425 qed (auto simp add: min_def max_def not_le less_imp_le) |
422 qed (auto simp add: min_def max_def not_le less_imp_le) |
426 |
|
427 interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max |
|
428 by (rule distrib_lattice_min_max) |
|
429 |
423 |
430 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
424 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
431 by (rule ext)+ (auto intro: antisym) |
425 by (rule ext)+ (auto intro: antisym) |
432 |
426 |
433 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
427 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |