diff -r 78d828f43cdf -r 4b4742aa43f2 Tutorial/Tutorial5.thy --- a/Tutorial/Tutorial5.thy Sat Dec 17 16:58:11 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,218 +0,0 @@ - - -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 \, \cbv* and the machine - correspond to each other, we only need to - prove this property for one of them. We chose - \cbv. - - First we need to establish two elimination - properties and two auxiliary lemmas about contexts. -*} - - -lemma valid_elim: - assumes a: "valid ((x, T) # \)" - shows "atom x \ \ \ valid \" -using a by (cases) (auto) - -lemma valid_insert: - assumes a: "valid (\ @ [(x, T)] @ \)" - shows "valid (\ @ \)" -using a -by (induct \) - (auto simp add: fresh_append fresh_Cons dest!: valid_elim) - -lemma fresh_list: - shows "atom y \ xs = (\x \ set xs. atom y \ x)" -by (induct xs) (simp_all add: fresh_Nil fresh_Cons) - -lemma context_unique: - assumes a1: "valid \" - and a2: "(x, T) \ set \" - and a3: "(x, U) \ set \" - 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: "\ @ [(x, T')] @ \ \ e : T" - and b: "\ \ e' : T'" - shows "\ @ \ \ e[x ::= e'] : T" -using a b -proof (nominal_induct \'\"\ @ [(x, T')] @ \" e T avoiding: x e' \ rule: typing.strong_induct) - case (t_Var y T x e' \) - have a1: "valid (\ @ [(x, T')] @ \)" by fact - have a2: "(y,T) \ set (\ @ [(x, T')] @ \)" by fact - have a3: "\ \ e' : T'" by fact - - from a1 have a4: "valid (\ @ \)" by (rule valid_insert) - { assume eq: "x = y" - - have "\ @ \ \ Var y[x ::= e'] : T" sorry - } - moreover - { assume ineq: "x \ y" - from a2 have "(y, T) \ set (\ @ \)" using ineq by simp - then have "\ @ \ \ Var y[x ::= e'] : T" using ineq a4 by auto - } - ultimately show "\ @ \ \ Var y[x::=e'] : T" by blast -next - case (t_Lam y T1 t T2 x e' \) - have a1: "atom y \ e'" by fact - have a2: "atom y \ \ @ [(x, T')] @ \" by fact - have a3: "\ \ e' : T'" by fact - have ih: "\ \ e' : T' \ ((y, T1) # \) @ \ \ t [x ::= e'] : T2" - using t_Lam(6)[of "(y, T1) # \"] by auto - - - show "\ @ \ \ (Lam [y]. t)[x ::= e'] : T1 \ T2" sorry -next - case (t_App t1 T1 T2 t2 x e' \) - have ih1: "\ \ e' : T' \ \ @ \ \ t1 [x ::= e'] : T1 \ T2" using t_App(2) by auto - have ih2: "\ \ e' : T' \ \ @ \ \ t2 [x ::= e'] : T1" using t_App(4) by auto - have a: "\ \ e' : T'" by fact - - show "\ @ \ \ 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') # \ \ e : T" - and b: "\ \ e' : T'" - shows "\ \ 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: "\ \ App t1 t2 : T" - obtains T' where "\ \ t1 : T' \ T" "\ \ 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: "\ \ Lam [x].t : T" - and fc: "atom x \ \" - obtains T1 T2 where "T = T1 \ T2" "(x, T1) # \ \ 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 \ 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 \cbv t'" - and b: "\ \ t : T" - shows "\ \ t' : T" -using a b -proof (nominal_induct avoiding: \ T rule: cbv.strong_induct) - case (cbv1 v x t \ T) - have fc: "atom x \ \" by fact - have "\ \ App (Lam [x]. t) v : T" by fact - then obtain T' where - *: "\ \ Lam [x]. t : T' \ T" and - **: "\ \ v : T'" by (rule t_App_elim) - have "(x, T') # \ \ t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff) - - show "\ \ 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 \cbv* t'" - and b: "\ \ t : T" - shows "\ \ 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: " \* " - and b: "\ \ t : T" - shows "\ \ t' : T" -proof - - have "t \cbv* t'" using a machines_implies_cbvs by simp - then show "\ \ t' : T" using b cbvs_type_preservation by simp -qed - -theorem eval_type_preservation: - assumes a: "t \ t'" - and b: "\ \ t : T" - shows "\ \ t' : T" -proof - - have " \* " using a eval_implies_machines by simp - then show "\ \ t' : T" using b machine_type_preservation by simp -qed - -text {* The Progress Property *} - -lemma canonical_tArr: - assumes a: "[] \ t : T1 \ T2" - and b: "val t" - obtains x t' where "t = Lam [x].t'" -using b a by (induct) (auto) - -theorem progress: - assumes a: "[] \ t : T" - shows "(\t'. t \cbv t') \ (val t)" -using a -by (induct \\"[]::ty_ctx" t T) - (auto elim: canonical_tArr simp add: val.simps) - -text {* - Done! Congratulations! -*} - -end -