--- a/src/HOL/SupInf.thy Mon Feb 08 14:06:51 2010 +0100
+++ b/src/HOL/SupInf.thy Mon Feb 08 14:06:54 2010 +0100
@@ -6,38 +6,6 @@
imports RComplete
begin
-lemma minus_max_eq_min:
- 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::{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::{lattice_ab_group_add, linorder} set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
-proof (induct S rule: finite_ne_induct)
- case (singleton x)
- thus ?case by simp
-next
- case (insert x S)
- thus ?case by (simp add: minus_max_eq_min)
-qed
-
-lemma minus_Min_eq_Max [simp]:
- fixes S :: "'a::{lattice_ab_group_add, linorder} set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
-proof (induct S rule: finite_ne_induct)
- case (singleton x)
- thus ?case by simp
-next
- case (insert x S)
- thus ?case by (simp add: minus_min_eq_max)
-qed
-
instantiation real :: Sup
begin
definition