--- a/Tutorial/Tutorial5.thy Tue Feb 19 05:38:46 2013 +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 \<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)
-using [[simproc del: alpha_lst]]
-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_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
-