|
7218
|
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
|
|
|
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 = "{x::nat=>real. True}/hyprel" (Equiv.quotient_def)
|
|
|
26 |
|
|
|
27 |
instance
|
|
|
28 |
hypreal :: {ord,plus,times,minus}
|
|
|
29 |
|
|
|
30 |
consts
|
|
|
31 |
|
|
|
32 |
"0hr" :: hypreal ("0hr")
|
|
|
33 |
"1hr" :: hypreal ("1hr")
|
|
|
34 |
"whr" :: hypreal ("whr")
|
|
|
35 |
"ehr" :: hypreal ("ehr")
|
|
|
36 |
|
|
|
37 |
|
|
|
38 |
defs
|
|
|
39 |
|
|
|
40 |
hypreal_zero_def "0hr == Abs_hypreal(hyprel^^{%n::nat. 0r})"
|
|
|
41 |
hypreal_one_def "1hr == Abs_hypreal(hyprel^^{%n::nat. 1r})"
|
|
|
42 |
|
|
|
43 |
(* an infinite number = [<1,2,3,...>] *)
|
|
|
44 |
omega_def "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
|
|
|
45 |
|
|
|
46 |
(* an infinitesimal number = [<1,1/2,1/3,...>] *)
|
|
|
47 |
epsilon_def "ehr == Abs_hypreal(hyprel^^{%n::nat. rinv(real_of_posnat n)})"
|
|
|
48 |
|
|
|
49 |
hypreal_minus_def
|
|
|
50 |
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
|
|
|
51 |
|
|
|
52 |
hypreal_diff_def
|
|
|
53 |
"x - y == x + -(y::hypreal)"
|
|
|
54 |
|
|
|
55 |
constdefs
|
|
|
56 |
|
|
|
57 |
hypreal_of_real :: real => hypreal ("&# _" [80] 80)
|
|
|
58 |
"hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})"
|
|
|
59 |
|
|
|
60 |
hrinv :: hypreal => hypreal
|
|
|
61 |
"hrinv(P) == Abs_hypreal(UN X: Rep_hypreal(P).
|
|
|
62 |
hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})"
|
|
|
63 |
|
|
|
64 |
(* n::nat --> (n+1)::hypreal *)
|
|
|
65 |
hypreal_of_posnat :: nat => hypreal ("&&# _" [80] 80)
|
|
|
66 |
"hypreal_of_posnat n == (hypreal_of_real(real_of_preal
|
|
|
67 |
(preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
|
|
|
68 |
|
|
|
69 |
hypreal_of_nat :: nat => hypreal ("&&## _" [80] 80)
|
|
|
70 |
"hypreal_of_nat n == hypreal_of_posnat n + -1hr"
|
|
|
71 |
|
|
|
72 |
defs
|
|
|
73 |
|
|
|
74 |
hypreal_add_def
|
|
|
75 |
"P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
|
|
|
76 |
hyprel^^{%n::nat. X n + Y n})"
|
|
|
77 |
|
|
|
78 |
hypreal_mult_def
|
|
|
79 |
"P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
|
|
|
80 |
hyprel^^{%n::nat. X n * Y n})"
|
|
|
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 |
|