1(* Formalisation of weakening using locally nameless *) 2(* terms; the nominal infrastructure can also derive *) 3(* strong induction principles for such representations *) 4(* *) 5(* Authors: Christian Urban and Randy Pollack *) 6theory LocalWeakening 7 imports "HOL-Nominal.Nominal" 8begin 9 10atom_decl name 11 12text \<open> 13 Curry-style lambda terms in locally nameless 14 representation without any binders 15\<close> 16nominal_datatype llam = 17 lPar "name" 18 | lVar "nat" 19 | lApp "llam" "llam" 20 | lLam "llam" 21 22text \<open>definition of vsub - at the moment a bit cumbersome\<close> 23 24lemma llam_cases: 25 "(\<exists>a. t = lPar a) \<or> (\<exists>n. t = lVar n) \<or> (\<exists>t1 t2. t = lApp t1 t2) \<or> 26 (\<exists>t1. t = lLam t1)" 27by (induct t rule: llam.induct) 28 (auto simp add: llam.inject) 29 30nominal_primrec 31 llam_size :: "llam \<Rightarrow> nat" 32where 33 "llam_size (lPar a) = 1" 34| "llam_size (lVar n) = 1" 35| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)" 36| "llam_size (lLam t) = 1 + (llam_size t)" 37by (rule TrueI)+ 38 39function 40 vsub :: "llam \<Rightarrow> nat \<Rightarrow> llam \<Rightarrow> llam" 41where 42 vsub_lPar: "vsub (lPar p) x s = lPar p" 43 | vsub_lVar: "vsub (lVar n) x s = (if n < x then (lVar n) 44 else (if n = x then s else (lVar (n - 1))))" 45 | vsub_lApp: "vsub (lApp t u) x s = (lApp (vsub t x s) (vsub u x s))" 46 | vsub_lLam: "vsub (lLam t) x s = (lLam (vsub t (x + 1) s))" 47using llam_cases 48apply(auto simp add: llam.inject) 49apply(rotate_tac 4) 50apply(drule_tac x="a" in meta_spec) 51apply(blast) 52done 53termination by (relation "measure (llam_size \<circ> fst)") auto 54 55lemma vsub_eqvt[eqvt]: 56 fixes pi::"name prm" 57 shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" 58by (induct t arbitrary: n rule: llam.induct) 59 (simp_all add: perm_nat_def) 60 61definition freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" where 62 "freshen t p \<equiv> vsub t 0 (lPar p)" 63 64lemma freshen_eqvt[eqvt]: 65 fixes pi::"name prm" 66 shows "pi\<bullet>(freshen t p) = freshen (pi\<bullet>t) (pi\<bullet>p)" 67by (simp add: vsub_eqvt freshen_def perm_nat_def) 68 69text \<open>types\<close> 70 71nominal_datatype ty = 72 TVar "nat" 73 | TArr "ty" "ty" (infix "\<rightarrow>" 200) 74 75lemma ty_fresh[simp]: 76 fixes x::"name" 77 and T::"ty" 78 shows "x\<sharp>T" 79by (induct T rule: ty.induct) 80 (simp_all add: fresh_nat) 81 82text \<open>valid contexts\<close> 83 84type_synonym cxt = "(name\<times>ty) list" 85 86inductive 87 valid :: "cxt \<Rightarrow> bool" 88where 89 v1[intro]: "valid []" 90| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,T)#\<Gamma>)" 91 92equivariance valid 93 94lemma v2_elim: 95 assumes a: "valid ((a,T)#\<Gamma>)" 96 shows "a\<sharp>\<Gamma> \<and> valid \<Gamma>" 97using a by (cases) (auto) 98 99text \<open>"weak" typing relation\<close> 100 101inductive 102 typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 103where 104 t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar x : T" 105| t_lApp[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lApp t1 t2 : T2" 106| t_lLam[intro]: "\<lbrakk>x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> freshen t x : T2\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lLam t : T1\<rightarrow>T2" 107 108equivariance typing 109 110lemma typing_implies_valid: 111 assumes a: "\<Gamma> \<turnstile> t : T" 112 shows "valid \<Gamma>" 113using a by (induct) (auto dest: v2_elim) 114 115text \<open> 116 we have to explicitly state that nominal_inductive should strengthen 117 over the variable x (since x is not a binder) 118\<close> 119nominal_inductive typing 120 avoids t_lLam: x 121 by (auto simp add: fresh_prod dest: v2_elim typing_implies_valid) 122 123text \<open>strong induction principle for typing\<close> 124thm typing.strong_induct 125 126text \<open>sub-contexts\<close> 127 128abbreviation 129 "sub_context" :: "cxt \<Rightarrow> cxt \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 130where 131 "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2" 132 133lemma weakening_almost_automatic: 134 fixes \<Gamma>1 \<Gamma>2 :: cxt 135 assumes a: "\<Gamma>1 \<turnstile> t : T" 136 and b: "\<Gamma>1 \<subseteq> \<Gamma>2" 137 and c: "valid \<Gamma>2" 138shows "\<Gamma>2 \<turnstile> t : T" 139using a b c 140apply(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 141apply(auto) 142apply(drule_tac x="(x,T1)#\<Gamma>2" in meta_spec) 143apply(auto intro!: t_lLam) 144done 145 146lemma weakening_in_more_detail: 147 fixes \<Gamma>1 \<Gamma>2 :: cxt 148 assumes a: "\<Gamma>1 \<turnstile> t : T" 149 and b: "\<Gamma>1 \<subseteq> \<Gamma>2" 150 and c: "valid \<Gamma>2" 151shows "\<Gamma>2 \<turnstile> t : T" 152using a b c 153proof(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 154 case (t_lPar \<Gamma>1 x T \<Gamma>2) (* variable case *) 155 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 156 moreover 157 have "valid \<Gamma>2" by fact 158 moreover 159 have "(x,T)\<in> set \<Gamma>1" by fact 160 ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto 161next 162 case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *) 163 have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+ (* variable convention *) 164 have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact 165 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 166 then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp 167 moreover 168 have "valid \<Gamma>2" by fact 169 then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) 170 ultimately have "(x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" using ih by simp 171 with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto 172next 173 case (t_lApp \<Gamma>1 t1 T1 T2 t2 \<Gamma>2) 174 then show "\<Gamma>2 \<turnstile> lApp t1 t2 : T2" by auto 175qed 176 177end 178