equal
deleted
inserted
replaced
15 |
15 |
16 abbreviation |
16 abbreviation |
17 hcomplex_of_complex :: "complex => complex star" |
17 hcomplex_of_complex :: "complex => complex star" |
18 "hcomplex_of_complex == star_of" |
18 "hcomplex_of_complex == star_of" |
19 |
19 |
|
20 hcmod :: "complex star => real star" |
|
21 "hcmod == hnorm" |
|
22 |
20 definition |
23 definition |
21 |
24 |
22 (*--- real and Imaginary parts ---*) |
25 (*--- real and Imaginary parts ---*) |
23 |
26 |
24 hRe :: "hcomplex => hypreal" |
27 hRe :: "hcomplex => hypreal" |
25 "hRe = *f* Re" |
28 "hRe = *f* Re" |
26 |
29 |
27 hIm :: "hcomplex => hypreal" |
30 hIm :: "hcomplex => hypreal" |
28 "hIm = *f* Im" |
31 "hIm = *f* Im" |
29 |
32 |
30 |
|
31 (*----------- modulus ------------*) |
|
32 |
|
33 hcmod :: "hcomplex => hypreal" |
|
34 "hcmod = *f* cmod" |
|
35 |
33 |
36 (*------ imaginary unit ----------*) |
34 (*------ imaginary unit ----------*) |
37 |
35 |
38 iii :: hcomplex |
36 iii :: hcomplex |
39 "iii = star_of ii" |
37 "iii = star_of ii" |
74 |
72 |
75 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) |
73 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) |
76 "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
74 "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
77 |
75 |
78 lemmas hcomplex_defs [transfer_unfold] = |
76 lemmas hcomplex_defs [transfer_unfold] = |
79 hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def |
77 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
80 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
78 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
|
79 |
|
80 lemma hcmod_def: "hcmod = *f* cmod" |
|
81 by (rule hnorm_def) |
81 |
82 |
82 |
83 |
83 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
84 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
84 |
85 |
85 lemma hRe: "hRe (star_n X) = star_n (%n. Re(X n))" |
86 lemma hRe: "hRe (star_n X) = star_n (%n. Re(X n))" |