convert lemma sin_gt_zero to Isar style;
authorhuffman
Mon Sep 05 17:00:56 2011 -0700 (2011-09-05)
changeset 4472886f43cca4886
parent 44727 d45acd50a894
child 44729 32e22fda8c70
convert lemma sin_gt_zero to Isar style;
remove duplicate lemma sin_gt_zero1;
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 16:26:57 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 17:00:56 2011 -0700
     1.3 @@ -1434,37 +1434,30 @@
     1.4    thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
     1.5  qed
     1.6  
     1.7 -text {* FIXME: This is a long, ugly proof! *}
     1.8 -lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
     1.9 -apply (subgoal_tac
    1.10 -       "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
    1.11 -              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
    1.12 -     sums sin x")
    1.13 - prefer 2
    1.14 - apply (rule sin_paired [THEN sums_group], simp)
    1.15 -apply (simp del: fact_Suc)
    1.16 -apply (subst sums_unique, assumption)
    1.17 -apply (erule suminf_gt_zero [OF sums_summable, rule_format])
    1.18 -apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
    1.19 -apply (simp only: fact_Suc real_of_nat_mult)
    1.20 -apply (simp add: divide_inverse del: fact_Suc)
    1.21 -apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
    1.22 -apply (rule_tac c="real (Suc (Suc (4*n)))" in mult_less_imp_less_right)
    1.23 -apply (auto simp add: mult_assoc simp del: fact_Suc)
    1.24 -apply (rule_tac c="real (Suc (Suc (Suc (4*n))))" in mult_less_imp_less_right)
    1.25 -apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
    1.26 -apply (subgoal_tac "x * (x * x ^ (4*n)) = (x ^ (4*n)) * (x * x)")
    1.27 -apply (erule ssubst)+
    1.28 -apply (auto simp del: fact_Suc)
    1.29 -apply (subgoal_tac "0 < x ^ (4 * n)")
    1.30 - prefer 2 apply (simp only: zero_less_power)
    1.31 -apply (simp (no_asm_simp) add: mult_less_cancel_left)
    1.32 -apply (rule mult_strict_mono)
    1.33 -apply (simp_all (no_asm_simp))
    1.34 -done
    1.35 -
    1.36 -lemma sin_gt_zero1: "[|0 < x; x < 2 |] ==> 0 < sin x"
    1.37 -  by (rule sin_gt_zero)
    1.38 +lemma sin_gt_zero:
    1.39 +  assumes "0 < x" and "x < 2" shows "0 < sin x"
    1.40 +proof -
    1.41 +  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
    1.42 +  have pos: "\<forall>n. 0 < ?f n"
    1.43 +  proof
    1.44 +    fix n :: nat
    1.45 +    let ?k2 = "real (Suc (Suc (4 * n)))"
    1.46 +    let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
    1.47 +    have "x * x < ?k2 * ?k3"
    1.48 +      using assms by (intro mult_strict_mono', simp_all)
    1.49 +    hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
    1.50 +      by (intro mult_strict_right_mono zero_less_power `0 < x`)
    1.51 +    thus "0 < ?f n"
    1.52 +      by (simp del: mult_Suc,
    1.53 +        simp add: less_divide_eq mult_pos_pos field_simps del: mult_Suc)
    1.54 +  qed
    1.55 +  have sums: "?f sums sin x"
    1.56 +    by (rule sin_paired [THEN sums_group], simp)
    1.57 +  show "0 < sin x"
    1.58 +    unfolding sums_unique [OF sums]
    1.59 +    using sums_summable [OF sums] pos
    1.60 +    by (rule suminf_gt_zero)
    1.61 +qed
    1.62  
    1.63  lemma cos_double_less_one: "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"
    1.64  apply (cut_tac x = x in sin_gt_zero)