src/HOL/MacLaurin.thy
changeset 41120 74e41b2d48ea
parent 36974 b877866b5b00
child 41166 4b2a457b17e8
     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)