author | wenzelm |
Mon, 13 Mar 2000 13:21:39 +0100 | |
changeset 8434 | 5e4bba59bfaa |
parent 6071 | 1b2392ac5752 |
child 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
6044
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/ex/Primrec_defs.thy |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
5 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
6 |
Primitive Recursive Functions: preliminary definitions of the constructors |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
7 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
8 |
[These must reside in a separate theory in order to be visible in the |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
9 |
con_defs part of prim_rec's inductive definition.] |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
10 |
*) |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
11 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
12 |
Primrec_defs = Main + |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
13 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
14 |
consts |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
15 |
SC :: i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
16 |
CONST :: i=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
17 |
PROJ :: i=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
18 |
COMP :: [i,i]=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
19 |
PREC :: [i,i]=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
20 |
ACK :: i=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
21 |
ack :: [i,i]=>i |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
22 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
23 |
translations |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
24 |
"ack(x,y)" == "ACK(x) ` [y]" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
25 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
26 |
defs |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
27 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
28 |
SC_def "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
29 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
30 |
CONST_def "CONST(k) == lam l:list(nat).k" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
31 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
32 |
PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
33 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
34 |
COMP_def "COMP(g,fs) == lam l:list(nat). g ` List.map(%f. f`l, fs)" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
35 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
36 |
(*Note that g is applied first to PREC(f,g)`y and then to y!*) |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
37 |
PREC_def "PREC(f,g) == |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
38 |
lam l:list(nat). list_case(0, |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
39 |
%x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" |
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
40 |
|
6071 | 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)]))" |
|
6044
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
45 |
|
e0f9d930e956
Needs separate theory Primrec_defs due to new inductive defs package
paulson
parents:
diff
changeset
|
46 |
end |