1 (* Title: CCL/ex/nat.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Programs defined over the natural numbers |
|
7 *) |
|
8 |
|
9 Nat = Wfd + |
|
10 |
|
11 consts |
|
12 |
|
13 not :: "i=>i" |
|
14 "#+","#*","#-", |
|
15 "##","#<","#<=" :: "[i,i]=>i" (infixr 60) |
|
16 ackermann :: "[i,i]=>i" |
|
17 |
|
18 rules |
|
19 |
|
20 not_def "not(b) == if b then false else true" |
|
21 |
|
22 add_def "a #+ b == nrec(a,b,%x g.succ(g))" |
|
23 mult_def "a #* b == nrec(a,zero,%x g.b #+ g)" |
|
24 sub_def "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) \ |
|
25 \ in sub(a,b)" |
|
26 le_def "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) \ |
|
27 \ in le(a,b)" |
|
28 lt_def "a #< b == not(b #<= a)" |
|
29 |
|
30 div_def "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) \ |
|
31 \ in div(a,b)" |
|
32 ack_def |
|
33 "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. \ |
|
34 \ ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))\ |
|
35 \ in ack(a,b)" |
|
36 |
|
37 end |
|
38 |
|