|
1 (* Title: ZF/Coind/Static.thy |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 Static = BCR + |
|
8 |
|
9 consts |
|
10 ElabRel :: "i" |
|
11 inductive |
|
12 domains "ElabRel" <= "TyEnv * Exp * Ty" |
|
13 intrs |
|
14 elab_constI |
|
15 " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==> \ |
|
16 \ <te,e_const(c),t>:ElabRel " |
|
17 elab_varI |
|
18 " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> \ |
|
19 \ <te,e_var(x),te_app(te,x)>:ElabRel " |
|
20 elab_fnI |
|
21 " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty; \ |
|
22 \ <te_owr(te,x,t1),e,t2>:ElabRel |] ==> \ |
|
23 \ <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel " |
|
24 elab_fixI |
|
25 " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty; \ |
|
26 \ <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==> \ |
|
27 \ <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel " |
|
28 elab_appI |
|
29 " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty; \ |
|
30 \ <te,e1,t_fun(t1,t2)>:ElabRel; \ |
|
31 \ <te,e2,t1>:ElabRel |] ==> \ |
|
32 \ <te,e_app(e1,e2),t2>:ElabRel " |
|
33 type_intrs "te_appI::Exp.intrs@Ty.intrs" |
|
34 |
|
35 end |
|
36 |
|
37 |
|
38 |
|
39 |
|
40 |
|
41 |
|
42 |
|
43 |
|
44 |
|
45 |
|
46 |
|
47 |
|
48 |
|
49 |
|
50 |
|
51 |
|
52 |
|
53 |
|
54 |
|
55 |
|
56 |
|
57 |