src/HOL/Deriv.thy
changeset 30273 ecd6f0ca62ea
parent 30242 aea5d7fa7ef5
child 31017 2c227493ea56
equal deleted 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).