src/HOL/Series.thy
changeset 31336 e17f13cd1280
parent 31017 2c227493ea56
child 32707 836ec9d0a0c8
     1.1 --- a/src/HOL/Series.thy	Thu May 28 22:54:57 2009 -0700
     1.2 +++ b/src/HOL/Series.thy	Thu May 28 22:57:17 2009 -0700
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5  lemma series_zero: 
     1.6       "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
     1.7 -apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
     1.8 +apply (simp add: sums_def LIMSEQ_iff diff_minus[symmetric], safe)
     1.9  apply (rule_tac x = n in exI)
    1.10  apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
    1.11  done
    1.12 @@ -264,7 +264,7 @@
    1.13       "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
    1.14  apply (drule summable_sums)
    1.15  apply (simp only: sums_def sumr_group)
    1.16 -apply (unfold LIMSEQ_def, safe)
    1.17 +apply (unfold LIMSEQ_iff, safe)
    1.18  apply (drule_tac x="r" in spec, safe)
    1.19  apply (rule_tac x="no" in exI, safe)
    1.20  apply (drule_tac x="n*k" in spec)
    1.21 @@ -361,7 +361,7 @@
    1.22  lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
    1.23  apply (drule summable_convergent_sumr_iff [THEN iffD1])
    1.24  apply (drule convergent_Cauchy)
    1.25 -apply (simp only: Cauchy_def LIMSEQ_def, safe)
    1.26 +apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
    1.27  apply (drule_tac x="r" in spec, safe)
    1.28  apply (rule_tac x="M" in exI, safe)
    1.29  apply (drule_tac x="Suc n" in spec, simp)
    1.30 @@ -371,7 +371,7 @@
    1.31  lemma summable_Cauchy:
    1.32       "summable (f::nat \<Rightarrow> 'a::banach) =  
    1.33        (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"
    1.34 -apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def, safe)
    1.35 +apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)
    1.36  apply (drule spec, drule (1) mp)
    1.37  apply (erule exE, rule_tac x="M" in exI, clarify)
    1.38  apply (rule_tac x="m" and y="n" in linorder_le_cases)