56 apply (simp add: fact_diff_Suc) |
56 apply (simp add: fact_diff_Suc) |
57 prefer 2 apply simp |
57 prefer 2 apply simp |
58 apply (frule less_iff_Suc_add [THEN iffD1], clarify) |
58 apply (frule less_iff_Suc_add [THEN iffD1], clarify) |
59 apply (simp del: setsum_op_ivl_Suc) |
59 apply (simp del: setsum_op_ivl_Suc) |
60 apply (insert sumr_offset4 [of "Suc 0"]) |
60 apply (insert sumr_offset4 [of "Suc 0"]) |
61 apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc) |
61 apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc) |
62 apply (rule lemma_DERIV_subst) |
62 apply (rule lemma_DERIV_subst) |
63 apply (rule DERIV_add) |
63 apply (rule DERIV_add) |
64 apply (rule_tac [2] DERIV_const) |
64 apply (rule_tac [2] DERIV_const) |
65 apply (rule DERIV_sumr, clarify) |
65 apply (rule DERIV_sumr, clarify) |
66 prefer 2 apply simp |
66 prefer 2 apply simp |
67 apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc) |
67 apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc) |
68 apply (rule DERIV_cmult) |
68 apply (rule DERIV_cmult) |
69 apply (rule lemma_DERIV_subst) |
69 apply (rule lemma_DERIV_subst) |
70 apply (best intro!: DERIV_intros) |
70 apply (best intro!: DERIV_intros) |
71 apply (subst fact_Suc_nat) |
71 apply (subst fact_Suc) |
72 apply (subst real_of_nat_mult) |
72 apply (subst real_of_nat_mult) |
73 apply (simp add: mult_ac) |
73 apply (simp add: mult_ac) |
74 done |
74 done |
75 |
75 |
76 lemma Maclaurin: |
76 lemma Maclaurin: |
118 apply clarify |
118 apply clarify |
119 apply (simp add: m difg_def) |
119 apply (simp add: m difg_def) |
120 apply (frule less_iff_Suc_add [THEN iffD1], clarify) |
120 apply (frule less_iff_Suc_add [THEN iffD1], clarify) |
121 apply (simp del: setsum_op_ivl_Suc) |
121 apply (simp del: setsum_op_ivl_Suc) |
122 apply (insert sumr_offset4 [of "Suc 0"]) |
122 apply (insert sumr_offset4 [of "Suc 0"]) |
123 apply (simp del: setsum_op_ivl_Suc fact_Suc_nat) |
123 apply (simp del: setsum_op_ivl_Suc fact_Suc) |
124 done |
124 done |
125 |
125 |
126 have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" |
126 have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" |
127 by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp |
127 by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp |
128 |
128 |
178 show "t < h" by fact |
178 show "t < h" by fact |
179 show "f h = |
179 show "f h = |
180 (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + |
180 (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + |
181 diff n t / real (fact n) * h ^ n" |
181 diff n t / real (fact n) * h ^ n" |
182 using `difg (Suc m) t = 0` |
182 using `difg (Suc m) t = 0` |
183 by (simp add: m f_h difg_def del: fact_Suc_nat) |
183 by (simp add: m f_h difg_def del: fact_Suc) |
184 qed |
184 qed |
185 |
185 |
186 qed |
186 qed |
187 |
187 |
188 lemma Maclaurin_objl: |
188 lemma Maclaurin_objl: |