1(* *) 2(* Formalisation of some typical SOS-proofs. *) 3(* *) 4(* This work was inspired by challenge suggested by Adam *) 5(* Chlipala on the POPLmark mailing list. *) 6(* *) 7(* We thank Nick Benton for helping us with the *) 8(* termination-proof for evaluation. *) 9(* *) 10(* The formalisation was done by Julien Narboux and *) 11(* Christian Urban. *) 12 13theory SOS 14 imports "HOL-Nominal.Nominal" 15begin 16 17atom_decl name 18 19text \<open>types and terms\<close> 20nominal_datatype ty = 21 TVar "nat" 22 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) 23 24nominal_datatype trm = 25 Var "name" 26 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 27 | App "trm" "trm" 28 29lemma fresh_ty: 30 fixes x::"name" 31 and T::"ty" 32 shows "x\<sharp>T" 33by (induct T rule: ty.induct) 34 (auto simp add: fresh_nat) 35 36text \<open>Parallel and single substitution.\<close> 37fun 38 lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" 39where 40 "lookup [] x = Var x" 41| "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)" 42 43lemma lookup_eqvt[eqvt]: 44 fixes pi::"name prm" 45 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" 46by (induct \<theta>) (auto simp add: eqvts) 47 48lemma lookup_fresh: 49 fixes z::"name" 50 assumes a: "z\<sharp>\<theta>" and b: "z\<sharp>x" 51 shows "z \<sharp>lookup \<theta> x" 52using a b 53by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) 54 55lemma lookup_fresh': 56 assumes "z\<sharp>\<theta>" 57 shows "lookup \<theta> z = Var z" 58using assms 59by (induct rule: lookup.induct) 60 (auto simp add: fresh_list_cons fresh_prod fresh_atm) 61 62(* parallel substitution *) 63 64nominal_primrec 65 psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [95,95] 105) 66where 67 "\<theta><(Var x)> = (lookup \<theta> x)" 68| "\<theta><(App e\<^sub>1 e\<^sub>2)> = App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>)" 69| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)" 70apply(finite_guess)+ 71apply(rule TrueI)+ 72apply(simp add: abs_fresh)+ 73apply(fresh_guess)+ 74done 75 76lemma psubst_eqvt[eqvt]: 77 fixes pi::"name prm" 78 and t::"trm" 79 shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>" 80by (nominal_induct t avoiding: \<theta> rule: trm.strong_induct) 81 (perm_simp add: fresh_bij lookup_eqvt)+ 82 83lemma fresh_psubst: 84 fixes z::"name" 85 and t::"trm" 86 assumes "z\<sharp>t" and "z\<sharp>\<theta>" 87 shows "z\<sharp>(\<theta><t>)" 88using assms 89by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct) 90 (auto simp add: abs_fresh lookup_fresh) 91 92lemma psubst_empty[simp]: 93 shows "[]<t> = t" 94 by (nominal_induct t rule: trm.strong_induct) 95 (auto simp add: fresh_list_nil) 96 97text \<open>Single substitution\<close> 98abbreviation 99 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) 100where 101 "t[x::=t'] \<equiv> ([(x,t')])<t>" 102 103lemma subst[simp]: 104 shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 105 and "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>2[y::=t'])" 106 and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 107by (simp_all add: fresh_list_cons fresh_list_nil) 108 109lemma fresh_subst: 110 fixes z::"name" 111 shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]" 112by (nominal_induct t avoiding: z y s rule: trm.strong_induct) 113 (auto simp add: abs_fresh fresh_prod fresh_atm) 114 115lemma forget: 116 assumes a: "x\<sharp>e" 117 shows "e[x::=e'] = e" 118using a 119by (nominal_induct e avoiding: x e' rule: trm.strong_induct) 120 (auto simp add: fresh_atm abs_fresh) 121 122lemma psubst_subst_psubst: 123 assumes h: "x\<sharp>\<theta>" 124 shows "\<theta><e>[x::=e'] = ((x,e')#\<theta>)<e>" 125 using h 126by (nominal_induct e avoiding: \<theta> x e' rule: trm.strong_induct) 127 (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh') 128 129text \<open>Typing Judgements\<close> 130 131inductive 132 valid :: "(name\<times>ty) list \<Rightarrow> bool" 133where 134 v_nil[intro]: "valid []" 135| v_cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((x,T)#\<Gamma>)" 136 137equivariance valid 138 139inductive_cases 140 valid_elim[elim]: "valid ((x,T)#\<Gamma>)" 141 142lemma valid_insert: 143 assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)" 144 shows "valid (\<Delta> @ \<Gamma>)" 145using a 146by (induct \<Delta>) 147 (auto simp add: fresh_list_append fresh_list_cons elim!: valid_elim) 148 149lemma fresh_set: 150 shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)" 151by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) 152 153lemma context_unique: 154 assumes a1: "valid \<Gamma>" 155 and a2: "(x,T) \<in> set \<Gamma>" 156 and a3: "(x,U) \<in> set \<Gamma>" 157 shows "T = U" 158using a1 a2 a3 159by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) 160 161text \<open>Typing Relation\<close> 162 163inductive 164 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 165where 166 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 167| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> e\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T\<^sub>2" 168| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> e : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T\<^sub>1\<rightarrow>T\<^sub>2" 169 170equivariance typing 171 172nominal_inductive typing 173 by (simp_all add: abs_fresh fresh_ty) 174 175lemma typing_implies_valid: 176 assumes a: "\<Gamma> \<turnstile> t : T" 177 shows "valid \<Gamma>" 178using a by (induct) (auto) 179 180 181lemma t_App_elim: 182 assumes a: "\<Gamma> \<turnstile> App t1 t2 : T" 183 obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> t2 : T'" 184using a 185by (cases) (auto simp add: trm.inject) 186 187lemma t_Lam_elim: 188 assumes a: "\<Gamma> \<turnstile> Lam [x].t : T" "x\<sharp>\<Gamma>" 189 obtains T\<^sub>1 and T\<^sub>2 where "(x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2" and "T=T\<^sub>1\<rightarrow>T\<^sub>2" 190using a 191by (cases rule: typing.strong_cases [where x="x"]) 192 (auto simp add: abs_fresh fresh_ty alpha trm.inject) 193 194abbreviation 195 "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [55,55] 55) 196where 197 "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>\<^sub>1 \<longrightarrow> (x,T)\<in>set \<Gamma>\<^sub>2" 198 199lemma weakening: 200 fixes \<Gamma>\<^sub>1 \<Gamma>\<^sub>2::"(name\<times>ty) list" 201 assumes "\<Gamma>\<^sub>1 \<turnstile> e: T" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2" 202 shows "\<Gamma>\<^sub>2 \<turnstile> e: T" 203 using assms 204proof(nominal_induct \<Gamma>\<^sub>1 e T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct) 205 case (t_Lam x \<Gamma>\<^sub>1 T\<^sub>1 t T\<^sub>2 \<Gamma>\<^sub>2) 206 have vc: "x\<sharp>\<Gamma>\<^sub>2" by fact 207 have ih: "\<lbrakk>valid ((x,T\<^sub>1)#\<Gamma>\<^sub>2); (x,T\<^sub>1)#\<Gamma>\<^sub>1 \<subseteq> (x,T\<^sub>1)#\<Gamma>\<^sub>2\<rbrakk> \<Longrightarrow> (x,T\<^sub>1)#\<Gamma>\<^sub>2 \<turnstile> t : T\<^sub>2" by fact 208 have "valid \<Gamma>\<^sub>2" by fact 209 then have "valid ((x,T\<^sub>1)#\<Gamma>\<^sub>2)" using vc by auto 210 moreover 211 have "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2" by fact 212 then have "(x,T\<^sub>1)#\<Gamma>\<^sub>1 \<subseteq> (x,T\<^sub>1)#\<Gamma>\<^sub>2" by simp 213 ultimately have "(x,T\<^sub>1)#\<Gamma>\<^sub>2 \<turnstile> t : T\<^sub>2" using ih by simp 214 with vc show "\<Gamma>\<^sub>2 \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" by auto 215qed (auto) 216 217lemma type_substitutivity_aux: 218 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" 219 and b: "\<Gamma> \<turnstile> e' : T'" 220 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 221using a b 222proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct) 223 case (t_Var y T e' \<Delta>) 224 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 225 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 226 and a3: "\<Gamma> \<turnstile> e' : T'" . 227 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) 228 { assume eq: "x=y" 229 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) 230 with a3 have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening) 231 } 232 moreover 233 { assume ineq: "x\<noteq>y" 234 from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp 235 then have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto 236 } 237 ultimately show "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" by blast 238qed (force simp add: fresh_list_append fresh_list_cons)+ 239 240corollary type_substitutivity: 241 assumes a: "(x,T')#\<Gamma> \<turnstile> e : T" 242 and b: "\<Gamma> \<turnstile> e' : T'" 243 shows "\<Gamma> \<turnstile> e[x::=e'] : T" 244using a b type_substitutivity_aux[where \<Delta>="[]"] 245by (auto) 246 247text \<open>Values\<close> 248inductive 249 val :: "trm\<Rightarrow>bool" 250where 251 v_Lam[intro]: "val (Lam [x].e)" 252 253equivariance val 254 255lemma not_val_App[simp]: 256 shows 257 "\<not> val (App e\<^sub>1 e\<^sub>2)" 258 "\<not> val (Var x)" 259 by (auto elim: val.cases) 260 261text \<open>Big-Step Evaluation\<close> 262 263inductive 264 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 265where 266 b_Lam[intro]: "Lam [x].e \<Down> Lam [x].e" 267| b_App[intro]: "\<lbrakk>x\<sharp>(e\<^sub>1,e\<^sub>2,e'); e\<^sub>1\<Down>Lam [x].e; e\<^sub>2\<Down>e\<^sub>2'; e[x::=e\<^sub>2']\<Down>e'\<rbrakk> \<Longrightarrow> App e\<^sub>1 e\<^sub>2 \<Down> e'" 268 269equivariance big 270 271nominal_inductive big 272 by (simp_all add: abs_fresh) 273 274lemma big_preserves_fresh: 275 fixes x::"name" 276 assumes a: "e \<Down> e'" "x\<sharp>e" 277 shows "x\<sharp>e'" 278 using a by (induct) (auto simp add: abs_fresh fresh_subst) 279 280lemma b_App_elim: 281 assumes a: "App e\<^sub>1 e\<^sub>2 \<Down> e'" "x\<sharp>(e\<^sub>1,e\<^sub>2,e')" 282 obtains f\<^sub>1 and f\<^sub>2 where "e\<^sub>1 \<Down> Lam [x]. f\<^sub>1" "e\<^sub>2 \<Down> f\<^sub>2" "f\<^sub>1[x::=f\<^sub>2] \<Down> e'" 283 using a 284by (cases rule: big.strong_cases[where x="x" and xa="x"]) 285 (auto simp add: trm.inject) 286 287lemma subject_reduction: 288 assumes a: "e \<Down> e'" and b: "\<Gamma> \<turnstile> e : T" 289 shows "\<Gamma> \<turnstile> e' : T" 290 using a b 291proof (nominal_induct avoiding: \<Gamma> arbitrary: T rule: big.strong_induct) 292 case (b_App x e\<^sub>1 e\<^sub>2 e' e e\<^sub>2' \<Gamma> T) 293 have vc: "x\<sharp>\<Gamma>" by fact 294 have "\<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T" by fact 295 then obtain T' where a1: "\<Gamma> \<turnstile> e\<^sub>1 : T'\<rightarrow>T" and a2: "\<Gamma> \<turnstile> e\<^sub>2 : T'" 296 by (cases) (auto simp add: trm.inject) 297 have ih1: "\<Gamma> \<turnstile> e\<^sub>1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].e : T' \<rightarrow> T" by fact 298 have ih2: "\<Gamma> \<turnstile> e\<^sub>2 : T' \<Longrightarrow> \<Gamma> \<turnstile> e\<^sub>2' : T'" by fact 299 have ih3: "\<Gamma> \<turnstile> e[x::=e\<^sub>2'] : T \<Longrightarrow> \<Gamma> \<turnstile> e' : T" by fact 300 have "\<Gamma> \<turnstile> Lam [x].e : T'\<rightarrow>T" using ih1 a1 by simp 301 then have "((x,T')#\<Gamma>) \<turnstile> e : T" using vc 302 by (auto elim: t_Lam_elim simp add: ty.inject) 303 moreover 304 have "\<Gamma> \<turnstile> e\<^sub>2': T'" using ih2 a2 by simp 305 ultimately have "\<Gamma> \<turnstile> e[x::=e\<^sub>2'] : T" by (simp add: type_substitutivity) 306 thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp 307qed (blast) 308 309lemma subject_reduction2: 310 assumes a: "e \<Down> e'" and b: "\<Gamma> \<turnstile> e : T" 311 shows "\<Gamma> \<turnstile> e' : T" 312 using a b 313by (nominal_induct avoiding: \<Gamma> T rule: big.strong_induct) 314 (force elim: t_App_elim t_Lam_elim simp add: ty.inject type_substitutivity)+ 315 316lemma unicity_of_evaluation: 317 assumes a: "e \<Down> e\<^sub>1" 318 and b: "e \<Down> e\<^sub>2" 319 shows "e\<^sub>1 = e\<^sub>2" 320 using a b 321proof (nominal_induct e e\<^sub>1 avoiding: e\<^sub>2 rule: big.strong_induct) 322 case (b_Lam x e t\<^sub>2) 323 have "Lam [x].e \<Down> t\<^sub>2" by fact 324 thus "Lam [x].e = t\<^sub>2" by cases (simp_all add: trm.inject) 325next 326 case (b_App x e\<^sub>1 e\<^sub>2 e' e\<^sub>1' e\<^sub>2' t\<^sub>2) 327 have ih1: "\<And>t. e\<^sub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^sub>1' = t" by fact 328 have ih2:"\<And>t. e\<^sub>2 \<Down> t \<Longrightarrow> e\<^sub>2' = t" by fact 329 have ih3: "\<And>t. e\<^sub>1'[x::=e\<^sub>2'] \<Down> t \<Longrightarrow> e' = t" by fact 330 have app: "App e\<^sub>1 e\<^sub>2 \<Down> t\<^sub>2" by fact 331 have vc: "x\<sharp>e\<^sub>1" "x\<sharp>e\<^sub>2" "x\<sharp>t\<^sub>2" by fact+ 332 then have "x\<sharp>App e\<^sub>1 e\<^sub>2" by auto 333 from app vc obtain f\<^sub>1 f\<^sub>2 where x1: "e\<^sub>1 \<Down> Lam [x]. f\<^sub>1" and x2: "e\<^sub>2 \<Down> f\<^sub>2" and x3: "f\<^sub>1[x::=f\<^sub>2] \<Down> t\<^sub>2" 334 by (auto elim!: b_App_elim) 335 then have "Lam [x]. f\<^sub>1 = Lam [x]. e\<^sub>1'" using ih1 by simp 336 then 337 have "f\<^sub>1 = e\<^sub>1'" by (auto simp add: trm.inject alpha) 338 moreover 339 have "f\<^sub>2 = e\<^sub>2'" using x2 ih2 by simp 340 ultimately have "e\<^sub>1'[x::=e\<^sub>2'] \<Down> t\<^sub>2" using x3 by simp 341 thus "e' = t\<^sub>2" using ih3 by simp 342qed 343 344lemma reduces_evaluates_to_values: 345 assumes h: "t \<Down> t'" 346 shows "val t'" 347using h by (induct) (auto) 348 349(* Valuation *) 350 351nominal_primrec 352 V :: "ty \<Rightarrow> trm set" 353where 354 "V (TVar x) = {e. val e}" 355| "V (T\<^sub>1 \<rightarrow> T\<^sub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^sub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2}" 356 by (rule TrueI)+ 357 358lemma V_eqvt: 359 fixes pi::"name prm" 360 assumes a: "x\<in>V T" 361 shows "(pi\<bullet>x)\<in>V T" 362using a 363apply(nominal_induct T arbitrary: pi x rule: ty.strong_induct) 364apply(auto simp add: trm.inject) 365apply(simp add: eqvts) 366apply(rule_tac x="pi\<bullet>xa" in exI) 367apply(rule_tac x="pi\<bullet>e" in exI) 368apply(simp) 369apply(auto) 370apply(drule_tac x="(rev pi)\<bullet>v" in bspec) 371apply(force) 372apply(auto) 373apply(rule_tac x="pi\<bullet>v'" in exI) 374apply(auto) 375apply(drule_tac pi="pi" in big.eqvt) 376apply(perm_simp add: eqvts) 377done 378 379lemma V_arrow_elim_weak: 380 assumes h:"u \<in> V (T\<^sub>1 \<rightarrow> T\<^sub>2)" 381 obtains a t where "u = Lam [a].t" and "\<forall> v \<in> (V T\<^sub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2" 382using h by (auto) 383 384lemma V_arrow_elim_strong: 385 fixes c::"'a::fs_name" 386 assumes h: "u \<in> V (T\<^sub>1 \<rightarrow> T\<^sub>2)" 387 obtains a t where "a\<sharp>c" "u = Lam [a].t" "\<forall>v \<in> (V T\<^sub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2" 388using h 389apply - 390apply(erule V_arrow_elim_weak) 391apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(a,t,c)") (*A*) 392apply(erule exE) 393apply(drule_tac x="a'" in meta_spec) 394apply(drule_tac x="[(a,a')]\<bullet>t" in meta_spec) 395apply(drule meta_mp) 396apply(simp) 397apply(drule meta_mp) 398apply(simp add: trm.inject alpha fresh_left fresh_prod calc_atm fresh_atm) 399apply(perm_simp) 400apply(force) 401apply(drule meta_mp) 402apply(rule ballI) 403apply(drule_tac x="[(a,a')]\<bullet>v" in bspec) 404apply(simp add: V_eqvt) 405apply(auto) 406apply(rule_tac x="[(a,a')]\<bullet>v'" in exI) 407apply(auto) 408apply(drule_tac pi="[(a,a')]" in big.eqvt) 409apply(perm_simp add: eqvts calc_atm) 410apply(simp add: V_eqvt) 411(*A*) 412apply(rule exists_fresh') 413apply(simp add: fin_supp) 414done 415 416lemma Vs_are_values: 417 assumes a: "e \<in> V T" 418 shows "val e" 419using a by (nominal_induct T arbitrary: e rule: ty.strong_induct) (auto) 420 421lemma values_reduce_to_themselves: 422 assumes a: "val v" 423 shows "v \<Down> v" 424using a by (induct) (auto) 425 426lemma Vs_reduce_to_themselves: 427 assumes a: "v \<in> V T" 428 shows "v \<Down> v" 429using a by (simp add: values_reduce_to_themselves Vs_are_values) 430 431text \<open>'\<theta> maps x to e' asserts that \<theta> substitutes x with e\<close> 432abbreviation 433 mapsto :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55) 434where 435 "\<theta> maps x to e \<equiv> (lookup \<theta> x) = e" 436 437abbreviation 438 v_closes :: "(name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ Vcloses _" [55,55] 55) 439where 440 "\<theta> Vcloses \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> (\<exists>v. \<theta> maps x to v \<and> v \<in> V T)" 441 442lemma case_distinction_on_context: 443 fixes \<Gamma>::"(name\<times>ty) list" 444 assumes asm1: "valid ((m,t)#\<Gamma>)" 445 and asm2: "(n,U) \<in> set ((m,T)#\<Gamma>)" 446 shows "(n,U) = (m,T) \<or> ((n,U) \<in> set \<Gamma> \<and> n \<noteq> m)" 447proof - 448 from asm2 have "(n,U) \<in> set [(m,T)] \<or> (n,U) \<in> set \<Gamma>" by auto 449 moreover 450 { assume eq: "m=n" 451 assume "(n,U) \<in> set \<Gamma>" 452 then have "\<not> n\<sharp>\<Gamma>" 453 by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm) 454 moreover have "m\<sharp>\<Gamma>" using asm1 by auto 455 ultimately have False using eq by auto 456 } 457 ultimately show ?thesis by auto 458qed 459 460lemma monotonicity: 461 fixes m::"name" 462 fixes \<theta>::"(name \<times> trm) list" 463 assumes h1: "\<theta> Vcloses \<Gamma>" 464 and h2: "e \<in> V T" 465 and h3: "valid ((x,T)#\<Gamma>)" 466 shows "(x,e)#\<theta> Vcloses (x,T)#\<Gamma>" 467proof(intro strip) 468 fix x' T' 469 assume "(x',T') \<in> set ((x,T)#\<Gamma>)" 470 then have "((x',T')=(x,T)) \<or> ((x',T')\<in>set \<Gamma> \<and> x'\<noteq>x)" using h3 471 by (rule_tac case_distinction_on_context) 472 moreover 473 { (* first case *) 474 assume "(x',T') = (x,T)" 475 then have "\<exists>e'. ((x,e)#\<theta>) maps x to e' \<and> e' \<in> V T'" using h2 by auto 476 } 477 moreover 478 { (* second case *) 479 assume "(x',T') \<in> set \<Gamma>" and neq:"x' \<noteq> x" 480 then have "\<exists>e'. \<theta> maps x' to e' \<and> e' \<in> V T'" using h1 by auto 481 then have "\<exists>e'. ((x,e)#\<theta>) maps x' to e' \<and> e' \<in> V T'" using neq by auto 482 } 483 ultimately show "\<exists>e'. ((x,e)#\<theta>) maps x' to e' \<and> e' \<in> V T'" by blast 484qed 485 486lemma termination_aux: 487 assumes h1: "\<Gamma> \<turnstile> e : T" 488 and h2: "\<theta> Vcloses \<Gamma>" 489 shows "\<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" 490using h2 h1 491proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.strong_induct) 492 case (App e\<^sub>1 e\<^sub>2 \<Gamma> \<theta> T) 493 have ih\<^sub>1: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^sub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^sub>1> \<Down> v \<and> v \<in> V T" by fact 494 have ih\<^sub>2: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^sub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^sub>2> \<Down> v \<and> v \<in> V T" by fact 495 have as\<^sub>1: "\<theta> Vcloses \<Gamma>" by fact 496 have as\<^sub>2: "\<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T" by fact 497 then obtain T' where "\<Gamma> \<turnstile> e\<^sub>1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> e\<^sub>2 : T'" by (auto elim: t_App_elim) 498 then obtain v\<^sub>1 v\<^sub>2 where "(i)": "\<theta><e\<^sub>1> \<Down> v\<^sub>1" "v\<^sub>1 \<in> V (T' \<rightarrow> T)" 499 and "(ii)": "\<theta><e\<^sub>2> \<Down> v\<^sub>2" "v\<^sub>2 \<in> V T'" using ih\<^sub>1 ih\<^sub>2 as\<^sub>1 by blast 500 from "(i)" obtain x e' 501 where "v\<^sub>1 = Lam [x].e'" 502 and "(iii)": "(\<forall>v \<in> (V T').\<exists> v'. e'[x::=v] \<Down> v' \<and> v' \<in> V T)" 503 and "(iv)": "\<theta><e\<^sub>1> \<Down> Lam [x].e'" 504 and fr: "x\<sharp>(\<theta>,e\<^sub>1,e\<^sub>2)" by (blast elim: V_arrow_elim_strong) 505 from fr have fr\<^sub>1: "x\<sharp>\<theta><e\<^sub>1>" and fr\<^sub>2: "x\<sharp>\<theta><e\<^sub>2>" by (simp_all add: fresh_psubst) 506 from "(ii)" "(iii)" obtain v\<^sub>3 where "(v)": "e'[x::=v\<^sub>2] \<Down> v\<^sub>3" "v\<^sub>3 \<in> V T" by auto 507 from fr\<^sub>2 "(ii)" have "x\<sharp>v\<^sub>2" by (simp add: big_preserves_fresh) 508 then have "x\<sharp>e'[x::=v\<^sub>2]" by (simp add: fresh_subst) 509 then have fr\<^sub>3: "x\<sharp>v\<^sub>3" using "(v)" by (simp add: big_preserves_fresh) 510 from fr\<^sub>1 fr\<^sub>2 fr\<^sub>3 have "x\<sharp>(\<theta><e\<^sub>1>,\<theta><e\<^sub>2>,v\<^sub>3)" by simp 511 with "(iv)" "(ii)" "(v)" have "App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>) \<Down> v\<^sub>3" by auto 512 then show "\<exists>v. \<theta><App e\<^sub>1 e\<^sub>2> \<Down> v \<and> v \<in> V T" using "(v)" by auto 513next 514 case (Lam x e \<Gamma> \<theta> T) 515 have ih:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" by fact 516 have as\<^sub>1: "\<theta> Vcloses \<Gamma>" by fact 517 have as\<^sub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact 518 have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact+ 519 from as\<^sub>2 fs obtain T\<^sub>1 T\<^sub>2 520 where "(i)": "(x,T\<^sub>1)#\<Gamma> \<turnstile> e:T\<^sub>2" and "(ii)": "T = T\<^sub>1 \<rightarrow> T\<^sub>2" using fs 521 by (auto elim: t_Lam_elim) 522 from "(i)" have "(iii)": "valid ((x,T\<^sub>1)#\<Gamma>)" by (simp add: typing_implies_valid) 523 have "\<forall>v \<in> (V T\<^sub>1). \<exists>v'. (\<theta><e>)[x::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2" 524 proof 525 fix v 526 assume "v \<in> (V T\<^sub>1)" 527 with "(iii)" as\<^sub>1 have "(x,v)#\<theta> Vcloses (x,T\<^sub>1)#\<Gamma>" using monotonicity by auto 528 with ih "(i)" obtain v' where "((x,v)#\<theta>)<e> \<Down> v' \<and> v' \<in> V T\<^sub>2" by blast 529 then have "\<theta><e>[x::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2" using fs by (simp add: psubst_subst_psubst) 530 then show "\<exists>v'. \<theta><e>[x::=v] \<Down> v' \<and> v' \<in> V T\<^sub>2" by auto 531 qed 532 then have "Lam[x].\<theta><e> \<in> V (T\<^sub>1 \<rightarrow> T\<^sub>2)" by auto 533 then have "\<theta><Lam [x].e> \<Down> Lam [x].\<theta><e> \<and> Lam [x].\<theta><e> \<in> V (T\<^sub>1\<rightarrow>T\<^sub>2)" using fs by auto 534 thus "\<exists>v. \<theta><Lam [x].e> \<Down> v \<and> v \<in> V T" using "(ii)" by auto 535next 536 case (Var x \<Gamma> \<theta> T) 537 have "\<Gamma> \<turnstile> (Var x) : T" by fact 538 then have "(x,T)\<in>set \<Gamma>" by (cases) (auto simp add: trm.inject) 539 with Var have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T" 540 by (auto intro!: Vs_reduce_to_themselves) 541 then show "\<exists>v. \<theta><Var x> \<Down> v \<and> v \<in> V T" by auto 542qed 543 544theorem termination_of_evaluation: 545 assumes a: "[] \<turnstile> e : T" 546 shows "\<exists>v. e \<Down> v \<and> val v" 547proof - 548 from a have "\<exists>v. []<e> \<Down> v \<and> v \<in> V T" by (rule termination_aux) (auto) 549 thus "\<exists>v. e \<Down> v \<and> val v" using Vs_are_values by auto 550qed 551 552end 553