src/HOL/Deriv.thy
 changeset 30273 ecd6f0ca62ea parent 30242 aea5d7fa7ef5 child 31017 2c227493ea56
equal inserted replaced
30268:5af6ed62385b 30273:ecd6f0ca62ea
`   200   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   200   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   201   assumes f: "DERIV f x :> D"`
`   201   assumes f: "DERIV f x :> D"`
`   202   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"`
`   202   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"`
`   203 proof (induct n)`
`   203 proof (induct n)`
`   204 case 0`
`   204 case 0`
`   205   show ?case by (simp add: power_Suc f)`
`   205   show ?case by (simp add: f)`
`   206 case (Suc k)`
`   206 case (Suc k)`
`   207   from DERIV_mult' [OF f Suc] show ?case`
`   207   from DERIV_mult' [OF f Suc] show ?case`
`   208     apply (simp only: of_nat_Suc ring_distribs mult_1_left)`
`   208     apply (simp only: of_nat_Suc ring_distribs mult_1_left)`
`   209     apply (simp only: power_Suc algebra_simps)`
`   209     apply (simp only: power_Suc algebra_simps)`
`   210     done`
`   210     done`
`   212 `
`   212 `
`   213 lemma DERIV_power:`
`   213 lemma DERIV_power:`
`   214   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   214   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"`
`   215   assumes f: "DERIV f x :> D"`
`   215   assumes f: "DERIV f x :> D"`
`   216   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"`
`   216   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)`
`   217 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)`
`   218 `
`   218 `
`   219 `
`   219 `
`   220 text {* Caratheodory formulation of derivative at a point *}`
`   220 text {* Caratheodory formulation of derivative at a point *}`
`   221 `
`   221 `
`   222 lemma CARAT_DERIV:`
`   222 lemma CARAT_DERIV:`
`   287 text{*Power of -1*}`
`   287 text{*Power of -1*}`
`   288 `
`   288 `
`   289 lemma DERIV_inverse:`
`   289 lemma DERIV_inverse:`
`   290   fixes x :: "'a::{real_normed_field,recpower}"`
`   290   fixes x :: "'a::{real_normed_field,recpower}"`
`   291   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"`
`   291   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"`
`   292 by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc)`
`   292 by (drule DERIV_inverse' [OF DERIV_ident]) simp`
`   293 `
`   293 `
`   294 text{*Derivative of inverse*}`
`   294 text{*Derivative of inverse*}`
`   295 lemma DERIV_inverse_fun:`
`   295 lemma DERIV_inverse_fun:`
`   296   fixes x :: "'a::{real_normed_field,recpower}"`
`   296   fixes x :: "'a::{real_normed_field,recpower}"`
`   297   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]`
`   297   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]`
`   298       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"`
`   298       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"`
`   299 by (drule (1) DERIV_inverse') (simp add: mult_ac power_Suc nonzero_inverse_mult_distrib)`
`   299 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)`
`   300 `
`   300 `
`   301 text{*Derivative of quotient*}`
`   301 text{*Derivative of quotient*}`
`   302 lemma DERIV_quotient:`
`   302 lemma DERIV_quotient:`
`   303   fixes x :: "'a::{real_normed_field,recpower}"`
`   303   fixes x :: "'a::{real_normed_field,recpower}"`
`   304   shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]`
`   304   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))"`
`   305        ==> 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 power_Suc)`
`   306 by (drule (2) DERIV_divide) (simp add: mult_commute)`
`   307 `
`   307 `
`   308 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"`
`   308 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"`
`   309 by auto`
`   309 by auto`
`   310 `
`   310 `
`   311 `
`   311 `
`   405 `
`   405 `
`   406 lemma differentiable_power [simp]:`
`   406 lemma differentiable_power [simp]:`
`   407   fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"`
`   407   fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"`
`   408   assumes "f differentiable x"`
`   408   assumes "f differentiable x"`
`   409   shows "(\<lambda>x. f x ^ n) differentiable x"`
`   409   shows "(\<lambda>x. f x ^ n) differentiable x"`
`   410   by (induct n, simp, simp add: power_Suc prems)`
`   410   by (induct n, simp, simp add: prems)`
`   411 `
`   411 `
`   412 `
`   412 `
`   413 subsection {* Nested Intervals and Bisection *}`
`   413 subsection {* Nested Intervals and Bisection *}`
`   414 `
`   414 `
`   415 text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).`
`   415 text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).`