src/HOL/Hyperreal/Deriv.thy
changeset 21810 b2d23672b003
parent 21785 885667874dfc
child 22613 2f119f54d150
equal deleted inserted replaced
21809:4b93e949ac33 21810:b2d23672b003
   481             simp add: left_distrib right_distrib mult_commute add_assoc)
   481             simp add: left_distrib right_distrib mult_commute add_assoc)
   482 apply (rule_tac b1 = "star_of Db * star_of (f x)"
   482 apply (rule_tac b1 = "star_of Db * star_of (f x)"
   483          in add_commute [THEN subst])
   483          in add_commute [THEN subst])
   484 apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
   484 apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
   485                     Infinitesimal_add Infinitesimal_mult
   485                     Infinitesimal_add Infinitesimal_mult
   486                     Infinitesimal_hypreal_of_real_mult
   486                     Infinitesimal_star_of_mult
   487                     Infinitesimal_hypreal_of_real_mult2
   487                     Infinitesimal_star_of_mult2
   488           simp add: add_assoc [symmetric])
   488           simp add: add_assoc [symmetric])
   489 done
   489 done
   490 
   490 
   491 text{*Multiplying by a constant*}
   491 text{*Multiplying by a constant*}
   492 lemma NSDERIV_cmult: "NSDERIV f x :> D
   492 lemma NSDERIV_cmult: "NSDERIV f x :> D
   534                xa \<in> Infinitesimal;
   534                xa \<in> Infinitesimal;
   535                xa \<noteq> 0
   535                xa \<noteq> 0
   536             |] ==> D = 0"
   536             |] ==> D = 0"
   537 apply (simp add: nsderiv_def)
   537 apply (simp add: nsderiv_def)
   538 apply (drule bspec, auto)
   538 apply (drule bspec, auto)
   539 apply (rule star_of_approx_iff [THEN iffD1], simp)
       
   540 done
   539 done
   541 
   540 
   542 (* can be proved differently using NSLIM_isCont_iff *)
   541 (* can be proved differently using NSLIM_isCont_iff *)
   543 lemma NSDERIV_approx:
   542 lemma NSDERIV_approx:
   544      "[| NSDERIV f x :> D;  h \<in> Infinitesimal;  h \<noteq> 0 |]
   543      "[| NSDERIV f x :> D;  h \<in> Infinitesimal;  h \<noteq> 0 |]