generalize constants in SEQ.thy to class metric_space
authorhuffman
Thu May 28 22:57:17 2009 -0700 (2009-05-28)
changeset 31336e17f13cd1280
parent 31293 198eae6f5a35
child 31337 a9ed5fcc5e39
generalize constants in SEQ.thy to class metric_space
src/HOL/Deriv.thy
src/HOL/Integration.thy
src/HOL/Lim.thy
src/HOL/Log.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Deriv.thy	Thu May 28 22:54:57 2009 -0700
     1.2 +++ b/src/HOL/Deriv.thy	Thu May 28 22:57:17 2009 -0700
     1.3 @@ -577,7 +577,7 @@
     1.4  apply (drule not_P_Bolzano_bisect', assumption+)
     1.5  apply (rename_tac "l")
     1.6  apply (drule_tac x = l in spec, clarify)
     1.7 -apply (simp add: LIMSEQ_def)
     1.8 +apply (simp add: LIMSEQ_iff)
     1.9  apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
    1.10  apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
    1.11  apply (drule real_less_half_sum, auto)
     2.1 --- a/src/HOL/Integration.thy	Thu May 28 22:54:57 2009 -0700
     2.2 +++ b/src/HOL/Integration.thy	Thu May 28 22:57:17 2009 -0700
     2.3 @@ -430,7 +430,7 @@
     2.4  lemma Cauchy_iff2:
     2.5       "Cauchy X =
     2.6        (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
     2.7 -apply (simp add: Cauchy_def, auto)
     2.8 +apply (simp add: Cauchy_iff, auto)
     2.9  apply (drule reals_Archimedean, safe)
    2.10  apply (drule_tac x = n in spec, auto)
    2.11  apply (rule_tac x = M in exI, auto)
     3.1 --- a/src/HOL/Lim.thy	Thu May 28 22:54:57 2009 -0700
     3.2 +++ b/src/HOL/Lim.thy	Thu May 28 22:57:17 2009 -0700
     3.3 @@ -700,7 +700,7 @@
     3.4      }
     3.5      then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
     3.6      with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
     3.7 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
     3.8 +    thus ?thesis by (unfold LIMSEQ_iff, auto simp add: linorder_not_less)
     3.9    qed
    3.10    ultimately show False by simp
    3.11  qed
     4.1 --- a/src/HOL/Log.thy	Thu May 28 22:54:57 2009 -0700
     4.2 +++ b/src/HOL/Log.thy	Thu May 28 22:57:17 2009 -0700
     4.3 @@ -248,7 +248,7 @@
     4.4  qed
     4.5  
     4.6  lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
     4.7 -  apply (unfold LIMSEQ_def)
     4.8 +  apply (unfold LIMSEQ_iff)
     4.9    apply clarsimp
    4.10    apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
    4.11    apply clarify
     5.1 --- a/src/HOL/SEQ.thy	Thu May 28 22:54:57 2009 -0700
     5.2 +++ b/src/HOL/SEQ.thy	Thu May 28 22:57:17 2009 -0700
     5.3 @@ -18,18 +18,18 @@
     5.4    [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
     5.5  
     5.6  definition
     5.7 -  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     5.8 +  LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
     5.9      ("((_)/ ----> (_))" [60, 60] 60) where
    5.10      --{*Standard definition of convergence of sequence*}
    5.11 -  [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
    5.12 +  [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    5.13  
    5.14  definition
    5.15 -  lim :: "(nat => 'a::real_normed_vector) => 'a" where
    5.16 +  lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
    5.17      --{*Standard definition of limit using choice operator*}
    5.18    "lim X = (THE L. X ----> L)"
    5.19  
    5.20  definition
    5.21 -  convergent :: "(nat => 'a::real_normed_vector) => bool" where
    5.22 +  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    5.23      --{*Standard definition of convergence*}
    5.24    "convergent X = (\<exists>L. X ----> L)"
    5.25  
    5.26 @@ -62,9 +62,9 @@
    5.27    [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
    5.28  
    5.29  definition
    5.30 -  Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
    5.31 +  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    5.32      --{*Standard definition of the Cauchy condition*}
    5.33 -  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
    5.34 +  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    5.35  
    5.36  
    5.37  subsection {* Bounded Sequences *}
    5.38 @@ -302,28 +302,46 @@
    5.39  subsection {* Limits of Sequences *}
    5.40  
    5.41  lemma LIMSEQ_iff:
    5.42 -      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    5.43 -by (rule LIMSEQ_def)
    5.44 +  fixes L :: "'a::real_normed_vector"
    5.45 +  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    5.46 +unfolding LIMSEQ_def dist_norm ..
    5.47  
    5.48  lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
    5.49 -by (simp only: LIMSEQ_def Zseq_def)
    5.50 +by (simp only: LIMSEQ_iff Zseq_def)
    5.51 +
    5.52 +lemma metric_LIMSEQ_I:
    5.53 +  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
    5.54 +by (simp add: LIMSEQ_def)
    5.55 +
    5.56 +lemma metric_LIMSEQ_D:
    5.57 +  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
    5.58 +by (simp add: LIMSEQ_def)
    5.59  
    5.60  lemma LIMSEQ_I:
    5.61 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    5.62 -by (simp add: LIMSEQ_def)
    5.63 +  fixes L :: "'a::real_normed_vector"
    5.64 +  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    5.65 +by (simp add: LIMSEQ_iff)
    5.66  
    5.67  lemma LIMSEQ_D:
    5.68 -  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
    5.69 -by (simp add: LIMSEQ_def)
    5.70 +  fixes L :: "'a::real_normed_vector"
    5.71 +  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
    5.72 +by (simp add: LIMSEQ_iff)
    5.73  
    5.74  lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
    5.75  by (simp add: LIMSEQ_def)
    5.76  
    5.77 -lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)"
    5.78 -by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff)
    5.79 +lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    5.80 +apply (safe intro!: LIMSEQ_const)
    5.81 +apply (rule ccontr)
    5.82 +apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
    5.83 +apply (simp add: zero_less_dist_iff)
    5.84 +apply auto
    5.85 +done
    5.86  
    5.87 -lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
    5.88 -apply (simp add: LIMSEQ_def, safe)
    5.89 +lemma LIMSEQ_norm:
    5.90 +  fixes a :: "'a::real_normed_vector"
    5.91 +  shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
    5.92 +apply (simp add: LIMSEQ_iff, safe)
    5.93  apply (drule_tac x="r" in spec, safe)
    5.94  apply (rule_tac x="no" in exI, safe)
    5.95  apply (drule_tac x="n" in spec, safe)
    5.96 @@ -332,8 +350,8 @@
    5.97  
    5.98  lemma LIMSEQ_ignore_initial_segment:
    5.99    "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
   5.100 -apply (rule LIMSEQ_I)
   5.101 -apply (drule (1) LIMSEQ_D)
   5.102 +apply (rule metric_LIMSEQ_I)
   5.103 +apply (drule (1) metric_LIMSEQ_D)
   5.104  apply (erule exE, rename_tac N)
   5.105  apply (rule_tac x=N in exI)
   5.106  apply simp
   5.107 @@ -341,8 +359,8 @@
   5.108  
   5.109  lemma LIMSEQ_offset:
   5.110    "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
   5.111 -apply (rule LIMSEQ_I)
   5.112 -apply (drule (1) LIMSEQ_D)
   5.113 +apply (rule metric_LIMSEQ_I)
   5.114 +apply (drule (1) metric_LIMSEQ_D)
   5.115  apply (erule exE, rename_tac N)
   5.116  apply (rule_tac x="N + k" in exI)
   5.117  apply clarify
   5.118 @@ -374,20 +392,36 @@
   5.119    shows "(- a) - (- b) = - (a - b)"
   5.120  by simp
   5.121  
   5.122 -lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
   5.123 +lemma LIMSEQ_add:
   5.124 +  fixes a b :: "'a::real_normed_vector"
   5.125 +  shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
   5.126  by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add)
   5.127  
   5.128 -lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
   5.129 +lemma LIMSEQ_minus:
   5.130 +  fixes a :: "'a::real_normed_vector"
   5.131 +  shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
   5.132  by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus)
   5.133  
   5.134 -lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
   5.135 +lemma LIMSEQ_minus_cancel:
   5.136 +  fixes a :: "'a::real_normed_vector"
   5.137 +  shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
   5.138  by (drule LIMSEQ_minus, simp)
   5.139  
   5.140 -lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
   5.141 +lemma LIMSEQ_diff:
   5.142 +  fixes a b :: "'a::real_normed_vector"
   5.143 +  shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
   5.144  by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
   5.145  
   5.146  lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
   5.147 -by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff)
   5.148 +apply (rule ccontr)
   5.149 +apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
   5.150 +apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
   5.151 +apply (clarify, rename_tac M N)
   5.152 +apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
   5.153 +apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
   5.154 +apply (erule le_less_trans, rule add_strict_mono, simp, simp)
   5.155 +apply (subst dist_commute, rule dist_triangle)
   5.156 +done
   5.157  
   5.158  lemma (in bounded_linear) LIMSEQ:
   5.159    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
   5.160 @@ -492,6 +526,7 @@
   5.161  by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
   5.162  
   5.163  lemma LIMSEQ_setsum:
   5.164 +  fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
   5.165    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   5.166    shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
   5.167  proof (cases "finite S")
   5.168 @@ -534,39 +569,40 @@
   5.169      by (simp add: setprod_def LIMSEQ_const)
   5.170  qed
   5.171  
   5.172 -lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
   5.173 +lemma LIMSEQ_add_const:
   5.174 +  fixes a :: "'a::real_normed_vector"
   5.175 +  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
   5.176  by (simp add: LIMSEQ_add LIMSEQ_const)
   5.177  
   5.178  (* FIXME: delete *)
   5.179  lemma LIMSEQ_add_minus:
   5.180 -     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
   5.181 +  fixes a b :: "'a::real_normed_vector"
   5.182 +  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
   5.183  by (simp only: LIMSEQ_add LIMSEQ_minus)
   5.184  
   5.185 -lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
   5.186 +lemma LIMSEQ_diff_const:
   5.187 +  fixes a b :: "'a::real_normed_vector"
   5.188 +  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
   5.189  by (simp add: LIMSEQ_diff LIMSEQ_const)
   5.190  
   5.191 -lemma LIMSEQ_diff_approach_zero: 
   5.192 -  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
   5.193 -     f ----> L"
   5.194 -  apply (drule LIMSEQ_add)
   5.195 -  apply assumption
   5.196 -  apply simp
   5.197 -done
   5.198 +lemma LIMSEQ_diff_approach_zero:
   5.199 +  fixes L :: "'a::real_normed_vector"
   5.200 +  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
   5.201 +by (drule (1) LIMSEQ_add, simp)
   5.202  
   5.203 -lemma LIMSEQ_diff_approach_zero2: 
   5.204 -  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
   5.205 -     g ----> L";
   5.206 -  apply (drule LIMSEQ_diff)
   5.207 -  apply assumption
   5.208 -  apply simp
   5.209 -done
   5.210 +lemma LIMSEQ_diff_approach_zero2:
   5.211 +  fixes L :: "'a::real_normed_vector"
   5.212 +  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L";
   5.213 +by (drule (1) LIMSEQ_diff, simp)
   5.214  
   5.215  text{*A sequence tends to zero iff its abs does*}
   5.216 -lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)"
   5.217 -by (simp add: LIMSEQ_def)
   5.218 +lemma LIMSEQ_norm_zero:
   5.219 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.220 +  shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
   5.221 +by (simp add: LIMSEQ_iff)
   5.222  
   5.223  lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
   5.224 -by (simp add: LIMSEQ_def)
   5.225 +by (simp add: LIMSEQ_iff)
   5.226  
   5.227  lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
   5.228  by (drule LIMSEQ_norm, simp)
   5.229 @@ -653,7 +689,9 @@
   5.230  lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
   5.231  by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
   5.232  
   5.233 -lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
   5.234 +lemma convergent_minus_iff:
   5.235 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.236 +  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
   5.237  apply (simp add: convergent_def)
   5.238  apply (auto dest: LIMSEQ_minus)
   5.239  apply (drule LIMSEQ_minus, auto)
   5.240 @@ -1119,20 +1157,35 @@
   5.241  
   5.242  subsection {* Cauchy Sequences *}
   5.243  
   5.244 -lemma CauchyI:
   5.245 -  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
   5.246 +lemma metric_CauchyI:
   5.247 +  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   5.248 +by (simp add: Cauchy_def)
   5.249 +
   5.250 +lemma metric_CauchyD:
   5.251 +  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   5.252  by (simp add: Cauchy_def)
   5.253  
   5.254 +lemma Cauchy_iff:
   5.255 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.256 +  shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
   5.257 +unfolding Cauchy_def dist_norm ..
   5.258 +
   5.259 +lemma CauchyI:
   5.260 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.261 +  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"
   5.262 +by (simp add: Cauchy_iff)
   5.263 +
   5.264  lemma CauchyD:
   5.265 -  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   5.266 -by (simp add: Cauchy_def)
   5.267 +  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   5.268 +  shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
   5.269 +by (simp add: Cauchy_iff)
   5.270  
   5.271  lemma Cauchy_subseq_Cauchy:
   5.272    "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
   5.273 -apply (auto simp add: Cauchy_def) 
   5.274 -apply (drule_tac x=e in spec, clarify)  
   5.275 -apply (rule_tac x=M in exI, clarify) 
   5.276 -apply (blast intro: seq_suble le_trans dest!: spec) 
   5.277 +apply (auto simp add: Cauchy_def)
   5.278 +apply (drule_tac x=e in spec, clarify)
   5.279 +apply (rule_tac x=M in exI, clarify)
   5.280 +apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
   5.281  done
   5.282  
   5.283  subsubsection {* Cauchy Sequences are Bounded *}
   5.284 @@ -1149,7 +1202,7 @@
   5.285  done
   5.286  
   5.287  lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
   5.288 -apply (simp add: Cauchy_def)
   5.289 +apply (simp add: Cauchy_iff)
   5.290  apply (drule spec, drule mp, rule zero_less_one, safe)
   5.291  apply (drule_tac x="M" in spec, simp)
   5.292  apply (drule lemmaCauchy)
   5.293 @@ -1167,22 +1220,21 @@
   5.294  
   5.295  theorem LIMSEQ_imp_Cauchy:
   5.296    assumes X: "X ----> a" shows "Cauchy X"
   5.297 -proof (rule CauchyI)
   5.298 +proof (rule metric_CauchyI)
   5.299    fix e::real assume "0 < e"
   5.300    hence "0 < e/2" by simp
   5.301 -  with X have "\<exists>N. \<forall>n\<ge>N. norm (X n - a) < e/2" by (rule LIMSEQ_D)
   5.302 -  then obtain N where N: "\<forall>n\<ge>N. norm (X n - a) < e/2" ..
   5.303 -  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < e"
   5.304 +  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
   5.305 +  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
   5.306 +  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   5.307    proof (intro exI allI impI)
   5.308      fix m assume "N \<le> m"
   5.309 -    hence m: "norm (X m - a) < e/2" using N by fast
   5.310 +    hence m: "dist (X m) a < e/2" using N by fast
   5.311      fix n assume "N \<le> n"
   5.312 -    hence n: "norm (X n - a) < e/2" using N by fast
   5.313 -    have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp
   5.314 -    also have "\<dots> \<le> norm (X m - a) + norm (X n - a)"
   5.315 -      by (rule norm_triangle_ineq4)
   5.316 -    also from m n have "\<dots> < e" by(simp add:field_simps)
   5.317 -    finally show "norm (X m - X n) < e" .
   5.318 +    hence n: "dist (X n) a < e/2" using N by fast
   5.319 +    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
   5.320 +      by (rule dist_triangle2)
   5.321 +    also from m n have "\<dots> < e" by simp
   5.322 +    finally show "dist (X m) (X n) < e" .
   5.323    qed
   5.324  qed
   5.325  
   5.326 @@ -1311,7 +1363,7 @@
   5.327  lemma convergent_subseq_convergent:
   5.328    fixes X :: "nat \<Rightarrow> 'a::banach"
   5.329    shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
   5.330 -  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) 
   5.331 +  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
   5.332  
   5.333  
   5.334  subsection {* Power Sequences *}
     6.1 --- a/src/HOL/Series.thy	Thu May 28 22:54:57 2009 -0700
     6.2 +++ b/src/HOL/Series.thy	Thu May 28 22:57:17 2009 -0700
     6.3 @@ -160,7 +160,7 @@
     6.4  
     6.5  lemma series_zero: 
     6.6       "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
     6.7 -apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
     6.8 +apply (simp add: sums_def LIMSEQ_iff diff_minus[symmetric], safe)
     6.9  apply (rule_tac x = n in exI)
    6.10  apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
    6.11  done
    6.12 @@ -264,7 +264,7 @@
    6.13       "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
    6.14  apply (drule summable_sums)
    6.15  apply (simp only: sums_def sumr_group)
    6.16 -apply (unfold LIMSEQ_def, safe)
    6.17 +apply (unfold LIMSEQ_iff, safe)
    6.18  apply (drule_tac x="r" in spec, safe)
    6.19  apply (rule_tac x="no" in exI, safe)
    6.20  apply (drule_tac x="n*k" in spec)
    6.21 @@ -361,7 +361,7 @@
    6.22  lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
    6.23  apply (drule summable_convergent_sumr_iff [THEN iffD1])
    6.24  apply (drule convergent_Cauchy)
    6.25 -apply (simp only: Cauchy_def LIMSEQ_def, safe)
    6.26 +apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
    6.27  apply (drule_tac x="r" in spec, safe)
    6.28  apply (rule_tac x="M" in exI, safe)
    6.29  apply (drule_tac x="Suc n" in spec, simp)
    6.30 @@ -371,7 +371,7 @@
    6.31  lemma summable_Cauchy:
    6.32       "summable (f::nat \<Rightarrow> 'a::banach) =  
    6.33        (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"
    6.34 -apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def, safe)
    6.35 +apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)
    6.36  apply (drule spec, drule (1) mp)
    6.37  apply (erule exE, rule_tac x="M" in exI, clarify)
    6.38  apply (rule_tac x="m" and y="n" in linorder_le_cases)