+
−
+
−
theory Tutorial5+
−
imports Tutorial4+
−
begin+
−
+
−
section {* 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 a+
−
by (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 a3+
−
by (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 blast+
−
next+
−
  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" sorry+
−
next+
−
  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" sorry+
−
qed +
−
+
−
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 auto+
−
+
−
+
−
section {* 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 a+
−
by (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 fc+
−
apply(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)+
−
done+
−
+
−
+
−
section {* 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 b+
−
proof (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 " sorry+
−
qed (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 b+
−
by (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 simp+
−
qed+
−
+
−
theorem 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 simp+
−
qed+
−
+
−
text {* 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 a+
−
by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)+
−
   (auto elim: canonical_tArr simp add: val.simps)+
−
+
−
text {*+
−
  Done! Congratulations!+
−
*}+
−
+
−
end+
−
+
−