equal
deleted
inserted
replaced
|
1 (* Title: ZF/Coind/ECR.thy |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 ECR = Static + Dynamic + |
|
8 |
|
9 (* The extended correspondence relation *) |
|
10 |
|
11 consts |
|
12 HasTyRel :: "i" |
|
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 |
|
19 "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ |
|
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) \ |
|
23 \ |] ==> \ |
|
24 \ <v_clos(x,e,ve),t>:HasTyRel" |
|
25 monos "[Pow_mono]" |
|
26 type_intrs "Val_ValEnv.intrs" |
|
27 |
|
28 (* Pointwise extension to environments *) |
|
29 |
|
30 consts |
|
31 hastyenv :: "[i,i] => o" |
|
32 rules |
|
33 hastyenv_def |
|
34 " hastyenv(ve,te) == \ |
|
35 \ ve_dom(ve) = te_dom(te) & \ |
|
36 \ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)" |
|
37 |
|
38 end |