--- a/src/HOL/MacLaurin.thy Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/MacLaurin.thy Wed Dec 15 08:34:01 2010 +0100
@@ -1,6 +1,7 @@
(* Author : Jacques D. Fleuriot
Copyright : 2001 University of Edinburgh
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+ Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard Häupler, 2005
*)
header{*MacLaurin Series*}
@@ -18,11 +19,9 @@
"0 < h ==>
\<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
(B * ((h^n) / real(fact n)))"
-apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
+by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
real(fact n) / (h^n)"
- in exI)
-apply (simp)
-done
+ in exI, simp)
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
by arith
@@ -32,46 +31,141 @@
by (subst fact_reduce_nat, auto)
lemma Maclaurin_lemma2:
- assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
- assumes n: "n = Suc k"
- assumes difg: "difg =
- (\<lambda>m t. diff m t -
- ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
- B * (t ^ (n - m) / real (fact (n - m)))))"
- shows
- "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
-unfolding difg
- apply clarify
- apply (rule DERIV_diff)
- apply (simp add: diff)
- apply (simp only: n)
- apply (rule DERIV_add)
- apply (rule_tac [2] DERIV_cmult)
- apply (rule_tac [2] lemma_DERIV_subst)
- apply (rule_tac [2] DERIV_quotient)
- apply (rule_tac [3] DERIV_const)
- apply (rule_tac [2] DERIV_pow)
- prefer 3
+ assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+ and INIT : "n = Suc k"
+ and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
+ B * (t ^ (n - m) / real (fact (n - m)))))"
+ shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
+proof (rule allI)+
+ fix m
+ fix t
+ show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
+ proof
+ assume INIT2: "m < n & 0 \<le> t & t \<le> h"
+ hence INTERV: "0 \<le> t & t \<le> h" ..
+ from INIT2 and INIT have mtok: "m < Suc k" by arith
+ have "DERIV (\<lambda>t. diff m t -
+ ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +
+ B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))
+ t :> diff (Suc m) t -
+ ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
+ B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"
+ proof -
+ from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp
+ moreover
+ have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +
+ B * (x ^ (Suc k - m) / real (fact (Suc k - m))))
+ t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
+ B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
+ proof -
+ have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t
+ :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"
+ proof -
+ have "\<exists> d. k = m + d"
+ proof -
+ from INIT2 have "m < n" ..
+ hence "\<exists> d. n = m + d + Suc 0" by arith
+ with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)
+ qed
+ from this obtain d where kmd: "k = m + d" ..
+ 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>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"
+
+ proof -
+ 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"
+ proof -
+ 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))"
+ proof -
+ have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>
+ DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
+ :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
+ proof (rule allI)
+ fix r
+ show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>
+ DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
+ :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
+ proof
+ assume "0 \<le> r & r < 0 + d"
+ have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *
+ (x ^ Suc r * inverse (real (fact (Suc r)))))
+ t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"
+ proof -
+ have "(1 + real r) * real (fact r) \<noteq> 0" by auto
+ from this have "real (fact r) + real r * real (fact r) \<noteq> 0"
+ by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)
+ 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))) +
+ 0 * t ^ Suc r"
+ apply - by ( rule DERIV_intros | rule refl)+ auto
+ moreover
+ have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
+ 0 * t ^ Suc r =
+ t ^ r * inverse (real (fact r))"
+ proof -
+
+ have " real (Suc r) * t ^ (Suc r - Suc 0) *
+ inverse (real (Suc r) * real (fact r)) +
+ 0 * t ^ Suc r =
+ t ^ r * inverse (real (fact r))" by (simp add: mult_ac)
+ hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +
+ 0 * t ^ Suc r =
+ t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)
+ thus ?thesis by (subst fact_Suc)
+ qed
+ ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t
+ :> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)
+ thus ?thesis by (rule DERIV_cmult)
+ qed
+ thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /
+ real (fact (Suc r)))
+ 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)
+ qed
+ qed
+ thus ?thesis by (rule DERIV_sumr)
+ qed
+ moreover
+ from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .
+ ultimately show ?thesis by (rule DERIV_add)
+ qed
+ moreover
+ 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
+ ultimately show ?thesis by (rule lemma_DERIV_subst)
+ qed
+ with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
+ qed
+ moreover
+ have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t
+ :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
+ proof -
+ have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t
+ :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"
+ proof -
+ have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)
+ moreover
+ have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)
+ moreover
+ have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp
+ ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t
+ :> ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
+ real (fact (Suc k - m)) ^ Suc (Suc 0)"
+ apply -
+ apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto
+ moreover
+ 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))) /
+ 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)
+ ultimately show ?thesis by (rule lemma_DERIV_subst)
+ qed
+ moreover
+ thus ?thesis by (rule DERIV_cmult)
+ qed
+ ultimately show ?thesis by (rule DERIV_add)
+ qed
+ ultimately show ?thesis by (rule DERIV_diff)
+ qed
+ from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify
+ qed
+qed
-apply (simp add: fact_diff_Suc)
- prefer 2 apply simp
- apply (frule less_iff_Suc_add [THEN iffD1], clarify)
- apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
- apply (rule lemma_DERIV_subst)
- apply (rule DERIV_add)
- apply (rule_tac [2] DERIV_const)
- apply (rule DERIV_sumr, clarify)
- prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
- apply (rule DERIV_cmult)
- apply (rule lemma_DERIV_subst)
- apply (best intro!: DERIV_intros)
- apply (subst fact_Suc)
- apply (subst real_of_nat_mult)
- apply (simp add: mult_ac)
-done
lemma Maclaurin:
assumes h: "0 < h"
@@ -83,7 +177,7 @@
"\<exists>t. 0 < t & t < h &
f h =
setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
- (diff n t / real (fact n)) * h ^ n"
+ (diff n t / real (fact n)) * h ^ n"
proof -
from n obtain m where m: "n = Suc m"
by (cases n, simp add: n)
@@ -195,17 +289,23 @@
lemma Maclaurin2:
- "[| 0 < h; diff 0 = f;
- \<forall>m t.
- m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
- ==> \<exists>t. 0 < t &
- t \<le> h &
- f h =
- (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n"
-apply (case_tac "n", auto)
-apply (drule Maclaurin, auto)
-done
+ assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
+ and DERIV: "\<forall>m t.
+ m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
+ shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
+ diff n t / real (fact n) * h ^ n"
+proof (cases "n")
+ case 0 with INIT1 INIT2 show ?thesis by fastsimp
+next
+ case Suc
+ hence "n > 0" by simp
+ from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
+ f h =
+ (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
+ by (rule Maclaurin)
+ thus ?thesis by fastsimp
+qed
lemma Maclaurin2_objl:
"0 < h & diff 0 = f &
@@ -219,31 +319,62 @@
by (blast intro: Maclaurin2)
lemma Maclaurin_minus:
- "[| h < 0; n > 0; diff 0 = f;
- \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
- ==> \<exists>t. h < t &
- t < 0 &
- f h =
- (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n"
-apply (cut_tac f = "%x. f (-x)"
- and diff = "%n x. (-1 ^ n) * diff n (-x)"
- and h = "-h" and n = n in Maclaurin_objl)
-apply (simp)
-apply safe
-apply (subst minus_mult_right)
-apply (rule DERIV_cmult)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_chain2 [where g=uminus])
-apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
-prefer 2 apply force
-apply force
-apply (rule_tac x = "-t" in exI, auto)
-apply (subgoal_tac "(\<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))")
-apply (rule_tac [2] setsum_cong[OF refl])
-apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
-done
+ assumes INTERV : "h < 0" and
+ INIT : "0 < n" "diff 0 = f" and
+ ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
+ shows "\<exists>t. h < t & t < 0 &
+ f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
+ diff n t / real (fact n) * h ^ n"
+proof -
+ from INTERV have "0 < -h" by simp
+ moreover
+ from INIT have "0 < n" by simp
+ moreover
+ from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp
+ moreover
+ have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>
+ DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
+ proof (rule allI impI)+
+ fix m t
+ assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"
+ with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
+ proof -
+
+ from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)
+ proof -
+ from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force
+ moreover
+ from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus)
+ ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)
+ thus ?thesis by simp
+ qed
+ thus ?thesis
+ proof -
+ assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)
+ hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)
+ thus ?thesis by simp
+ qed
+ qed
+ qed
+ ultimately have t_exists: "\<exists>t>0. t < - h \<and>
+ f (- (- h)) =
+ (\<Sum>m = 0..<n.
+ (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
+ (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
+ from this obtain t where t_def: "?P t" ..
+ moreover
+ have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
+ by (auto simp add: power_mult_distrib[symmetric])
+ moreover
+ 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))"
+ by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
+ ultimately have " h < - t \<and>
+ - t < 0 \<and>
+ f h =
+ (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
+ by auto
+ thus ?thesis ..
+qed
lemma Maclaurin_minus_objl:
"(h < 0 & n > 0 & diff 0 = f &
@@ -269,42 +400,109 @@
by (induct "n", auto)
lemma Maclaurin_bi_le:
- "[| diff 0 = f;
- \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
- ==> \<exists>t. abs t \<le> abs x &
+ assumes INIT : "diff 0 = f"
+ and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
+ shows "\<exists>t. abs t \<le> abs x &
f x =
(\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
diff n t / real (fact n) * x ^ n"
-apply (case_tac "n = 0", force)
-apply (case_tac "x = 0")
- apply (rule_tac x = 0 in exI)
- apply (force simp add: Maclaurin_bi_le_lemma)
-apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
- txt{*Case 1, where @{term "x < 0"}*}
- apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
- apply (simp add: abs_if)
- apply (rule_tac x = t in exI)
- apply (simp add: abs_if)
-txt{*Case 2, where @{term "0 < x"}*}
-apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
- apply (simp add: abs_if)
-apply (rule_tac x = t in exI)
-apply (simp add: abs_if)
-done
+proof (cases "n = 0")
+ case True from INIT True show ?thesis by force
+next
+ case False
+ from this have n_not_zero:"n \<noteq> 0" .
+ from False INIT DERIV show ?thesis
+ proof (cases "x = 0")
+ case True show ?thesis
+ proof -
+ from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
+ 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)
+ thus ?thesis ..
+ qed
+ next
+ case False
+ note linorder_less_linear [of "x" "0"]
+ thus ?thesis
+ proof (elim disjE)
+ assume "x = 0" with False show ?thesis ..
+ next
+ assume x_less_zero: "x < 0" moreover
+ from n_not_zero have "0 < n" by simp moreover
+ have "diff 0 = diff 0" by simp moreover
+ have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+ proof (rule allI, rule allI, rule impI)
+ fix m t
+ assume "m < n & x \<le> t & t \<le> 0"
+ with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)
+ qed
+ ultimately have t_exists:"\<exists>t>x. t < 0 \<and>
+ diff 0 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)
+ from this obtain t where t_def: "?P t" ..
+ from t_def x_less_zero INIT have "\<bar>t\<bar> \<le> \<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"
+ by (simp add: abs_if order_less_le)
+ thus ?thesis by (rule exI)
+ next
+ assume x_greater_zero: "x > 0" moreover
+ from n_not_zero have "0 < n" by simp moreover
+ have "diff 0 = diff 0" by simp moreover
+ have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+ proof (rule allI, rule allI, rule impI)
+ fix m t
+ assume "m < n & 0 \<le> t & t \<le> x"
+ with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp
+ qed
+ ultimately have t_exists:"\<exists>t>0. t < x \<and>
+ diff 0 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)
+ from this obtain t where t_def: "?P t" ..
+ from t_def x_greater_zero INIT have "\<bar>t\<bar> \<le> \<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"
+ by fastsimp
+ thus ?thesis ..
+ qed
+ qed
+qed
+
lemma Maclaurin_all_lt:
- "[| diff 0 = f;
- \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
- x ~= 0; n > 0
- |] ==> \<exists>t. 0 < abs t & abs t < abs x &
+ assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
+ and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
+ shows "\<exists>t. 0 < abs t & abs t < abs x &
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
- (diff n t / real (fact n)) * x ^ n"
-apply (rule_tac x = x and y = 0 in linorder_cases)
-prefer 2 apply blast
-apply (drule_tac [2] diff=diff in Maclaurin)
-apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
-apply (rule_tac [!] x = t in exI, auto)
-done
+ (diff n t / real (fact n)) * x ^ n"
+proof -
+ have "(x = 0) \<Longrightarrow> ?thesis"
+ proof -
+ assume "x = 0"
+ with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..
+ qed
+ moreover have "(x < 0) \<Longrightarrow> ?thesis"
+ proof -
+ assume x_less_zero: "x < 0"
+ 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
+ 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)
+ from this obtain t where "?P t" ..
+ with x_less_zero have "0 < \<bar>t\<bar> \<and>
+ \<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" by simp
+ thus ?thesis ..
+ qed
+ moreover have "(x > 0) \<Longrightarrow> ?thesis"
+ proof -
+ assume x_greater_zero: "x > 0"
+ 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
+ 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)
+ from this obtain t where "?P t" ..
+ with x_greater_zero have "0 < \<bar>t\<bar> \<and>
+ \<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" by fastsimp
+ thus ?thesis ..
+ qed
+ ultimately show ?thesis by (fastsimp)
+qed
+
lemma Maclaurin_all_lt_objl:
"diff 0 = f &
@@ -322,20 +520,42 @@
diff 0 0"
by (induct n, auto)
-lemma Maclaurin_all_le: "[| diff 0 = f;
- \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
- |] ==> \<exists>t. abs t \<le> abs x &
+
+lemma Maclaurin_all_le:
+ assumes INIT: "diff 0 = f"
+ and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
+ shows "\<exists>t. abs t \<le> abs x &
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n"
-apply(cases "n=0")
-apply (force)
-apply (case_tac "x = 0")
-apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
-apply (drule not0_implies_Suc)
-apply (rule_tac x = 0 in exI, force)
-apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
-apply (rule_tac x = t in exI, auto)
-done
+proof -
+ note linorder_le_less_linear [of n 0]
+ thus ?thesis
+ proof
+ assume "n\<le> 0" with INIT show ?thesis by force
+ next
+ assume n_greater_zero: "n > 0" show ?thesis
+ proof (cases "x = 0")
+ case True
+ from n_greater_zero have "n \<noteq> 0" by auto
+ 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)
+ from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)
+ hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)
+ with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
+ f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"
+ by force
+ thus ?thesis ..
+ next
+ case False
+ from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>
+ \<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)
+ from this obtain t where "?P t" ..
+ hence "\<bar>t\<bar> \<le> \<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" by (simp add: order_less_le)
+ thus ?thesis ..
+ qed
+ qed
+qed
+
lemma Maclaurin_all_le_objl: "diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)