# HG changeset patch
# User huffman
# Date 1315265217 25200
# Node ID d45acd50a894f0ab53c51f697a7b005c3b39ab36
# Parent  8478eab380e9af177cb4ccaf2a60d27bc5c2b49e
modify lemma sums_group, and shorten proofs that use it

diff -r 8478eab380e9 -r d45acd50a894 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Sep 05 16:07:40 2011 -0700
+++ b/src/HOL/Series.thy	Mon Sep 05 16:26:57 2011 -0700
@@ -304,8 +304,7 @@
 
 lemma sums_group:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
-  shows "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
-apply (drule summable_sums)
+  shows "\<lbrakk>f sums s; 0 < k\<rbrakk> \<Longrightarrow> (\<lambda>n. setsum f {n*k..<n*k+k}) sums s"
 apply (simp only: sums_def sumr_group)
 apply (unfold LIMSEQ_iff, safe)
 apply (drule_tac x="r" in spec, safe)
@@ -380,7 +379,7 @@
 apply assumption
 apply simp
 apply (drule_tac k="k" in summable_ignore_initial_segment)
-apply (drule_tac k="Suc (Suc 0)" in sums_group, simp)
+apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
 apply simp
 apply (frule sums_unique)
 apply (drule sums_summable)
diff -r 8478eab380e9 -r d45acd50a894 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Sep 05 16:07:40 2011 -0700
+++ b/src/HOL/Transcendental.thy	Mon Sep 05 16:26:57 2011 -0700
@@ -1430,8 +1430,7 @@
       sums  sin x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
-    unfolding sin_def
-    by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
+    by (rule sin_converges [THEN sums_group], simp)
   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
 qed
 
@@ -1440,44 +1439,24 @@
 apply (subgoal_tac
        "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
               -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
-     sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
+     sums sin x")
  prefer 2
- apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
-apply (rotate_tac 2)
-apply (drule sin_paired [THEN sums_unique, THEN ssubst])
-unfolding One_nat_def
-apply (auto simp del: fact_Suc)
-apply (frule sums_unique)
-apply (auto simp del: fact_Suc)
-apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc)
-apply (erule sums_summable)
-apply (case_tac "m=0")
-apply (simp (no_asm_simp))
-apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
-apply (simp only: mult_less_cancel_left, simp)
-apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
-apply (subgoal_tac "x*x < 2*3", simp)
-apply (rule mult_strict_mono)
+ apply (rule sin_paired [THEN sums_group], simp)
+apply (simp del: fact_Suc)
+apply (subst sums_unique, assumption)
+apply (erule suminf_gt_zero [OF sums_summable, rule_format])
 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (subst real_of_nat_mult)
-apply (subst real_of_nat_mult)
-apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse del: fact_Suc)
+apply (simp only: fact_Suc real_of_nat_mult)
+apply (simp add: divide_inverse del: fact_Suc)
 apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
-apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
+apply (rule_tac c="real (Suc (Suc (4*n)))" in mult_less_imp_less_right)
 apply (auto simp add: mult_assoc simp del: fact_Suc)
-apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
+apply (rule_tac c="real (Suc (Suc (Suc (4*n))))" in mult_less_imp_less_right)
 apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
-apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
+apply (subgoal_tac "x * (x * x ^ (4*n)) = (x ^ (4*n)) * (x * x)")
 apply (erule ssubst)+
 apply (auto simp del: fact_Suc)
-apply (subgoal_tac "0 < x ^ (4 * m) ")
+apply (subgoal_tac "0 < x ^ (4 * n)")
  prefer 2 apply (simp only: zero_less_power)
 apply (simp (no_asm_simp) add: mult_less_cancel_left)
 apply (rule mult_strict_mono)
@@ -1496,8 +1475,7 @@
      "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
-    unfolding cos_def
-    by (rule cos_converges [THEN sums_summable, THEN sums_group], simp)
+    by (rule cos_converges [THEN sums_group], simp)
   thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
 qed