|
1048
|
1 |
(* Title: Redex.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Ole Rasmussen
|
|
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Redex = Univ +
|
|
|
9 |
consts
|
|
|
10 |
redexes :: "i"
|
|
|
11 |
|
|
|
12 |
datatype
|
|
|
13 |
"redexes" = Var ("n: nat")
|
|
|
14 |
| Fun ("t: redexes")
|
|
|
15 |
| App ("b:bool" ,"f:redexes" , "a:redexes")
|
|
|
16 |
type_intrs "[bool_into_univ]"
|
|
|
17 |
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
redex_rec :: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i"
|
|
|
21 |
|
|
|
22 |
defs
|
|
|
23 |
redex_rec_def
|
|
|
24 |
"redex_rec(p,b,c,d) == \
|
|
|
25 |
\ Vrec(p, %p g.redexes_case(b, %x.c(x,g`x), \
|
|
|
26 |
\ %n x y.d(n, x, y, g`x, g`y), p))"
|
|
|
27 |
end
|
|
|
28 |
|