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