|
1 (* Title: ZF/ex/Primrec.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Primitive Recursive Functions: the inductive definition |
|
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), 317-338. |
|
12 |
|
13 See also E. Mendelson, Introduction to Mathematical Logic. |
|
14 (Van Nostrand, 1964), page 250, exercise 11. |
|
15 *) |
|
16 |
|
17 Primrec = Primrec_defs + |
|
18 consts |
|
19 prim_rec :: i |
|
20 |
|
21 inductive |
|
22 domains "prim_rec" <= "list(nat)->nat" |
|
23 intrs |
|
24 SC "SC \\<in> prim_rec" |
|
25 CONST "k \\<in> nat ==> CONST(k) \\<in> prim_rec" |
|
26 PROJ "i \\<in> nat ==> PROJ(i) \\<in> prim_rec" |
|
27 COMP "[| g \\<in> prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec" |
|
28 PREC "[| f \\<in> prim_rec; g \\<in> prim_rec |] ==> PREC(f,g): prim_rec" |
|
29 monos list_mono |
|
30 con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def |
|
31 type_intrs "nat_typechecks @ list.intrs @ |
|
32 [lam_type, list_case_type, drop_type, map_type, |
|
33 apply_type, rec_type]" |
|
34 |
|
35 end |