# HG changeset patch
# User huffman
# Date 1156369247 -7200
# Node ID 4bd5cd97c5475e197db1aa920b641891b4ded73f
# Parent  eba80f91e3fccf0742aee1acc5155dfe9949ce54
speed up proof of summable_Cauchy

diff -r eba80f91e3fc -r 4bd5cd97c547 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Aug 23 22:44:32 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Wed Aug 23 23:40:47 2006 +0200
@@ -346,18 +346,21 @@
 lemma summable_Cauchy:
      "summable f =  
       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
-apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
-apply (drule_tac [!] spec, auto)
-apply (rule_tac x = M in exI)
-apply (rule_tac [2] x = N in exI, auto)
-apply (cut_tac [!] m = m and n = n in less_linear, auto)
-apply (frule le_less_trans [THEN less_imp_le], assumption)
-apply (drule_tac x = n in spec, simp)
-apply (drule_tac x = m in spec)
-apply(simp add: setsum_diff[symmetric])
-apply(subst abs_minus_commute)
-apply(simp add: setsum_diff[symmetric])
-apply(simp add: setsum_diff[symmetric])
+apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus [symmetric], 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)
+apply (frule (1) order_trans)
+apply (drule_tac x="n" in spec, drule (1) mp)
+apply (drule_tac x="m" in spec, drule (1) mp)
+apply (simp add: setsum_diff [symmetric])
+apply simp
+apply (drule spec, drule (1) mp)
+apply (erule exE, rule_tac x="N" in exI, clarify)
+apply (rule_tac x="m" and y="n" in linorder_le_cases)
+apply (subst abs_minus_commute)
+apply (simp add: setsum_diff [symmetric])
+apply (simp add: setsum_diff [symmetric])
 done
 
 text{*Comparison test*}