nominal2: comparison Tutorial/Tutorial4.thy

equal deleted inserted replaced

-:e0391947b7da
+:7b2691911fbc
 theory Tutorial4
-imports Tutorial1 Tutorial2 Tutorial3
+imports Tutorial1 Tutorial2
 begin
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
 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 3 *}
+subsection {* EXERCISE 11 *}
 text {*
 Show that cbv* is transitive, by filling the gaps in the
 proof below.
 *}
-lemma
+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 "e3' \<longrightarrow>cbv* e3" by fact
 show "e1 \<longrightarrow>cbv* e3" sorry
 qed
-lemma cbvs3 [intro]:
-assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+text {*
-shows "e1 \<longrightarrow>cbv* e3"
+In order to help establishing the property that the machine
-using a by (induct) (auto)
-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.
 *}
 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:
-*}
+subsection {* EXERCISE 12 *}
-subsection {* EXERCISE 8 *}
 text {*
 If more simple exercises are needed, then complete the following proof.
 *}
 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
+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
+show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" sorry
-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
+show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry
-then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto
+qed
-qed
+section {* EXERCISE 13 *}
-section {* EXERCISE 9 *}
 text {*
 The point of the cbv-reduction was that we can easily relatively
 establish the follwoing property:
 *}
 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 CK machine. *}
+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 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.
 *}
 corollary machines_implies_cbvs:
 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.
+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"
 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 *}
+subsection {* EXERCISE 13 *}
 text {*
 Complete the first and second case in the
 proof below.
 *}
 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" sorry
-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
+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"
 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" "val v"
+assumes a: "t \<longrightarrow>cbv* v"
+and     b: "val v"
 shows "t \<Down> v"
-using a
+proof -
-by (induct) (auto intro: eval_val cbvs_eval)
+have "v \<Down> v" using b eval_val by simp
+then show "t \<Down> v" using a cbvs_eval by auto
-text {*
+qed
-All facts tied together give us the desired property about
-machines.
+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 -
-have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
-then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
+show "t1 \<Down> t2" sorry
 qed
 end

changeset 2701	7b2691911fbc
parent 2693	2abc8cb46a5c
child 2706	8ae1c2e6369e