# HG changeset patch
# User huffman
# Date 1315007310 25200
# Node ID 8e6cdb9c00a7e54dffdb60cea9474dcabc97f3e2
# Parent  31d41a0f6b5d09cc362b341e2eeb282f4a699cdb
remove redundant lemma reals_complete2 in favor of complete_real

diff -r 31d41a0f6b5d -r 8e6cdb9c00a7 NEWS
--- a/NEWS	Fri Sep 02 15:19:59 2011 -0700
+++ b/NEWS	Fri Sep 02 16:48:30 2011 -0700
@@ -274,6 +274,7 @@
   realpow_two_disj ~> power2_eq_iff
   real_squared_diff_one_factored ~> square_diff_one_factored
   realpow_two_diff ~> square_diff_square_factored
+  reals_complete2 ~> complete_real
   exp_ln_eq ~> ln_unique
   lemma_DERIV_subst ~> DERIV_cong
   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
diff -r 31d41a0f6b5d -r 8e6cdb9c00a7 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Sep 02 15:19:59 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 02 16:48:30 2011 -0700
@@ -1110,7 +1110,7 @@
     with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
     with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
       by (auto simp: real_of_ereal_ord_simps)
-    with reals_complete2[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
+    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     obtain s where s:
        "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
        by auto
diff -r 31d41a0f6b5d -r 8e6cdb9c00a7 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Fri Sep 02 15:19:59 2011 -0700
+++ b/src/HOL/RComplete.thy	Fri Sep 02 16:48:30 2011 -0700
@@ -80,14 +80,6 @@
       Collect_def mem_def isUb_def UNIV_def by simp
 qed
 
-text{*A version of the same theorem without all those predicates!*}
-lemma reals_complete2:
-  fixes S :: "(real set)"
-  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
-  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
-               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
-using assms by (rule complete_real)
-
 
 subsection {* The Archimedean Property of the Reals *}
 
diff -r 31d41a0f6b5d -r 8e6cdb9c00a7 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Fri Sep 02 15:19:59 2011 -0700
+++ b/src/HOL/SupInf.thy	Fri Sep 02 16:48:30 2011 -0700
@@ -30,7 +30,7 @@
       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   shows "x \<le> Sup X"
 proof (auto simp add: Sup_real_def) 
-  from reals_complete2
+  from complete_real
   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
     by (blast intro: x z)
   hence "x \<le> s"
@@ -46,7 +46,7 @@
       and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   shows "Sup X \<le> z"
 proof (auto simp add: Sup_real_def) 
-  from reals_complete2 x
+  from complete_real x
   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
     by (blast intro: z)
   hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
@@ -119,7 +119,7 @@
     apply (metis ex_in_conv x)
     apply (rule Sup_upper_EX) 
     apply blast
-    apply (metis insert_iff linear order_refl order_trans z)
+    apply (metis insert_iff linear order_trans z)
     done
   moreover 
   have "Sup (insert a X) \<le> Sup X"
@@ -333,7 +333,7 @@
     apply (metis ex_in_conv x)
     apply (rule Inf_lower_EX)
     apply (erule insertI2)
-    apply (metis insert_iff linear order_refl order_trans z)
+    apply (metis insert_iff linear order_trans z)
     done
   moreover 
   have "Inf X \<le> Inf (insert a X)"