1.1 --- a/src/HOL/RComplete.thy	Wed Sep 23 11:06:32 2009 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Fri Sep 25 13:47:28 2009 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
     1.5    by simp
     1.6  
     1.7 +lemma abs_diff_less_iff:
     1.8 +  "(\<bar>x - a\<bar> < (r::'a::ordered_idom)) = (a - r < x \<and> x < a + r)"
     1.9 +  by auto
    1.10  
    1.11  subsection {* Completeness of Positive Reals *}
    1.12  
    1.13 @@ -301,6 +304,20 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +text{*A version of the same theorem without all those predicates!*}
    1.18 +lemma reals_complete2:
    1.19 +  fixes S :: "(real set)"
    1.20 +  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
    1.21 +  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
    1.22 +               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
    1.23 +proof -
    1.24 +  have "\<exists>x. isLub UNIV S x" 
    1.25 +    by (rule reals_complete)
    1.26 +       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
    1.27 +  thus ?thesis
    1.28 +    by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
    1.29 +qed
    1.30 +
    1.31  
    1.32  subsection {* The Archimedean Property of the Reals *}
    1.33