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
```     1 (*  Title       : MacLaurin.thy
```
```     2     Author      : Jacques D. Fleuriot
```
```     3     Copyright   : 2001 University of Edinburgh
```
```     4     Description : MacLaurin series
```
```     5 *)
```
```     6
```
```     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`