1theory CK_Machine 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 7 This theory establishes soundness and completeness for a CK-machine 8 with respect to a cbv-big-step semantics. The language includes 9 functions, recursion, booleans and numbers. In the soundness proof 10 the small-step cbv-reduction relation is used in order to get the 11 induction through. The type-preservation property is proved for the 12 machine and also for the small- and big-step semantics. Finally, 13 the progress property is proved for the small-step semantics. 14 15 The development is inspired by notes about context machines written 16 by Roshan James (Indiana University) and also by the lecture notes 17 written by Andy Pitts for his semantics course. See 18 19 \<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close> 20 \<^url>\<open>https://www.cl.cam.ac.uk/teaching/2001/Semantics\<close> 21\<close> 22 23atom_decl name 24 25nominal_datatype lam = 26 VAR "name" 27| APP "lam" "lam" 28| LAM "\<guillemotleft>name\<guillemotright>lam" ("LAM [_]._") 29| NUM "nat" 30| DIFF "lam" "lam" ("_ -- _") (* subtraction *) 31| PLUS "lam" "lam" ("_ ++ _") (* addition *) 32| TRUE 33| FALSE 34| IF "lam" "lam" "lam" 35| FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._") (* recursion *) 36| ZET "lam" (* zero test *) 37| EQI "lam" "lam" (* equality test on numbers *) 38 39section \<open>Capture-Avoiding Substitution\<close> 40 41nominal_primrec 42 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) 43where 44 "(VAR x)[y::=s] = (if x=y then s else (VAR x))" 45| "(APP t\<^sub>1 t\<^sub>2)[y::=s] = APP (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])" 46| "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])" 47| "(NUM n)[y::=s] = NUM n" 48| "(t\<^sub>1 -- t\<^sub>2)[y::=s] = (t\<^sub>1[y::=s]) -- (t\<^sub>2[y::=s])" 49| "(t\<^sub>1 ++ t\<^sub>2)[y::=s] = (t\<^sub>1[y::=s]) ++ (t\<^sub>2[y::=s])" 50| "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])" 51| "TRUE[y::=s] = TRUE" 52| "FALSE[y::=s] = FALSE" 53| "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])" 54| "(ZET t)[y::=s] = ZET (t[y::=s])" 55| "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])" 56apply(finite_guess)+ 57apply(rule TrueI)+ 58apply(simp add: abs_fresh)+ 59apply(fresh_guess)+ 60done 61 62lemma subst_eqvt[eqvt]: 63 fixes pi::"name prm" 64 shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]" 65by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct) 66 (auto simp add: perm_bij fresh_atm fresh_bij) 67 68lemma fresh_fact: 69 fixes z::"name" 70 shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]" 71by (nominal_induct t avoiding: z y s rule: lam.strong_induct) 72 (auto simp add: abs_fresh fresh_prod fresh_atm fresh_nat) 73 74lemma subst_rename: 75 assumes a: "y\<sharp>t" 76 shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]" 77using a 78by (nominal_induct t avoiding: x y s rule: lam.strong_induct) 79 (auto simp add: calc_atm fresh_atm abs_fresh perm_nat_def) 80 81section \<open>Evaluation Contexts\<close> 82 83datatype ctx = 84 Hole ("\<box>") 85 | CAPPL "ctx" "lam" 86 | CAPPR "lam" "ctx" 87 | CDIFFL "ctx" "lam" 88 | CDIFFR "lam" "ctx" 89 | CPLUSL "ctx" "lam" 90 | CPLUSR "lam" "ctx" 91 | CIF "ctx" "lam" "lam" 92 | CZET "ctx" 93 | CEQIL "ctx" "lam" 94 | CEQIR "lam" "ctx" 95 96text \<open>The operation of filling a term into a context:\<close> 97 98fun 99 filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>") 100where 101 "\<box>\<lbrakk>t\<rbrakk> = t" 102| "(CAPPL E t')\<lbrakk>t\<rbrakk> = APP (E\<lbrakk>t\<rbrakk>) t'" 103| "(CAPPR t' E)\<lbrakk>t\<rbrakk> = APP t' (E\<lbrakk>t\<rbrakk>)" 104| "(CDIFFL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) -- t'" 105| "(CDIFFR t' E)\<lbrakk>t\<rbrakk> = t' -- (E\<lbrakk>t\<rbrakk>)" 106| "(CPLUSL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) ++ t'" 107| "(CPLUSR t' E)\<lbrakk>t\<rbrakk> = t' ++ (E\<lbrakk>t\<rbrakk>)" 108| "(CIF E t1 t2)\<lbrakk>t\<rbrakk> = IF (E\<lbrakk>t\<rbrakk>) t1 t2" 109| "(CZET E)\<lbrakk>t\<rbrakk> = ZET (E\<lbrakk>t\<rbrakk>)" 110| "(CEQIL E t')\<lbrakk>t\<rbrakk> = EQI (E\<lbrakk>t\<rbrakk>) t'" 111| "(CEQIR t' E)\<lbrakk>t\<rbrakk> = EQI t' (E\<lbrakk>t\<rbrakk>)" 112 113text \<open>The operation of composing two contexts:\<close> 114 115fun 116 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _") 117where 118 "\<box> \<circ> E' = E'" 119| "(CAPPL E t') \<circ> E' = CAPPL (E \<circ> E') t'" 120| "(CAPPR t' E) \<circ> E' = CAPPR t' (E \<circ> E')" 121| "(CDIFFL E t') \<circ> E' = CDIFFL (E \<circ> E') t'" 122| "(CDIFFR t' E) \<circ> E' = CDIFFR t' (E \<circ> E')" 123| "(CPLUSL E t') \<circ> E' = CPLUSL (E \<circ> E') t'" 124| "(CPLUSR t' E) \<circ> E' = CPLUSR t' (E \<circ> E')" 125| "(CIF E t1 t2) \<circ> E' = CIF (E \<circ> E') t1 t2" 126| "(CZET E) \<circ> E' = CZET (E \<circ> E')" 127| "(CEQIL E t') \<circ> E' = CEQIL (E \<circ> E') t'" 128| "(CEQIR t' E) \<circ> E' = CEQIR t' (E \<circ> E')" 129 130lemma ctx_compose: 131 shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" 132by (induct E1 rule: ctx.induct) (auto) 133 134text \<open>Composing a list (stack) of contexts.\<close> 135 136fun 137 ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>") 138where 139 "[]\<down> = \<box>" 140 | "(E#Es)\<down> = (Es\<down>) \<circ> E" 141 142section \<open>The CK-Machine\<close> 143 144inductive 145 val :: "lam\<Rightarrow>bool" 146where 147 v_LAM[intro]: "val (LAM [x].e)" 148| v_NUM[intro]: "val (NUM n)" 149| v_FALSE[intro]: "val FALSE" 150| v_TRUE[intro]: "val TRUE" 151 152equivariance val 153 154inductive 155 machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>") 156where 157 m1[intro]: "<APP e1 e2,Es> \<mapsto> <e1,(CAPPL \<box> e2)#Es>" 158| m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<mapsto> <e2,(CAPPR v \<box>)#Es>" 159| m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<mapsto> <e[y::=v],Es>" 160| m4[intro]: "<e1 -- e2, Es> \<mapsto> <e1,(CDIFFL \<box> e2)#Es>" 161| m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<mapsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>" 162| m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1 - n2),Es>" 163| m4'[intro]:"<e1 ++ e2, Es> \<mapsto> <e1,(CPLUSL \<box> e2)#Es>" 164| m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<mapsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>" 165| m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1+n2),Es>" 166| m7[intro]: "<IF e1 e2 e3,Es> \<mapsto> <e1,(CIF \<box> e2 e3)#Es>" 167| m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<mapsto> <e1,Es>" 168| m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<mapsto> <e2,Es>" 169| mA[intro]: "<FIX [x].t,Es> \<mapsto> <t[x::=FIX [x].t],Es>" 170| mB[intro]: "<ZET e,Es> \<mapsto> <e,(CZET \<box>)#Es>" 171| mC[intro]: "<NUM 0,(CZET \<box>)#Es> \<mapsto> <TRUE,Es>" 172| mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZET \<box>)#Es> \<mapsto> <FALSE,Es>" 173| mE[intro]: "<EQI e1 e2,Es> \<mapsto> <e1,(CEQIL \<box> e2)#Es>" 174| mF[intro]: "<NUM n1,(CEQIL \<box> e2)#Es> \<mapsto> <e2,(CEQIR (NUM n1) \<box>)#Es>" 175| mG[intro]: "<NUM n,(CEQIR (NUM n) \<box>)#Es> \<mapsto> <TRUE,Es>" 176| mH[intro]: "n1\<noteq>n2 \<Longrightarrow> <NUM n1,(CEQIR (NUM n2) \<box>)#Es> \<mapsto> <FALSE,Es>" 177 178inductive 179 "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto>* <_,_>") 180where 181 ms1[intro]: "<e,Es> \<mapsto>* <e,Es>" 182| ms2[intro]: "\<lbrakk><e1,Es1> \<mapsto> <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>" 183 184lemma ms3[intro,trans]: 185 assumes a: "<e1,Es1> \<mapsto>* <e2,Es2>" "<e2,Es2> \<mapsto>* <e3,Es3>" 186 shows "<e1,Es1> \<mapsto>* <e3,Es3>" 187using a by (induct) (auto) 188 189lemma ms4[intro]: 190 assumes a: "<e1,Es1> \<mapsto> <e2,Es2>" 191 shows "<e1,Es1> \<mapsto>* <e2,Es2>" 192using a by (rule ms2) (rule ms1) 193 194section \<open>The Evaluation Relation (Big-Step Semantics)\<close> 195 196inductive 197 eval :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<Down> _") 198where 199 eval_NUM[intro]: "NUM n \<Down> NUM n" 200| eval_DIFF[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 -- t2 \<Down> NUM (n1 - n2)" 201| eval_PLUS[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 ++ t2 \<Down> NUM (n1 + n2)" 202| eval_LAM[intro]: "LAM [x].t \<Down> LAM [x].t" 203| eval_APP[intro]: "\<lbrakk>t1\<Down> LAM [x].t; t2\<Down> t2'; t[x::=t2']\<Down> t'\<rbrakk> \<Longrightarrow> APP t1 t2 \<Down> t'" 204| eval_FIX[intro]: "t[x::= FIX [x].t] \<Down> t' \<Longrightarrow> FIX [x].t \<Down> t'" 205| eval_IF1[intro]: "\<lbrakk>t1 \<Down> TRUE; t2 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'" 206| eval_IF2[intro]: "\<lbrakk>t1 \<Down> FALSE; t3 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'" 207| eval_TRUE[intro]: "TRUE \<Down> TRUE" 208| eval_FALSE[intro]:"FALSE \<Down> FALSE" 209| eval_ZET1[intro]: "t \<Down> NUM 0 \<Longrightarrow> ZET t \<Down> TRUE" 210| eval_ZET2[intro]: "\<lbrakk>t \<Down> NUM n; 0 < n\<rbrakk> \<Longrightarrow> ZET t \<Down> FALSE" 211| eval_EQ1[intro]: "\<lbrakk>t1 \<Down> NUM n; t2 \<Down> NUM n\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> TRUE" 212| eval_EQ2[intro]: "\<lbrakk>t1 \<Down> NUM n1; t2 \<Down> NUM n2; n1\<noteq>n2\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> FALSE" 213 214declare lam.inject[simp] 215inductive_cases eval_elim: 216 "APP t1 t2 \<Down> t'" 217 "IF t1 t2 t3 \<Down> t'" 218 "ZET t \<Down> t'" 219 "EQI t1 t2 \<Down> t'" 220 "t1 ++ t2 \<Down> t'" 221 "t1 -- t2 \<Down> t'" 222 "(NUM n) \<Down> t" 223 "TRUE \<Down> t" 224 "FALSE \<Down> t" 225declare lam.inject[simp del] 226 227lemma eval_to: 228 assumes a: "t \<Down> t'" 229 shows "val t'" 230using a by (induct) (auto) 231 232lemma eval_val: 233 assumes a: "val t" 234 shows "t \<Down> t" 235using a by (induct) (auto) 236 237text \<open>The Completeness Property:\<close> 238 239theorem eval_implies_machine_star_ctx: 240 assumes a: "t \<Down> t'" 241 shows "<t,Es> \<mapsto>* <t',Es>" 242using a 243by (induct arbitrary: Es) 244 (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+ 245 246corollary eval_implies_machine_star: 247 assumes a: "t \<Down> t'" 248 shows "<t,[]> \<mapsto>* <t',[]>" 249using a by (auto dest: eval_implies_machine_star_ctx) 250 251section \<open>The CBV Reduction Relation (Small-Step Semantics)\<close> 252 253lemma less_eqvt[eqvt]: 254 fixes pi::"name prm" 255 and n1 n2::"nat" 256 shows "(pi\<bullet>(n1 < n2)) = ((pi\<bullet>n1) < (pi\<bullet>n2))" 257by (simp add: perm_nat_def perm_bool) 258 259inductive 260 cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _") 261where 262 cbv1: "\<lbrakk>val v; x\<sharp>v\<rbrakk> \<Longrightarrow> APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" 263| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t t2 \<longrightarrow>cbv APP t' t2" 264| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t2 t \<longrightarrow>cbv APP t2 t'" 265| cbv4[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t -- t2 \<longrightarrow>cbv t' -- t2" 266| cbv5[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 -- t \<longrightarrow>cbv t2 -- t'" 267| cbv6[intro]: "(NUM n1) -- (NUM n2) \<longrightarrow>cbv NUM (n1 - n2)" 268| cbv4'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t ++ t2 \<longrightarrow>cbv t' ++ t2" 269| cbv5'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 ++ t \<longrightarrow>cbv t2 ++ t'" 270| cbv6'[intro]:"(NUM n1) ++ (NUM n2) \<longrightarrow>cbv NUM (n1 + n2)" 271| cbv7[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> IF t t1 t2 \<longrightarrow>cbv IF t' t1 t2" 272| cbv8[intro]: "IF TRUE t1 t2 \<longrightarrow>cbv t1" 273| cbv9[intro]: "IF FALSE t1 t2 \<longrightarrow>cbv t2" 274| cbvA[intro]: "FIX [x].t \<longrightarrow>cbv t[x::=FIX [x].t]" 275| cbvB[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> ZET t \<longrightarrow>cbv ZET t'" 276| cbvC[intro]: "ZET (NUM 0) \<longrightarrow>cbv TRUE" 277| cbvD[intro]: "0 < n \<Longrightarrow> ZET (NUM n) \<longrightarrow>cbv FALSE" 278| cbvE[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t t2 \<longrightarrow>cbv EQI t' t2" 279| cbvF[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t2 t \<longrightarrow>cbv EQI t2 t'" 280| cbvG[intro]: "EQI (NUM n) (NUM n) \<longrightarrow>cbv TRUE" 281| cbvH[intro]: "n1\<noteq>n2 \<Longrightarrow> EQI (NUM n1) (NUM n2) \<longrightarrow>cbv FALSE" 282 283equivariance cbv 284nominal_inductive cbv 285 by (simp_all add: abs_fresh fresh_fact) 286 287lemma better_cbv1[intro]: 288 assumes a: "val v" 289 shows "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" 290proof - 291 obtain y::"name" where fs: "y\<sharp>(x,t,v)" by (rule exists_fresh, rule fin_supp, blast) 292 have "APP (LAM [x].t) v = APP (LAM [y].([(y,x)]\<bullet>t)) v" using fs 293 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) 294 also have "\<dots> \<longrightarrow>cbv ([(y,x)]\<bullet>t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1) 295 also have "\<dots> = t[x::=v]" using fs by (simp add: subst_rename[symmetric]) 296 finally show "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" by simp 297qed 298 299inductive 300 "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _") 301where 302 cbvs1[intro]: "e \<longrightarrow>cbv* e" 303| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3" 304 305lemma cbvs3[intro,trans]: 306 assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3" 307 shows "e1 \<longrightarrow>cbv* e3" 308using a by (induct) (auto) 309 310lemma cbv_in_ctx: 311 assumes a: "t \<longrightarrow>cbv t'" 312 shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" 313using a by (induct E) (auto) 314 315lemma machine_implies_cbv_star_ctx: 316 assumes a: "<e,Es> \<mapsto> <e',Es'>" 317 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" 318using a by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx) 319 320lemma machine_star_implies_cbv_star_ctx: 321 assumes a: "<e,Es> \<mapsto>* <e',Es'>" 322 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" 323using a 324by (induct) (auto dest: machine_implies_cbv_star_ctx) 325 326lemma machine_star_implies_cbv_star: 327 assumes a: "<e,[]> \<mapsto>* <e',[]>" 328 shows "e \<longrightarrow>cbv* e'" 329using a by (auto dest: machine_star_implies_cbv_star_ctx) 330 331lemma cbv_eval: 332 assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3" 333 shows "t1 \<Down> t3" 334using a 335by (induct arbitrary: t3) 336 (auto elim!: eval_elim intro: eval_val) 337 338lemma cbv_star_eval: 339 assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3" 340 shows "t1 \<Down> t3" 341using a by (induct) (auto simp add: cbv_eval) 342 343lemma cbv_star_implies_eval: 344 assumes a: "t \<longrightarrow>cbv* v" "val v" 345 shows "t \<Down> v" 346using a 347by (induct) 348 (auto simp add: eval_val cbv_star_eval dest: cbvs2) 349 350text \<open>The Soundness Property\<close> 351 352theorem machine_star_implies_eval: 353 assumes a: "<t1,[]> \<mapsto>* <t2,[]>" 354 and b: "val t2" 355 shows "t1 \<Down> t2" 356proof - 357 from a have "t1 \<longrightarrow>cbv* t2" by (simp add: machine_star_implies_cbv_star) 358 then show "t1 \<Down> t2" using b by (simp add: cbv_star_implies_eval) 359qed 360 361section \<open>Typing\<close> 362 363text \<open>Types\<close> 364 365nominal_datatype ty = 366 tVAR "string" 367| tBOOL 368| tINT 369| tARR "ty" "ty" ("_ \<rightarrow> _") 370 371declare ty.inject[simp] 372 373lemma ty_fresh: 374 fixes x::"name" 375 and T::"ty" 376 shows "x\<sharp>T" 377by (induct T rule: ty.induct) 378 (auto simp add: fresh_string) 379 380text \<open>Typing Contexts\<close> 381 382type_synonym tctx = "(name\<times>ty) list" 383 384text \<open>Sub-Typing Contexts\<close> 385 386abbreviation 387 "sub_tctx" :: "tctx \<Rightarrow> tctx \<Rightarrow> bool" ("_ \<subseteq> _") 388where 389 "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2" 390 391text \<open>Valid Typing Contexts\<close> 392 393inductive 394 valid :: "tctx \<Rightarrow> bool" 395where 396 v1[intro]: "valid []" 397| v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)" 398 399equivariance valid 400 401lemma valid_elim[dest]: 402 assumes a: "valid ((x,T)#\<Gamma>)" 403 shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>" 404using a by (cases) (auto) 405 406lemma valid_insert: 407 assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)" 408 shows "valid (\<Delta> @ \<Gamma>)" 409using a 410by (induct \<Delta>) 411 (auto simp add: fresh_list_append fresh_list_cons dest!: valid_elim) 412 413lemma fresh_set: 414 shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)" 415by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) 416 417lemma context_unique: 418 assumes a1: "valid \<Gamma>" 419 and a2: "(x,T) \<in> set \<Gamma>" 420 and a3: "(x,U) \<in> set \<Gamma>" 421 shows "T = U" 422using a1 a2 a3 423by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) 424 425section \<open>The Typing Relation\<close> 426 427inductive 428 typing :: "tctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 429where 430 t_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> VAR x : T" 431| 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" 432| 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" 433| t_NUM[intro]: "\<Gamma> \<turnstile> (NUM n) : tINT" 434| t_DIFF[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : tINT; \<Gamma> \<turnstile> t\<^sub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 -- t\<^sub>2 : tINT" 435| t_PLUS[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : tINT; \<Gamma> \<turnstile> t\<^sub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 ++ t\<^sub>2 : tINT" 436| t_TRUE[intro]: "\<Gamma> \<turnstile> TRUE : tBOOL" 437| t_FALSE[intro]: "\<Gamma> \<turnstile> FALSE : tBOOL" 438| t_IF[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : tBOOL; \<Gamma> \<turnstile> t2 : T; \<Gamma> \<turnstile> t3 : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> IF t1 t2 t3 : T" 439| t_ZET[intro]: "\<Gamma> \<turnstile> t : tINT \<Longrightarrow> \<Gamma> \<turnstile> ZET t : tBOOL" 440| t_EQI[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : tINT; \<Gamma> \<turnstile> t2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> EQI t1 t2 : tBOOL" 441| t_FIX[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T)#\<Gamma> \<turnstile> t : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> FIX [x].t : T" 442 443declare lam.inject[simp] 444inductive_cases typing_inversion[elim]: 445 "\<Gamma> \<turnstile> t\<^sub>1 -- t\<^sub>2 : T" 446 "\<Gamma> \<turnstile> t\<^sub>1 ++ t\<^sub>2 : T" 447 "\<Gamma> \<turnstile> IF t1 t2 t3 : T" 448 "\<Gamma> \<turnstile> ZET t : T" 449 "\<Gamma> \<turnstile> EQI t1 t2 : T" 450 "\<Gamma> \<turnstile> APP t1 t2 : T" 451 "\<Gamma> \<turnstile> TRUE : T" 452 "\<Gamma> \<turnstile> FALSE : T" 453 "\<Gamma> \<turnstile> NUM n : T" 454declare lam.inject[simp del] 455 456equivariance typing 457nominal_inductive typing 458 by (simp_all add: abs_fresh ty_fresh) 459 460lemma t_LAM_inversion[dest]: 461 assumes ty: "\<Gamma> \<turnstile> LAM [x].t : T" 462 and fc: "x\<sharp>\<Gamma>" 463 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" 464using ty fc 465by (cases rule: typing.strong_cases) 466 (auto simp add: alpha lam.inject abs_fresh ty_fresh) 467 468lemma t_FIX_inversion[dest]: 469 assumes ty: "\<Gamma> \<turnstile> FIX [x].t : T" 470 and fc: "x\<sharp>\<Gamma>" 471 shows "(x,T)#\<Gamma> \<turnstile> t : T" 472using ty fc 473by (cases rule: typing.strong_cases) 474 (auto simp add: alpha lam.inject abs_fresh ty_fresh) 475 476section \<open>The Type-Preservation Property for the CBV Reduction Relation\<close> 477 478lemma weakening: 479 fixes \<Gamma>1 \<Gamma>2::"tctx" 480 assumes a: "\<Gamma>1 \<turnstile> t : T" 481 and b: "valid \<Gamma>2" 482 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" 483 shows "\<Gamma>2 \<turnstile> t : T" 484using a b c 485by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) 486 (auto | atomize)+ 487 488lemma type_substitution_aux: 489 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" 490 and b: "\<Gamma> \<turnstile> e' : T'" 491 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 492using a b 493proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) 494 case (t_VAR y T x e' \<Delta>) 495 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 496 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 497 and a3: "\<Gamma> \<turnstile> e' : T'" . 498 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) 499 { assume eq: "x=y" 500 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) 501 with a3 have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using eq a4 by (auto intro: weakening) 502 } 503 moreover 504 { assume ineq: "x\<noteq>y" 505 from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp 506 then have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using ineq a4 by auto 507 } 508 ultimately show "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" by blast 509qed (auto | force simp add: fresh_list_append fresh_list_cons)+ 510 511corollary type_substitution: 512 assumes a: "(x,T')#\<Gamma> \<turnstile> e : T" 513 and b: "\<Gamma> \<turnstile> e' : T'" 514 shows "\<Gamma> \<turnstile> e[x::=e'] : T" 515using a b 516by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified]) 517 518theorem cbv_type_preservation: 519 assumes a: "t \<longrightarrow>cbv t'" 520 and b: "\<Gamma> \<turnstile> t : T" 521 shows "\<Gamma> \<turnstile> t' : T" 522using a b 523apply(nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) 524apply(auto elim!: typing_inversion dest: t_LAM_inversion simp add: type_substitution) 525apply(frule t_FIX_inversion) 526apply(auto simp add: type_substitution) 527done 528 529corollary cbv_star_type_preservation: 530 assumes a: "t \<longrightarrow>cbv* t'" 531 and b: "\<Gamma> \<turnstile> t : T" 532 shows "\<Gamma> \<turnstile> t' : T" 533using a b 534by (induct) (auto intro: cbv_type_preservation) 535 536section \<open>The Type-Preservation Property for the Machine and Evaluation Relation\<close> 537 538theorem machine_type_preservation: 539 assumes a: "<t,[]> \<mapsto>* <t',[]>" 540 and b: "\<Gamma> \<turnstile> t : T" 541 shows "\<Gamma> \<turnstile> t' : T" 542proof - 543 from a have "t \<longrightarrow>cbv* t'" by (simp add: machine_star_implies_cbv_star) 544 then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbv_star_type_preservation) 545qed 546 547theorem eval_type_preservation: 548 assumes a: "t \<Down> t'" 549 and b: "\<Gamma> \<turnstile> t : T" 550 shows "\<Gamma> \<turnstile> t' : T" 551proof - 552 from a have "<t,[]> \<mapsto>* <t',[]>" by (simp add: eval_implies_machine_star) 553 then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation) 554qed 555 556text \<open>The Progress Property\<close> 557 558lemma canonical_tARR[dest]: 559 assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2" 560 and b: "val t" 561 shows "\<exists>x t'. t = LAM [x].t'" 562using b a by (induct) (auto) 563 564lemma canonical_tINT[dest]: 565 assumes a: "[] \<turnstile> t : tINT" 566 and b: "val t" 567 shows "\<exists>n. t = NUM n" 568using b a 569by (induct) (auto simp add: fresh_list_nil) 570 571lemma canonical_tBOOL[dest]: 572 assumes a: "[] \<turnstile> t : tBOOL" 573 and b: "val t" 574 shows "t = TRUE \<or> t = FALSE" 575using b a 576by (induct) (auto simp add: fresh_list_nil) 577 578theorem progress: 579 assumes a: "[] \<turnstile> t : T" 580 shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)" 581using a 582by (induct \<Gamma>\<equiv>"[]::tctx" t T) 583 (auto dest!: canonical_tINT intro!: cbv.intros gr0I) 584 585end 586 587