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