src/HOL/SupInf.thy
changeset 35028 108662d50512
parent 33657 a4179bf442d1
child 35037 748f0bc3f7ca
     1.1 --- a/src/HOL/SupInf.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/SupInf.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -7,17 +7,17 @@
     1.4  begin
     1.5  
     1.6  lemma minus_max_eq_min:
     1.7 -  fixes x :: "'a::{lordered_ab_group_add, linorder}"
     1.8 +  fixes x :: "'a::{lattice_ab_group_add, linorder}"
     1.9    shows "- (max x y) = min (-x) (-y)"
    1.10  by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
    1.11  
    1.12  lemma minus_min_eq_max:
    1.13 -  fixes x :: "'a::{lordered_ab_group_add, linorder}"
    1.14 +  fixes x :: "'a::{lattice_ab_group_add, linorder}"
    1.15    shows "- (min x y) = max (-x) (-y)"
    1.16  by (metis minus_max_eq_min minus_minus)
    1.17  
    1.18  lemma minus_Max_eq_Min [simp]:
    1.19 -  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    1.20 +  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
    1.21    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
    1.22  proof (induct S rule: finite_ne_induct)
    1.23    case (singleton x)
    1.24 @@ -28,7 +28,7 @@
    1.25  qed
    1.26  
    1.27  lemma minus_Min_eq_Max [simp]:
    1.28 -  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    1.29 +  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
    1.30    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
    1.31  proof (induct S rule: finite_ne_induct)
    1.32    case (singleton x)