1 

     2 

     3 theory Tutorial5

     4 imports Tutorial4

     5 begin

     6 

     7 section {* Type-Preservation and Progress Lemma*}

     8 

     9 text {*

    10   The point of this tutorial is to prove the

    11   type-preservation and progress lemma. Since

    12   we now know that \<Down>, \<longrightarrow>cbv* and the machine

    13   correspond to each other, we only need to

    14   prove this property for one of them. We chose

    15   \<longrightarrow>cbv.

    16 

    17   First we need to establish two elimination

    18   properties and two auxiliary lemmas about contexts.

    19 *}

    20 

    21 

    22 lemma valid_elim:

    23   assumes a: "valid ((x, T) # \<Gamma>)"

    24   shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"

    25 using a by (cases) (auto)

    26 

    27 lemma valid_insert:

    28   assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"

    29   shows "valid (\<Delta> @ \<Gamma>)" 

    30 using a

    31 by (induct \<Delta>)

    32    (auto simp add: fresh_append fresh_Cons dest!: valid_elim)

    33 

    34 lemma fresh_list: 

    35   shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"

    36 by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

    37 

    38 lemma context_unique:

    39   assumes a1: "valid \<Gamma>"

    40   and     a2: "(x, T) \<in> set \<Gamma>"

    41   and     a3: "(x, U) \<in> set \<Gamma>"

    42   shows "T = U" 

    43 using a1 a2 a3

    44 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)

    45 

    46 

    47 section {* EXERCISE 16 *}

    48 

    49 text {*

    50   Next we want to show the type substitution lemma. Unfortunately,

    51   we have to prove a slightly more general version of it, where

    52   the variable being substituted occurs somewhere inside the 

    53   context.

    54 *}

    55 

    56 lemma type_substitution_aux:

    57   assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"

    58   and     b: "\<Gamma> \<turnstile> e' : T'"

    59   shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" 

    60 using a b 

    61 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)

    62   case (t_Var y T x e' \<Delta>)

    63   have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact

    64   have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 

    65   have a3: "\<Gamma> \<turnstile> e' : T'" by fact

    66   

    67   from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)

    68   { assume eq: "x = y"

    69     

    70     have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry

    71   }

    72   moreover

    73   { assume ineq: "x \<noteq> y"

    74     from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp

    75     then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto

    76   }

    77   ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast

    78 next

    79   case (t_Lam y T1 t T2 x e' \<Delta>)

    80   have a1: "atom y \<sharp> e'" by fact

    81   have a2: "atom y \<sharp> \<Delta> @ [(x, T')] @ \<Gamma>" by fact

    82   have a3: "\<Gamma> \<turnstile> e' : T'" by fact 

    83   have ih: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> ((y, T1) # \<Delta>) @ \<Gamma> \<turnstile> t [x ::= e'] : T2" 

    84     using t_Lam(6)[of "(y, T1) # \<Delta>"] by auto 

    85   

    86 

    87   show "\<Delta> @ \<Gamma> \<turnstile> (Lam [y]. t)[x ::= e'] : T1 \<rightarrow> T2" sorry

    88 next

    89   case (t_App t1 T1 T2 t2 x e' \<Delta>)

    90   have ih1: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t1 [x ::= e'] : T1 \<rightarrow> T2" using t_App(2) by auto 

    91   have ih2: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t2 [x ::= e'] : T1" using t_App(4) by auto 

    92   have a: "\<Gamma> \<turnstile> e' : T'" by fact

    93 

    94   show "\<Delta> @ \<Gamma> \<turnstile> App t1 t2 [x ::= e'] : T2" sorry

    95 qed 

    96 

    97 text {*

    98   From this we can derive the usual version of the substitution

    99   lemma.

   100 *}

   101 

   102 corollary type_substitution:

   103   assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"

   104   and     b: "\<Gamma> \<turnstile> e' : T'"

   105   shows "\<Gamma> \<turnstile> e[x ::= e'] : T"

   106 using a b type_substitution_aux[of "[]"]

   107 by auto

   108 

   109 

   110 section {* Type Preservation *}

   111 

   112 text {*

   113   Finally we are in a position to establish the type preservation

   114   property. We just need the following two inversion rules for

   115   particualr typing instances.

   116 *}

   117 

   118 lemma t_App_elim:

   119   assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"

   120   obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"

   121 using a

   122 by (cases) (auto simp add: lam.eq_iff lam.distinct)

   123 

   124 text {* we have not yet generated strong elimination rules *}

   125 lemma t_Lam_elim:

   126   assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 

   127   and     fc: "atom x \<sharp> \<Gamma>" 

   128   obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"

   129 using ty fc

   130 apply(cases)

   131 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)

   132 apply(auto simp add: Abs1_eq_iff)

   133 apply(rotate_tac 3)

   134 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)

   135 apply(perm_simp)

   136 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)

   137 done

   138 

   139 

   140 section {* EXERCISE 17 *}

   141 

   142 text {*

   143   Fill in the gaps in the t_Lam case. You will need

   144   the type substitution lemma proved above. 

   145 *}

   146 

   147 theorem cbv_type_preservation:

   148   assumes a: "t \<longrightarrow>cbv t'"

   149   and     b: "\<Gamma> \<turnstile> t : T" 

   150   shows "\<Gamma> \<turnstile> t' : T"

   151 using a b

   152 proof (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)

   153   case (cbv1 v x t \<Gamma> T) 

   154   have fc: "atom x \<sharp> \<Gamma>" by fact

   155   have "\<Gamma> \<turnstile> App (Lam [x]. t) v : T" by fact

   156   then obtain T' where 

   157       *: "\<Gamma> \<turnstile> Lam [x]. t : T' \<rightarrow> T" and 

   158      **: "\<Gamma> \<turnstile> v : T'" by (rule t_App_elim)

   159   have "(x, T') # \<Gamma> \<turnstile> t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff)

   160 

   161   show "\<Gamma> \<turnstile> t [x ::= v] : T " sorry

   162 qed (auto elim!: t_App_elim)

   163 

   164 text {*

   165   We can easily extend this to sequences of cbv* reductions.

   166 *}

   167 

   168 corollary cbvs_type_preservation:

   169   assumes a: "t \<longrightarrow>cbv* t'"

   170   and     b: "\<Gamma> \<turnstile> t : T" 

   171   shows "\<Gamma> \<turnstile> t' : T"

   172 using a b

   173 by (induct) (auto intro: cbv_type_preservation)

   174 

   175 text {* 

   176   The type-preservation property for the machine and 

   177   evaluation relation. 

   178 *}

   179 

   180 theorem machine_type_preservation:

   181   assumes a: "<t, []> \<mapsto>* <t', []>"

   182   and     b: "\<Gamma> \<turnstile> t : T" 

   183   shows "\<Gamma> \<turnstile> t' : T"

   184 proof -

   185   have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp

   186   then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp

   187 qed

   188 

   189 theorem eval_type_preservation:

   190   assumes a: "t \<Down> t'"

   191   and     b: "\<Gamma> \<turnstile> t : T" 

   192   shows "\<Gamma> \<turnstile> t' : T"

   193 proof -

   194   have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp

   195   then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp

   196 qed

   197 

   198 text {* The Progress Property *}

   199 

   200 lemma canonical_tArr:

   201   assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"

   202   and     b: "val t"

   203   obtains x t' where "t = Lam [x].t'"

   204 using b a by (induct) (auto) 

   205 

   206 theorem progress:

   207   assumes a: "[] \<turnstile> t : T"

   208   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

   209 using a

   210 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

   211    (auto elim: canonical_tArr simp add: val.simps)

   212 

   213 text {*

   214   Done! Congratulations!

   215 *}

   216 

   217 end

   218