src/ZF/ex/Primrec0.thy
 author lcp Tue Aug 16 18:58:42 1994 +0200 (1994-08-16) changeset 532 851df239ac8b parent 71 729fe026c5f3 permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
 lcp@16 1 (* Title: ZF/ex/primrec.thy lcp@16 2 ID: \$Id\$ lcp@16 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory lcp@16 4 Copyright 1993 University of Cambridge lcp@16 5 lcp@16 6 Primitive Recursive Functions lcp@16 7 lcp@16 8 Proof adopted from lcp@16 9 Nora Szasz, lcp@16 10 A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, lcp@16 11 In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. lcp@71 12 lcp@71 13 See also E. Mendelson, Introduction to Mathematical Logic. lcp@71 14 (Van Nostrand, 1964), page 250, exercise 11. lcp@16 15 *) lcp@16 16 lcp@16 17 Primrec0 = ListFn + lcp@16 18 consts lcp@16 19 SC :: "i" lcp@16 20 CONST :: "i=>i" lcp@16 21 PROJ :: "i=>i" lcp@16 22 COMP :: "[i,i]=>i" lcp@16 23 PREC :: "[i,i]=>i" lcp@16 24 primrec :: "i" lcp@16 25 ACK :: "i=>i" lcp@16 26 ack :: "[i,i]=>i" lcp@16 27 lcp@16 28 translations lcp@16 29 "ack(x,y)" == "ACK(x) ` [y]" lcp@16 30 lcp@16 31 rules lcp@16 32 lcp@16 33 SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)" lcp@16 34 lcp@16 35 CONST_def "CONST(k) == lam l:list(nat).k" lcp@16 36 lcp@16 37 PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))" lcp@16 38 lcp@16 39 COMP_def "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)" lcp@16 40 lcp@16 41 (*Note that g is applied first to PREC(f,g)`y and then to y!*) lcp@16 42 PREC_def "PREC(f,g) == \ lcp@16 43 \ lam l:list(nat). list_case(0, \ lcp@16 44 \ %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" lcp@16 45 lcp@16 46 ACK_def "ACK(i) == rec(i, SC, \ lcp@16 47 \ %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))" lcp@16 48 lcp@16 49 end