author huffman Tue Aug 09 10:30:00 2011 -0700 (2011-08-09) changeset 44125 230a8665c919 parent 44124 4c2a61a897d8 child 44126 ce44e70d0c47
mark some redundant theorems as legacy
```     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.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.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.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.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.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.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