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