12224

1 
(* Title : MacLaurin.thy


2 
Author : Jacques D. Fleuriot


3 
Copyright : 2001 University of Edinburgh


4 
Description : MacLaurin series


5 
*)


6 

14738

7 
theory MacLaurin = Log


8 
files ("MacLaurin_lemmas.ML"):


9 


10 
use "MacLaurin_lemmas.ML"


11 


12 
lemma Maclaurin_sin_bound:


13 
"abs(sin x  sumr 0 n (%m. (if even m then 0 else (( 1) ^ ((m  (Suc 0)) div 2)) / real (fact m)) *


14 
x ^ m)) <= inverse(real (fact n)) * abs(x) ^ n"


15 
proof 


16 
have "!! x (y::real). x <= 1 \<Longrightarrow> 0 <= y \<Longrightarrow> x * y \<le> 1 * y"


17 
by (rule_tac mult_right_mono,simp_all)


18 
note est = this[simplified]


19 
show ?thesis


20 
apply (cut_tac f=sin and n=n and x=x and


21 
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)"


22 
in Maclaurin_all_le_objl)


23 
apply (tactic{* (Step_tac 1) *})


24 
apply (simp)


25 
apply (subst mod_Suc_eq_Suc_mod)


26 
apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*})


27 
apply (tactic{* Step_tac 1 *})


28 
apply (simp)+


29 
apply (rule DERIV_minus, simp+)


30 
apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)


31 
apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *})


32 
apply (tactic {* rtac (ARITH_PROVE "[x = y; abs u <= (v::real) ] ==> abs ((x + u)  y) <= v") 1 *})


33 
apply (rule sumr_fun_eq)


34 
apply (tactic{* Step_tac 1 *})


35 
apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*})


36 
apply (subst even_even_mod_4_iff)


37 
apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *})


38 
apply (tactic{* Step_tac 1 *})


39 
apply (simp)


40 
apply (simp_all add:even_num_iff)


41 
apply (drule lemma_even_mod_4_div_2[simplified])


42 
apply(simp add: numeral_2_eq_2 real_divide_def)


43 
apply (drule lemma_odd_mod_4_div_2 );


44 
apply (simp add: numeral_2_eq_2 real_divide_def)


45 
apply (auto intro: real_mult_le_lemma mult_right_mono simp add: est mult_pos_le mult_ac real_divide_def abs_mult abs_inverse power_abs[symmetric])


46 
done


47 
qed


48 


49 
end 