--- a/src/HOL/Lim.thy Sun Aug 14 08:45:38 2011 -0700
+++ b/src/HOL/Lim.thy Sun Aug 14 10:25:43 2011 -0700
@@ -181,32 +181,32 @@
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
by (rule tendsto_rabs_zero_iff)
-lemma at_neq_bot:
+lemma trivial_limit_at:
fixes a :: "'a::real_normed_algebra_1"
- shows "at a \<noteq> bot" -- {* TODO: find a more appropriate class *}
-unfolding eventually_False [symmetric]
+ shows "\<not> trivial_limit (at a)" -- {* TODO: find a more appropriate class *}
+unfolding trivial_limit_def
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"
+ fixes k L :: "'b::t2_space"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
-by (simp add: tendsto_const_iff at_neq_bot)
+by (simp add: tendsto_const_iff trivial_limit_at)
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"
+ fixes k L :: "'b::t2_space"
shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
-by (simp add: tendsto_const_iff at_neq_bot)
+ by (simp add: tendsto_const_iff trivial_limit_at)
lemma LIM_unique:
fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
- fixes L M :: "'b::metric_space"
+ fixes L M :: "'b::t2_space"
shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
-by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)
+ using trivial_limit_at by (rule tendsto_unique)
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
by (rule tendsto_ident_at)
--- a/src/HOL/Limits.thy Sun Aug 14 08:45:38 2011 -0700
+++ b/src/HOL/Limits.thy Sun Aug 14 10:25:43 2011 -0700
@@ -581,15 +581,37 @@
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
by (simp add: tendsto_def)
+lemma tendsto_unique:
+ fixes f :: "'a \<Rightarrow> 'b::t2_space"
+ assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
+ shows "a = b"
+proof (rule ccontr)
+ assume "a \<noteq> b"
+ obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
+ using hausdorff [OF `a \<noteq> b`] by fast
+ have "eventually (\<lambda>x. f x \<in> U) F"
+ using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
+ moreover
+ have "eventually (\<lambda>x. f x \<in> V) F"
+ using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
+ ultimately
+ have "eventually (\<lambda>x. False) F"
+ proof (rule eventually_elim2)
+ fix x
+ assume "f x \<in> U" "f x \<in> V"
+ hence "f x \<in> U \<inter> V" by simp
+ with `U \<inter> V = {}` show "False" by simp
+ qed
+ with `\<not> trivial_limit F` show "False"
+ by (simp add: trivial_limit_def)
+qed
+
lemma tendsto_const_iff:
- fixes k l :: "'a::metric_space"
- assumes "F \<noteq> bot" shows "((\<lambda>n. k) ---> l) F \<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
+ fixes a b :: "'a::t2_space"
+ assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
+ by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
+
+subsubsection {* Distance and norms *}
lemma tendsto_dist [tendsto_intros]:
assumes f: "(f ---> l) F" and g: "(g ---> m) F"
@@ -611,8 +633,6 @@
qed
qed
-subsubsection {* Norms *}
-
lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp
@@ -865,31 +885,4 @@
shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
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 F" "(f ---> l) F" "(f ---> l') F"
- shows "l = l'"
-proof (rule ccontr)
- assume "l \<noteq> l'"
- obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
- using hausdorff [OF `l \<noteq> l'`] by fast
- have "eventually (\<lambda>x. f x \<in> U) F"
- using `(f ---> l) F` `open U` `l \<in> U` by (rule topological_tendstoD)
- moreover
- have "eventually (\<lambda>x. f x \<in> V) F"
- using `(f ---> l') F` `open V` `l' \<in> V` by (rule topological_tendstoD)
- ultimately
- have "eventually (\<lambda>x. False) F"
- proof (rule eventually_elim2)
- fix x
- assume "f x \<in> U" "f x \<in> V"
- hence "f x \<in> U \<inter> V" by simp
- with `U \<inter> V = {}` show "False" by simp
- qed
- with `\<not> trivial_limit F` show "False"
- by (simp add: trivial_limit_def)
-qed
-
end
--- a/src/HOL/SEQ.thy Sun Aug 14 08:45:38 2011 -0700
+++ b/src/HOL/SEQ.thy Sun Aug 14 10:25:43 2011 -0700
@@ -189,7 +189,7 @@
"X ----> L \<equiv> (X ---> L) sequentially"
definition
- lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
+ lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
--{*Standard definition of limit using choice operator*}
"lim X = (THE L. X ----> L)"
@@ -301,9 +301,9 @@
by (rule tendsto_const)
lemma LIMSEQ_const_iff:
- fixes k l :: "'a::metric_space"
+ fixes k l :: "'a::t2_space"
shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
-by (rule tendsto_const_iff, rule sequentially_bot)
+ using trivial_limit_sequentially by (rule tendsto_const_iff)
lemma LIMSEQ_norm:
fixes a :: "'a::real_normed_vector"
@@ -366,9 +366,9 @@
by (rule tendsto_diff)
lemma LIMSEQ_unique:
- fixes a b :: "'a::metric_space"
+ fixes a b :: "'a::t2_space"
shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
+ using trivial_limit_sequentially by (rule tendsto_unique)
lemma (in bounded_linear) LIMSEQ:
"X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"