cleaned up proof of Maclaurin_sin_bound
authorhuffman
Thu May 17 00:45:27 2007 +0200 (2007-05-17)
changeset 22985501e6dfe4e5a
parent 22984 67d434ad9ef8
child 22986 d21d3539f6bb
cleaned up proof of Maclaurin_sin_bound
src/HOL/Hyperreal/MacLaurin.thy
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed May 16 23:07:08 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu May 17 00:45:27 2007 +0200
     1.3 @@ -560,27 +560,33 @@
     1.4    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
     1.5      by (rule_tac mult_right_mono,simp_all)
     1.6    note est = this[simplified]
     1.7 +  let ?diff = "\<lambda>(n::nat) x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)"
     1.8 +  have diff_0: "?diff 0 = sin" by simp
     1.9 +  have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
    1.10 +    apply (clarify)
    1.11 +    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    1.12 +    apply (cut_tac m=m in mod_exhaust_less_4)
    1.13 +    apply (safe, simp_all)
    1.14 +    apply (rule DERIV_minus, simp)
    1.15 +    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
    1.16 +    done
    1.17 +  from Maclaurin_all_le [OF diff_0 DERIV_diff]
    1.18 +  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
    1.19 +    t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
    1.20 +      ?diff n t / real (fact n) * x ^ n" by fast
    1.21 +  have diff_m_0:
    1.22 +    "\<And>m. ?diff m 0 = (if even m then 0
    1.23 +         else (- 1) ^ ((m - Suc 0) div 2))"
    1.24 +    apply (subst even_even_mod_4_iff)
    1.25 +    apply (cut_tac m=m in mod_exhaust_less_4)
    1.26 +    apply (elim disjE, simp_all)
    1.27 +    apply (safe dest!: mod_eqD, simp_all)
    1.28 +    done
    1.29    show ?thesis
    1.30 -    apply (cut_tac f=sin and n=n and x=x and
    1.31 -      diff = "%n x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)"
    1.32 -      in Maclaurin_all_le_objl)
    1.33 -    apply safe
    1.34 -    apply simp
    1.35 -    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    1.36 -    apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
    1.37 -    apply (rule DERIV_minus, simp+)
    1.38 -    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
    1.39 -    apply (erule ssubst)
    1.40 +    apply (subst t2)
    1.41      apply (rule sin_bound_lemma)
    1.42      apply (rule setsum_cong[OF refl])
    1.43 -    apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
    1.44 -    apply (subst even_even_mod_4_iff)
    1.45 -    apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
    1.46 -    apply (simp_all add:even_num_iff)
    1.47 -    apply (drule lemma_even_mod_4_div_2[simplified])
    1.48 -    apply(simp add: numeral_2_eq_2 divide_inverse)
    1.49 -    apply (drule lemma_odd_mod_4_div_2)
    1.50 -    apply (simp add: numeral_2_eq_2 divide_inverse)
    1.51 +    apply (subst diff_m_0, simp)
    1.52      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
    1.53                     simp add: est mult_nonneg_nonneg mult_ac divide_inverse
    1.54                            power_abs [symmetric] abs_mult)