--- 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
--- 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
--- 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 *}
--- 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)"