Numerals and simprocs for types real and hypreal. The abstract
constants 0, 1 and binary numerals work harmoniously.
1 (* Title : Real/RealDef.thy
3 Author : Jacques D. Fleuriot
4 Copyright : 1998 University of Cambridge
5 Description : The reals
10 instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
14 realrel :: "((preal * preal) * (preal * preal)) set"
15 "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
18 real = "UNIV//realrel" (Equiv.quotient_def)
22 real :: {ord, zero, one, plus, times, minus, inverse}
25 (*Overloaded constants denoting the Nat and Real subsets of enclosing
26 types such as hypreal and complex*)
27 Nats, Reals :: "'a set"
29 (*overloaded constant for injecting other types into "real"*)
36 "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1),
37 preal_of_prat(prat_of_pnat 1))})"
40 "1 == Abs_REAL(realrel``
41 {(preal_of_prat(prat_of_pnat 1) + preal_of_prat(prat_of_pnat 1),
42 preal_of_prat(prat_of_pnat 1))})"
45 "- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})"
48 "R - (S::real) == R + - S"
51 "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
54 "R / (S::real) == R * inverse S"
58 (** these don't use the overloaded "real" function: users don't see them **)
60 real_of_preal :: preal => real
62 Abs_REAL(realrel``{(m + preal_of_prat(prat_of_pnat 1),
63 preal_of_prat(prat_of_pnat 1))})"
65 real_of_posnat :: nat => real
66 "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
72 real_of_nat_def "real n == real_of_posnat n + (- 1)"
75 "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
76 (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
79 "P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
80 (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
84 "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
85 (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
87 "P <= (Q::real) == ~(Q < P)"
90 Reals :: "'a set" ("\\<real>")
91 Nats :: "'a set" ("\\<nat>")