# HG changeset patch
# User hoelzl
# Date 1383641100 -3600
# Node ID 326fd7103cb4d169d38e2c4c6ab09bf040eae4dc
# Parent  89991ef58448e225d4949e8aba9040f1d4e92801
generalize bdd_above/below_uminus to ordered_ab_group_add

diff -r 89991ef58448 -r 326fd7103cb4 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
@@ -96,6 +96,16 @@
 lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
   by (rule bdd_belowI[of _ bot]) simp
 
+lemma bdd_above_uminus[simp]:
+  fixes X :: "'a::ordered_ab_group_add set"
+  shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
+  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+
+lemma bdd_below_uminus[simp]:
+  fixes X :: "'a::ordered_ab_group_add set"
+  shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
+  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+
 context lattice
 begin
 
diff -r 89991ef58448 -r 326fd7103cb4 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
@@ -919,13 +919,6 @@
     using 1 2 3 by (rule_tac x="Real B" in exI, simp)
 qed
 
-(* TODO: generalize to ordered group *)
-lemma bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below (X::real set)"
-  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
-
-lemma bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above (X::real set)"
-  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
-
 instantiation real :: linear_continuum
 begin