# HG changeset patch
# User huffman
# Date 1313333664 25200
# Node ID 0639898074ae54b3c683ad589dfd5ed5af239715
# Parent  013f7b14f6ff343e814e27e1f0af4769b6a95dd1
generalize lemmas about LIM and LIMSEQ to tendsto

diff -r 013f7b14f6ff -r 0639898074ae src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Sat Aug 13 18:10:14 2011 -0700
+++ b/src/HOL/Lim.thy	Sun Aug 14 07:54:24 2011 -0700
@@ -95,7 +95,7 @@
 lemma LIM_add_zero:
   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
-by (drule (1) LIM_add, simp)
+  by (rule tendsto_add_zero)
 
 lemma LIM_minus:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -170,16 +170,16 @@
 by (rule tendsto_norm_zero_iff)
 
 lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
-by (fold real_norm_def, rule LIM_norm)
+  by (rule tendsto_rabs)
 
 lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0"
-by (fold real_norm_def, rule LIM_norm_zero)
+  by (rule tendsto_rabs_zero)
 
 lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0"
-by (fold real_norm_def, rule LIM_norm_zero_cancel)
+  by (rule tendsto_rabs_zero_cancel)
 
 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
-by (fold real_norm_def, rule LIM_norm_zero_iff)
+  by (rule tendsto_rabs_zero_iff)
 
 lemma at_neq_bot:
   fixes a :: "'a::real_normed_algebra_1"
@@ -345,7 +345,7 @@
 
 lemma (in bounded_linear) LIM_zero:
   "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
-by (drule LIM, simp only: zero)
+  by (rule tendsto_zero)
 
 text {* Bounded Bilinear Operators *}
 
@@ -358,15 +358,15 @@
   assumes f: "f -- a --> 0"
   assumes g: "g -- a --> 0"
   shows "(\<lambda>x. f x ** g x) -- a --> 0"
-using LIM [OF f g] by (simp add: zero_left)
+  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 bounded_linear.LIM_zero [OF bounded_linear_left])
+  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 bounded_linear.LIM_zero [OF bounded_linear_right])
+  by (rule tendsto_right_zero)
 
 lemmas LIM_mult = mult.LIM
 
@@ -384,7 +384,7 @@
   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
-by (induct n, simp, simp add: LIM_mult f)
+  using assms by (rule tendsto_power)
 
 subsubsection {* Derived theorems about @{term LIM} *}
 
@@ -401,8 +401,7 @@
 lemma LIM_sgn:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
-unfolding sgn_div_norm
-by (simp add: LIM_scaleR LIM_inverse LIM_norm)
+  by (rule tendsto_sgn)
 
 
 subsection {* Continuity *}
@@ -511,11 +510,7 @@
   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   fixes A :: "'a set" assumes "finite A"
   shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
-  using `finite A`
-proof induct
-  case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" 
-    unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert)
-qed auto
+  unfolding isCont_def by (simp add: tendsto_setsum)
 
 lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
diff -r 013f7b14f6ff -r 0639898074ae src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat Aug 13 18:10:14 2011 -0700
+++ b/src/HOL/Limits.thy	Sun Aug 14 07:54:24 2011 -0700
@@ -623,6 +623,8 @@
   qed
 qed
 
+subsubsection {* Norms *}
+
 lemma norm_conv_dist: "norm x = dist x 0"
   unfolding dist_norm by simp
 
@@ -642,11 +644,34 @@
   "((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A"
   unfolding tendsto_iff dist_norm by simp
 
+lemma tendsto_rabs [tendsto_intros]:
+  "(f ---> (l::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) A"
+  by (fold real_norm_def, rule tendsto_norm)
+
+lemma tendsto_rabs_zero:
+  "(f ---> (0::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) A"
+  by (fold real_norm_def, rule tendsto_norm_zero)
+
+lemma tendsto_rabs_zero_cancel:
+  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<Longrightarrow> (f ---> 0) A"
+  by (fold real_norm_def, rule tendsto_norm_zero_cancel)
+
+lemma tendsto_rabs_zero_iff:
+  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<longleftrightarrow> (f ---> 0) A"
+  by (fold real_norm_def, rule tendsto_norm_zero_iff)
+
+subsubsection {* Addition and subtraction *}
+
 lemma tendsto_add [tendsto_intros]:
   fixes a b :: "'a::real_normed_vector"
   shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A"
   by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
 
+lemma tendsto_add_zero:
+  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+  shows "\<lbrakk>(f ---> 0) A; (g ---> 0) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) A"
+  by (drule (1) tendsto_add, simp)
+
 lemma tendsto_minus [tendsto_intros]:
   fixes a :: "'a::real_normed_vector"
   shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A"
@@ -668,29 +693,61 @@
   shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A"
 proof (cases "finite S")
   assume "finite S" thus ?thesis using assms
-  proof (induct set: finite)
-    case empty show ?case
-      by (simp add: tendsto_const)
-  next
-    case (insert i F) thus ?case
-      by (simp add: tendsto_add)
-  qed
+    by (induct, simp add: tendsto_const, simp add: tendsto_add)
 next
   assume "\<not> finite S" thus ?thesis
     by (simp add: tendsto_const)
 qed
 
+subsubsection {* Linear operators and multiplication *}
+
 lemma (in bounded_linear) tendsto [tendsto_intros]:
   "(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A"
   by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
 
+lemma (in bounded_linear) tendsto_zero:
+  "(g ---> 0) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) A"
+  by (drule tendsto, simp only: zero)
+
 lemma (in bounded_bilinear) tendsto [tendsto_intros]:
   "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A"
   by (simp only: tendsto_Zfun_iff prod_diff_prod
                  Zfun_add Zfun Zfun_left Zfun_right)
 
+lemma (in bounded_bilinear) tendsto_zero:
+  assumes f: "(f ---> 0) A"
+  assumes g: "(g ---> 0) A"
+  shows "((\<lambda>x. f x ** g x) ---> 0) A"
+  using tendsto [OF f g] by (simp add: zero_left)
 
-subsection {* Continuity of Inverse *}
+lemma (in bounded_bilinear) tendsto_left_zero:
+  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. f x ** c) ---> 0) A"
+  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])
+
+lemma (in bounded_bilinear) tendsto_right_zero:
+  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) A"
+  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
+
+lemmas tendsto_mult = mult.tendsto
+
+lemma tendsto_power [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
+  shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) A"
+  by (induct n) (simp_all add: tendsto_const tendsto_mult)
+
+lemma tendsto_setprod [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) A"
+  shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) A"
+proof (cases "finite S")
+  assume "finite S" thus ?thesis using assms
+    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
+next
+  assume "\<not> finite S" thus ?thesis
+    by (simp add: tendsto_const)
+qed
+
+subsubsection {* Inverse and division *}
 
 lemma (in bounded_bilinear) Zfun_prod_Bfun:
   assumes f: "Zfun f A"
@@ -815,6 +872,13 @@
     \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A"
   by (simp add: mult.tendsto tendsto_inverse divide_inverse)
 
+lemma tendsto_sgn [tendsto_intros]:
+  fixes l :: "'a::real_normed_vector"
+  shows "\<lbrakk>(f ---> l) A; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) A"
+  unfolding sgn_div_norm by (simp add: tendsto_intros)
+
+subsubsection {* Uniqueness *}
+
 lemma tendsto_unique:
   fixes f :: "'a \<Rightarrow> 'b::t2_space"
   assumes "\<not> trivial_limit A"  "(f ---> l) A"  "(f ---> l') A"
diff -r 013f7b14f6ff -r 0639898074ae src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sat Aug 13 18:10:14 2011 -0700
+++ b/src/HOL/SEQ.thy	Sun Aug 14 07:54:24 2011 -0700
@@ -441,7 +441,7 @@
 lemma LIMSEQ_pow:
   fixes a :: "'a::{power, real_normed_algebra}"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
-by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
+  by (rule tendsto_power)
 
 lemma LIMSEQ_setsum:
   fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -453,23 +453,7 @@
   fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
-proof (cases "finite S")
-  case True
-  thus ?thesis using n
-  proof (induct)
-    case empty
-    show ?case
-      by (simp add: LIMSEQ_const)
-  next
-    case insert
-    thus ?case
-      by (simp add: LIMSEQ_mult)
-  qed
-next
-  case False
-  thus ?thesis
-    by (simp add: setprod_def LIMSEQ_const)
-qed
+  using assms by (rule tendsto_setprod)
 
 lemma LIMSEQ_add_const: (* FIXME: delete *)
   fixes a :: "'a::real_normed_vector"
@@ -501,13 +485,13 @@
 lemma LIMSEQ_norm_zero:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
-by (simp add: LIMSEQ_iff)
+  by (rule tendsto_norm_zero_iff)
 
 lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
-by (simp add: LIMSEQ_iff)
+  by (rule tendsto_rabs_zero_iff)
 
 lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
-by (drule LIMSEQ_norm, simp)
+  by (rule tendsto_rabs)
 
 text{*An unbounded sequence's inverse tends to 0*}