src/HOL/Lattices.thy
changeset 51489 f738e6dbd844
parent 51487 f4bfdee99304
child 51540 eea5c4ca4a0e
     1.1 --- a/src/HOL/Lattices.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -716,32 +716,6 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection {* @{const min}/@{const max} on linear orders as
     1.8 -  special case of @{const inf}/@{const sup} *}
     1.9 -
    1.10 -sublocale linorder < min_max!: distrib_lattice min less_eq less max
    1.11 -proof
    1.12 -  fix x y z
    1.13 -  show "max x (min y z) = min (max x y) (max x z)"
    1.14 -    by (auto simp add: min_def max_def)
    1.15 -qed (auto simp add: min_def max_def not_le less_imp_le)
    1.16 -
    1.17 -lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.18 -  by (rule ext)+ (auto intro: antisym)
    1.19 -
    1.20 -lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.21 -  by (rule ext)+ (auto intro: antisym)
    1.22 -
    1.23 -lemmas le_maxI1 = min_max.sup_ge1
    1.24 -lemmas le_maxI2 = min_max.sup_ge2
    1.25 - 
    1.26 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
    1.27 -  min_max.inf.left_commute
    1.28 -
    1.29 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
    1.30 -  min_max.sup.left_commute
    1.31 -
    1.32 -
    1.33  subsection {* Lattice on @{typ bool} *}
    1.34  
    1.35  instantiation bool :: boolean_algebra