--- a/Tutorial/Tutorial5.thy	Sat Jan 22 16:37:00 2011 -0600
+++ b/Tutorial/Tutorial5.thy	Sat Jan 22 18:59:48 2011 -0600
@@ -1,9 +1,22 @@
+
+
 theory Tutorial5
 imports Tutorial4
 begin
 
+section {* Type-Preservation and Progress Lemma*}
 
-section {* Type Preservation (fixme separate file) *}
+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:
@@ -30,6 +43,16 @@
 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'"
@@ -40,10 +63,11 @@
   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"
-    from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
-    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)
+    
+    have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry
   }
   moreover
   { assume ineq: "x \<noteq> y"
@@ -51,15 +75,46 @@
     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
-qed (force simp add: fresh_append fresh_Cons)+
+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[where \<Delta>="[]"]
+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'"
@@ -81,13 +136,34 @@
 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
-by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
-   (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+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'"