Go backward to C.3 Natural NumbersGo up to C Logic Evaluator DefinitionsGo forward to C.5 Rational Numbers

## C.4 Integer Numbers

```// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// the integer numbers
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------

// integers are pairs of naturals
pred Z(x) <=>
and(Tuple(x), =(2, length(x)), N(.0(x)), N(.1(x)));

// constructor function
fun I(x: N, y: N) =
if(<=N(y, x), tuple(-N(x, y), N0), tuple(N0, -N(y, x)));

// constants
fun Z0 = I(N0, N0);
fun Z1 = I(N1, N0);
fun Z2 = I(N2, N0);

// basic arithmetic
fun +Z(x: Z, y: Z) = I(+N(.0(x), .0(y)), +N(.1(x), .1(y)));
fun *Z(x: Z, y: Z) =
I(+N(*N(.0(x), .0(y)), *N(.1(x), .1(y))),
+N(*N(.0(x), .1(y)), *N(.1(x), .0(y))));
fun -Z(x: Z) = tuple(.1(x), .0(x));
fun -Z(x: Z, y: Z) = +Z(x, -Z(y));

// total order
pred <=Z(x: Z, y: Z) <=> =(.1(-Z(y, x)), N0);

// absolute value and sign
fun ||(x: Z) = if(<=Z(Z0, x), x, -Z(x));
fun sign(x: Z) = if(=(x, Z0), Z0, if(<=Z(Z0, x), Z1, -Z(Z1)));

// the set of integers in interval [-x, x]
fun Z[](x: Z) =
let(y = .0(x):
++(set(z in nat(N0, y): true, tuple(z, N0)),
set(z in nat(N0, y): true, tuple(N0, z))));

// quotient and remainder
fun divZ(x: Z, y: Z) =
such(q in Z[](||(x)), r in  Z[](-Z(||(y), Z1)):
and(=(x, +Z(*Z(q, y), r)),
or(=(sign(r), Z0), =(sign(r), sign(y)))), q);
fun modZ(x: Z, y: Z) =
such(q in Z[](||(x)), r in  Z[](-Z(||(y), Z1)):
and(=(x, +Z(*Z(q, y), r)),
or(=(sign(r), Z0), =(sign(r), sign(y)))), r);

// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999