--- a/Tutorial/Tutorial1.thy	Sat Jan 22 12:46:01 2011 -0600
+++ b/Tutorial/Tutorial1.thy	Sat Jan 22 15:07:36 2011 -0600
@@ -60,6 +60,7 @@
         \<bullet>    bullet    (permutation application)
 *}
 
+
 theory Tutorial1
 imports Lambda
 begin
@@ -460,13 +461,15 @@
 proof(induct)
   case (ms1 e1 Es1)
   have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
-  then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
+  
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
 next
   case (ms2 e1 Es1 e2 Es2 e2' Es2') 
   have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
   have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
   have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
-  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
+
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
 qed
 
 text {* 
@@ -584,41 +587,6 @@
 qed
 
 
-theorem 
-  assumes a: "t \<Down> t'"
-  shows "<t, Es> \<mapsto>* <t', Es>"
-using a 
-proof (induct arbitrary: Es)
-  case (e_Lam x t Es) 
-  -- {* no assumptions *}
-  show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto
-next
-  case (e_App t1 x t t2 v' v Es) 
-  -- {* all assumptions in this case *}
-  have a1: "t1 \<Down> Lam [x].t" by fact
-  have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact
-  have a2: "t2 \<Down> v'" by fact
-  have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact
-  have a3: "t[x::=v'] \<Down> v" by fact
-  have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact
-  -- {* your reasoning *}
-  have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto
-  moreover
-  have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto 
-  moreover
-  have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto
-  moreover
-  have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>" 
-  using ih2 by auto
-  moreover
-  have "val v'" using a2 eval_to_val by auto
-  then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto
-  moreover
-  have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto
-  ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast
-qed
-
-
 text {* 
   Again the automatic tools in Isabelle can discharge automatically 
   of the routine work in these proofs. We can write: 
@@ -637,7 +605,6 @@
 using a eval_implies_machines_ctx by simp
 
 
-
 section {* Function Definitions: Filling a Lambda-Term into a Context *}
  
 text {*
@@ -666,7 +633,7 @@
   by simp
 
 fun 
- ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99)
+ ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99)
 where
   "\<box> \<odot> E' = E'"
 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
@@ -715,11 +682,19 @@
   show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 qed
 
+
+subsection {* EXERCISE 6 *}
+
+text {*
+  Remove the sorries in the ctx_append proof below. You can make 
+  use of the following two properties.    
+*}
+
 lemma neut_hole:
   shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
 
-lemma odot_assoc: (* fixme call compose *)
+lemma compose_assoc:  
   shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 
@@ -735,7 +710,6 @@
   show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry
 qed
 
-
 text {* 
   The last proof involves several steps of equational reasoning.
   Isar provides some convenient means to express such equational 
@@ -743,7 +717,6 @@
   construction. 
 *}
 
-
 lemma 
   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
@@ -752,14 +725,14 @@
 next
   case (Cons E Es1)
   have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-  have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
+  have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
+  also have "\<dots> = (Es1 @ Es2)\<down> \<odot> E" by simp
   also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
-  also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using odot_assoc by simp
+  also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp
   also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
   finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
 qed
 
 
-
 end