mark some redundant theorems as legacy
authorhuffman
Tue Aug 09 10:30:00 2011 -0700 (2011-08-09)
changeset 44125230a8665c919
parent 44124 4c2a61a897d8
child 44126 ce44e70d0c47
mark some redundant theorems as legacy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 09 08:53:12 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 09 10:30:00 2011 -0700
     1.3 @@ -3054,7 +3054,7 @@
     1.4    apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
     1.5    apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
     1.6    apply(rule assms[unfolded convex_def, rule_format]) prefer 6
     1.7 -  apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto
     1.8 +  by (auto intro: tendsto_intros)
     1.9  
    1.10  lemma convex_interior:
    1.11    fixes s :: "'a::real_normed_vector set"
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 09 08:53:12 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 09 10:30:00 2011 -0700
     2.3 @@ -137,13 +137,14 @@
     2.4  
     2.5  lemma (in bounded_linear) has_derivative: "(f has_derivative f) net"
     2.6    unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
     2.7 -  unfolding diff by(simp add: Lim_const)
     2.8 +  unfolding diff by (simp add: tendsto_const)
     2.9  
    2.10  lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
    2.11    apply(rule bounded_linear.has_derivative) using bounded_linear_ident[unfolded id_def] by simp
    2.12  
    2.13  lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
    2.14 -  unfolding has_derivative_def apply(rule,rule bounded_linear_zero) by(simp add: Lim_const)
    2.15 +  unfolding has_derivative_def
    2.16 +  by (rule, rule bounded_linear_zero, simp add: tendsto_const)
    2.17  
    2.18  lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
    2.19  proof -
    2.20 @@ -156,7 +157,8 @@
    2.21  
    2.22  lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
    2.23    unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
    2.24 -  using assms[unfolded has_derivative_def] using Lim_cmul[OF assms[unfolded has_derivative_def,THEN conjunct2]]
    2.25 +  using assms[unfolded has_derivative_def]
    2.26 +  using scaleR.tendsto[OF tendsto_const assms[unfolded has_derivative_def,THEN conjunct2]]
    2.27    unfolding scaleR_right_diff_distrib scaleR_right_distrib by auto 
    2.28  
    2.29  lemma has_derivative_cmul_eq: assumes "c \<noteq> 0" 
    2.30 @@ -177,7 +179,7 @@
    2.31  proof-
    2.32    note as = assms[unfolded has_derivative_def]
    2.33    show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
    2.34 -    using Lim_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
    2.35 +    using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
    2.36      by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib)
    2.37  qed
    2.38  
    2.39 @@ -224,7 +226,8 @@
    2.40      apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
    2.41      apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
    2.42      apply (rule derivative_linear [OF assms])
    2.43 -    apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR apply(rule Lim_vmul)
    2.44 +    apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR
    2.45 +    apply (intro tendsto_intros)
    2.46      using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
    2.47      apply(rule,assumption,rule disjI2,rule,rule) proof-
    2.48      have *:"\<And>x. x - 0 = (x::'a)" by auto 
    2.49 @@ -368,7 +371,7 @@
    2.50      by(rule linear_continuous_within[OF f'[THEN conjunct1]])
    2.51    show ?thesis unfolding continuous_within
    2.52      using f'[THEN conjunct2, THEN Lim_mul_norm_within]
    2.53 -    apply- apply(drule Lim_add)
    2.54 +    apply- apply(drule tendsto_add)
    2.55      apply(rule **[unfolded continuous_within])
    2.56      unfolding Lim_within and dist_norm
    2.57      apply (rule, rule)
    2.58 @@ -618,7 +621,7 @@
    2.59      fix i assume i:"i<DIM('a)" def e \<equiv> "norm (f' (basis i) - f'' (basis i))"
    2.60      assume "f' (basis i) \<noteq> f'' (basis i)"
    2.61      hence "e>0" unfolding e_def by auto
    2.62 -    guess d using Lim_sub[OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this
    2.63 +    guess d using tendsto_diff [OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this
    2.64      guess c using assms(3)[rule_format,OF i d[THEN conjunct1]] .. note c=this
    2.65      have *:"norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R basis i)) = norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R basis i)) + f'' (c *\<^sub>R basis i)))"
    2.66        unfolding scaleR_right_distrib by auto
    2.67 @@ -1522,7 +1525,7 @@
    2.68        thus "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
    2.69          apply-
    2.70          apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
    2.71 -        apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption
    2.72 +        apply(rule tendsto_intros g[rule_format] as)+ by assumption
    2.73      qed
    2.74    qed
    2.75    show ?thesis unfolding has_derivative_within_alt apply(rule_tac x=g in exI)
    2.76 @@ -1559,12 +1562,12 @@
    2.77          apply(rule tendsto_unique[OF trivial_limit_sequentially])
    2.78          apply(rule lem3[rule_format])
    2.79          unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
    2.80 -        apply(rule Lim_cmul) by(rule lem3[rule_format])
    2.81 +        apply (intro tendsto_intros) by(rule lem3[rule_format])
    2.82        show "g' x (y + z) = g' x y + g' x z"
    2.83          apply(rule tendsto_unique[OF trivial_limit_sequentially])
    2.84          apply(rule lem3[rule_format])
    2.85          unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
    2.86 -        apply(rule Lim_add) by(rule lem3[rule_format])+
    2.87 +        apply(rule tendsto_add) by(rule lem3[rule_format])+
    2.88      qed
    2.89      show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
    2.90      proof(rule,rule) case goal1
    2.91 @@ -1613,7 +1616,7 @@
    2.92      apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
    2.93      apply(rule,rule)
    2.94      apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)  
    2.95 -    apply(rule `a\<in>s`) by(auto intro!: Lim_const)
    2.96 +    apply(rule `a\<in>s`) by(auto intro!: tendsto_const)
    2.97  qed auto
    2.98  
    2.99  lemma has_antiderivative_limit:
   2.100 @@ -1682,16 +1685,16 @@
   2.101      using assms by auto
   2.102    have "((\<lambda>y. f' (y - x)) ---> 0) (at x within s)"
   2.103      unfolding f'.zero[THEN sym]
   2.104 -    apply(rule Lim_linear[of "\<lambda>y. y - x" 0 "at x within s" f'])
   2.105 -    using Lim_sub[OF Lim_within_id Lim_const, of x x s]
   2.106 +    using bounded_linear.tendsto [of f' "\<lambda>y. y - x" 0 "at x within s"]
   2.107 +    using tendsto_diff [OF Lim_within_id tendsto_const, of x x s]
   2.108      unfolding id_def using assms(1) unfolding has_derivative_def by auto
   2.109    hence "((\<lambda>y. f x + f' (y - x)) ---> f x) (at x within s)"
   2.110 -    using Lim_add[OF Lim_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
   2.111 +    using tendsto_add[OF tendsto_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
   2.112      by auto
   2.113    ultimately
   2.114    have *:"((\<lambda>x'. h (f x + f' (x' - x)) ((1/(norm (x' - x))) *\<^sub>R (g x' - (g x + g' (x' - x))))
   2.115               + h ((1/ (norm (x' - x))) *\<^sub>R (f x' - (f x + f' (x' - x)))) (g x')) ---> h (f x) 0 + h 0 (g x)) (at x within s)"
   2.116 -    apply-apply(rule Lim_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
   2.117 +    apply-apply(rule tendsto_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
   2.118      using assms(1-2)  unfolding has_derivative_within by auto
   2.119    guess B using bounded_bilinear.pos_bounded[OF assms(3)] .. note B=this
   2.120    guess C using f'.pos_bounded .. note C=this
   2.121 @@ -1725,7 +1728,7 @@
   2.122      apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
   2.123      apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
   2.124      done
   2.125 -  thus ?thesis using Lim_add[OF * **] unfolding has_derivative_within 
   2.126 +  thus ?thesis using tendsto_add[OF * **] unfolding has_derivative_within 
   2.127      unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
   2.128       h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
   2.129      scaleR_right_diff_distrib h.zero_right h.zero_left
     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 09 08:53:12 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 09 10:30:00 2011 -0700
     3.3 @@ -248,7 +248,7 @@
     3.4      show "eventually (\<lambda>x. a * X x \<in> S) net"
     3.5        by (rule eventually_mono[OF _ *]) auto
     3.6    qed
     3.7 -qed auto
     3.8 +qed (auto intro: tendsto_const)
     3.9  
    3.10  lemma ereal_lim_uminus:
    3.11    fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
    3.12 @@ -460,12 +460,12 @@
    3.13    assumes inc: "incseq X" and lim: "X ----> L"
    3.14    shows "X N \<le> L"
    3.15    using inc
    3.16 -  by (intro ereal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def)
    3.17 +  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
    3.18  
    3.19  lemma decseq_ge_ereal: assumes dec: "decseq X"
    3.20    and lim: "X ----> (L::ereal)" shows "X N >= L"
    3.21    using dec
    3.22 -  by (intro ereal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def)
    3.23 +  by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
    3.24  
    3.25  lemma liminf_bounded_open:
    3.26    fixes x :: "nat \<Rightarrow> ereal"
    3.27 @@ -519,7 +519,7 @@
    3.28  lemma lim_ereal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
    3.29    obtains l where "f ----> (l::ereal)"
    3.30  proof(cases "f = (\<lambda>x. - \<infinity>)")
    3.31 -  case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
    3.32 +  case True then show thesis using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
    3.33  next
    3.34    case False
    3.35    from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
    3.36 @@ -1138,7 +1138,7 @@
    3.37        by (induct i) (insert assms, auto) }
    3.38    note this[simp]
    3.39    show ?thesis unfolding sums_def
    3.40 -    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan)
    3.41 +    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
    3.42  qed
    3.43  
    3.44  lemma suminf_finite:
    3.45 @@ -1298,4 +1298,4 @@
    3.46      apply (subst SUP_commute) ..
    3.47  qed
    3.48  
    3.49 -end
    3.50 \ No newline at end of file
    3.51 +end
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 09 08:53:12 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 09 10:30:00 2011 -0700
     4.3 @@ -4476,7 +4476,7 @@
     4.4    "bounded {integral {a..b} (f k) | k . k \<in> UNIV}"
     4.5    shows "g integrable_on {a..b} \<and> ((\<lambda>k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially"
     4.6  proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0"
     4.7 -  show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto
     4.8 +  show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using tendsto_const by auto
     4.9  next assume ab:"content {a..b} \<noteq> 0"
    4.10    have fg:"\<forall>x\<in>{a..b}. \<forall> k. (f k x) $$ 0 \<le> (g x) $$ 0"
    4.11    proof safe case goal1 note assms(3)[rule_format,OF this]
    4.12 @@ -4631,7 +4631,8 @@
    4.13      proof(rule monotone_convergence_interval,safe)
    4.14        case goal1 show ?case using int .
    4.15      next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
    4.16 -    next case goal3 thus ?case apply-apply(cases "x\<in>s") using assms(4) by auto
    4.17 +    next case goal3 thus ?case apply-apply(cases "x\<in>s")
    4.18 +        using assms(4) by (auto intro: tendsto_const)
    4.19      next case goal4 note * = integral_nonneg
    4.20        have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
    4.21          unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int])
    4.22 @@ -4681,13 +4682,13 @@
    4.23    proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto
    4.24    next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
    4.25    next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
    4.26 -  next case goal4 thus ?case apply-apply(rule Lim_sub) 
    4.27 -      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
    4.28 +  next case goal4 thus ?case apply-apply(rule tendsto_diff) 
    4.29 +      using seq_offset[OF assms(3)[rule_format],of x 1] by (auto intro: tendsto_const)
    4.30    next case goal5 thus ?case using assms(4) unfolding bounded_iff
    4.31        apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
    4.32        apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
    4.33        apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed
    4.34 -  note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]]
    4.35 +  note conjunctD2[OF this] note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
    4.36      integrable_add[OF this(1) assms(1)[rule_format,of 0]]
    4.37    thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
    4.38      using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
    4.39 @@ -4702,11 +4703,11 @@
    4.40      apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto
    4.41    have "(\<lambda>x. - g x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. - f k x))
    4.42      ---> integral s (\<lambda>x. - g x))  sequentially" apply(rule monotone_convergence_increasing)
    4.43 -    apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg)
    4.44 +    apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule tendsto_minus)
    4.45      apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto
    4.46    note * = conjunctD2[OF this]
    4.47    show ?thesis apply rule using integrable_neg[OF *(1)] defer
    4.48 -    using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
    4.49 +    using tendsto_minus[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
    4.50      unfolding integral_neg[OF *(1),THEN sym] by auto qed
    4.51  
    4.52  subsection {* absolute integrability (this is the same as Lebesgue integrability). *}
     5.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 09 08:53:12 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 09 10:30:00 2011 -0700
     5.3 @@ -1223,62 +1223,15 @@
     5.4    thus ?lhs unfolding islimpt_approachable by auto
     5.5  qed
     5.6  
     5.7 -text{* Basic arithmetical combining theorems for limits. *}
     5.8 -
     5.9 -lemma Lim_linear:
    5.10 -  assumes "(f ---> l) net" "bounded_linear h"
    5.11 -  shows "((\<lambda>x. h (f x)) ---> h l) net"
    5.12 -using `bounded_linear h` `(f ---> l) net`
    5.13 -by (rule bounded_linear.tendsto)
    5.14 -
    5.15 -lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
    5.16 -  unfolding tendsto_def Limits.eventually_at_topological by fast
    5.17 -
    5.18 -lemma Lim_const[intro]: "((\<lambda>x. a) ---> a) net" by (rule tendsto_const)
    5.19 -
    5.20 -lemma Lim_cmul[intro]:
    5.21 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.22 -  shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
    5.23 -  by (intro tendsto_intros)
    5.24 -
    5.25 -lemma Lim_neg:
    5.26 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.27 -  shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
    5.28 -  by (rule tendsto_minus)
    5.29 -
    5.30 -lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
    5.31 - "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
    5.32 -  by (rule tendsto_add)
    5.33 -
    5.34 -lemma Lim_sub:
    5.35 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.36 -  shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
    5.37 -  by (rule tendsto_diff)
    5.38 -
    5.39 -lemma Lim_mul:
    5.40 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.41 -  assumes "(c ---> d) net"  "(f ---> l) net"
    5.42 -  shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
    5.43 -  using assms by (rule scaleR.tendsto)
    5.44 -
    5.45 -lemma Lim_inv:
    5.46 +lemma Lim_inv: (* TODO: delete *)
    5.47    fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
    5.48    assumes "(f ---> l) A" and "l \<noteq> 0"
    5.49    shows "((inverse o f) ---> inverse l) A"
    5.50    unfolding o_def using assms by (rule tendsto_inverse)
    5.51  
    5.52 -lemma Lim_vmul:
    5.53 -  fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
    5.54 -  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
    5.55 -  by (intro tendsto_intros)
    5.56 -
    5.57  lemma Lim_null:
    5.58    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.59 -  shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
    5.60 -
    5.61 -lemma Lim_null_norm:
    5.62 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.63 -  shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. norm(f x)) ---> 0) net"
    5.64 +  shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"
    5.65    by (simp add: Lim dist_norm)
    5.66  
    5.67  lemma Lim_null_comparison:
    5.68 @@ -1297,15 +1250,10 @@
    5.69      using assms `e>0` unfolding tendsto_iff by auto
    5.70  qed
    5.71  
    5.72 -lemma Lim_component:
    5.73 +lemma Lim_component: (* TODO: rename and declare [tendsto_intros] *)
    5.74    fixes f :: "'a \<Rightarrow> ('a::euclidean_space)"
    5.75    shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $$i) ---> l$$i) net"
    5.76 -  unfolding tendsto_iff
    5.77 -  apply (clarify)
    5.78 -  apply (drule spec, drule (1) mp)
    5.79 -  apply (erule eventually_elim1)
    5.80 -  apply (erule le_less_trans [OF dist_nth_le])
    5.81 -  done
    5.82 +  unfolding euclidean_component_def by (intro tendsto_intros)
    5.83  
    5.84  lemma Lim_transform_bound:
    5.85    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.86 @@ -1422,8 +1370,6 @@
    5.87    unfolding tendsto_def Limits.eventually_within eventually_at_topological
    5.88    by auto
    5.89  
    5.90 -lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
    5.91 -
    5.92  lemma Lim_at_id: "(id ---> a) (at a)"
    5.93  apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
    5.94  
    5.95 @@ -1478,10 +1424,10 @@
    5.96  unfolding netlimit_def
    5.97  apply (rule some_equality)
    5.98  apply (rule Lim_at_within)
    5.99 -apply (rule Lim_ident_at)
   5.100 +apply (rule LIM_ident)
   5.101  apply (erule tendsto_unique [OF assms])
   5.102  apply (rule Lim_at_within)
   5.103 -apply (rule Lim_ident_at)
   5.104 +apply (rule LIM_ident)
   5.105  done
   5.106  
   5.107  lemma netlimit_at:
   5.108 @@ -1498,8 +1444,8 @@
   5.109    assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
   5.110    shows "(g ---> l) net"
   5.111  proof-
   5.112 -  from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\<lambda>x. f x - g x" 0 net f l] by auto
   5.113 -  thus "?thesis" using Lim_neg [of "\<lambda> x. - g x" "-l" net] by auto
   5.114 +  from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using tendsto_diff[of "\<lambda>x. f x - g x" 0 net f l] by auto
   5.115 +  thus "?thesis" using tendsto_minus [of "\<lambda> x. - g x" "-l" net] by auto
   5.116  qed
   5.117  
   5.118  lemma Lim_transform_eventually:
   5.119 @@ -1592,7 +1538,7 @@
   5.120  proof
   5.121    assume "?lhs" moreover
   5.122    { assume "l \<in> S"
   5.123 -    hence "?rhs" using Lim_const[of l sequentially] by auto
   5.124 +    hence "?rhs" using tendsto_const[of l sequentially] by auto
   5.125    } moreover
   5.126    { assume "l islimpt S"
   5.127      hence "?rhs" unfolding islimpt_sequential by auto
   5.128 @@ -2809,7 +2755,7 @@
   5.129          by (rule infinite_enumerate)
   5.130        then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = l" by auto
   5.131        hence "subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   5.132 -        unfolding o_def by (simp add: fr Lim_const)
   5.133 +        unfolding o_def by (simp add: fr tendsto_const)
   5.134        hence "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   5.135          by - (rule exI)
   5.136        from f have "\<forall>n. f (r n) \<in> s" by simp
   5.137 @@ -3597,7 +3543,7 @@
   5.138                      \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
   5.139  (* BH: maybe the previous lemma should replace this one? *)
   5.140  unfolding uniformly_continuous_on_sequentially'
   5.141 -unfolding dist_norm Lim_null_norm [symmetric] ..
   5.142 +unfolding dist_norm tendsto_norm_zero_iff ..
   5.143  
   5.144  text{* The usual transformation theorems. *}
   5.145  
   5.146 @@ -3628,34 +3574,34 @@
   5.147  text{* Combination results for pointwise continuity. *}
   5.148  
   5.149  lemma continuous_const: "continuous net (\<lambda>x. c)"
   5.150 -  by (auto simp add: continuous_def Lim_const)
   5.151 +  by (auto simp add: continuous_def tendsto_const)
   5.152  
   5.153  lemma continuous_cmul:
   5.154    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   5.155    shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
   5.156 -  by (auto simp add: continuous_def Lim_cmul)
   5.157 +  by (auto simp add: continuous_def intro: tendsto_intros)
   5.158  
   5.159  lemma continuous_neg:
   5.160    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   5.161    shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
   5.162 -  by (auto simp add: continuous_def Lim_neg)
   5.163 +  by (auto simp add: continuous_def tendsto_minus)
   5.164  
   5.165  lemma continuous_add:
   5.166    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   5.167    shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
   5.168 -  by (auto simp add: continuous_def Lim_add)
   5.169 +  by (auto simp add: continuous_def tendsto_add)
   5.170  
   5.171  lemma continuous_sub:
   5.172    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   5.173    shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
   5.174 -  by (auto simp add: continuous_def Lim_sub)
   5.175 +  by (auto simp add: continuous_def tendsto_diff)
   5.176  
   5.177  
   5.178  text{* Same thing for setwise continuity. *}
   5.179  
   5.180  lemma continuous_on_const:
   5.181   "continuous_on s (\<lambda>x. c)"
   5.182 -  unfolding continuous_on_def by auto
   5.183 +  unfolding continuous_on_def by (auto intro: tendsto_intros)
   5.184  
   5.185  lemma continuous_on_cmul:
   5.186    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   5.187 @@ -3692,11 +3638,11 @@
   5.188  proof-
   5.189    { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   5.190      hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
   5.191 -      using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   5.192 +      using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   5.193        unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   5.194    }
   5.195    thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   5.196 -    unfolding dist_norm Lim_null_norm [symmetric] by auto
   5.197 +    unfolding dist_norm tendsto_norm_zero_iff by auto
   5.198  qed
   5.199  
   5.200  lemma dist_minus:
   5.201 @@ -3718,10 +3664,10 @@
   5.202    {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   5.203                      "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
   5.204      hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
   5.205 -      using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
   5.206 +      using tendsto_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
   5.207      hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
   5.208    thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   5.209 -    unfolding dist_norm Lim_null_norm [symmetric] by auto
   5.210 +    unfolding dist_norm tendsto_norm_zero_iff by auto
   5.211  qed
   5.212  
   5.213  lemma uniformly_continuous_on_sub:
   5.214 @@ -3736,11 +3682,11 @@
   5.215  
   5.216  lemma continuous_within_id:
   5.217   "continuous (at a within s) (\<lambda>x. x)"
   5.218 -  unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at])
   5.219 +  unfolding continuous_within by (rule Lim_at_within [OF LIM_ident])
   5.220  
   5.221  lemma continuous_at_id:
   5.222   "continuous (at a) (\<lambda>x. x)"
   5.223 -  unfolding continuous_at by (rule Lim_ident_at)
   5.224 +  unfolding continuous_at by (rule LIM_ident)
   5.225  
   5.226  lemma continuous_on_id:
   5.227   "continuous_on s (\<lambda>x. x)"
   5.228 @@ -4103,7 +4049,7 @@
   5.229  lemma continuous_vmul:
   5.230    fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
   5.231    shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
   5.232 -  unfolding continuous_def using Lim_vmul[of c] by auto
   5.233 +  unfolding continuous_def by (intro tendsto_intros)
   5.234  
   5.235  lemma continuous_mul:
   5.236    fixes c :: "'a::metric_space \<Rightarrow> real"
   5.237 @@ -4434,7 +4380,7 @@
   5.238  proof (rule continuous_attains_sup [OF assms])
   5.239    { fix x assume "x\<in>s"
   5.240      have "(dist a ---> dist a x) (at x within s)"
   5.241 -      by (intro tendsto_dist tendsto_const Lim_at_within Lim_ident_at)
   5.242 +      by (intro tendsto_dist tendsto_const Lim_at_within LIM_ident)
   5.243    }
   5.244    thus "continuous_on s (dist a)"
   5.245      unfolding continuous_on ..
   5.246 @@ -4681,7 +4627,7 @@
   5.247      obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
   5.248        using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
   5.249      have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
   5.250 -      using Lim_sub[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
   5.251 +      using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
   5.252      hence "l - l' \<in> t"
   5.253        using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
   5.254        using f(3) by auto
   5.255 @@ -5126,8 +5072,8 @@
   5.256        hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   5.257          unfolding Lim_sequentially by(auto simp add: dist_norm)
   5.258        hence "(f ---> x) sequentially" unfolding f_def
   5.259 -        using Lim_add[OF Lim_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   5.260 -        using Lim_vmul[of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
   5.261 +        using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   5.262 +        using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
   5.263      ultimately have "x \<in> closure {a<..<b}"
   5.264        using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto  }
   5.265    thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
   5.266 @@ -6157,4 +6103,18 @@
   5.267  (** TODO move this someplace else within this theory **)
   5.268  instance euclidean_space \<subseteq> banach ..
   5.269  
   5.270 +text {* Legacy theorem names *}
   5.271 +
   5.272 +lemmas Lim_ident_at = LIM_ident
   5.273 +lemmas Lim_const = tendsto_const
   5.274 +lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
   5.275 +lemmas Lim_neg = tendsto_minus
   5.276 +lemmas Lim_add = tendsto_add
   5.277 +lemmas Lim_sub = tendsto_diff
   5.278 +lemmas Lim_mul = scaleR.tendsto
   5.279 +lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
   5.280 +lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
   5.281 +lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
   5.282 +lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
   5.283 +
   5.284  end