# HG changeset patch
# User huffman
# Date 1243576637 25200
# Node ID e17f13cd1280788120aa610d595f0049fc9997b3
# Parent  198eae6f5a35db06eb62e9e9cde336bbea2142ee
generalize constants in SEQ.thy to class metric_space

diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Deriv.thy	Thu May 28 22:57:17 2009 -0700
@@ -577,7 +577,7 @@
 apply (drule not_P_Bolzano_bisect', assumption+)
 apply (rename_tac "l")
 apply (drule_tac x = l in spec, clarify)
-apply (simp add: LIMSEQ_def)
+apply (simp add: LIMSEQ_iff)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
 apply (drule real_less_half_sum, auto)
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Integration.thy	Thu May 28 22:57:17 2009 -0700
@@ -430,7 +430,7 @@
 lemma Cauchy_iff2:
      "Cauchy X =
       (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
-apply (simp add: Cauchy_def, auto)
+apply (simp add: Cauchy_iff, auto)
 apply (drule reals_Archimedean, safe)
 apply (drule_tac x = n in spec, auto)
 apply (rule_tac x = M in exI, auto)
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Lim.thy	Thu May 28 22:57:17 2009 -0700
@@ -700,7 +700,7 @@
     }
     then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
     with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
-    thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
+    thus ?thesis by (unfold LIMSEQ_iff, auto simp add: linorder_not_less)
   qed
   ultimately show False by simp
 qed
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Log.thy	Thu May 28 22:57:17 2009 -0700
@@ -248,7 +248,7 @@
 qed
 
 lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
-  apply (unfold LIMSEQ_def)
+  apply (unfold LIMSEQ_iff)
   apply clarsimp
   apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
   apply clarify
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/SEQ.thy	Thu May 28 22:57:17 2009 -0700
@@ -18,18 +18,18 @@
   [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
 
 definition
-  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+  LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
     ("((_)/ ----> (_))" [60, 60] 60) where
     --{*Standard definition of convergence of sequence*}
-  [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+  [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
 
 definition
-  lim :: "(nat => 'a::real_normed_vector) => 'a" where
+  lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
     --{*Standard definition of limit using choice operator*}
   "lim X = (THE L. X ----> L)"
 
 definition
-  convergent :: "(nat => 'a::real_normed_vector) => bool" where
+  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
     --{*Standard definition of convergence*}
   "convergent X = (\<exists>L. X ----> L)"
 
@@ -62,9 +62,9 @@
   [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
 
 definition
-  Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
+  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
     --{*Standard definition of the Cauchy condition*}
-  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
 
 
 subsection {* Bounded Sequences *}
@@ -302,28 +302,46 @@
 subsection {* Limits of Sequences *}
 
 lemma LIMSEQ_iff:
-      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
-by (rule LIMSEQ_def)
+  fixes L :: "'a::real_normed_vector"
+  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
+unfolding LIMSEQ_def dist_norm ..
 
 lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
-by (simp only: LIMSEQ_def Zseq_def)
+by (simp only: LIMSEQ_iff Zseq_def)
+
+lemma metric_LIMSEQ_I:
+  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_def)
+
+lemma metric_LIMSEQ_D:
+  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
+by (simp add: LIMSEQ_def)
 
 lemma LIMSEQ_I:
-  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
-by (simp add: LIMSEQ_def)
+  fixes L :: "'a::real_normed_vector"
+  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_D:
-  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
-by (simp add: LIMSEQ_def)
+  fixes L :: "'a::real_normed_vector"
+  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
 by (simp add: LIMSEQ_def)
 
-lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)"
-by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff)
+lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
+apply (safe intro!: LIMSEQ_const)
+apply (rule ccontr)
+apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
+apply (simp add: zero_less_dist_iff)
+apply auto
+done
 
-lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
-apply (simp add: LIMSEQ_def, safe)
+lemma LIMSEQ_norm:
+  fixes a :: "'a::real_normed_vector"
+  shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
+apply (simp add: LIMSEQ_iff, safe)
 apply (drule_tac x="r" in spec, safe)
 apply (rule_tac x="no" in exI, safe)
 apply (drule_tac x="n" in spec, safe)
@@ -332,8 +350,8 @@
 
 lemma LIMSEQ_ignore_initial_segment:
   "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
-apply (rule LIMSEQ_I)
-apply (drule (1) LIMSEQ_D)
+apply (rule metric_LIMSEQ_I)
+apply (drule (1) metric_LIMSEQ_D)
 apply (erule exE, rename_tac N)
 apply (rule_tac x=N in exI)
 apply simp
@@ -341,8 +359,8 @@
 
 lemma LIMSEQ_offset:
   "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
-apply (rule LIMSEQ_I)
-apply (drule (1) LIMSEQ_D)
+apply (rule metric_LIMSEQ_I)
+apply (drule (1) metric_LIMSEQ_D)
 apply (erule exE, rename_tac N)
 apply (rule_tac x="N + k" in exI)
 apply clarify
@@ -374,20 +392,36 @@
   shows "(- a) - (- b) = - (a - b)"
 by simp
 
-lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
+lemma LIMSEQ_add:
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
 by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add)
 
-lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
+lemma LIMSEQ_minus:
+  fixes a :: "'a::real_normed_vector"
+  shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
 by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus)
 
-lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
+lemma LIMSEQ_minus_cancel:
+  fixes a :: "'a::real_normed_vector"
+  shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
 by (drule LIMSEQ_minus, simp)
 
-lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
+lemma LIMSEQ_diff:
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
 by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
 
 lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff)
+apply (rule ccontr)
+apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
+apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
+apply (clarify, rename_tac M N)
+apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
+apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
+apply (erule le_less_trans, rule add_strict_mono, simp, simp)
+apply (subst dist_commute, rule dist_triangle)
+done
 
 lemma (in bounded_linear) LIMSEQ:
   "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
@@ -492,6 +526,7 @@
 by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
 
 lemma LIMSEQ_setsum:
+  fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
 proof (cases "finite S")
@@ -534,39 +569,40 @@
     by (simp add: setprod_def LIMSEQ_const)
 qed
 
-lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
+lemma LIMSEQ_add_const:
+  fixes a :: "'a::real_normed_vector"
+  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
 by (simp add: LIMSEQ_add LIMSEQ_const)
 
 (* FIXME: delete *)
 lemma LIMSEQ_add_minus:
-     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
+  fixes a b :: "'a::real_normed_vector"
+  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
 by (simp only: LIMSEQ_add LIMSEQ_minus)
 
-lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
+lemma LIMSEQ_diff_const:
+  fixes a b :: "'a::real_normed_vector"
+  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
 by (simp add: LIMSEQ_diff LIMSEQ_const)
 
-lemma LIMSEQ_diff_approach_zero: 
-  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
-     f ----> L"
-  apply (drule LIMSEQ_add)
-  apply assumption
-  apply simp
-done
+lemma LIMSEQ_diff_approach_zero:
+  fixes L :: "'a::real_normed_vector"
+  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
+by (drule (1) LIMSEQ_add, simp)
 
-lemma LIMSEQ_diff_approach_zero2: 
-  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
-     g ----> L";
-  apply (drule LIMSEQ_diff)
-  apply assumption
-  apply simp
-done
+lemma LIMSEQ_diff_approach_zero2:
+  fixes L :: "'a::real_normed_vector"
+  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L";
+by (drule (1) LIMSEQ_diff, simp)
 
 text{*A sequence tends to zero iff its abs does*}
-lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)"
-by (simp add: LIMSEQ_def)
+lemma LIMSEQ_norm_zero:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
+by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
-by (simp add: LIMSEQ_def)
+by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
 by (drule LIMSEQ_norm, simp)
@@ -653,7 +689,9 @@
 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
 by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
 
-lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
+lemma convergent_minus_iff:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
 apply (simp add: convergent_def)
 apply (auto dest: LIMSEQ_minus)
 apply (drule LIMSEQ_minus, auto)
@@ -1119,20 +1157,35 @@
 
 subsection {* Cauchy Sequences *}
 
-lemma CauchyI:
-  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
+lemma metric_CauchyI:
+  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+by (simp add: Cauchy_def)
+
+lemma metric_CauchyD:
+  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
 by (simp add: Cauchy_def)
 
+lemma Cauchy_iff:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
+unfolding Cauchy_def dist_norm ..
+
+lemma CauchyI:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
+by (simp add: Cauchy_iff)
+
 lemma CauchyD:
-  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
-by (simp add: Cauchy_def)
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
+by (simp add: Cauchy_iff)
 
 lemma Cauchy_subseq_Cauchy:
   "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
-apply (auto simp add: Cauchy_def) 
-apply (drule_tac x=e in spec, clarify)  
-apply (rule_tac x=M in exI, clarify) 
-apply (blast intro: seq_suble le_trans dest!: spec) 
+apply (auto simp add: Cauchy_def)
+apply (drule_tac x=e in spec, clarify)
+apply (rule_tac x=M in exI, clarify)
+apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
 done
 
 subsubsection {* Cauchy Sequences are Bounded *}
@@ -1149,7 +1202,7 @@
 done
 
 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
-apply (simp add: Cauchy_def)
+apply (simp add: Cauchy_iff)
 apply (drule spec, drule mp, rule zero_less_one, safe)
 apply (drule_tac x="M" in spec, simp)
 apply (drule lemmaCauchy)
@@ -1167,22 +1220,21 @@
 
 theorem LIMSEQ_imp_Cauchy:
   assumes X: "X ----> a" shows "Cauchy X"
-proof (rule CauchyI)
+proof (rule metric_CauchyI)
   fix e::real assume "0 < e"
   hence "0 < e/2" by simp
-  with X have "\<exists>N. \<forall>n\<ge>N. norm (X n - a) < e/2" by (rule LIMSEQ_D)
-  then obtain N where N: "\<forall>n\<ge>N. norm (X n - a) < e/2" ..
-  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < e"
+  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
+  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
+  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   proof (intro exI allI impI)
     fix m assume "N \<le> m"
-    hence m: "norm (X m - a) < e/2" using N by fast
+    hence m: "dist (X m) a < e/2" using N by fast
     fix n assume "N \<le> n"
-    hence n: "norm (X n - a) < e/2" using N by fast
-    have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp
-    also have "\<dots> \<le> norm (X m - a) + norm (X n - a)"
-      by (rule norm_triangle_ineq4)
-    also from m n have "\<dots> < e" by(simp add:field_simps)
-    finally show "norm (X m - X n) < e" .
+    hence n: "dist (X n) a < e/2" using N by fast
+    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
+      by (rule dist_triangle2)
+    also from m n have "\<dots> < e" by simp
+    finally show "dist (X m) (X n) < e" .
   qed
 qed
 
@@ -1311,7 +1363,7 @@
 lemma convergent_subseq_convergent:
   fixes X :: "nat \<Rightarrow> 'a::banach"
   shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
-  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) 
+  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
 
 
 subsection {* Power Sequences *}
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Series.thy	Thu May 28 22:57:17 2009 -0700
@@ -160,7 +160,7 @@
 
 lemma series_zero: 
      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
-apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
+apply (simp add: sums_def LIMSEQ_iff diff_minus[symmetric], safe)
 apply (rule_tac x = n in exI)
 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
 done
@@ -264,7 +264,7 @@
      "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
 apply (drule summable_sums)
 apply (simp only: sums_def sumr_group)
-apply (unfold LIMSEQ_def, safe)
+apply (unfold LIMSEQ_iff, safe)
 apply (drule_tac x="r" in spec, safe)
 apply (rule_tac x="no" in exI, safe)
 apply (drule_tac x="n*k" in spec)
@@ -361,7 +361,7 @@
 lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
 apply (drule summable_convergent_sumr_iff [THEN iffD1])
 apply (drule convergent_Cauchy)
-apply (simp only: Cauchy_def LIMSEQ_def, safe)
+apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
 apply (drule_tac x="r" in spec, safe)
 apply (rule_tac x="M" in exI, safe)
 apply (drule_tac x="Suc n" in spec, simp)
@@ -371,7 +371,7 @@
 lemma summable_Cauchy:
      "summable (f::nat \<Rightarrow> 'a::banach) =  
       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"
-apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def, safe)
+apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)
 apply (drule spec, drule (1) mp)
 apply (erule exE, rule_tac x="M" in exI, clarify)
 apply (rule_tac x="m" and y="n" in linorder_le_cases)