src/HOL/MacLaurin.thy
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 44890 22f665a2e91c child 49962 a8cc904a6820 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
 haftmann@28952 ` 1` ```(* Author : Jacques D. Fleuriot ``` paulson@12224 ` 2` ``` Copyright : 2001 University of Edinburgh ``` paulson@15079 ` 3` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` bulwahn@41120 ` 4` ``` Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard HÃ¤upler, 2005 ``` paulson@12224 ` 5` ```*) ``` paulson@12224 ` 6` paulson@15944 ` 7` ```header{*MacLaurin Series*} ``` paulson@15944 ` 8` nipkow@15131 ` 9` ```theory MacLaurin ``` chaieb@29811 ` 10` ```imports Transcendental ``` nipkow@15131 ` 11` ```begin ``` paulson@15079 ` 12` paulson@15079 ` 13` ```subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} ``` paulson@15079 ` 14` paulson@15079 ` 15` ```text{*This is a very long, messy proof even now that it's been broken down ``` paulson@15079 ` 16` ```into lemmas.*} ``` paulson@15079 ` 17` paulson@15079 ` 18` ```lemma Maclaurin_lemma: ``` paulson@15079 ` 19` ``` "0 < h ==> ``` nipkow@15539 ` 20` ``` \B. f h = (\m=0.. fact (Suc m - n) = (Suc m - n) * fact (m - n)" ``` avigad@32038 ` 30` ``` by (subst fact_reduce_nat, auto) ``` avigad@32038 ` 31` paulson@15079 ` 32` ```lemma Maclaurin_lemma2: ``` hoelzl@41166 ` 33` ``` fixes B ``` bulwahn@41120 ` 34` ``` assumes DERIV : "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t" ``` hoelzl@41166 ` 35` ``` and INIT : "n = Suc k" ``` hoelzl@41166 ` 36` ``` defines "difg \ (\m t. diff m t - ((\p = 0.. (\m t. diff m t - ?difg m t)") ``` bulwahn@41120 ` 38` ``` shows "\m t. m < n & 0 \ t & t \ h --> DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 39` ```proof (rule allI impI)+ ``` hoelzl@41166 ` 40` ``` fix m t assume INIT2: "m < n & 0 \ t & t \ h" ``` hoelzl@41166 ` 41` ``` have "DERIV (difg m) t :> diff (Suc m) t - ``` hoelzl@41166 ` 42` ``` ((\x = 0..x = 0..x = 0..x::nat. real (fact x) + real x * real (fact x) \ 0" ``` hoelzl@41166 ` 53` ``` by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff) ``` hoelzl@41166 ` 54` ``` have "\x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) = ``` hoelzl@41166 ` 55` ``` diff (Suc m + x) 0 * t^x / real (fact x)" ``` hoelzl@41166 ` 56` ``` by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2]) ``` hoelzl@41166 ` 57` ``` moreover ``` hoelzl@41166 ` 58` ``` have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) = ``` hoelzl@41166 ` 59` ``` B * (t ^ (n - Suc m) / real (fact (n - Suc m)))" ``` hoelzl@41166 ` 60` ``` using `0 < n - m` by (simp add: fact_reduce_nat) ``` hoelzl@41166 ` 61` ``` ultimately show "DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 62` ``` unfolding difg_def by simp ``` bulwahn@41120 ` 63` ```qed ``` avigad@32038 ` 64` paulson@15079 ` 65` ```lemma Maclaurin: ``` huffman@29187 ` 66` ``` assumes h: "0 < h" ``` huffman@29187 ` 67` ``` assumes n: "0 < n" ``` huffman@29187 ` 68` ``` assumes diff_0: "diff 0 = f" ``` huffman@29187 ` 69` ``` assumes diff_Suc: ``` huffman@29187 ` 70` ``` "\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` huffman@29187 ` 71` ``` shows ``` huffman@29187 ` 72` ``` "\t. 0 < t & t < h & ``` paulson@15079 ` 73` ``` f h = ``` nipkow@15539 ` 74` ``` setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..m = 0..real) / real (fact m) * h ^ m) + ``` huffman@29187 ` 82` ``` B * (h ^ n / real (fact n))" ``` huffman@29187 ` 83` ``` using Maclaurin_lemma [OF h] .. ``` huffman@29187 ` 84` hoelzl@41166 ` 85` ``` def g \ "(\t. f t - ``` hoelzl@41166 ` 86` ``` (setsum (\m. (diff m 0 / real(fact m)) * t^m) {0.. "(%m t. diff m t - ``` huffman@29187 ` 96` ``` (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..(m\nat) t\real. ``` huffman@29187 ` 103` ``` m < n \ (0\real) \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 104` ``` using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2) ``` huffman@29187 ` 105` huffman@29187 ` 106` ``` have difg_eq_0: "\m. m < n --> difg m 0 = 0" ``` huffman@29187 ` 107` ``` apply clarify ``` huffman@29187 ` 108` ``` apply (simp add: m difg_def) ``` huffman@29187 ` 109` ``` apply (frule less_iff_Suc_add [THEN iffD1], clarify) ``` huffman@29187 ` 110` ``` apply (simp del: setsum_op_ivl_Suc) ``` huffman@30082 ` 111` ``` apply (insert sumr_offset4 [of "Suc 0"]) ``` avigad@32047 ` 112` ``` apply (simp del: setsum_op_ivl_Suc fact_Suc) ``` huffman@29187 ` 113` ``` done ``` huffman@29187 ` 114` huffman@29187 ` 115` ``` have isCont_difg: "\m x. \m < n; 0 \ x; x \ h\ \ isCont (difg m) x" ``` huffman@29187 ` 116` ``` by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 117` huffman@29187 ` 118` ``` have differentiable_difg: ``` huffman@29187 ` 119` ``` "\m x. \m < n; 0 \ x; x \ h\ \ difg m differentiable x" ``` huffman@29187 ` 120` ``` by (rule differentiableI [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 121` huffman@29187 ` 122` ``` have difg_Suc_eq_0: "\m t. \m < n; 0 \ t; t \ h; DERIV (difg m) t :> 0\ ``` huffman@29187 ` 123` ``` \ difg (Suc m) t = 0" ``` huffman@29187 ` 124` ``` by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 125` huffman@29187 ` 126` ``` have "m < n" using m by simp ``` huffman@29187 ` 127` huffman@29187 ` 128` ``` have "\t. 0 < t \ t < h \ DERIV (difg m) t :> 0" ``` huffman@29187 ` 129` ``` using `m < n` ``` huffman@29187 ` 130` ``` proof (induct m) ``` hoelzl@41166 ` 131` ``` case 0 ``` huffman@29187 ` 132` ``` show ?case ``` huffman@29187 ` 133` ``` proof (rule Rolle) ``` huffman@29187 ` 134` ``` show "0 < h" by fact ``` huffman@29187 ` 135` ``` show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) ``` huffman@29187 ` 136` ``` show "\x. 0 \ x \ x \ h \ isCont (difg (0\nat)) x" ``` huffman@29187 ` 137` ``` by (simp add: isCont_difg n) ``` huffman@29187 ` 138` ``` show "\x. 0 < x \ x < h \ difg (0\nat) differentiable x" ``` huffman@29187 ` 139` ``` by (simp add: differentiable_difg n) ``` huffman@29187 ` 140` ``` qed ``` huffman@29187 ` 141` ``` next ``` hoelzl@41166 ` 142` ``` case (Suc m') ``` huffman@29187 ` 143` ``` hence "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0" by simp ``` huffman@29187 ` 144` ``` then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast ``` huffman@29187 ` 145` ``` have "\t'. 0 < t' \ t' < t \ DERIV (difg (Suc m')) t' :> 0" ``` huffman@29187 ` 146` ``` proof (rule Rolle) ``` huffman@29187 ` 147` ``` show "0 < t" by fact ``` huffman@29187 ` 148` ``` show "difg (Suc m') 0 = difg (Suc m') t" ``` huffman@29187 ` 149` ``` using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0) ``` huffman@29187 ` 150` ``` show "\x. 0 \ x \ x \ t \ isCont (difg (Suc m')) x" ``` huffman@29187 ` 151` ``` using `t < h` `Suc m' < n` by (simp add: isCont_difg) ``` huffman@29187 ` 152` ``` show "\x. 0 < x \ x < t \ difg (Suc m') differentiable x" ``` huffman@29187 ` 153` ``` using `t < h` `Suc m' < n` by (simp add: differentiable_difg) ``` huffman@29187 ` 154` ``` qed ``` huffman@29187 ` 155` ``` thus ?case ``` huffman@29187 ` 156` ``` using `t < h` by auto ``` huffman@29187 ` 157` ``` qed ``` huffman@29187 ` 158` huffman@29187 ` 159` ``` then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast ``` huffman@29187 ` 160` huffman@29187 ` 161` ``` hence "difg (Suc m) t = 0" ``` huffman@29187 ` 162` ``` using `m < n` by (simp add: difg_Suc_eq_0) ``` huffman@29187 ` 163` huffman@29187 ` 164` ``` show ?thesis ``` huffman@29187 ` 165` ``` proof (intro exI conjI) ``` huffman@29187 ` 166` ``` show "0 < t" by fact ``` huffman@29187 ` 167` ``` show "t < h" by fact ``` huffman@29187 ` 168` ``` show "f h = ``` huffman@29187 ` 169` ``` (\m = 0..0 & diff 0 = f & ``` nipkow@25134 ` 178` ``` (\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` nipkow@25134 ` 179` ``` --> (\t. 0 < t & t < h & ``` nipkow@25134 ` 180` ``` f h = (\m=0..m t. ``` bulwahn@41120 ` 188` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 189` ``` shows "\t. 0 < t \ t \ h \ f h = ``` bulwahn@41120 ` 190` ``` (\m=0.. 0" by simp ``` bulwahn@41120 ` 197` ``` from INIT1 this INIT2 DERIV have "\t>0. t < h \ ``` bulwahn@41120 ` 198` ``` f h = ``` hoelzl@41166 ` 199` ``` (\m = 0..m t. ``` paulson@15079 ` 207` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` paulson@15079 ` 208` ``` --> (\t. 0 < t & ``` paulson@15079 ` 209` ``` t \ h & ``` paulson@15079 ` 210` ``` f h = ``` nipkow@15539 ` 211` ``` (\m=0..m t. m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 218` ``` shows "\t. h < t & t < 0 & ``` bulwahn@41120 ` 219` ``` f h = (\m=0..t>0. t < - h \ ``` bulwahn@41120 ` 226` ``` f (- (- h)) = ``` bulwahn@41120 ` 227` ``` (\m = 0.. ``` bulwahn@41120 ` 239` ``` - t < 0 \ ``` bulwahn@41120 ` 240` ``` f h = ``` bulwahn@41120 ` 241` ``` (\m = 0.. 0 & diff 0 = f & ``` paulson@15079 ` 248` ``` (\m t. ``` paulson@15079 ` 249` ``` m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t)) ``` paulson@15079 ` 250` ``` --> (\t. h < t & ``` paulson@15079 ` 251` ``` t < 0 & ``` paulson@15079 ` 252` ``` f h = ``` nipkow@15539 ` 253` ``` (\m=0..0 \ ``` nipkow@25134 ` 264` ``` diff 0 0 = ``` nipkow@25134 ` 265` ``` (\m = 0..m t. m < n & abs t \ abs x --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 272` ``` shows "\t. abs t \ abs x & ``` paulson@15079 ` 273` ``` f x = ``` nipkow@15539 ` 274` ``` (\m=0..t. _ \ f x = ?f x t") ``` hoelzl@41166 ` 276` ```proof cases ``` hoelzl@41166 ` 277` ``` assume "n = 0" with `diff 0 = f` show ?thesis by force ``` bulwahn@41120 ` 278` ```next ``` hoelzl@41166 ` 279` ``` assume "n \ 0" ``` hoelzl@41166 ` 280` ``` show ?thesis ``` hoelzl@41166 ` 281` ``` proof (cases rule: linorder_cases) ``` hoelzl@41166 ` 282` ``` assume "x = 0" with `n \ 0` `diff 0 = f` DERIV ``` hoelzl@41166 ` 283` ``` have "\0\ \ \x\ \ f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma) ``` hoelzl@41166 ` 284` ``` thus ?thesis .. ``` bulwahn@41120 ` 285` ``` next ``` hoelzl@41166 ` 286` ``` assume "x < 0" ``` hoelzl@41166 ` 287` ``` with `n \ 0` DERIV ``` hoelzl@41166 ` 288` ``` have "\t>x. t < 0 \ diff 0 x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 289` ``` then guess t .. ``` hoelzl@41166 ` 290` ``` with `x < 0` `diff 0 = f` have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 291` ``` thus ?thesis .. ``` hoelzl@41166 ` 292` ``` next ``` hoelzl@41166 ` 293` ``` assume "x > 0" ``` hoelzl@41166 ` 294` ``` with `n \ 0` `diff 0 = f` DERIV ``` hoelzl@41166 ` 295` ``` have "\t>0. t < x \ diff 0 x = ?f x t" by (intro Maclaurin) auto ``` hoelzl@41166 ` 296` ``` then guess t .. ``` hoelzl@41166 ` 297` ``` with `x > 0` `diff 0 = f` have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 298` ``` thus ?thesis .. ``` bulwahn@41120 ` 299` ``` qed ``` bulwahn@41120 ` 300` ```qed ``` bulwahn@41120 ` 301` paulson@15079 ` 302` ```lemma Maclaurin_all_lt: ``` bulwahn@41120 ` 303` ``` assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \ 0" ``` bulwahn@41120 ` 304` ``` and DERIV: "\m x. DERIV (diff m) x :> diff(Suc m) x" ``` hoelzl@41166 ` 305` ``` shows "\t. 0 < abs t & abs t < abs x & f x = ``` hoelzl@41166 ` 306` ``` (\m=0..t. _ \ _ \ f x = ?f x t") ``` hoelzl@41166 ` 308` ```proof (cases rule: linorder_cases) ``` hoelzl@41166 ` 309` ``` assume "x = 0" with INIT3 show "?thesis".. ``` hoelzl@41166 ` 310` ```next ``` hoelzl@41166 ` 311` ``` assume "x < 0" ``` hoelzl@41166 ` 312` ``` with assms have "\t>x. t < 0 \ f x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 313` ``` then guess t .. ``` hoelzl@41166 ` 314` ``` with `x < 0` have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 315` ``` thus ?thesis .. ``` hoelzl@41166 ` 316` ```next ``` hoelzl@41166 ` 317` ``` assume "x > 0" ``` hoelzl@41166 ` 318` ``` with assms have "\t>0. t < x \ f x = ?f x t " by (intro Maclaurin) auto ``` hoelzl@41166 ` 319` ``` then guess t .. ``` hoelzl@41166 ` 320` ``` with `x > 0` have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 321` ``` thus ?thesis .. ``` bulwahn@41120 ` 322` ```qed ``` bulwahn@41120 ` 323` paulson@15079 ` 324` paulson@15079 ` 325` ```lemma Maclaurin_all_lt_objl: ``` paulson@15079 ` 326` ``` "diff 0 = f & ``` paulson@15079 ` 327` ``` (\m x. DERIV (diff m) x :> diff(Suc m) x) & ``` nipkow@25162 ` 328` ``` x ~= 0 & n > 0 ``` paulson@15079 ` 329` ``` --> (\t. 0 < abs t & abs t < abs x & ``` nipkow@15539 ` 330` ``` f x = (\m=0.. n \ 0 --> ``` nipkow@15539 ` 337` ``` (\m=0..m x. DERIV (diff m) x :> diff (Suc m) x" ``` hoelzl@41166 ` 345` ``` shows "\t. abs t \ abs x & f x = ``` hoelzl@41166 ` 346` ``` (\m=0..t. _ \ f x = ?f x t") ``` hoelzl@41166 ` 348` ```proof cases ``` hoelzl@41166 ` 349` ``` assume "n = 0" with INIT show ?thesis by force ``` bulwahn@41120 ` 350` ``` next ``` hoelzl@41166 ` 351` ``` assume "n \ 0" ``` hoelzl@41166 ` 352` ``` show ?thesis ``` hoelzl@41166 ` 353` ``` proof cases ``` hoelzl@41166 ` 354` ``` assume "x = 0" ``` hoelzl@41166 ` 355` ``` with `n \ 0` have "(\m = 0.. 0` have " \0\ \ \x\ \ f x = ?f x 0" by force ``` hoelzl@41166 ` 358` ``` thus ?thesis .. ``` hoelzl@41166 ` 359` ``` next ``` hoelzl@41166 ` 360` ``` assume "x \ 0" ``` hoelzl@41166 ` 361` ``` with INIT `n \ 0` DERIV have "\t. 0 < \t\ \ \t\ < \x\ \ f x = ?f x t" ``` hoelzl@41166 ` 362` ``` by (intro Maclaurin_all_lt) auto ``` hoelzl@41166 ` 363` ``` then guess t .. ``` hoelzl@41166 ` 364` ``` hence "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 365` ``` thus ?thesis .. ``` bulwahn@41120 ` 366` ``` qed ``` bulwahn@41120 ` 367` ```qed ``` bulwahn@41120 ` 368` paulson@15079 ` 369` ```lemma Maclaurin_all_le_objl: "diff 0 = f & ``` paulson@15079 ` 370` ``` (\m x. DERIV (diff m) x :> diff (Suc m) x) ``` paulson@15079 ` 371` ``` --> (\t. abs t \ abs x & ``` nipkow@15539 ` 372` ``` f x = (\m=0.. 0 |] ``` paulson@15079 ` 380` ``` ==> (\t. 0 < abs t & ``` paulson@15079 ` 381` ``` abs t < abs x & ``` nipkow@15539 ` 382` ``` exp x = (\m=0..t. abs t \ abs x & ``` nipkow@15539 ` 389` ``` exp x = (\m=0..0 --> Suc (Suc (2 * n - 2)) = 2*n" ``` paulson@15251 ` 402` ```by (induct "n", auto) ``` paulson@15079 ` 403` paulson@15079 ` 404` ```lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: ``` nipkow@25134 ` 405` ``` "n\0 --> Suc (Suc (4*n - 2)) = 4*n" ``` paulson@15251 ` 406` ```by (induct "n", auto) ``` paulson@15079 ` 407` paulson@15079 ` 408` ```lemma Suc_mult_two_diff_one [rule_format, simp]: ``` nipkow@25134 ` 409` ``` "n\0 --> Suc (2 * n - 1) = 2*n" ``` paulson@15251 ` 410` ```by (induct "n", auto) ``` paulson@15079 ` 411` paulson@15234 ` 412` paulson@15234 ` 413` ```text{*It is unclear why so many variant results are needed.*} ``` paulson@15079 ` 414` huffman@36974 ` 415` ```lemma sin_expansion_lemma: ``` hoelzl@41166 ` 416` ``` "sin (x + real (Suc m) * pi / 2) = ``` huffman@36974 ` 417` ``` cos (x + real (m) * pi / 2)" ``` huffman@36974 ` 418` ```by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto) ``` huffman@36974 ` 419` paulson@15079 ` 420` ```lemma Maclaurin_sin_expansion2: ``` paulson@15079 ` 421` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 422` ``` sin x = ``` huffman@44306 ` 423` ``` (\m=0..t. sin x = ``` huffman@44306 ` 443` ``` (\m=0.. 0; 0 < x |] ==> ``` paulson@15079 ` 451` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 452` ``` sin x = ``` huffman@44306 ` 453` ``` (\m=0.. ``` paulson@15079 ` 468` ``` \t. 0 < t & t \ x & ``` paulson@15079 ` 469` ``` sin x = ``` huffman@44306 ` 470` ``` (\m=0..m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1" ``` paulson@15251 ` 488` ```by (induct "n", auto) ``` paulson@15079 ` 489` huffman@36974 ` 490` ```lemma cos_expansion_lemma: ``` huffman@36974 ` 491` ``` "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)" ``` huffman@36974 ` 492` ```by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto) ``` huffman@36974 ` 493` paulson@15079 ` 494` ```lemma Maclaurin_cos_expansion: ``` paulson@15079 ` 495` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 496` ``` cos x = ``` huffman@44306 ` 497` ``` (\m=0.. 0 |] ==> ``` paulson@15079 ` 515` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 516` ``` cos x = ``` huffman@44306 ` 517` ``` (\m=0.. 0 |] ==> ``` paulson@15079 ` 531` ``` \t. x < t & t < 0 & ``` paulson@15079 ` 532` ``` cos x = ``` huffman@44306 ` 533` ``` (\m=0.. (v::real) |] ==> \(x + u) - y\ \ v" ``` paulson@15079 ` 551` ```by auto ``` paulson@15079 ` 552` paulson@15079 ` 553` ```lemma Maclaurin_sin_bound: ``` huffman@44306 ` 554` ``` "abs(sin x - (\m=0.. inverse(real (fact n)) * \x\ ^ n" ``` obua@14738 ` 556` ```proof - ``` paulson@15079 ` 557` ``` have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 1 * y" ``` obua@14738 ` 558` ``` by (rule_tac mult_right_mono,simp_all) ``` obua@14738 ` 559` ``` note est = this[simplified] ``` huffman@22985 ` 560` ``` let ?diff = "\(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)" ``` huffman@22985 ` 561` ``` have diff_0: "?diff 0 = sin" by simp ``` huffman@22985 ` 562` ``` have DERIV_diff: "\m x. DERIV (?diff m) x :> ?diff (Suc m) x" ``` huffman@22985 ` 563` ``` apply (clarify) ``` huffman@22985 ` 564` ``` apply (subst (1 2 3) mod_Suc_eq_Suc_mod) ``` huffman@22985 ` 565` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` hoelzl@31881 ` 566` ``` apply (safe, auto intro!: DERIV_intros) ``` huffman@22985 ` 567` ``` done ``` huffman@22985 ` 568` ``` from Maclaurin_all_le [OF diff_0 DERIV_diff] ``` huffman@22985 ` 569` ``` obtain t where t1: "\t\ \ \x\" and ``` huffman@22985 ` 570` ``` t2: "sin x = (\m = 0..m. ?diff m 0 = (if even m then 0 ``` huffman@23177 ` 574` ``` else -1 ^ ((m - Suc 0) div 2))" ``` huffman@22985 ` 575` ``` apply (subst even_even_mod_4_iff) ``` huffman@22985 ` 576` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` huffman@22985 ` 577` ``` apply (elim disjE, simp_all) ``` huffman@22985 ` 578` ``` apply (safe dest!: mod_eqD, simp_all) ``` huffman@22985 ` 579` ``` done ``` obua@14738 ` 580` ``` show ?thesis ``` huffman@44306 ` 581` ``` unfolding sin_coeff_def ``` huffman@22985 ` 582` ``` apply (subst t2) ``` paulson@15079 ` 583` ``` apply (rule sin_bound_lemma) ``` nipkow@15536 ` 584` ``` apply (rule setsum_cong[OF refl]) ``` huffman@22985 ` 585` ``` apply (subst diff_m_0, simp) ``` paulson@15079 ` 586` ``` apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono ``` hoelzl@41166 ` 587` ``` simp add: est mult_nonneg_nonneg mult_ac divide_inverse ``` paulson@16924 ` 588` ``` power_abs [symmetric] abs_mult) ``` obua@14738 ` 589` ``` done ``` obua@14738 ` 590` ```qed ``` obua@14738 ` 591` paulson@15079 ` 592` ```end ```