1(* The definitions for a challenge suggested by Adam Chlipala *) 2 3theory Compile 4imports "HOL-Nominal.Nominal" 5begin 6 7atom_decl name 8 9nominal_datatype data = 10 DNat 11 | DProd "data" "data" 12 | DSum "data" "data" 13 14nominal_datatype ty = 15 Data "data" 16 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) 17 18nominal_datatype trm = 19 Var "name" 20 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 21 | App "trm" "trm" 22 | Const "nat" 23 | Pr "trm" "trm" 24 | Fst "trm" 25 | Snd "trm" 26 | InL "trm" 27 | InR "trm" 28 | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" 29 ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100) 30 31nominal_datatype dataI = OneI | NatI 32 33nominal_datatype tyI = 34 DataI "dataI" 35 | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100) 36 37nominal_datatype trmI = 38 IVar "name" 39 | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100) 40 | IApp "trmI" "trmI" 41 | IUnit 42 | INat "nat" 43 | ISucc "trmI" 44 | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100) 45 | IRef "trmI" 46 | ISeq "trmI" "trmI" ("_;;_" [100,100] 100) 47 | Iif "trmI" "trmI" "trmI" 48 49text \<open>valid contexts\<close> 50 51inductive 52 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool" 53where 54 v1[intro]: "valid []" 55| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *) 56 57text \<open>typing judgements for trms\<close> 58 59inductive 60 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 61where 62 t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>" 63| t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2" 64| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2" 65| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)" 66| t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)" 67| t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)" 68| t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)" 69| t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)" 70| t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)" 71| t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2); 72 ((x1,Data(\<sigma>1))#\<Gamma>) \<turnstile> e1 : \<tau>; ((x2,Data(\<sigma>2))#\<Gamma>) \<turnstile> e2 : \<tau>\<rbrakk> 73 \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) : \<tau>" 74 75text \<open>typing judgements for Itrms\<close> 76 77inductive 78 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80) 79where 80 t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>" 81| t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2" 82| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2" 83| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)" 84| t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)" 85| t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)" 86| t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)" 87| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)" 88| t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>" 89| t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>" 90 91text \<open>capture-avoiding substitution\<close> 92 93class subst = 94 fixes subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100) 95 96instantiation trm :: subst 97begin 98 99nominal_primrec subst_trm 100where 101 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 102| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" 103| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 104| "(Const n)[y::=t'] = Const n" 105| "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])" 106| "(Fst e)[y::=t'] = Fst (e[y::=t'])" 107| "(Snd e)[y::=t'] = Snd (e[y::=t'])" 108| "(InL e)[y::=t'] = InL (e[y::=t'])" 109| "(InR e)[y::=t'] = InR (e[y::=t'])" 110| "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow> 111 (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] = 112 (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))" 113 apply(finite_guess)+ 114 apply(rule TrueI)+ 115 apply(simp add: abs_fresh)+ 116 apply(fresh_guess)+ 117 done 118 119instance .. 120 121end 122 123instantiation trmI :: subst 124begin 125 126nominal_primrec subst_trmI 127where 128 "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))" 129| "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])" 130| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])" 131| "(INat n)[y::=t'] = INat n" 132| "(IUnit)[y::=t'] = IUnit" 133| "(ISucc e)[y::=t'] = ISucc (e[y::=t'])" 134| "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])" 135| "(IRef e)[y::=t'] = IRef (e[y::=t'])" 136| "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])" 137| "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])" 138 apply(finite_guess)+ 139 apply(rule TrueI)+ 140 apply(simp add: abs_fresh)+ 141 apply(fresh_guess)+ 142 done 143 144instance .. 145 146end 147 148lemma Isubst_eqvt[eqvt]: 149 fixes pi::"name prm" 150 and t1::"trmI" 151 and t2::"trmI" 152 and x::"name" 153 shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])" 154 apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct) 155 apply (simp_all add: subst_trmI.simps eqvts fresh_bij) 156 done 157 158lemma Isubst_supp: 159 fixes t1::"trmI" 160 and t2::"trmI" 161 and x::"name" 162 shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})" 163 apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct) 164 apply (auto simp add: subst_trmI.simps trmI.supp supp_atm abs_supp supp_nat) 165 apply blast+ 166 done 167 168lemma Isubst_fresh: 169 fixes x::"name" 170 and y::"name" 171 and t1::"trmI" 172 and t2::"trmI" 173 assumes a: "x\<sharp>[y].t1" "x\<sharp>t2" 174 shows "x\<sharp>(t1[y::=t2])" 175using a 176apply(auto simp add: fresh_def Isubst_supp) 177apply(drule rev_subsetD) 178apply(rule Isubst_supp) 179apply(simp add: abs_supp) 180done 181 182text \<open>big-step evaluation for trms\<close> 183 184inductive 185 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 186where 187 b0[intro]: "Lam [x].e \<Down> Lam [x].e" 188| b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'" 189| b2[intro]: "Const n \<Down> Const n" 190| b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'" 191| b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1" 192| b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2" 193| b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'" 194| b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'" 195| b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''" 196| b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''" 197 198inductive 199 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80) 200where 201 m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)" 202| m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk> 203 \<Longrightarrow> (m,IApp e1 e2) I\<Down> (m''',e4)" 204| m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)" 205| m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))" 206| m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))" 207| m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))" 208| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)" 209| m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)" 210| m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)" 211| m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)" 212 213text \<open>Translation functions\<close> 214 215nominal_primrec 216 trans :: "trm \<Rightarrow> trmI" 217where 218 "trans (Var x) = (IVar x)" 219| "trans (App e1 e2) = IApp (trans e1) (trans e2)" 220| "trans (Lam [x].e) = ILam [x].(trans e)" 221| "trans (Const n) = INat n" 222| "trans (Pr e1 e2) = 223 (let limit = IRef(INat 0) in 224 let v1 = (trans e1) in 225 let v2 = (trans e2) in 226 (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" 227| "trans (Fst e) = IRef (ISucc (trans e))" 228| "trans (Snd e) = IRef (ISucc (ISucc (trans e)))" 229| "trans (InL e) = 230 (let limit = IRef(INat 0) in 231 let v = (trans e) in 232 (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" 233| "trans (InR e) = 234 (let limit = IRef(INat 0) in 235 let v = (trans e) in 236 (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))" 237| "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 238 trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) = 239 (let v = (trans e) in 240 let v1 = (trans e1) in 241 let v2 = (trans e2) in 242 Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))" 243 apply(finite_guess add: Let_def)+ 244 apply(rule TrueI)+ 245 apply(simp add: abs_fresh Isubst_fresh)+ 246 apply(fresh_guess add: Let_def)+ 247 done 248 249nominal_primrec 250 trans_type :: "ty \<Rightarrow> tyI" 251where 252 "trans_type (Data \<sigma>) = DataI(NatI)" 253| "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)" 254 by (rule TrueI)+ 255 256end 257