src/HOL/Transcendental.thy
changeset 44727 d45acd50a894
parent 44726 8478eab380e9
child 44728 86f43cca4886
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 16:07:40 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 16:26:57 2011 -0700
     1.3 @@ -1430,8 +1430,7 @@
     1.4        sums  sin x"
     1.5  proof -
     1.6    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
     1.7 -    unfolding sin_def
     1.8 -    by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
     1.9 +    by (rule sin_converges [THEN sums_group], simp)
    1.10    thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
    1.11  qed
    1.12  
    1.13 @@ -1440,44 +1439,24 @@
    1.14  apply (subgoal_tac
    1.15         "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
    1.16                -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
    1.17 -     sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
    1.18 +     sums sin x")
    1.19   prefer 2
    1.20 - apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
    1.21 -apply (rotate_tac 2)
    1.22 -apply (drule sin_paired [THEN sums_unique, THEN ssubst])
    1.23 -unfolding One_nat_def
    1.24 -apply (auto simp del: fact_Suc)
    1.25 -apply (frule sums_unique)
    1.26 -apply (auto simp del: fact_Suc)
    1.27 -apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
    1.28 -apply (auto simp del: fact_Suc)
    1.29 -apply (erule sums_summable)
    1.30 -apply (case_tac "m=0")
    1.31 -apply (simp (no_asm_simp))
    1.32 -apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
    1.33 -apply (simp only: mult_less_cancel_left, simp)
    1.34 -apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
    1.35 -apply (subgoal_tac "x*x < 2*3", simp)
    1.36 -apply (rule mult_strict_mono)
    1.37 + apply (rule sin_paired [THEN sums_group], simp)
    1.38 +apply (simp del: fact_Suc)
    1.39 +apply (subst sums_unique, assumption)
    1.40 +apply (erule suminf_gt_zero [OF sums_summable, rule_format])
    1.41  apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
    1.42 -apply (subst fact_Suc)
    1.43 -apply (subst fact_Suc)
    1.44 -apply (subst fact_Suc)
    1.45 -apply (subst fact_Suc)
    1.46 -apply (subst real_of_nat_mult)
    1.47 -apply (subst real_of_nat_mult)
    1.48 -apply (subst real_of_nat_mult)
    1.49 -apply (subst real_of_nat_mult)
    1.50 -apply (simp (no_asm) add: divide_inverse del: fact_Suc)
    1.51 +apply (simp only: fact_Suc real_of_nat_mult)
    1.52 +apply (simp add: divide_inverse del: fact_Suc)
    1.53  apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
    1.54 -apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
    1.55 +apply (rule_tac c="real (Suc (Suc (4*n)))" in mult_less_imp_less_right)
    1.56  apply (auto simp add: mult_assoc simp del: fact_Suc)
    1.57 -apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
    1.58 +apply (rule_tac c="real (Suc (Suc (Suc (4*n))))" in mult_less_imp_less_right)
    1.59  apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
    1.60 -apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
    1.61 +apply (subgoal_tac "x * (x * x ^ (4*n)) = (x ^ (4*n)) * (x * x)")
    1.62  apply (erule ssubst)+
    1.63  apply (auto simp del: fact_Suc)
    1.64 -apply (subgoal_tac "0 < x ^ (4 * m) ")
    1.65 +apply (subgoal_tac "0 < x ^ (4 * n)")
    1.66   prefer 2 apply (simp only: zero_less_power)
    1.67  apply (simp (no_asm_simp) add: mult_less_cancel_left)
    1.68  apply (rule mult_strict_mono)
    1.69 @@ -1496,8 +1475,7 @@
    1.70       "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
    1.71  proof -
    1.72    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
    1.73 -    unfolding cos_def
    1.74 -    by (rule cos_converges [THEN sums_summable, THEN sums_group], simp)
    1.75 +    by (rule cos_converges [THEN sums_group], simp)
    1.76    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
    1.77  qed
    1.78