# HG changeset patch # User huffman # Date 1314548412 25200 # Node ID e6f291cb5810332ed0a99d4228d91122a7d1d73c # Parent 5e5e6ad3922c687da5832f9efa3fecf52a00efe2 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems diff -r 5e5e6ad3922c -r e6f291cb5810 NEWS --- a/NEWS Sat Aug 27 17:26:14 2011 +0200 +++ b/NEWS Sun Aug 28 09:20:12 2011 -0700 @@ -246,8 +246,8 @@ mult_right.setsum ~> setsum_right_distrib mult_left.diff ~> left_diff_distrib -* Complex_Main: Several redundant theorems about real numbers have -been removed or generalized and renamed. INCOMPATIBILITY. +* Complex_Main: Several redundant theorems have been removed or +replaced by more general versions. INCOMPATIBILITY. real_0_le_divide_iff ~> zero_le_divide_iff realpow_two_disj ~> power2_eq_iff @@ -255,6 +255,53 @@ realpow_two_diff ~> square_diff_square_factored exp_ln_eq ~> ln_unique lemma_DERIV_subst ~> DERIV_cong + LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff + LIMSEQ_const ~> tendsto_const + LIMSEQ_norm ~> tendsto_norm + LIMSEQ_add ~> tendsto_add + LIMSEQ_minus ~> tendsto_minus + LIMSEQ_minus_cancel ~> tendsto_minus_cancel + LIMSEQ_diff ~> tendsto_diff + bounded_linear.LIMSEQ ~> bounded_linear.tendsto + bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto + LIMSEQ_mult ~> tendsto_mult + LIMSEQ_inverse ~> tendsto_inverse + LIMSEQ_divide ~> tendsto_divide + LIMSEQ_pow ~> tendsto_power + LIMSEQ_setsum ~> tendsto_setsum + LIMSEQ_setprod ~> tendsto_setprod + LIMSEQ_norm_zero ~> tendsto_norm_zero_iff + LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff + LIMSEQ_imp_rabs ~> tendsto_rabs + LIM_ident ~> tendsto_ident_at + LIM_const ~> tendsto_const + LIM_add ~> tendsto_add + LIM_add_zero ~> tendsto_add_zero + LIM_minus ~> tendsto_minus + LIM_diff ~> tendsto_diff + LIM_norm ~> tendsto_norm + LIM_norm_zero ~> tendsto_norm_zero + LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel + LIM_norm_zero_iff ~> tendsto_norm_zero_iff + LIM_rabs ~> tendsto_rabs + LIM_rabs_zero ~> tendsto_rabs_zero + LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel + LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff + LIM_compose ~> tendsto_compose + LIM_mult ~> tendsto_mult + LIM_scaleR ~> tendsto_scaleR + LIM_of_real ~> tendsto_of_real + LIM_power ~> tendsto_power + LIM_inverse ~> tendsto_inverse + LIM_sgn ~> tendsto_sgn + isCont_LIM_compose ~> isCont_tendsto_compose + bounded_linear.LIM ~> bounded_linear.tendsto + bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero + bounded_bilinear.LIM ~> bounded_bilinear.tendsto + bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero + bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero + bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero + LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] *** Document preparation *** diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sun Aug 28 09:20:12 2011 -0700 @@ -1687,7 +1687,7 @@ have "norm x < 1" using assms by auto have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] - using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto + using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto { fix n have "0 \ ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \ x`) } { fix n have "?a (Suc n) \ ?a n" unfolding inverse_eq_divide[symmetric] proof (rule mult_mono) diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Deriv.thy Sun Aug 28 09:20:12 2011 -0700 @@ -37,18 +37,18 @@ by (simp add: deriv_def) lemma DERIV_const [simp]: "DERIV (\x. k) x :> 0" -by (simp add: deriv_def) + by (simp add: deriv_def tendsto_const) lemma DERIV_ident [simp]: "DERIV (\x. x) x :> 1" -by (simp add: deriv_def cong: LIM_cong) + by (simp add: deriv_def tendsto_const cong: LIM_cong) lemma DERIV_add: "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + g x) x :> D + E" -by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add) + by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add) lemma DERIV_minus: "DERIV f x :> D \ DERIV (\x. - f x) x :> - D" -by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus) + by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus) lemma DERIV_diff: "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x - g x) x :> D - E" @@ -64,7 +64,7 @@ hence "(\h. (f(x+h) - f(x)) / h) -- 0 --> D" by (rule DERIV_D) hence "(\h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0" - by (intro LIM_mult LIM_ident) + by (intro tendsto_mult tendsto_ident_at) hence "(\h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0" by simp hence "(\h. f(x+h) - f(x)) -- 0 --> 0" @@ -90,7 +90,7 @@ hence "(\h. f(x+h) * ((g(x+h) - g x) / h) + ((f(x+h) - f x) / h) * g x) -- 0 --> f x * E + D * g x" - by (intro LIM_add LIM_mult LIM_const DERIV_D f g) + by (intro tendsto_intros DERIV_D f g) thus "(\h. (f(x+h) * g(x+h) - f x * g x) / h) -- 0 --> f x * E + D * g x" by (simp only: DERIV_mult_lemma) @@ -172,7 +172,7 @@ by (unfold DERIV_iff2) thus "(\z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))) -- x --> ?E" - by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq) + by (intro tendsto_intros lim_f neq) qed qed @@ -245,10 +245,10 @@ from f have "f -- x --> f x" by (rule DERIV_isCont [unfolded isCont_def]) with cont_d have "(\z. d (f z)) -- x --> d (f x)" - by (rule isCont_LIM_compose) + by (rule isCont_tendsto_compose) hence "(\z. d (f z) * ((f z - f x) / (z - x))) -- x --> d (f x) * D" - by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) + by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]]) thus "(\z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" by (simp add: d dfx) qed @@ -485,7 +485,7 @@ lemma lim_uminus: fixes g :: "nat \ 'a::real_normed_vector" shows "convergent g ==> lim (%x. - g x) = - (lim g)" -apply (rule LIMSEQ_minus [THEN limI]) +apply (rule tendsto_minus [THEN limI]) apply (simp add: convergent_LIMSEQ_iff) done @@ -521,7 +521,7 @@ ((\n. l \ g(n)) & g ----> l)" apply (drule lemma_nest, auto) apply (subgoal_tac "l = m") -apply (drule_tac [2] f = f in LIMSEQ_diff) +apply (drule_tac [2] f = f in tendsto_diff) apply (auto intro: LIMSEQ_unique) done @@ -599,7 +599,7 @@ a \ b |] ==> P(a,b)" apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+) -apply (rule LIMSEQ_minus_cancel) +apply (rule tendsto_minus_cancel) apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero) apply (rule ccontr) apply (drule not_P_Bolzano_bisect', assumption+) @@ -1488,7 +1488,7 @@ using cont 1 2 by (rule isCont_LIM_compose2) thus "(\y. inverse ((f (g y) - x) / (g y - g x))) -- x --> inverse D" - using neq by (rule LIM_inverse) + using neq by (rule tendsto_inverse) qed diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Library/FrechetDeriv.thy --- a/src/HOL/Library/FrechetDeriv.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Sun Aug 28 09:20:12 2011 -0700 @@ -32,13 +32,13 @@ by (rule bounded_linear_intro [where K=0], simp_all) lemma FDERIV_const: "FDERIV (\x. k) x :> (\h. 0)" - by (simp add: fderiv_def bounded_linear_zero) + by (simp add: fderiv_def bounded_linear_zero tendsto_const) lemma bounded_linear_ident: "bounded_linear (\x. x)" by (rule bounded_linear_intro [where K=1], simp_all) lemma FDERIV_ident: "FDERIV (\x. x) x :> (\h. h)" - by (simp add: fderiv_def bounded_linear_ident) + by (simp add: fderiv_def bounded_linear_ident tendsto_const) subsection {* Addition *} @@ -90,7 +90,7 @@ from f' g' have "(\h. norm (f (x + h) - f x - F h) / norm h + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" - by (rule LIM_add_zero) + by (rule tendsto_add_zero) thus "(\h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h)) / norm h) -- 0 --> 0" apply (rule real_LIM_sandwich_zero) @@ -178,13 +178,13 @@ have "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" by (rule FDERIV_D [OF f]) hence "(\h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0" - by (intro LIM_mult_zero LIM_norm_zero LIM_ident) + by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at) hence "(\h. norm (f (x + h) - f x - F h)) -- 0 --> 0" by (simp cong: LIM_cong) hence "(\h. f (x + h) - f x - F h) -- 0 --> 0" - by (rule LIM_norm_zero_cancel) + by (rule tendsto_norm_zero_cancel) hence "(\h. f (x + h) - f x - F h + F h) -- 0 --> 0" - by (intro LIM_add_zero F.LIM_zero LIM_ident) + by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at) hence "(\h. f (x + h) - f x) -- 0 --> 0" by simp thus "isCont f x" @@ -266,11 +266,11 @@ apply (rule FDERIV_isCont [OF f]) done have Ng: "?Ng -- 0 --> 0" - using isCont_LIM_compose [OF Ng1 Ng2] by simp + using isCont_tendsto_compose [OF Ng1 Ng2] by simp have "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0 * kG + 0 * (0 + kF)" - by (intro LIM_add LIM_mult LIM_const Nf Ng) + by (intro tendsto_intros Nf Ng) thus "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0" by simp next @@ -369,7 +369,7 @@ from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]] have "?fun2 -- 0 --> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K" - by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D) + by (intro tendsto_intros LIM_zero FDERIV_D) thus "?fun2 -- 0 --> 0" by simp next @@ -474,12 +474,12 @@ proof (rule real_LIM_sandwich_zero) show "(\h. norm (?inv (x + h) - ?inv x) * norm (?inv x)) -- 0 --> 0" - apply (rule LIM_mult_left_zero) - apply (rule LIM_norm_zero) + apply (rule tendsto_mult_left_zero) + apply (rule tendsto_norm_zero) apply (rule LIM_zero) apply (rule LIM_offset_zero) - apply (rule LIM_inverse) - apply (rule LIM_ident) + apply (rule tendsto_inverse) + apply (rule tendsto_ident_at) apply (rule x) done next @@ -517,7 +517,7 @@ apply (subst diff_divide_distrib) apply (subst times_divide_eq_left [symmetric]) apply (simp cong: LIM_cong) - apply (simp add: LIM_norm_zero_iff LIM_zero_iff) + apply (simp add: tendsto_norm_zero_iff LIM_zero_iff) done end diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Library/Product_Vector.thy Sun Aug 28 09:20:12 2011 -0700 @@ -544,7 +544,7 @@ apply (rule FDERIV_bounded_linear [OF g]) apply (simp add: norm_Pair) apply (rule real_LIM_sandwich_zero) -apply (rule LIM_add_zero) +apply (rule tendsto_add_zero) apply (rule FDERIV_D [OF f]) apply (rule FDERIV_D [OF g]) apply (rename_tac h) diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Lim.thy Sun Aug 28 09:20:12 2011 -0700 @@ -211,51 +211,6 @@ finally show "norm (g x - 0) \ norm (f x - 0)" . qed -text {* Bounded Linear Operators *} - -lemma (in bounded_linear) LIM: - "g -- a --> l \ (\x. f (g x)) -- a --> f l" -by (rule tendsto) - -lemma (in bounded_linear) LIM_zero: - "g -- a --> 0 \ (\x. f (g x)) -- a --> 0" - by (rule tendsto_zero) - -text {* Bounded Bilinear Operators *} - -lemma (in bounded_bilinear) LIM: - "\f -- a --> L; g -- a --> M\ \ (\x. f x ** g x) -- a --> L ** M" -by (rule tendsto) - -lemma (in bounded_bilinear) LIM_prod_zero: - fixes a :: "'d::metric_space" - assumes f: "f -- a --> 0" - assumes g: "g -- a --> 0" - shows "(\x. f x ** g x) -- a --> 0" - using f g by (rule tendsto_zero) - -lemma (in bounded_bilinear) LIM_left_zero: - "f -- a --> 0 \ (\x. f x ** c) -- a --> 0" - by (rule tendsto_left_zero) - -lemma (in bounded_bilinear) LIM_right_zero: - "f -- a --> 0 \ (\x. c ** f x) -- a --> 0" - by (rule tendsto_right_zero) - -lemmas LIM_mult_zero = - bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult] - -lemmas LIM_mult_left_zero = - bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult] - -lemmas LIM_mult_right_zero = - bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult] - -lemma LIM_inverse_fun: - assumes a: "a \ (0::'a::real_normed_div_algebra)" - shows "inverse -- a --> inverse a" - by (rule tendsto_inverse [OF tendsto_ident_at a]) - subsection {* Continuity *} @@ -495,29 +450,4 @@ (X -- a --> (L::'b::topological_space))" using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. -subsection {* Legacy theorem names *} - -lemmas LIM_ident [simp] = tendsto_ident_at -lemmas LIM_const [simp] = tendsto_const [where F="at x", standard] -lemmas LIM_add = tendsto_add [where F="at x", standard] -lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard] -lemmas LIM_minus = tendsto_minus [where F="at x", standard] -lemmas LIM_diff = tendsto_diff [where F="at x", standard] -lemmas LIM_norm = tendsto_norm [where F="at x", standard] -lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard] -lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard] -lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard] -lemmas LIM_rabs = tendsto_rabs [where F="at x", standard] -lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard] -lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard] -lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard] -lemmas LIM_compose = tendsto_compose [where F="at x", standard] -lemmas LIM_mult = tendsto_mult [where F="at x", standard] -lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard] -lemmas LIM_of_real = tendsto_of_real [where F="at x", standard] -lemmas LIM_power = tendsto_power [where F="at x", standard] -lemmas LIM_inverse = tendsto_inverse [where F="at x", standard] -lemmas LIM_sgn = tendsto_sgn [where F="at x", standard] -lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard] - end diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Limits.thy Sun Aug 28 09:20:12 2011 -0700 @@ -791,6 +791,15 @@ lemmas tendsto_mult [tendsto_intros] = bounded_bilinear.tendsto [OF bounded_bilinear_mult] +lemmas tendsto_mult_zero = + bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] + +lemmas tendsto_mult_left_zero = + bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] + +lemmas tendsto_mult_right_zero = + bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] + lemma tendsto_power [tendsto_intros]: fixes f :: "'a \ 'b::{power,real_normed_algebra}" shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 28 09:20:12 2011 -0700 @@ -47,7 +47,7 @@ shows "FDERIV f x :> f' = (f has_derivative f') (at x)" unfolding fderiv_def has_derivative_def netlimit_at_vector by (simp add: diff_diff_eq Lim_at_zero [where a=x] - LIM_norm_zero_iff [where 'b='b, symmetric]) + tendsto_norm_zero_iff [where 'b='b, symmetric]) lemma DERIV_conv_has_derivative: "(DERIV f x :> f') = (f has_derivative op * f') (at x)" diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 28 09:20:12 2011 -0700 @@ -1332,10 +1332,10 @@ unfolding netlimit_def apply (rule some_equality) apply (rule Lim_at_within) -apply (rule LIM_ident) +apply (rule tendsto_ident_at) apply (erule tendsto_unique [OF assms]) apply (rule Lim_at_within) -apply (rule LIM_ident) +apply (rule tendsto_ident_at) done lemma netlimit_at: @@ -3569,11 +3569,11 @@ lemma continuous_within_id: "continuous (at a within s) (\x. x)" - unfolding continuous_within by (rule Lim_at_within [OF LIM_ident]) + unfolding continuous_within by (rule Lim_at_within [OF tendsto_ident_at]) lemma continuous_at_id: "continuous (at a) (\x. x)" - unfolding continuous_at by (rule LIM_ident) + unfolding continuous_at by (rule tendsto_ident_at) lemma continuous_on_id: "continuous_on s (\x. x)" @@ -4260,7 +4260,7 @@ proof (rule continuous_attains_sup [OF assms]) { fix x assume "x\s" have "(dist a ---> dist a x) (at x within s)" - by (intro tendsto_dist tendsto_const Lim_at_within LIM_ident) + by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at) } thus "continuous_on s (dist a)" unfolding continuous_on .. diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/NSA/HSEQ.thy --- a/src/HOL/NSA/HSEQ.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/NSA/HSEQ.thy Sun Aug 28 09:20:12 2011 -0700 @@ -207,10 +207,10 @@ text{*We prove the NS version from the standard one, since the NS proof seems more complicated than the standard one above!*} lemma NSLIMSEQ_norm_zero: "((\n. norm (X n)) ----NS> 0) = (X ----NS> 0)" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero) +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff) lemma NSLIMSEQ_rabs_zero: "((%n. \f n\) ----NS> 0) = (f ----NS> (0::real))" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero) +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff) text{*Generalization to other limits*} lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \f n\) ----NS> \l\" diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Probability/Caratheodory.thy --- a/src/HOL/Probability/Caratheodory.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Probability/Caratheodory.thy Sun Aug 28 09:20:12 2011 -0700 @@ -128,7 +128,7 @@ by (induct n) (auto simp add: binaryset_def f) qed moreover - have "... ----> f A + f B" by (rule LIMSEQ_const) + have "... ----> f A + f B" by (rule tendsto_const) ultimately have "(\n. \i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" by metis @@ -985,7 +985,7 @@ ultimately have "(\i. f' (\i. A i) - f' (A i)) ----> 0" by (simp add: zero_ereal_def) then have "(\i. f' (A i)) ----> f' (\i. A i)" - by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const]) + by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const]) then show "(\i. f (A i)) ----> f (\i. A i)" using A by (subst (1 2) f') auto qed diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Sun Aug 28 09:20:12 2011 -0700 @@ -2191,9 +2191,9 @@ have 3: "\x n. 0 \ f n x - f 0 x" using `mono f` unfolding mono_def le_fun_def by (auto simp: field_simps) have 4: "\x. (\i. f i x - f 0 x) ----> u x - f 0 x" - using lim by (auto intro!: LIMSEQ_diff) + using lim by (auto intro!: tendsto_diff) have 5: "(\i. (\x. f i x - f 0 x \M)) ----> x - integral\<^isup>L M (f 0)" - using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff) + using f ilim by (auto intro!: tendsto_diff simp: integral_diff) note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5] have "integrable M (\x. (u x - f 0 x) + f 0 x)" using diff(1) f by (rule integral_add(1)) @@ -2329,7 +2329,7 @@ and "(\i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim) proof - { fix x j assume x: "x \ space M" - from u'[OF x] have "(\i. \u i x\) ----> \u' x\" by (rule LIMSEQ_imp_rabs) + from u'[OF x] have "(\i. \u i x\) ----> \u' x\" by (rule tendsto_rabs) from LIMSEQ_le_const2[OF this] have "\u' x\ \ w x" using bound[OF x] by auto } note u'_bound = this @@ -2400,7 +2400,7 @@ unfolding ereal_max_0 proof (rule lim_imp_Liminf[symmetric], unfold lim_ereal) have "(\i. ?diff i x) ----> 2 * w x - \u' x - u' x\" - using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs) + using u'[OF x] by (safe intro!: tendsto_intros) then show "(\i. max 0 (?diff i x)) ----> max 0 (2 * w x)" by (auto intro!: tendsto_real_max simp add: lim_ereal) qed (rule trivial_limit_sequentially) @@ -2492,7 +2492,7 @@ show "mono ?w'" by (auto simp: mono_def le_fun_def intro!: setsum_mono2) { fix x show "(\n. ?w' n x) ----> ?w x" - using w by (cases "x \ space M") (simp_all add: LIMSEQ_const sums_def) } + using w by (cases "x \ space M") (simp_all add: tendsto_const sums_def) } have *: "\n. integral\<^isup>L M (?w' n) = (\i = 0..< n. (\x. \f i x\ \M))" using borel by (simp add: integral_setsum integrable_abs cong: integral_cong) from abs_sum diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Aug 28 09:20:12 2011 -0700 @@ -209,7 +209,7 @@ from finite_continuity_from_below[OF _ A] `range A \ sets M` M'.finite_continuity_from_below[OF _ A] have convergent: "(\i. ?d (A i)) ----> ?d (\i. A i)" - by (auto intro!: LIMSEQ_diff) + by (auto intro!: tendsto_diff) obtain n :: nat where "- ?d (\i. A i) / e < real n" using reals_Archimedean2 by auto moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] have "real n \ - ?d (\i. A i) / e" using `0 sets M` A] M'.finite_continuity_from_above[OF `range A \ sets M` A] - have "(\i. ?d (A i)) ----> ?d (\i. A i)" by (intro LIMSEQ_diff) + have "(\i. ?d (A i)) ----> ?d (\i. A i)" by (intro tendsto_diff) thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] by (rule_tac LIMSEQ_le_const) (auto intro!: exI) next diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/SEQ.thy Sun Aug 28 09:20:12 2011 -0700 @@ -772,7 +772,7 @@ have X: "!!n. X n = X 0" by (blast intro: const [of 0]) have "X = (\n. X 0)" - by (blast intro: ext X) + by (blast intro: X) hence "L = X 0" using tendsto_const [of "X 0" sequentially] by (auto intro: LIMSEQ_unique lim) thus ?thesis @@ -1144,25 +1144,4 @@ apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) done -subsection {* Legacy theorem names *} - -lemmas LIMSEQ_Zfun_iff = tendsto_Zfun_iff [where F=sequentially] -lemmas LIMSEQ_const = tendsto_const [where F=sequentially] -lemmas LIMSEQ_norm = tendsto_norm [where F=sequentially] -lemmas LIMSEQ_add = tendsto_add [where F=sequentially] -lemmas LIMSEQ_minus = tendsto_minus [where F=sequentially] -lemmas LIMSEQ_minus_cancel = tendsto_minus_cancel [where F=sequentially] -lemmas LIMSEQ_diff = tendsto_diff [where F=sequentially] -lemmas (in bounded_linear) LIMSEQ = tendsto [where F=sequentially] -lemmas (in bounded_bilinear) LIMSEQ = tendsto [where F=sequentially] -lemmas LIMSEQ_mult = tendsto_mult [where F=sequentially] -lemmas LIMSEQ_inverse = tendsto_inverse [where F=sequentially] -lemmas LIMSEQ_divide = tendsto_divide [where F=sequentially] -lemmas LIMSEQ_pow = tendsto_power [where F=sequentially] -lemmas LIMSEQ_setsum = tendsto_setsum [where F=sequentially] -lemmas LIMSEQ_setprod = tendsto_setprod [where F=sequentially] -lemmas LIMSEQ_norm_zero = tendsto_norm_zero_iff [where F=sequentially] -lemmas LIMSEQ_rabs_zero = tendsto_rabs_zero_iff [where F=sequentially] -lemmas LIMSEQ_imp_rabs = tendsto_rabs [where F=sequentially] - end diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Series.thy --- a/src/HOL/Series.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Series.thy Sun Aug 28 09:20:12 2011 -0700 @@ -183,12 +183,12 @@ unfolding sums_def apply (rule LIMSEQ_offset[of _ n]) unfolding setsum_const - apply (rule LIMSEQ_const) + apply (rule tendsto_const) done qed lemma sums_zero[simp, intro]: "(\n. 0) sums 0" -unfolding sums_def by (simp add: LIMSEQ_const) + unfolding sums_def by (simp add: tendsto_const) lemma summable_zero[simp, intro]: "summable (\n. 0)" by (rule sums_zero [THEN sums_summable]) @@ -198,7 +198,7 @@ lemma (in bounded_linear) sums: "(\n. X n) sums a \ (\n. f (X n)) sums (f a)" -unfolding sums_def by (drule LIMSEQ, simp only: setsum) + unfolding sums_def by (drule tendsto, simp only: setsum) lemma (in bounded_linear) summable: "summable (\n. X n) \ summable (\n. f (X n))" @@ -260,7 +260,7 @@ lemma sums_add: fixes a b :: "'a::real_normed_field" shows "\X sums a; Y sums b\ \ (\n. X n + Y n) sums (a + b)" -unfolding sums_def by (simp add: setsum_addf LIMSEQ_add) + unfolding sums_def by (simp add: setsum_addf tendsto_add) lemma summable_add: fixes X Y :: "nat \ 'a::real_normed_field" @@ -275,7 +275,7 @@ lemma sums_diff: fixes X Y :: "nat \ 'a::real_normed_field" shows "\X sums a; Y sums b\ \ (\n. X n - Y n) sums (a - b)" -unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff) + unfolding sums_def by (simp add: setsum_subtractf tendsto_diff) lemma summable_diff: fixes X Y :: "nat \ 'a::real_normed_field" @@ -290,7 +290,7 @@ lemma sums_minus: fixes X :: "nat \ 'a::real_normed_field" shows "X sums a ==> (\n. - X n) sums (- a)" -unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus) + unfolding sums_def by (simp add: setsum_negf tendsto_minus) lemma summable_minus: fixes X :: "nat \ 'a::real_normed_field" @@ -344,7 +344,7 @@ shows "\summable f; \m\n. 0 \ f m\ \ setsum f {0.. suminf f" apply (drule summable_sums) apply (simp add: sums_def) -apply (cut_tac k = "setsum f {0..n. x ^ n) ----> 0" by (rule LIMSEQ_power_zero) hence "(\n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)" - using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const) + using neq_0 by (intro tendsto_intros) hence "(\n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)" by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) thus "(\n. x ^ n) sums (1 / (1 - x))" @@ -583,7 +583,7 @@ lemma summable_norm: fixes f :: "nat \ 'a::banach" shows "summable (\n. norm (f n)) \ norm (suminf f) \ (\n. norm (f n))" -by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel + by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_sumr_LIMSEQ_suminf norm_setsum) lemma summable_rabs: @@ -692,7 +692,7 @@ have "(\n. (\k=0..k=0.. (\k. a k) * (\k. b k)" - by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf + by (intro tendsto_mult summable_sumr_LIMSEQ_suminf summable_norm_cancel [OF a] summable_norm_cancel [OF b]) hence 1: "(\n. setsum ?g (?S1 n)) ----> (\k. a k) * (\k. b k)" by (simp only: setsum_product setsum_Sigma [rule_format] @@ -700,7 +700,7 @@ have "(\n. (\k=0..k=0.. (\k. norm (a k)) * (\k. norm (b k))" - using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf) + using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf) hence "(\n. setsum ?f (?S1 n)) ----> (\k. norm (a k)) * (\k. norm (b k))" by (simp only: setsum_product setsum_Sigma [rule_format] finite_atLeastLessThan) diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Transcendental.thy Sun Aug 28 09:20:12 2011 -0700 @@ -294,7 +294,7 @@ hence ord: "\n m. m \ n \ ?a n \ ?a m" and ge0: "\ n. 0 \ ?a n" by auto { fix n have "?a (Suc n) \ ?a n" using ord[where n="Suc n" and m=n] by auto } note monotone = this - note leibniz = summable_Leibniz'[OF _ ge0, of "\x. x", OF LIMSEQ_minus[OF `a ----> 0`, unfolded minus_zero] monotone] + note leibniz = summable_Leibniz'[OF _ ge0, of "\x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone] have "summable (\ n. (-1)^n * ?a n)" using leibniz(1) by auto then obtain l where "(\ n. (-1)^n * ?a n) sums l" unfolding summable_def by auto from this[THEN sums_minus] @@ -308,7 +308,7 @@ have ?pos using `0 \ ?a 0` by auto moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto - moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN LIMSEQ_minus_cancel] by auto + moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] by auto ultimately show ?thesis by auto qed from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1] @@ -2582,21 +2582,21 @@ lemma zeroseq_arctan_series: fixes x :: real assumes "\x\ \ 1" shows "(\ n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0") -proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const) +proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: tendsto_const) next case False have "norm x \ 1" and "x \ 1" and "-1 \ x" using assms by auto show "?a ----> 0" proof (cases "\x\ < 1") case True hence "norm x < 1" by auto - from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]] + from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]] have "(\n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0" unfolding inverse_eq_divide Suc_eq_plus1 by simp then show ?thesis using pos2 by (rule LIMSEQ_linear) next case False hence "x = -1 \ x = 1" using `\x\ \ 1` by auto hence n_eq: "\ n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto - from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]] + from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]] show ?thesis unfolding n_eq Suc_eq_plus1 by auto qed qed @@ -2775,8 +2775,8 @@ hence "?diff 1 n \ ?a 1 n" by auto } have "?a 1 ----> 0" - unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def - by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat) + unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def + by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat) have "?diff 1 ----> 0" proof (rule LIMSEQ_I) fix r :: real assume "0 < r" @@ -2785,7 +2785,7 @@ have "norm (?diff 1 n - 0) < r" by auto } thus "\ N. \ n \ N. norm (?diff 1 n - 0) < r" by blast qed - from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus] + from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus] have "(?c 1) sums (arctan 1)" unfolding sums_def by auto hence "arctan 1 = (\ i. ?c 1 i)" by (rule sums_unique)