src/HOL/Deriv.thy
changeset 31017 2c227493ea56
parent 30273 ecd6f0ca62ea
child 31336 e17f13cd1280
     1.1 --- a/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title       : Deriv.thy
     1.5 -    ID          : $Id$
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 1998  University of Cambridge
     1.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.9 @@ -197,7 +196,7 @@
    1.10  done
    1.11  
    1.12  lemma DERIV_power_Suc:
    1.13 -  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
    1.14 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
    1.15    assumes f: "DERIV f x :> D"
    1.16    shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
    1.17  proof (induct n)
    1.18 @@ -211,7 +210,7 @@
    1.19  qed
    1.20  
    1.21  lemma DERIV_power:
    1.22 -  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
    1.23 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
    1.24    assumes f: "DERIV f x :> D"
    1.25    shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
    1.26  by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
    1.27 @@ -287,20 +286,20 @@
    1.28  text{*Power of -1*}
    1.29  
    1.30  lemma DERIV_inverse:
    1.31 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.32 +  fixes x :: "'a::{real_normed_field}"
    1.33    shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
    1.34  by (drule DERIV_inverse' [OF DERIV_ident]) simp
    1.35  
    1.36  text{*Derivative of inverse*}
    1.37  lemma DERIV_inverse_fun:
    1.38 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.39 +  fixes x :: "'a::{real_normed_field}"
    1.40    shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
    1.41        ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
    1.42  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
    1.43  
    1.44  text{*Derivative of quotient*}
    1.45  lemma DERIV_quotient:
    1.46 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.47 +  fixes x :: "'a::{real_normed_field}"
    1.48    shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
    1.49         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
    1.50  by (drule (2) DERIV_divide) (simp add: mult_commute)
    1.51 @@ -404,7 +403,7 @@
    1.52    unfolding divide_inverse using prems by simp
    1.53  
    1.54  lemma differentiable_power [simp]:
    1.55 -  fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
    1.56 +  fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
    1.57    assumes "f differentiable x"
    1.58    shows "(\<lambda>x. f x ^ n) differentiable x"
    1.59    by (induct n, simp, simp add: prems)