equal
deleted
inserted
replaced
138 |
138 |
139 lemma CDERIV_pow [simp]: |
139 lemma CDERIV_pow [simp]: |
140 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
140 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
141 apply (induct n) |
141 apply (induct n) |
142 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
142 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
143 apply (auto simp add: distrib_right real_of_nat_Suc) |
143 apply (auto simp add: distrib_right of_nat_Suc) |
144 apply (case_tac "n") |
144 apply (case_tac "n") |
145 apply (auto simp add: ac_simps add.commute) |
145 apply (auto simp add: ac_simps) |
146 done |
146 done |
147 |
147 |
148 text{*Nonstandard version*} |
148 text{*Nonstandard version*} |
149 lemma NSCDERIV_pow: |
149 lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
150 "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
150 by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def) |
151 by (simp add: NSDERIV_DERIV_iff del: of_real_real_of_nat_eq) |
|
152 |
151 |
153 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
152 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
154 lemma NSCDERIV_inverse: |
153 lemma NSCDERIV_inverse: |
155 "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
154 "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
156 unfolding numeral_2_eq_2 |
155 unfolding numeral_2_eq_2 |