+ −
theory Tutorial4+ −
imports Tutorial1 Tutorial2+ −
begin+ −
+ −
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 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 nomrmalform that corresponds to the evaluation + −
relation, we introduce the call-by-value small-step semantics.+ −
*}+ −
+ −
+ −
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+ −
+ −
+ −
+ −
subsection {* EXERCISE 12 *}+ −
+ −
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+ −
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+ −
have "t \<longrightarrow>cbv t'" by fact+ −
+ −
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+ −
have a: "t \<longrightarrow>cbv t'" by fact+ −
+ −
show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry+ −
qed+ −
+ −
section {* EXERCISE 13 *} + −
+ −
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)+ −
+ −
show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" sorry+ −
next+ −
case (m2 v t2 Es)+ −
have "val v" by fact+ −
+ −
show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry+ −
next+ −
case (m3 v x t Es)+ −
have "val v" by fact+ −
+ −
show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry+ −
qed+ −
+ −
text {* + −
It is not difficult to extend the lemma above to+ −
arbitrary reductions sequences of the 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 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 one auxiliary lemma about+ −
inverting the e_App rule. + −
*}+ −
+ −
+ −
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 13 *}+ −
+ −
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+ −
+ −
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+ −
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) + −
+ −
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. + −
*}+ −
+ −
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. + −
+ −
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" + −
and b: "val v"+ −
shows "t \<Down> v"+ −
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: 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 - + −
+ −
show "t1 \<Down> t2" sorry+ −
qed+ −
+ −
end+ −
+ −