add lemma metric_tendsto_imp_tendsto

--- a/src/HOL/Lim.thy	Wed Aug 17 09:59:10 2011 -0700
+++ b/src/HOL/Lim.thy	Wed Aug 17 11:06:39 2011 -0700
@@ -132,12 +132,8 @@
   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 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
+  by (rule metric_tendsto_imp_tendsto [OF f],
+    auto simp add: eventually_at_topological le)
 
 lemma LIM_imp_LIM:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -145,9 +141,8 @@
   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"
-apply (rule metric_LIM_imp_LIM [OF f])
-apply (simp add: dist_norm le)
-done
+  by (rule metric_LIM_imp_LIM [OF f],
+    simp add: dist_norm le)
 
 lemma LIM_norm:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"

--- a/src/HOL/Limits.thy	Wed Aug 17 09:59:10 2011 -0700
+++ b/src/HOL/Limits.thy	Wed Aug 17 11:06:39 2011 -0700
@@ -627,6 +627,17 @@
     by (rule eventually_mono)
 qed
 
+lemma metric_tendsto_imp_tendsto:
+  assumes f: "(f ---> a) F"
+  assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
+  shows "(g ---> b) F"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
+  with le show "eventually (\<lambda>x. dist (g x) b < e) F"
+    using le_less_trans by (rule eventually_elim2)
+qed
+
 subsubsection {* Distance and norms *}
 
 lemma tendsto_dist [tendsto_intros]: