# HG changeset patch
# User hoelzl
# Date 1364296853 -3600
# Node ID 2831ce75ec49e20d010825c8cd330281efc7e0f2
# Parent  6a56b7088a6ab16b3bce2b00b33e32ba198666a7
remove posreal_complete

diff -r 6a56b7088a6a -r 2831ce75ec49 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Tue Mar 26 12:20:52 2013 +0100
+++ b/src/HOL/RComplete.thy	Tue Mar 26 12:20:53 2013 +0100
@@ -21,39 +21,6 @@
 subsection {* Completeness of Positive Reals *}
 
 text {*
-  Supremum property for the set of positive reals
-
-  Let @{text "P"} be a non-empty set of positive reals, with an upper
-  bound @{text "y"}.  Then @{text "P"} has a least upper bound
-  (written @{text "S"}).
-
-  FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?
-*}
-
-text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
-
-lemma posreal_complete:
-  fixes P :: "real set"
-  assumes not_empty_P: "\<exists>x. x \<in> P"
-    and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
-  shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
-proof -
-  from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z"
-    by (auto intro: less_imp_le)
-  from complete_real [OF not_empty_P this] obtain S
-  where S1: "\<And>x. x \<in> P \<Longrightarrow> x \<le> S" and S2: "\<And>z. \<forall>x\<in>P. x \<le> z \<Longrightarrow> S \<le> z" by fast
-  have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
-  proof
-    fix y show "(\<exists>x\<in>P. y < x) = (y < S)"
-      apply (cases "\<exists>x\<in>P. y < x", simp_all)
-      apply (clarify, drule S1, simp)
-      apply (simp add: not_less S2)
-      done
-  qed
-  thus ?thesis ..
-qed
-
-text {*
   \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
 *}
 
@@ -68,16 +35,8 @@
   \medskip reals Completeness (again!)
 *}
 
-lemma reals_complete:
-  assumes notempty_S: "\<exists>X. X \<in> S"
-    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
-  shows "\<exists>t. isLub (UNIV :: real set) S t"
-proof -
-  from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
-    unfolding isUb_def setle_def by simp_all
-  from complete_real [OF this] show ?thesis
-    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-qed
+lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
+  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
 
 
 subsection {* The Archimedean Property of the Reals *}