|
13957
|
1 |
(* Title : NSCA.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 2001,2002 University of Edinburgh
|
|
|
4 |
Description : Infinite, infinitesimal complex number etc!
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
NSCA = NSComplexArith0 +
|
|
|
8 |
|
|
|
9 |
consts
|
|
|
10 |
|
|
|
11 |
(* infinitely close *)
|
|
|
12 |
"@c=" :: [hcomplex,hcomplex] => bool (infixl 50)
|
|
|
13 |
|
|
|
14 |
|
|
|
15 |
constdefs
|
|
|
16 |
(* standard complex numbers reagarded as an embedded subset of NS complex *)
|
|
|
17 |
SComplex :: "hcomplex set"
|
|
|
18 |
"SComplex == {x. EX r. x = hcomplex_of_complex r}"
|
|
|
19 |
|
|
|
20 |
CInfinitesimal :: "hcomplex set"
|
|
|
21 |
"CInfinitesimal == {x. ALL r: Reals. 0 < r --> hcmod x < r}"
|
|
|
22 |
|
|
|
23 |
CFinite :: "hcomplex set"
|
|
|
24 |
"CFinite == {x. EX r: Reals. hcmod x < r}"
|
|
|
25 |
|
|
|
26 |
CInfinite :: "hcomplex set"
|
|
|
27 |
"CInfinite == {x. ALL r: Reals. r < hcmod x}"
|
|
|
28 |
|
|
|
29 |
(* standard part map *)
|
|
|
30 |
stc :: hcomplex => hcomplex
|
|
|
31 |
"stc x == (@r. x : CFinite & r:SComplex & r @c= x)"
|
|
|
32 |
|
|
|
33 |
cmonad :: hcomplex => hcomplex set
|
|
|
34 |
"cmonad x == {y. x @c= y}"
|
|
|
35 |
|
|
|
36 |
cgalaxy :: hcomplex => hcomplex set
|
|
|
37 |
"cgalaxy x == {y. (x - y) : CFinite}"
|
|
|
38 |
|
|
|
39 |
|
|
|
40 |
defs
|
|
|
41 |
|
|
|
42 |
capprox_def "x @c= y == (x - y) : CInfinitesimal"
|
|
|
43 |
|
|
|
44 |
end
|