equal
deleted
inserted
replaced
1 (* Title : NSA.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Infinite numbers, Infinitesimals, |
|
5 infinitely close relation etc. |
|
6 *) |
|
7 |
|
8 NSA = HRealAbs + RComplete + |
|
9 |
|
10 constdefs |
|
11 |
|
12 (* standard real numbers reagarded as *) |
|
13 (* an embedded subset of hyperreals *) |
|
14 SReal :: "hypreal set" |
|
15 "SReal == {x. EX r. x = hypreal_of_real r}" |
|
16 |
|
17 Infinitesimal :: "hypreal set" |
|
18 "Infinitesimal == {x. ALL r: SReal. 0 < r --> abs x < r}" |
|
19 |
|
20 HFinite :: "hypreal set" |
|
21 "HFinite == {x. EX r: SReal. abs x < r}" |
|
22 |
|
23 HInfinite :: "hypreal set" |
|
24 "HInfinite == {x. ALL r: SReal. r < abs x}" |
|
25 |
|
26 consts |
|
27 |
|
28 (* standard part map *) |
|
29 st :: hypreal => hypreal |
|
30 |
|
31 (* infinitely close *) |
|
32 "@=" :: [hypreal,hypreal] => bool (infixl 50) |
|
33 |
|
34 monad :: hypreal => hypreal set |
|
35 galaxy :: hypreal => hypreal set |
|
36 |
|
37 defs |
|
38 |
|
39 inf_close_def "x @= y == (x + -y) : Infinitesimal" |
|
40 st_def "st == (%x. @r. x : HFinite & r:SReal & r @= x)" |
|
41 |
|
42 monad_def "monad x == {y. x @= y}" |
|
43 galaxy_def "galaxy x == {y. (x + -y) : HFinite}" |
|
44 |
|
45 end |
|
46 |
|
47 |
|
48 |
|
49 |
|