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)
```