3335

1 
(* Title: HOL/ex/Primrec


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1997 University of Cambridge


5 


6 
Primitive Recursive Functions


7 


8 
Proof adopted from


9 
Nora Szasz,


10 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,


11 
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317338.


12 


13 
See also E. Mendelson, Introduction to Mathematical Logic.


14 
(Van Nostrand, 1964), page 250, exercise 11.


15 


16 
Demonstrates recursive definitions, the TFL package


17 
*)


18 

6481

19 
Primrec = Main +

3335

20 


21 
consts ack :: "nat * nat => nat"

8703

22 
recdef ack "less_than <*lex*> less_than"

3419

23 
"ack (0,n) = Suc n"

3335

24 
"ack (Suc m,0) = (ack (m, 1))"


25 
"ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"


26 


27 
consts list_add :: nat list => nat

5184

28 
primrec

3335

29 
"list_add [] = 0"


30 
"list_add (m#ms) = m + list_add ms"


31 


32 
consts zeroHd :: nat list => nat

5184

33 
primrec

3335

34 
"zeroHd [] = 0"


35 
"zeroHd (m#ms) = m"


36 


37 


38 
(** The set of primitive recursive functions of type nat list => nat **)


39 
consts


40 
PRIMREC :: (nat list => nat) set


41 
SC :: nat list => nat


42 
CONST :: [nat, nat list] => nat


43 
PROJ :: [nat, nat list] => nat


44 
COMP :: [nat list => nat, (nat list => nat)list, nat list] => nat


45 
PREC :: [nat list => nat, nat list => nat, nat list] => nat


46 


47 
defs


48 


49 
SC_def "SC l == Suc (zeroHd l)"


50 


51 
CONST_def "CONST k l == k"


52 


53 
PROJ_def "PROJ i l == zeroHd (drop i l)"


54 


55 
COMP_def "COMP g fs l == g (map (%f. f l) fs)"


56 


57 
(*Note that g is applied first to PREC f g y and then to y!*)


58 
PREC_def "PREC f g l == case l of


59 
[] => 0


60 
 x#l' => nat_rec (f l') (%y r. g (r#y#l')) x"


61 


62 


63 
inductive PRIMREC


64 
intrs


65 
SC "SC : PRIMREC"


66 
CONST "CONST k : PRIMREC"


67 
PROJ "PROJ i : PRIMREC"


68 
COMP "[ g: PRIMREC; fs: lists PRIMREC ] ==> COMP g fs : PRIMREC"


69 
PREC "[ f: PRIMREC; g: PRIMREC ] ==> PREC f g: PRIMREC"

5717

70 
monos lists_mono

3335

71 


72 
end
