1 (* Title : Deriv.thy |
|
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
|
4 Copyright : 1998 University of Cambridge |
|
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
|
6 *) |
|
7 |
|
8 header{* Differentiation (Nonstandard) *} |
|
9 |
|
10 theory HDeriv |
|
11 imports Deriv HLim |
|
12 begin |
|
13 |
|
14 text{*Nonstandard Definitions*} |
|
15 |
|
16 definition |
|
17 nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" |
|
18 ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where |
|
19 "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}. |
|
20 (( *f* f)(star_of x + h) |
|
21 - star_of (f x))/h @= star_of D)" |
|
22 |
|
23 definition |
|
24 NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" |
|
25 (infixl "NSdifferentiable" 60) where |
|
26 "f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)" |
|
27 |
|
28 definition |
|
29 increment :: "[real=>real,real,hypreal] => hypreal" where |
|
30 [code func del]: "increment f x h = (@inc. f NSdifferentiable x & |
|
31 inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))" |
|
32 |
|
33 |
|
34 subsection {* Derivatives *} |
|
35 |
|
36 lemma DERIV_NS_iff: |
|
37 "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)" |
|
38 by (simp add: deriv_def LIM_NSLIM_iff) |
|
39 |
|
40 lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D" |
|
41 by (simp add: deriv_def LIM_NSLIM_iff) |
|
42 |
|
43 lemma hnorm_of_hypreal: |
|
44 "\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>" |
|
45 by transfer (rule norm_of_real) |
|
46 |
|
47 lemma Infinitesimal_of_hypreal: |
|
48 "x \<in> Infinitesimal \<Longrightarrow> |
|
49 (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal" |
|
50 apply (rule InfinitesimalI2) |
|
51 apply (drule (1) InfinitesimalD2) |
|
52 apply (simp add: hnorm_of_hypreal) |
|
53 done |
|
54 |
|
55 lemma of_hypreal_eq_0_iff: |
|
56 "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)" |
|
57 by transfer (rule of_real_eq_0_iff) |
|
58 |
|
59 lemma NSDeriv_unique: |
|
60 "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E" |
|
61 apply (subgoal_tac "( *f* of_real) epsilon \<in> Infinitesimal - {0::'a star}") |
|
62 apply (simp only: nsderiv_def) |
|
63 apply (drule (1) bspec)+ |
|
64 apply (drule (1) approx_trans3) |
|
65 apply simp |
|
66 apply (simp add: Infinitesimal_of_hypreal Infinitesimal_epsilon) |
|
67 apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero) |
|
68 done |
|
69 |
|
70 text {*First NSDERIV in terms of NSLIM*} |
|
71 |
|
72 text{*first equivalence *} |
|
73 lemma NSDERIV_NSLIM_iff: |
|
74 "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)" |
|
75 apply (simp add: nsderiv_def NSLIM_def, auto) |
|
76 apply (drule_tac x = xa in bspec) |
|
77 apply (rule_tac [3] ccontr) |
|
78 apply (drule_tac [3] x = h in spec) |
|
79 apply (auto simp add: mem_infmal_iff starfun_lambda_cancel) |
|
80 done |
|
81 |
|
82 text{*second equivalence *} |
|
83 lemma NSDERIV_NSLIM_iff2: |
|
84 "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)" |
|
85 by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff diff_minus [symmetric] |
|
86 LIM_NSLIM_iff [symmetric]) |
|
87 |
|
88 (* while we're at it! *) |
|
89 |
|
90 lemma NSDERIV_iff2: |
|
91 "(NSDERIV f x :> D) = |
|
92 (\<forall>w. |
|
93 w \<noteq> star_of x & w \<approx> star_of x --> |
|
94 ( *f* (%z. (f z - f x) / (z-x))) w \<approx> star_of D)" |
|
95 by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) |
|
96 |
|
97 (*FIXME DELETE*) |
|
98 lemma hypreal_not_eq_minus_iff: |
|
99 "(x \<noteq> a) = (x - a \<noteq> (0::'a::ab_group_add))" |
|
100 by auto |
|
101 |
|
102 lemma NSDERIVD5: |
|
103 "(NSDERIV f x :> D) ==> |
|
104 (\<forall>u. u \<approx> hypreal_of_real x --> |
|
105 ( *f* (%z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))" |
|
106 apply (auto simp add: NSDERIV_iff2) |
|
107 apply (case_tac "u = hypreal_of_real x", auto) |
|
108 apply (drule_tac x = u in spec, auto) |
|
109 apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1) |
|
110 apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1]) |
|
111 apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ") |
|
112 apply (auto simp add: |
|
113 approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] |
|
114 Infinitesimal_subset_HFinite [THEN subsetD]) |
|
115 done |
|
116 |
|
117 lemma NSDERIVD4: |
|
118 "(NSDERIV f x :> D) ==> |
|
119 (\<forall>h \<in> Infinitesimal. |
|
120 (( *f* f)(hypreal_of_real x + h) - |
|
121 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" |
|
122 apply (auto simp add: nsderiv_def) |
|
123 apply (case_tac "h = (0::hypreal) ") |
|
124 apply (auto simp add: diff_minus) |
|
125 apply (drule_tac x = h in bspec) |
|
126 apply (drule_tac [2] c = h in approx_mult1) |
|
127 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
128 simp add: diff_minus) |
|
129 done |
|
130 |
|
131 lemma NSDERIVD3: |
|
132 "(NSDERIV f x :> D) ==> |
|
133 (\<forall>h \<in> Infinitesimal - {0}. |
|
134 (( *f* f)(hypreal_of_real x + h) - |
|
135 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" |
|
136 apply (auto simp add: nsderiv_def) |
|
137 apply (rule ccontr, drule_tac x = h in bspec) |
|
138 apply (drule_tac [2] c = h in approx_mult1) |
|
139 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
140 simp add: mult_assoc diff_minus) |
|
141 done |
|
142 |
|
143 text{*Differentiability implies continuity |
|
144 nice and simple "algebraic" proof*} |
|
145 lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x" |
|
146 apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def) |
|
147 apply (drule approx_minus_iff [THEN iffD1]) |
|
148 apply (drule hypreal_not_eq_minus_iff [THEN iffD1]) |
|
149 apply (drule_tac x = "xa - star_of x" in bspec) |
|
150 prefer 2 apply (simp add: add_assoc [symmetric]) |
|
151 apply (auto simp add: mem_infmal_iff [symmetric] add_commute) |
|
152 apply (drule_tac c = "xa - star_of x" in approx_mult1) |
|
153 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
154 simp add: mult_assoc nonzero_mult_divide_cancel_right) |
|
155 apply (drule_tac x3=D in |
|
156 HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, |
|
157 THEN mem_infmal_iff [THEN iffD1]]) |
|
158 apply (auto simp add: mult_commute |
|
159 intro: approx_trans approx_minus_iff [THEN iffD2]) |
|
160 done |
|
161 |
|
162 text{*Differentiation rules for combinations of functions |
|
163 follow from clear, straightforard, algebraic |
|
164 manipulations*} |
|
165 text{*Constant function*} |
|
166 |
|
167 (* use simple constant nslimit theorem *) |
|
168 lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)" |
|
169 by (simp add: NSDERIV_NSLIM_iff) |
|
170 |
|
171 text{*Sum of functions- proved easily*} |
|
172 |
|
173 lemma NSDERIV_add: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] |
|
174 ==> NSDERIV (%x. f x + g x) x :> Da + Db" |
|
175 apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) |
|
176 apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec) |
|
177 apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add) |
|
178 apply (auto simp add: diff_def add_ac) |
|
179 done |
|
180 |
|
181 text{*Product of functions - Proof is trivial but tedious |
|
182 and long due to rearrangement of terms*} |
|
183 |
|
184 lemma lemma_nsderiv1: |
|
185 fixes a b c d :: "'a::comm_ring star" |
|
186 shows "(a*b) - (c*d) = (b*(a - c)) + (c*(b - d))" |
|
187 by (simp add: right_diff_distrib mult_ac) |
|
188 |
|
189 lemma lemma_nsderiv2: |
|
190 fixes x y z :: "'a::real_normed_field star" |
|
191 shows "[| (x - y) / z = star_of D + yb; z \<noteq> 0; |
|
192 z \<in> Infinitesimal; yb \<in> Infinitesimal |] |
|
193 ==> x - y \<approx> 0" |
|
194 apply (simp add: nonzero_divide_eq_eq) |
|
195 apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add |
|
196 simp add: mult_assoc mem_infmal_iff [symmetric]) |
|
197 apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) |
|
198 done |
|
199 |
|
200 lemma NSDERIV_mult: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] |
|
201 ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" |
|
202 apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) |
|
203 apply (auto dest!: spec |
|
204 simp add: starfun_lambda_cancel lemma_nsderiv1) |
|
205 apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib) |
|
206 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ |
|
207 apply (auto simp add: times_divide_eq_right [symmetric] |
|
208 simp del: times_divide_eq) |
|
209 apply (drule_tac D = Db in lemma_nsderiv2, assumption+) |
|
210 apply (drule_tac |
|
211 approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) |
|
212 apply (auto intro!: approx_add_mono1 |
|
213 simp add: left_distrib right_distrib mult_commute add_assoc) |
|
214 apply (rule_tac b1 = "star_of Db * star_of (f x)" |
|
215 in add_commute [THEN subst]) |
|
216 apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] |
|
217 Infinitesimal_add Infinitesimal_mult |
|
218 Infinitesimal_star_of_mult |
|
219 Infinitesimal_star_of_mult2 |
|
220 simp add: add_assoc [symmetric]) |
|
221 done |
|
222 |
|
223 text{*Multiplying by a constant*} |
|
224 lemma NSDERIV_cmult: "NSDERIV f x :> D |
|
225 ==> NSDERIV (%x. c * f x) x :> c*D" |
|
226 apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff |
|
227 minus_mult_right right_diff_distrib [symmetric]) |
|
228 apply (erule NSLIM_const [THEN NSLIM_mult]) |
|
229 done |
|
230 |
|
231 text{*Negation of function*} |
|
232 lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D" |
|
233 proof (simp add: NSDERIV_NSLIM_iff) |
|
234 assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D" |
|
235 hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D" |
|
236 by (rule NSLIM_minus) |
|
237 have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h" |
|
238 by (simp add: minus_divide_left diff_def) |
|
239 with deriv |
|
240 show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp |
|
241 qed |
|
242 |
|
243 text{*Subtraction*} |
|
244 lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db" |
|
245 by (blast dest: NSDERIV_add NSDERIV_minus) |
|
246 |
|
247 lemma NSDERIV_diff: |
|
248 "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] |
|
249 ==> NSDERIV (%x. f x - g x) x :> Da-Db" |
|
250 apply (simp add: diff_minus) |
|
251 apply (blast intro: NSDERIV_add_minus) |
|
252 done |
|
253 |
|
254 text{* Similarly to the above, the chain rule admits an entirely |
|
255 straightforward derivation. Compare this with Harrison's |
|
256 HOL proof of the chain rule, which proved to be trickier and |
|
257 required an alternative characterisation of differentiability- |
|
258 the so-called Carathedory derivative. Our main problem is |
|
259 manipulation of terms.*} |
|
260 |
|
261 (* lemmas *) |
|
262 |
|
263 lemma NSDERIV_zero: |
|
264 "[| NSDERIV g x :> D; |
|
265 ( *f* g) (star_of x + xa) = star_of (g x); |
|
266 xa \<in> Infinitesimal; |
|
267 xa \<noteq> 0 |
|
268 |] ==> D = 0" |
|
269 apply (simp add: nsderiv_def) |
|
270 apply (drule bspec, auto) |
|
271 done |
|
272 |
|
273 (* can be proved differently using NSLIM_isCont_iff *) |
|
274 lemma NSDERIV_approx: |
|
275 "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |] |
|
276 ==> ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0" |
|
277 apply (simp add: nsderiv_def) |
|
278 apply (simp add: mem_infmal_iff [symmetric]) |
|
279 apply (rule Infinitesimal_ratio) |
|
280 apply (rule_tac [3] approx_star_of_HFinite, auto) |
|
281 done |
|
282 |
|
283 (*--------------------------------------------------------------- |
|
284 from one version of differentiability |
|
285 |
|
286 f(x) - f(a) |
|
287 --------------- \<approx> Db |
|
288 x - a |
|
289 ---------------------------------------------------------------*) |
|
290 |
|
291 lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da; |
|
292 ( *f* g) (star_of(x) + xa) \<noteq> star_of (g x); |
|
293 ( *f* g) (star_of(x) + xa) \<approx> star_of (g x) |
|
294 |] ==> (( *f* f) (( *f* g) (star_of(x) + xa)) |
|
295 - star_of (f (g x))) |
|
296 / (( *f* g) (star_of(x) + xa) - star_of (g x)) |
|
297 \<approx> star_of(Da)" |
|
298 by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric]) |
|
299 |
|
300 (*-------------------------------------------------------------- |
|
301 from other version of differentiability |
|
302 |
|
303 f(x + h) - f(x) |
|
304 ----------------- \<approx> Db |
|
305 h |
|
306 --------------------------------------------------------------*) |
|
307 |
|
308 lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |] |
|
309 ==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa |
|
310 \<approx> star_of(Db)" |
|
311 by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) |
|
312 |
|
313 lemma lemma_chain: "(z::'a::real_normed_field star) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)" |
|
314 proof - |
|
315 assume z: "z \<noteq> 0" |
|
316 have "x * y = x * (inverse z * z) * y" by (simp add: z) |
|
317 thus ?thesis by (simp add: mult_assoc) |
|
318 qed |
|
319 |
|
320 text{*This proof uses both definitions of differentiability.*} |
|
321 lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] |
|
322 ==> NSDERIV (f o g) x :> Da * Db" |
|
323 apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def |
|
324 mem_infmal_iff [symmetric]) |
|
325 apply clarify |
|
326 apply (frule_tac f = g in NSDERIV_approx) |
|
327 apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric]) |
|
328 apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ") |
|
329 apply (drule_tac g = g in NSDERIV_zero) |
|
330 apply (auto simp add: divide_inverse) |
|
331 apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) |
|
332 apply (erule hypreal_not_eq_minus_iff [THEN iffD1]) |
|
333 apply (rule approx_mult_star_of) |
|
334 apply (simp_all add: divide_inverse [symmetric]) |
|
335 apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2]) |
|
336 apply (blast intro: NSDERIVD2) |
|
337 done |
|
338 |
|
339 text{*Differentiation of natural number powers*} |
|
340 lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1" |
|
341 by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if) |
|
342 |
|
343 lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c" |
|
344 by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp) |
|
345 |
|
346 (*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*) |
|
347 lemma NSDERIV_inverse: |
|
348 fixes x :: "'a::{real_normed_field,recpower}" |
|
349 shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))" |
|
350 apply (simp add: nsderiv_def) |
|
351 apply (rule ballI, simp, clarify) |
|
352 apply (frule (1) Infinitesimal_add_not_zero) |
|
353 apply (simp add: add_commute) |
|
354 (*apply (auto simp add: starfun_inverse_inverse realpow_two |
|
355 simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*) |
|
356 apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc |
|
357 nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_def |
|
358 del: inverse_mult_distrib inverse_minus_eq |
|
359 minus_mult_left [symmetric] minus_mult_right [symmetric]) |
|
360 apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right) |
|
361 apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib |
|
362 del: minus_mult_left [symmetric] minus_mult_right [symmetric]) |
|
363 apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans) |
|
364 apply (rule inverse_add_Infinitesimal_approx2) |
|
365 apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal |
|
366 simp add: inverse_minus_eq [symmetric] HFinite_minus_iff) |
|
367 apply (rule Infinitesimal_HFinite_mult, auto) |
|
368 done |
|
369 |
|
370 subsubsection {* Equivalence of NS and Standard definitions *} |
|
371 |
|
372 lemma divideR_eq_divide: "x /\<^sub>R y = x / y" |
|
373 by (simp add: real_scaleR_def divide_inverse mult_commute) |
|
374 |
|
375 text{*Now equivalence between NSDERIV and DERIV*} |
|
376 lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)" |
|
377 by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) |
|
378 |
|
379 (* NS version *) |
|
380 lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" |
|
381 by (simp add: NSDERIV_DERIV_iff DERIV_pow) |
|
382 |
|
383 text{*Derivative of inverse*} |
|
384 |
|
385 lemma NSDERIV_inverse_fun: |
|
386 fixes x :: "'a::{real_normed_field,recpower}" |
|
387 shows "[| NSDERIV f x :> d; f(x) \<noteq> 0 |] |
|
388 ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" |
|
389 by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc) |
|
390 |
|
391 text{*Derivative of quotient*} |
|
392 |
|
393 lemma NSDERIV_quotient: |
|
394 fixes x :: "'a::{real_normed_field,recpower}" |
|
395 shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |] |
|
396 ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) |
|
397 - (e*f(x))) / (g(x) ^ Suc (Suc 0))" |
|
398 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc) |
|
399 |
|
400 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==> |
|
401 \<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isNSCont g x & g x = l" |
|
402 by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV |
|
403 mult_commute) |
|
404 |
|
405 lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" |
|
406 by auto |
|
407 |
|
408 lemma CARAT_DERIVD: |
|
409 assumes all: "\<forall>z. f z - f x = g z * (z-x)" |
|
410 and nsc: "isNSCont g x" |
|
411 shows "NSDERIV f x :> g x" |
|
412 proof - |
|
413 from nsc |
|
414 have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> |
|
415 ( *f* g) w * (w - star_of x) / (w - star_of x) \<approx> |
|
416 star_of (g x)" |
|
417 by (simp add: isNSCont_def nonzero_mult_divide_cancel_right) |
|
418 thus ?thesis using all |
|
419 by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) |
|
420 qed |
|
421 |
|
422 subsubsection {* Differentiability predicate *} |
|
423 |
|
424 lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D" |
|
425 by (simp add: NSdifferentiable_def) |
|
426 |
|
427 lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x" |
|
428 by (force simp add: NSdifferentiable_def) |
|
429 |
|
430 |
|
431 subsection {*(NS) Increment*} |
|
432 lemma incrementI: |
|
433 "f NSdifferentiable x ==> |
|
434 increment f x h = ( *f* f) (hypreal_of_real(x) + h) - |
|
435 hypreal_of_real (f x)" |
|
436 by (simp add: increment_def) |
|
437 |
|
438 lemma incrementI2: "NSDERIV f x :> D ==> |
|
439 increment f x h = ( *f* f) (hypreal_of_real(x) + h) - |
|
440 hypreal_of_real (f x)" |
|
441 apply (erule NSdifferentiableI [THEN incrementI]) |
|
442 done |
|
443 |
|
444 (* The Increment theorem -- Keisler p. 65 *) |
|
445 lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |] |
|
446 ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h" |
|
447 apply (frule_tac h = h in incrementI2, simp add: nsderiv_def) |
|
448 apply (drule bspec, auto) |
|
449 apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) |
|
450 apply (frule_tac b1 = "hypreal_of_real (D) + y" |
|
451 in hypreal_mult_right_cancel [THEN iffD2]) |
|
452 apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) |
|
453 apply assumption |
|
454 apply (simp add: times_divide_eq_right [symmetric]) |
|
455 apply (auto simp add: left_distrib) |
|
456 done |
|
457 |
|
458 lemma increment_thm2: |
|
459 "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |] |
|
460 ==> \<exists>e \<in> Infinitesimal. increment f x h = |
|
461 hypreal_of_real(D)*h + e*h" |
|
462 by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm) |
|
463 |
|
464 |
|
465 lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |] |
|
466 ==> increment f x h \<approx> 0" |
|
467 apply (drule increment_thm2, |
|
468 auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric]) |
|
469 apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) |
|
470 done |
|
471 |
|
472 end |
|