|
1048
|
1 |
(* Title: Terms.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Ole Rasmussen
|
|
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Terms = Cube+
|
|
|
9 |
|
|
|
10 |
consts
|
|
1401
|
11 |
lambda :: i
|
|
|
12 |
unmark :: i=>i
|
|
|
13 |
Apl :: [i,i]=>i
|
|
1048
|
14 |
|
|
|
15 |
translations
|
|
|
16 |
"Apl(n,m)" == "App(0,n,m)"
|
|
|
17 |
|
|
|
18 |
inductive
|
|
|
19 |
domains "lambda" <= "redexes"
|
|
|
20 |
intrs
|
|
|
21 |
Lambda_Var " n:nat ==> Var(n):lambda"
|
|
|
22 |
Lambda_Fun " u:lambda ==> Fun(u):lambda"
|
|
|
23 |
Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
|
|
|
24 |
type_intrs "redexes.intrs@bool_typechecks"
|
|
|
25 |
|
|
|
26 |
defs
|
|
1155
|
27 |
unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
|
|
|
28 |
%x m.Fun(m),
|
|
|
29 |
%b x y m p.Apl(m,p))"
|
|
1048
|
30 |
end
|
|
|
31 |
|
|
|
32 |
|