35 |
35 |
36 |
36 |
37 defs |
37 defs |
38 |
38 |
39 hypreal_zero_def |
39 hypreal_zero_def |
40 "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})" |
40 "0 == Abs_hypreal(hyprel``{%n::nat. (#0::real)})" |
41 |
41 |
42 hypreal_one_def |
42 hypreal_one_def |
43 "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})" |
43 "1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})" |
44 |
44 |
45 (* an infinite number = [<1,2,3,...>] *) |
45 (* an infinite number = [<1,2,3,...>] *) |
46 omega_def |
46 omega_def |
47 "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})" |
47 "whr == Abs_hypreal(hyprel``{%n::nat. real_of_nat (Suc n)})" |
48 |
48 |
49 (* an infinitesimal number = [<1,1/2,1/3,...>] *) |
49 (* an infinitesimal number = [<1,1/2,1/3,...>] *) |
50 epsilon_def |
50 epsilon_def |
51 "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})" |
51 "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})" |
52 |
52 |
53 hypreal_minus_def |
53 hypreal_minus_def |
54 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})" |
54 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
55 |
55 |
56 hypreal_diff_def |
56 hypreal_diff_def |
57 "x - y == x + -(y::hypreal)" |
57 "x - y == x + -(y::hypreal)" |
58 |
58 |
59 hypreal_inverse_def |
59 hypreal_inverse_def |
60 "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
60 "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
61 hyprel```{%n. if X n = #0 then #0 else inverse (X n)})" |
61 hyprel``{%n. if X n = #0 then #0 else inverse (X n)})" |
62 |
62 |
63 hypreal_divide_def |
63 hypreal_divide_def |
64 "P / Q::hypreal == P * inverse Q" |
64 "P / Q::hypreal == P * inverse Q" |
65 |
65 |
66 constdefs |
66 constdefs |
67 |
67 |
68 hypreal_of_real :: real => hypreal |
68 hypreal_of_real :: real => hypreal |
69 "hypreal_of_real r == Abs_hypreal(hyprel```{%n::nat. r})" |
69 "hypreal_of_real r == Abs_hypreal(hyprel``{%n::nat. r})" |
70 |
70 |
71 defs |
71 defs |
72 |
72 |
73 hypreal_add_def |
73 hypreal_add_def |
74 "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
74 "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
75 hyprel```{%n::nat. X n + Y n})" |
75 hyprel``{%n::nat. X n + Y n})" |
76 |
76 |
77 hypreal_mult_def |
77 hypreal_mult_def |
78 "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
78 "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). |
79 hyprel```{%n::nat. X n * Y n})" |
79 hyprel``{%n::nat. X n * Y n})" |
80 |
80 |
81 hypreal_less_def |
81 hypreal_less_def |
82 "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & |
82 "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & |
83 Y: Rep_hypreal(Q) & |
83 Y: Rep_hypreal(Q) & |
84 {n::nat. X n < Y n} : FreeUltrafilterNat" |
84 {n::nat. X n < Y n} : FreeUltrafilterNat" |