Go backward to C.10 Equivalence Relations Go up to C Logic Evaluator Definitions Go forward to C.12 Integers as Equivalence Classes |
// ---------------------------------------------------------------- // $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 $ // ----------------------------------------------------------------