1.1 --- a/src/HOL/MacLaurin.thy Tue Dec 14 00:16:30 2010 +0100
1.2 +++ b/src/HOL/MacLaurin.thy Wed Dec 15 08:34:01 2010 +0100
1.3 @@ -1,6 +1,7 @@
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 + Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard Häupler, 2005
1.8 *)
1.9
1.10 header{*MacLaurin Series*}
1.11 @@ -18,11 +19,9 @@
1.12 "0 < h ==>
1.13 \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
1.14 (B * ((h^n) / real(fact n)))"
1.15 -apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
1.16 +by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
1.17 real(fact n) / (h^n)"
1.18 - in exI)
1.19 -apply (simp)
1.20 -done
1.21 + in exI, simp)
1.22
1.23 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
1.24 by arith
1.25 @@ -32,46 +31,141 @@
1.26 by (subst fact_reduce_nat, auto)
1.27
1.28 lemma Maclaurin_lemma2:
1.29 - assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.30 - assumes n: "n = Suc k"
1.31 - assumes difg: "difg =
1.32 - (\<lambda>m t. diff m t -
1.33 - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.34 - B * (t ^ (n - m) / real (fact (n - m)))))"
1.35 - shows
1.36 - "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
1.37 -unfolding difg
1.38 - apply clarify
1.39 - apply (rule DERIV_diff)
1.40 - apply (simp add: diff)
1.41 - apply (simp only: n)
1.42 - apply (rule DERIV_add)
1.43 - apply (rule_tac [2] DERIV_cmult)
1.44 - apply (rule_tac [2] lemma_DERIV_subst)
1.45 - apply (rule_tac [2] DERIV_quotient)
1.46 - apply (rule_tac [3] DERIV_const)
1.47 - apply (rule_tac [2] DERIV_pow)
1.48 - prefer 3
1.49 + assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.50 + and INIT : "n = Suc k"
1.51 + and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.52 + B * (t ^ (n - m) / real (fact (n - m)))))"
1.53 + shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
1.54 +proof (rule allI)+
1.55 + fix m
1.56 + fix t
1.57 + show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
1.58 + proof
1.59 + assume INIT2: "m < n & 0 \<le> t & t \<le> h"
1.60 + hence INTERV: "0 \<le> t & t \<le> h" ..
1.61 + from INIT2 and INIT have mtok: "m < Suc k" by arith
1.62 + have "DERIV (\<lambda>t. diff m t -
1.63 + ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.64 + B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))
1.65 + t :> diff (Suc m) t -
1.66 + ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
1.67 + B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"
1.68 + proof -
1.69 + from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp
1.70 + moreover
1.71 + have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +
1.72 + B * (x ^ (Suc k - m) / real (fact (Suc k - m))))
1.73 + t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
1.74 + B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
1.75 + proof -
1.76 + have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t
1.77 + :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"
1.78 + proof -
1.79 + have "\<exists> d. k = m + d"
1.80 + proof -
1.81 + from INIT2 have "m < n" ..
1.82 + hence "\<exists> d. n = m + d + Suc 0" by arith
1.83 + with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)
1.84 + qed
1.85 + from this obtain d where kmd: "k = m + d" ..
1.86 + have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) +
1.87 + diff m 0)
1.88 + t :> (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"
1.89 +
1.90 + proof -
1.91 + have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) + diff m 0) t :> (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0"
1.92 + proof -
1.93 + from DERIV and INTERV have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma)))) t :> (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r))"
1.94 + proof -
1.95 + have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>
1.96 + DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
1.97 + :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
1.98 + proof (rule allI)
1.99 + fix r
1.100 + show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>
1.101 + DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
1.102 + :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
1.103 + proof
1.104 + assume "0 \<le> r & r < 0 + d"
1.105 + have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *
1.106 + (x ^ Suc r * inverse (real (fact (Suc r)))))
1.107 + t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"
1.108 + proof -
1.109 + have "(1 + real r) * real (fact r) \<noteq> 0" by auto
1.110 + from this have "real (fact r) + real r * real (fact r) \<noteq> 0"
1.111 + by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)
1.112 + from this have "DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t :> real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
1.113 + 0 * t ^ Suc r"
1.114 + apply - by ( rule DERIV_intros | rule refl)+ auto
1.115 + moreover
1.116 + have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
1.117 + 0 * t ^ Suc r =
1.118 + t ^ r * inverse (real (fact r))"
1.119 + proof -
1.120 +
1.121 + have " real (Suc r) * t ^ (Suc r - Suc 0) *
1.122 + inverse (real (Suc r) * real (fact r)) +
1.123 + 0 * t ^ Suc r =
1.124 + t ^ r * inverse (real (fact r))" by (simp add: mult_ac)
1.125 + hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +
1.126 + 0 * t ^ Suc r =
1.127 + t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)
1.128 + thus ?thesis by (subst fact_Suc)
1.129 + qed
1.130 + ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t
1.131 + :> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)
1.132 + thus ?thesis by (rule DERIV_cmult)
1.133 + qed
1.134 + thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /
1.135 + real (fact (Suc r)))
1.136 + t :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)" by (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
1.137 + qed
1.138 + qed
1.139 + thus ?thesis by (rule DERIV_sumr)
1.140 + qed
1.141 + moreover
1.142 + from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .
1.143 + ultimately show ?thesis by (rule DERIV_add)
1.144 + qed
1.145 + moreover
1.146 + have " (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0 = (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))" by simp
1.147 + ultimately show ?thesis by (rule lemma_DERIV_subst)
1.148 + qed
1.149 + with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
1.150 + qed
1.151 + moreover
1.152 + have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t
1.153 + :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
1.154 + proof -
1.155 + have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t
1.156 + :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"
1.157 + proof -
1.158 + have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)
1.159 + moreover
1.160 + have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)
1.161 + moreover
1.162 + have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp
1.163 + ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t
1.164 + :> ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
1.165 + real (fact (Suc k - m)) ^ Suc (Suc 0)"
1.166 + apply -
1.167 + apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto
1.168 + moreover
1.169 + from mtok and INIT have "( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
1.170 + real (fact (Suc k - m)) ^ Suc (Suc 0) = t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))" by (simp add: fact_diff_Suc)
1.171 + ultimately show ?thesis by (rule lemma_DERIV_subst)
1.172 + qed
1.173 + moreover
1.174 + thus ?thesis by (rule DERIV_cmult)
1.175 + qed
1.176 + ultimately show ?thesis by (rule DERIV_add)
1.177 + qed
1.178 + ultimately show ?thesis by (rule DERIV_diff)
1.179 + qed
1.180 + from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify
1.181 + qed
1.182 +qed
1.183
1.184 -apply (simp add: fact_diff_Suc)
1.185 - prefer 2 apply simp
1.186 - apply (frule less_iff_Suc_add [THEN iffD1], clarify)
1.187 - apply (simp del: setsum_op_ivl_Suc)
1.188 - apply (insert sumr_offset4 [of "Suc 0"])
1.189 - apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
1.190 - apply (rule lemma_DERIV_subst)
1.191 - apply (rule DERIV_add)
1.192 - apply (rule_tac [2] DERIV_const)
1.193 - apply (rule DERIV_sumr, clarify)
1.194 - prefer 2 apply simp
1.195 - apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
1.196 - apply (rule DERIV_cmult)
1.197 - apply (rule lemma_DERIV_subst)
1.198 - apply (best intro!: DERIV_intros)
1.199 - apply (subst fact_Suc)
1.200 - apply (subst real_of_nat_mult)
1.201 - apply (simp add: mult_ac)
1.202 -done
1.203
1.204 lemma Maclaurin:
1.205 assumes h: "0 < h"
1.206 @@ -83,7 +177,7 @@
1.207 "\<exists>t. 0 < t & t < h &
1.208 f h =
1.209 setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
1.210 - (diff n t / real (fact n)) * h ^ n"
1.211 + (diff n t / real (fact n)) * h ^ n"
1.212 proof -
1.213 from n obtain m where m: "n = Suc m"
1.214 by (cases n, simp add: n)
1.215 @@ -195,17 +289,23 @@
1.216
1.217
1.218 lemma Maclaurin2:
1.219 - "[| 0 < h; diff 0 = f;
1.220 - \<forall>m t.
1.221 - m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
1.222 - ==> \<exists>t. 0 < t &
1.223 - t \<le> h &
1.224 - f h =
1.225 - (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.226 - diff n t / real (fact n) * h ^ n"
1.227 -apply (case_tac "n", auto)
1.228 -apply (drule Maclaurin, auto)
1.229 -done
1.230 + assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
1.231 + and DERIV: "\<forall>m t.
1.232 + m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
1.233 + shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
1.234 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.235 + diff n t / real (fact n) * h ^ n"
1.236 +proof (cases "n")
1.237 + case 0 with INIT1 INIT2 show ?thesis by fastsimp
1.238 +next
1.239 + case Suc
1.240 + hence "n > 0" by simp
1.241 + from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
1.242 + f h =
1.243 + (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
1.244 + by (rule Maclaurin)
1.245 + thus ?thesis by fastsimp
1.246 +qed
1.247
1.248 lemma Maclaurin2_objl:
1.249 "0 < h & diff 0 = f &
1.250 @@ -219,31 +319,62 @@
1.251 by (blast intro: Maclaurin2)
1.252
1.253 lemma Maclaurin_minus:
1.254 - "[| h < 0; n > 0; diff 0 = f;
1.255 - \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
1.256 - ==> \<exists>t. h < t &
1.257 - t < 0 &
1.258 - f h =
1.259 - (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.260 - diff n t / real (fact n) * h ^ n"
1.261 -apply (cut_tac f = "%x. f (-x)"
1.262 - and diff = "%n x. (-1 ^ n) * diff n (-x)"
1.263 - and h = "-h" and n = n in Maclaurin_objl)
1.264 -apply (simp)
1.265 -apply safe
1.266 -apply (subst minus_mult_right)
1.267 -apply (rule DERIV_cmult)
1.268 -apply (rule lemma_DERIV_subst)
1.269 -apply (rule DERIV_chain2 [where g=uminus])
1.270 -apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
1.271 -prefer 2 apply force
1.272 -apply force
1.273 -apply (rule_tac x = "-t" in exI, auto)
1.274 -apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
1.275 - (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
1.276 -apply (rule_tac [2] setsum_cong[OF refl])
1.277 -apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
1.278 -done
1.279 + assumes INTERV : "h < 0" and
1.280 + INIT : "0 < n" "diff 0 = f" and
1.281 + ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
1.282 + shows "\<exists>t. h < t & t < 0 &
1.283 + f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.284 + diff n t / real (fact n) * h ^ n"
1.285 +proof -
1.286 + from INTERV have "0 < -h" by simp
1.287 + moreover
1.288 + from INIT have "0 < n" by simp
1.289 + moreover
1.290 + from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp
1.291 + moreover
1.292 + have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>
1.293 + DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
1.294 + proof (rule allI impI)+
1.295 + fix m t
1.296 + assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"
1.297 + with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
1.298 + proof -
1.299 +
1.300 + from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)
1.301 + proof -
1.302 + from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force
1.303 + moreover
1.304 + from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus)
1.305 + ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)
1.306 + thus ?thesis by simp
1.307 + qed
1.308 + thus ?thesis
1.309 + proof -
1.310 + assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)
1.311 + hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)
1.312 + thus ?thesis by simp
1.313 + qed
1.314 + qed
1.315 + qed
1.316 + ultimately have t_exists: "\<exists>t>0. t < - h \<and>
1.317 + f (- (- h)) =
1.318 + (\<Sum>m = 0..<n.
1.319 + (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
1.320 + (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
1.321 + from this obtain t where t_def: "?P t" ..
1.322 + moreover
1.323 + have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
1.324 + by (auto simp add: power_mult_distrib[symmetric])
1.325 + moreover
1.326 + have "(SUM m = 0..<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m = 0..<n. diff m 0 * h ^ m / real (fact m))"
1.327 + by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
1.328 + ultimately have " h < - t \<and>
1.329 + - t < 0 \<and>
1.330 + f h =
1.331 + (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
1.332 + by auto
1.333 + thus ?thesis ..
1.334 +qed
1.335
1.336 lemma Maclaurin_minus_objl:
1.337 "(h < 0 & n > 0 & diff 0 = f &
1.338 @@ -269,42 +400,109 @@
1.339 by (induct "n", auto)
1.340
1.341 lemma Maclaurin_bi_le:
1.342 - "[| diff 0 = f;
1.343 - \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
1.344 - ==> \<exists>t. abs t \<le> abs x &
1.345 + assumes INIT : "diff 0 = f"
1.346 + and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
1.347 + shows "\<exists>t. abs t \<le> abs x &
1.348 f x =
1.349 (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
1.350 diff n t / real (fact n) * x ^ n"
1.351 -apply (case_tac "n = 0", force)
1.352 -apply (case_tac "x = 0")
1.353 - apply (rule_tac x = 0 in exI)
1.354 - apply (force simp add: Maclaurin_bi_le_lemma)
1.355 -apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
1.356 - txt{*Case 1, where @{term "x < 0"}*}
1.357 - apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
1.358 - apply (simp add: abs_if)
1.359 - apply (rule_tac x = t in exI)
1.360 - apply (simp add: abs_if)
1.361 -txt{*Case 2, where @{term "0 < x"}*}
1.362 -apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
1.363 - apply (simp add: abs_if)
1.364 -apply (rule_tac x = t in exI)
1.365 -apply (simp add: abs_if)
1.366 -done
1.367 +proof (cases "n = 0")
1.368 + case True from INIT True show ?thesis by force
1.369 +next
1.370 + case False
1.371 + from this have n_not_zero:"n \<noteq> 0" .
1.372 + from False INIT DERIV show ?thesis
1.373 + proof (cases "x = 0")
1.374 + case True show ?thesis
1.375 + proof -
1.376 + from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
1.377 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n" by(force simp add: Maclaurin_bi_le_lemma)
1.378 + thus ?thesis ..
1.379 + qed
1.380 + next
1.381 + case False
1.382 + note linorder_less_linear [of "x" "0"]
1.383 + thus ?thesis
1.384 + proof (elim disjE)
1.385 + assume "x = 0" with False show ?thesis ..
1.386 + next
1.387 + assume x_less_zero: "x < 0" moreover
1.388 + from n_not_zero have "0 < n" by simp moreover
1.389 + have "diff 0 = diff 0" by simp moreover
1.390 + have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.391 + proof (rule allI, rule allI, rule impI)
1.392 + fix m t
1.393 + assume "m < n & x \<le> t & t \<le> 0"
1.394 + with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)
1.395 + qed
1.396 + ultimately have t_exists:"\<exists>t>x. t < 0 \<and>
1.397 + diff 0 x =
1.398 + (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
1.399 + from this obtain t where t_def: "?P t" ..
1.400 + from t_def x_less_zero INIT have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
1.401 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
1.402 + by (simp add: abs_if order_less_le)
1.403 + thus ?thesis by (rule exI)
1.404 + next
1.405 + assume x_greater_zero: "x > 0" moreover
1.406 + from n_not_zero have "0 < n" by simp moreover
1.407 + have "diff 0 = diff 0" by simp moreover
1.408 + have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.409 + proof (rule allI, rule allI, rule impI)
1.410 + fix m t
1.411 + assume "m < n & 0 \<le> t & t \<le> x"
1.412 + with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp
1.413 + qed
1.414 + ultimately have t_exists:"\<exists>t>0. t < x \<and>
1.415 + diff 0 x =
1.416 + (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
1.417 + from this obtain t where t_def: "?P t" ..
1.418 + from t_def x_greater_zero INIT have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
1.419 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
1.420 + by fastsimp
1.421 + thus ?thesis ..
1.422 + qed
1.423 + qed
1.424 +qed
1.425 +
1.426
1.427 lemma Maclaurin_all_lt:
1.428 - "[| diff 0 = f;
1.429 - \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
1.430 - x ~= 0; n > 0
1.431 - |] ==> \<exists>t. 0 < abs t & abs t < abs x &
1.432 + assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
1.433 + and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
1.434 + shows "\<exists>t. 0 < abs t & abs t < abs x &
1.435 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.436 - (diff n t / real (fact n)) * x ^ n"
1.437 -apply (rule_tac x = x and y = 0 in linorder_cases)
1.438 -prefer 2 apply blast
1.439 -apply (drule_tac [2] diff=diff in Maclaurin)
1.440 -apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
1.441 -apply (rule_tac [!] x = t in exI, auto)
1.442 -done
1.443 + (diff n t / real (fact n)) * x ^ n"
1.444 +proof -
1.445 + have "(x = 0) \<Longrightarrow> ?thesis"
1.446 + proof -
1.447 + assume "x = 0"
1.448 + with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..
1.449 + qed
1.450 + moreover have "(x < 0) \<Longrightarrow> ?thesis"
1.451 + proof -
1.452 + assume x_less_zero: "x < 0"
1.453 + from DERIV have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp
1.454 + with x_less_zero INIT2 INIT1 have "\<exists>t>x. t < 0 \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
1.455 + from this obtain t where "?P t" ..
1.456 + with x_less_zero have "0 < \<bar>t\<bar> \<and>
1.457 + \<bar>t\<bar> < \<bar>x\<bar> \<and>
1.458 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by simp
1.459 + thus ?thesis ..
1.460 + qed
1.461 + moreover have "(x > 0) \<Longrightarrow> ?thesis"
1.462 + proof -
1.463 + assume x_greater_zero: "x > 0"
1.464 + from DERIV have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp
1.465 + with x_greater_zero INIT2 INIT1 have "\<exists>t>0. t < x \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
1.466 + from this obtain t where "?P t" ..
1.467 + with x_greater_zero have "0 < \<bar>t\<bar> \<and>
1.468 + \<bar>t\<bar> < \<bar>x\<bar> \<and>
1.469 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by fastsimp
1.470 + thus ?thesis ..
1.471 + qed
1.472 + ultimately show ?thesis by (fastsimp)
1.473 +qed
1.474 +
1.475
1.476 lemma Maclaurin_all_lt_objl:
1.477 "diff 0 = f &
1.478 @@ -322,20 +520,42 @@
1.479 diff 0 0"
1.480 by (induct n, auto)
1.481
1.482 -lemma Maclaurin_all_le: "[| diff 0 = f;
1.483 - \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
1.484 - |] ==> \<exists>t. abs t \<le> abs x &
1.485 +
1.486 +lemma Maclaurin_all_le:
1.487 + assumes INIT: "diff 0 = f"
1.488 + and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
1.489 + shows "\<exists>t. abs t \<le> abs x &
1.490 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.491 (diff n t / real (fact n)) * x ^ n"
1.492 -apply(cases "n=0")
1.493 -apply (force)
1.494 -apply (case_tac "x = 0")
1.495 -apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
1.496 -apply (drule not0_implies_Suc)
1.497 -apply (rule_tac x = 0 in exI, force)
1.498 -apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
1.499 -apply (rule_tac x = t in exI, auto)
1.500 -done
1.501 +proof -
1.502 + note linorder_le_less_linear [of n 0]
1.503 + thus ?thesis
1.504 + proof
1.505 + assume "n\<le> 0" with INIT show ?thesis by force
1.506 + next
1.507 + assume n_greater_zero: "n > 0" show ?thesis
1.508 + proof (cases "x = 0")
1.509 + case True
1.510 + from n_greater_zero have "n \<noteq> 0" by auto
1.511 + from True this have f_0:"(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" by (rule Maclaurin_zero)
1.512 + from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)
1.513 + hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)
1.514 + with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
1.515 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"
1.516 + by force
1.517 + thus ?thesis ..
1.518 + next
1.519 + case False
1.520 + from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>
1.521 + \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_all_lt)
1.522 + from this obtain t where "?P t" ..
1.523 + hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
1.524 + f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by (simp add: order_less_le)
1.525 + thus ?thesis ..
1.526 + qed
1.527 + qed
1.528 +qed
1.529 +
1.530
1.531 lemma Maclaurin_all_le_objl: "diff 0 = f &
1.532 (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)