# HG changeset patch
# User hoelzl
# Date 1358421684 -3600
# Node ID ae7cd20ed118f4e063f40f0754ee6299617a3c20
# Parent  5b193d3dd6b656a20c3d876ed160fc33236d4c49
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy

diff -r 5b193d3dd6b6 -r ae7cd20ed118 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:09:48 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:21:24 2013 +0100
@@ -1403,14 +1403,14 @@
   proof
     fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)"
     proof(cases "x=x0")
-      case True thus ?thesis using convergent_imp_cauchy[OF assms(5)] by auto
+      case True thus ?thesis using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
     next
       case False show ?thesis unfolding Cauchy_def
       proof(rule,rule)
         fix e::real assume "e>0"
         hence *:"e/2>0" "e/2/norm(x-x0)>0"
           using False by (auto intro!: divide_pos_pos)
-        guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
+        guess M using LIMSEQ_imp_Cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
         guess N using lem1[rule_format,OF *(2)] .. note N = this
         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
           apply(rule_tac x="max M N" in exI)
diff -r 5b193d3dd6b6 -r ae7cd20ed118 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:48 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:21:24 2013 +0100
@@ -3249,14 +3249,6 @@
     by blast
 qed
 
-lemma convergent_imp_cauchy:
- "(s ---> l) sequentially ==> Cauchy s"
-proof(simp only: cauchy_def, rule, rule)
-  fix e::real assume "e>0" "(s ---> l) sequentially"
-  then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding LIMSEQ_def by(erule_tac x="e/2" in allE) auto
-  thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"  using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
-qed
-
 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)"
 proof-
   from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
@@ -3323,7 +3315,7 @@
     then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
       unfolding islimpt_sequential by auto
     then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
-      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
+      using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto
     hence "x \<in> s"  using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
   }
   thus "closed s" unfolding closed_limpt by auto
@@ -3350,7 +3342,7 @@
 lemma convergent_imp_bounded:
   fixes s :: "nat \<Rightarrow> 'a::metric_space"
   shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
-  by (intro cauchy_imp_bounded convergent_imp_cauchy)
+  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
 
 subsubsection{* Total boundedness *}
 
@@ -3377,7 +3369,7 @@
     qed }
   hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
   then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
-  from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
+  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
   then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
   show False
     using N[THEN spec[where x=N], THEN spec[where x="N+1"]]