1(* Title: ZF/Coind/ECR.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4*) 5 6theory ECR imports Static Dynamic begin 7 8(* The extended correspondence relation *) 9 10consts 11 HasTyRel :: i 12coinductive 13 domains "HasTyRel" \<subseteq> "Val * Ty" 14 intros 15 htr_constI [intro!]: 16 "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel" 17 htr_closI [intro]: 18 "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv; 19 <te,e_fn(x,e),t> \<in> ElabRel; 20 ve_dom(ve) = te_dom(te); 21 {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |] 22 ==> <v_clos(x,e,ve),t> \<in> HasTyRel" 23 monos Pow_mono 24 type_intros Val_ValEnv.intros 25 26(* Pointwise extension to environments *) 27 28definition 29 hastyenv :: "[i,i] => o" where 30 "hastyenv(ve,te) == 31 ve_dom(ve) = te_dom(te) & 32 (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)" 33 34(* Specialised co-induction rule *) 35 36lemma htr_closCI [intro]: 37 "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv; 38 <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te); 39 {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> 40 Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel) |] 41 ==> <v_clos(x, e, ve),t> \<in> HasTyRel" 42apply (rule singletonI [THEN HasTyRel.coinduct], auto) 43done 44 45(* Specialised elimination rules *) 46 47inductive_cases 48 htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel" 49 and htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel" 50 51 52(* Properties of the pointwise extension to environments *) 53 54lemmas HasTyRel_non_zero = 55 HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE] 56 57lemma hastyenv_owr: 58 "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |] 59 ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))" 60by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero) 61 62lemma basic_consistency_lem: 63 "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)" 64apply (unfold isofenv_def hastyenv_def) 65apply (force intro: te_appI ve_domI) 66done 67 68 69(* ############################################################ *) 70(* The Consistency theorem *) 71(* ############################################################ *) 72 73lemma consistency_const: 74 "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |] 75 ==> <v_const(c), t> \<in> HasTyRel" 76by blast 77 78 79lemma consistency_var: 80 "[| x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel |] ==> 81 <ve_app(ve,x),t> \<in> HasTyRel" 82by (unfold hastyenv_def, blast) 83 84lemma consistency_fn: 85 "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; hastyenv(ve,te); 86 <te,e_fn(x,e),t> \<in> ElabRel 87 |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel" 88by (unfold hastyenv_def, blast) 89 90declare ElabRel.dom_subset [THEN subsetD, dest] 91 92declare Ty.intros [simp, intro!] 93declare TyEnv.intros [simp, intro!] 94declare Val_ValEnv.intros [simp, intro!] 95 96lemma consistency_fix: 97 "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val; 98 v_clos(x,e,ve_owr(ve,f,cl)) = cl; 99 hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==> 100 <cl,t> \<in> HasTyRel" 101apply (unfold hastyenv_def) 102apply (erule elab_fixE, safe) 103apply hypsubst_thin 104apply (rule subst, assumption) 105apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI) 106apply simp_all 107apply (blast intro: ve_owrI) 108apply (rule ElabRel.fnI) 109apply (simp_all add: ValNEE, force) 110done 111 112 113lemma consistency_app1: 114 "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const; 115 <ve,e1,v_const(c1)> \<in> EvalRel; 116 \<forall>t te. 117 hastyenv(ve,te) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel; 118 <ve, e2, v_const(c2)> \<in> EvalRel; 119 \<forall>t te. 120 hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v_const(c2),t> \<in> HasTyRel; 121 hastyenv(ve, te); 122 <te,e_app(e1,e2),t> \<in> ElabRel |] 123 ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel" 124by (blast intro!: c_appI intro: isof_app) 125 126lemma consistency_app2: 127 "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; 128 v \<in> Val; 129 <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel; 130 \<forall>t te. hastyenv(ve,te) \<longrightarrow> 131 <te,e1,t> \<in> ElabRel \<longrightarrow> <v_clos(xm,em,vem),t> \<in> HasTyRel; 132 <ve,e2,v2> \<in> EvalRel; 133 \<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v2,t> \<in> HasTyRel; 134 <ve_owr(vem,xm,v2),em,v> \<in> EvalRel; 135 \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow> 136 <te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel; 137 hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |] 138 ==> <v,t> \<in> HasTyRel" 139apply (erule elab_appE) 140apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+) 141apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+) 142apply (erule htr_closE) 143apply (erule elab_fnE, simp) 144apply clarify 145apply (drule spec [THEN spec, THEN mp, THEN mp]) 146prefer 2 apply assumption+ 147apply (rule hastyenv_owr, assumption) 148apply assumption 149apply (simp add: hastyenv_def, blast+) 150done 151 152lemma consistency [rule_format]: 153 "<ve,e,v> \<in> EvalRel 154 ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)" 155apply (erule EvalRel.induct) 156apply (simp_all add: consistency_const consistency_var consistency_fn 157 consistency_fix consistency_app1) 158apply (blast intro: consistency_app2) 159done 160 161lemma basic_consistency: 162 "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te); 163 <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |] 164 ==> isof(c,t)" 165by (blast dest: consistency intro!: basic_consistency_lem) 166 167end 168