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