equal
deleted
inserted
replaced
12 abbreviation |
12 abbreviation |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
14 SComplex :: "hcomplex set" where |
14 SComplex :: "hcomplex set" where |
15 "SComplex \<equiv> Standard" |
15 "SComplex \<equiv> Standard" |
16 |
16 |
17 definition |
17 definition --{* standard part map*} |
18 stc :: "hcomplex => hcomplex" where |
18 stc :: "hcomplex => hcomplex" where |
19 --{* standard part map*} |
19 [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
20 "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
|
21 |
20 |
22 |
21 |
23 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |
22 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |
24 |
23 |
25 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)" |
24 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)" |