1theory Weakening 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 A simple proof of the Weakening Property in the simply-typed 7 lambda-calculus. The proof is simple, because we can make use 8 of the variable convention.\<close> 9 10atom_decl name 11 12text \<open>Terms and Types\<close> 13 14nominal_datatype lam = 15 Var "name" 16 | App "lam" "lam" 17 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) 18 19nominal_datatype ty = 20 TVar "string" 21 | TArr "ty" "ty" ("_ \<rightarrow> _" [100,100] 100) 22 23lemma ty_fresh: 24 fixes x::"name" 25 and T::"ty" 26 shows "x\<sharp>T" 27by (nominal_induct T rule: ty.strong_induct) 28 (auto simp add: fresh_string) 29 30text \<open> 31 Valid contexts (at the moment we have no type for finite 32 sets yet, therefore typing-contexts are lists).\<close> 33 34inductive 35 valid :: "(name\<times>ty) list \<Rightarrow> bool" 36where 37 v1[intro]: "valid []" 38 | v2[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)" 39 40equivariance valid 41 42text\<open>Typing judgements\<close> 43 44inductive 45 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 46where 47 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 48 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" 49 | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2" 50 51text \<open> 52 We derive the strong induction principle for the typing 53 relation (this induction principle has the variable convention 54 already built-in).\<close> 55 56equivariance typing 57nominal_inductive typing 58 by (simp_all add: abs_fresh ty_fresh) 59 60text \<open>Abbreviation for the notion of subcontexts.\<close> 61 62abbreviation 63 "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 64where 65 "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2" 66 67text \<open>Now it comes: The Weakening Lemma\<close> 68 69text \<open> 70 The first version is, after setting up the induction, 71 completely automatic except for use of atomize.\<close> 72 73lemma weakening_version1: 74 fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" 75 assumes a: "\<Gamma>1 \<turnstile> t : T" 76 and b: "valid \<Gamma>2" 77 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 78 shows "\<Gamma>2 \<turnstile> t : T" 79using a b c 80by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 81 (auto | atomize)+ 82 83text \<open> 84 The second version gives the details for the variable 85 and lambda case.\<close> 86 87lemma weakening_version2: 88 fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" 89 and t ::"lam" 90 and \<tau> ::"ty" 91 assumes a: "\<Gamma>1 \<turnstile> t : T" 92 and b: "valid \<Gamma>2" 93 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 94 shows "\<Gamma>2 \<turnstile> t : T" 95using a b c 96proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 97 case (t_Var \<Gamma>1 x T) (* variable case *) 98 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 99 moreover 100 have "valid \<Gamma>2" by fact 101 moreover 102 have "(x,T)\<in> set \<Gamma>1" by fact 103 ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto 104next 105 case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) 106 have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *) 107 have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact 108 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 109 then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp 110 moreover 111 have "valid \<Gamma>2" by fact 112 then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) 113 ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp 114 with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto 115qed (auto) (* app case *) 116 117text\<open> 118 The original induction principle for the typing relation 119 is not strong enough - even this simple lemma fails to be 120 simple ;o)\<close> 121 122lemma weakening_not_straigh_forward: 123 fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" 124 assumes a: "\<Gamma>1 \<turnstile> t : T" 125 and b: "valid \<Gamma>2" 126 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 127 shows "\<Gamma>2 \<turnstile> t : T" 128using a b c 129proof (induct arbitrary: \<Gamma>2) 130 case (t_Var \<Gamma>1 x T) (* variable case still works *) 131 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 132 moreover 133 have "valid \<Gamma>2" by fact 134 moreover 135 have "(x,T) \<in> (set \<Gamma>1)" by fact 136 ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto 137next 138 case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) 139 (* These are all assumptions available in this case*) 140 have a0: "x\<sharp>\<Gamma>1" by fact 141 have a1: "(x,T1)#\<Gamma>1 \<turnstile> t : T2" by fact 142 have a2: "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 143 have a3: "valid \<Gamma>2" by fact 144 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact 145 have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" using a2 by simp 146 moreover 147 have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 148 oops 149 150text\<open> 151 To show that the proof with explicit renaming is not simple, 152 here is the proof without using the variable convention. It 153 crucially depends on the equivariance property of the typing 154 relation. 155 156\<close> 157 158lemma weakening_with_explicit_renaming: 159 fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" 160 assumes a: "\<Gamma>1 \<turnstile> t : T" 161 and b: "valid \<Gamma>2" 162 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 163 shows "\<Gamma>2 \<turnstile> t : T" 164using a b c 165proof (induct arbitrary: \<Gamma>2) 166 case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) 167 have fc0: "x\<sharp>\<Gamma>1" by fact 168 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact 169 obtain c::"name" where fc1: "c\<sharp>(x,t,\<Gamma>1,\<Gamma>2)" (* we obtain a fresh name *) 170 by (rule exists_fresh) (auto simp add: fs_name1) 171 have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *) 172 by (auto simp add: lam.inject alpha fresh_prod fresh_atm) 173 moreover 174 have "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *) 175 proof - 176 (* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *) 177 have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" 178 proof - 179 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 180 then have "[(c,x)]\<bullet>((x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc0 fc1 181 by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh) 182 then show "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" by (rule perm_boolE) 183 qed 184 moreover 185 have "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" 186 proof - 187 have "valid \<Gamma>2" by fact 188 then show "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc1 189 by (auto intro!: v2 simp add: fresh_left calc_atm eqvts) 190 qed 191 (* these two facts give us by induction hypothesis the following *) 192 ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp 193 (* we now apply renamings to get to our goal *) 194 then have "[(c,x)]\<bullet>((x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2)" by (rule perm_boolI) 195 then have "(c,T1)#\<Gamma>2 \<turnstile> ([(c,x)]\<bullet>t) : T2" using fc1 196 by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh) 197 then show "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" using fc1 by auto 198 qed 199 ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp 200qed (auto) (* var and app cases *) 201 202text \<open> 203 Moral: compare the proof with explicit renamings to weakening_version1 204 and weakening_version2, and imagine you are proving something more substantial 205 than the weakening lemma.\<close> 206 207end 208