--- 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"
--- 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"
--- 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*}