src/HOL/RComplete.thy
 changeset 32707 836ec9d0a0c8 parent 30242 aea5d7fa7ef5 child 32960 69916a850301
```     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
```