--- a/Tutorial/Tutorial4.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-
-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
-