add lemma sequentially_imp_eventually_within;
rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;

--- 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 "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+    eventually (\<lambda>n. P (f n)) sequentially"
+  shows "eventually P (at a within s)"
+proof (rule ccontr)
+  let ?I = "\<lambda>n. inverse (real (Suc n))"
+  def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+  assume "\<not> eventually P (at a within s)"
+  hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+    unfolding Limits.eventually_within Limits.eventually_at by fast
+  hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+  hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
+    unfolding F_def by (rule someI_ex)
+  hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
+    and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> 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 (\<lambda>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 "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+    eventually (\<lambda>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 \<Rightarrow> 'b::topological_space"
   assumes f: "f -- a --> l"
   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>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 "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
-  shows "eventually P (at a)"
-proof (rule ccontr)
-  let ?I = "\<lambda>n. inverse (real (Suc n))"
-  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
-  assume "\<not> eventually P (at a)"
-  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
-    unfolding eventually_at by simp
-  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
-  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
-    by (rule someI_ex)
-  hence F1: "\<And>n. ?F n \<noteq> a"
-    and F2: "\<And>n. dist (?F n) a < ?I n"
-    and F3: "\<And>n. \<not> 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 "\<forall>n. ?F n \<noteq> a"
-    by (rule allI) (rule F1)
-  ultimately have "eventually (\<lambda>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 \<Rightarrow> 'b::topological_space"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>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:
   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =