1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.3 @@ -96,6 +96,16 @@
     1.4  lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
     1.5    by (rule bdd_belowI[of _ bot]) simp
     1.6  
     1.7 +lemma bdd_above_uminus[simp]:
     1.8 +  fixes X :: "'a::ordered_ab_group_add set"
     1.9 +  shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
    1.10 +  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.11 +
    1.12 +lemma bdd_below_uminus[simp]:
    1.13 +  fixes X :: "'a::ordered_ab_group_add set"
    1.14 +  shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
    1.15 +  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.16 +
    1.17  context lattice
    1.18  begin
    1.19  

     2.1 --- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
     2.2 +++ b/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
     2.3 @@ -919,13 +919,6 @@
     2.4      using 1 2 3 by (rule_tac x="Real B" in exI, simp)
     2.5  qed
     2.6  
     2.7 -(* TODO: generalize to ordered group *)
     2.8 -lemma bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below (X::real set)"
     2.9 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    2.10 -
    2.11 -lemma bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above (X::real set)"
    2.12 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    2.13 -
    2.14  instantiation real :: linear_continuum
    2.15  begin
    2.16