1(* Title: ZF/Coind/Values.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4*) 5 6theory Values imports Language Map begin 7 8(* Values, values environments and associated operators *) 9 10consts 11 Val :: i 12 ValEnv :: i 13 Val_ValEnv :: i 14 15codatatype 16 "Val" = v_const ("c \<in> Const") 17 | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv") 18 and 19 "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)") 20 monos PMap_mono 21 type_intros A_into_univ mapQU 22 23consts 24 ve_owr :: "[i,i,i] => i" 25 ve_dom :: "i=>i" 26 ve_app :: "[i,i] => i" 27 28 29primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))" 30 31primrec "ve_dom(ve_mk(m)) = domain(m)" 32 33primrec "ve_app(ve_mk(m), a) = map_app(m,a)" 34 35definition 36 ve_emp :: i where 37 "ve_emp == ve_mk(map_emp)" 38 39 40(* Elimination rules *) 41 42lemma ValEnvE: 43 "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q" 44apply (unfold Part_def Val_def ValEnv_def, clarify) 45apply (erule Val_ValEnv.cases) 46apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs) 47done 48 49lemma ValE: 50 "[| v \<in> Val; 51 !!c. [| v = v_const(c); c \<in> Const |] ==> Q; 52 !!e ve x. 53 [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q 54 |] ==> 55 Q" 56apply (unfold Part_def Val_def ValEnv_def, clarify) 57apply (erule Val_ValEnv.cases) 58apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs) 59done 60 61(* Nonempty sets *) 62 63lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0" 64by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast) 65 66declare v_closNE [THEN notE, elim!] 67 68 69lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0" 70apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs) 71apply (drule constNEE, auto) 72done 73 74 75(* Proving that the empty set is not a value *) 76 77lemma ValNEE: "v \<in> Val ==> v \<noteq> 0" 78by (erule ValE, auto) 79 80(* Equalities for value environments *) 81 82lemma ve_dom_owr [simp]: 83 "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) \<union> {x}" 84apply (erule ValEnvE) 85apply (auto simp add: map_domain_owr) 86done 87 88lemma ve_app_owr [simp]: 89 "ve \<in> ValEnv 90 ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))" 91by (erule ValEnvE, simp add: map_app_owr) 92 93(* Introduction rules for operators on value environments *) 94 95lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val" 96by (erule ValEnvE, simp add: pmap_appI) 97 98lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar" 99apply (erule ValEnvE, simp) 100apply (blast dest: pmap_domainD) 101done 102 103lemma ve_empI: "ve_emp \<in> ValEnv" 104apply (unfold ve_emp_def) 105apply (rule Val_ValEnv.intros) 106apply (rule pmap_empI) 107done 108 109lemma ve_owrI: 110 "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv" 111apply (erule ValEnvE, simp) 112apply (blast intro: pmap_owrI Val_ValEnv.intros) 113done 114 115end 116