src/HOL/Lattices.thy
changeset 51540 eea5c4ca4a0e
parent 51489 f738e6dbd844
child 51546 2e26df807dc7
     1.1 --- a/src/HOL/Lattices.thy	Tue Mar 26 15:10:28 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Tue Mar 26 20:49:57 2013 +0100
     1.3 @@ -689,6 +689,19 @@
     1.4  end
     1.5  
     1.6  
     1.7 +subsection {* @{text "min/max"} as special case of lattice *}
     1.8 +
     1.9 +sublocale linorder < min!: semilattice_order min less_eq less
    1.10 +  + max!: semilattice_order max greater_eq greater
    1.11 +  by default (auto simp add: min_def max_def)
    1.12 +
    1.13 +lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.14 +  by (auto intro: antisym simp add: min_def fun_eq_iff)
    1.15 +
    1.16 +lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.17 +  by (auto intro: antisym simp add: max_def fun_eq_iff)
    1.18 +
    1.19 +
    1.20  subsection {* Uniqueness of inf and sup *}
    1.21  
    1.22  lemma (in semilattice_inf) inf_unique: