1.1 --- a/src/HOL/Lim.thy	Sat Aug 13 18:10:14 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 14 07:54:24 2011 -0700
     1.3 @@ -95,7 +95,7 @@
     1.4  lemma LIM_add_zero:
     1.5    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
     1.6    shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
     1.7 -by (drule (1) LIM_add, simp)
     1.8 +  by (rule tendsto_add_zero)
     1.9  
    1.10  lemma LIM_minus:
    1.11    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.12 @@ -170,16 +170,16 @@
    1.13  by (rule tendsto_norm_zero_iff)
    1.14  
    1.15  lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
    1.16 -by (fold real_norm_def, rule LIM_norm)
    1.17 +  by (rule tendsto_rabs)
    1.18  
    1.19  lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0"
    1.20 -by (fold real_norm_def, rule LIM_norm_zero)
    1.21 +  by (rule tendsto_rabs_zero)
    1.22  
    1.23  lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0"
    1.24 -by (fold real_norm_def, rule LIM_norm_zero_cancel)
    1.25 +  by (rule tendsto_rabs_zero_cancel)
    1.26  
    1.27  lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
    1.28 -by (fold real_norm_def, rule LIM_norm_zero_iff)
    1.29 +  by (rule tendsto_rabs_zero_iff)
    1.30  
    1.31  lemma at_neq_bot:
    1.32    fixes a :: "'a::real_normed_algebra_1"
    1.33 @@ -345,7 +345,7 @@
    1.34  
    1.35  lemma (in bounded_linear) LIM_zero:
    1.36    "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
    1.37 -by (drule LIM, simp only: zero)
    1.38 +  by (rule tendsto_zero)
    1.39  
    1.40  text {* Bounded Bilinear Operators *}
    1.41  
    1.42 @@ -358,15 +358,15 @@
    1.43    assumes f: "f -- a --> 0"
    1.44    assumes g: "g -- a --> 0"
    1.45    shows "(\<lambda>x. f x ** g x) -- a --> 0"
    1.46 -using LIM [OF f g] by (simp add: zero_left)
    1.47 +  using f g by (rule tendsto_zero)
    1.48  
    1.49  lemma (in bounded_bilinear) LIM_left_zero:
    1.50    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
    1.51 -by (rule bounded_linear.LIM_zero [OF bounded_linear_left])
    1.52 +  by (rule tendsto_left_zero)
    1.53  
    1.54  lemma (in bounded_bilinear) LIM_right_zero:
    1.55    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
    1.56 -by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
    1.57 +  by (rule tendsto_right_zero)
    1.58  
    1.59  lemmas LIM_mult = mult.LIM
    1.60  
    1.61 @@ -384,7 +384,7 @@
    1.62    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.63    assumes f: "f -- a --> l"
    1.64    shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
    1.65 -by (induct n, simp, simp add: LIM_mult f)
    1.66 +  using assms by (rule tendsto_power)
    1.67  
    1.68  subsubsection {* Derived theorems about @{term LIM} *}
    1.69  
    1.70 @@ -401,8 +401,7 @@
    1.71  lemma LIM_sgn:
    1.72    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.73    shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
    1.74 -unfolding sgn_div_norm
    1.75 -by (simp add: LIM_scaleR LIM_inverse LIM_norm)
    1.76 +  by (rule tendsto_sgn)
    1.77  
    1.78  
    1.79  subsection {* Continuity *}
    1.80 @@ -511,11 +510,7 @@
    1.81    fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
    1.82    fixes A :: "'a set" assumes "finite A"
    1.83    shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
    1.84 -  using `finite A`
    1.85 -proof induct
    1.86 -  case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" 
    1.87 -    unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert)
    1.88 -qed auto
    1.89 +  unfolding isCont_def by (simp add: tendsto_setsum)
    1.90  
    1.91  lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
    1.92    and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"

     2.1 --- a/src/HOL/Limits.thy	Sat Aug 13 18:10:14 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Sun Aug 14 07:54:24 2011 -0700
     2.3 @@ -623,6 +623,8 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +subsubsection {* Norms *}
     2.8 +
     2.9  lemma norm_conv_dist: "norm x = dist x 0"
    2.10    unfolding dist_norm by simp
    2.11  
    2.12 @@ -642,11 +644,34 @@
    2.13    "((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A"
    2.14    unfolding tendsto_iff dist_norm by simp
    2.15  
    2.16 +lemma tendsto_rabs [tendsto_intros]:
    2.17 +  "(f ---> (l::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) A"
    2.18 +  by (fold real_norm_def, rule tendsto_norm)
    2.19 +
    2.20 +lemma tendsto_rabs_zero:
    2.21 +  "(f ---> (0::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) A"
    2.22 +  by (fold real_norm_def, rule tendsto_norm_zero)
    2.23 +
    2.24 +lemma tendsto_rabs_zero_cancel:
    2.25 +  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<Longrightarrow> (f ---> 0) A"
    2.26 +  by (fold real_norm_def, rule tendsto_norm_zero_cancel)
    2.27 +
    2.28 +lemma tendsto_rabs_zero_iff:
    2.29 +  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<longleftrightarrow> (f ---> 0) A"
    2.30 +  by (fold real_norm_def, rule tendsto_norm_zero_iff)
    2.31 +
    2.32 +subsubsection {* Addition and subtraction *}
    2.33 +
    2.34  lemma tendsto_add [tendsto_intros]:
    2.35    fixes a b :: "'a::real_normed_vector"
    2.36    shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A"
    2.37    by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
    2.38  
    2.39 +lemma tendsto_add_zero:
    2.40 +  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
    2.41 +  shows "\<lbrakk>(f ---> 0) A; (g ---> 0) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) A"
    2.42 +  by (drule (1) tendsto_add, simp)
    2.43 +
    2.44  lemma tendsto_minus [tendsto_intros]:
    2.45    fixes a :: "'a::real_normed_vector"
    2.46    shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A"
    2.47 @@ -668,29 +693,61 @@
    2.48    shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A"
    2.49  proof (cases "finite S")
    2.50    assume "finite S" thus ?thesis using assms
    2.51 -  proof (induct set: finite)
    2.52 -    case empty show ?case
    2.53 -      by (simp add: tendsto_const)
    2.54 -  next
    2.55 -    case (insert i F) thus ?case
    2.56 -      by (simp add: tendsto_add)
    2.57 -  qed
    2.58 +    by (induct, simp add: tendsto_const, simp add: tendsto_add)
    2.59  next
    2.60    assume "\<not> finite S" thus ?thesis
    2.61      by (simp add: tendsto_const)
    2.62  qed
    2.63  
    2.64 +subsubsection {* Linear operators and multiplication *}
    2.65 +
    2.66  lemma (in bounded_linear) tendsto [tendsto_intros]:
    2.67    "(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A"
    2.68    by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
    2.69  
    2.70 +lemma (in bounded_linear) tendsto_zero:
    2.71 +  "(g ---> 0) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) A"
    2.72 +  by (drule tendsto, simp only: zero)
    2.73 +
    2.74  lemma (in bounded_bilinear) tendsto [tendsto_intros]:
    2.75    "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A"
    2.76    by (simp only: tendsto_Zfun_iff prod_diff_prod
    2.77                   Zfun_add Zfun Zfun_left Zfun_right)
    2.78  
    2.79 +lemma (in bounded_bilinear) tendsto_zero:
    2.80 +  assumes f: "(f ---> 0) A"
    2.81 +  assumes g: "(g ---> 0) A"
    2.82 +  shows "((\<lambda>x. f x ** g x) ---> 0) A"
    2.83 +  using tendsto [OF f g] by (simp add: zero_left)
    2.84  
    2.85 -subsection {* Continuity of Inverse *}
    2.86 +lemma (in bounded_bilinear) tendsto_left_zero:
    2.87 +  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. f x ** c) ---> 0) A"
    2.88 +  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])
    2.89 +
    2.90 +lemma (in bounded_bilinear) tendsto_right_zero:
    2.91 +  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) A"
    2.92 +  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
    2.93 +
    2.94 +lemmas tendsto_mult = mult.tendsto
    2.95 +
    2.96 +lemma tendsto_power [tendsto_intros]:
    2.97 +  fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    2.98 +  shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) A"
    2.99 +  by (induct n) (simp_all add: tendsto_const tendsto_mult)
   2.100 +
   2.101 +lemma tendsto_setprod [tendsto_intros]:
   2.102 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   2.103 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) A"
   2.104 +  shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) A"
   2.105 +proof (cases "finite S")
   2.106 +  assume "finite S" thus ?thesis using assms
   2.107 +    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
   2.108 +next
   2.109 +  assume "\<not> finite S" thus ?thesis
   2.110 +    by (simp add: tendsto_const)
   2.111 +qed
   2.112 +
   2.113 +subsubsection {* Inverse and division *}
   2.114  
   2.115  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   2.116    assumes f: "Zfun f A"
   2.117 @@ -815,6 +872,13 @@
   2.118      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A"
   2.119    by (simp add: mult.tendsto tendsto_inverse divide_inverse)
   2.120  
   2.121 +lemma tendsto_sgn [tendsto_intros]:
   2.122 +  fixes l :: "'a::real_normed_vector"
   2.123 +  shows "\<lbrakk>(f ---> l) A; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) A"
   2.124 +  unfolding sgn_div_norm by (simp add: tendsto_intros)
   2.125 +
   2.126 +subsubsection {* Uniqueness *}
   2.127 +
   2.128  lemma tendsto_unique:
   2.129    fixes f :: "'a \<Rightarrow> 'b::t2_space"
   2.130    assumes "\<not> trivial_limit A"  "(f ---> l) A"  "(f ---> l') A"

     3.1 --- a/src/HOL/SEQ.thy	Sat Aug 13 18:10:14 2011 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 07:54:24 2011 -0700
     3.3 @@ -441,7 +441,7 @@
     3.4  lemma LIMSEQ_pow:
     3.5    fixes a :: "'a::{power, real_normed_algebra}"
     3.6    shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
     3.7 -by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
     3.8 +  by (rule tendsto_power)
     3.9  
    3.10  lemma LIMSEQ_setsum:
    3.11    fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
    3.12 @@ -453,23 +453,7 @@
    3.13    fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
    3.14    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
    3.15    shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
    3.16 -proof (cases "finite S")
    3.17 -  case True
    3.18 -  thus ?thesis using n
    3.19 -  proof (induct)
    3.20 -    case empty
    3.21 -    show ?case
    3.22 -      by (simp add: LIMSEQ_const)
    3.23 -  next
    3.24 -    case insert
    3.25 -    thus ?case
    3.26 -      by (simp add: LIMSEQ_mult)
    3.27 -  qed
    3.28 -next
    3.29 -  case False
    3.30 -  thus ?thesis
    3.31 -    by (simp add: setprod_def LIMSEQ_const)
    3.32 -qed
    3.33 +  using assms by (rule tendsto_setprod)
    3.34  
    3.35  lemma LIMSEQ_add_const: (* FIXME: delete *)
    3.36    fixes a :: "'a::real_normed_vector"
    3.37 @@ -501,13 +485,13 @@
    3.38  lemma LIMSEQ_norm_zero:
    3.39    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    3.40    shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
    3.41 -by (simp add: LIMSEQ_iff)
    3.42 +  by (rule tendsto_norm_zero_iff)
    3.43  
    3.44  lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
    3.45 -by (simp add: LIMSEQ_iff)
    3.46 +  by (rule tendsto_rabs_zero_iff)
    3.47  
    3.48  lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
    3.49 -by (drule LIMSEQ_norm, simp)
    3.50 +  by (rule tendsto_rabs)
    3.51  
    3.52  text{*An unbounded sequence's inverse tends to 0*}
    3.53