|
1478
|
1 |
(* Title: Terms.thy
|
|
1048
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Ole Rasmussen
|
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Terms = Cube+
|
|
|
9 |
|
|
|
10 |
consts
|
|
1478
|
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
|
|
11319
|
21 |
Lambda_Var " n \\<in> nat ==> Var(n):lambda"
|
|
|
22 |
Lambda_Fun " u \\<in> lambda ==> Fun(u):lambda"
|
|
|
23 |
Lambda_App "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
|
|
1478
|
24 |
type_intrs "redexes.intrs@bool_typechecks"
|
|
1048
|
25 |
|
|
6046
|
26 |
primrec
|
|
|
27 |
"unmark(Var(n)) = Var(n)"
|
|
|
28 |
"unmark(Fun(u)) = Fun(unmark(u))"
|
|
|
29 |
"unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
|
|
|
30 |
|
|
1048
|
31 |
end
|
|
|
32 |
|
|
|
33 |
|