src/HOL/Hyperreal/MacLaurin.thy
author obua
Tue May 11 20:11:08 2004 +0200 (2004-05-11)
changeset 14738 83f1a514dcb4
parent 12224 02df7cbe7d25
child 15079 2ef899e4526d
permissions -rw-r--r--
changes made due to new Ring_and_Field theory
paulson@12224
     1
(*  Title       : MacLaurin.thy
paulson@12224
     2
    Author      : Jacques D. Fleuriot
paulson@12224
     3
    Copyright   : 2001 University of Edinburgh
paulson@12224
     4
    Description : MacLaurin series
paulson@12224
     5
*)
paulson@12224
     6
obua@14738
     7
theory MacLaurin = Log
obua@14738
     8
files ("MacLaurin_lemmas.ML"):
obua@14738
     9
obua@14738
    10
use "MacLaurin_lemmas.ML"
obua@14738
    11
obua@14738
    12
lemma Maclaurin_sin_bound: 
obua@14738
    13
  "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * 
obua@14738
    14
  x ^ m))  <= inverse(real (fact n)) * abs(x) ^ n"
obua@14738
    15
proof -
obua@14738
    16
  have "!! x (y::real). x <= 1 \<Longrightarrow> 0 <= y \<Longrightarrow> x * y \<le> 1 * y" 
obua@14738
    17
    by (rule_tac mult_right_mono,simp_all)
obua@14738
    18
  note est = this[simplified]
obua@14738
    19
  show ?thesis
obua@14738
    20
    apply (cut_tac f=sin and n=n and x=x and 
obua@14738
    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)"
obua@14738
    22
      in Maclaurin_all_le_objl)
obua@14738
    23
    apply (tactic{* (Step_tac 1) *})
obua@14738
    24
    apply (simp)
obua@14738
    25
    apply (subst mod_Suc_eq_Suc_mod)
obua@14738
    26
    apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*})
obua@14738
    27
    apply (tactic{* Step_tac 1 *})
obua@14738
    28
    apply (simp)+
obua@14738
    29
    apply (rule DERIV_minus, simp+)
obua@14738
    30
    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
obua@14738
    31
    apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *})
obua@14738
    32
    apply (tactic {* rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1 *})
obua@14738
    33
    apply (rule sumr_fun_eq)
obua@14738
    34
    apply (tactic{* Step_tac 1 *})
obua@14738
    35
    apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*})
obua@14738
    36
    apply (subst even_even_mod_4_iff)
obua@14738
    37
    apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *})
obua@14738
    38
    apply (tactic{* Step_tac 1 *})
obua@14738
    39
    apply (simp)
obua@14738
    40
    apply (simp_all add:even_num_iff)
obua@14738
    41
    apply (drule lemma_even_mod_4_div_2[simplified])
obua@14738
    42
    apply(simp add: numeral_2_eq_2 real_divide_def)
obua@14738
    43
    apply (drule lemma_odd_mod_4_div_2 );
obua@14738
    44
    apply (simp add: numeral_2_eq_2 real_divide_def)
obua@14738
    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])
obua@14738
    46
    done
obua@14738
    47
qed
obua@14738
    48
obua@14738
    49
end