diff r 1d477a2b1572 r a2e9b39df938 src/HOL/Lim.thy
 a/src/HOL/Lim.thy Thu Aug 25 19:41:38 2011 0700
+++ b/src/HOL/Lim.thy Fri Aug 26 08:12:38 2011 0700
@@ 444,46 +444,51 @@
subsection {* Relation of LIM and LIMSEQ *}
+lemma sequentially_imp_eventually_within:
+ fixes a :: "'a::metric_space"
+ assumes "\f. (\n. f n \ s \ f n \ a) \ f > a \
+ eventually (\n. P (f n)) sequentially"
+ shows "eventually P (at a within s)"
+proof (rule ccontr)
+ let ?I = "\n. inverse (real (Suc n))"
+ def F \ "\n::nat. SOME x. x \ s \ x \ a \ dist x a < ?I n \ \ P x"
+ assume "\ eventually P (at a within s)"
+ hence P: "\d>0. \x. x \ s \ x \ a \ dist x a < d \ \ P x"
+ unfolding Limits.eventually_within Limits.eventually_at by fast
+ hence "\n. \x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" by simp
+ hence F: "\n. F n \ s \ F n \ a \ dist (F n) a < ?I n \ \ P (F n)"
+ unfolding F_def by (rule someI_ex)
+ hence F0: "\n. F n \ s" and F1: "\n. F n \ a"
+ and F2: "\n. dist (F n) a < ?I n" and F3: "\n. \ P (F n)"
+ by fast+
+ from LIMSEQ_inverse_real_of_nat have "F > a"
+ by (rule metric_tendsto_imp_tendsto,
+ simp add: dist_norm F2 less_imp_le)
+ hence "eventually (\n. P (F n)) sequentially"
+ using assms F0 F1 by simp
+ thus "False" by (simp add: F3)
+qed
+
+lemma sequentially_imp_eventually_at:
+ fixes a :: "'a::metric_space"
+ assumes "\f. (\n. f n \ a) \ f > a \
+ eventually (\n. P (f n)) sequentially"
+ shows "eventually P (at a)"
+ using assms sequentially_imp_eventually_within [where s=UNIV]
+ unfolding within_UNIV by simp
+
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \ 'b::topological_space"
assumes f: "f  a > l"
shows "\S. (\n. S n \ a) \ S > a \ (\n. f (S n)) > l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
lemma LIMSEQ_SEQ_conv2_lemma:
 fixes a :: "'a::metric_space"
 assumes "\S. (\n. S n \ a) \ S > a \ eventually (\x. P (S x)) sequentially"
 shows "eventually P (at a)"
proof (rule ccontr)
 let ?I = "\n. inverse (real (Suc n))"
 let ?F = "\n::nat. SOME x. x \ a \ dist x a < ?I n \ \ P x"
 assume "\ eventually P (at a)"
 hence P: "\d>0. \x. x \ a \ dist x a < d \ \ P x"
 unfolding eventually_at by simp
 hence "\n. \x. x \ a \ dist x a < ?I n \ \ P x" by simp
 hence F: "\n. ?F n \ a \ dist (?F n) a < ?I n \ \ P (?F n)"
 by (rule someI_ex)
 hence F1: "\n. ?F n \ a"
 and F2: "\n. dist (?F n) a < ?I n"
 and F3: "\n. \ P (?F n)"
 by fast+
 have "?F > a"
 using LIMSEQ_inverse_real_of_nat
 by (rule metric_tendsto_imp_tendsto,
 simp add: dist_norm F2 [THEN less_imp_le])
 moreover have "\n. ?F n \ a"
 by (rule allI) (rule F1)
 ultimately have "eventually (\n. P (?F n)) sequentially"
 using assms by simp
 thus "False" by (simp add: F3)
qed

lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::metric_space \ 'b::topological_space"
assumes "\S. (\n. S n \ a) \ S > a \ (\n. f (S n)) > l"
shows "f  a > l"
using assms unfolding tendsto_def [where l=l]
 by (simp add: LIMSEQ_SEQ_conv2_lemma)
+ by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
"(\S. (\n. S n \ a) \ S > (a::'a::metric_space) \ (\n. X (S n)) > L) =