An ordered type of finite values, extended with positive and negative infinites as well as successor and predecessor functions to represent strict lower and upper bounds.
Negative and positive infinites are used to represent half-planes as intervals; we require that all values are larger than the negative infinite and smaller than the positive infinite.
Values of the form x + \epsilon and x - \epsilon are used to transform open bounds in the finite type into closed bounds on the extended type t, with the equivalence:
y <= x - \epsilon \Leftrightarrow y < x
and
x + \epsilon <= y \Leftrightarrow y < x
This signature does not expose x + \epsilon and x - \epsilon values directly; instead, we use \mathrm{succ} and \mathrm{pred} functions which can be thought of as addition and subtraction of \epsilon, respectively.
The comparison function on extended values is an extension of the regular order on finite values.
val view : t -> finite Intervals_intf.boundview t converts the internal representation to a bound for examination.
val minfty : tminfty is an extended value -\infty such that for any extended value x, -\infty \le x.
Finite values are included in t. We will identify a finite value in finite and its representation in t.
val pinfty : tpinfty is an extended value +\infty such that for any extended value x, x \le +\infty.
Each element of the ordered type t has a successor. The successor of an element is always greater than the element itself:
\forall x, x \le \mathrm{succ}(x)
We say that x is a finite upper bound if it is strictly smaller than its successor, i.e. if x < \mathrm{succ}(x), and we require that all finite values are finite upper bounds (however there may be finite upper bounds that are not finite values).
succ must be the inverse of pred below.
Each element of the ordered type t has a predecessor. The predecessor of an element is always smaller than the element itself:
\forall x, \mathrm{pred}(x) \le x
We say that x is a finite lower bound if it is strictly greater than its predecessor, i.e. if \mathrm{pred}(x) < x, and we require that all finite values are finite lower bounds (however there may be finite lower bounds that are not finite values).
pred must be the inverse of succ above.