77 "hexpi = *f* expi" |
77 "hexpi = *f* expi" |
78 |
78 |
79 definition |
79 definition |
80 HComplex :: "[hypreal,hypreal] => hcomplex" where |
80 HComplex :: "[hypreal,hypreal] => hcomplex" where |
81 "HComplex = *f2* Complex" |
81 "HComplex = *f2* Complex" |
82 |
82 (* |
83 definition |
83 definition |
84 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) where |
84 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) where |
85 "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
85 "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
86 |
86 *) |
87 lemmas hcomplex_defs [transfer_unfold] = |
87 lemmas hcomplex_defs [transfer_unfold] = |
88 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
88 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
89 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
89 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def |
90 |
90 |
91 lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard" |
91 lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard" |
92 by (simp add: hcomplex_defs) |
92 by (simp add: hcomplex_defs) |
93 |
93 |
94 lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard" |
94 lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard" |
461 |
461 |
462 |
462 |
463 subsection{*A Few Nonlinear Theorems*} |
463 subsection{*A Few Nonlinear Theorems*} |
464 |
464 |
465 lemma hcomplex_of_hypreal_hyperpow: |
465 lemma hcomplex_of_hypreal_hyperpow: |
466 "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
466 "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) pow n" |
467 by transfer (rule complex_of_real_pow) |
467 by transfer (rule complex_of_real_pow) |
468 |
468 |
469 lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n" |
469 lemma hcmod_hcpow: "!!x n. hcmod(x pow n) = hcmod(x) pow n" |
470 by transfer (rule complex_mod_complexpow) |
470 by transfer (rule complex_mod_complexpow) |
471 |
471 |
472 lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)" |
472 lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)" |
473 by transfer (rule complex_mod_inverse) |
473 by transfer (rule complex_mod_inverse) |
474 |
474 |
496 |
496 |
497 lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n" |
497 lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n" |
498 by transfer (rule norm_power) |
498 by transfer (rule norm_power) |
499 |
499 |
500 lemma hcpow_minus: |
500 lemma hcpow_minus: |
501 "!!x n. (-x::hcomplex) hcpow n = |
501 "!!x n. (-x::hcomplex) pow n = |
502 (if ( *p* even) n then (x hcpow n) else -(x hcpow n))" |
502 (if ( *p* even) n then (x pow n) else -(x pow n))" |
503 by transfer (rule neg_power_if) |
503 by transfer (rule neg_power_if) |
504 |
504 |
505 lemma hcpow_mult: |
505 lemma hcpow_mult: |
506 "!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" |
506 "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)" |
507 by transfer (rule power_mult_distrib) |
507 by transfer (rule power_mult_distrib) |
508 |
508 |
509 lemma hcpow_zero [simp]: "!!n. 0 hcpow (n + 1) = 0" |
509 lemma hcpow_zero2 [simp]: |
510 by transfer simp |
510 "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)" |
511 |
|
512 lemma hcpow_zero2 [simp]: "!!n. 0 hcpow (hSuc n) = 0" |
|
513 by transfer (rule power_0_Suc) |
511 by transfer (rule power_0_Suc) |
514 |
512 |
515 lemma hcpow_not_zero [simp,intro]: |
513 lemma hcpow_not_zero [simp,intro]: |
516 "!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)" |
514 "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)" |
517 by transfer (rule field_power_not_zero) |
515 by (rule hyperpow_not_zero) |
518 |
516 |
519 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
517 lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0" |
520 by (blast intro: ccontr dest: hcpow_not_zero) |
518 by (blast intro: ccontr dest: hcpow_not_zero) |
521 |
519 |
522 subsection{*The Function @{term hsgn}*} |
520 subsection{*The Function @{term hsgn}*} |
523 |
521 |
524 lemma hsgn_zero [simp]: "hsgn 0 = 0" |
522 lemma hsgn_zero [simp]: "hsgn 0 = 0" |
707 "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
705 "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
708 hcis a * hcis (hypreal_of_hypnat n * a)" |
706 hcis a * hcis (hypreal_of_hypnat n * a)" |
709 by transfer (simp add: cis_real_of_nat_Suc_mult) |
707 by transfer (simp add: cis_real_of_nat_Suc_mult) |
710 |
708 |
711 lemma NSDeMoivre_ext: |
709 lemma NSDeMoivre_ext: |
712 "!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
710 "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)" |
713 by transfer (rule DeMoivre) |
711 by transfer (rule DeMoivre) |
714 |
712 |
715 lemma NSDeMoivre2: |
713 lemma NSDeMoivre2: |
716 "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
714 "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
717 apply transfer |
715 apply transfer |
718 apply (fold real_of_nat_def) |
716 apply (fold real_of_nat_def) |
719 apply (rule DeMoivre2) |
717 apply (rule DeMoivre2) |
720 done |
718 done |
721 |
719 |
722 lemma DeMoivre2_ext: |
720 lemma DeMoivre2_ext: |
723 "!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
721 "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
724 by transfer (rule DeMoivre2) |
722 by transfer (rule DeMoivre2) |
725 |
723 |
726 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
724 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
727 by transfer (rule cis_inverse) |
725 by transfer (rule cis_inverse) |
728 |
726 |
739 by (simp add: NSDeMoivre) |
737 by (simp add: NSDeMoivre) |
740 |
738 |
741 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
739 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
742 by (simp add: NSDeMoivre) |
740 by (simp add: NSDeMoivre) |
743 |
741 |
744 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" |
742 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)" |
745 by (simp add: NSDeMoivre_ext) |
743 by (simp add: NSDeMoivre_ext) |
746 |
744 |
747 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
745 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)" |
748 by (simp add: NSDeMoivre_ext) |
746 by (simp add: NSDeMoivre_ext) |
749 |
747 |
750 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
748 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
751 by transfer (rule expi_add) |
749 by transfer (rule expi_add) |
752 |
750 |