diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial4.thy
--- a/Tutorial/Tutorial4.thy	Tue Jan 25 02:46:05 2011 +0900
+++ b/Tutorial/Tutorial4.thy	Tue Jan 25 02:51:44 2011 +0900
@@ -1,22 +1,58 @@
 
 theory Tutorial4
-imports Tutorial1 Tutorial2 Tutorial3
+imports Tutorial1 Tutorial2
 begin
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
 
-text {*
-  In order to help establishing the property that the Machine
-  calculates a normal form 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'"
+| 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 11 *}
+
+text {*
+  Show that cbv* is transitive, by filling the gaps in the 
+  proof below.
+*}
+
+lemma cbvs3 [intro]:
+  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 
+
+
+text {*
+  In order to help establishing the property that the machine
+  calculates a normal form that corresponds to the evaluation 
+  relation, we introduce the call-by-value small-step semantics.
+*}
+
 
 equivariance val
 equivariance cbv
@@ -44,7 +80,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
@@ -54,23 +90,9 @@
   finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
 qed
 
-text {*
-  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 *}
+subsection {* EXERCISE 12 *}
 
 text {*  
   If more simple exercises are needed, then complete the following proof. 
@@ -83,26 +105,22 @@
 proof (induct E)
   case Hole
   have "t \<longrightarrow>cbv t'" by fact
-  then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" by simp
+  show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" sorry
 next
   case (CAppL E s)
   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
-  moreover
   have "t \<longrightarrow>cbv t'" by fact
-  ultimately 
-  have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
-  then show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" by auto
+
+  show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" sorry
 next
   case (CAppR s E)
   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
-  moreover
   have a: "t \<longrightarrow>cbv t'" by fact
-  ultimately 
-  have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
-  then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto
+  
+  show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry
 qed
 
-section {* EXERCISE 9 *} 
+section {* EXERCISE 13 *} 
  
 text {*
   The point of the cbv-reduction was that we can easily relatively 
@@ -131,7 +149,8 @@
 
 text {* 
   It is not difficult to extend the lemma above to
-  arbitrary reductions sequences of the CK machine. *}
+  arbitrary reductions sequences of the machine. 
+*}
 
 lemma machines_implies_cbvs_ctx:
   assumes a: "<e, Es> \<mapsto>* <e', Es'>"
@@ -140,7 +159,7 @@
 by (induct) (blast)+
 
 text {* 
-  So whenever we let the CL machine start in an initial
+  So whenever we let the machine start in an initial
   state and it arrives at a final state, then there exists
   a corresponding cbv-reduction sequence. 
 *}
@@ -156,14 +175,10 @@
 
 text {*
   We now want to relate the cbv-reduction to the evaluation
-  relation. For this we need two auxiliary lemmas. 
+  relation. For this we need one auxiliary lemma about
+  inverting the e_App rule. 
 *}
 
-lemma eval_val:
-  assumes a: "val t"
-  shows "t \<Down> t"
-using a by (induct) (auto)
-
 
 lemma e_App_elim:
   assumes a: "App t1 t2 \<Down> v"
@@ -171,7 +186,7 @@
 using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
 
 
-subsection {* EXERCISE *}
+subsection {* EXERCISE 13 *}
 
 text {*
   Complete the first and second case in the 
@@ -186,9 +201,8 @@
   case (cbv1 v x t t3)
   have a1: "val v" by fact
   have a2: "t[x ::= v] \<Down> t3" by fact
-  have a3: "Lam [x].t \<Down> Lam [x].t" by auto
-  have a4: "v \<Down> v" using a1 eval_val by auto
-  show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto 
+
+  show "App (Lam [x].t) v \<Down> t3" sorry
 next
   case (cbv2 t t' t2 t3)
   have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
@@ -197,14 +211,15 @@
     where a1: "t' \<Down> Lam [x].t''" 
       and a2: "t2 \<Down> v'" 
       and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim) 
-  have "t \<Down>  Lam [x].t''" using ih a1 by auto 
-  then show "App t t2 \<Down> t3" using a2 a3 by auto
+  
+  show "App t t2 \<Down> t3" sorry
 qed (auto elim!: e_App_elim)
 
 
 text {* 
   Next we extend the lemma above to arbitray initial
-  sequences of cbv-reductions. *}
+  sequences of cbv-reductions. 
+*}
 
 lemma cbvs_eval:
   assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
@@ -214,30 +229,42 @@
 text {* 
   Finally, we can show that if from a term t we reach a value 
   by a cbv-reduction sequence, then t evaluates to this value. 
+
+  This proof is not by induction. So we have to set up the proof
+  with
+
+    proof -
+    
+  in order to prevent Isabelle from applying a default introduction   
+  rule.
 *}
 
 lemma cbvs_implies_eval:
-  assumes a: "t \<longrightarrow>cbv* v" "val v"
+  assumes a: "t \<longrightarrow>cbv* v" 
+  and     b: "val v"
   shows "t \<Down> v"
-using a
-by (induct) (auto intro: eval_val cbvs_eval)
+proof - 
+  have "v \<Down> v" using b eval_val by simp
+  then show "t \<Down> v" using a cbvs_eval by auto
+qed
+
+section {* EXERCISE 15 *}
 
 text {* 
-  All facts tied together give us the desired property about
-  machines. 
+  All facts tied together give us the desired property 
+  about machines: we know that a machines transitions
+  correspond to cbvs transitions, and with the lemma
+  above they correspond to an eval judgement.
 *}
 
 theorem machines_implies_eval:
   assumes a: "<t1, []> \<mapsto>* <t2, []>" 
   and     b: "val t2" 
   shows "t1 \<Down> t2"
-proof -
-  have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
-  then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
+proof - 
+  
+  show "t1 \<Down> t2" sorry
 qed
 
-
-
-
 end