src/HOL/Deriv.thy
changeset 30273 ecd6f0ca62ea
parent 30242 aea5d7fa7ef5
child 31017 2c227493ea56
     1.1 --- a/src/HOL/Deriv.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -202,7 +202,7 @@
     1.4    shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
     1.5  proof (induct n)
     1.6  case 0
     1.7 -  show ?case by (simp add: power_Suc f)
     1.8 +  show ?case by (simp add: f)
     1.9  case (Suc k)
    1.10    from DERIV_mult' [OF f Suc] show ?case
    1.11      apply (simp only: of_nat_Suc ring_distribs mult_1_left)
    1.12 @@ -214,7 +214,7 @@
    1.13    fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
    1.14    assumes f: "DERIV f x :> D"
    1.15    shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
    1.16 -by (cases "n", simp, simp add: DERIV_power_Suc f)
    1.17 +by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
    1.18  
    1.19  
    1.20  text {* Caratheodory formulation of derivative at a point *}
    1.21 @@ -289,21 +289,21 @@
    1.22  lemma DERIV_inverse:
    1.23    fixes x :: "'a::{real_normed_field,recpower}"
    1.24    shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
    1.25 -by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc)
    1.26 +by (drule DERIV_inverse' [OF DERIV_ident]) simp
    1.27  
    1.28  text{*Derivative of inverse*}
    1.29  lemma DERIV_inverse_fun:
    1.30    fixes x :: "'a::{real_normed_field,recpower}"
    1.31    shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
    1.32        ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
    1.33 -by (drule (1) DERIV_inverse') (simp add: mult_ac power_Suc nonzero_inverse_mult_distrib)
    1.34 +by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
    1.35  
    1.36  text{*Derivative of quotient*}
    1.37  lemma DERIV_quotient:
    1.38    fixes x :: "'a::{real_normed_field,recpower}"
    1.39    shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
    1.40         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
    1.41 -by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
    1.42 +by (drule (2) DERIV_divide) (simp add: mult_commute)
    1.43  
    1.44  lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.45  by auto
    1.46 @@ -407,7 +407,7 @@
    1.47    fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
    1.48    assumes "f differentiable x"
    1.49    shows "(\<lambda>x. f x ^ n) differentiable x"
    1.50 -  by (induct n, simp, simp add: power_Suc prems)
    1.51 +  by (induct n, simp, simp add: prems)
    1.52  
    1.53  
    1.54  subsection {* Nested Intervals and Bisection *}