equal
deleted
inserted
replaced
|
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 |