diff -r da9bed7baf23 -r af4fb03ecf32 Tutorial/Tutorial4s.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial4s.thy	Sun Jan 23 07:15:59 2011 +0900
@@ -0,0 +1,244 @@
+theory Tutorial4
+imports Tutorial1
+begin
+
+section {* The CBV Reduction Relation (Small-Step Semantics) *}
+
+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
+nominal_inductive cbv
+  avoids cbv1: "x"
+  unfolding fresh_star_def
+  by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)
+
+text {*
+  In order to satisfy the vc-condition we have to formulate
+  this relation with the additional freshness constraint
+  atom x \<sharp> v. Although this makes the definition vc-ompatible, it
+  makes the definition less useful. We can with a little bit of 
+  pain show that the more restricted rule is equivalent to the
+  usual rule. 
+*}
+
+lemma subst_rename: 
+  assumes a: "atom y \<sharp> t"
+  shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet> t)[y ::= s]"
+using a 
+by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+   (auto simp add: lam.fresh fresh_at_base)
+
+
+lemma better_cbv1 [intro]: 
+  assumes a: "val 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
+    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+  also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto
+  also have "\<dots> = t[x ::= v]" using fs subst_rename[symmetric] by simp
+  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 *}
+
+text {*  
+  If more simple exercises are needed, then complete the following proof. 
+*}
+
+lemma cbv_in_ctx:
+  assumes a: "t \<longrightarrow>cbv t'"
+  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
+using a
+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
+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
+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
+qed
+
+section {* EXERCISE 9 *} 
+ 
+text {*
+  The point of the cbv-reduction was that we can easily relatively 
+  establish the follwoing property:
+*}
+
+lemma machine_implies_cbvs_ctx:
+  assumes a: "<e, Es> \<mapsto> <e', Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a 
+proof (induct)
+  case (m1 t1 t2 Es)
+thm machine.intros thm cbv2
+  have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
+  then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp
+next
+  case (m2 v t2 Es)
+  have "val v" by fact
+  have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"  using ctx_compose ctx_composes.simps filling.simps by simp
+  then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp
+next
+  case (m3 v x t Es)
+  have aa: "val v" by fact
+  have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
+  then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using better_cbv1[OF aa] cbv_in_ctx by simp
+  then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast
+qed
+
+text {* 
+  It is not difficult to extend the lemma above to
+  arbitrary reductions sequences of the CK machine. *}
+
+lemma machines_implies_cbvs_ctx:
+  assumes a: "<e, Es> \<mapsto>* <e', Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a machine_implies_cbvs_ctx 
+by (induct) (blast)+
+
+text {* 
+  So whenever we let the CL machine start in an initial
+  state and it arrives at a final state, then there exists
+  a corresponding cbv-reduction sequence. 
+*}
+
+corollary machines_implies_cbvs:
+  assumes a: "<e, []> \<mapsto>* <e', []>"
+  shows "e \<longrightarrow>cbv* e'"
+proof - 
+  have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>" 
+     using a machines_implies_cbvs_ctx by blast
+  then show "e \<longrightarrow>cbv* e'" by simp  
+qed
+
+text {*
+  We now want to relate the cbv-reduction to the evaluation
+  relation. For this we need two auxiliary lemmas. 
+*}
+
+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"
+  obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
+using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
+
+
+subsection {* EXERCISE *}
+
+text {*
+  Complete the first and second case in the 
+  proof below. 
+*}
+
+lemma cbv_eval:
+  assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a
+proof(induct arbitrary: t3)
+  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 
+next
+  case (cbv2 t t' t2 t3)
+  have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
+  have "App t' t2 \<Down> t3" by fact
+  then obtain x t'' v' 
+    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
+qed (auto elim!: e_App_elim)
+
+
+text {* 
+  Next we extend the lemma above to arbitray initial
+  sequences of cbv-reductions. *}
+
+lemma cbvs_eval:
+  assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a by (induct) (auto intro: cbv_eval)
+
+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. 
+*}
+
+lemma cbvs_implies_eval:
+  assumes a: "t \<longrightarrow>cbv* v" "val v"
+  shows "t \<Down> v"
+using a
+by (induct) (auto intro: eval_val cbvs_eval)
+
+text {* 
+  All facts tied together give us the desired property about
+  machines. 
+*}
+
+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
+qed
+
+
+
+
+end
+