theory Tutorial4imports Tutorial1 Tutorial2beginsection {* 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" sorrynext 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" sorryqed 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 valequivariance cbvnominal_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 simpqedsubsection {* 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 aproof (induct E) case Hole have "t \<longrightarrow>cbv t'" by fact show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" sorrynext 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>" sorrynext 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>" sorryqedsection {* EXERCISE 13 *} text {* The point of the cbv-reduction was that we can easily relatively establish the following 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>" sorrynext 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>" sorrynext 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>" sorryqedtext {* 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 qedtext {* 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 aproof(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" sorrynext 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" sorryqed (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 autoqedsection {* 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" sorryqedend