clean up proofs of lemma Maclaurin
authorhuffman
Sun Dec 28 14:40:43 2008 -0800 (2008-12-28)
changeset 291877b09385234f9
parent 29184 85889d58b5da
child 29188 ff41885a1234
clean up proofs of lemma Maclaurin
src/HOL/MacLaurin.thy
     1.1 --- a/src/HOL/MacLaurin.thy	Sun Dec 28 16:39:27 2008 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Sun Dec 28 14:40:43 2008 -0800
     1.3 @@ -58,129 +58,157 @@
     1.4  *}
     1.5  
     1.6  lemma Maclaurin_lemma2:
     1.7 -      "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t;
     1.8 -          n = Suc k;
     1.9 -        difg =
    1.10 +  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.11 +  assumes n: "n = Suc k"
    1.12 +  assumes difg: "difg =
    1.13          (\<lambda>m t. diff m t -
    1.14                 ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    1.15 -                B * (t ^ (n - m) / real (fact (n - m)))))|] ==>
    1.16 -        \<forall>m t. m < n & 0 \<le> t & t \<le> h -->
    1.17 -                    DERIV (difg m) t :> difg (Suc m) t"
    1.18 -apply clarify
    1.19 -apply (rule DERIV_diff)
    1.20 -apply (simp (no_asm_simp))
    1.21 -apply (tactic {* DERIV_tac @{context} *})
    1.22 -apply (tactic {* DERIV_tac @{context} *})
    1.23 -apply (rule_tac [2] lemma_DERIV_subst)
    1.24 -apply (rule_tac [2] DERIV_quotient)
    1.25 -apply (rule_tac [3] DERIV_const)
    1.26 -apply (rule_tac [2] DERIV_pow)
    1.27 -  prefer 3 apply (simp add: fact_diff_Suc)
    1.28 - prefer 2 apply simp
    1.29 -apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.30 -apply (simp del: setsum_op_ivl_Suc)
    1.31 -apply (insert sumr_offset4 [of 1])
    1.32 -apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.33 -apply (rule lemma_DERIV_subst)
    1.34 -apply (rule DERIV_add)
    1.35 -apply (rule_tac [2] DERIV_const)
    1.36 -apply (rule DERIV_sumr, clarify)
    1.37 - prefer 2 apply simp
    1.38 -apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
    1.39 -apply (rule DERIV_cmult)
    1.40 -apply (rule lemma_DERIV_subst)
    1.41 -apply (best intro: DERIV_chain2 intro!: DERIV_intros)
    1.42 -apply (subst fact_Suc)
    1.43 -apply (subst real_of_nat_mult)
    1.44 -apply (simp add: mult_ac)
    1.45 +                B * (t ^ (n - m) / real (fact (n - m)))))"
    1.46 +  shows
    1.47 +      "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
    1.48 +unfolding difg
    1.49 + apply clarify
    1.50 + apply (rule DERIV_diff)
    1.51 +  apply (simp add: diff)
    1.52 + apply (simp only: n)
    1.53 + apply (rule DERIV_add)
    1.54 +  apply (rule_tac [2] DERIV_cmult)
    1.55 +  apply (rule_tac [2] lemma_DERIV_subst)
    1.56 +   apply (rule_tac [2] DERIV_quotient)
    1.57 +     apply (rule_tac [3] DERIV_const)
    1.58 +    apply (rule_tac [2] DERIV_pow)
    1.59 +   prefer 3 apply (simp add: fact_diff_Suc)
    1.60 +  prefer 2 apply simp
    1.61 + apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.62 + apply (simp del: setsum_op_ivl_Suc)
    1.63 + apply (insert sumr_offset4 [of 1])
    1.64 + apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.65 + apply (rule lemma_DERIV_subst)
    1.66 +  apply (rule DERIV_add)
    1.67 +   apply (rule_tac [2] DERIV_const)
    1.68 +  apply (rule DERIV_sumr, clarify)
    1.69 +  prefer 2 apply simp
    1.70 + apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
    1.71 + apply (rule DERIV_cmult)
    1.72 + apply (rule lemma_DERIV_subst)
    1.73 +  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
    1.74 + apply (subst fact_Suc)
    1.75 + apply (subst real_of_nat_mult)
    1.76 + apply (simp add: mult_ac)
    1.77  done
    1.78  
    1.79  
    1.80 -lemma Maclaurin_lemma3:
    1.81 -  fixes difg :: "nat => real => real" shows
    1.82 -     "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
    1.83 -        \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0;  n < m; 0 < t;
    1.84 -        t < h|]
    1.85 -     ==> \<exists>ta. 0 < ta & ta < t & DERIV (difg (Suc n)) ta :> 0"
    1.86 -apply (rule Rolle, assumption, simp)
    1.87 -apply (drule_tac x = n and P="%k. k<Suc m --> difg k 0 = 0" in spec)
    1.88 -apply (rule DERIV_unique)
    1.89 -prefer 2 apply assumption
    1.90 -apply force
    1.91 -apply (metis DERIV_isCont dlo_simps(4) dlo_simps(9) less_trans_Suc nat_less_le not_less_eq real_le_trans)
    1.92 -apply (metis Suc_less_eq differentiableI dlo_simps(7) dlo_simps(8) dlo_simps(9)   real_le_trans xt1(8))
    1.93 -done
    1.94 -
    1.95  lemma Maclaurin:
    1.96 -   "[| 0 < h; n > 0; diff 0 = f;
    1.97 -       \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
    1.98 -    ==> \<exists>t. 0 < t &
    1.99 -              t < h &
   1.100 +  assumes h: "0 < h"
   1.101 +  assumes n: "0 < n"
   1.102 +  assumes diff_0: "diff 0 = f"
   1.103 +  assumes diff_Suc:
   1.104 +    "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
   1.105 +  shows
   1.106 +    "\<exists>t. 0 < t & t < h &
   1.107                f h =
   1.108                setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
   1.109                (diff n t / real (fact n)) * h ^ n"
   1.110 -apply (case_tac "n = 0", force)
   1.111 -apply (drule not0_implies_Suc)
   1.112 -apply (erule exE)
   1.113 -apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
   1.114 -apply (erule exE)
   1.115 -apply (subgoal_tac "\<exists>g.
   1.116 -     g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
   1.117 - prefer 2 apply blast
   1.118 -apply (erule exE)
   1.119 -apply (subgoal_tac "g 0 = 0 & g h =0")
   1.120 - prefer 2
   1.121 - apply (simp del: setsum_op_ivl_Suc)
   1.122 - apply (cut_tac n = m and k = 1 in sumr_offset2)
   1.123 - apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
   1.124 -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.125 - prefer 2 apply blast
   1.126 -apply (erule exE)
   1.127 -apply (subgoal_tac "difg 0 = g")
   1.128 - prefer 2 apply simp
   1.129 -apply (frule Maclaurin_lemma2, assumption+)
   1.130 -apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
   1.131 - apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
   1.132 - apply (erule impE)
   1.133 -  apply (simp (no_asm_simp))
   1.134 - apply (erule exE)
   1.135 - apply (rule_tac x = t in exI)
   1.136 - apply (simp del: realpow_Suc fact_Suc)
   1.137 -apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
   1.138 - prefer 2
   1.139 - apply clarify
   1.140 - apply simp
   1.141 - apply (frule less_iff_Suc_add [THEN iffD1], clarify)
   1.142 - apply (simp del: setsum_op_ivl_Suc)
   1.143 -apply (insert sumr_offset4 [of 1])
   1.144 -apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
   1.145 -apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
   1.146 -apply (rule allI, rule impI)
   1.147 -apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
   1.148 -apply (erule impE, assumption)
   1.149 -apply (erule exE)
   1.150 -apply (rule_tac x = t in exI)
   1.151 -(* do some tidying up *)
   1.152 -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.153 -       in thin_rl)
   1.154 -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.155 -       in thin_rl)
   1.156 -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.157 -       in thin_rl)
   1.158 -(* back to business *)
   1.159 -apply (simp (no_asm_simp))
   1.160 -apply (rule DERIV_unique)
   1.161 -prefer 2 apply blast
   1.162 -apply force
   1.163 -apply (rule allI, induct_tac "ma")
   1.164 -apply (rule impI, rule Rolle, assumption, simp, simp)
   1.165 -apply (metis DERIV_isCont zero_less_Suc)
   1.166 -apply (metis One_nat_def differentiableI dlo_simps(7))
   1.167 -apply safe
   1.168 -apply force
   1.169 -apply (frule Maclaurin_lemma3, assumption+, safe)
   1.170 -apply (rule_tac x = ta in exI, force)
   1.171 -done
   1.172 +proof -
   1.173 +  from n obtain m where m: "n = Suc m"
   1.174 +    by (cases n, simp add: n)
   1.175 +
   1.176 +  obtain B where f_h: "f h =
   1.177 +        (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
   1.178 +        B * (h ^ n / real (fact n))"
   1.179 +    using Maclaurin_lemma [OF h] ..
   1.180 +
   1.181 +  obtain g where g_def: "g = (%t. f t -
   1.182 +    (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}
   1.183 +      + (B * (t^n / real(fact n)))))" by blast
   1.184 +
   1.185 +  have g2: "g 0 = 0 & g h = 0"
   1.186 +    apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
   1.187 +    apply (cut_tac n = m and k = 1 in sumr_offset2)
   1.188 +    apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
   1.189 +    done
   1.190 +
   1.191 +  obtain difg where difg_def: "difg = (%m t. diff m t -
   1.192 +    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
   1.193 +      + (B * ((t ^ (n - m)) / real (fact (n - m))))))" by blast
   1.194 +
   1.195 +  have difg_0: "difg 0 = g"
   1.196 +    unfolding difg_def g_def by (simp add: diff_0)
   1.197 +
   1.198 +  have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real.
   1.199 +        m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
   1.200 +    using diff_Suc m difg_def by (rule Maclaurin_lemma2)
   1.201 +
   1.202 +  have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
   1.203 +    apply clarify
   1.204 +    apply (simp add: m difg_def)
   1.205 +    apply (frule less_iff_Suc_add [THEN iffD1], clarify)
   1.206 +    apply (simp del: setsum_op_ivl_Suc)
   1.207 +    apply (insert sumr_offset4 [of 1])
   1.208 +    apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
   1.209 +    done
   1.210 +
   1.211 +  have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
   1.212 +    by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
   1.213 +
   1.214 +  have differentiable_difg:
   1.215 +    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
   1.216 +    by (rule differentiableI [OF difg_Suc [rule_format]]) simp
   1.217 +
   1.218 +  have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
   1.219 +        \<Longrightarrow> difg (Suc m) t = 0"
   1.220 +    by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
   1.221 +
   1.222 +  have "m < n" using m by simp
   1.223 +
   1.224 +  have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
   1.225 +  using `m < n`
   1.226 +  proof (induct m)
   1.227 +  case 0
   1.228 +    show ?case
   1.229 +    proof (rule Rolle)
   1.230 +      show "0 < h" by fact
   1.231 +      show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
   1.232 +      show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
   1.233 +        by (simp add: isCont_difg n)
   1.234 +      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
   1.235 +        by (simp add: differentiable_difg n)
   1.236 +    qed
   1.237 +  next
   1.238 +  case (Suc m')
   1.239 +    hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
   1.240 +    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
   1.241 +    have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
   1.242 +    proof (rule Rolle)
   1.243 +      show "0 < t" by fact
   1.244 +      show "difg (Suc m') 0 = difg (Suc m') t"
   1.245 +        using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
   1.246 +      show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
   1.247 +        using `t < h` `Suc m' < n` by (simp add: isCont_difg)
   1.248 +      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
   1.249 +        using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
   1.250 +    qed
   1.251 +    thus ?case
   1.252 +      using `t < h` by auto
   1.253 +  qed
   1.254 +
   1.255 +  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
   1.256 +
   1.257 +  hence "difg (Suc m) t = 0"
   1.258 +    using `m < n` by (simp add: difg_Suc_eq_0)
   1.259 +
   1.260 +  show ?thesis
   1.261 +  proof (intro exI conjI)
   1.262 +    show "0 < t" by fact
   1.263 +    show "t < h" by fact
   1.264 +    show "f h =
   1.265 +      (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.266 +      diff n t / real (fact n) * h ^ n"
   1.267 +      using `difg (Suc m) t = 0`
   1.268 +      by (simp add: m f_h difg_def del: realpow_Suc fact_Suc)
   1.269 +  qed
   1.270 +
   1.271 +qed
   1.272  
   1.273  lemma Maclaurin_objl:
   1.274    "0 < h & n>0 & diff 0 = f &