1theory Type_Preservation 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 7 This theory shows how to prove the type preservation 8 property for the simply-typed lambda-calculus and 9 beta-reduction. 10 11\<close> 12 13atom_decl name 14 15nominal_datatype lam = 16 Var "name" 17| App "lam" "lam" 18| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._") 19 20text \<open>Capture-Avoiding Substitution\<close> 21 22nominal_primrec 23 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]") 24where 25 "(Var x)[y::=s] = (if x=y then s else (Var x))" 26| "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])" 27| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" 28apply(finite_guess)+ 29apply(rule TrueI)+ 30apply(simp add: abs_fresh) 31apply(fresh_guess)+ 32done 33 34lemma subst_eqvt[eqvt]: 35 fixes pi::"name prm" 36 shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]" 37by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct) 38 (auto simp add: perm_bij fresh_atm fresh_bij) 39 40lemma fresh_fact: 41 fixes z::"name" 42 shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]" 43by (nominal_induct t avoiding: z y s rule: lam.strong_induct) 44 (auto simp add: abs_fresh fresh_prod fresh_atm) 45 46text \<open>Types\<close> 47 48nominal_datatype ty = 49 TVar "string" 50 | TArr "ty" "ty" ("_ \<rightarrow> _") 51 52lemma ty_fresh: 53 fixes x::"name" 54 and T::"ty" 55 shows "x\<sharp>T" 56by (induct T rule: ty.induct) 57 (auto simp add: fresh_string) 58 59text \<open>Typing Contexts\<close> 60 61type_synonym ctx = "(name\<times>ty) list" 62 63abbreviation 64 "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<subseteq> _") 65where 66 "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2" 67 68text \<open>Validity of Typing Contexts\<close> 69 70inductive 71 valid :: "(name\<times>ty) list \<Rightarrow> bool" 72where 73 v1[intro]: "valid []" 74 | v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)" 75 76equivariance valid 77 78lemma valid_elim[dest]: 79 assumes a: "valid ((x,T)#\<Gamma>)" 80 shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>" 81using a by (cases) (auto) 82 83lemma valid_insert: 84 assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)" 85 shows "valid (\<Delta> @ \<Gamma>)" 86using a 87by (induct \<Delta>) 88 (auto simp add: fresh_list_append fresh_list_cons dest!: valid_elim) 89 90lemma fresh_set: 91 shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)" 92by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) 93 94lemma context_unique: 95 assumes a1: "valid \<Gamma>" 96 and a2: "(x,T) \<in> set \<Gamma>" 97 and a3: "(x,U) \<in> set \<Gamma>" 98 shows "T = U" 99using a1 a2 a3 100by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) 101 102text \<open>Typing Relation\<close> 103 104inductive 105 typing :: "ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 106where 107 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 108| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" 109| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" 110 111equivariance typing 112nominal_inductive typing 113 by (simp_all add: abs_fresh ty_fresh) 114 115lemma t_Lam_inversion[dest]: 116 assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 117 and fc: "x\<sharp>\<Gamma>" 118 shows "\<exists>T\<^sub>1 T\<^sub>2. T = T\<^sub>1 \<rightarrow> T\<^sub>2 \<and> (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2" 119using ty fc 120by (cases rule: typing.strong_cases) 121 (auto simp add: alpha lam.inject abs_fresh ty_fresh) 122 123lemma t_App_inversion[dest]: 124 assumes ty: "\<Gamma> \<turnstile> App t1 t2 : T" 125 shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'" 126using ty 127by (cases) (auto simp add: lam.inject) 128 129lemma weakening: 130 fixes \<Gamma>1 \<Gamma>2::"ctx" 131 assumes a: "\<Gamma>1 \<turnstile> t : T" 132 and b: "valid \<Gamma>2" 133 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 134 shows "\<Gamma>2 \<turnstile> t : T" 135using a b c 136by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 137 (auto | atomize)+ 138 139lemma type_substitution_aux: 140 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" 141 and b: "\<Gamma> \<turnstile> e' : T'" 142 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 143using a b 144proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) 145 case (t_Var y T x e' \<Delta>) 146 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 147 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 148 and a3: "\<Gamma> \<turnstile> e' : T'" . 149 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) 150 { assume eq: "x=y" 151 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) 152 with a3 have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening) 153 } 154 moreover 155 { assume ineq: "x\<noteq>y" 156 from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp 157 then have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto 158 } 159 ultimately show "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" by blast 160qed (force simp add: fresh_list_append fresh_list_cons)+ 161 162corollary type_substitution: 163 assumes a: "(x,T')#\<Gamma> \<turnstile> e : T" 164 and b: "\<Gamma> \<turnstile> e' : T'" 165 shows "\<Gamma> \<turnstile> e[x::=e'] : T" 166using a b 167by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified]) 168 169text \<open>Beta Reduction\<close> 170 171inductive 172 "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _") 173where 174 b1[intro]: "t1 \<longrightarrow>\<^sub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^sub>\<beta> App t2 s" 175| b2[intro]: "s1 \<longrightarrow>\<^sub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^sub>\<beta> App t s2" 176| b3[intro]: "t1 \<longrightarrow>\<^sub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^sub>\<beta> Lam [x].t2" 177| b4[intro]: "x\<sharp>s \<Longrightarrow> App (Lam [x].t) s \<longrightarrow>\<^sub>\<beta> t[x::=s]" 178 179equivariance beta 180nominal_inductive beta 181 by (auto simp add: abs_fresh fresh_fact) 182 183 184theorem type_preservation: 185 assumes a: "t \<longrightarrow>\<^sub>\<beta> t'" 186 and b: "\<Gamma> \<turnstile> t : T" 187 shows "\<Gamma> \<turnstile> t' : T" 188using a b 189proof (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct) 190 case (b1 t1 t2 s \<Gamma> T) 191 have "\<Gamma> \<turnstile> App t1 s : T" by fact 192 then obtain T' where a1: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto 193 have ih: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> t2 : T' \<rightarrow> T" by fact 194 with a1 a2 show "\<Gamma> \<turnstile> App t2 s : T" by auto 195next 196 case (b2 s1 s2 t \<Gamma> T) 197 have "\<Gamma> \<turnstile> App t s1 : T" by fact 198 then obtain T' where a1: "\<Gamma> \<turnstile> t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s1 : T'" by auto 199 have ih: "\<Gamma> \<turnstile> s1 : T' \<Longrightarrow> \<Gamma> \<turnstile> s2 : T'" by fact 200 with a1 a2 show "\<Gamma> \<turnstile> App t s2 : T" by auto 201next 202 case (b3 t1 t2 x \<Gamma> T) 203 have vc: "x\<sharp>\<Gamma>" by fact 204 have "\<Gamma> \<turnstile> Lam [x].t1 : T" by fact 205 then obtain T1 T2 where a1: "(x,T1)#\<Gamma> \<turnstile> t1 : T2" and a2: "T = T1 \<rightarrow> T2" using vc by auto 206 have ih: "(x,T1)#\<Gamma> \<turnstile> t1 : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> t2 : T2" by fact 207 with a1 a2 show "\<Gamma> \<turnstile> Lam [x].t2 : T" using vc by auto 208next 209 case (b4 x s t \<Gamma> T) 210 have vc: "x\<sharp>\<Gamma>" by fact 211 have "\<Gamma> \<turnstile> App (Lam [x].t) s : T" by fact 212 then obtain T' where a1: "\<Gamma> \<turnstile> Lam [x].t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto 213 from a1 obtain T1 T2 where a3: "(x,T')#\<Gamma> \<turnstile> t : T" using vc by (auto simp add: ty.inject) 214 from a3 a2 show "\<Gamma> \<turnstile> t[x::=s] : T" by (simp add: type_substitution) 215qed 216 217 218theorem type_preservation_automatic: 219 assumes a: "t \<longrightarrow>\<^sub>\<beta> t'" 220 and b: "\<Gamma> \<turnstile> t : T" 221 shows "\<Gamma> \<turnstile> t' : T" 222using a b 223by (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct) 224 (auto dest!: t_Lam_inversion t_App_inversion simp add: ty.inject type_substitution) 225 226end 227