src/HOL/MacLaurin.thy
 author hoelzl Tue Mar 18 15:53:48 2014 +0100 (2014-03-18) changeset 56193 c726ecfb22b6 parent 56181 2aa0b19e74f3 child 56238 5d147e1e18d1 permissions -rw-r--r--
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
 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 ==> ``` hoelzl@56193 ` 20` ``` \B. f h = (\m fact (Suc m - n) = (Suc m - n) * fact (m - n)" ``` avigad@32038 ` 29` ``` by (subst fact_reduce_nat, auto) ``` avigad@32038 ` 30` paulson@15079 ` 31` ```lemma Maclaurin_lemma2: ``` hoelzl@41166 ` 32` ``` fixes B ``` bulwahn@41120 ` 33` ``` assumes DERIV : "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t" ``` hoelzl@41166 ` 34` ``` and INIT : "n = Suc k" ``` hoelzl@56193 ` 35` ``` defines "difg \ (\m t. diff m t - ((\p (\m t. diff m t - ?difg m t)") ``` bulwahn@41120 ` 37` ``` shows "\m t. m < n & 0 \ t & t \ h --> DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 38` ```proof (rule allI impI)+ ``` hoelzl@41166 ` 39` ``` fix m t assume INIT2: "m < n & 0 \ t & t \ h" ``` hoelzl@41166 ` 40` ``` have "DERIV (difg m) t :> diff (Suc m) t - ``` hoelzl@56193 ` 41` ``` ((\xxxx::nat. real (fact x) + real x * real (fact x) \ 0" ``` hoelzl@41166 ` 52` ``` by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff) ``` hoelzl@41166 ` 53` ``` have "\x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) = ``` hoelzl@41166 ` 54` ``` diff (Suc m + x) 0 * t^x / real (fact x)" ``` hoelzl@41166 ` 55` ``` by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2]) ``` hoelzl@41166 ` 56` ``` moreover ``` hoelzl@41166 ` 57` ``` have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) = ``` hoelzl@41166 ` 58` ``` B * (t ^ (n - Suc m) / real (fact (n - Suc m)))" ``` hoelzl@41166 ` 59` ``` using `0 < n - m` by (simp add: fact_reduce_nat) ``` hoelzl@41166 ` 60` ``` ultimately show "DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 61` ``` unfolding difg_def by simp ``` bulwahn@41120 ` 62` ```qed ``` avigad@32038 ` 63` paulson@15079 ` 64` ```lemma Maclaurin: ``` huffman@29187 ` 65` ``` assumes h: "0 < h" ``` huffman@29187 ` 66` ``` assumes n: "0 < n" ``` huffman@29187 ` 67` ``` assumes diff_0: "diff 0 = f" ``` huffman@29187 ` 68` ``` assumes diff_Suc: ``` huffman@29187 ` 69` ``` "\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` huffman@29187 ` 70` ``` shows ``` huffman@29187 ` 71` ``` "\t. 0 < t & t < h & ``` paulson@15079 ` 72` ``` f h = ``` hoelzl@56193 ` 73` ``` setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..mreal) / real (fact m) * h ^ m) + ``` huffman@29187 ` 81` ``` B * (h ^ n / real (fact n))" ``` huffman@29187 ` 82` ``` using Maclaurin_lemma [OF h] .. ``` huffman@29187 ` 83` hoelzl@41166 ` 84` ``` def g \ "(\t. f t - ``` hoelzl@56193 ` 85` ``` (setsum (\m. (diff m 0 / real(fact m)) * t^m) {.. "(%m t. diff m t - ``` hoelzl@56193 ` 92` ``` (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..(m\nat) t\real. ``` huffman@29187 ` 99` ``` m < n \ (0\real) \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t" ``` hoelzl@41166 ` 100` ``` using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2) ``` huffman@29187 ` 101` hoelzl@56193 ` 102` ``` have difg_eq_0: "\mm x. \m < n; 0 \ x; x \ h\ \ isCont (difg m) x" ``` huffman@29187 ` 106` ``` by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 107` huffman@29187 ` 108` ``` have differentiable_difg: ``` hoelzl@56181 ` 109` ``` "\m x. \m < n; 0 \ x; x \ h\ \ difg m differentiable (at x)" ``` huffman@29187 ` 110` ``` by (rule differentiableI [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 111` huffman@29187 ` 112` ``` have difg_Suc_eq_0: "\m t. \m < n; 0 \ t; t \ h; DERIV (difg m) t :> 0\ ``` huffman@29187 ` 113` ``` \ difg (Suc m) t = 0" ``` huffman@29187 ` 114` ``` by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp ``` huffman@29187 ` 115` huffman@29187 ` 116` ``` have "m < n" using m by simp ``` huffman@29187 ` 117` huffman@29187 ` 118` ``` have "\t. 0 < t \ t < h \ DERIV (difg m) t :> 0" ``` huffman@29187 ` 119` ``` using `m < n` ``` huffman@29187 ` 120` ``` proof (induct m) ``` hoelzl@41166 ` 121` ``` case 0 ``` huffman@29187 ` 122` ``` show ?case ``` huffman@29187 ` 123` ``` proof (rule Rolle) ``` huffman@29187 ` 124` ``` show "0 < h" by fact ``` huffman@29187 ` 125` ``` show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) ``` huffman@29187 ` 126` ``` show "\x. 0 \ x \ x \ h \ isCont (difg (0\nat)) x" ``` huffman@29187 ` 127` ``` by (simp add: isCont_difg n) ``` hoelzl@56181 ` 128` ``` show "\x. 0 < x \ x < h \ difg (0\nat) differentiable (at x)" ``` huffman@29187 ` 129` ``` by (simp add: differentiable_difg n) ``` huffman@29187 ` 130` ``` qed ``` huffman@29187 ` 131` ``` next ``` hoelzl@41166 ` 132` ``` case (Suc m') ``` huffman@29187 ` 133` ``` hence "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0" by simp ``` huffman@29187 ` 134` ``` then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast ``` huffman@29187 ` 135` ``` have "\t'. 0 < t' \ t' < t \ DERIV (difg (Suc m')) t' :> 0" ``` huffman@29187 ` 136` ``` proof (rule Rolle) ``` huffman@29187 ` 137` ``` show "0 < t" by fact ``` huffman@29187 ` 138` ``` show "difg (Suc m') 0 = difg (Suc m') t" ``` huffman@29187 ` 139` ``` using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0) ``` huffman@29187 ` 140` ``` show "\x. 0 \ x \ x \ t \ isCont (difg (Suc m')) x" ``` huffman@29187 ` 141` ``` using `t < h` `Suc m' < n` by (simp add: isCont_difg) ``` hoelzl@56181 ` 142` ``` show "\x. 0 < x \ x < t \ difg (Suc m') differentiable (at x)" ``` huffman@29187 ` 143` ``` using `t < h` `Suc m' < n` by (simp add: differentiable_difg) ``` huffman@29187 ` 144` ``` qed ``` huffman@29187 ` 145` ``` thus ?case ``` huffman@29187 ` 146` ``` using `t < h` by auto ``` huffman@29187 ` 147` ``` qed ``` huffman@29187 ` 148` huffman@29187 ` 149` ``` then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast ``` huffman@29187 ` 150` huffman@29187 ` 151` ``` hence "difg (Suc m) t = 0" ``` huffman@29187 ` 152` ``` using `m < n` by (simp add: difg_Suc_eq_0) ``` huffman@29187 ` 153` huffman@29187 ` 154` ``` show ?thesis ``` huffman@29187 ` 155` ``` proof (intro exI conjI) ``` huffman@29187 ` 156` ``` show "0 < t" by fact ``` huffman@29187 ` 157` ``` show "t < h" by fact ``` huffman@29187 ` 158` ``` show "f h = ``` hoelzl@56193 ` 159` ``` (\m0 & diff 0 = f & ``` nipkow@25134 ` 168` ``` (\m t. m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` nipkow@25134 ` 169` ``` --> (\t. 0 < t & t < h & ``` hoelzl@56193 ` 170` ``` f h = (\mm t. ``` bulwahn@41120 ` 178` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 179` ``` shows "\t. 0 < t \ t \ h \ f h = ``` hoelzl@56193 ` 180` ``` (\m 0" by simp ``` bulwahn@41120 ` 187` ``` from INIT1 this INIT2 DERIV have "\t>0. t < h \ ``` bulwahn@41120 ` 188` ``` f h = ``` hoelzl@56193 ` 189` ``` (\mm t. ``` paulson@15079 ` 197` ``` m < n & 0 \ t & t \ h --> DERIV (diff m) t :> diff (Suc m) t) ``` paulson@15079 ` 198` ``` --> (\t. 0 < t & ``` paulson@15079 ` 199` ``` t \ h & ``` paulson@15079 ` 200` ``` f h = ``` hoelzl@56193 ` 201` ``` (\mm t. m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 208` ``` shows "\t. h < t & t < 0 & ``` hoelzl@56193 ` 209` ``` f h = (\mt>0. t < - h \ ``` bulwahn@41120 ` 216` ``` f (- (- h)) = ``` hoelzl@56193 ` 217` ``` (\m ``` bulwahn@41120 ` 229` ``` - t < 0 \ ``` bulwahn@41120 ` 230` ``` f h = ``` hoelzl@56193 ` 231` ``` (\m 0 & diff 0 = f & ``` paulson@15079 ` 238` ``` (\m t. ``` paulson@15079 ` 239` ``` m < n & h \ t & t \ 0 --> DERIV (diff m) t :> diff (Suc m) t)) ``` paulson@15079 ` 240` ``` --> (\t. h < t & ``` paulson@15079 ` 241` ``` t < 0 & ``` paulson@15079 ` 242` ``` f h = ``` hoelzl@56193 ` 243` ``` (\m0 \ ``` nipkow@25134 ` 254` ``` diff 0 0 = ``` hoelzl@56193 ` 255` ``` (\mm t. m < n & abs t \ abs x --> DERIV (diff m) t :> diff (Suc m) t" ``` bulwahn@41120 ` 262` ``` shows "\t. abs t \ abs x & ``` paulson@15079 ` 263` ``` f x = ``` hoelzl@56193 ` 264` ``` (\mt. _ \ f x = ?f x t") ``` hoelzl@41166 ` 266` ```proof cases ``` hoelzl@41166 ` 267` ``` assume "n = 0" with `diff 0 = f` show ?thesis by force ``` bulwahn@41120 ` 268` ```next ``` hoelzl@41166 ` 269` ``` assume "n \ 0" ``` hoelzl@41166 ` 270` ``` show ?thesis ``` hoelzl@41166 ` 271` ``` proof (cases rule: linorder_cases) ``` hoelzl@41166 ` 272` ``` assume "x = 0" with `n \ 0` `diff 0 = f` DERIV ``` hoelzl@41166 ` 273` ``` have "\0\ \ \x\ \ f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma) ``` hoelzl@41166 ` 274` ``` thus ?thesis .. ``` bulwahn@41120 ` 275` ``` next ``` hoelzl@41166 ` 276` ``` assume "x < 0" ``` hoelzl@41166 ` 277` ``` with `n \ 0` DERIV ``` hoelzl@41166 ` 278` ``` have "\t>x. t < 0 \ diff 0 x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 279` ``` then guess t .. ``` hoelzl@41166 ` 280` ``` with `x < 0` `diff 0 = f` have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 281` ``` thus ?thesis .. ``` hoelzl@41166 ` 282` ``` next ``` hoelzl@41166 ` 283` ``` assume "x > 0" ``` hoelzl@41166 ` 284` ``` with `n \ 0` `diff 0 = f` DERIV ``` hoelzl@41166 ` 285` ``` have "\t>0. t < x \ diff 0 x = ?f x t" by (intro Maclaurin) auto ``` hoelzl@41166 ` 286` ``` then guess t .. ``` hoelzl@41166 ` 287` ``` with `x > 0` `diff 0 = f` have "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 288` ``` thus ?thesis .. ``` bulwahn@41120 ` 289` ``` qed ``` bulwahn@41120 ` 290` ```qed ``` bulwahn@41120 ` 291` paulson@15079 ` 292` ```lemma Maclaurin_all_lt: ``` bulwahn@41120 ` 293` ``` assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \ 0" ``` bulwahn@41120 ` 294` ``` and DERIV: "\m x. DERIV (diff m) x :> diff(Suc m) x" ``` hoelzl@41166 ` 295` ``` shows "\t. 0 < abs t & abs t < abs x & f x = ``` hoelzl@56193 ` 296` ``` (\mt. _ \ _ \ f x = ?f x t") ``` hoelzl@41166 ` 298` ```proof (cases rule: linorder_cases) ``` hoelzl@41166 ` 299` ``` assume "x = 0" with INIT3 show "?thesis".. ``` hoelzl@41166 ` 300` ```next ``` hoelzl@41166 ` 301` ``` assume "x < 0" ``` hoelzl@41166 ` 302` ``` with assms have "\t>x. t < 0 \ f x = ?f x t" by (intro Maclaurin_minus) auto ``` hoelzl@41166 ` 303` ``` then guess t .. ``` hoelzl@41166 ` 304` ``` with `x < 0` have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 305` ``` thus ?thesis .. ``` hoelzl@41166 ` 306` ```next ``` hoelzl@41166 ` 307` ``` assume "x > 0" ``` hoelzl@41166 ` 308` ``` with assms have "\t>0. t < x \ f x = ?f x t " by (intro Maclaurin) auto ``` hoelzl@41166 ` 309` ``` then guess t .. ``` hoelzl@41166 ` 310` ``` with `x > 0` have "0 < \t\ \ \t\ < \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 311` ``` thus ?thesis .. ``` bulwahn@41120 ` 312` ```qed ``` bulwahn@41120 ` 313` paulson@15079 ` 314` paulson@15079 ` 315` ```lemma Maclaurin_all_lt_objl: ``` paulson@15079 ` 316` ``` "diff 0 = f & ``` paulson@15079 ` 317` ``` (\m x. DERIV (diff m) x :> diff(Suc m) x) & ``` nipkow@25162 ` 318` ``` x ~= 0 & n > 0 ``` paulson@15079 ` 319` ``` --> (\t. 0 < abs t & abs t < abs x & ``` hoelzl@56193 ` 320` ``` f x = (\m n \ 0 --> ``` hoelzl@56193 ` 327` ``` (\mm x. DERIV (diff m) x :> diff (Suc m) x" ``` hoelzl@41166 ` 335` ``` shows "\t. abs t \ abs x & f x = ``` hoelzl@56193 ` 336` ``` (\mt. _ \ f x = ?f x t") ``` hoelzl@41166 ` 338` ```proof cases ``` hoelzl@41166 ` 339` ``` assume "n = 0" with INIT show ?thesis by force ``` bulwahn@41120 ` 340` ``` next ``` hoelzl@41166 ` 341` ``` assume "n \ 0" ``` hoelzl@41166 ` 342` ``` show ?thesis ``` hoelzl@41166 ` 343` ``` proof cases ``` hoelzl@41166 ` 344` ``` assume "x = 0" ``` hoelzl@56193 ` 345` ``` with `n \ 0` have "(\m 0` have " \0\ \ \x\ \ f x = ?f x 0" by force ``` hoelzl@41166 ` 348` ``` thus ?thesis .. ``` hoelzl@41166 ` 349` ``` next ``` hoelzl@41166 ` 350` ``` assume "x \ 0" ``` hoelzl@41166 ` 351` ``` with INIT `n \ 0` DERIV have "\t. 0 < \t\ \ \t\ < \x\ \ f x = ?f x t" ``` hoelzl@41166 ` 352` ``` by (intro Maclaurin_all_lt) auto ``` hoelzl@41166 ` 353` ``` then guess t .. ``` hoelzl@41166 ` 354` ``` hence "\t\ \ \x\ \ f x = ?f x t" by simp ``` hoelzl@41166 ` 355` ``` thus ?thesis .. ``` bulwahn@41120 ` 356` ``` qed ``` bulwahn@41120 ` 357` ```qed ``` bulwahn@41120 ` 358` paulson@15079 ` 359` ```lemma Maclaurin_all_le_objl: "diff 0 = f & ``` paulson@15079 ` 360` ``` (\m x. DERIV (diff m) x :> diff (Suc m) x) ``` paulson@15079 ` 361` ``` --> (\t. abs t \ abs x & ``` hoelzl@56193 ` 362` ``` f x = (\m 0 |] ``` paulson@15079 ` 370` ``` ==> (\t. 0 < abs t & ``` paulson@15079 ` 371` ``` abs t < abs x & ``` hoelzl@56193 ` 372` ``` exp x = (\mt. abs t \ abs x & ``` hoelzl@56193 ` 379` ``` exp x = (\m0 --> Suc (Suc (2 * n - 2)) = 2*n" ``` paulson@15251 ` 392` ```by (induct "n", auto) ``` paulson@15079 ` 393` paulson@15079 ` 394` ```lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: ``` nipkow@25134 ` 395` ``` "n\0 --> Suc (Suc (4*n - 2)) = 4*n" ``` paulson@15251 ` 396` ```by (induct "n", auto) ``` paulson@15079 ` 397` paulson@15079 ` 398` ```lemma Suc_mult_two_diff_one [rule_format, simp]: ``` nipkow@25134 ` 399` ``` "n\0 --> Suc (2 * n - 1) = 2*n" ``` paulson@15251 ` 400` ```by (induct "n", auto) ``` paulson@15079 ` 401` paulson@15234 ` 402` paulson@15234 ` 403` ```text{*It is unclear why so many variant results are needed.*} ``` paulson@15079 ` 404` huffman@36974 ` 405` ```lemma sin_expansion_lemma: ``` hoelzl@41166 ` 406` ``` "sin (x + real (Suc m) * pi / 2) = ``` huffman@36974 ` 407` ``` cos (x + real (m) * pi / 2)" ``` webertj@49962 ` 408` ```by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto) ``` huffman@36974 ` 409` paulson@15079 ` 410` ```lemma Maclaurin_sin_expansion2: ``` paulson@15079 ` 411` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 412` ``` sin x = ``` hoelzl@56193 ` 413` ``` (\mt. sin x = ``` hoelzl@56193 ` 433` ``` (\m 0; 0 < x |] ==> ``` paulson@15079 ` 441` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 442` ``` sin x = ``` hoelzl@56193 ` 443` ``` (\m ``` paulson@15079 ` 458` ``` \t. 0 < t & t \ x & ``` paulson@15079 ` 459` ``` sin x = ``` hoelzl@56193 ` 460` ``` (\mm<(Suc n). cos_coeff m * 0 ^ m) = 1" ``` paulson@15251 ` 478` ```by (induct "n", auto) ``` paulson@15079 ` 479` huffman@36974 ` 480` ```lemma cos_expansion_lemma: ``` huffman@36974 ` 481` ``` "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)" ``` webertj@49962 ` 482` ```by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto) ``` huffman@36974 ` 483` paulson@15079 ` 484` ```lemma Maclaurin_cos_expansion: ``` paulson@15079 ` 485` ``` "\t. abs t \ abs x & ``` paulson@15079 ` 486` ``` cos x = ``` hoelzl@56193 ` 487` ``` (\m 0 |] ==> ``` paulson@15079 ` 505` ``` \t. 0 < t & t < x & ``` paulson@15079 ` 506` ``` cos x = ``` hoelzl@56193 ` 507` ``` (\m 0 |] ==> ``` paulson@15079 ` 521` ``` \t. x < t & t < 0 & ``` paulson@15079 ` 522` ``` cos x = ``` hoelzl@56193 ` 523` ``` (\m (v::real) |] ==> \(x + u) - y\ \ v" ``` paulson@15079 ` 541` ```by auto ``` paulson@15079 ` 542` paulson@15079 ` 543` ```lemma Maclaurin_sin_bound: ``` hoelzl@56193 ` 544` ``` "abs(sin x - (\m inverse(real (fact n)) * \x\ ^ n" ``` obua@14738 ` 546` ```proof - ``` paulson@15079 ` 547` ``` have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 1 * y" ``` obua@14738 ` 548` ``` by (rule_tac mult_right_mono,simp_all) ``` obua@14738 ` 549` ``` note est = this[simplified] ``` huffman@22985 ` 550` ``` 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 ` 551` ``` have diff_0: "?diff 0 = sin" by simp ``` huffman@22985 ` 552` ``` have DERIV_diff: "\m x. DERIV (?diff m) x :> ?diff (Suc m) x" ``` huffman@22985 ` 553` ``` apply (clarify) ``` huffman@22985 ` 554` ``` apply (subst (1 2 3) mod_Suc_eq_Suc_mod) ``` huffman@22985 ` 555` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` hoelzl@31881 ` 556` ``` apply (safe, auto intro!: DERIV_intros) ``` huffman@22985 ` 557` ``` done ``` huffman@22985 ` 558` ``` from Maclaurin_all_le [OF diff_0 DERIV_diff] ``` huffman@22985 ` 559` ``` obtain t where t1: "\t\ \ \x\" and ``` hoelzl@56193 ` 560` ``` t2: "sin x = (\mm. ?diff m 0 = (if even m then 0 ``` huffman@23177 ` 564` ``` else -1 ^ ((m - Suc 0) div 2))" ``` huffman@22985 ` 565` ``` apply (subst even_even_mod_4_iff) ``` huffman@22985 ` 566` ``` apply (cut_tac m=m in mod_exhaust_less_4) ``` huffman@22985 ` 567` ``` apply (elim disjE, simp_all) ``` huffman@22985 ` 568` ``` apply (safe dest!: mod_eqD, simp_all) ``` huffman@22985 ` 569` ``` done ``` obua@14738 ` 570` ``` show ?thesis ``` huffman@44306 ` 571` ``` unfolding sin_coeff_def ``` huffman@22985 ` 572` ``` apply (subst t2) ``` paulson@15079 ` 573` ``` apply (rule sin_bound_lemma) ``` nipkow@15536 ` 574` ``` apply (rule setsum_cong[OF refl]) ``` huffman@22985 ` 575` ``` apply (subst diff_m_0, simp) ``` paulson@15079 ` 576` ``` apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono ``` hoelzl@41166 ` 577` ``` simp add: est mult_nonneg_nonneg mult_ac divide_inverse ``` paulson@16924 ` 578` ``` power_abs [symmetric] abs_mult) ``` obua@14738 ` 579` ``` done ``` obua@14738 ` 580` ```qed ``` obua@14738 ` 581` paulson@15079 ` 582` ```end ```