src/HOL/MacLaurin.thy
author huffman
Tue Feb 24 11:12:58 2009 -0800 (2009-02-24)
changeset 30082 43c5b7bfc791
parent 29811 026b0f9f579f
child 30273 ecd6f0ca62ea
permissions -rw-r--r--
make more proofs work whether or not One_nat_def is a simp rule
     1 (*  Author      : Jacques D. Fleuriot
     2     Copyright   : 2001 University of Edinburgh
     3     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     4 *)
     5 
     6 header{*MacLaurin Series*}
     7 
     8 theory MacLaurin
     9 imports Transcendental
    10 begin
    11 
    12 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
    13 
    14 text{*This is a very long, messy proof even now that it's been broken down
    15 into lemmas.*}
    16 
    17 lemma Maclaurin_lemma:
    18     "0 < h ==>
    19      \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
    20                (B * ((h^n) / real(fact n)))"
    21 apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
    22                  real(fact n) / (h^n)"
    23        in exI)
    24 apply (simp) 
    25 done
    26 
    27 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
    28 by arith
    29 
    30 text{*A crude tactic to differentiate by proof.*}
    31 
    32 lemmas deriv_rulesI =
    33   DERIV_ident DERIV_const DERIV_cos DERIV_cmult
    34   DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
    35   DERIV_add DERIV_diff DERIV_mult DERIV_minus
    36   DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
    37   DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
    38   DERIV_ident DERIV_const DERIV_cos
    39 
    40 ML
    41 {*
    42 local
    43 exception DERIV_name;
    44 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
    45 |   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
    46 |   get_fun_name _ = raise DERIV_name;
    47 
    48 in
    49 
    50 fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
    51   resolve_tac @{thms deriv_rulesI} i ORELSE
    52     ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
    53                      @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
    54 
    55 fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
    56 
    57 end
    58 *}
    59 
    60 lemma Maclaurin_lemma2:
    61   assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    62   assumes n: "n = Suc k"
    63   assumes difg: "difg =
    64         (\<lambda>m t. diff m t -
    65                ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    66                 B * (t ^ (n - m) / real (fact (n - m)))))"
    67   shows
    68       "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
    69 unfolding difg
    70  apply clarify
    71  apply (rule DERIV_diff)
    72   apply (simp add: diff)
    73  apply (simp only: n)
    74  apply (rule DERIV_add)
    75   apply (rule_tac [2] DERIV_cmult)
    76   apply (rule_tac [2] lemma_DERIV_subst)
    77    apply (rule_tac [2] DERIV_quotient)
    78      apply (rule_tac [3] DERIV_const)
    79     apply (rule_tac [2] DERIV_pow)
    80    prefer 3 apply (simp add: fact_diff_Suc)
    81   prefer 2 apply simp
    82  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    83  apply (simp del: setsum_op_ivl_Suc)
    84  apply (insert sumr_offset4 [of "Suc 0"])
    85  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    86  apply (rule lemma_DERIV_subst)
    87   apply (rule DERIV_add)
    88    apply (rule_tac [2] DERIV_const)
    89   apply (rule DERIV_sumr, clarify)
    90   prefer 2 apply simp
    91  apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
    92  apply (rule DERIV_cmult)
    93  apply (rule lemma_DERIV_subst)
    94   apply (best intro: DERIV_chain2 intro!: DERIV_intros)
    95  apply (subst fact_Suc)
    96  apply (subst real_of_nat_mult)
    97  apply (simp add: mult_ac)
    98 done
    99 
   100 
   101 lemma Maclaurin:
   102   assumes h: "0 < h"
   103   assumes n: "0 < n"
   104   assumes diff_0: "diff 0 = f"
   105   assumes diff_Suc:
   106     "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
   107   shows
   108     "\<exists>t. 0 < t & t < h &
   109               f h =
   110               setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
   111               (diff n t / real (fact n)) * h ^ n"
   112 proof -
   113   from n obtain m where m: "n = Suc m"
   114     by (cases n, simp add: n)
   115 
   116   obtain B where f_h: "f h =
   117         (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
   118         B * (h ^ n / real (fact n))"
   119     using Maclaurin_lemma [OF h] ..
   120 
   121   obtain g where g_def: "g = (%t. f t -
   122     (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}
   123       + (B * (t^n / real(fact n)))))" by blast
   124 
   125   have g2: "g 0 = 0 & g h = 0"
   126     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
   127     apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
   128     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
   129     done
   130 
   131   obtain difg where difg_def: "difg = (%m t. diff m t -
   132     (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
   133       + (B * ((t ^ (n - m)) / real (fact (n - m))))))" by blast
   134 
   135   have difg_0: "difg 0 = g"
   136     unfolding difg_def g_def by (simp add: diff_0)
   137 
   138   have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real.
   139         m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
   140     using diff_Suc m difg_def by (rule Maclaurin_lemma2)
   141 
   142   have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
   143     apply clarify
   144     apply (simp add: m difg_def)
   145     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
   146     apply (simp del: setsum_op_ivl_Suc)
   147     apply (insert sumr_offset4 [of "Suc 0"])
   148     apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
   149     done
   150 
   151   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
   152     by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
   153 
   154   have differentiable_difg:
   155     "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
   156     by (rule differentiableI [OF difg_Suc [rule_format]]) simp
   157 
   158   have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
   159         \<Longrightarrow> difg (Suc m) t = 0"
   160     by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
   161 
   162   have "m < n" using m by simp
   163 
   164   have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
   165   using `m < n`
   166   proof (induct m)
   167   case 0
   168     show ?case
   169     proof (rule Rolle)
   170       show "0 < h" by fact
   171       show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
   172       show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
   173         by (simp add: isCont_difg n)
   174       show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
   175         by (simp add: differentiable_difg n)
   176     qed
   177   next
   178   case (Suc m')
   179     hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
   180     then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
   181     have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
   182     proof (rule Rolle)
   183       show "0 < t" by fact
   184       show "difg (Suc m') 0 = difg (Suc m') t"
   185         using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
   186       show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
   187         using `t < h` `Suc m' < n` by (simp add: isCont_difg)
   188       show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
   189         using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
   190     qed
   191     thus ?case
   192       using `t < h` by auto
   193   qed
   194 
   195   then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
   196 
   197   hence "difg (Suc m) t = 0"
   198     using `m < n` by (simp add: difg_Suc_eq_0)
   199 
   200   show ?thesis
   201   proof (intro exI conjI)
   202     show "0 < t" by fact
   203     show "t < h" by fact
   204     show "f h =
   205       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
   206       diff n t / real (fact n) * h ^ n"
   207       using `difg (Suc m) t = 0`
   208       by (simp add: m f_h difg_def del: realpow_Suc fact_Suc)
   209   qed
   210 
   211 qed
   212 
   213 lemma Maclaurin_objl:
   214   "0 < h & n>0 & diff 0 = f &
   215   (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   216    --> (\<exists>t. 0 < t & t < h &
   217             f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   218                   diff n t / real (fact n) * h ^ n)"
   219 by (blast intro: Maclaurin)
   220 
   221 
   222 lemma Maclaurin2:
   223    "[| 0 < h; diff 0 = f;
   224        \<forall>m t.
   225           m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
   226     ==> \<exists>t. 0 < t &
   227               t \<le> h &
   228               f h =
   229               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   230               diff n t / real (fact n) * h ^ n"
   231 apply (case_tac "n", auto)
   232 apply (drule Maclaurin, auto)
   233 done
   234 
   235 lemma Maclaurin2_objl:
   236      "0 < h & diff 0 = f &
   237        (\<forall>m t.
   238           m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   239     --> (\<exists>t. 0 < t &
   240               t \<le> h &
   241               f h =
   242               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   243               diff n t / real (fact n) * h ^ n)"
   244 by (blast intro: Maclaurin2)
   245 
   246 lemma Maclaurin_minus:
   247    "[| h < 0; n > 0; diff 0 = f;
   248        \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
   249     ==> \<exists>t. h < t &
   250               t < 0 &
   251               f h =
   252               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   253               diff n t / real (fact n) * h ^ n"
   254 apply (cut_tac f = "%x. f (-x)"
   255         and diff = "%n x. (-1 ^ n) * diff n (-x)"
   256         and h = "-h" and n = n in Maclaurin_objl)
   257 apply (simp)
   258 apply safe
   259 apply (subst minus_mult_right)
   260 apply (rule DERIV_cmult)
   261 apply (rule lemma_DERIV_subst)
   262 apply (rule DERIV_chain2 [where g=uminus])
   263 apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
   264 prefer 2 apply force
   265 apply force
   266 apply (rule_tac x = "-t" in exI, auto)
   267 apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
   268                     (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
   269 apply (rule_tac [2] setsum_cong[OF refl])
   270 apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
   271 done
   272 
   273 lemma Maclaurin_minus_objl:
   274      "(h < 0 & n > 0 & diff 0 = f &
   275        (\<forall>m t.
   276           m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
   277     --> (\<exists>t. h < t &
   278               t < 0 &
   279               f h =
   280               (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   281               diff n t / real (fact n) * h ^ n)"
   282 by (blast intro: Maclaurin_minus)
   283 
   284 
   285 subsection{*More Convenient "Bidirectional" Version.*}
   286 
   287 (* not good for PVS sin_approx, cos_approx *)
   288 
   289 lemma Maclaurin_bi_le_lemma [rule_format]:
   290   "n>0 \<longrightarrow>
   291    diff 0 0 =
   292    (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   293    diff n 0 * 0 ^ n / real (fact n)"
   294 by (induct "n", auto)
   295 
   296 lemma Maclaurin_bi_le:
   297    "[| diff 0 = f;
   298        \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
   299     ==> \<exists>t. abs t \<le> abs x &
   300               f x =
   301               (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
   302               diff n t / real (fact n) * x ^ n"
   303 apply (case_tac "n = 0", force)
   304 apply (case_tac "x = 0")
   305  apply (rule_tac x = 0 in exI)
   306  apply (force simp add: Maclaurin_bi_le_lemma)
   307 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
   308  txt{*Case 1, where @{term "x < 0"}*}
   309  apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
   310   apply (simp add: abs_if)
   311  apply (rule_tac x = t in exI)
   312  apply (simp add: abs_if)
   313 txt{*Case 2, where @{term "0 < x"}*}
   314 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
   315  apply (simp add: abs_if)
   316 apply (rule_tac x = t in exI)
   317 apply (simp add: abs_if)
   318 done
   319 
   320 lemma Maclaurin_all_lt:
   321      "[| diff 0 = f;
   322          \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
   323         x ~= 0; n > 0
   324       |] ==> \<exists>t. 0 < abs t & abs t < abs x &
   325                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   326                      (diff n t / real (fact n)) * x ^ n"
   327 apply (rule_tac x = x and y = 0 in linorder_cases)
   328 prefer 2 apply blast
   329 apply (drule_tac [2] diff=diff in Maclaurin)
   330 apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
   331 apply (rule_tac [!] x = t in exI, auto)
   332 done
   333 
   334 lemma Maclaurin_all_lt_objl:
   335      "diff 0 = f &
   336       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
   337       x ~= 0 & n > 0
   338       --> (\<exists>t. 0 < abs t & abs t < abs x &
   339                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   340                      (diff n t / real (fact n)) * x ^ n)"
   341 by (blast intro: Maclaurin_all_lt)
   342 
   343 lemma Maclaurin_zero [rule_format]:
   344      "x = (0::real)
   345       ==> n \<noteq> 0 -->
   346           (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
   347           diff 0 0"
   348 by (induct n, auto)
   349 
   350 lemma Maclaurin_all_le: "[| diff 0 = f;
   351         \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
   352       |] ==> \<exists>t. abs t \<le> abs x &
   353               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   354                     (diff n t / real (fact n)) * x ^ n"
   355 apply(cases "n=0")
   356 apply (force)
   357 apply (case_tac "x = 0")
   358 apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
   359 apply (drule not0_implies_Suc)
   360 apply (rule_tac x = 0 in exI, force)
   361 apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
   362 apply (rule_tac x = t in exI, auto)
   363 done
   364 
   365 lemma Maclaurin_all_le_objl: "diff 0 = f &
   366       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
   367       --> (\<exists>t. abs t \<le> abs x &
   368               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   369                     (diff n t / real (fact n)) * x ^ n)"
   370 by (blast intro: Maclaurin_all_le)
   371 
   372 
   373 subsection{*Version for Exponential Function*}
   374 
   375 lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
   376       ==> (\<exists>t. 0 < abs t &
   377                 abs t < abs x &
   378                 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   379                         (exp t / real (fact n)) * x ^ n)"
   380 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
   381 
   382 
   383 lemma Maclaurin_exp_le:
   384      "\<exists>t. abs t \<le> abs x &
   385             exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   386                        (exp t / real (fact n)) * x ^ n"
   387 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
   388 
   389 
   390 subsection{*Version for Sine Function*}
   391 
   392 lemma mod_exhaust_less_4:
   393   "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
   394 by auto
   395 
   396 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
   397   "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
   398 by (induct "n", auto)
   399 
   400 lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
   401   "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
   402 by (induct "n", auto)
   403 
   404 lemma Suc_mult_two_diff_one [rule_format, simp]:
   405   "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
   406 by (induct "n", auto)
   407 
   408 
   409 text{*It is unclear why so many variant results are needed.*}
   410 
   411 lemma Maclaurin_sin_expansion2:
   412      "\<exists>t. abs t \<le> abs x &
   413        sin x =
   414        (\<Sum>m=0..<n. (if even m then 0
   415                        else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   416                        x ^ m)
   417       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   418 apply (cut_tac f = sin and n = n and x = x
   419         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
   420 apply safe
   421 apply (simp (no_asm))
   422 apply (simp (no_asm))
   423 apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
   424 apply (rule ccontr, simp)
   425 apply (drule_tac x = x in spec, simp)
   426 apply (erule ssubst)
   427 apply (rule_tac x = t in exI, simp)
   428 apply (rule setsum_cong[OF refl])
   429 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   430 done
   431 
   432 lemma Maclaurin_sin_expansion:
   433      "\<exists>t. sin x =
   434        (\<Sum>m=0..<n. (if even m then 0
   435                        else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   436                        x ^ m)
   437       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   438 apply (insert Maclaurin_sin_expansion2 [of x n]) 
   439 apply (blast intro: elim:); 
   440 done
   441 
   442 
   443 lemma Maclaurin_sin_expansion3:
   444      "[| n > 0; 0 < x |] ==>
   445        \<exists>t. 0 < t & t < x &
   446        sin x =
   447        (\<Sum>m=0..<n. (if even m then 0
   448                        else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   449                        x ^ m)
   450       + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
   451 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
   452 apply safe
   453 apply simp
   454 apply (simp (no_asm))
   455 apply (erule ssubst)
   456 apply (rule_tac x = t in exI, simp)
   457 apply (rule setsum_cong[OF refl])
   458 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   459 done
   460 
   461 lemma Maclaurin_sin_expansion4:
   462      "0 < x ==>
   463        \<exists>t. 0 < t & t \<le> x &
   464        sin x =
   465        (\<Sum>m=0..<n. (if even m then 0
   466                        else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   467                        x ^ m)
   468       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   469 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
   470 apply safe
   471 apply simp
   472 apply (simp (no_asm))
   473 apply (erule ssubst)
   474 apply (rule_tac x = t in exI, simp)
   475 apply (rule setsum_cong[OF refl])
   476 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   477 done
   478 
   479 
   480 subsection{*Maclaurin Expansion for Cosine Function*}
   481 
   482 lemma sumr_cos_zero_one [simp]:
   483  "(\<Sum>m=0..<(Suc n).
   484      (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
   485 by (induct "n", auto)
   486 
   487 lemma Maclaurin_cos_expansion:
   488      "\<exists>t. abs t \<le> abs x &
   489        cos x =
   490        (\<Sum>m=0..<n. (if even m
   491                        then -1 ^ (m div 2)/(real (fact m))
   492                        else 0) *
   493                        x ^ m)
   494       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   495 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
   496 apply safe
   497 apply (simp (no_asm))
   498 apply (simp (no_asm))
   499 apply (case_tac "n", simp)
   500 apply (simp del: setsum_op_ivl_Suc)
   501 apply (rule ccontr, simp)
   502 apply (drule_tac x = x in spec, simp)
   503 apply (erule ssubst)
   504 apply (rule_tac x = t in exI, simp)
   505 apply (rule setsum_cong[OF refl])
   506 apply (auto simp add: cos_zero_iff even_mult_two_ex)
   507 done
   508 
   509 lemma Maclaurin_cos_expansion2:
   510      "[| 0 < x; n > 0 |] ==>
   511        \<exists>t. 0 < t & t < x &
   512        cos x =
   513        (\<Sum>m=0..<n. (if even m
   514                        then -1 ^ (m div 2)/(real (fact m))
   515                        else 0) *
   516                        x ^ m)
   517       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   518 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
   519 apply safe
   520 apply simp
   521 apply (simp (no_asm))
   522 apply (erule ssubst)
   523 apply (rule_tac x = t in exI, simp)
   524 apply (rule setsum_cong[OF refl])
   525 apply (auto simp add: cos_zero_iff even_mult_two_ex)
   526 done
   527 
   528 lemma Maclaurin_minus_cos_expansion:
   529      "[| x < 0; n > 0 |] ==>
   530        \<exists>t. x < t & t < 0 &
   531        cos x =
   532        (\<Sum>m=0..<n. (if even m
   533                        then -1 ^ (m div 2)/(real (fact m))
   534                        else 0) *
   535                        x ^ m)
   536       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   537 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
   538 apply safe
   539 apply simp
   540 apply (simp (no_asm))
   541 apply (erule ssubst)
   542 apply (rule_tac x = t in exI, simp)
   543 apply (rule setsum_cong[OF refl])
   544 apply (auto simp add: cos_zero_iff even_mult_two_ex)
   545 done
   546 
   547 (* ------------------------------------------------------------------------- *)
   548 (* Version for ln(1 +/- x). Where is it??                                    *)
   549 (* ------------------------------------------------------------------------- *)
   550 
   551 lemma sin_bound_lemma:
   552     "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
   553 by auto
   554 
   555 text {* TODO: move to Parity.thy *}
   556 lemma nat_odd_1 [simp]: "odd (1::nat)"
   557   unfolding even_nat_def by simp
   558 
   559 lemma Maclaurin_sin_bound:
   560   "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   561   x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
   562 proof -
   563   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   564     by (rule_tac mult_right_mono,simp_all)
   565   note est = this[simplified]
   566   let ?diff = "\<lambda>(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)"
   567   have diff_0: "?diff 0 = sin" by simp
   568   have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
   569     apply (clarify)
   570     apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
   571     apply (cut_tac m=m in mod_exhaust_less_4)
   572     apply (safe, simp_all)
   573     apply (rule DERIV_minus, simp)
   574     apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
   575     done
   576   from Maclaurin_all_le [OF diff_0 DERIV_diff]
   577   obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
   578     t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
   579       ?diff n t / real (fact n) * x ^ n" by fast
   580   have diff_m_0:
   581     "\<And>m. ?diff m 0 = (if even m then 0
   582          else -1 ^ ((m - Suc 0) div 2))"
   583     apply (subst even_even_mod_4_iff)
   584     apply (cut_tac m=m in mod_exhaust_less_4)
   585     apply (elim disjE, simp_all)
   586     apply (safe dest!: mod_eqD, simp_all)
   587     done
   588   show ?thesis
   589     apply (subst t2)
   590     apply (rule sin_bound_lemma)
   591     apply (rule setsum_cong[OF refl])
   592     apply (subst diff_m_0, simp)
   593     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
   594                    simp add: est mult_nonneg_nonneg mult_ac divide_inverse
   595                           power_abs [symmetric] abs_mult)
   596     done
   597 qed
   598 
   599 end