src/HOL/Hyperreal/Deriv.thy
changeset 21785 885667874dfc
parent 21784 e76faa6e65fd
child 21810 b2d23672b003
equal deleted inserted replaced
21784:e76faa6e65fd 21785:885667874dfc
   697        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
   697        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
   698 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
   698 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
   699 
   699 
   700 lemma NSDERIV_quotient:
   700 lemma NSDERIV_quotient:
   701   fixes x :: "'a::{real_normed_field,recpower}"
   701   fixes x :: "'a::{real_normed_field,recpower}"
   702   shows "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
   702   shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
   703        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
   703        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
   704                             - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
   704                             - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
   705 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
   705 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
   706 
   706 
   707 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
   707 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>