27468
|
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
|
28562
|
30 |
[code del]: "increment f x h = (@inc. f NSdifferentiable x &
|
27468
|
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
|