src/HOL/MacLaurin.thy
changeset 28952 15a4b2cf8c34
parent 27239 f2f42f9fa09d
child 29168 ff13de554ed0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MacLaurin.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,576 @@
     1.4 +(*  Author      : Jacques D. Fleuriot
     1.5 +    Copyright   : 2001 University of Edinburgh
     1.6 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.7 +*)
     1.8 +
     1.9 +header{*MacLaurin Series*}
    1.10 +
    1.11 +theory MacLaurin
    1.12 +imports Dense_Linear_Order Transcendental
    1.13 +begin
    1.14 +
    1.15 +subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
    1.16 +
    1.17 +text{*This is a very long, messy proof even now that it's been broken down
    1.18 +into lemmas.*}
    1.19 +
    1.20 +lemma Maclaurin_lemma:
    1.21 +    "0 < h ==>
    1.22 +     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
    1.23 +               (B * ((h^n) / real(fact n)))"
    1.24 +apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
    1.25 +                 real(fact n) / (h^n)"
    1.26 +       in exI)
    1.27 +apply (simp) 
    1.28 +done
    1.29 +
    1.30 +lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
    1.31 +by arith
    1.32 +
    1.33 +text{*A crude tactic to differentiate by proof.*}
    1.34 +
    1.35 +lemmas deriv_rulesI =
    1.36 +  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
    1.37 +  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
    1.38 +  DERIV_add DERIV_diff DERIV_mult DERIV_minus
    1.39 +  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
    1.40 +  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
    1.41 +  DERIV_ident DERIV_const DERIV_cos
    1.42 +
    1.43 +ML
    1.44 +{*
    1.45 +local
    1.46 +exception DERIV_name;
    1.47 +fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
    1.48 +|   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
    1.49 +|   get_fun_name _ = raise DERIV_name;
    1.50 +
    1.51 +in
    1.52 +
    1.53 +fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
    1.54 +  resolve_tac @{thms deriv_rulesI} i ORELSE
    1.55 +    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
    1.56 +                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
    1.57 +
    1.58 +fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
    1.59 +
    1.60 +end
    1.61 +*}
    1.62 +
    1.63 +lemma Maclaurin_lemma2:
    1.64 +      "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t;
    1.65 +          n = Suc k;
    1.66 +        difg =
    1.67 +        (\<lambda>m t. diff m t -
    1.68 +               ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    1.69 +                B * (t ^ (n - m) / real (fact (n - m)))))|] ==>
    1.70 +        \<forall>m t. m < n & 0 \<le> t & t \<le> h -->
    1.71 +                    DERIV (difg m) t :> difg (Suc m) t"
    1.72 +apply clarify
    1.73 +apply (rule DERIV_diff)
    1.74 +apply (simp (no_asm_simp))
    1.75 +apply (tactic {* DERIV_tac @{context} *})
    1.76 +apply (tactic {* DERIV_tac @{context} *})
    1.77 +apply (rule_tac [2] lemma_DERIV_subst)
    1.78 +apply (rule_tac [2] DERIV_quotient)
    1.79 +apply (rule_tac [3] DERIV_const)
    1.80 +apply (rule_tac [2] DERIV_pow)
    1.81 +  prefer 3 apply (simp add: fact_diff_Suc)
    1.82 + prefer 2 apply simp
    1.83 +apply (frule_tac m = m in less_add_one, clarify)
    1.84 +apply (simp del: setsum_op_ivl_Suc)
    1.85 +apply (insert sumr_offset4 [of 1])
    1.86 +apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.87 +apply (rule lemma_DERIV_subst)
    1.88 +apply (rule DERIV_add)
    1.89 +apply (rule_tac [2] DERIV_const)
    1.90 +apply (rule DERIV_sumr, clarify)
    1.91 + prefer 2 apply simp
    1.92 +apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
    1.93 +apply (rule DERIV_cmult)
    1.94 +apply (rule lemma_DERIV_subst)
    1.95 +apply (best intro: DERIV_chain2 intro!: DERIV_intros)
    1.96 +apply (subst fact_Suc)
    1.97 +apply (subst real_of_nat_mult)
    1.98 +apply (simp add: mult_ac)
    1.99 +done
   1.100 +
   1.101 +
   1.102 +lemma Maclaurin_lemma3:
   1.103 +  fixes difg :: "nat => real => real" shows
   1.104 +     "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
   1.105 +        \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0;  n < m; 0 < t;
   1.106 +        t < h|]
   1.107 +     ==> \<exists>ta. 0 < ta & ta < t & DERIV (difg (Suc n)) ta :> 0"
   1.108 +apply (rule Rolle, assumption, simp)
   1.109 +apply (drule_tac x = n and P="%k. k<Suc m --> difg k 0 = 0" in spec)
   1.110 +apply (rule DERIV_unique)
   1.111 +prefer 2 apply assumption
   1.112 +apply force
   1.113 +apply (metis DERIV_isCont dlo_simps(4) dlo_simps(9) less_trans_Suc nat_less_le not_less_eq real_le_trans)
   1.114 +apply (metis Suc_less_eq differentiableI dlo_simps(7) dlo_simps(8) dlo_simps(9)   real_le_trans xt1(8))
   1.115 +done
   1.116 +
   1.117 +lemma Maclaurin:
   1.118 +   "[| 0 < h; n > 0; diff 0 = f;
   1.119 +       \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
   1.120 +    ==> \<exists>t. 0 < t &
   1.121 +              t < h &
   1.122 +              f h =
   1.123 +              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
   1.124 +              (diff n t / real (fact n)) * h ^ n"
   1.125 +apply (case_tac "n = 0", force)
   1.126 +apply (drule not0_implies_Suc)
   1.127 +apply (erule exE)
   1.128 +apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
   1.129 +apply (erule exE)
   1.130 +apply (subgoal_tac "\<exists>g.
   1.131 +     g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
   1.132 + prefer 2 apply blast
   1.133 +apply (erule exE)
   1.134 +apply (subgoal_tac "g 0 = 0 & g h =0")
   1.135 + prefer 2
   1.136 + apply (simp del: setsum_op_ivl_Suc)
   1.137 + apply (cut_tac n = m and k = 1 in sumr_offset2)
   1.138 + apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
   1.139 +apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
   1.140 + prefer 2 apply blast
   1.141 +apply (erule exE)
   1.142 +apply (subgoal_tac "difg 0 = g")
   1.143 + prefer 2 apply simp
   1.144 +apply (frule Maclaurin_lemma2, assumption+)
   1.145 +apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
   1.146 + apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
   1.147 + apply (erule impE)
   1.148 +  apply (simp (no_asm_simp))
   1.149 + apply (erule exE)
   1.150 + apply (rule_tac x = t in exI)
   1.151 + apply (simp del: realpow_Suc fact_Suc)
   1.152 +apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
   1.153 + prefer 2
   1.154 + apply clarify
   1.155 + apply simp
   1.156 + apply (frule_tac m = ma in less_add_one, clarify)
   1.157 + apply (simp del: setsum_op_ivl_Suc)
   1.158 +apply (insert sumr_offset4 [of 1])
   1.159 +apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
   1.160 +apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
   1.161 +apply (rule allI, rule impI)
   1.162 +apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
   1.163 +apply (erule impE, assumption)
   1.164 +apply (erule exE)
   1.165 +apply (rule_tac x = t in exI)
   1.166 +(* do some tidying up *)
   1.167 +apply (erule_tac [!] V= "difg = (%m t. diff m t - (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0..<n-m} + B * (t ^ (n - m) / real (fact (n - m)))))"
   1.168 +       in thin_rl)
   1.169 +apply (erule_tac [!] V="g = (%t. f t - (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))"
   1.170 +       in thin_rl)
   1.171 +apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
   1.172 +       in thin_rl)
   1.173 +(* back to business *)
   1.174 +apply (simp (no_asm_simp))
   1.175 +apply (rule DERIV_unique)
   1.176 +prefer 2 apply blast
   1.177 +apply force
   1.178 +apply (rule allI, induct_tac "ma")
   1.179 +apply (rule impI, rule Rolle, assumption, simp, simp)
   1.180 +apply (metis DERIV_isCont zero_less_Suc)
   1.181 +apply (metis One_nat_def differentiableI dlo_simps(7))
   1.182 +apply safe
   1.183 +apply force
   1.184 +apply (frule Maclaurin_lemma3, assumption+, safe)
   1.185 +apply (rule_tac x = ta in exI, force)
   1.186 +done
   1.187 +
   1.188 +lemma Maclaurin_objl:
   1.189 +  "0 < h & n>0 & diff 0 = f &
   1.190 +  (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   1.191 +   --> (\<exists>t. 0 < t & t < h &
   1.192 +            f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.193 +                  diff n t / real (fact n) * h ^ n)"
   1.194 +by (blast intro: Maclaurin)
   1.195 +
   1.196 +
   1.197 +lemma Maclaurin2:
   1.198 +   "[| 0 < h; diff 0 = f;
   1.199 +       \<forall>m t.
   1.200 +          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
   1.201 +    ==> \<exists>t. 0 < t &
   1.202 +              t \<le> h &
   1.203 +              f h =
   1.204 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.205 +              diff n t / real (fact n) * h ^ n"
   1.206 +apply (case_tac "n", auto)
   1.207 +apply (drule Maclaurin, auto)
   1.208 +done
   1.209 +
   1.210 +lemma Maclaurin2_objl:
   1.211 +     "0 < h & diff 0 = f &
   1.212 +       (\<forall>m t.
   1.213 +          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   1.214 +    --> (\<exists>t. 0 < t &
   1.215 +              t \<le> h &
   1.216 +              f h =
   1.217 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.218 +              diff n t / real (fact n) * h ^ n)"
   1.219 +by (blast intro: Maclaurin2)
   1.220 +
   1.221 +lemma Maclaurin_minus:
   1.222 +   "[| h < 0; n > 0; diff 0 = f;
   1.223 +       \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
   1.224 +    ==> \<exists>t. h < t &
   1.225 +              t < 0 &
   1.226 +              f h =
   1.227 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.228 +              diff n t / real (fact n) * h ^ n"
   1.229 +apply (cut_tac f = "%x. f (-x)"
   1.230 +        and diff = "%n x. (-1 ^ n) * diff n (-x)"
   1.231 +        and h = "-h" and n = n in Maclaurin_objl)
   1.232 +apply (simp)
   1.233 +apply safe
   1.234 +apply (subst minus_mult_right)
   1.235 +apply (rule DERIV_cmult)
   1.236 +apply (rule lemma_DERIV_subst)
   1.237 +apply (rule DERIV_chain2 [where g=uminus])
   1.238 +apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
   1.239 +prefer 2 apply force
   1.240 +apply force
   1.241 +apply (rule_tac x = "-t" in exI, auto)
   1.242 +apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
   1.243 +                    (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
   1.244 +apply (rule_tac [2] setsum_cong[OF refl])
   1.245 +apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
   1.246 +done
   1.247 +
   1.248 +lemma Maclaurin_minus_objl:
   1.249 +     "(h < 0 & n > 0 & diff 0 = f &
   1.250 +       (\<forall>m t.
   1.251 +          m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
   1.252 +    --> (\<exists>t. h < t &
   1.253 +              t < 0 &
   1.254 +              f h =
   1.255 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.256 +              diff n t / real (fact n) * h ^ n)"
   1.257 +by (blast intro: Maclaurin_minus)
   1.258 +
   1.259 +
   1.260 +subsection{*More Convenient "Bidirectional" Version.*}
   1.261 +
   1.262 +(* not good for PVS sin_approx, cos_approx *)
   1.263 +
   1.264 +lemma Maclaurin_bi_le_lemma [rule_format]:
   1.265 +  "n>0 \<longrightarrow>
   1.266 +   diff 0 0 =
   1.267 +   (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   1.268 +   diff n 0 * 0 ^ n / real (fact n)"
   1.269 +by (induct "n", auto)
   1.270 +
   1.271 +lemma Maclaurin_bi_le:
   1.272 +   "[| diff 0 = f;
   1.273 +       \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
   1.274 +    ==> \<exists>t. abs t \<le> abs x &
   1.275 +              f x =
   1.276 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
   1.277 +              diff n t / real (fact n) * x ^ n"
   1.278 +apply (case_tac "n = 0", force)
   1.279 +apply (case_tac "x = 0")
   1.280 + apply (rule_tac x = 0 in exI)
   1.281 + apply (force simp add: Maclaurin_bi_le_lemma)
   1.282 +apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
   1.283 + txt{*Case 1, where @{term "x < 0"}*}
   1.284 + apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
   1.285 +  apply (simp add: abs_if)
   1.286 + apply (rule_tac x = t in exI)
   1.287 + apply (simp add: abs_if)
   1.288 +txt{*Case 2, where @{term "0 < x"}*}
   1.289 +apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
   1.290 + apply (simp add: abs_if)
   1.291 +apply (rule_tac x = t in exI)
   1.292 +apply (simp add: abs_if)
   1.293 +done
   1.294 +
   1.295 +lemma Maclaurin_all_lt:
   1.296 +     "[| diff 0 = f;
   1.297 +         \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
   1.298 +        x ~= 0; n > 0
   1.299 +      |] ==> \<exists>t. 0 < abs t & abs t < abs x &
   1.300 +               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.301 +                     (diff n t / real (fact n)) * x ^ n"
   1.302 +apply (rule_tac x = x and y = 0 in linorder_cases)
   1.303 +prefer 2 apply blast
   1.304 +apply (drule_tac [2] diff=diff in Maclaurin)
   1.305 +apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
   1.306 +apply (rule_tac [!] x = t in exI, auto)
   1.307 +done
   1.308 +
   1.309 +lemma Maclaurin_all_lt_objl:
   1.310 +     "diff 0 = f &
   1.311 +      (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
   1.312 +      x ~= 0 & n > 0
   1.313 +      --> (\<exists>t. 0 < abs t & abs t < abs x &
   1.314 +               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.315 +                     (diff n t / real (fact n)) * x ^ n)"
   1.316 +by (blast intro: Maclaurin_all_lt)
   1.317 +
   1.318 +lemma Maclaurin_zero [rule_format]:
   1.319 +     "x = (0::real)
   1.320 +      ==> n \<noteq> 0 -->
   1.321 +          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
   1.322 +          diff 0 0"
   1.323 +by (induct n, auto)
   1.324 +
   1.325 +lemma Maclaurin_all_le: "[| diff 0 = f;
   1.326 +        \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
   1.327 +      |] ==> \<exists>t. abs t \<le> abs x &
   1.328 +              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.329 +                    (diff n t / real (fact n)) * x ^ n"
   1.330 +apply(cases "n=0")
   1.331 +apply (force)
   1.332 +apply (case_tac "x = 0")
   1.333 +apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
   1.334 +apply (drule not0_implies_Suc)
   1.335 +apply (rule_tac x = 0 in exI, force)
   1.336 +apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
   1.337 +apply (rule_tac x = t in exI, auto)
   1.338 +done
   1.339 +
   1.340 +lemma Maclaurin_all_le_objl: "diff 0 = f &
   1.341 +      (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
   1.342 +      --> (\<exists>t. abs t \<le> abs x &
   1.343 +              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.344 +                    (diff n t / real (fact n)) * x ^ n)"
   1.345 +by (blast intro: Maclaurin_all_le)
   1.346 +
   1.347 +
   1.348 +subsection{*Version for Exponential Function*}
   1.349 +
   1.350 +lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
   1.351 +      ==> (\<exists>t. 0 < abs t &
   1.352 +                abs t < abs x &
   1.353 +                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   1.354 +                        (exp t / real (fact n)) * x ^ n)"
   1.355 +by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
   1.356 +
   1.357 +
   1.358 +lemma Maclaurin_exp_le:
   1.359 +     "\<exists>t. abs t \<le> abs x &
   1.360 +            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   1.361 +                       (exp t / real (fact n)) * x ^ n"
   1.362 +by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
   1.363 +
   1.364 +
   1.365 +subsection{*Version for Sine Function*}
   1.366 +
   1.367 +lemma MVT2:
   1.368 +     "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   1.369 +      ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
   1.370 +apply (drule MVT)
   1.371 +apply (blast intro: DERIV_isCont)
   1.372 +apply (force dest: order_less_imp_le simp add: differentiable_def)
   1.373 +apply (blast dest: DERIV_unique order_less_imp_le)
   1.374 +done
   1.375 +
   1.376 +lemma mod_exhaust_less_4:
   1.377 +  "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
   1.378 +by auto
   1.379 +
   1.380 +lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
   1.381 +  "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
   1.382 +by (induct "n", auto)
   1.383 +
   1.384 +lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
   1.385 +  "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
   1.386 +by (induct "n", auto)
   1.387 +
   1.388 +lemma Suc_mult_two_diff_one [rule_format, simp]:
   1.389 +  "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
   1.390 +by (induct "n", auto)
   1.391 +
   1.392 +
   1.393 +text{*It is unclear why so many variant results are needed.*}
   1.394 +
   1.395 +lemma Maclaurin_sin_expansion2:
   1.396 +     "\<exists>t. abs t \<le> abs x &
   1.397 +       sin x =
   1.398 +       (\<Sum>m=0..<n. (if even m then 0
   1.399 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   1.400 +                       x ^ m)
   1.401 +      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.402 +apply (cut_tac f = sin and n = n and x = x
   1.403 +        and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
   1.404 +apply safe
   1.405 +apply (simp (no_asm))
   1.406 +apply (simp (no_asm))
   1.407 +apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
   1.408 +apply (rule ccontr, simp)
   1.409 +apply (drule_tac x = x in spec, simp)
   1.410 +apply (erule ssubst)
   1.411 +apply (rule_tac x = t in exI, simp)
   1.412 +apply (rule setsum_cong[OF refl])
   1.413 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   1.414 +done
   1.415 +
   1.416 +lemma Maclaurin_sin_expansion:
   1.417 +     "\<exists>t. sin x =
   1.418 +       (\<Sum>m=0..<n. (if even m then 0
   1.419 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   1.420 +                       x ^ m)
   1.421 +      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.422 +apply (insert Maclaurin_sin_expansion2 [of x n]) 
   1.423 +apply (blast intro: elim:); 
   1.424 +done
   1.425 +
   1.426 +
   1.427 +lemma Maclaurin_sin_expansion3:
   1.428 +     "[| n > 0; 0 < x |] ==>
   1.429 +       \<exists>t. 0 < t & t < x &
   1.430 +       sin x =
   1.431 +       (\<Sum>m=0..<n. (if even m then 0
   1.432 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   1.433 +                       x ^ m)
   1.434 +      + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
   1.435 +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)
   1.436 +apply safe
   1.437 +apply simp
   1.438 +apply (simp (no_asm))
   1.439 +apply (erule ssubst)
   1.440 +apply (rule_tac x = t in exI, simp)
   1.441 +apply (rule setsum_cong[OF refl])
   1.442 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   1.443 +done
   1.444 +
   1.445 +lemma Maclaurin_sin_expansion4:
   1.446 +     "0 < x ==>
   1.447 +       \<exists>t. 0 < t & t \<le> x &
   1.448 +       sin x =
   1.449 +       (\<Sum>m=0..<n. (if even m then 0
   1.450 +                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   1.451 +                       x ^ m)
   1.452 +      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.453 +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)
   1.454 +apply safe
   1.455 +apply simp
   1.456 +apply (simp (no_asm))
   1.457 +apply (erule ssubst)
   1.458 +apply (rule_tac x = t in exI, simp)
   1.459 +apply (rule setsum_cong[OF refl])
   1.460 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
   1.461 +done
   1.462 +
   1.463 +
   1.464 +subsection{*Maclaurin Expansion for Cosine Function*}
   1.465 +
   1.466 +lemma sumr_cos_zero_one [simp]:
   1.467 + "(\<Sum>m=0..<(Suc n).
   1.468 +     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
   1.469 +by (induct "n", auto)
   1.470 +
   1.471 +lemma Maclaurin_cos_expansion:
   1.472 +     "\<exists>t. abs t \<le> abs x &
   1.473 +       cos x =
   1.474 +       (\<Sum>m=0..<n. (if even m
   1.475 +                       then -1 ^ (m div 2)/(real (fact m))
   1.476 +                       else 0) *
   1.477 +                       x ^ m)
   1.478 +      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.479 +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)
   1.480 +apply safe
   1.481 +apply (simp (no_asm))
   1.482 +apply (simp (no_asm))
   1.483 +apply (case_tac "n", simp)
   1.484 +apply (simp del: setsum_op_ivl_Suc)
   1.485 +apply (rule ccontr, simp)
   1.486 +apply (drule_tac x = x in spec, simp)
   1.487 +apply (erule ssubst)
   1.488 +apply (rule_tac x = t in exI, simp)
   1.489 +apply (rule setsum_cong[OF refl])
   1.490 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
   1.491 +done
   1.492 +
   1.493 +lemma Maclaurin_cos_expansion2:
   1.494 +     "[| 0 < x; n > 0 |] ==>
   1.495 +       \<exists>t. 0 < t & t < x &
   1.496 +       cos x =
   1.497 +       (\<Sum>m=0..<n. (if even m
   1.498 +                       then -1 ^ (m div 2)/(real (fact m))
   1.499 +                       else 0) *
   1.500 +                       x ^ m)
   1.501 +      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.502 +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)
   1.503 +apply safe
   1.504 +apply simp
   1.505 +apply (simp (no_asm))
   1.506 +apply (erule ssubst)
   1.507 +apply (rule_tac x = t in exI, simp)
   1.508 +apply (rule setsum_cong[OF refl])
   1.509 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
   1.510 +done
   1.511 +
   1.512 +lemma Maclaurin_minus_cos_expansion:
   1.513 +     "[| x < 0; n > 0 |] ==>
   1.514 +       \<exists>t. x < t & t < 0 &
   1.515 +       cos x =
   1.516 +       (\<Sum>m=0..<n. (if even m
   1.517 +                       then -1 ^ (m div 2)/(real (fact m))
   1.518 +                       else 0) *
   1.519 +                       x ^ m)
   1.520 +      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.521 +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)
   1.522 +apply safe
   1.523 +apply simp
   1.524 +apply (simp (no_asm))
   1.525 +apply (erule ssubst)
   1.526 +apply (rule_tac x = t in exI, simp)
   1.527 +apply (rule setsum_cong[OF refl])
   1.528 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
   1.529 +done
   1.530 +
   1.531 +(* ------------------------------------------------------------------------- *)
   1.532 +(* Version for ln(1 +/- x). Where is it??                                    *)
   1.533 +(* ------------------------------------------------------------------------- *)
   1.534 +
   1.535 +lemma sin_bound_lemma:
   1.536 +    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
   1.537 +by auto
   1.538 +
   1.539 +lemma Maclaurin_sin_bound:
   1.540 +  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   1.541 +  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
   1.542 +proof -
   1.543 +  have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   1.544 +    by (rule_tac mult_right_mono,simp_all)
   1.545 +  note est = this[simplified]
   1.546 +  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)"
   1.547 +  have diff_0: "?diff 0 = sin" by simp
   1.548 +  have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
   1.549 +    apply (clarify)
   1.550 +    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
   1.551 +    apply (cut_tac m=m in mod_exhaust_less_4)
   1.552 +    apply (safe, simp_all)
   1.553 +    apply (rule DERIV_minus, simp)
   1.554 +    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
   1.555 +    done
   1.556 +  from Maclaurin_all_le [OF diff_0 DERIV_diff]
   1.557 +  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
   1.558 +    t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
   1.559 +      ?diff n t / real (fact n) * x ^ n" by fast
   1.560 +  have diff_m_0:
   1.561 +    "\<And>m. ?diff m 0 = (if even m then 0
   1.562 +         else -1 ^ ((m - Suc 0) div 2))"
   1.563 +    apply (subst even_even_mod_4_iff)
   1.564 +    apply (cut_tac m=m in mod_exhaust_less_4)
   1.565 +    apply (elim disjE, simp_all)
   1.566 +    apply (safe dest!: mod_eqD, simp_all)
   1.567 +    done
   1.568 +  show ?thesis
   1.569 +    apply (subst t2)
   1.570 +    apply (rule sin_bound_lemma)
   1.571 +    apply (rule setsum_cong[OF refl])
   1.572 +    apply (subst diff_m_0, simp)
   1.573 +    apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
   1.574 +                   simp add: est mult_nonneg_nonneg mult_ac divide_inverse
   1.575 +                          power_abs [symmetric] abs_mult)
   1.576 +    done
   1.577 +qed
   1.578 +
   1.579 +end