equal
deleted
inserted
replaced
13 |
13 |
14 typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def) |
14 typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def) |
15 |
15 |
16 |
16 |
17 instance |
17 instance |
18 real :: {ord, plus, times, minus} |
18 real :: {ord, zero, plus, times, minus} |
19 |
19 |
20 consts |
20 consts |
21 |
21 |
22 "0r" :: real ("0r") |
|
23 "1r" :: real ("1r") |
22 "1r" :: real ("1r") |
24 |
23 |
25 defs |
24 defs |
26 |
25 |
27 real_zero_def |
26 real_zero_def |
28 "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), |
27 "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), |
29 preal_of_prat(prat_of_pnat 1p))})" |
28 preal_of_prat(prat_of_pnat 1p))})" |
30 real_one_def |
29 real_one_def |
31 "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + |
30 "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + |
32 preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" |
31 preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" |
33 |
32 |
42 "real_of_preal m == |
41 "real_of_preal m == |
43 Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p), |
42 Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p), |
44 preal_of_prat(prat_of_pnat 1p))})" |
43 preal_of_prat(prat_of_pnat 1p))})" |
45 |
44 |
46 rinv :: real => real |
45 rinv :: real => real |
47 "rinv(R) == (@S. R ~= 0r & S*R = 1r)" |
46 "rinv(R) == (@S. R ~= 0 & S*R = 1r)" |
48 |
47 |
49 real_of_posnat :: nat => real |
48 real_of_posnat :: nat => real |
50 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
49 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
51 |
50 |
52 real_of_nat :: nat => real |
51 real_of_nat :: nat => real |