src/HOL/Hyperreal/MacLaurin.thy
 changeset 14738 83f1a514dcb4 parent 12224 02df7cbe7d25 child 15079 2ef899e4526d
```     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue May 11 14:00:02 2004 +0200
1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue May 11 20:11:08 2004 +0200
1.3 @@ -4,4 +4,46 @@
1.4      Description : MacLaurin series
1.5  *)
1.6
1.7 -MacLaurin = Log
1.8 +theory MacLaurin = Log
1.9 +files ("MacLaurin_lemmas.ML"):
1.10 +
1.11 +use "MacLaurin_lemmas.ML"
1.12 +
1.13 +lemma Maclaurin_sin_bound:
1.14 +  "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.15 +  x ^ m))  <= inverse(real (fact n)) * abs(x) ^ n"
1.16 +proof -
1.17 +  have "!! x (y::real). x <= 1 \<Longrightarrow> 0 <= y \<Longrightarrow> x * y \<le> 1 * y"
1.18 +    by (rule_tac mult_right_mono,simp_all)
1.19 +  note est = this[simplified]
1.20 +  show ?thesis
1.21 +    apply (cut_tac f=sin and n=n and x=x and
1.22 +      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.23 +      in Maclaurin_all_le_objl)
1.24 +    apply (tactic{* (Step_tac 1) *})
1.25 +    apply (simp)
1.26 +    apply (subst mod_Suc_eq_Suc_mod)
1.27 +    apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*})
1.28 +    apply (tactic{* Step_tac 1 *})
1.29 +    apply (simp)+
1.30 +    apply (rule DERIV_minus, simp+)
1.31 +    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
1.32 +    apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *})
1.33 +    apply (tactic {* rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1 *})
1.34 +    apply (rule sumr_fun_eq)
1.35 +    apply (tactic{* Step_tac 1 *})
1.36 +    apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*})
1.37 +    apply (subst even_even_mod_4_iff)
1.38 +    apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *})
1.39 +    apply (tactic{* Step_tac 1 *})
1.40 +    apply (simp)