Go backward to C.2 Relations and Functions Go up to C Logic Evaluator Definitions Go forward to C.4 Integer Numbers

C.3 Natural Numbers

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

// we use the builtin type
pred N(x) <=> Nat(x);

// the constructors
fun N0 = 0;
fun '(x: N) = +(x, 1);

// predecessor
fun ^-(x: N) = such(n in nat(0, x): =(x, '(n)), n);

// constants
fun N1 = '(N0);
fun N2 = '(N1);

// addition, multiplication, comparison
fun +N(x: N, y: N) recursive y =
  if(=(y, N0), x, '(+N(x, ^-(y))));
fun *N(x: N, y: N) recursive y =
  if(=(y, N0), N0, +N(x, *N(x, ^-(y))));
pred <=N(x: N, y: N) recursive y <=>
  if(=(x, N0), true, if(=(y, N0), false, <=N(^-(x), ^-(y))));

// difference
fun -N(x: N, y: N) = such(z in nat(0, x): =(x, +N(z, y)), z);

// quotient and remainder
fun divN(x: N, y: N) = 
  such(q in nat(0, x), r in nat(0, ^-(y)): 
    =(x, +N(*N(q, y), r)), q);
fun modN(x: N, y: N) = 
  such(q in nat(0, x), r in nat(0, ^-(y)): 
    =(x, +N(*N(q, y), r)), r);

// exponentiation
fun ^N(x: N, n: N) recursive n =
  if(=(n, N0), N1, *N(x, ^N(x, ^-(n))));

// more notions
pred divides(x, y) <=> exists(z in nat(N0, y): =(*N(x, z), y));
fun gcd(x, y) = 
  let(m = if(=(x, N0), y, x):
    such(z in nat(N0, m): 
      and(divides(z, x), divides(z, y),
        forall(w in nat(+N(z, N1), m):
          or(not(divides(w, x)), not(divides(w, y))))),
      z));
fun lcm(x, y) = such(z in nat(N1, *N(x, y)): 
  and(divides(x, z), divides(y, z),
    forall(w in nat(x, -(z, N1)):
      or(not(divides(x, w)), not(divides(y, w))))),
  z);
pred relprime(x, y) <=> =(gcd(x, y), N1);
pred isprime(x) <=>
  and(not(<=N(x, N1)), 
    forall(y in nat(N0, x):
      implies(divides(y, x), or(=(y, N1), =(y, x)))));

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

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

read natural;

// redefine addition, multiplication, comparison to builtin 
fun +N(x, y) = +(x, y);
fun *N(x, y) = *(x, y);
pred <=N(x, y) <=> <=(x, y);

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