149 *) |
128 *) |
150 |
129 |
151 |
130 |
152 subsection{*The Finite Elements form a Subring*} |
131 subsection{*The Finite Elements form a Subring*} |
153 |
132 |
154 lemma CFinite_add: "[|x \<in> CFinite; y \<in> CFinite|] ==> (x+y) \<in> CFinite" |
133 lemma SComplex_subset_HFinite [simp]: "SComplex \<le> HFinite" |
155 apply (simp add: CFinite_def) |
134 apply (auto simp add: SComplex_def HFinite_def) |
156 apply (blast intro!: SReal_add hcmod_add_less) |
|
157 done |
|
158 |
|
159 lemma CFinite_mult: "[|x \<in> CFinite; y \<in> CFinite|] ==> x*y \<in> CFinite" |
|
160 apply (simp add: CFinite_def) |
|
161 apply (blast intro!: SReal_mult hcmod_mult_less) |
|
162 done |
|
163 |
|
164 lemma CFinite_minus_iff [simp]: "(-x \<in> CFinite) = (x \<in> CFinite)" |
|
165 by (simp add: CFinite_def) |
|
166 |
|
167 lemma SComplex_subset_CFinite [simp]: "SComplex \<le> CFinite" |
|
168 apply (auto simp add: SComplex_def CFinite_def) |
|
169 apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI) |
135 apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI) |
170 apply (auto intro: SReal_add) |
136 apply (auto intro: SReal_add) |
171 done |
137 done |
172 |
138 |
173 lemma HFinite_hcmod_hcomplex_of_complex [simp]: |
139 lemma HFinite_hcmod_hcomplex_of_complex [simp]: |
174 "hcmod (hcomplex_of_complex r) \<in> HFinite" |
140 "hcmod (hcomplex_of_complex r) \<in> HFinite" |
175 by (auto intro!: SReal_subset_HFinite [THEN subsetD]) |
141 by (auto intro!: SReal_subset_HFinite [THEN subsetD]) |
176 |
142 |
177 lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> CFinite" |
143 lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \<in> HFinite" |
178 by (auto intro!: SComplex_subset_CFinite [THEN subsetD]) |
144 by (rule HFinite_star_of) |
179 |
145 |
180 lemma CFiniteD: "x \<in> CFinite ==> \<exists>t \<in> Reals. hcmod x < t" |
146 lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)" |
181 by (simp add: CFinite_def) |
147 by (simp add: HFinite_def) |
182 |
148 |
183 lemma CFinite_hcmod_iff: "(x \<in> CFinite) = (hcmod x \<in> HFinite)" |
149 lemma HFinite_bounded_hcmod: |
184 by (simp add: CFinite_def HFinite_def) |
150 "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite" |
185 |
151 by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff) |
186 lemma CFinite_number_of [simp]: "number_of w \<in> CFinite" |
|
187 by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]]) |
|
188 |
|
189 lemma CFinite_bounded: "[|x \<in> CFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite" |
|
190 by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff) |
|
191 |
152 |
192 |
153 |
193 subsection{*The Complex Infinitesimals form a Subring*} |
154 subsection{*The Complex Infinitesimals form a Subring*} |
194 |
|
195 lemma CInfinitesimal_zero [iff]: "0 \<in> CInfinitesimal" |
|
196 by (simp add: CInfinitesimal_def) |
|
197 |
155 |
198 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" |
156 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" |
199 by auto |
157 by auto |
200 |
158 |
201 lemma CInfinitesimal_hcmod_iff: |
159 lemma Infinitesimal_hcmod_iff: |
202 "(z \<in> CInfinitesimal) = (hcmod z \<in> Infinitesimal)" |
160 "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)" |
203 by (simp add: CInfinitesimal_def Infinitesimal_def) |
161 by (simp add: Infinitesimal_def) |
204 |
162 |
205 lemma one_not_CInfinitesimal [simp]: "1 \<notin> CInfinitesimal" |
163 lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)" |
206 by (simp add: CInfinitesimal_hcmod_iff) |
164 by (simp add: HInfinite_def) |
207 |
165 |
208 lemma CInfinitesimal_add: |
166 lemma HFinite_diff_Infinitesimal_hcmod: |
209 "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> (x+y) \<in> CInfinitesimal" |
167 "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal" |
210 apply (auto simp add: CInfinitesimal_hcmod_iff) |
168 by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff) |
211 apply (rule hrabs_le_Infinitesimal) |
169 |
212 apply (rule_tac y = "hcmod y" in Infinitesimal_add, auto) |
170 lemma hcmod_less_Infinitesimal: |
213 done |
171 "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal" |
214 |
172 by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
215 lemma CInfinitesimal_minus_iff [simp]: |
173 |
216 "(-x:CInfinitesimal) = (x:CInfinitesimal)" |
174 lemma hcmod_le_Infinitesimal: |
217 by (simp add: CInfinitesimal_def) |
175 "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal" |
218 |
176 by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
219 lemma CInfinitesimal_diff: |
177 |
220 "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x-y \<in> CInfinitesimal" |
178 lemma Infinitesimal_interval_hcmod: |
221 by (simp add: diff_minus CInfinitesimal_add) |
179 "[| e \<in> Infinitesimal; |
222 |
180 e' \<in> Infinitesimal; |
223 lemma CInfinitesimal_mult: |
|
224 "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x * y \<in> CInfinitesimal" |
|
225 by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
|
226 |
|
227 lemma CInfinitesimal_CFinite_mult: |
|
228 "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (x * y) \<in> CInfinitesimal" |
|
229 by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult) |
|
230 |
|
231 lemma CInfinitesimal_CFinite_mult2: |
|
232 "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (y * x) \<in> CInfinitesimal" |
|
233 by (auto dest: CInfinitesimal_CFinite_mult simp add: mult_commute) |
|
234 |
|
235 lemma CInfinite_hcmod_iff: "(z \<in> CInfinite) = (hcmod z \<in> HInfinite)" |
|
236 by (simp add: CInfinite_def HInfinite_def) |
|
237 |
|
238 lemma CInfinite_inverse_CInfinitesimal: |
|
239 "x \<in> CInfinite ==> inverse x \<in> CInfinitesimal" |
|
240 by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse) |
|
241 |
|
242 lemma CInfinite_mult: "[|x \<in> CInfinite; y \<in> CInfinite|] ==> (x*y): CInfinite" |
|
243 by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult) |
|
244 |
|
245 lemma CInfinite_minus_iff [simp]: "(-x \<in> CInfinite) = (x \<in> CInfinite)" |
|
246 by (simp add: CInfinite_def) |
|
247 |
|
248 lemma CFinite_sum_squares: |
|
249 "[|a \<in> CFinite; b \<in> CFinite; c \<in> CFinite|] |
|
250 ==> a*a + b*b + c*c \<in> CFinite" |
|
251 by (auto intro: CFinite_mult CFinite_add) |
|
252 |
|
253 lemma not_CInfinitesimal_not_zero: "x \<notin> CInfinitesimal ==> x \<noteq> 0" |
|
254 by auto |
|
255 |
|
256 lemma not_CInfinitesimal_not_zero2: "x \<in> CFinite - CInfinitesimal ==> x \<noteq> 0" |
|
257 by auto |
|
258 |
|
259 lemma CFinite_diff_CInfinitesimal_hcmod: |
|
260 "x \<in> CFinite - CInfinitesimal ==> hcmod x \<in> HFinite - Infinitesimal" |
|
261 by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff) |
|
262 |
|
263 lemma hcmod_less_CInfinitesimal: |
|
264 "[| e \<in> CInfinitesimal; hcmod x < hcmod e |] ==> x \<in> CInfinitesimal" |
|
265 by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff) |
|
266 |
|
267 lemma hcmod_le_CInfinitesimal: |
|
268 "[| e \<in> CInfinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> CInfinitesimal" |
|
269 by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff) |
|
270 |
|
271 lemma CInfinitesimal_interval: |
|
272 "[| e \<in> CInfinitesimal; |
|
273 e' \<in> CInfinitesimal; |
|
274 hcmod e' < hcmod x ; hcmod x < hcmod e |
181 hcmod e' < hcmod x ; hcmod x < hcmod e |
275 |] ==> x \<in> CInfinitesimal" |
182 |] ==> x \<in> Infinitesimal" |
276 by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff) |
183 by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff) |
277 |
184 |
278 lemma CInfinitesimal_interval2: |
185 lemma Infinitesimal_interval2_hcmod: |
279 "[| e \<in> CInfinitesimal; |
186 "[| e \<in> Infinitesimal; |
280 e' \<in> CInfinitesimal; |
187 e' \<in> Infinitesimal; |
281 hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e |
188 hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e |
282 |] ==> x \<in> CInfinitesimal" |
189 |] ==> x \<in> Infinitesimal" |
283 by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff) |
190 by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff) |
284 |
191 |
285 lemma not_CInfinitesimal_mult: |
192 lemma Infinitesimal_hcomplex_of_complex_mult: |
286 "[| x \<notin> CInfinitesimal; y \<notin> CInfinitesimal|] ==> (x*y) \<notin> CInfinitesimal" |
193 "x \<in> Infinitesimal ==> x * hcomplex_of_complex r \<in> Infinitesimal" |
287 apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
194 by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult) |
288 apply (drule not_Infinitesimal_mult, auto) |
195 |
289 done |
196 lemma Infinitesimal_hcomplex_of_complex_mult2: |
290 |
197 "x \<in> Infinitesimal ==> hcomplex_of_complex r * x \<in> Infinitesimal" |
291 lemma CInfinitesimal_mult_disj: |
198 by (auto intro!: Infinitesimal_HFinite_mult2 simp add: Infinitesimal_hcmod_iff hcmod_mult) |
292 "x*y \<in> CInfinitesimal ==> x \<in> CInfinitesimal | y \<in> CInfinitesimal" |
|
293 by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
|
294 |
|
295 lemma CFinite_CInfinitesimal_diff_mult: |
|
296 "[| x \<in> CFinite - CInfinitesimal; y \<in> CFinite - CInfinitesimal |] |
|
297 ==> x*y \<in> CFinite - CInfinitesimal" |
|
298 by (blast dest: CFinite_mult not_CInfinitesimal_mult) |
|
299 |
|
300 lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \<le> CFinite" |
|
301 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
|
302 simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff) |
|
303 |
|
304 lemma CInfinitesimal_hcomplex_of_complex_mult: |
|
305 "x \<in> CInfinitesimal ==> x * hcomplex_of_complex r \<in> CInfinitesimal" |
|
306 by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
|
307 |
|
308 lemma CInfinitesimal_hcomplex_of_complex_mult2: |
|
309 "x \<in> CInfinitesimal ==> hcomplex_of_complex r * x \<in> CInfinitesimal" |
|
310 by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
|
311 |
199 |
312 |
200 |
313 subsection{*The ``Infinitely Close'' Relation*} |
201 subsection{*The ``Infinitely Close'' Relation*} |
314 |
202 |
315 (* |
203 (* |
316 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)" |
204 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)" |
317 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff])); |
205 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); |
318 *) |
206 *) |
319 |
207 |
320 lemma mem_cinfmal_iff: "x:CInfinitesimal = (x @c= 0)" |
208 lemma approx_mult_subst_SComplex: |
321 by (simp add: CInfinitesimal_hcmod_iff capprox_def) |
209 "[| u @= x*hcomplex_of_complex v; x @= y |] |
322 |
210 ==> u @= y*hcomplex_of_complex v" |
323 lemma capprox_minus_iff: "(x @c= y) = (x + -y @c= 0)" |
211 by (auto intro: approx_mult_subst2) |
324 by (simp add: capprox_def diff_minus) |
212 |
325 |
213 lemma approx_hcomplex_of_complex_HFinite: |
326 lemma capprox_minus_iff2: "(x @c= y) = (-y + x @c= 0)" |
214 "x @= hcomplex_of_complex D ==> x \<in> HFinite" |
327 by (simp add: capprox_def diff_minus add_commute) |
215 by (rule approx_star_of_HFinite) |
328 |
216 |
329 lemma capprox_refl [simp]: "x @c= x" |
217 lemma approx_mult_hcomplex_of_complex: |
330 by (simp add: capprox_def) |
218 "[|a @= hcomplex_of_complex b; c @= hcomplex_of_complex d |] |
331 |
219 ==> a*c @= hcomplex_of_complex b * hcomplex_of_complex d" |
332 lemma capprox_sym: "x @c= y ==> y @c= x" |
220 by (rule approx_mult_star_of) |
333 by (simp add: capprox_def CInfinitesimal_def hcmod_diff_commute) |
221 |
334 |
222 lemma approx_SComplex_mult_cancel_zero: |
335 lemma capprox_trans: "[| x @c= y; y @c= z |] ==> x @c= z" |
223 "[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0" |
336 apply (simp add: capprox_def) |
224 apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) |
337 apply (drule CInfinitesimal_add, assumption) |
225 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
338 apply (simp add: diff_minus) |
226 done |
339 done |
227 |
340 |
228 lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0" |
341 lemma capprox_trans2: "[| r @c= x; s @c= x |] ==> r @c= s" |
229 by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1) |
342 by (blast intro: capprox_sym capprox_trans) |
230 |
343 |
231 lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0" |
344 lemma capprox_trans3: "[| x @c= r; x @c= s|] ==> r @c= s" |
232 by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult2) |
345 by (blast intro: capprox_sym capprox_trans) |
233 |
346 |
234 lemma approx_mult_SComplex_zero_cancel_iff [simp]: |
347 lemma number_of_capprox_reorient [simp]: |
235 "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)" |
348 "(number_of w @c= x) = (x @c= number_of w)" |
236 by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2) |
349 by (blast intro: capprox_sym) |
237 |
350 |
238 lemma approx_SComplex_mult_cancel: |
351 lemma CInfinitesimal_capprox_minus: "(x-y \<in> CInfinitesimal) = (x @c= y)" |
239 "[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z" |
352 by (simp add: diff_minus capprox_minus_iff [symmetric] mem_cinfmal_iff) |
240 apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) |
353 |
241 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
354 lemma capprox_monad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))" |
242 done |
355 by (auto simp add: cmonad_def dest: capprox_sym elim!: capprox_trans equalityCE) |
243 |
356 |
244 lemma approx_SComplex_mult_cancel_iff1 [simp]: |
357 lemma Infinitesimal_capprox: |
245 "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)" |
358 "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x @c= y" |
246 by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD] |
359 apply (simp add: mem_cinfmal_iff) |
247 intro: approx_SComplex_mult_cancel) |
360 apply (blast intro: capprox_trans capprox_sym) |
248 |
361 done |
249 lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)" |
362 |
250 apply (subst hcmod_diff_commute) |
363 lemma capprox_add: "[| a @c= b; c @c= d |] ==> a+c @c= b+d" |
251 apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) |
364 apply (simp add: capprox_def diff_minus) |
252 done |
365 apply (rule minus_add_distrib [THEN ssubst]) |
253 |
366 apply (rule add_assoc [THEN ssubst]) |
254 lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)" |
367 apply (rule_tac b1 = c in add_left_commute [THEN subst]) |
255 by (simp add: approx_hcmod_approx_zero) |
368 apply (rule add_assoc [THEN subst]) |
256 |
369 apply (blast intro: CInfinitesimal_add) |
257 lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)" |
370 done |
258 by (simp add: approx_def) |
371 |
|
372 lemma capprox_minus: "a @c= b ==> -a @c= -b" |
|
373 apply (rule capprox_minus_iff [THEN iffD2, THEN capprox_sym]) |
|
374 apply (drule capprox_minus_iff [THEN iffD1]) |
|
375 apply (simp add: add_commute) |
|
376 done |
|
377 |
|
378 lemma capprox_minus2: "-a @c= -b ==> a @c= b" |
|
379 by (auto dest: capprox_minus) |
|
380 |
|
381 lemma capprox_minus_cancel [simp]: "(-a @c= -b) = (a @c= b)" |
|
382 by (blast intro: capprox_minus capprox_minus2) |
|
383 |
|
384 lemma capprox_add_minus: "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d" |
|
385 by (blast intro!: capprox_add capprox_minus) |
|
386 |
|
387 lemma capprox_mult1: |
|
388 "[| a @c= b; c \<in> CFinite|] ==> a*c @c= b*c" |
|
389 apply (simp add: capprox_def diff_minus) |
|
390 apply (simp only: CInfinitesimal_CFinite_mult minus_mult_left left_distrib [symmetric]) |
|
391 done |
|
392 |
|
393 lemma capprox_mult2: "[|a @c= b; c \<in> CFinite|] ==> c*a @c= c*b" |
|
394 by (simp add: capprox_mult1 mult_commute) |
|
395 |
|
396 lemma capprox_mult_subst: |
|
397 "[|u @c= v*x; x @c= y; v \<in> CFinite|] ==> u @c= v*y" |
|
398 by (blast intro: capprox_mult2 capprox_trans) |
|
399 |
|
400 lemma capprox_mult_subst2: |
|
401 "[| u @c= x*v; x @c= y; v \<in> CFinite |] ==> u @c= y*v" |
|
402 by (blast intro: capprox_mult1 capprox_trans) |
|
403 |
|
404 lemma capprox_mult_subst_SComplex: |
|
405 "[| u @c= x*hcomplex_of_complex v; x @c= y |] |
|
406 ==> u @c= y*hcomplex_of_complex v" |
|
407 by (auto intro: capprox_mult_subst2) |
|
408 |
|
409 lemma capprox_eq_imp: "a = b ==> a @c= b" |
|
410 by (simp add: capprox_def) |
|
411 |
|
412 lemma CInfinitesimal_minus_capprox: "x \<in> CInfinitesimal ==> -x @c= x" |
|
413 by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2) |
|
414 |
|
415 lemma bex_CInfinitesimal_iff: "(\<exists>y \<in> CInfinitesimal. x - z = y) = (x @c= z)" |
|
416 by (unfold capprox_def, blast) |
|
417 |
|
418 lemma bex_CInfinitesimal_iff2: "(\<exists>y \<in> CInfinitesimal. x = z + y) = (x @c= z)" |
|
419 by (simp add: bex_CInfinitesimal_iff [symmetric], force) |
|
420 |
|
421 lemma CInfinitesimal_add_capprox: |
|
422 "[| y \<in> CInfinitesimal; x + y = z |] ==> x @c= z" |
|
423 apply (rule bex_CInfinitesimal_iff [THEN iffD1]) |
|
424 apply (drule CInfinitesimal_minus_iff [THEN iffD2]) |
|
425 apply (simp add: eq_commute compare_rls) |
|
426 done |
|
427 |
|
428 lemma CInfinitesimal_add_capprox_self: "y \<in> CInfinitesimal ==> x @c= x + y" |
|
429 apply (rule bex_CInfinitesimal_iff [THEN iffD1]) |
|
430 apply (drule CInfinitesimal_minus_iff [THEN iffD2]) |
|
431 apply (simp add: eq_commute compare_rls) |
|
432 done |
|
433 |
|
434 lemma CInfinitesimal_add_capprox_self2: "y \<in> CInfinitesimal ==> x @c= y + x" |
|
435 by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute) |
|
436 |
|
437 lemma CInfinitesimal_add_minus_capprox_self: |
|
438 "y \<in> CInfinitesimal ==> x @c= x + -y" |
|
439 by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2]) |
|
440 |
|
441 lemma CInfinitesimal_add_cancel: |
|
442 "[| y \<in> CInfinitesimal; x+y @c= z|] ==> x @c= z" |
|
443 apply (drule_tac x = x in CInfinitesimal_add_capprox_self [THEN capprox_sym]) |
|
444 apply (erule capprox_trans3 [THEN capprox_sym], assumption) |
|
445 done |
|
446 |
|
447 lemma CInfinitesimal_add_right_cancel: |
|
448 "[| y \<in> CInfinitesimal; x @c= z + y|] ==> x @c= z" |
|
449 apply (drule_tac x = z in CInfinitesimal_add_capprox_self2 [THEN capprox_sym]) |
|
450 apply (erule capprox_trans3 [THEN capprox_sym]) |
|
451 apply (simp add: add_commute) |
|
452 apply (erule capprox_sym) |
|
453 done |
|
454 |
|
455 lemma capprox_add_left_cancel: "d + b @c= d + c ==> b @c= c" |
|
456 apply (drule capprox_minus_iff [THEN iffD1]) |
|
457 apply (simp add: minus_add_distrib capprox_minus_iff [symmetric] add_ac) |
|
458 done |
|
459 |
|
460 lemma capprox_add_right_cancel: "b + d @c= c + d ==> b @c= c" |
|
461 apply (rule capprox_add_left_cancel) |
|
462 apply (simp add: add_commute) |
|
463 done |
|
464 |
|
465 lemma capprox_add_mono1: "b @c= c ==> d + b @c= d + c" |
|
466 apply (rule capprox_minus_iff [THEN iffD2]) |
|
467 apply (simp add: capprox_minus_iff [symmetric] add_ac) |
|
468 done |
|
469 |
|
470 lemma capprox_add_mono2: "b @c= c ==> b + a @c= c + a" |
|
471 apply (simp (no_asm_simp) add: add_commute capprox_add_mono1) |
|
472 done |
|
473 |
|
474 lemma capprox_add_left_iff [iff]: "(a + b @c= a + c) = (b @c= c)" |
|
475 by (fast elim: capprox_add_left_cancel capprox_add_mono1) |
|
476 |
|
477 lemma capprox_add_right_iff [iff]: "(b + a @c= c + a) = (b @c= c)" |
|
478 by (simp add: add_commute) |
|
479 |
|
480 lemma capprox_CFinite: "[| x \<in> CFinite; x @c= y |] ==> y \<in> CFinite" |
|
481 apply (drule bex_CInfinitesimal_iff2 [THEN iffD2], safe) |
|
482 apply (drule CInfinitesimal_subset_CFinite [THEN subsetD, THEN CFinite_minus_iff [THEN iffD2]]) |
|
483 apply (drule CFinite_add) |
|
484 apply (assumption, auto) |
|
485 done |
|
486 |
|
487 lemma capprox_hcomplex_of_complex_CFinite: |
|
488 "x @c= hcomplex_of_complex D ==> x \<in> CFinite" |
|
489 by (rule capprox_sym [THEN [2] capprox_CFinite], auto) |
|
490 |
|
491 lemma capprox_mult_CFinite: |
|
492 "[|a @c= b; c @c= d; b \<in> CFinite; d \<in> CFinite|] ==> a*c @c= b*d" |
|
493 apply (rule capprox_trans) |
|
494 apply (rule_tac [2] capprox_mult2) |
|
495 apply (rule capprox_mult1) |
|
496 prefer 2 apply (blast intro: capprox_CFinite capprox_sym, auto) |
|
497 done |
|
498 |
|
499 lemma capprox_mult_hcomplex_of_complex: |
|
500 "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |] |
|
501 ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d" |
|
502 apply (blast intro!: capprox_mult_CFinite capprox_hcomplex_of_complex_CFinite CFinite_hcomplex_of_complex) |
|
503 done |
|
504 |
|
505 lemma capprox_SComplex_mult_cancel_zero: |
|
506 "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0" |
|
507 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]]) |
|
508 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) |
|
509 done |
|
510 |
|
511 lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0" |
|
512 by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1) |
|
513 |
|
514 lemma capprox_mult_SComplex2: "[| a \<in> SComplex; x @c= 0 |] ==> a*x @c= 0" |
|
515 by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult2) |
|
516 |
|
517 lemma capprox_mult_SComplex_zero_cancel_iff [simp]: |
|
518 "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @c= 0) = (x @c= 0)" |
|
519 by (blast intro: capprox_SComplex_mult_cancel_zero capprox_mult_SComplex2) |
|
520 |
|
521 lemma capprox_SComplex_mult_cancel: |
|
522 "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z" |
|
523 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]]) |
|
524 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) |
|
525 done |
|
526 |
|
527 lemma capprox_SComplex_mult_cancel_iff1 [simp]: |
|
528 "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @c= a*z) = (w @c= z)" |
|
529 by (auto intro!: capprox_mult2 SComplex_subset_CFinite [THEN subsetD] |
|
530 intro: capprox_SComplex_mult_cancel) |
|
531 |
|
532 lemma capprox_hcmod_approx_zero: "(x @c= y) = (hcmod (y - x) @= 0)" |
|
533 apply (rule capprox_minus_iff [THEN ssubst]) |
|
534 apply (simp add: capprox_def CInfinitesimal_hcmod_iff mem_infmal_iff diff_minus [symmetric] hcmod_diff_commute) |
|
535 done |
|
536 |
|
537 lemma capprox_approx_zero_iff: "(x @c= 0) = (hcmod x @= 0)" |
|
538 by (simp add: capprox_hcmod_approx_zero) |
|
539 |
|
540 lemma capprox_minus_zero_cancel_iff [simp]: "(-x @c= 0) = (x @c= 0)" |
|
541 by (simp add: capprox_hcmod_approx_zero) |
|
542 |
259 |
543 lemma Infinitesimal_hcmod_add_diff: |
260 lemma Infinitesimal_hcmod_add_diff: |
544 "u @c= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal" |
261 "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal" |
|
262 apply (drule approx_approx_zero_iff [THEN iffD1]) |
545 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2) |
263 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2) |
546 apply (auto dest: capprox_approx_zero_iff [THEN iffD1] |
264 apply (auto simp add: mem_infmal_iff [symmetric] diff_def) |
547 simp add: mem_infmal_iff [symmetric] diff_def) |
|
548 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) |
265 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) |
549 apply (auto simp add: diff_minus [symmetric]) |
266 apply (auto simp add: diff_minus [symmetric]) |
550 done |
267 done |
551 |
268 |
552 lemma approx_hcmod_add_hcmod: "u @c= 0 ==> hcmod(x + u) @= hcmod x" |
269 lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x" |
553 apply (rule approx_minus_iff [THEN iffD2]) |
270 apply (rule approx_minus_iff [THEN iffD2]) |
554 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) |
271 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) |
555 done |
272 done |
556 |
273 |
557 lemma capprox_hcmod_approx: "x @c= y ==> hcmod x @= hcmod y" |
274 lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y" |
558 by (auto intro: approx_hcmod_add_hcmod |
275 by (auto intro: approx_hcmod_add_hcmod |
559 dest!: bex_CInfinitesimal_iff2 [THEN iffD2] |
276 dest!: bex_Infinitesimal_iff2 [THEN iffD2] |
560 simp add: mem_cinfmal_iff) |
277 simp add: mem_infmal_iff) |
561 |
278 |
562 |
279 |
563 subsection{*Zero is the Only Infinitesimal Complex Number*} |
280 subsection{*Zero is the Only Infinitesimal Complex Number*} |
564 |
281 |
565 lemma CInfinitesimal_less_SComplex: |
282 lemma Infinitesimal_less_SComplex: |
566 "[| x \<in> SComplex; y \<in> CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x" |
283 "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x" |
567 by (auto intro!: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: CInfinitesimal_hcmod_iff) |
284 by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff) |
568 |
285 |
569 lemma SComplex_Int_CInfinitesimal_zero: "SComplex Int CInfinitesimal = {0}" |
286 lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" |
570 apply (auto simp add: SComplex_def CInfinitesimal_hcmod_iff) |
287 by (auto simp add: SComplex_def Infinitesimal_hcmod_iff) |
571 apply (cut_tac r = r in SReal_hcmod_hcomplex_of_complex) |
288 |
572 apply (drule_tac A = Reals in IntI, assumption) |
289 lemma SComplex_Infinitesimal_zero: |
573 apply (subgoal_tac "hcmod (hcomplex_of_complex r) = 0") |
290 "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0" |
574 apply simp |
291 by (cut_tac SComplex_Int_Infinitesimal_zero, blast) |
575 apply (simp add: SReal_Int_Infinitesimal_zero) |
292 |
576 done |
293 lemma SComplex_HFinite_diff_Infinitesimal: |
577 |
294 "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal" |
578 lemma SComplex_CInfinitesimal_zero: |
295 by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD]) |
579 "[| x \<in> SComplex; x \<in> CInfinitesimal|] ==> x = 0" |
296 |
580 by (cut_tac SComplex_Int_CInfinitesimal_zero, blast) |
297 lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: |
581 |
|
582 lemma SComplex_CFinite_diff_CInfinitesimal: |
|
583 "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> CFinite - CInfinitesimal" |
|
584 by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD]) |
|
585 |
|
586 lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal: |
|
587 "hcomplex_of_complex x \<noteq> 0 |
298 "hcomplex_of_complex x \<noteq> 0 |
588 ==> hcomplex_of_complex x \<in> CFinite - CInfinitesimal" |
299 ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal" |
589 by (rule SComplex_CFinite_diff_CInfinitesimal, auto) |
300 by (rule SComplex_HFinite_diff_Infinitesimal, auto) |
590 |
301 |
591 lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]: |
302 lemma hcomplex_of_complex_Infinitesimal_iff_0: |
592 "(hcomplex_of_complex x \<in> CInfinitesimal) = (x=0)" |
303 "(hcomplex_of_complex x \<in> Infinitesimal) = (x=0)" |
593 apply (auto) |
304 by (rule star_of_Infinitesimal_iff_0) |
594 apply (rule ccontr) |
305 |
595 apply (rule hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN DiffD2], auto) |
306 lemma number_of_not_Infinitesimal [simp]: |
596 done |
307 "number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal" |
597 |
308 by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) |
598 lemma number_of_not_CInfinitesimal [simp]: |
309 |
599 "number_of w \<noteq> (0::hcomplex) ==> number_of w \<notin> CInfinitesimal" |
310 lemma approx_SComplex_not_zero: |
600 by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero]) |
311 "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
601 |
312 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) |
602 lemma capprox_SComplex_not_zero: |
313 |
603 "[| y \<in> SComplex; x @c= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
314 lemma SComplex_approx_iff: |
604 by (auto dest: SComplex_CInfinitesimal_zero capprox_sym [THEN mem_cinfmal_iff [THEN iffD2]]) |
315 "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)" |
605 |
316 by (auto simp add: SComplex_def) |
606 lemma CFinite_diff_CInfinitesimal_capprox: |
317 |
607 "[| x @c= y; y \<in> CFinite - CInfinitesimal |] |
318 lemma number_of_Infinitesimal_iff [simp]: |
608 ==> x \<in> CFinite - CInfinitesimal" |
319 "((number_of w :: hcomplex) \<in> Infinitesimal) = |
609 apply (auto intro: capprox_sym [THEN [2] capprox_CFinite] |
320 (number_of w = (0::hcomplex))" |
610 simp add: mem_cinfmal_iff) |
|
611 apply (drule capprox_trans3, assumption) |
|
612 apply (blast dest: capprox_sym) |
|
613 done |
|
614 |
|
615 lemma CInfinitesimal_ratio: |
|
616 "[| y \<noteq> 0; y \<in> CInfinitesimal; x/y \<in> CFinite |] ==> x \<in> CInfinitesimal" |
|
617 apply (drule CInfinitesimal_CFinite_mult2, assumption) |
|
618 apply (simp add: divide_inverse mult_assoc) |
|
619 done |
|
620 |
|
621 lemma SComplex_capprox_iff: |
|
622 "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @c= y) = (x = y)" |
|
623 apply auto |
|
624 apply (simp add: capprox_def) |
|
625 apply (subgoal_tac "x-y = 0", simp) |
|
626 apply (rule SComplex_CInfinitesimal_zero) |
|
627 apply (simp add: SComplex_diff, assumption) |
|
628 done |
|
629 |
|
630 lemma number_of_capprox_iff [simp]: |
|
631 "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))" |
|
632 by (rule SComplex_capprox_iff, auto) |
|
633 |
|
634 lemma number_of_CInfinitesimal_iff [simp]: |
|
635 "(number_of w \<in> CInfinitesimal) = (number_of w = (0::hcomplex))" |
|
636 apply (rule iffI) |
321 apply (rule iffI) |
637 apply (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero]) |
322 apply (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) |
638 apply (simp (no_asm_simp)) |
323 apply (simp (no_asm_simp)) |
639 done |
324 done |
640 |
325 |
641 lemma hcomplex_of_complex_approx_iff [simp]: |
326 lemma hcomplex_of_complex_approx_iff: |
642 "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)" |
327 "(hcomplex_of_complex k @= hcomplex_of_complex m) = (k = m)" |
643 apply auto |
328 by (rule star_of_approx_iff) |
644 apply (rule inj_hcomplex_of_complex [THEN injD]) |
329 |
645 apply (rule SComplex_capprox_iff [THEN iffD1], auto) |
330 lemma hcomplex_of_complex_approx_number_of_iff [simp]: |
646 done |
331 "(hcomplex_of_complex k @= number_of w) = (k = number_of w)" |
647 |
|
648 lemma hcomplex_of_complex_capprox_number_of_iff [simp]: |
|
649 "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)" |
|
650 by (subst hcomplex_of_complex_approx_iff [symmetric], auto) |
332 by (subst hcomplex_of_complex_approx_iff [symmetric], auto) |
651 |
333 |
652 lemma capprox_unique_complex: |
334 lemma approx_unique_complex: |
653 "[| r \<in> SComplex; s \<in> SComplex; r @c= x; s @c= x|] ==> r = s" |
335 "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
654 by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2) |
336 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) |
655 |
337 |
656 lemma hcomplex_capproxD1: |
338 lemma hcomplex_approxD1: |
657 "star_n X @c= star_n Y |
339 "star_n X @= star_n Y |
658 ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" |
340 ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" |
659 apply (simp add: approx_FreeUltrafilterNat_iff2, safe) |
341 apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
660 apply (drule capprox_minus_iff [THEN iffD1]) |
342 apply (drule approx_minus_iff [THEN iffD1]) |
661 apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
343 apply (simp add: star_n_minus star_n_add mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
662 apply (drule_tac x = m in spec) |
344 apply (drule_tac x = m in spec) |
663 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
345 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
664 apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) |
346 apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) |
665 apply (case_tac "X n") |
347 apply (case_tac "X n") |
666 apply (case_tac "Y n") |
348 apply (case_tac "Y n") |
667 apply (auto simp add: complex_minus complex_add complex_mod |
349 apply (auto simp add: complex_minus complex_add complex_mod |
668 simp del: realpow_Suc) |
350 simp del: realpow_Suc) |
669 done |
351 done |
670 |
352 |
671 (* same proof *) |
353 (* same proof *) |
672 lemma hcomplex_capproxD2: |
354 lemma hcomplex_approxD2: |
673 "star_n X @c= star_n Y |
355 "star_n X @= star_n Y |
674 ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" |
356 ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" |
675 apply (simp add: approx_FreeUltrafilterNat_iff2, safe) |
357 apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
676 apply (drule capprox_minus_iff [THEN iffD1]) |
358 apply (drule approx_minus_iff [THEN iffD1]) |
677 apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
359 apply (simp add: star_n_minus star_n_add mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
678 apply (drule_tac x = m in spec) |
360 apply (drule_tac x = m in spec) |
679 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
361 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
680 apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) |
362 apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) |
681 apply (case_tac "X n") |
363 apply (case_tac "X n") |
682 apply (case_tac "Y n") |
364 apply (case_tac "Y n") |
683 apply (auto simp add: complex_minus complex_add complex_mod |
365 apply (auto simp add: complex_minus complex_add complex_mod |
684 simp del: realpow_Suc) |
366 simp del: realpow_Suc) |
685 done |
367 done |
686 |
368 |
687 lemma hcomplex_capproxI: |
369 lemma hcomplex_approxI: |
688 "[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); |
370 "[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); |
689 star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) |
371 star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) |
690 |] ==> star_n X @c= star_n Y" |
372 |] ==> star_n X @= star_n Y" |
691 apply (drule approx_minus_iff [THEN iffD1]) |
373 apply (drule approx_minus_iff [THEN iffD1]) |
692 apply (drule approx_minus_iff [THEN iffD1]) |
374 apply (drule approx_minus_iff [THEN iffD1]) |
693 apply (rule capprox_minus_iff [THEN iffD2]) |
375 apply (rule approx_minus_iff [THEN iffD2]) |
694 apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
376 apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
695 apply (drule_tac x = "u/2" in spec) |
377 apply (drule_tac x = "u/2" in spec) |
696 apply (drule_tac x = "u/2" in spec, auto, ultra) |
378 apply (drule_tac x = "u/2" in spec, auto, ultra) |
697 apply (case_tac "X x") |
379 apply (case_tac "X x") |
698 apply (case_tac "Y x") |
380 apply (case_tac "Y x") |
699 apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2) |
381 apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2) |
792 "(star_n X \<in> SComplex) = |
474 "(star_n X \<in> SComplex) = |
793 (star_n (%n. Re(X n)) \<in> Reals & |
475 (star_n (%n. Re(X n)) \<in> Reals & |
794 star_n (%n. Im(X n)) \<in> Reals)" |
476 star_n (%n. Im(X n)) \<in> Reals)" |
795 by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) |
477 by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) |
796 |
478 |
797 lemma CInfinitesimal_Infinitesimal_iff: |
479 lemma Infinitesimal_Infinitesimal_iff: |
798 "(star_n X \<in> CInfinitesimal) = |
480 "(star_n X \<in> Infinitesimal) = |
799 (star_n (%n. Re(X n)) \<in> Infinitesimal & |
481 (star_n (%n. Re(X n)) \<in> Infinitesimal & |
800 star_n (%n. Im(X n)) \<in> Infinitesimal)" |
482 star_n (%n. Im(X n)) \<in> Infinitesimal)" |
801 by (simp add: mem_cinfmal_iff mem_infmal_iff star_n_zero_num capprox_approx_iff) |
483 by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) |
802 |
484 |
803 lemma eq_Abs_star_EX: |
485 lemma eq_Abs_star_EX: |
804 "(\<exists>t. P t) = (\<exists>X. P (star_n X))" |
486 "(\<exists>t. P t) = (\<exists>X. P (star_n X))" |
805 by (rule ex_star_eq) |
487 by (rule ex_star_eq) |
806 |
488 |
807 lemma eq_Abs_star_Bex: |
489 lemma eq_Abs_star_Bex: |
808 "(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))" |
490 "(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))" |
809 by (simp add: Bex_def ex_star_eq) |
491 by (simp add: Bex_def ex_star_eq) |
810 |
492 |
811 (* Here we go - easy proof now!! *) |
493 (* Here we go - easy proof now!! *) |
812 lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t" |
494 lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" |
813 apply (cases x) |
495 apply (cases x) |
814 apply (auto simp add: CFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff capprox_approx_iff) |
496 apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) |
815 apply (drule st_part_Ex, safe)+ |
497 apply (drule st_part_Ex, safe)+ |
816 apply (rule_tac x = t in star_cases) |
498 apply (rule_tac x = t in star_cases) |
817 apply (rule_tac x = ta in star_cases, auto) |
499 apply (rule_tac x = ta in star_cases, auto) |
818 apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) |
500 apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) |
819 apply auto |
501 apply auto |
820 done |
502 done |
821 |
503 |
822 lemma stc_part_Ex1: "x:CFinite ==> EX! t. t \<in> SComplex & x @c= t" |
504 lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" |
823 apply (drule stc_part_Ex, safe) |
505 apply (drule stc_part_Ex, safe) |
824 apply (drule_tac [2] capprox_sym, drule_tac [2] capprox_sym, drule_tac [2] capprox_sym) |
506 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
825 apply (auto intro!: capprox_unique_complex) |
507 apply (auto intro!: approx_unique_complex) |
826 done |
508 done |
827 |
509 |
828 lemma CFinite_Int_CInfinite_empty: "CFinite Int CInfinite = {}" |
510 lemmas hcomplex_of_complex_approx_inverse = |
829 by (simp add: CFinite_def CInfinite_def, auto) |
511 hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
830 |
|
831 lemma CFinite_not_CInfinite: "x \<in> CFinite ==> x \<notin> CInfinite" |
|
832 by (insert CFinite_Int_CInfinite_empty, blast) |
|
833 |
|
834 text{*Not sure this is a good idea!*} |
|
835 declare CFinite_Int_CInfinite_empty [simp] |
|
836 |
|
837 lemma not_CFinite_CInfinite: "x\<notin> CFinite ==> x \<in> CInfinite" |
|
838 by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff) |
|
839 |
|
840 lemma CInfinite_CFinite_disj: "x \<in> CInfinite | x \<in> CFinite" |
|
841 by (blast intro: not_CFinite_CInfinite) |
|
842 |
|
843 lemma CInfinite_CFinite_iff: "(x \<in> CInfinite) = (x \<notin> CFinite)" |
|
844 by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite) |
|
845 |
|
846 lemma CFinite_CInfinite_iff: "(x \<in> CFinite) = (x \<notin> CInfinite)" |
|
847 by (simp add: CInfinite_CFinite_iff) |
|
848 |
|
849 lemma CInfinite_diff_CFinite_CInfinitesimal_disj: |
|
850 "x \<notin> CInfinitesimal ==> x \<in> CInfinite | x \<in> CFinite - CInfinitesimal" |
|
851 by (fast intro: not_CFinite_CInfinite) |
|
852 |
|
853 lemma CFinite_inverse: |
|
854 "[| x \<in> CFinite; x \<notin> CInfinitesimal |] ==> inverse x \<in> CFinite" |
|
855 apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj) |
|
856 apply (auto dest!: CInfinite_inverse_CInfinitesimal) |
|
857 done |
|
858 |
|
859 lemma CFinite_inverse2: "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite" |
|
860 by (blast intro: CFinite_inverse) |
|
861 |
|
862 lemma CInfinitesimal_inverse_CFinite: |
|
863 "x \<notin> CInfinitesimal ==> inverse(x) \<in> CFinite" |
|
864 apply (drule CInfinite_diff_CFinite_CInfinitesimal_disj) |
|
865 apply (blast intro: CFinite_inverse CInfinite_inverse_CInfinitesimal CInfinitesimal_subset_CFinite [THEN subsetD]) |
|
866 done |
|
867 |
|
868 |
|
869 lemma CFinite_not_CInfinitesimal_inverse: |
|
870 "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite - CInfinitesimal" |
|
871 apply (auto intro: CInfinitesimal_inverse_CFinite) |
|
872 apply (drule CInfinitesimal_CFinite_mult2, assumption) |
|
873 apply (simp add: not_CInfinitesimal_not_zero) |
|
874 done |
|
875 |
|
876 lemma capprox_inverse: |
|
877 "[| x @c= y; y \<in> CFinite - CInfinitesimal |] ==> inverse x @c= inverse y" |
|
878 apply (frule CFinite_diff_CInfinitesimal_capprox, assumption) |
|
879 apply (frule not_CInfinitesimal_not_zero2) |
|
880 apply (frule_tac x = x in not_CInfinitesimal_not_zero2) |
|
881 apply (drule CFinite_inverse2)+ |
|
882 apply (drule capprox_mult2, assumption, auto) |
|
883 apply (drule_tac c = "inverse x" in capprox_mult1, assumption) |
|
884 apply (auto intro: capprox_sym simp add: mult_assoc) |
|
885 done |
|
886 |
|
887 lemmas hcomplex_of_complex_capprox_inverse = |
|
888 hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse] |
|
889 |
|
890 lemma inverse_add_CInfinitesimal_capprox: |
|
891 "[| x \<in> CFinite - CInfinitesimal; |
|
892 h \<in> CInfinitesimal |] ==> inverse(x + h) @c= inverse x" |
|
893 by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self) |
|
894 |
|
895 lemma inverse_add_CInfinitesimal_capprox2: |
|
896 "[| x \<in> CFinite - CInfinitesimal; |
|
897 h \<in> CInfinitesimal |] ==> inverse(h + x) @c= inverse x" |
|
898 apply (rule add_commute [THEN subst]) |
|
899 apply (blast intro: inverse_add_CInfinitesimal_capprox) |
|
900 done |
|
901 |
|
902 lemma inverse_add_CInfinitesimal_approx_CInfinitesimal: |
|
903 "[| x \<in> CFinite - CInfinitesimal; |
|
904 h \<in> CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h" |
|
905 apply (rule capprox_trans2) |
|
906 apply (auto intro: inverse_add_CInfinitesimal_capprox |
|
907 simp add: mem_cinfmal_iff diff_minus capprox_minus_iff [symmetric]) |
|
908 done |
|
909 |
|
910 lemma CInfinitesimal_square_iff [iff]: |
|
911 "(x*x \<in> CInfinitesimal) = (x \<in> CInfinitesimal)" |
|
912 by (simp add: CInfinitesimal_hcmod_iff hcmod_mult) |
|
913 |
|
914 lemma capprox_CFinite_mult_cancel: |
|
915 "[| a \<in> CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z" |
|
916 apply safe |
|
917 apply (frule CFinite_inverse, assumption) |
|
918 apply (drule not_CInfinitesimal_not_zero) |
|
919 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) |
|
920 done |
|
921 |
|
922 lemma capprox_CFinite_mult_cancel_iff1: |
|
923 "a \<in> CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)" |
|
924 by (auto intro: capprox_mult2 capprox_CFinite_mult_cancel) |
|
925 |
512 |
926 |
513 |
927 subsection{*Theorems About Monads*} |
514 subsection{*Theorems About Monads*} |
928 |
515 |
929 lemma capprox_cmonad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))" |
516 lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)" |
930 apply (simp add: cmonad_def) |
517 by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) |
931 apply (auto dest: capprox_sym elim!: capprox_trans equalityCE) |
|
932 done |
|
933 |
|
934 lemma CInfinitesimal_cmonad_eq: |
|
935 "e \<in> CInfinitesimal ==> cmonad (x+e) = cmonad x" |
|
936 by (fast intro!: CInfinitesimal_add_capprox_self [THEN capprox_sym] capprox_cmonad_iff [THEN iffD1]) |
|
937 |
|
938 lemma mem_cmonad_iff: "(u \<in> cmonad x) = (-u \<in> cmonad (-x))" |
|
939 by (simp add: cmonad_def) |
|
940 |
|
941 lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \<in> cmonad 0)" |
|
942 by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def) |
|
943 |
|
944 lemma cmonad_zero_minus_iff: "(x \<in> cmonad 0) = (-x \<in> cmonad 0)" |
|
945 by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric]) |
|
946 |
|
947 lemma cmonad_zero_hcmod_iff: "(x \<in> cmonad 0) = (hcmod x:monad 0)" |
|
948 by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric] CInfinitesimal_hcmod_iff Infinitesimal_monad_zero_iff [symmetric]) |
|
949 |
|
950 lemma mem_cmonad_self [simp]: "x \<in> cmonad x" |
|
951 by (simp add: cmonad_def) |
|
952 |
518 |
953 |
519 |
954 subsection{*Theorems About Standard Part*} |
520 subsection{*Theorems About Standard Part*} |
955 |
521 |
956 lemma stc_capprox_self: "x \<in> CFinite ==> stc x @c= x" |
522 lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x" |
957 apply (simp add: stc_def) |
523 apply (simp add: stc_def) |
958 apply (frule stc_part_Ex, safe) |
524 apply (frule stc_part_Ex, safe) |
959 apply (rule someI2) |
525 apply (rule someI2) |
960 apply (auto intro: capprox_sym) |
526 apply (auto intro: approx_sym) |
961 done |
527 done |
962 |
528 |
963 lemma stc_SComplex: "x \<in> CFinite ==> stc x \<in> SComplex" |
529 lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex" |
964 apply (simp add: stc_def) |
530 apply (simp add: stc_def) |
965 apply (frule stc_part_Ex, safe) |
531 apply (frule stc_part_Ex, safe) |
966 apply (rule someI2) |
532 apply (rule someI2) |
967 apply (auto intro: capprox_sym) |
533 apply (auto intro: approx_sym) |
968 done |
534 done |
969 |
535 |
970 lemma stc_CFinite: "x \<in> CFinite ==> stc x \<in> CFinite" |
536 lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite" |
971 by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]]) |
537 by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]]) |
972 |
538 |
973 lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x" |
539 lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x" |
974 apply (simp add: stc_def) |
540 apply (simp add: stc_def) |
975 apply (rule some_equality) |
541 apply (rule some_equality) |
976 apply (auto intro: SComplex_subset_CFinite [THEN subsetD]) |
542 apply (auto intro: SComplex_subset_HFinite [THEN subsetD]) |
977 apply (blast dest: SComplex_capprox_iff [THEN iffD1]) |
543 apply (blast dest: SComplex_approx_iff [THEN iffD1]) |
978 done |
544 done |
979 |
545 |
980 lemma stc_hcomplex_of_complex: |
546 lemma stc_hcomplex_of_complex: |
981 "stc (hcomplex_of_complex x) = hcomplex_of_complex x" |
547 "stc (hcomplex_of_complex x) = hcomplex_of_complex x" |
982 by auto |
548 by auto |
983 |
549 |
984 lemma stc_eq_capprox: |
550 lemma stc_eq_approx: |
985 "[| x \<in> CFinite; y \<in> CFinite; stc x = stc y |] ==> x @c= y" |
551 "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y" |
986 by (auto dest!: stc_capprox_self elim!: capprox_trans3) |
552 by (auto dest!: stc_approx_self elim!: approx_trans3) |
987 |
553 |
988 lemma capprox_stc_eq: |
554 lemma approx_stc_eq: |
989 "[| x \<in> CFinite; y \<in> CFinite; x @c= y |] ==> stc x = stc y" |
555 "[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y" |
990 by (blast intro: capprox_trans capprox_trans2 SComplex_capprox_iff [THEN iffD1] |
556 by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1] |
991 dest: stc_capprox_self stc_SComplex) |
557 dest: stc_approx_self stc_SComplex) |
992 |
558 |
993 lemma stc_eq_capprox_iff: |
559 lemma stc_eq_approx_iff: |
994 "[| x \<in> CFinite; y \<in> CFinite|] ==> (x @c= y) = (stc x = stc y)" |
560 "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)" |
995 by (blast intro: capprox_stc_eq stc_eq_capprox) |
561 by (blast intro: approx_stc_eq stc_eq_approx) |
996 |
562 |
997 lemma stc_CInfinitesimal_add_SComplex: |
563 lemma stc_Infinitesimal_add_SComplex: |
998 "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(x + e) = x" |
564 "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x" |
999 apply (frule stc_SComplex_eq [THEN subst]) |
565 apply (frule stc_SComplex_eq [THEN subst]) |
1000 prefer 2 apply assumption |
566 prefer 2 apply assumption |
1001 apply (frule SComplex_subset_CFinite [THEN subsetD]) |
567 apply (frule SComplex_subset_HFinite [THEN subsetD]) |
1002 apply (frule CInfinitesimal_subset_CFinite [THEN subsetD]) |
568 apply (frule Infinitesimal_subset_HFinite [THEN subsetD]) |
1003 apply (drule stc_SComplex_eq) |
569 apply (drule stc_SComplex_eq) |
1004 apply (rule capprox_stc_eq) |
570 apply (rule approx_stc_eq) |
1005 apply (auto intro: CFinite_add simp add: CInfinitesimal_add_capprox_self [THEN capprox_sym]) |
571 apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym]) |
1006 done |
572 done |
1007 |
573 |
1008 lemma stc_CInfinitesimal_add_SComplex2: |
574 lemma stc_Infinitesimal_add_SComplex2: |
1009 "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(e + x) = x" |
575 "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x" |
1010 apply (rule add_commute [THEN subst]) |
576 apply (rule add_commute [THEN subst]) |
1011 apply (blast intro!: stc_CInfinitesimal_add_SComplex) |
577 apply (blast intro!: stc_Infinitesimal_add_SComplex) |
1012 done |
578 done |
1013 |
579 |
1014 lemma CFinite_stc_CInfinitesimal_add: |
580 lemma HFinite_stc_Infinitesimal_add: |
1015 "x \<in> CFinite ==> \<exists>e \<in> CInfinitesimal. x = stc(x) + e" |
581 "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e" |
1016 by (blast dest!: stc_capprox_self [THEN capprox_sym] bex_CInfinitesimal_iff2 [THEN iffD2]) |
582 by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) |
1017 |
583 |
1018 lemma stc_add: |
584 lemma stc_add: |
1019 "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
585 "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
1020 apply (frule CFinite_stc_CInfinitesimal_add) |
586 apply (frule HFinite_stc_Infinitesimal_add) |
1021 apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe) |
587 apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe) |
1022 apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))") |
588 apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))") |
1023 apply (drule_tac [2] sym, drule_tac [2] sym) |
589 apply (drule_tac [2] sym, drule_tac [2] sym) |
1024 prefer 2 apply simp |
590 prefer 2 apply simp |
1025 apply (simp (no_asm_simp) add: add_ac) |
591 apply (simp (no_asm_simp) add: add_ac) |
1026 apply (drule stc_SComplex)+ |
592 apply (drule stc_SComplex)+ |
1027 apply (drule SComplex_add, assumption) |
593 apply (drule SComplex_add, assumption) |
1028 apply (drule CInfinitesimal_add, assumption) |
594 apply (drule Infinitesimal_add, assumption) |
1029 apply (rule add_assoc [THEN subst]) |
595 apply (rule add_assoc [THEN subst]) |
1030 apply (blast intro!: stc_CInfinitesimal_add_SComplex2) |
596 apply (blast intro!: stc_Infinitesimal_add_SComplex2) |
1031 done |
597 done |
1032 |
598 |
1033 lemma stc_number_of [simp]: "stc (number_of w) = number_of w" |
599 lemma stc_number_of [simp]: "stc (number_of w) = number_of w" |
1034 by (rule SComplex_number_of [THEN stc_SComplex_eq]) |
600 by (rule SComplex_number_of [THEN stc_SComplex_eq]) |
1035 |
601 |
1126 "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" |
681 "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" |
1127 apply (simp add: st_def stc_def) |
682 apply (simp add: st_def stc_def) |
1128 apply (frule st_part_Ex, safe) |
683 apply (frule st_part_Ex, safe) |
1129 apply (rule someI2) |
684 apply (rule someI2) |
1130 apply (auto intro: approx_sym) |
685 apply (auto intro: approx_sym) |
1131 apply (drule CFinite_HFinite_hcomplex_of_hypreal) |
686 apply (drule HFinite_HFinite_hcomplex_of_hypreal) |
1132 apply (frule stc_part_Ex, safe) |
687 apply (frule stc_part_Ex, safe) |
1133 apply (rule someI2) |
688 apply (rule someI2) |
1134 apply (auto intro: capprox_sym intro!: capprox_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal) |
689 apply (auto intro: approx_sym intro!: approx_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal) |
1135 done |
690 done |
1136 |
691 |
1137 (* |
692 (* |
1138 Goal "x \<in> CFinite ==> hcmod(stc x) = st(hcmod x)" |
693 Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)" |
1139 by (dtac stc_capprox_self 1) |
694 by (dtac stc_approx_self 1) |
1140 by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym])); |
695 by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym])); |
1141 |
696 |
1142 |
697 |
1143 approx_hcmod_add_hcmod |
698 approx_hcmod_add_hcmod |
1144 *) |
699 *) |
1145 |
700 |
1146 lemma CInfinitesimal_hcnj_iff [simp]: |
701 lemma Infinitesimal_hcnj_iff [simp]: |
1147 "(hcnj z \<in> CInfinitesimal) = (z \<in> CInfinitesimal)" |
702 "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)" |
1148 by (simp add: CInfinitesimal_hcmod_iff) |
703 by (simp add: Infinitesimal_hcmod_iff) |
1149 |
704 |
1150 lemma CInfinite_HInfinite_iff: |
705 lemma HInfinite_HInfinite_iff: |
1151 "(star_n X \<in> CInfinite) = |
706 "(star_n X \<in> HInfinite) = |
1152 (star_n (%n. Re(X n)) \<in> HInfinite | |
707 (star_n (%n. Re(X n)) \<in> HInfinite | |
1153 star_n (%n. Im(X n)) \<in> HInfinite)" |
708 star_n (%n. Im(X n)) \<in> HInfinite)" |
1154 by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff) |
709 by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) |
1155 |
710 |
1156 text{*These theorems should probably be deleted*} |
711 text{*These theorems should probably be deleted*} |
1157 lemma hcomplex_split_CInfinitesimal_iff: |
712 lemma hcomplex_split_Infinitesimal_iff: |
1158 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) = |
713 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> Infinitesimal) = |
1159 (x \<in> Infinitesimal & y \<in> Infinitesimal)" |
714 (x \<in> Infinitesimal & y \<in> Infinitesimal)" |
1160 apply (cases x, cases y) |
715 apply (cases x, cases y) |
1161 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff) |
716 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) |
1162 done |
717 done |
1163 |
718 |
1164 lemma hcomplex_split_CFinite_iff: |
719 lemma hcomplex_split_HFinite_iff: |
1165 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) = |
720 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HFinite) = |
1166 (x \<in> HFinite & y \<in> HFinite)" |
721 (x \<in> HFinite & y \<in> HFinite)" |
1167 apply (cases x, cases y) |
722 apply (cases x, cases y) |
1168 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CFinite_HFinite_iff) |
723 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) |
1169 done |
724 done |
1170 |
725 |
1171 lemma hcomplex_split_SComplex_iff: |
726 lemma hcomplex_split_SComplex_iff: |
1172 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) = |
727 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) = |
1173 (x \<in> Reals & y \<in> Reals)" |
728 (x \<in> Reals & y \<in> Reals)" |
1174 apply (cases x, cases y) |
729 apply (cases x, cases y) |
1175 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) |
730 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) |
1176 done |
731 done |
1177 |
732 |
1178 lemma hcomplex_split_CInfinite_iff: |
733 lemma hcomplex_split_HInfinite_iff: |
1179 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) = |
734 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HInfinite) = |
1180 (x \<in> HInfinite | y \<in> HInfinite)" |
735 (x \<in> HInfinite | y \<in> HInfinite)" |
1181 apply (cases x, cases y) |
736 apply (cases x, cases y) |
1182 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CInfinite_HInfinite_iff) |
737 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) |
1183 done |
738 done |
1184 |
739 |
1185 lemma hcomplex_split_capprox_iff: |
740 lemma hcomplex_split_approx_iff: |
1186 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c= |
741 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= |
1187 hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = |
742 hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = |
1188 (x @= x' & y @= y')" |
743 (x @= x' & y @= y')" |
1189 apply (cases x, cases y, cases x', cases y') |
744 apply (cases x, cases y, cases x', cases y') |
1190 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal capprox_approx_iff) |
745 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) |
1191 done |
746 done |
1192 |
747 |
1193 lemma complex_seq_to_hcomplex_CInfinitesimal: |
748 lemma complex_seq_to_hcomplex_Infinitesimal: |
1194 "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==> |
749 "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==> |
1195 star_n X - hcomplex_of_complex x \<in> CInfinitesimal" |
750 star_n X - hcomplex_of_complex x \<in> Infinitesimal" |
1196 apply (simp add: star_n_diff CInfinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff hcmod) |
751 by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) |
1197 apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset) |
752 |
1198 done |
753 lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: |
1199 |
754 "hcomplex_of_hypreal epsilon \<in> Infinitesimal" |
1200 lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]: |
755 by (simp add: Infinitesimal_hcmod_iff) |
1201 "hcomplex_of_hypreal epsilon \<in> CInfinitesimal" |
|
1202 by (simp add: CInfinitesimal_hcmod_iff) |
|
1203 |
756 |
1204 lemma hcomplex_of_complex_approx_zero_iff [simp]: |
757 lemma hcomplex_of_complex_approx_zero_iff [simp]: |
1205 "(hcomplex_of_complex z @c= 0) = (z = 0)" |
758 "(hcomplex_of_complex z @= 0) = (z = 0)" |
1206 by (simp add: star_of_zero [symmetric] del: star_of_zero) |
759 by (simp add: star_of_zero [symmetric] del: star_of_zero) |
1207 |
760 |
1208 lemma hcomplex_of_complex_approx_zero_iff2 [simp]: |
761 lemma hcomplex_of_complex_approx_zero_iff2 [simp]: |
1209 "(0 @c= hcomplex_of_complex z) = (z = 0)" |
762 "(0 @= hcomplex_of_complex z) = (z = 0)" |
1210 by (simp add: star_of_zero [symmetric] del: star_of_zero) |
763 by (simp add: star_of_zero [symmetric] del: star_of_zero) |
1211 |
764 |
1212 end |
765 end |