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

C.13 Rationals as Equivalence Classes

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

read equiv;
read integer;

// just consider subset of Z x Z
fun Q' = 
  set(x in Z[](I(3, 0)), y in Z[](I(3, 0)): 
    not(=(y, Z0)), tuple(x, y));

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

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

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

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

// constants
fun Q0 = []Q(tuple(Z0, Z1));
fun Q1 = []Q(tuple(Z1, Z1));
fun Q2 = []Q(tuple(Z2, Z1));

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

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

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