258 by (rule isCont_LIM_compose) |
258 by (rule isCont_LIM_compose) |
259 hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x))) |
259 hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x))) |
260 -- x --> d (f x) * D" |
260 -- x --> d (f x) * D" |
261 by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) |
261 by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) |
262 thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" |
262 thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" |
263 by (simp add: d dfx real_scaleR_def) |
263 by (simp add: d dfx) |
264 qed |
264 qed |
265 |
265 |
266 text {* |
266 text {* |
267 Let's do the standard proof, though theorem |
267 Let's do the standard proof, though theorem |
268 @{text "LIM_mult2"} follows from a NS proof |
268 @{text "LIM_mult2"} follows from a NS proof |
277 apply (erule DERIV_cmult) |
277 apply (erule DERIV_cmult) |
278 done |
278 done |
279 |
279 |
280 text {* Standard version *} |
280 text {* Standard version *} |
281 lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" |
281 lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" |
282 by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute) |
282 by (drule (1) DERIV_chain', simp add: o_def mult_commute) |
283 |
283 |
284 lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db" |
284 lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db" |
285 by (auto dest: DERIV_chain simp add: o_def) |
285 by (auto dest: DERIV_chain simp add: o_def) |
286 |
286 |
287 text {* Derivative of linear multiplication *} |
287 text {* Derivative of linear multiplication *} |
288 lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" |
288 lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" |
289 by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) |
289 by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) |
290 |
290 |
291 lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" |
291 lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" |
292 apply (cut_tac DERIV_power [OF DERIV_ident]) |
292 apply (cut_tac DERIV_power [OF DERIV_ident]) |
293 apply (simp add: real_scaleR_def real_of_nat_def) |
293 apply (simp add: real_of_nat_def) |
294 done |
294 done |
295 |
295 |
296 text {* Power of @{text "-1"} *} |
296 text {* Power of @{text "-1"} *} |
297 |
297 |
298 lemma DERIV_inverse: |
298 lemma DERIV_inverse: |
1530 by (fastsimp intro: isCont_diff) |
1530 by (fastsimp intro: isCont_diff) |
1531 qed |
1531 qed |
1532 moreover |
1532 moreover |
1533 have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x" |
1533 have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x" |
1534 proof - |
1534 proof - |
1535 have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const) |
1535 have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp |
1536 with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult) |
1536 with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp |
1537 moreover |
1537 moreover |
1538 have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const) |
1538 have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp |
1539 with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult) |
1539 with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp |
1540 ultimately show ?thesis by (simp add: differentiable_diff) |
1540 ultimately show ?thesis by simp |
1541 qed |
1541 qed |
1542 ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT) |
1542 ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT) |
1543 then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" .. |
1543 then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" .. |
1544 then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" .. |
1544 then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" .. |
1545 |
1545 |