--- a/src/HOL/Library/Product_Vector.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Library/Product_Vector.thy Tue May 04 13:11:15 2010 -0700
@@ -312,30 +312,6 @@
(simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
-lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
-
-lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
-
-lemma LIMSEQ_Pair:
- assumes "X ----> a" and "Y ----> b"
- shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
-lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
-unfolding LIM_conv_tendsto by (rule tendsto_fst)
-
-lemma LIM_snd: "f -- x --> a \<Longrightarrow> (\<lambda>x. snd (f x)) -- x --> snd a"
-unfolding LIM_conv_tendsto by (rule tendsto_snd)
-
-lemma LIM_Pair:
- assumes "f -- x --> a" and "g -- x --> b"
- shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
-using assms unfolding LIM_conv_tendsto
-by (rule tendsto_Pair)
-
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
@@ -360,7 +336,7 @@
lemma isCont_Pair [simp]:
"\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
- unfolding isCont_def by (rule LIM_Pair)
+ unfolding isCont_def by (rule tendsto_Pair)
subsection {* Product is a complete metric space *}
@@ -374,7 +350,7 @@
using Cauchy_snd [OF `Cauchy X`]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
- using LIMSEQ_Pair [OF 1 2] by simp
+ using tendsto_Pair [OF 1 2] by simp
then show "convergent X"
by (rule convergentI)
qed
--- a/src/HOL/Lim.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Lim.thy Tue May 04 13:11:15 2010 -0700
@@ -12,15 +12,13 @@
text{*Standard Definitions*}
-definition
- LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
+abbreviation
+ LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
- [code del]: "f -- a --> L =
- (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
- --> dist (f x) L < r)"
+ "f -- a --> L \<equiv> (f ---> L) (at a)"
definition
- isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
+ isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where
"isCont f a = (f -- a --> (f a))"
definition
@@ -29,8 +27,10 @@
subsection {* Limits of Functions *}
-lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
-unfolding LIM_def tendsto_iff eventually_at ..
+lemma LIM_def: "f -- a --> L =
+ (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
+ --> dist (f x) L < r)"
+unfolding tendsto_iff eventually_at ..
lemma metric_LIM_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
@@ -61,91 +61,87 @@
by (simp add: LIM_eq)
lemma LIM_offset:
- fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ fixes a :: "'a::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-unfolding LIM_def dist_norm
-apply clarify
-apply (drule_tac x="r" in spec, safe)
-apply (rule_tac x="s" in exI, safe)
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_at dist_norm)
+apply (clarify, rule_tac x=d in exI, safe)
apply (drule_tac x="x + k" in spec)
apply (simp add: algebra_simps)
done
lemma LIM_offset_zero:
- fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ fixes a :: "'a::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
lemma LIM_offset_zero_cancel:
- fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ fixes a :: "'a::real_normed_vector"
shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
by (drule_tac k="- a" in LIM_offset, simp)
lemma LIM_const [simp]: "(%x. k) -- x --> k"
-by (simp add: LIM_def)
+by (rule tendsto_const)
lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
lemma LIM_add:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
assumes f: "f -- a --> L" and g: "g -- a --> M"
shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
-using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
+using assms by (rule tendsto_add)
lemma LIM_add_zero:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ 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)
-lemma minus_diff_minus:
- fixes a b :: "'a::ab_group_add"
- shows "(- a) - (- b) = - (a - b)"
-by simp
-
lemma LIM_minus:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
-unfolding LIM_conv_tendsto by (rule tendsto_minus)
+by (rule tendsto_minus)
(* TODO: delete *)
lemma LIM_add_minus:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
by (intro LIM_add LIM_minus)
lemma LIM_diff:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
-unfolding LIM_conv_tendsto by (rule tendsto_diff)
+by (rule tendsto_diff)
lemma LIM_zero:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
-by (simp add: LIM_def dist_norm)
+unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_cancel:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
-by (simp add: LIM_def dist_norm)
+unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_iff:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
-by (simp add: LIM_def dist_norm)
+unfolding tendsto_iff dist_norm by simp
lemma metric_LIM_imp_LIM:
assumes f: "f -- a --> l"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
shows "g -- a --> m"
-apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe)
-apply (rule_tac x="s" in exI, safe)
-apply (drule_tac x="x" in spec, safe)
+apply (rule tendstoI, drule tendstoD [OF f])
+apply (simp add: eventually_at_topological, safe)
+apply (rule_tac x="S" in exI, safe)
+apply (drule_tac x="x" in bspec, safe)
apply (erule (1) order_le_less_trans [OF le])
done
lemma LIM_imp_LIM:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
assumes f: "f -- a --> l"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
shows "g -- a --> m"
@@ -154,24 +150,24 @@
done
lemma LIM_norm:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
-unfolding LIM_conv_tendsto by (rule tendsto_norm)
+by (rule tendsto_norm)
lemma LIM_norm_zero:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
-by (drule LIM_norm, simp)
+by (rule tendsto_norm_zero)
lemma LIM_norm_zero_cancel:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
-by (erule LIM_imp_LIM, simp)
+by (rule tendsto_norm_zero_cancel)
lemma LIM_norm_zero_iff:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
-by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
+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)
@@ -185,78 +181,66 @@
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)
+lemma at_neq_bot:
+ fixes a :: "'a::real_normed_algebra_1"
+ shows "at a \<noteq> bot" -- {* TODO: find a more appropriate class *}
+unfolding eventually_False [symmetric]
+unfolding eventually_at dist_norm
+by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
+
lemma LIM_const_not_eq:
fixes a :: "'a::real_normed_algebra_1"
+ fixes k L :: "'b::metric_space"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
-apply (simp add: LIM_def)
-apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe)
-apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm)
-done
+by (simp add: tendsto_const_iff at_neq_bot)
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
lemma LIM_const_eq:
fixes a :: "'a::real_normed_algebra_1"
+ fixes k L :: "'b::metric_space"
shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
-apply (rule ccontr)
-apply (blast dest: LIM_const_not_eq)
-done
+by (simp add: tendsto_const_iff at_neq_bot)
lemma LIM_unique:
fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
+ fixes L M :: "'b::metric_space"
shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
-apply (rule ccontr)
-apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
-apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
-apply (clarify, rename_tac r s)
-apply (subgoal_tac "min r s \<noteq> 0")
-apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp)
-apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L +
- dist (f (a + of_real (min r s / 2))) M")
-apply (erule le_less_trans, rule add_strict_mono)
-apply (drule spec, erule mp, simp add: dist_norm)
-apply (drule spec, erule mp, simp add: dist_norm)
-apply (subst dist_commute, rule dist_triangle)
-apply simp
-done
+by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
-by (auto simp add: LIM_def)
+by (rule tendsto_ident_at)
text{*Limits are equal for functions equal except at limit point*}
lemma LIM_equal:
"[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
-by (simp add: LIM_def)
+unfolding tendsto_def eventually_at_topological by simp
lemma LIM_cong:
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
\<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
-by (simp add: LIM_def)
+by (simp add: LIM_equal)
lemma metric_LIM_equal2:
assumes 1: "0 < R"
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
shows "g -- a --> l \<Longrightarrow> f -- a --> l"
-apply (unfold LIM_def, safe)
-apply (drule_tac x="r" in spec, safe)
-apply (rule_tac x="min s R" in exI, safe)
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp add: eventually_at, safe)
+apply (rule_tac x="min d R" in exI, safe)
apply (simp add: 1)
apply (simp add: 2)
done
lemma LIM_equal2:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
assumes 1: "0 < R"
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
shows "g -- a --> l \<Longrightarrow> f -- a --> l"
-apply (unfold LIM_def dist_norm, safe)
-apply (drule_tac x="r" in spec, safe)
-apply (rule_tac x="min s R" in exI, safe)
-apply (simp add: 1)
-apply (simp add: 2)
-done
+by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
-text{*Two uses in Transcendental.ML*}
+text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *)
lemma LIM_trans:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l"
@@ -268,24 +252,52 @@
assumes g: "g -- l --> g l"
assumes f: "f -- a --> l"
shows "(\<lambda>x. g (f x)) -- a --> g l"
-proof (rule metric_LIM_I)
- fix r::real assume r: "0 < r"
- obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r"
- using metric_LIM_D [OF g r] by fast
- obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s"
- using metric_LIM_D [OF f s] by fast
+proof (rule topological_tendstoI)
+ fix C assume C: "open C" "g l \<in> C"
+ obtain B where B: "open B" "l \<in> B"
+ and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C"
+ using topological_tendstoD [OF g C]
+ unfolding eventually_at_topological by fast
+ obtain A where A: "open A" "a \<in> A"
+ and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
+ using topological_tendstoD [OF f B]
+ unfolding eventually_at_topological by fast
+ show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
+ unfolding eventually_at_topological
+ proof (intro exI conjI ballI impI)
+ show "open A" and "a \<in> A" using A .
+ next
+ fix x assume "x \<in> A" and "x \<noteq> a"
+ then show "g (f x) \<in> C"
+ by (cases "f x = l", simp add: C, simp add: gC fB)
+ qed
+qed
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r"
- proof (rule exI, safe)
- show "0 < t" using t .
+lemma LIM_compose_eventually:
+ assumes f: "f -- a --> b"
+ assumes g: "g -- b --> c"
+ assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
+ shows "(\<lambda>x. g (f x)) -- a --> c"
+proof (rule topological_tendstoI)
+ fix C assume C: "open C" "c \<in> C"
+ obtain B where B: "open B" "b \<in> B"
+ and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C"
+ using topological_tendstoD [OF g C]
+ unfolding eventually_at_topological by fast
+ obtain A where A: "open A" "a \<in> A"
+ and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
+ using topological_tendstoD [OF f B]
+ unfolding eventually_at_topological by fast
+ have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)"
+ unfolding eventually_at_topological
+ proof (intro exI conjI ballI impI)
+ show "open A" and "a \<in> A" using A .
next
- fix x assume "x \<noteq> a" and "dist x a < t"
- hence "dist (f x) l < s" by (rule less_s)
- thus "dist (g (f x)) (g l) < r"
- using r less_r by (case_tac "f x = l", simp_all)
+ fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b"
+ then show "g (f x) \<in> C" by (simp add: gC fB)
qed
+ with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
+ by (rule eventually_rev_mp)
qed
lemma metric_LIM_compose2:
@@ -293,31 +305,8 @@
assumes g: "g -- b --> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
shows "(\<lambda>x. g (f x)) -- a --> c"
-proof (rule metric_LIM_I)
- fix r :: real
- assume r: "0 < r"
- obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r"
- using metric_LIM_D [OF g r] by fast
- obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s"
- using metric_LIM_D [OF f s] by fast
- obtain d where d: "0 < d"
- and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
- using inj by fast
-
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r"
- proof (safe intro!: exI)
- show "0 < min d t" using d t by simp
- next
- fix x
- assume "x \<noteq> a" and "dist x a < min d t"
- hence "f x \<noteq> b" and "dist (f x) b < s"
- using neq_b less_s by simp_all
- thus "dist (g (f x)) c < r"
- by (rule less_r)
- qed
-qed
+using f g inj [folded eventually_at]
+by (rule LIM_compose_eventually)
lemma LIM_compose2:
fixes a :: "'a::real_normed_vector"
@@ -331,7 +320,7 @@
unfolding o_def by (rule LIM_compose)
lemma real_LIM_sandwich_zero:
- fixes f g :: "'a::metric_space \<Rightarrow> real"
+ fixes f g :: "'a::topological_space \<Rightarrow> real"
assumes f: "f -- a --> 0"
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
@@ -349,7 +338,7 @@
lemma (in bounded_linear) LIM:
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
-unfolding LIM_conv_tendsto by (rule tendsto)
+by (rule tendsto)
lemma (in bounded_linear) cont: "f -- a --> f a"
by (rule LIM [OF LIM_ident])
@@ -362,7 +351,7 @@
lemma (in bounded_bilinear) LIM:
"\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
-unfolding LIM_conv_tendsto by (rule tendsto)
+by (rule tendsto)
lemma (in bounded_bilinear) LIM_prod_zero:
fixes a :: "'d::metric_space"
@@ -402,7 +391,6 @@
lemma LIM_inverse:
fixes L :: "'a::real_normed_div_algebra"
shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
-unfolding LIM_conv_tendsto
by (rule tendsto_inverse)
lemma LIM_inverse_fun:
@@ -599,7 +587,7 @@
subsection {* Relation of LIM and LIMSEQ *}
lemma LIMSEQ_SEQ_conv1:
- fixes a :: "'a::metric_space"
+ fixes a :: "'a::metric_space" and L :: "'b::metric_space"
assumes X: "X -- a --> L"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
proof (safe intro!: metric_LIMSEQ_I)
@@ -620,7 +608,7 @@
lemma LIMSEQ_SEQ_conv2:
- fixes a :: real
+ fixes a :: real and L :: "'a::metric_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "X -- a --> L"
proof (rule ccontr)
@@ -688,7 +676,7 @@
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
- (X -- a --> L)"
+ (X -- a --> (L::'a::metric_space))"
proof
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
--- a/src/HOL/Limits.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Limits.thy Tue May 04 13:11:15 2010 -0700
@@ -241,23 +241,41 @@
unfolding expand_net_eq by (auto elim: eventually_rev_mp)
-subsection {* Standard Nets *}
+subsection {* Map function for nets *}
+
+definition
+ netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net"
+where [code del]:
+ "netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
+
+lemma eventually_netmap:
+ "eventually P (netmap f net) = eventually (\<lambda>x. P (f x)) net"
+unfolding netmap_def
+apply (rule eventually_Abs_net)
+apply (rule is_filter.intro)
+apply (auto elim!: eventually_rev_mp)
+done
+
+lemma netmap_ident: "netmap (\<lambda>x. x) net = net"
+by (simp add: expand_net_eq eventually_netmap)
+
+lemma netmap_netmap: "netmap f (netmap g net) = netmap (\<lambda>x. f (g x)) net"
+by (simp add: expand_net_eq eventually_netmap)
+
+lemma netmap_mono: "net \<le> net' \<Longrightarrow> netmap f net \<le> netmap f net'"
+unfolding le_net_def eventually_netmap by simp
+
+lemma netmap_bot [simp]: "netmap f bot = bot"
+by (simp add: expand_net_eq eventually_netmap)
+
+
+subsection {* Sequentially *}
definition
sequentially :: "nat net"
where [code del]:
"sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
-definition
- within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
-where [code del]:
- "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
-
-definition
- at :: "'a::topological_space \<Rightarrow> 'a net"
-where [code del]:
- "at a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-
lemma eventually_sequentially:
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
unfolding sequentially_def
@@ -269,6 +287,36 @@
then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
qed auto
+lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
+unfolding expand_net_eq eventually_sequentially by auto
+
+lemma eventually_False_sequentially [simp]:
+ "\<not> eventually (\<lambda>n. False) sequentially"
+by (simp add: eventually_False)
+
+lemma le_sequentially:
+ "net \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) net)"
+unfolding le_net_def eventually_sequentially
+by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
+
+
+subsection {* Standard Nets *}
+
+definition
+ within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
+where [code del]:
+ "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
+
+definition
+ nhds :: "'a::topological_space \<Rightarrow> 'a net"
+where [code del]:
+ "nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+
+definition
+ at :: "'a::topological_space \<Rightarrow> 'a net"
+where [code del]:
+ "at a = nhds a within - {a}"
+
lemma eventually_within:
"eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
unfolding within_def
@@ -278,28 +326,27 @@
lemma within_UNIV: "net within UNIV = net"
unfolding expand_net_eq eventually_within by simp
-lemma eventually_at_topological:
- "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-unfolding at_def
+lemma eventually_nhds:
+ "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+unfolding nhds_def
proof (rule eventually_Abs_net, rule is_filter.intro)
- have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. x \<noteq> a \<longrightarrow> True)" by simp
- thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> True)" by - rule
+ have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
+ thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by - rule
next
fix P Q
- assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
- and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)"
+ assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
+ and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
then obtain S T where
- "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
- "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)" by auto
- hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). x \<noteq> a \<longrightarrow> P x \<and> Q x)"
+ "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
+ "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
+ hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
by (simp add: open_Int)
- thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x \<and> Q x)" by - rule
+ thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by - rule
qed auto
-lemma eventually_at:
- fixes a :: "'a::metric_space"
- shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_at_topological open_dist
+lemma eventually_nhds_metric:
+ "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
+unfolding eventually_nhds open_dist
apply safe
apply fast
apply (rule_tac x="{x. dist x a < d}" in exI, simp)
@@ -309,6 +356,15 @@
apply (erule le_less_trans [OF dist_triangle])
done
+lemma eventually_at_topological:
+ "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+unfolding at_def eventually_within eventually_nhds by simp
+
+lemma eventually_at:
+ fixes a :: "'a::metric_space"
+ shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+unfolding at_def eventually_within eventually_nhds_metric by auto
+
subsection {* Boundedness *}
@@ -507,6 +563,9 @@
setup Tendsto_Intros.setup
+lemma tendsto_mono: "net \<le> net' \<Longrightarrow> (f ---> l) net' \<Longrightarrow> (f ---> l) net"
+unfolding tendsto_def le_net_def by fast
+
lemma topological_tendstoI:
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
\<Longrightarrow> (f ---> l) net"
@@ -548,12 +607,22 @@
unfolding tendsto_def eventually_at_topological by auto
lemma tendsto_ident_at_within [tendsto_intros]:
- "a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)"
+ "((\<lambda>x. x) ---> a) (at a within S)"
unfolding tendsto_def eventually_within eventually_at_topological by auto
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"
by (simp add: tendsto_def)
+lemma tendsto_const_iff:
+ fixes k l :: "'a::metric_space"
+ assumes "net \<noteq> bot" shows "((\<lambda>n. k) ---> l) net \<longleftrightarrow> k = l"
+apply (safe intro!: tendsto_const)
+apply (rule ccontr)
+apply (drule_tac e="dist k l" in tendstoD)
+apply (simp add: zero_less_dist_iff)
+apply (simp add: eventually_False assms)
+done
+
lemma tendsto_dist [tendsto_intros]:
assumes f: "(f ---> l) net" and g: "(g ---> m) net"
shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
@@ -574,13 +643,24 @@
qed
qed
+lemma norm_conv_dist: "norm x = dist x 0"
+unfolding dist_norm by simp
+
lemma tendsto_norm [tendsto_intros]:
"(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
-apply (simp add: tendsto_iff dist_norm, safe)
-apply (drule_tac x="e" in spec, safe)
-apply (erule eventually_elim1)
-apply (erule order_le_less_trans [OF norm_triangle_ineq3])
-done
+unfolding norm_conv_dist by (intro tendsto_intros)
+
+lemma tendsto_norm_zero:
+ "(f ---> 0) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) net"
+by (drule tendsto_norm, simp)
+
+lemma tendsto_norm_zero_cancel:
+ "((\<lambda>x. norm (f x)) ---> 0) net \<Longrightarrow> (f ---> 0) net"
+unfolding tendsto_iff dist_norm by simp
+
+lemma tendsto_norm_zero_iff:
+ "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
+unfolding tendsto_iff dist_norm by simp
lemma add_diff_add:
fixes a b c d :: "'a::ab_group_add"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue May 04 13:11:15 2010 -0700
@@ -313,23 +313,10 @@
end
-lemma LIMSEQ_Cart_nth:
- "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
-
-lemma LIM_Cart_nth:
- "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
-unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
-
lemma Cauchy_Cart_nth:
"Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])
-lemma LIMSEQ_vector:
- assumes "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
- shows "X ----> a"
-using assms unfolding LIMSEQ_conv_tendsto by (rule tendsto_vector)
-
lemma Cauchy_vector:
fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
@@ -371,7 +358,7 @@
using Cauchy_Cart_nth [OF `Cauchy X`]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
- by (simp add: LIMSEQ_vector)
+ by (simp add: tendsto_vector)
then show "convergent X"
by (rule convergentI)
qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 13:11:15 2010 -0700
@@ -2507,15 +2507,14 @@
ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
using `Cauchy f` unfolding complete_def by auto
then show "convergent f"
- unfolding convergent_def LIMSEQ_conv_tendsto [symmetric] by auto
+ unfolding convergent_def by auto
qed
lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
proof(simp add: complete_def, rule, rule)
fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
hence "convergent f" by (rule Cauchy_convergent)
- hence "\<exists>l. f ----> l" unfolding convergent_def .
- thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto .
+ thus "\<exists>l. f ----> l" unfolding convergent_def .
qed
lemma complete_imp_closed: assumes "complete s" shows "closed s"
@@ -5336,7 +5335,7 @@
unfolding dist_norm
apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
unfolding continuous_on
- by (intro ballI tendsto_intros, simp, assumption)+
+ by (intro ballI tendsto_intros, simp)+
next
have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto
show ?cth unfolding homeomorphic_minimal
@@ -5346,7 +5345,7 @@
unfolding dist_norm
apply (auto simp add: pos_divide_le_eq)
unfolding continuous_on
- by (intro ballI tendsto_intros, simp, assumption)+
+ by (intro ballI tendsto_intros, simp)+
qed
text{* "Isometry" (up to constant bounds) of injective linear map etc. *}
--- a/src/HOL/SEQ.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/SEQ.thy Tue May 04 13:11:15 2010 -0700
@@ -13,16 +13,10 @@
imports Limits
begin
-definition
- Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
- --{*Standard definition of sequence converging to zero*}
- [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
-
-definition
- LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
+abbreviation
+ LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
("((_)/ ----> (_))" [60, 60] 60) where
- --{*Standard definition of convergence of sequence*}
- [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+ "X ----> L \<equiv> (X ---> L) sequentially"
definition
lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
@@ -119,86 +113,13 @@
done
-subsection {* Sequences That Converge to Zero *}
-
-lemma ZseqI:
- "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X"
-unfolding Zseq_def by simp
-
-lemma ZseqD:
- "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r"
-unfolding Zseq_def by simp
-
-lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
-unfolding Zseq_def Zfun_def eventually_sequentially ..
-
-lemma Zseq_zero: "Zseq (\<lambda>n. 0)"
-unfolding Zseq_def by simp
-
-lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)"
-unfolding Zseq_def by force
-
-lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)"
-unfolding Zseq_def by simp
-
-lemma Zseq_imp_Zseq:
- assumes X: "Zseq X"
- assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
- shows "Zseq (\<lambda>n. Y n)"
-using X Y Zfun_imp_Zfun [of X sequentially Y K]
-unfolding Zseq_conv_Zfun by simp
-
-lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
-by (erule_tac K="1" in Zseq_imp_Zseq, simp)
-
-lemma Zseq_add:
- "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n + Y n)"
-unfolding Zseq_conv_Zfun by (rule Zfun_add)
-
-lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)"
-unfolding Zseq_def by simp
-
-lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n - Y n)"
-by (simp only: diff_minus Zseq_add Zseq_minus)
-
-lemma (in bounded_linear) Zseq:
- "Zseq X \<Longrightarrow> Zseq (\<lambda>n. f (X n))"
-unfolding Zseq_conv_Zfun by (rule Zfun)
-
-lemma (in bounded_bilinear) Zseq:
- "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
-unfolding Zseq_conv_Zfun by (rule Zfun)
-
-lemma (in bounded_bilinear) Zseq_prod_Bseq:
- "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
-unfolding Zseq_conv_Zfun Bseq_conv_Bfun
-by (rule Zfun_prod_Bfun)
-
-lemma (in bounded_bilinear) Bseq_prod_Zseq:
- "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
-unfolding Zseq_conv_Zfun Bseq_conv_Bfun
-by (rule Bfun_prod_Zfun)
-
-lemma (in bounded_bilinear) Zseq_left:
- "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
-by (rule bounded_linear_left [THEN bounded_linear.Zseq])
-
-lemma (in bounded_bilinear) Zseq_right:
- "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)"
-by (rule bounded_linear_right [THEN bounded_linear.Zseq])
-
-lemmas Zseq_mult = mult.Zseq
-lemmas Zseq_mult_right = mult.Zseq_right
-lemmas Zseq_mult_left = mult.Zseq_left
-
-
subsection {* Limits of Sequences *}
lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
by simp
-lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
-unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
+lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+unfolding tendsto_iff eventually_sequentially ..
lemma LIMSEQ_iff:
fixes L :: "'a::real_normed_vector"
@@ -206,10 +127,10 @@
unfolding LIMSEQ_def dist_norm ..
lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
- by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)
+ unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
-lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
-by (simp only: LIMSEQ_iff Zseq_def)
+lemma LIMSEQ_Zfun_iff: "((\<lambda>n. X n) ----> L) = Zfun (\<lambda>n. X n - L) sequentially"
+by (rule tendsto_Zfun_iff)
lemma metric_LIMSEQ_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
@@ -230,25 +151,23 @@
by (simp add: LIMSEQ_iff)
lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
-by (simp add: LIMSEQ_def)
+by (rule tendsto_const)
-lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
-apply (safe intro!: LIMSEQ_const)
-apply (rule ccontr)
-apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
-apply (simp add: zero_less_dist_iff)
-apply auto
-done
+lemma LIMSEQ_const_iff:
+ fixes k l :: "'a::metric_space"
+ shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
+by (rule tendsto_const_iff, rule sequentially_bot)
lemma LIMSEQ_norm:
fixes a :: "'a::real_normed_vector"
shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_norm)
+by (rule tendsto_norm)
lemma LIMSEQ_ignore_initial_segment:
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
-apply (rule metric_LIMSEQ_I)
-apply (drule (1) metric_LIMSEQ_D)
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_sequentially)
apply (erule exE, rename_tac N)
apply (rule_tac x=N in exI)
apply simp
@@ -256,8 +175,9 @@
lemma LIMSEQ_offset:
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
-apply (rule metric_LIMSEQ_I)
-apply (drule (1) metric_LIMSEQ_D)
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_sequentially)
apply (erule exE, rename_tac N)
apply (rule_tac x="N + k" in exI)
apply clarify
@@ -275,30 +195,32 @@
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
- unfolding LIMSEQ_def
+ unfolding tendsto_def eventually_sequentially
by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
lemma LIMSEQ_add:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_add)
+by (rule tendsto_add)
lemma LIMSEQ_minus:
fixes a :: "'a::real_normed_vector"
shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_minus)
+by (rule tendsto_minus)
lemma LIMSEQ_minus_cancel:
fixes a :: "'a::real_normed_vector"
shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
-by (drule LIMSEQ_minus, simp)
+by (rule tendsto_minus_cancel)
lemma LIMSEQ_diff:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_diff)
+by (rule tendsto_diff)
-lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
+lemma LIMSEQ_unique:
+ fixes a b :: "'a::metric_space"
+ shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
apply (rule ccontr)
apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
@@ -311,16 +233,16 @@
lemma (in bounded_linear) LIMSEQ:
"X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto)
+by (rule tendsto)
lemma (in bounded_bilinear) LIMSEQ:
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto)
+by (rule tendsto)
lemma LIMSEQ_mult:
fixes a b :: "'a::real_normed_algebra"
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
-by (rule mult.LIMSEQ)
+by (rule mult.tendsto)
lemma increasing_LIMSEQ:
fixes f :: "nat \<Rightarrow> real"
@@ -365,19 +287,17 @@
lemma Bseq_inverse:
fixes a :: "'a::real_normed_div_algebra"
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
-unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
-by (rule Bfun_inverse)
+unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
lemma LIMSEQ_inverse:
fixes a :: "'a::real_normed_div_algebra"
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
-unfolding LIMSEQ_conv_tendsto
by (rule tendsto_inverse)
lemma LIMSEQ_divide:
fixes a b :: "'a::real_normed_field"
shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b"
-by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
+by (rule tendsto_divide)
lemma LIMSEQ_pow:
fixes a :: "'a::{power, real_normed_algebra}"
@@ -388,7 +308,7 @@
fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
-using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
+using assms by (rule tendsto_setsum)
lemma LIMSEQ_setprod:
fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
@@ -412,21 +332,21 @@
by (simp add: setprod_def LIMSEQ_const)
qed
-lemma LIMSEQ_add_const:
+lemma LIMSEQ_add_const: (* FIXME: delete *)
fixes a :: "'a::real_normed_vector"
shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
-by (simp add: LIMSEQ_add LIMSEQ_const)
+by (intro tendsto_intros)
(* FIXME: delete *)
lemma LIMSEQ_add_minus:
fixes a b :: "'a::real_normed_vector"
shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
-by (simp only: LIMSEQ_add LIMSEQ_minus)
+by (intro tendsto_intros)
-lemma LIMSEQ_diff_const:
+lemma LIMSEQ_diff_const: (* FIXME: delete *)
fixes a b :: "'a::real_normed_vector"
shows "f ----> a ==> (%n.(f n - b)) ----> a - b"
-by (simp add: LIMSEQ_diff LIMSEQ_const)
+by (intro tendsto_intros)
lemma LIMSEQ_diff_approach_zero:
fixes L :: "'a::real_normed_vector"
@@ -833,9 +753,10 @@
lemma LIMSEQ_subseq_LIMSEQ:
"\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
-apply (auto simp add: LIMSEQ_def)
-apply (drule_tac x=r in spec, clarify)
-apply (rule_tac x=no in exI, clarify)
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_sequentially)
+apply (clarify, rule_tac x=N in exI, clarsimp)
apply (blast intro: seq_suble le_trans dest!: spec)
done
@@ -919,12 +840,8 @@
apply (blast dest: order_antisym)+
done
-text{* The best of both worlds: Easier to prove this result as a standard
- theorem and then use equivalence to "transfer" it into the
- equivalent nonstandard form if needed!*}
-
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
-apply (simp add: LIMSEQ_def)
+unfolding tendsto_def eventually_sequentially
apply (rule_tac x = "X m" in exI, safe)
apply (rule_tac x = m in exI, safe)
apply (drule spec, erule impE, auto)
@@ -1382,7 +1299,7 @@
fixes x :: "'a::{real_normed_algebra_1}"
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
-apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
+apply (simp only: LIMSEQ_Zfun_iff, erule Zfun_le)
apply (simp add: power_abs norm_power_ineq)
done
--- a/src/HOL/Series.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOL/Series.thy Tue May 04 13:11:15 2010 -0700
@@ -100,7 +100,7 @@
lemma summable_sums: "summable f ==> f sums (suminf f)"
apply (simp add: summable_def suminf_def sums_def)
-apply (blast intro: theI LIMSEQ_unique)
+apply (fast intro: theI LIMSEQ_unique)
done
lemma summable_sumr_LIMSEQ_suminf:
@@ -672,8 +672,8 @@
by (rule convergentI)
hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
by (rule convergent_Cauchy)
- have "Zseq (\<lambda>n. setsum ?f (?S1 n - ?S2 n))"
- proof (rule ZseqI, simp only: norm_setsum_f)
+ have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially"
+ proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)
fix r :: real
assume r: "0 < r"
from CauchyD [OF Cauchy r] obtain N
@@ -694,14 +694,15 @@
finally show "setsum ?f (?S1 n - ?S2 n) < r" .
qed
qed
- hence "Zseq (\<lambda>n. setsum ?g (?S1 n - ?S2 n))"
- apply (rule Zseq_le [rule_format])
+ hence "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
+ apply (rule Zfun_le [rule_format])
apply (simp only: norm_setsum_f)
apply (rule order_trans [OF norm_setsum setsum_mono])
apply (auto simp add: norm_mult_ineq)
done
hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
- by (simp only: LIMSEQ_Zseq_iff setsum_diff finite_S1 S2_le_S1 diff_0_right)
+ unfolding tendsto_Zfun_iff diff_0_right
+ by (simp only: setsum_diff finite_S1 S2_le_S1)
with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (rule LIMSEQ_diff_approach_zero2)
--- a/src/HOLCF/Cont.thy Tue May 04 20:30:22 2010 +0200
+++ b/src/HOLCF/Cont.thy Tue May 04 13:11:15 2010 -0700
@@ -237,7 +237,7 @@
text {* functions with discrete domain *}
-lemma cont_discrete_cpo [simp]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
+lemma cont_discrete_cpo [cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
apply (drule discrete_chain_const, clarify)
apply (simp add: lub_const)