Go backward to C.11 Modular Arithmetic Go up to C Logic Evaluator Definitions Go forward to C.13 Rationals as Equivalence Classes

C.12 Integers as Equivalence Classes

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

// just consider subset of N x N
fun Z' = set(x in nat(0, 6), y in nat(0, 6): true, tuple(x, y));

// x0-x1 = y0-y1
fun ~Z = set(x in Z', y in Z': 
  =(+N(.0(x), .1(y)), +N(.0(y), .1(x))), tuple(x, y));

// Z as a quotient set
fun Z = /(Z', ~Z);

// selector function
fun _(x) = such(a in x: true, a);

// equivalence class of x
fun []Z(x in Z') = [](x, ~Z);

// constants
fun Z0 = []Z(tuple(N0, N0));
fun Z1 = []Z(tuple(N1, N0));
fun Z2 = []Z(tuple(N2, N0));

// arithmetic
fun +Z(x in Z, y in Z) = 
  []Z(tuple(+N(.0(_(x)), .0(_(y))), +N(.1(_(x)), .1(_(y)))));
fun -Z(x in Z) = []Z(tuple(.1(_(x)), .0(_(x))));
fun -Z(x in Z, y in Z) = 
  []Z(tuple(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x)))));
fun *Z(x in Z, y in Z) = 
  []Z(tuple(+N(*N(.0(_(x)), .0(_(y))), *N(.1(_(x)), .1(_(y)))),
            +N(*N(.0(_(x)), .1(_(y))), *N(.1(_(x)), .0(_(y))))));

// order
pred <=Z(x in Z, y in Z) <=> 
  <=N(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x))));

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