17456

1 
(* Title: CCL/ex/Nat.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 
*)


6 

17456

7 
header {* Programs defined over the natural numbers *}


8 


9 
theory Nat


10 
imports Wfd


11 
begin

0

12 


13 
consts


14 

17456

15 
not :: "i=>i"


16 
"#+" :: "[i,i]=>i" (infixr 60)


17 
"#*" :: "[i,i]=>i" (infixr 60)


18 
"#" :: "[i,i]=>i" (infixr 60)


19 
"##" :: "[i,i]=>i" (infixr 60)


20 
"#<" :: "[i,i]=>i" (infixr 60)


21 
"#<=" :: "[i,i]=>i" (infixr 60)


22 
ackermann :: "[i,i]=>i"

0

23 

17456

24 
defs

0

25 

17456

26 
not_def: "not(b) == if b then false else true"

0

27 

17456

28 
add_def: "a #+ b == nrec(a,b,%x g. succ(g))"


29 
mult_def: "a #* b == nrec(a,zero,%x g. b #+ g)"


30 
sub_def: "a # b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))

1149

31 
in sub(a,b)"

17456

32 
le_def: "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))

1149

33 
in le(a,b)"

17456

34 
lt_def: "a #< b == not(b #<= a)"

0

35 

17456

36 
div_def: "a ## b == letrec div x y be if x #< y then zero else succ(div(x#y,y))

1149

37 
in div(a,b)"

17456

38 
ack_def:


39 
"ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.

3837

40 
ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))

1149

41 
in ack(a,b)"

0

42 

17456

43 
ML {* use_legacy_bindings (the_context ()) *}


44 

0

45 
end


46 
