src/HOL/Deriv.thy
changeset 31017 2c227493ea56
parent 30273 ecd6f0ca62ea
child 31336 e17f13cd1280
--- a/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title       : Deriv.thy
-    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -197,7 +196,7 @@
 done
 
 lemma DERIV_power_Suc:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
 proof (induct n)
@@ -211,7 +210,7 @@
 qed
 
 lemma DERIV_power:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
@@ -287,20 +286,20 @@
 text{*Power of -1*}
 
 lemma DERIV_inverse:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
 by (drule DERIV_inverse' [OF DERIV_ident]) simp
 
 text{*Derivative of inverse*}
 lemma DERIV_inverse_fun:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
 
 text{*Derivative of quotient*}
 lemma DERIV_quotient:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
 by (drule (2) DERIV_divide) (simp add: mult_commute)
@@ -404,7 +403,7 @@
   unfolding divide_inverse using prems by simp
 
 lemma differentiable_power [simp]:
-  fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
+  fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
   assumes "f differentiable x"
   shows "(\<lambda>x. f x ^ n) differentiable x"
   by (induct n, simp, simp add: prems)