author | paulson |
Tue, 16 Jan 2001 12:20:52 +0100 | |
changeset 10919 | 144ede948e58 |
parent 10834 | a7897aebbffc |
child 11701 | 3d51fbf81c17 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HOL/Real/Hyperreal/HyperDef.thy |
2 |
ID : $Id$ |
|
3 |
Author : Jacques D. Fleuriot |
|
4 |
Copyright : 1998 University of Cambridge |
|
5 |
Description : Construction of hyperreals using ultrafilters |
|
6 |
*) |
|
7 |
||
8 |
HyperDef = Filter + Real + |
|
9 |
||
10 |
consts |
|
11 |
||
12 |
FreeUltrafilterNat :: nat set set ("\\<U>") |
|
13 |
||
14 |
defs |
|
15 |
||
16 |
FreeUltrafilterNat_def |
|
17 |
"FreeUltrafilterNat == (@U. U : FreeUltrafilter (UNIV:: nat set))" |
|
18 |
||
19 |
||
20 |
constdefs |
|
21 |
hyprel :: "((nat=>real)*(nat=>real)) set" |
|
22 |
"hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & |
|
23 |
{n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
|
24 |
||
25 |
typedef hypreal = "UNIV//hyprel" (Equiv.quotient_def) |
|
26 |
||
27 |
instance |
|
28 |
hypreal :: {ord, zero, plus, times, minus, inverse} |
|
29 |
||
30 |
consts |
|
31 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
32 |
"1hr" :: hypreal ("1hr") |
10751 | 33 |
|
34 |
||
35 |
defs |
|
36 |
||
37 |
hypreal_zero_def |
|
10834 | 38 |
"0 == Abs_hypreal(hyprel``{%n::nat. (#0::real)})" |
10751 | 39 |
|
40 |
hypreal_one_def |
|
10834 | 41 |
"1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})" |
10751 | 42 |
|
43 |
hypreal_minus_def |
|
10834 | 44 |
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
10751 | 45 |
|
46 |
hypreal_diff_def |
|
47 |
"x - y == x + -(y::hypreal)" |
|
48 |
||
49 |
hypreal_inverse_def |
|
50 |
"inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
|
10834 | 51 |
hyprel``{%n. if X n = #0 then #0 else inverse (X n)})" |
10751 | 52 |
|
53 |
hypreal_divide_def |
|
54 |
"P / Q::hypreal == P * inverse Q" |
|
55 |
||
56 |
constdefs |
|
57 |
||
58 |
hypreal_of_real :: real => hypreal |
|
10834 | 59 |
"hypreal_of_real r == Abs_hypreal(hyprel``{%n::nat. r})" |
10751 | 60 |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
61 |
omega :: hypreal (*an infinite number = [<1,2,3,...>] *) |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
62 |
"omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})" |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
63 |
|
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
64 |
epsilon :: hypreal (*an infinitesimal number = [<1,1/2,1/3,...>] *) |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
65 |
"epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})" |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
66 |
|
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
67 |
syntax (xsymbols) |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
68 |
omega :: hypreal ("\\<omega>") |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
69 |
epsilon :: hypreal ("\\<epsilon>") |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
70 |
|
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
71 |
|
10751 | 72 |
defs |
73 |
||
74 |
hypreal_add_def |
|
75 |
"P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
|
10834 | 76 |
hyprel``{%n::nat. X n + Y n})" |
10751 | 77 |
|
78 |
hypreal_mult_def |
|
79 |
"P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
|
10834 | 80 |
hyprel``{%n::nat. X n * Y n})" |
10751 | 81 |
|
82 |
hypreal_less_def |
|
83 |
"P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & |
|
84 |
Y: Rep_hypreal(Q) & |
|
85 |
{n::nat. X n < Y n} : FreeUltrafilterNat" |
|
86 |
hypreal_le_def |
|
87 |
"P <= (Q::hypreal) == ~(Q < P)" |
|
88 |
||
89 |
end |
|
90 |
||
91 |