|
915
|
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
|