equal
deleted
inserted
replaced
7 ECR = Static + Dynamic + |
7 ECR = Static + Dynamic + |
8 |
8 |
9 (* The extended correspondence relation *) |
9 (* The extended correspondence relation *) |
10 |
10 |
11 consts |
11 consts |
12 HasTyRel :: "i" |
12 HasTyRel :: i |
13 coinductive |
13 coinductive |
14 domains "HasTyRel" <= "Val * Ty" |
14 domains "HasTyRel" <= "Val * Ty" |
15 intrs |
15 intrs |
16 htr_constI |
16 htr_constI |
17 "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel" |
17 "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel" |
26 type_intrs "Val_ValEnv.intrs" |
26 type_intrs "Val_ValEnv.intrs" |
27 |
27 |
28 (* Pointwise extension to environments *) |
28 (* Pointwise extension to environments *) |
29 |
29 |
30 consts |
30 consts |
31 hastyenv :: "[i,i] => o" |
31 hastyenv :: [i,i] => o |
32 defs |
32 defs |
33 hastyenv_def |
33 hastyenv_def |
34 " hastyenv(ve,te) == |
34 " hastyenv(ve,te) == |
35 ve_dom(ve) = te_dom(te) & |
35 ve_dom(ve) = te_dom(te) & |
36 (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)" |
36 (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)" |