Go backward to C.10 Equivalence Relations Go up to C Logic Evaluator Definitions Go forward to C.12 Integers as Equivalence Classes

C.11 Modular Arithmetic

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

read integer;
read equiv;

// positive integers
pred Z+(x) <=> and(Z(x), =(sign(x), Z1));

// just consider subset of Z
fun Z' = Z[](I(5, 0));

// x = y mod m
fun =m(m: Z+) =
  set(x in Z', y in Z': =(modZ(x, m), modZ(y, m)), tuple(x, y));

// Z_m
fun Z(m: Z+) = /(Z', =m(m));

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

// equivalence class of x modulo m
fun []m(m: Z+, x: Z) = [](x, =m(m));

// modular arithmetic
fun +m(m: Z+, x in Z(m), y in Z(m)) = []m(m, +Z(_(x), _(y)));
fun -m(m: Z+, x in Z(m), y in Z(m)) = []m(m, -Z(_(x), _(y)));
fun -m(m: Z+, x in Z(m))            = []m(m, -Z(_(x)));
fun *m(m: Z+, x in Z(m), y in Z(m)) = []m(m, *Z(_(x), _(y)));

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