8 NSA = HRealAbs + RComplete + |
8 NSA = HRealAbs + RComplete + |
9 |
9 |
10 constdefs |
10 constdefs |
11 |
11 |
12 Infinitesimal :: "hypreal set" |
12 Infinitesimal :: "hypreal set" |
13 "Infinitesimal == {x. ALL r: SReal. 0 < r --> abs x < r}" |
13 "Infinitesimal == {x. ALL r: Reals. 0 < r --> abs x < r}" |
14 |
14 |
15 HFinite :: "hypreal set" |
15 HFinite :: "hypreal set" |
16 "HFinite == {x. EX r: SReal. abs x < r}" |
16 "HFinite == {x. EX r: Reals. abs x < r}" |
17 |
17 |
18 HInfinite :: "hypreal set" |
18 HInfinite :: "hypreal set" |
19 "HInfinite == {x. ALL r: SReal. r < abs x}" |
19 "HInfinite == {x. ALL r: Reals. r < abs x}" |
20 |
20 |
21 (* standard part map *) |
21 (* standard part map *) |
22 st :: hypreal => hypreal |
22 st :: hypreal => hypreal |
23 "st == (%x. @r. x : HFinite & r:SReal & r @= x)" |
23 "st == (%x. @r. x : HFinite & r:Reals & r @= x)" |
24 |
24 |
25 monad :: hypreal => hypreal set |
25 monad :: hypreal => hypreal set |
26 "monad x == {y. x @= y}" |
26 "monad x == {y. x @= y}" |
27 |
27 |
28 galaxy :: hypreal => hypreal set |
28 galaxy :: hypreal => hypreal set |
29 "galaxy x == {y. (x + -y) : HFinite}" |
29 "galaxy x == {y. (x + -y) : HFinite}" |
30 |
30 |
31 (* infinitely close *) |
31 (* infinitely close *) |
32 inf_close :: "[hypreal, hypreal] => bool" (infixl "@=" 50) |
32 approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50) |
33 "x @= y == (x + -y) : Infinitesimal" |
33 "x @= y == (x + -y) : Infinitesimal" |
34 |
34 |
35 |
35 |
36 defs |
36 defs |
37 |
37 |
38 (*standard real numbers as a subset of the hyperreals*) |
38 (*standard real numbers as a subset of the hyperreals*) |
39 SReal_def "SReal == {x. EX r. x = hypreal_of_real r}" |
39 SReal_def "Reals == {x. EX r. x = hypreal_of_real r}" |
40 |
40 |
41 syntax (symbols) |
41 syntax (symbols) |
42 inf_close :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50) |
42 approx :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50) |
43 |
43 |
44 end |
44 end |
45 |
45 |
46 |
46 |
47 |
47 |