Go backward to C.3 Natural Numbers Go up to C Logic Evaluator Definitions Go 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
// ----------------------------------------------------------------

read set;
read natural0;

// 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 $
// ----------------------------------------------------------------