--- a/Tutorial/Tutorial4.thy	Fri Jan 21 22:58:03 2011 +0100
+++ b/Tutorial/Tutorial4.thy	Sat Jan 22 12:46:01 2011 -0600
@@ -5,18 +5,62 @@
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
 
+
+inductive
+  cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 
+where
+  cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
+| cbv2: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
+| cbv3: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
+
+inductive 
+  "cbv_star" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
+where
+  cbvs1: "e \<longrightarrow>cbv* e"
+| cbvs2: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+declare cbv.intros[intro] cbv_star.intros[intro]
+
+subsection {* EXERCISE 3 *}
+
+text {*
+  Show that cbv* is transitive, by filling the gaps in the 
+  proof below.
+*}
+
+lemma 
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a 
+proof (induct) 
+  case (cbvs1 e1)
+  have asm: "e1 \<longrightarrow>cbv* e3" by fact
+  show "e1 \<longrightarrow>cbv* e3" sorry
+next
+  case (cbvs2 e1 e2 e3')
+  have "e1 \<longrightarrow>cbv e2" by fact
+  have "e2 \<longrightarrow>cbv* e3'" by fact
+  have "e3' \<longrightarrow>cbv* e3 \<Longrightarrow> e2 \<longrightarrow>cbv* e3" by fact
+  have "e3' \<longrightarrow>cbv* e3" by fact
+
+  show "e1 \<longrightarrow>cbv* e3" sorry
+qed 
+
+lemma cbvs3 [intro]:
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a by (induct) (auto) 
+
+
+
+
+
 text {*
   In order to help establishing the property that the CK Machine
   calculates a nomrmalform that corresponds to the evaluation 
   relation, we introduce the call-by-value small-step semantics.
 *}
 
-inductive
-  cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 
-where
-  cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
-| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
-| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
 
 equivariance val
 equivariance cbv
@@ -44,7 +88,7 @@
 
 lemma better_cbv1 [intro]: 
   assumes a: "val v" 
-  shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
+  shows "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
 proof -
   obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)
   have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs
@@ -58,16 +102,8 @@
   The transitive closure of the cbv-reduction relation: 
 *}
 
-inductive 
-  "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
-where
-  cbvs1[intro]: "e \<longrightarrow>cbv* e"
-| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
 
-lemma cbvs3 [intro]:
-  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
-  shows "e1 \<longrightarrow>cbv* e3"
-using a by (induct) (auto) 
+
 
 
 subsection {* EXERCISE 8 *}