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