310 |
310 |
311 lemma approx_unique_complex: |
311 lemma approx_unique_complex: |
312 "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
312 "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
313 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) |
313 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) |
314 |
314 |
315 lemma hcomplex_approxD1: |
315 subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *} |
316 "star_n X @= star_n Y |
316 |
317 ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" |
317 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x" |
318 apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
318 by (induct x) simp |
319 apply (drule approx_minus_iff [THEN iffD1]) |
319 |
320 apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
320 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
321 apply (drule_tac x = m in spec) |
321 by (induct x) simp |
322 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
322 |
323 apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) |
323 lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x" |
324 apply (case_tac "X n") |
324 by transfer (rule abs_Re_le_cmod) |
325 apply (case_tac "Y n") |
325 |
326 apply (auto simp add: complex_diff complex_mod |
326 lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x" |
327 simp del: realpow_Suc) |
327 by transfer (rule abs_Im_le_cmod) |
328 done |
328 |
329 |
329 lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal" |
330 (* same proof *) |
330 apply (rule InfinitesimalI2, simp) |
331 lemma hcomplex_approxD2: |
331 apply (rule order_le_less_trans [OF abs_hRe_le_hcmod]) |
332 "star_n X @= star_n Y |
332 apply (erule (1) InfinitesimalD2) |
333 ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" |
333 done |
334 apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
334 |
335 apply (drule approx_minus_iff [THEN iffD1]) |
335 lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal" |
336 apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
336 apply (rule InfinitesimalI2, simp) |
337 apply (drule_tac x = m in spec) |
337 apply (rule order_le_less_trans [OF abs_hIm_le_hcmod]) |
338 apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
338 apply (erule (1) InfinitesimalD2) |
339 apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) |
339 done |
340 apply (case_tac "X n") |
340 |
341 apply (case_tac "Y n") |
341 lemma real_sqrt_lessI: "\<lbrakk>0 \<le> x; 0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u" |
342 apply (auto simp add: complex_diff complex_mod |
342 by (frule (1) real_sqrt_less_mono) simp |
343 simp del: realpow_Suc) |
343 |
344 done |
344 lemma hypreal_sqrt_lessI: |
345 |
345 "\<And>x u. \<lbrakk>0 \<le> x; 0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u" |
346 lemma hcomplex_approxI: |
346 by transfer (rule real_sqrt_lessI) |
347 "[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); |
347 |
348 star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) |
348 lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x" |
349 |] ==> star_n X @= star_n Y" |
349 by transfer (rule real_sqrt_ge_zero) |
350 apply (drule approx_minus_iff [THEN iffD1]) |
350 |
351 apply (drule approx_minus_iff [THEN iffD1]) |
351 lemma Infinitesimal_sqrt: |
352 apply (rule approx_minus_iff [THEN iffD2]) |
352 "\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal" |
353 apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_diff Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
353 apply (rule InfinitesimalI2) |
354 apply (drule_tac x = "u/2" in spec) |
354 apply (drule_tac r="r\<twosuperior>" in InfinitesimalD2, simp) |
355 apply (drule_tac x = "u/2" in spec, auto, ultra) |
355 apply (simp add: hypreal_sqrt_ge_zero) |
356 apply (case_tac "X x") |
356 apply (rule hypreal_sqrt_lessI, simp_all) |
357 apply (case_tac "Y x") |
357 done |
358 apply (auto simp add: complex_diff complex_mod snd_conv fst_conv numeral_2_eq_2) |
358 |
359 apply (rename_tac a b c d) |
359 lemma Infinitesimal_HComplex: |
360 apply (subgoal_tac "sqrt (abs (a - c) ^ 2 + abs (b - d) ^ 2) < u") |
360 "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal" |
361 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) |
361 apply (rule Infinitesimal_hcmod_iff [THEN iffD2]) |
362 apply (simp add: power2_eq_square) |
362 apply (simp add: hcmod_i) |
363 done |
363 apply (rule Infinitesimal_sqrt) |
364 |
364 apply (rule Infinitesimal_add) |
365 lemma approx_approx_iff: |
365 apply (erule Infinitesimal_hrealpow, simp) |
366 "(star_n X @= star_n Y) = |
366 apply (erule Infinitesimal_hrealpow, simp) |
367 (star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)) & |
367 apply (rule add_nonneg_nonneg) |
368 star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)))" |
368 apply (rule zero_le_power2) |
369 apply (blast intro: hcomplex_approxI hcomplex_approxD1 hcomplex_approxD2) |
369 apply (rule zero_le_power2) |
370 done |
370 done |
|
371 |
|
372 lemma hcomplex_Infinitesimal_iff: |
|
373 "(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)" |
|
374 apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm) |
|
375 apply (drule (1) Infinitesimal_HComplex, simp) |
|
376 done |
|
377 |
|
378 lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y" |
|
379 by transfer (rule complex_Re_diff) |
|
380 |
|
381 lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y" |
|
382 by transfer (rule complex_Im_diff) |
|
383 |
|
384 lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y" |
|
385 unfolding approx_def by (drule Infinitesimal_hRe) simp |
|
386 |
|
387 lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y" |
|
388 unfolding approx_def by (drule Infinitesimal_hIm) simp |
|
389 |
|
390 lemma approx_HComplex: |
|
391 "\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d" |
|
392 unfolding approx_def by (simp add: Infinitesimal_HComplex) |
|
393 |
|
394 lemma hcomplex_approx_iff: |
|
395 "(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)" |
|
396 unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff) |
|
397 |
|
398 lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite" |
|
399 apply (auto simp add: HFinite_def SReal_def) |
|
400 apply (rule_tac x="star_of r" in exI, simp) |
|
401 apply (erule order_le_less_trans [OF abs_hRe_le_hcmod]) |
|
402 done |
|
403 |
|
404 lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite" |
|
405 apply (auto simp add: HFinite_def SReal_def) |
|
406 apply (rule_tac x="star_of r" in exI, simp) |
|
407 apply (erule order_le_less_trans [OF abs_hIm_le_hcmod]) |
|
408 done |
|
409 |
|
410 lemma HFinite_HComplex: |
|
411 "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite" |
|
412 apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp) |
|
413 apply (rule HFinite_add) |
|
414 apply (simp add: HFinite_hcmod_iff hcmod_i) |
|
415 apply (simp add: HFinite_hcmod_iff hcmod_i) |
|
416 done |
|
417 |
|
418 lemma hcomplex_HFinite_iff: |
|
419 "(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)" |
|
420 apply (safe intro!: HFinite_hRe HFinite_hIm) |
|
421 apply (drule (1) HFinite_HComplex, simp) |
|
422 done |
|
423 |
|
424 lemma hcomplex_HInfinite_iff: |
|
425 "(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)" |
|
426 by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff) |
371 |
427 |
372 lemma hcomplex_of_hypreal_approx_iff [simp]: |
428 lemma hcomplex_of_hypreal_approx_iff [simp]: |
373 "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" |
429 "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" |
374 apply (cases x, cases z) |
430 by (simp add: hcomplex_approx_iff) |
375 apply (simp add: hcomplex_of_hypreal approx_approx_iff) |
431 |
376 done |
432 lemma Standard_HComplex: |
377 |
433 "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard" |
378 lemma HFinite_HFinite_Re: |
434 by (simp add: HComplex_def) |
379 "star_n X \<in> HFinite |
|
380 ==> star_n (%n. Re(X n)) \<in> HFinite" |
|
381 apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
|
382 apply (rule_tac x = u in exI, ultra) |
|
383 apply (case_tac "X x") |
|
384 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) |
|
385 apply (rule ccontr, drule linorder_not_less [THEN iffD1]) |
|
386 apply (drule order_less_le_trans, assumption) |
|
387 apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) |
|
388 apply (auto simp add: numeral_2_eq_2 [symmetric]) |
|
389 done |
|
390 |
|
391 lemma HFinite_HFinite_Im: |
|
392 "star_n X \<in> HFinite |
|
393 ==> star_n (%n. Im(X n)) \<in> HFinite" |
|
394 apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
|
395 apply (rule_tac x = u in exI, ultra) |
|
396 apply (case_tac "X x") |
|
397 apply (auto simp add: complex_mod simp del: realpow_Suc) |
|
398 apply (rule ccontr, drule linorder_not_less [THEN iffD1]) |
|
399 apply (drule order_less_le_trans, assumption) |
|
400 apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) |
|
401 done |
|
402 |
|
403 lemma HFinite_Re_Im_HFinite: |
|
404 "[| star_n (%n. Re(X n)) \<in> HFinite; |
|
405 star_n (%n. Im(X n)) \<in> HFinite |
|
406 |] ==> star_n X \<in> HFinite" |
|
407 apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
|
408 apply (rename_tac u v) |
|
409 apply (rule_tac x = "2* (u + v) " in exI) |
|
410 apply ultra |
|
411 apply (case_tac "X x") |
|
412 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) |
|
413 apply (subgoal_tac "0 < u") |
|
414 prefer 2 apply arith |
|
415 apply (subgoal_tac "0 < v") |
|
416 prefer 2 apply arith |
|
417 apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v") |
|
418 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) |
|
419 apply (simp add: power2_eq_square) |
|
420 done |
|
421 |
|
422 lemma HFinite_HFinite_iff: |
|
423 "(star_n X \<in> HFinite) = |
|
424 (star_n (%n. Re(X n)) \<in> HFinite & |
|
425 star_n (%n. Im(X n)) \<in> HFinite)" |
|
426 by (blast intro: HFinite_Re_Im_HFinite HFinite_HFinite_Im HFinite_HFinite_Re) |
|
427 |
|
428 lemma SComplex_Re_SReal: |
|
429 "star_n X \<in> SComplex |
|
430 ==> star_n (%n. Re(X n)) \<in> Reals" |
|
431 apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff) |
|
432 apply (rule_tac x = "Re x" in exI, ultra) |
|
433 done |
|
434 |
|
435 lemma SComplex_Im_SReal: |
|
436 "star_n X \<in> SComplex |
|
437 ==> star_n (%n. Im(X n)) \<in> Reals" |
|
438 apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff) |
|
439 apply (rule_tac x = "Im x" in exI, ultra) |
|
440 done |
|
441 |
|
442 lemma Reals_Re_Im_SComplex: |
|
443 "[| star_n (%n. Re(X n)) \<in> Reals; |
|
444 star_n (%n. Im(X n)) \<in> Reals |
|
445 |] ==> star_n X \<in> SComplex" |
|
446 apply (auto simp add: Standard_def image_def SReal_def star_of_def star_n_eq_iff) |
|
447 apply (rule_tac x = "Complex r ra" in exI, ultra) |
|
448 done |
|
449 |
|
450 lemma SComplex_SReal_iff: |
|
451 "(star_n X \<in> SComplex) = |
|
452 (star_n (%n. Re(X n)) \<in> Reals & |
|
453 star_n (%n. Im(X n)) \<in> Reals)" |
|
454 by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) |
|
455 |
|
456 lemma Infinitesimal_Infinitesimal_iff: |
|
457 "(star_n X \<in> Infinitesimal) = |
|
458 (star_n (%n. Re(X n)) \<in> Infinitesimal & |
|
459 star_n (%n. Im(X n)) \<in> Infinitesimal)" |
|
460 by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) |
|
461 |
|
462 lemma eq_Abs_star_EX: |
|
463 "(\<exists>t. P t) = (\<exists>X. P (star_n X))" |
|
464 by (rule ex_star_eq) |
|
465 |
|
466 lemma eq_Abs_star_Bex: |
|
467 "(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))" |
|
468 by (simp add: Bex_def ex_star_eq) |
|
469 |
435 |
470 (* Here we go - easy proof now!! *) |
436 (* Here we go - easy proof now!! *) |
471 lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" |
437 lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" |
472 apply (cases x) |
438 apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff) |
473 apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) |
439 apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI) |
474 apply (drule st_part_Ex, safe)+ |
440 apply (simp add: st_approx_self [THEN approx_sym]) |
475 apply (rule_tac x = t in star_cases) |
441 apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard]) |
476 apply (rule_tac x = ta in star_cases, auto) |
|
477 apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) |
|
478 apply auto |
|
479 done |
442 done |
480 |
443 |
481 lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" |
444 lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" |
482 apply (drule stc_part_Ex, safe) |
445 apply (drule stc_part_Ex, safe) |
483 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
446 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
635 |
596 |
636 lemma Infinitesimal_hcnj_iff [simp]: |
597 lemma Infinitesimal_hcnj_iff [simp]: |
637 "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)" |
598 "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)" |
638 by (simp add: Infinitesimal_hcmod_iff) |
599 by (simp add: Infinitesimal_hcmod_iff) |
639 |
600 |
640 lemma HInfinite_HInfinite_iff: |
|
641 "(star_n X \<in> HInfinite) = |
|
642 (star_n (%n. Re(X n)) \<in> HInfinite | |
|
643 star_n (%n. Im(X n)) \<in> HInfinite)" |
|
644 by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) |
|
645 |
|
646 text{*These theorems should probably be deleted*} |
|
647 lemma hcomplex_split_Infinitesimal_iff: |
|
648 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> Infinitesimal) = |
|
649 (x \<in> Infinitesimal & y \<in> Infinitesimal)" |
|
650 apply (cases x, cases y) |
|
651 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) |
|
652 done |
|
653 |
|
654 lemma hcomplex_split_HFinite_iff: |
|
655 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HFinite) = |
|
656 (x \<in> HFinite & y \<in> HFinite)" |
|
657 apply (cases x, cases y) |
|
658 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) |
|
659 done |
|
660 |
|
661 lemma hcomplex_split_SComplex_iff: |
|
662 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) = |
|
663 (x \<in> Reals & y \<in> Reals)" |
|
664 apply (cases x, cases y) |
|
665 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) |
|
666 done |
|
667 |
|
668 lemma hcomplex_split_HInfinite_iff: |
|
669 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HInfinite) = |
|
670 (x \<in> HInfinite | y \<in> HInfinite)" |
|
671 apply (cases x, cases y) |
|
672 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) |
|
673 done |
|
674 |
|
675 lemma hcomplex_split_approx_iff: |
|
676 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= |
|
677 hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = |
|
678 (x @= x' & y @= y')" |
|
679 apply (cases x, cases y, cases x', cases y') |
|
680 apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) |
|
681 done |
|
682 |
|
683 lemma complex_seq_to_hcomplex_Infinitesimal: |
|
684 "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==> |
|
685 star_n X - hcomplex_of_complex x \<in> Infinitesimal" |
|
686 by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) |
|
687 |
|
688 lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: |
601 lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: |
689 "hcomplex_of_hypreal epsilon \<in> Infinitesimal" |
602 "hcomplex_of_hypreal epsilon \<in> Infinitesimal" |
690 by (simp add: Infinitesimal_hcmod_iff) |
603 by (simp add: Infinitesimal_hcmod_iff) |
691 |
604 |
692 end |
605 end |