equal
deleted
inserted
replaced
31 |
31 |
32 |
32 |
33 defs |
33 defs |
34 |
34 |
35 real_zero_def |
35 real_zero_def |
36 "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p), |
36 "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1), |
37 preal_of_prat(prat_of_pnat 1p))})" |
37 preal_of_prat(prat_of_pnat 1))})" |
|
38 |
38 real_one_def |
39 real_one_def |
39 "1 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p) + |
40 "1 == Abs_REAL(realrel`` |
40 preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" |
41 {(preal_of_prat(prat_of_pnat 1) + preal_of_prat(prat_of_pnat 1), |
|
42 preal_of_prat(prat_of_pnat 1))})" |
41 |
43 |
42 real_minus_def |
44 real_minus_def |
43 "- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})" |
45 "- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})" |
44 |
46 |
45 real_diff_def |
47 real_diff_def |
51 real_divide_def |
53 real_divide_def |
52 "R / (S::real) == R * inverse S" |
54 "R / (S::real) == R * inverse S" |
53 |
55 |
54 constdefs |
56 constdefs |
55 |
57 |
56 (** these don't use the overloaded real because users don't see them **) |
58 (** these don't use the overloaded "real" function: users don't see them **) |
57 |
59 |
58 real_of_preal :: preal => real |
60 real_of_preal :: preal => real |
59 "real_of_preal m == |
61 "real_of_preal m == |
60 Abs_REAL(realrel``{(m+preal_of_prat(prat_of_pnat 1p), |
62 Abs_REAL(realrel``{(m + preal_of_prat(prat_of_pnat 1), |
61 preal_of_prat(prat_of_pnat 1p))})" |
63 preal_of_prat(prat_of_pnat 1))})" |
62 |
64 |
63 real_of_posnat :: nat => real |
65 real_of_posnat :: nat => real |
64 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
66 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
65 |
67 |
66 |
68 |