src/CCL/ex/Nat.thy
changeset 0 a5a9c433f639
child 1149 5750eba8820d
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     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