2696
+ − 1
theory Tutorial4
+ − 2
imports Tutorial1
+ − 3
begin
+ − 4
+ − 5
section {* The CBV Reduction Relation (Small-Step Semantics) *}
+ − 6
+ − 7
text {*
+ − 8
In order to help establishing the property that the CK Machine
+ − 9
calculates a nomrmalform that corresponds to the evaluation
+ − 10
relation, we introduce the call-by-value small-step semantics.
+ − 11
*}
+ − 12
+ − 13
inductive
+ − 14
cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60)
+ − 15
where
+ − 16
cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
+ − 17
| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
+ − 18
| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
+ − 19
+ − 20
equivariance val
+ − 21
equivariance cbv
+ − 22
nominal_inductive cbv
+ − 23
avoids cbv1: "x"
+ − 24
unfolding fresh_star_def
+ − 25
by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)
+ − 26
+ − 27
text {*
+ − 28
In order to satisfy the vc-condition we have to formulate
+ − 29
this relation with the additional freshness constraint
+ − 30
atom x \<sharp> v. Although this makes the definition vc-ompatible, it
+ − 31
makes the definition less useful. We can with a little bit of
+ − 32
pain show that the more restricted rule is equivalent to the
+ − 33
usual rule.
+ − 34
*}
+ − 35
+ − 36
lemma subst_rename:
+ − 37
assumes a: "atom y \<sharp> t"
+ − 38
shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet> t)[y ::= s]"
+ − 39
using a
+ − 40
by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+ − 41
(auto simp add: lam.fresh fresh_at_base)
+ − 42
+ − 43
+ − 44
lemma better_cbv1 [intro]:
+ − 45
assumes a: "val v"
+ − 46
shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
+ − 47
proof -
+ − 48
obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)
+ − 49
have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs
+ − 50
by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+ − 51
also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto
+ − 52
also have "\<dots> = t[x ::= v]" using fs subst_rename[symmetric] by simp
+ − 53
finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
+ − 54
qed
+ − 55
+ − 56
text {*
+ − 57
The transitive closure of the cbv-reduction relation:
+ − 58
*}
+ − 59
+ − 60
inductive
+ − 61
"cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
+ − 62
where
+ − 63
cbvs1[intro]: "e \<longrightarrow>cbv* e"
+ − 64
| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+ − 65
+ − 66
lemma cbvs3 [intro]:
+ − 67
assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+ − 68
shows "e1 \<longrightarrow>cbv* e3"
+ − 69
using a by (induct) (auto)
+ − 70
+ − 71
+ − 72
subsection {* EXERCISE 8 *}
+ − 73
+ − 74
text {*
+ − 75
If more simple exercises are needed, then complete the following proof.
+ − 76
*}
+ − 77
+ − 78
lemma cbv_in_ctx:
+ − 79
assumes a: "t \<longrightarrow>cbv t'"
+ − 80
shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
+ − 81
using a
+ − 82
proof (induct E)
+ − 83
case Hole
+ − 84
have "t \<longrightarrow>cbv t'" by fact
+ − 85
then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" by simp
+ − 86
next
+ − 87
case (CAppL E s)
+ − 88
have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+ − 89
moreover
+ − 90
have "t \<longrightarrow>cbv t'" by fact
+ − 91
ultimately
+ − 92
have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+ − 93
then show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" by auto
+ − 94
next
+ − 95
case (CAppR s E)
+ − 96
have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+ − 97
moreover
+ − 98
have a: "t \<longrightarrow>cbv t'" by fact
+ − 99
ultimately
+ − 100
have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+ − 101
then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto
+ − 102
qed
+ − 103
+ − 104
section {* EXERCISE 9 *}
+ − 105
+ − 106
text {*
+ − 107
The point of the cbv-reduction was that we can easily relatively
+ − 108
establish the follwoing property:
+ − 109
*}
+ − 110
+ − 111
lemma machine_implies_cbvs_ctx:
+ − 112
assumes a: "<e, Es> \<mapsto> <e', Es'>"
+ − 113
shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+ − 114
using a
+ − 115
proof (induct)
+ − 116
case (m1 t1 t2 Es)
+ − 117
thm machine.intros thm cbv2
+ − 118
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
+ − 119
then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp
+ − 120
next
+ − 121
case (m2 v t2 Es)
+ − 122
have "val v" by fact
+ − 123
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
+ − 124
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
+ − 125
next
+ − 126
case (m3 v x t Es)
+ − 127
have aa: "val v" by fact
+ − 128
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
+ − 129
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
+ − 130
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
+ − 131
qed
+ − 132
+ − 133
text {*
+ − 134
It is not difficult to extend the lemma above to
+ − 135
arbitrary reductions sequences of the CK machine. *}
+ − 136
+ − 137
lemma machines_implies_cbvs_ctx:
+ − 138
assumes a: "<e, Es> \<mapsto>* <e', Es'>"
+ − 139
shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+ − 140
using a machine_implies_cbvs_ctx
+ − 141
by (induct) (blast)+
+ − 142
+ − 143
text {*
+ − 144
So whenever we let the CL machine start in an initial
+ − 145
state and it arrives at a final state, then there exists
+ − 146
a corresponding cbv-reduction sequence.
+ − 147
*}
+ − 148
+ − 149
corollary machines_implies_cbvs:
+ − 150
assumes a: "<e, []> \<mapsto>* <e', []>"
+ − 151
shows "e \<longrightarrow>cbv* e'"
+ − 152
proof -
+ − 153
have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>"
+ − 154
using a machines_implies_cbvs_ctx by blast
+ − 155
then show "e \<longrightarrow>cbv* e'" by simp
+ − 156
qed
+ − 157
+ − 158
text {*
+ − 159
We now want to relate the cbv-reduction to the evaluation
+ − 160
relation. For this we need two auxiliary lemmas.
+ − 161
*}
+ − 162
+ − 163
lemma eval_val:
+ − 164
assumes a: "val t"
+ − 165
shows "t \<Down> t"
+ − 166
using a by (induct) (auto)
+ − 167
+ − 168
+ − 169
lemma e_App_elim:
+ − 170
assumes a: "App t1 t2 \<Down> v"
+ − 171
obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
+ − 172
using a by (cases) (auto simp add: lam.eq_iff lam.distinct)
+ − 173
+ − 174
+ − 175
subsection {* EXERCISE *}
+ − 176
+ − 177
text {*
+ − 178
Complete the first and second case in the
+ − 179
proof below.
+ − 180
*}
+ − 181
+ − 182
lemma cbv_eval:
+ − 183
assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
+ − 184
shows "t1 \<Down> t3"
+ − 185
using a
+ − 186
proof(induct arbitrary: t3)
+ − 187
case (cbv1 v x t t3)
+ − 188
have a1: "val v" by fact
+ − 189
have a2: "t[x ::= v] \<Down> t3" by fact
+ − 190
have a3: "Lam [x].t \<Down> Lam [x].t" by auto
+ − 191
have a4: "v \<Down> v" using a1 eval_val by auto
+ − 192
show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto
+ − 193
next
+ − 194
case (cbv2 t t' t2 t3)
+ − 195
have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
+ − 196
have "App t' t2 \<Down> t3" by fact
+ − 197
then obtain x t'' v'
+ − 198
where a1: "t' \<Down> Lam [x].t''"
+ − 199
and a2: "t2 \<Down> v'"
+ − 200
and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim)
+ − 201
have "t \<Down> Lam [x].t''" using ih a1 by auto
+ − 202
then show "App t t2 \<Down> t3" using a2 a3 by auto
+ − 203
qed (auto elim!: e_App_elim)
+ − 204
+ − 205
+ − 206
text {*
+ − 207
Next we extend the lemma above to arbitray initial
+ − 208
sequences of cbv-reductions. *}
+ − 209
+ − 210
lemma cbvs_eval:
+ − 211
assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
+ − 212
shows "t1 \<Down> t3"
+ − 213
using a by (induct) (auto intro: cbv_eval)
+ − 214
+ − 215
text {*
+ − 216
Finally, we can show that if from a term t we reach a value
+ − 217
by a cbv-reduction sequence, then t evaluates to this value.
+ − 218
*}
+ − 219
+ − 220
lemma cbvs_implies_eval:
+ − 221
assumes a: "t \<longrightarrow>cbv* v" "val v"
+ − 222
shows "t \<Down> v"
+ − 223
using a
+ − 224
by (induct) (auto intro: eval_val cbvs_eval)
+ − 225
+ − 226
text {*
+ − 227
All facts tied together give us the desired property about
+ − 228
machines.
+ − 229
*}
+ − 230
+ − 231
theorem machines_implies_eval:
+ − 232
assumes a: "<t1, []> \<mapsto>* <t2, []>"
+ − 233
and b: "val t2"
+ − 234
shows "t1 \<Down> t2"
+ − 235
proof -
+ − 236
have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
+ − 237
then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
+ − 238
qed
+ − 239
+ − 240
+ − 241
+ − 242
+ − 243
end
+ − 244