--- a/NEWS Fri Sep 02 23:04:12 2011 +0200
+++ b/NEWS Fri Sep 02 16:58:00 2011 -0700
@@ -248,6 +248,11 @@
subset_interior ~> interior_mono
subset_closure ~> closure_mono
closure_univ ~> closure_UNIV
+ real_arch_lt ~> reals_Archimedean2
+ real_arch ~> reals_Archimedean3
+ real_abs_norm ~> abs_norm_cancel
+ real_abs_sub_norm ~> norm_triangle_ineq3
+ norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
* Complex_Main: The locale interpretations for the bounded_linear and
bounded_bilinear locales have been removed, in order to reduce the
@@ -269,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 23:04:12 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Sep 02 16:58:00 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/Multivariate_Analysis/Linear_Algebra.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Sep 02 16:58:00 2011 -0700
@@ -55,44 +55,35 @@
text{* Hence derive more interesting properties of the norm. *}
-(* FIXME: same as norm_scaleR
-lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"
- by (simp add: norm_vector_def setL2_right_distrib abs_mult)
-*)
-
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
- by (simp add: power2_eq_square)
+ by simp (* TODO: delete *)
lemma norm_cauchy_schwarz:
+ (* TODO: move to Inner_Product.thy *)
shows "inner x y <= norm x * norm y"
using Cauchy_Schwarz_ineq2[of x y] by auto
-lemma norm_cauchy_schwarz_abs:
- shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
- by (rule Cauchy_Schwarz_ineq2)
-
lemma norm_triangle_sub:
fixes x y :: "'a::real_normed_vector"
shows "norm x \<le> norm y + norm (x - y)"
using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
-lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
- by (rule abs_norm_cancel)
-lemma real_abs_sub_norm: "\<bar>norm x - norm y\<bar> <= norm(x - y)"
- by (rule norm_triangle_ineq3)
lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
by (simp add: norm_eq_sqrt_inner)
+
lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
by (simp add: norm_eq_sqrt_inner)
+
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
apply(subst order_eq_iff) unfolding norm_le by auto
+
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
- unfolding norm_eq_sqrt_inner by auto
+ by (simp add: norm_eq_sqrt_inner)
text{* Squaring equations and inequalities involving norms. *}
lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
- by (simp add: norm_eq_sqrt_inner)
+ by (simp only: power2_norm_eq_inner) (* TODO: move? *)
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
by (auto simp add: norm_eq_sqrt_inner)
@@ -159,10 +150,10 @@
unfolding dist_norm[THEN sym] .
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
- by (metis order_trans norm_triangle_ineq)
+ by (rule norm_triangle_ineq [THEN order_trans])
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
- by (metis basic_trans_rules(21) norm_triangle_ineq)
+ by (rule norm_triangle_ineq [THEN le_less_trans])
lemma setsum_clauses:
shows "setsum f {} = 0"
@@ -225,8 +216,8 @@
"orthogonal x a \<Longrightarrow> orthogonal (-x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
- unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
-
+ unfolding orthogonal_def inner_add inner_diff by auto
+
end
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
@@ -497,13 +488,10 @@
lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"
by (metis hull_redundant_eq)
-text{* Archimedian properties and useful consequences. *}
+subsection {* Archimedean properties and useful consequences *}
lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"
- using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)
-lemmas real_arch_lt = reals_Archimedean2
-
-lemmas real_arch = reals_Archimedean3
+ unfolding real_of_nat_def by (rule ex_le_of_nat)
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
using reals_Archimedean
@@ -530,7 +518,7 @@
lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
proof-
from x have x0: "x - 1 > 0" by arith
- from real_arch[OF x0, rule_format, of y]
+ from reals_Archimedean3[OF x0, rule_format, of y]
obtain n::nat where n:"y < real n * (x - 1)" by metis
from x0 have x00: "x- 1 \<ge> 0" by arith
from real_pow_lbound[OF x00, of n] n
@@ -570,7 +558,8 @@
shows "x = 0"
proof-
{assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith
- from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast
+ from reals_Archimedean3[OF xp, rule_format, of c]
+ obtain n::nat where n: "c < real n * x" by blast
with xc[rule_format, of n] have "n = 0" by arith
with n c have False by simp}
then show ?thesis by blast
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 02 16:58:00 2011 -0700
@@ -914,7 +914,7 @@
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
unfolding eventually_within
-by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl)
+by auto (metis dense order_le_less_trans)
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
unfolding trivial_limit_def
--- a/src/HOL/Probability/Borel_Space.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Fri Sep 02 16:58:00 2011 -0700
@@ -509,7 +509,7 @@
also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else -real k) <..})" using `i <DIM('a)`
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
fix x
- from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
+ from reals_Archimedean2[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
guess k::nat .. note k = this
{ fix i assume "i < DIM('a)"
then have "-x$$i < real k"
@@ -544,7 +544,7 @@
also have *: "{x::'a. x$$i < a} = (\<Union>k::nat. {..< (\<chi>\<chi> n. if n = i then a else real k)})" using `i <DIM('a)`
proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
fix x
- from real_arch_lt[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
+ from reals_Archimedean2[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"]
guess k::nat .. note k = this
{ fix i assume "i < DIM('a)"
then have "x$$i < real k"
@@ -1221,7 +1221,7 @@
{ fix x :: ereal assume *: "\<forall>i::nat. real i < x"
have "x = \<infinity>"
proof (rule ereal_top)
- fix B from real_arch_lt[of B] guess n ..
+ fix B from reals_Archimedean2[of B] guess n ..
then have "ereal B < real n" by auto
with * show "B \<le> x" by (metis less_trans less_imp_le)
qed }
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Sep 02 16:58:00 2011 -0700
@@ -392,10 +392,10 @@
proof (cases y)
case (real r)
with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
- from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
+ from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
then guess p .. note ux = this
- obtain m :: nat where m: "p < real m" using real_arch_lt ..
+ obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..
have "p \<le> r"
proof (rule ccontr)
assume "\<not> p \<le> r"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Sep 02 16:58:00 2011 -0700
@@ -41,7 +41,7 @@
qed
lemma mem_big_cube: obtains n where "x \<in> cube n"
-proof- from real_arch_lt[of "norm x"] guess n ..
+proof- from reals_Archimedean2[of "norm x"] guess n ..
thus ?thesis apply-apply(rule that[where n=n])
apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
by (auto simp add:dist_norm)
@@ -805,7 +805,7 @@
have "sets ?G = sets (\<Pi>\<^isub>M i\<in>I.
sigma \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>)"
by (subst sigma_product_algebra_sigma_eq[of I "\<lambda>_ i. {..<real i}" ])
- (auto intro!: measurable_sigma_sigma incseq_SucI real_arch_lt
+ (auto intro!: measurable_sigma_sigma incseq_SucI reals_Archimedean2
simp: product_algebra_def)
then show ?thesis
unfolding lborel_def borel_eq_lessThan lebesgue_def sigma_def by simp
--- a/src/HOL/RComplete.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/RComplete.thy Fri Sep 02 16:58:00 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 *}
@@ -106,27 +98,6 @@
unfolding real_of_nat_def using `0 < x`
by (auto intro: ex_less_of_nat_mult)
-lemma reals_Archimedean6:
- "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
-unfolding real_of_nat_def
-apply (rule exI [where x="nat (floor r + 1)"])
-apply (insert floor_correct [of r])
-apply (simp add: nat_add_distrib of_nat_nat)
-done
-
-lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
- by (drule reals_Archimedean6) auto
-
-text {* TODO: delete *}
-lemma reals_Archimedean_6b_int:
- "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
- unfolding real_of_int_def by (rule floor_exists)
-
-text {* TODO: delete *}
-lemma reals_Archimedean_6c_int:
- "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
- unfolding real_of_int_def by (rule floor_exists)
-
subsection{*Density of the Rational Reals in the Reals*}
@@ -134,50 +105,25 @@
original source is \emph{Real Analysis} by H.L. Royden.
It employs the Archimedean property of the reals. *}
-lemma Rats_dense_in_nn_real: fixes x::real
-assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y"
+lemma Rats_dense_in_real:
+ fixes x :: real
+ assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
proof -
from `x<y` have "0 < y-x" by simp
with reals_Archimedean obtain q::nat
- where q: "inverse (real q) < y-x" and "0 < real q" by auto
- def p \<equiv> "LEAST n. y \<le> real (Suc n)/real q"
- from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
- with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n")
- by (simp add: pos_less_divide_eq[THEN sym])
- also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
- ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
- by (unfold p_def) (rule Least_Suc)
- also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
- ultimately have suc: "y \<le> real (Suc p) / real q" by simp
- def r \<equiv> "real p/real q"
- have "x = y-(y-x)" by simp
- also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
- also have "\<dots> = real p / real q"
- by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc
- minus_divide_left add_divide_distrib[THEN sym]) simp
- finally have "x<r" by (unfold r_def)
- have "p<Suc p" .. also note main[THEN sym]
- finally have "\<not> ?P p" by (rule not_less_Least)
- hence "r<y" by (simp add: r_def)
- from r_def have "r \<in> \<rat>" by simp
- with `x<r` `r<y` show ?thesis by fast
-qed
-
-theorem Rats_dense_in_real: fixes x y :: real
-assumes "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y"
-proof -
- from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
- hence "0 \<le> x + real n" by arith
- also from `x<y` have "x + real n < y + real n" by arith
- ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
- by(rule Rats_dense_in_nn_real)
- then obtain r where "r \<in> \<rat>" and r2: "x + real n < r"
- and r3: "r < y + real n"
- by blast
- have "r - real n = r + real (int n)/real (-1::int)" by simp
- also from `r\<in>\<rat>` have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
- also from r2 have "x < r - real n" by arith
- moreover from r3 have "r - real n < y" by arith
+ where q: "inverse (real q) < y-x" and "0 < q" by auto
+ def p \<equiv> "ceiling (y * real q) - 1"
+ def r \<equiv> "of_int p / real q"
+ from q have "x < y - inverse (real q)" by simp
+ also have "y - inverse (real q) \<le> r"
+ unfolding r_def p_def
+ by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
+ finally have "x < r" .
+ moreover have "r < y"
+ unfolding r_def p_def
+ by (simp add: divide_less_eq diff_less_eq `0 < q`
+ less_ceiling_iff [symmetric])
+ moreover from r_def have "r \<in> \<rat>" by simp
ultimately show ?thesis by fast
qed
--- a/src/HOL/SupInf.thy Fri Sep 02 23:04:12 2011 +0200
+++ b/src/HOL/SupInf.thy Fri Sep 02 16:58:00 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"
@@ -79,7 +79,7 @@
lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
fixes z :: real
shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
- by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
+ by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)
lemma Sup_eq:
fixes a :: real
@@ -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)"