author | paulson |
Thu, 04 Jan 2001 10:23:01 +0100 | |
changeset 10778 | 2c6605049646 |
parent 10751 | a81ea5d3dd41 |
child 10797 | 028d22926a41 |
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 |
||
32 |
"1hr" :: hypreal ("1hr") |
|
33 |
"whr" :: hypreal ("whr") |
|
34 |
"ehr" :: hypreal ("ehr") |
|
35 |
||
36 |
||
37 |
defs |
|
38 |
||
39 |
hypreal_zero_def |
|
40 |
"0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})" |
|
41 |
||
42 |
hypreal_one_def |
|
43 |
"1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})" |
|
44 |
||
45 |
(* an infinite number = [<1,2,3,...>] *) |
|
46 |
omega_def |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
47 |
"whr == Abs_hypreal(hyprel^^{%n::nat. real_of_nat (Suc n)})" |
10751 | 48 |
|
49 |
(* an infinitesimal number = [<1,1/2,1/3,...>] *) |
|
50 |
epsilon_def |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
51 |
"ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_nat (Suc n))})" |
10751 | 52 |
|
53 |
hypreal_minus_def |
|
54 |
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})" |
|
55 |
||
56 |
hypreal_diff_def |
|
57 |
"x - y == x + -(y::hypreal)" |
|
58 |
||
59 |
hypreal_inverse_def |
|
60 |
"inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
|
61 |
hyprel^^{%n. if X n = #0 then #0 else inverse (X n)})" |
|
62 |
||
63 |
hypreal_divide_def |
|
64 |
"P / Q::hypreal == P * inverse Q" |
|
65 |
||
66 |
constdefs |
|
67 |
||
68 |
hypreal_of_real :: real => hypreal |
|
69 |
"hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})" |
|
70 |
||
71 |
defs |
|
72 |
||
73 |
hypreal_add_def |
|
74 |
"P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
|
75 |
hyprel^^{%n::nat. X n + Y n})" |
|
76 |
||
77 |
hypreal_mult_def |
|
78 |
"P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
|
79 |
hyprel^^{%n::nat. X n * Y n})" |
|
80 |
||
81 |
hypreal_less_def |
|
82 |
"P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & |
|
83 |
Y: Rep_hypreal(Q) & |
|
84 |
{n::nat. X n < Y n} : FreeUltrafilterNat" |
|
85 |
hypreal_le_def |
|
86 |
"P <= (Q::hypreal) == ~(Q < P)" |
|
87 |
||
88 |
end |
|
89 |
||
90 |