equal
deleted
inserted
replaced
1 (* Title: ZF/ex/Primrec_defs.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Primitive Recursive Functions: preliminary definitions of the constructors |
|
7 |
|
8 [These must reside in a separate theory in order to be visible in the |
|
9 con_defs part of prim_rec's inductive definition.] |
|
10 *) |
|
11 |
|
12 Primrec_defs = Main + |
|
13 |
|
14 consts |
|
15 SC :: i |
|
16 CONST :: i=>i |
|
17 PROJ :: i=>i |
|
18 COMP :: [i,i]=>i |
|
19 PREC :: [i,i]=>i |
|
20 ACK :: i=>i |
|
21 ack :: [i,i]=>i |
|
22 |
|
23 translations |
|
24 "ack(x,y)" == "ACK(x) ` [y]" |
|
25 |
|
26 defs |
|
27 |
|
28 SC_def "SC == \\<lambda>l \\<in> list(nat).list_case(0, %x xs. succ(x), l)" |
|
29 |
|
30 CONST_def "CONST(k) == \\<lambda>l \\<in> list(nat).k" |
|
31 |
|
32 PROJ_def "PROJ(i) == \\<lambda>l \\<in> list(nat). list_case(0, %x xs. x, drop(i,l))" |
|
33 |
|
34 COMP_def "COMP(g,fs) == \\<lambda>l \\<in> list(nat). g ` List.map(%f. f`l, fs)" |
|
35 |
|
36 (*Note that g is applied first to PREC(f,g)`y and then to y!*) |
|
37 PREC_def "PREC(f,g) == |
|
38 \\<lambda>l \\<in> list(nat). list_case(0, |
|
39 %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" |
|
40 |
|
41 primrec |
|
42 ACK_0 "ACK(0) = SC" |
|
43 ACK_succ "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), |
|
44 COMP(ACK(i), [PROJ(0)]))" |
|
45 |
|
46 end |
|