1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:09:48 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:21:24 2013 +0100
     1.3 @@ -1403,14 +1403,14 @@
     1.4    proof
     1.5      fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)"
     1.6      proof(cases "x=x0")
     1.7 -      case True thus ?thesis using convergent_imp_cauchy[OF assms(5)] by auto
     1.8 +      case True thus ?thesis using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
     1.9      next
    1.10        case False show ?thesis unfolding Cauchy_def
    1.11        proof(rule,rule)
    1.12          fix e::real assume "e>0"
    1.13          hence *:"e/2>0" "e/2/norm(x-x0)>0"
    1.14            using False by (auto intro!: divide_pos_pos)
    1.15 -        guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
    1.16 +        guess M using LIMSEQ_imp_Cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
    1.17          guess N using lem1[rule_format,OF *(2)] .. note N = this
    1.18          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
    1.19            apply(rule_tac x="max M N" in exI)

     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:48 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:21:24 2013 +0100
     2.3 @@ -3249,14 +3249,6 @@
     2.4      by blast
     2.5  qed
     2.6  
     2.7 -lemma convergent_imp_cauchy:
     2.8 - "(s ---> l) sequentially ==> Cauchy s"
     2.9 -proof(simp only: cauchy_def, rule, rule)
    2.10 -  fix e::real assume "e>0" "(s ---> l) sequentially"
    2.11 -  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
    2.12 -  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
    2.13 -qed
    2.14 -
    2.15  lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)"
    2.16  proof-
    2.17    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
    2.18 @@ -3323,7 +3315,7 @@
    2.19      then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
    2.20        unfolding islimpt_sequential by auto
    2.21      then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
    2.22 -      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
    2.23 +      using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto
    2.24      hence "x \<in> s"  using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
    2.25    }
    2.26    thus "closed s" unfolding closed_limpt by auto
    2.27 @@ -3350,7 +3342,7 @@
    2.28  lemma convergent_imp_bounded:
    2.29    fixes s :: "nat \<Rightarrow> 'a::metric_space"
    2.30    shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
    2.31 -  by (intro cauchy_imp_bounded convergent_imp_cauchy)
    2.32 +  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
    2.33  
    2.34  subsubsection{* Total boundedness *}
    2.35  
    2.36 @@ -3377,7 +3369,7 @@
    2.37      qed }
    2.38    hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
    2.39    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
    2.40 -  from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
    2.41 +  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
    2.42    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
    2.43    show False
    2.44      using N[THEN spec[where x=N], THEN spec[where x="N+1"]]