src/HOL/Lattices.thy
changeset 32204 b330aa4d59cb
parent 32064 53ca12ff305d
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/Lattices.thy	Sat Jul 25 18:44:54 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Sat Jul 25 18:44:54 2009 +0200
     1.3 @@ -413,20 +413,14 @@
     1.4  subsection {* @{const min}/@{const max} on linear orders as
     1.5    special case of @{const inf}/@{const sup} *}
     1.6  
     1.7 -lemma (in linorder) distrib_lattice_min_max:
     1.8 -  "distrib_lattice (op \<le>) (op <) min max"
     1.9 +sublocale linorder < min_max!: distrib_lattice less_eq less "Orderings.ord.min less_eq" "Orderings.ord.max less_eq"
    1.10  proof
    1.11 -  have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.12 -    by (auto simp add: less_le antisym)
    1.13    fix x y z
    1.14 -  show "max x (min y z) = min (max x y) (max x z)"
    1.15 -  unfolding min_def max_def
    1.16 -  by auto
    1.17 +  show "Orderings.ord.max less_eq x (Orderings.ord.min less_eq y z) =
    1.18 +    Orderings.ord.min less_eq (Orderings.ord.max less_eq x y) (Orderings.ord.max less_eq x z)"
    1.19 +  unfolding min_def max_def by auto
    1.20  qed (auto simp add: min_def max_def not_le less_imp_le)
    1.21  
    1.22 -interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
    1.23 -  by (rule distrib_lattice_min_max)
    1.24 -
    1.25  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.26    by (rule ext)+ (auto intro: antisym)
    1.27