This file provides a classical axiomatization of real numbers as a
discrete real archimedean field with in particular a theory of floor and
ceil.
realType == type of real numbers
sup A == where A : set R with R : realType, the supremum of A when
it exists, 0 otherwise
inf A := - sup (- A)
The mixin corresponding to realType extends an archiFieldType with two
properties:
Rint == the set of real numbers that can be written as z%:~R,
i.e., as an integer
Rtoint r == r when r is an integer, 0 otherwise
floor_set x := [set y | Rtoint y /\ y <= x]
Rfloor x == the floor of x as a real number
floor x == the floor of x as an integer (type int)
range1 x := [set y |x <= y < x + 1]
Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x)
ceil x := - floor (- x)