added notes by referees to comment about our changes
theory Tutorial5imports Tutorial4beginsection {* Type-Preservation and Progress Lemma*}text {* The point of this tutorial is to prove the type-preservation and progress lemma. Since we now know that \<Down>, \<longrightarrow>cbv* and the machine correspond to each other, we only need to prove this property for one of them. We chose \<longrightarrow>cbv. First we need to establish two elimination properties and two auxiliary lemmas about contexts.*}lemma valid_elim: assumes a: "valid ((x, T) # \<Gamma>)" shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"using a by (cases) (auto)lemma valid_insert: assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)" shows "valid (\<Delta> @ \<Gamma>)" using aby (induct \<Delta>) (auto simp add: fresh_append fresh_Cons dest!: valid_elim)lemma fresh_list: shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"by (induct xs) (simp_all add: fresh_Nil fresh_Cons)lemma context_unique: assumes a1: "valid \<Gamma>" and a2: "(x, T) \<in> set \<Gamma>" and a3: "(x, U) \<in> set \<Gamma>" shows "T = U" using a1 a2 a3by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)section {* EXERCISE 16 *}text {* Next we want to show the type substitution lemma. Unfortunately, we have to prove a slightly more general version of it, where the variable being substituted occurs somewhere inside the context.*}lemma type_substitution_aux: assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T" and b: "\<Gamma> \<turnstile> e' : T'" shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" using a b proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) case (t_Var y T x e' \<Delta>) have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact have a3: "\<Gamma> \<turnstile> e' : T'" by fact from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert) { assume eq: "x = y" have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry } moreover { assume ineq: "x \<noteq> y" from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto } ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blastnext case (t_Lam y T1 t T2 x e' \<Delta>) have a1: "atom y \<sharp> e'" by fact have a2: "atom y \<sharp> \<Delta> @ [(x, T')] @ \<Gamma>" by fact have a3: "\<Gamma> \<turnstile> e' : T'" by fact have ih: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> ((y, T1) # \<Delta>) @ \<Gamma> \<turnstile> t [x ::= e'] : T2" using t_Lam(6)[of "(y, T1) # \<Delta>"] by auto show "\<Delta> @ \<Gamma> \<turnstile> (Lam [y]. t)[x ::= e'] : T1 \<rightarrow> T2" sorrynext case (t_App t1 T1 T2 t2 x e' \<Delta>) have ih1: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t1 [x ::= e'] : T1 \<rightarrow> T2" using t_App(2) by auto have ih2: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t2 [x ::= e'] : T1" using t_App(4) by auto have a: "\<Gamma> \<turnstile> e' : T'" by fact show "\<Delta> @ \<Gamma> \<turnstile> App t1 t2 [x ::= e'] : T2" sorryqed text {* From this we can derive the usual version of the substitution lemma.*}corollary type_substitution: assumes a: "(x, T') # \<Gamma> \<turnstile> e : T" and b: "\<Gamma> \<turnstile> e' : T'" shows "\<Gamma> \<turnstile> e[x ::= e'] : T"using a b type_substitution_aux[of "[]"]by autosection {* Type Preservation *}text {* Finally we are in a position to establish the type preservation property. We just need the following two inversion rules for particualr typing instances.*}lemma t_App_elim: assumes a: "\<Gamma> \<turnstile> App t1 t2 : T" obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"using aby (cases) (auto simp add: lam.eq_iff lam.distinct)text {* we have not yet generated strong elimination rules *}lemma t_Lam_elim: assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" and fc: "atom x \<sharp> \<Gamma>" obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"using ty fcapply(cases)apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)apply(auto simp add: Abs1_eq_iff)apply(rotate_tac 3)apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)apply(perm_simp)apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)donesection {* EXERCISE 17 *}text {* Fill in the gaps in the t_Lam case. You will need the type substitution lemma proved above. *}theorem cbv_type_preservation: assumes a: "t \<longrightarrow>cbv t'" and b: "\<Gamma> \<turnstile> t : T" shows "\<Gamma> \<turnstile> t' : T"using a bproof (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) case (cbv1 v x t \<Gamma> T) have fc: "atom x \<sharp> \<Gamma>" by fact have "\<Gamma> \<turnstile> App (Lam [x]. t) v : T" by fact then obtain T' where *: "\<Gamma> \<turnstile> Lam [x]. t : T' \<rightarrow> T" and **: "\<Gamma> \<turnstile> v : T'" by (rule t_App_elim) have "(x, T') # \<Gamma> \<turnstile> t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff) show "\<Gamma> \<turnstile> t [x ::= v] : T " sorryqed (auto elim!: t_App_elim)text {* We can easily extend this to sequences of cbv* reductions.*}corollary cbvs_type_preservation: assumes a: "t \<longrightarrow>cbv* t'" and b: "\<Gamma> \<turnstile> t : T" shows "\<Gamma> \<turnstile> t' : T"using a bby (induct) (auto intro: cbv_type_preservation)text {* The type-preservation property for the machine and evaluation relation. *}theorem machine_type_preservation: assumes a: "<t, []> \<mapsto>* <t', []>" and b: "\<Gamma> \<turnstile> t : T" shows "\<Gamma> \<turnstile> t' : T"proof - have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simpqedtheorem eval_type_preservation: assumes a: "t \<Down> t'" and b: "\<Gamma> \<turnstile> t : T" shows "\<Gamma> \<turnstile> t' : T"proof - have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simpqedtext {* The Progress Property *}lemma canonical_tArr: assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2" and b: "val t" obtains x t' where "t = Lam [x].t'"using b a by (induct) (auto) theorem progress: assumes a: "[] \<turnstile> t : T" shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"using aby (induct \<Gamma>\<equiv>"[]::ty_ctx" t T) (auto elim: canonical_tArr simp add: val.simps)text {* Done! Congratulations!*}end