1(* Title: ZF/Coind/Static.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4*) 5 6theory Static imports Values Types begin 7 8(*** Basic correspondence relation -- not completely specified, as it is a 9 parameter of the proof. A concrete version could be defined inductively. 10***) 11 12axiomatization isof :: "[i,i] => o" 13 where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)" 14 15(*Its extension to environments*) 16 17definition 18 isofenv :: "[i,i] => o" where 19 "isofenv(ve,te) == 20 ve_dom(ve) = te_dom(te) & 21 (\<forall>x \<in> ve_dom(ve). 22 \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))" 23 24 25(*** Elaboration ***) 26 27consts ElabRel :: i 28 29inductive 30 domains "ElabRel" \<subseteq> "TyEnv * Exp * Ty" 31 intros 32 constI [intro!]: 33 "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==> 34 <te,e_const(c),t> \<in> ElabRel" 35 varI [intro!]: 36 "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> 37 <te,e_var(x),te_app(te,x)> \<in> ElabRel" 38 fnI [intro!]: 39 "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; 40 <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==> 41 <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel" 42 fixI [intro!]: 43 "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty; 44 <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==> 45 <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel" 46 appI [intro]: 47 "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; 48 <te,e1,t_fun(t1,t2)> \<in> ElabRel; 49 <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel" 50 type_intros te_appI Exp.intros Ty.intros 51 52 53inductive_cases 54 elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel" 55 and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel" 56 and elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel" 57 and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel" 58 and elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel" 59 60declare ElabRel.dom_subset [THEN subsetD, dest] 61 62end 63 64 65 66 67 68 69 70