|
1 (* Title: ZF/Coind/Dynamic.thy |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 Dynamic = Values + |
|
8 |
|
9 consts |
|
10 EvalRel :: "i" |
|
11 inductive |
|
12 domains "EvalRel" <= "ValEnv * Exp * Val" |
|
13 intrs |
|
14 eval_constI |
|
15 " [| ve:ValEnv; c:Const |] ==> \ |
|
16 \ <ve,e_const(c),v_const(c)>:EvalRel" |
|
17 eval_varI |
|
18 " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==> \ |
|
19 \ <ve,e_var(x),ve_app(ve,x)>:EvalRel" |
|
20 eval_fnI |
|
21 " [| ve:ValEnv; x:ExVar; e:Exp |] ==> \ |
|
22 \ <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel " |
|
23 eval_fixI |
|
24 " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \ |
|
25 \ v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==> \ |
|
26 \ <ve,e_fix(f,x,e),cl>:EvalRel " |
|
27 eval_appI1 |
|
28 " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \ |
|
29 \ <ve,e1,v_const(c1)>:EvalRel; \ |
|
30 \ <ve,e2,v_const(c2)>:EvalRel |] ==> \ |
|
31 \ <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel " |
|
32 eval_appI2 |
|
33 " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \ |
|
34 \ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \ |
|
35 \ <ve,e2,v2>:EvalRel; \ |
|
36 \ <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==> \ |
|
37 \ <ve,e_app(e1,e2),v>:EvalRel " |
|
38 type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs" |
|
39 |
|
40 |
|
41 end |