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