diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/SupInf.thy --- a/src/HOL/SupInf.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/SupInf.thy Fri Feb 05 14:33:50 2010 +0100 @@ -7,17 +7,17 @@ begin lemma minus_max_eq_min: - fixes x :: "'a::{lordered_ab_group_add, linorder}" + fixes x :: "'a::{lattice_ab_group_add, linorder}" shows "- (max x y) = min (-x) (-y)" 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) lemma minus_min_eq_max: - fixes x :: "'a::{lordered_ab_group_add, linorder}" + fixes x :: "'a::{lattice_ab_group_add, linorder}" shows "- (min x y) = max (-x) (-y)" by (metis minus_max_eq_min minus_minus) lemma minus_Max_eq_Min [simp]: - fixes S :: "'a::{lordered_ab_group_add, linorder} set" + fixes S :: "'a::{lattice_ab_group_add, linorder} set" shows "finite S \ S \ {} \ - (Max S) = Min (uminus ` S)" proof (induct S rule: finite_ne_induct) case (singleton x) @@ -28,7 +28,7 @@ qed lemma minus_Min_eq_Max [simp]: - fixes S :: "'a::{lordered_ab_group_add, linorder} set" + fixes S :: "'a::{lattice_ab_group_add, linorder} set" shows "finite S \ S \ {} \ - (Min S) = Max (uminus ` S)" proof (induct S rule: finite_ne_induct) case (singleton x)