Go backward to C.2 Relations and FunctionsGo up to C Logic Evaluator DefinitionsGo 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);

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
// ----------------------------------------------------------------

// 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 \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999