discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
--- 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 ***
--- 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 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
{ fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
proof (rule mult_mono)
--- 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 (\<lambda>x. k) x :> 0"
-by (simp add: deriv_def)
+ by (simp add: deriv_def tendsto_const)
lemma DERIV_ident [simp]: "DERIV (\<lambda>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:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>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 \<Longrightarrow> DERIV (\<lambda>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:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
@@ -64,7 +64,7 @@
hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
by (rule DERIV_D)
hence "(\<lambda>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 "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
by simp
hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
@@ -90,7 +90,7 @@
hence "(\<lambda>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 "(\<lambda>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 "(\<lambda>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 "(\<lambda>z. d (f z)) -- x --> d (f x)"
- by (rule isCont_LIM_compose)
+ by (rule isCont_tendsto_compose)
hence "(\<lambda>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 "(\<lambda>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 \<Rightarrow> '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 @@
((\<forall>n. l \<le> 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 \<le> 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 "(\<lambda>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
--- 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 (\<lambda>x. k) x :> (\<lambda>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 (\<lambda>x. x)"
by (rule bounded_linear_intro [where K=1], simp_all)
lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>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 "(\<lambda>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 "(\<lambda>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 "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
by (rule FDERIV_D [OF f])
hence "(\<lambda>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 "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
by (simp cong: LIM_cong)
hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
- by (rule LIM_norm_zero_cancel)
+ by (rule tendsto_norm_zero_cancel)
hence "(\<lambda>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 "(\<lambda>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 "(\<lambda>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 "(\<lambda>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 "(\<lambda>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
--- 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)
--- 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) \<le> norm (f x - 0)" .
qed
-text {* Bounded Linear Operators *}
-
-lemma (in bounded_linear) LIM:
- "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
-by (rule tendsto)
-
-lemma (in bounded_linear) LIM_zero:
- "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
- by (rule tendsto_zero)
-
-text {* Bounded Bilinear Operators *}
-
-lemma (in bounded_bilinear) LIM:
- "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>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 "(\<lambda>x. f x ** g x) -- a --> 0"
- using f g by (rule tendsto_zero)
-
-lemma (in bounded_bilinear) LIM_left_zero:
- "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
- by (rule tendsto_left_zero)
-
-lemma (in bounded_bilinear) LIM_right_zero:
- "f -- a --> 0 \<Longrightarrow> (\<lambda>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 \<noteq> (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
--- 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 \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
--- 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)"
--- 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) (\<lambda>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) (\<lambda>x. x)"
- unfolding continuous_at by (rule LIM_ident)
+ unfolding continuous_at by (rule tendsto_ident_at)
lemma continuous_on_id:
"continuous_on s (\<lambda>x. x)"
@@ -4260,7 +4260,7 @@
proof (rule continuous_attains_sup [OF assms])
{ fix x assume "x\<in>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 ..
--- 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: "((\<lambda>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. \<bar>f n\<bar>) ----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. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
--- 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 "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
by metis
@@ -985,7 +985,7 @@
ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
by (simp add: zero_ereal_def)
then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
- by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
+ by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
using A by (subst (1 2) f') auto
qed
--- 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: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
unfolding mono_def le_fun_def by (auto simp: field_simps)
have 4: "\<And>x. (\<lambda>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: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>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 (\<lambda>x. (u x - f 0 x) + f 0 x)"
using diff(1) f by (rule integral_add(1))
@@ -2329,7 +2329,7 @@
and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
proof -
{ fix x j assume x: "x \<in> space M"
- from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
+ from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule tendsto_rabs)
from LIMSEQ_le_const2[OF this]
have "\<bar>u' x\<bar> \<le> 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 "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
- 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 "(\<lambda>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 "(\<lambda>n. ?w' n x) ----> ?w x"
- using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
+ using w by (cases "x \<in> space M") (simp_all add: tendsto_const sums_def) }
have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
from abs_sum
--- 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 \<subseteq> sets M`
M'.finite_continuity_from_below[OF _ A]
have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
- by (auto intro!: LIMSEQ_diff)
+ by (auto intro!: tendsto_diff)
obtain n :: nat where "- ?d (\<Union>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 \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
@@ -295,7 +295,7 @@
from
finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
M'.finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
- have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro LIMSEQ_diff)
+ have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro tendsto_diff)
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
next
--- 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 = (\<lambda>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
--- 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]: "(\<lambda>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 (\<lambda>n. 0)"
by (rule sums_zero [THEN sums_summable])
@@ -198,7 +198,7 @@
lemma (in bounded_linear) sums:
"(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>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 (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
@@ -260,7 +260,7 @@
lemma sums_add:
fixes a b :: "'a::real_normed_field"
shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>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 \<Rightarrow> 'a::real_normed_field"
@@ -275,7 +275,7 @@
lemma sums_diff:
fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>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 \<Rightarrow> 'a::real_normed_field"
@@ -290,7 +290,7 @@
lemma sums_minus:
fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
shows "X sums a ==> (\<lambda>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 \<Rightarrow> 'a::real_normed_field"
@@ -344,7 +344,7 @@
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
apply (drule summable_sums)
apply (simp add: sums_def)
-apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
+apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
apply (erule LIMSEQ_le, blast)
apply (rule_tac x="n" in exI, clarify)
apply (rule setsum_mono2)
@@ -403,7 +403,7 @@
from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
by (rule LIMSEQ_power_zero)
hence "(\<lambda>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 "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
@@ -583,7 +583,7 @@
lemma summable_norm:
fixes f :: "nat \<Rightarrow> 'a::banach"
shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>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 "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k))
----> (\<Sum>k. a k) * (\<Sum>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: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (simp only: setsum_product setsum_Sigma [rule_format]
@@ -700,7 +700,7 @@
have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k)))
----> (\<Sum>k. norm (a k)) * (\<Sum>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 "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
by (simp only: setsum_product setsum_Sigma [rule_format]
finite_atLeastLessThan)
--- 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: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto
{ fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto }
note monotone = this
- note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF LIMSEQ_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
+ note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
have "summable (\<lambda> n. (-1)^n * ?a n)" using leibniz(1) by auto
then obtain l where "(\<lambda> 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 \<le> ?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 "\<bar>x\<bar> \<le> 1" shows "(\<lambda> 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 \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
show "?a ----> 0"
proof (cases "\<bar>x\<bar> < 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 "(\<lambda>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 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
hence n_eq: "\<And> 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 \<le> ?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 "\<exists> N. \<forall> n \<ge> 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 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)