|
1478
|
1 |
(* Title: ZF/Coind/ECR.thy
|
|
915
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Jacob Frost, Cambridge University Computer Laboratory
|
|
915
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
ECR = Static + Dynamic +
|
|
|
8 |
|
|
|
9 |
(* The extended correspondence relation *)
|
|
|
10 |
|
|
|
11 |
consts
|
|
1401
|
12 |
HasTyRel :: i
|
|
915
|
13 |
coinductive
|
|
|
14 |
domains "HasTyRel" <= "Val * Ty"
|
|
|
15 |
intrs
|
|
|
16 |
htr_constI
|
|
|
17 |
"[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
|
|
|
18 |
htr_closI
|
|
1155
|
19 |
"[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
|
|
1478
|
20 |
<te,e_fn(x,e),t>:ElabRel;
|
|
|
21 |
ve_dom(ve) = te_dom(te);
|
|
|
22 |
{<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
|
|
1155
|
23 |
|] ==>
|
|
|
24 |
<v_clos(x,e,ve),t>:HasTyRel"
|
|
915
|
25 |
monos "[Pow_mono]"
|
|
|
26 |
type_intrs "Val_ValEnv.intrs"
|
|
|
27 |
|
|
|
28 |
(* Pointwise extension to environments *)
|
|
|
29 |
|
|
|
30 |
consts
|
|
1401
|
31 |
hastyenv :: [i,i] => o
|
|
930
|
32 |
defs
|
|
915
|
33 |
hastyenv_def
|
|
1478
|
34 |
" hastyenv(ve,te) ==
|
|
|
35 |
ve_dom(ve) = te_dom(te) &
|
|
1155
|
36 |
(ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
|
|
915
|
37 |
|
|
|
38 |
end
|