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