# 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 \ {}` `\ \ S` obtain x where "x \ S - {-\}" "x \ \" by auto with y `\ \ S` have "\z\real ` (S - {-\}). z \ y" by (auto simp: real_of_ereal_ord_simps) - with reals_complete2[of "real ` (S - {-\})"] `x \ S - {-\}` + with complete_real[of "real ` (S - {-\})"] `x \ S - {-\}` obtain s where s: "\y\S - {-\}. real y \ s" "\z. (\y\S - {-\}. real y \ z) \ s \ 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 "\y. y\S" and "\(x::real). \y\S. y \ x" - shows "\x. (\y\S. y \ x) & - (\z. ((\y\S. y \ z) --> x \ 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 \ X \ x \ z" shows "x \ Sup X" proof (auto simp add: Sup_real_def) - from reals_complete2 + from complete_real obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" by (blast intro: x z) hence "x \ s" @@ -46,7 +46,7 @@ and z: "\x. x \ X \ x \ z" shows "Sup X \ z" proof (auto simp add: Sup_real_def) - from reals_complete2 x + from complete_real x obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" by (blast intro: z) hence "(LEAST z. \x\X. x \ 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) \ 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 \ Inf (insert a X)"