equal
deleted
inserted
replaced
29 |
29 |
30 |
30 |
31 defs |
31 defs |
32 |
32 |
33 real_zero_def |
33 real_zero_def |
34 "0 == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p), |
34 "0 == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p), |
35 preal_of_prat(prat_of_pnat 1p))})" |
35 preal_of_prat(prat_of_pnat 1p))})" |
36 real_one_def |
36 real_one_def |
37 "1r == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p) + |
37 "1r == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p) + |
38 preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" |
38 preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" |
39 |
39 |
40 real_minus_def |
40 real_minus_def |
41 "- R == Abs_real(UN (x,y):Rep_real(R). realrel```{(y,x)})" |
41 "- R == Abs_real(UN (x,y):Rep_real(R). realrel``{(y,x)})" |
42 |
42 |
43 real_diff_def |
43 real_diff_def |
44 "R - (S::real) == R + - S" |
44 "R - (S::real) == R + - S" |
45 |
45 |
46 real_inverse_def |
46 real_inverse_def |
51 |
51 |
52 constdefs |
52 constdefs |
53 |
53 |
54 real_of_preal :: preal => real |
54 real_of_preal :: preal => real |
55 "real_of_preal m == |
55 "real_of_preal m == |
56 Abs_real(realrel```{(m+preal_of_prat(prat_of_pnat 1p), |
56 Abs_real(realrel``{(m+preal_of_prat(prat_of_pnat 1p), |
57 preal_of_prat(prat_of_pnat 1p))})" |
57 preal_of_prat(prat_of_pnat 1p))})" |
58 |
58 |
59 real_of_posnat :: nat => real |
59 real_of_posnat :: nat => real |
60 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
60 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" |
61 |
61 |
64 |
64 |
65 defs |
65 defs |
66 |
66 |
67 real_add_def |
67 real_add_def |
68 "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). |
68 "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). |
69 (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)" |
69 (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)" |
70 |
70 |
71 real_mult_def |
71 real_mult_def |
72 "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). |
72 "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). |
73 (%(x1,y1). (%(x2,y2). realrel```{(x1*x2+y1*y2,x1*y2+x2*y1)}) |
73 (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)}) |
74 p2) p1)" |
74 p2) p1)" |
75 |
75 |
76 real_less_def |
76 real_less_def |
77 "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & |
77 "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & |
78 (x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)" |
78 (x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)" |