src/HOL/Deriv.thy
 changeset 31017 2c227493ea56 parent 30273 ecd6f0ca62ea child 31336 e17f13cd1280
equal inserted replaced
31016:e1309df633c6 31017:2c227493ea56
`     1 (*  Title       : Deriv.thy`
`     1 (*  Title       : Deriv.thy`
`     3     Author      : Jacques D. Fleuriot`
`     2     Author      : Jacques D. Fleuriot`
`     4     Copyright   : 1998  University of Cambridge`
`     3     Copyright   : 1998  University of Cambridge`
`     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004`
`     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004`
`     6     GMVT by Benjamin Porter, 2005`
`     5     GMVT by Benjamin Porter, 2005`
`     7 *)`
`     6 *)`
`   195 apply (simp add: ring_distribs nonzero_inverse_mult_distrib)`
`   194 apply (simp add: ring_distribs nonzero_inverse_mult_distrib)`
`   196 apply (simp add: mult_ac)`
`   195 apply (simp add: mult_ac)`
`   197 done`
`   196 done`
`   198 `
`   197 `
`   199 lemma DERIV_power_Suc:`
`   198 lemma DERIV_power_Suc:`
`   200   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   199   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"`
`   201   assumes f: "DERIV f x :> D"`
`   200   assumes f: "DERIV f x :> D"`
`   202   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"`
`   201   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"`
`   203 proof (induct n)`
`   202 proof (induct n)`
`   204 case 0`
`   203 case 0`
`   205   show ?case by (simp add: f)`
`   204   show ?case by (simp add: f)`
`   209     apply (simp only: power_Suc algebra_simps)`
`   208     apply (simp only: power_Suc algebra_simps)`
`   210     done`
`   209     done`
`   211 qed`
`   210 qed`
`   212 `
`   211 `
`   213 lemma DERIV_power:`
`   212 lemma DERIV_power:`
`   214   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   213   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"`
`   215   assumes f: "DERIV f x :> D"`
`   214   assumes f: "DERIV f x :> D"`
`   216   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"`
`   215   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"`
`   217 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)`
`   216 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)`
`   218 `
`   217 `
`   219 `
`   218 `
`   285 done`
`   284 done`
`   286 `
`   285 `
`   287 text{*Power of -1*}`
`   286 text{*Power of -1*}`
`   288 `
`   287 `
`   289 lemma DERIV_inverse:`
`   288 lemma DERIV_inverse:`
`   290   fixes x :: "'a::{real_normed_field,recpower}"`
`   289   fixes x :: "'a::{real_normed_field}"`
`   291   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"`
`   290   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"`
`   292 by (drule DERIV_inverse' [OF DERIV_ident]) simp`
`   291 by (drule DERIV_inverse' [OF DERIV_ident]) simp`
`   293 `
`   292 `
`   294 text{*Derivative of inverse*}`
`   293 text{*Derivative of inverse*}`
`   295 lemma DERIV_inverse_fun:`
`   294 lemma DERIV_inverse_fun:`
`   296   fixes x :: "'a::{real_normed_field,recpower}"`
`   295   fixes x :: "'a::{real_normed_field}"`
`   297   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]`
`   296   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]`
`   298       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"`
`   297       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"`
`   299 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)`
`   298 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)`
`   300 `
`   299 `
`   301 text{*Derivative of quotient*}`
`   300 text{*Derivative of quotient*}`
`   302 lemma DERIV_quotient:`
`   301 lemma DERIV_quotient:`
`   303   fixes x :: "'a::{real_normed_field,recpower}"`
`   302   fixes x :: "'a::{real_normed_field}"`
`   304   shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]`
`   303   shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]`
`   305        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"`
`   304        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"`
`   306 by (drule (2) DERIV_divide) (simp add: mult_commute)`
`   305 by (drule (2) DERIV_divide) (simp add: mult_commute)`
`   307 `
`   306 `
`   308 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"`
`   307 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"`
`   402   assumes "g differentiable x" and "g x \<noteq> 0"`
`   401   assumes "g differentiable x" and "g x \<noteq> 0"`
`   403   shows "(\<lambda>x. f x / g x) differentiable x"`
`   402   shows "(\<lambda>x. f x / g x) differentiable x"`
`   404   unfolding divide_inverse using prems by simp`
`   403   unfolding divide_inverse using prems by simp`
`   405 `
`   404 `
`   406 lemma differentiable_power [simp]:`
`   405 lemma differentiable_power [simp]:`
`   407   fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"`
`   406   fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"`
`   408   assumes "f differentiable x"`
`   407   assumes "f differentiable x"`
`   409   shows "(\<lambda>x. f x ^ n) differentiable x"`
`   408   shows "(\<lambda>x. f x ^ n) differentiable x"`
`   410   by (induct n, simp, simp add: prems)`
`   409   by (induct n, simp, simp add: prems)`
`   411 `
`   410 `
`   412 `
`   411 `