|
1 |
|
2 theory Blexer2 |
|
3 imports "Lexer" "PDerivs" |
|
4 begin |
|
5 |
|
6 section \<open>Bit-Encodings\<close> |
|
7 |
|
8 datatype bit = Z | S |
|
9 |
|
10 fun code :: "val \<Rightarrow> bit list" |
|
11 where |
|
12 "code Void = []" |
|
13 | "code (Char c) = []" |
|
14 | "code (Left v) = Z # (code v)" |
|
15 | "code (Right v) = S # (code v)" |
|
16 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
|
17 | "code (Stars []) = [S]" |
|
18 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
|
19 |
|
20 |
|
21 fun |
|
22 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
|
23 where |
|
24 "Stars_add v (Stars vs) = Stars (v # vs)" |
|
25 |
|
26 function |
|
27 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
|
28 where |
|
29 "decode' bs ZERO = (undefined, bs)" |
|
30 | "decode' bs ONE = (Void, bs)" |
|
31 | "decode' bs (CH d) = (Char d, bs)" |
|
32 | "decode' [] (ALT r1 r2) = (Void, [])" |
|
33 | "decode' (Z # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r1 in (Left v, bs'))" |
|
34 | "decode' (S # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r2 in (Right v, bs'))" |
|
35 | "decode' bs (SEQ r1 r2) = (let (v1, bs') = decode' bs r1 in |
|
36 let (v2, bs'') = decode' bs' r2 in (Seq v1 v2, bs''))" |
|
37 | "decode' [] (STAR r) = (Void, [])" |
|
38 | "decode' (S # bs) (STAR r) = (Stars [], bs)" |
|
39 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
|
40 let (vs, bs'') = decode' bs' (STAR r) |
|
41 in (Stars_add v vs, bs''))" |
|
42 by pat_completeness auto |
|
43 |
|
44 lemma decode'_smaller: |
|
45 assumes "decode'_dom (bs, r)" |
|
46 shows "length (snd (decode' bs r)) \<le> length bs" |
|
47 using assms |
|
48 apply(induct bs r) |
|
49 apply(auto simp add: decode'.psimps split: prod.split) |
|
50 using dual_order.trans apply blast |
|
51 by (meson dual_order.trans le_SucI) |
|
52 |
|
53 termination "decode'" |
|
54 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") |
|
55 apply(auto dest!: decode'_smaller) |
|
56 by (metis less_Suc_eq_le snd_conv) |
|
57 |
|
58 definition |
|
59 decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option" |
|
60 where |
|
61 "decode ds r \<equiv> (let (v, ds') = decode' ds r |
|
62 in (if ds' = [] then Some v else None))" |
|
63 |
|
64 lemma decode'_code_Stars: |
|
65 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" |
|
66 shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" |
|
67 using assms |
|
68 apply(induct vs) |
|
69 apply(auto) |
|
70 done |
|
71 |
|
72 lemma decode'_code: |
|
73 assumes "\<Turnstile> v : r" |
|
74 shows "decode' ((code v) @ ds) r = (v, ds)" |
|
75 using assms |
|
76 apply(induct v r arbitrary: ds) |
|
77 apply(auto) |
|
78 using decode'_code_Stars by blast |
|
79 |
|
80 lemma decode_code: |
|
81 assumes "\<Turnstile> v : r" |
|
82 shows "decode (code v) r = Some v" |
|
83 using assms unfolding decode_def |
|
84 by (smt append_Nil2 decode'_code old.prod.case) |
|
85 |
|
86 |
|
87 section {* Annotated Regular Expressions *} |
|
88 |
|
89 datatype arexp = |
|
90 AZERO |
|
91 | AONE "bit list" |
|
92 | ACHAR "bit list" char |
|
93 | ASEQs "bit list" "arexp list" |
|
94 | AALTs "bit list" "arexp list" |
|
95 | ASTAR "bit list" arexp |
|
96 |
|
97 abbreviation |
|
98 "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]" |
|
99 |
|
100 abbreviation |
|
101 "ASEQ bs r1 r2 \<equiv> ASEQs bs [r1, r2]" |
|
102 |
|
103 fun asize :: "arexp \<Rightarrow> nat" where |
|
104 "asize AZERO = 1" |
|
105 | "asize (AONE cs) = 1" |
|
106 | "asize (ACHAR cs c) = 1" |
|
107 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))" |
|
108 | "asize (ASEQs cs rs) = Suc (sum_list (map asize rs))" |
|
109 | "asize (ASTAR cs r) = Suc (asize r)" |
|
110 |
|
111 fun |
|
112 erase :: "arexp \<Rightarrow> rexp" |
|
113 where |
|
114 "erase AZERO = ZERO" |
|
115 | "erase (AONE _) = ONE" |
|
116 | "erase (ACHAR _ c) = CH c" |
|
117 | "erase (AALTs _ []) = ZERO" |
|
118 | "erase (AALTs _ [r]) = (erase r)" |
|
119 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
|
120 | "erase (ASEQs _ []) = ONE" |
|
121 | "erase (ASEQs _ [r]) = (erase r)" |
|
122 | "erase (ASEQs bs (r#rs)) = SEQ (erase r) (erase (ASEQs bs rs))" |
|
123 | "erase (ASTAR _ r) = STAR (erase r)" |
|
124 |
|
125 |
|
126 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
|
127 "fuse bs AZERO = AZERO" |
|
128 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
|
129 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
|
130 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs" |
|
131 | "fuse bs (ASEQs cs rs) = ASEQs (bs @ cs) rs" |
|
132 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
|
133 |
|
134 lemma fuse_append: |
|
135 shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)" |
|
136 apply(induct r) |
|
137 apply(auto) |
|
138 done |
|
139 |
|
140 |
|
141 fun intern :: "rexp \<Rightarrow> arexp" where |
|
142 "intern ZERO = AZERO" |
|
143 | "intern ONE = AONE []" |
|
144 | "intern (CH c) = ACHAR [] c" |
|
145 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
|
146 (fuse [S] (intern r2))" |
|
147 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
|
148 | "intern (STAR r) = ASTAR [] (intern r)" |
|
149 |
|
150 |
|
151 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
|
152 "retrieve (AONE bs) Void = bs" |
|
153 | "retrieve (ACHAR bs c) (Char d) = bs" |
|
154 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" |
|
155 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
|
156 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
|
157 | "retrieve (ASEQs bs []) v = bs" |
|
158 | "retrieve (ASEQs bs [r]) v = bs @ retrieve r v" |
|
159 | "retrieve (ASEQs bs (r#rs)) (Seq v1 v2) = bs @ retrieve r v1 @ retrieve (ASEQs [] rs) v2" |
|
160 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
|
161 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
|
162 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
|
163 |
|
164 |
|
165 |
|
166 fun |
|
167 bnullable :: "arexp \<Rightarrow> bool" |
|
168 where |
|
169 "bnullable (AZERO) = False" |
|
170 | "bnullable (AONE bs) = True" |
|
171 | "bnullable (ACHAR bs c) = False" |
|
172 | "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
|
173 | "bnullable (ASEQs bs rs) = (\<forall>r \<in> set rs. bnullable r)" |
|
174 | "bnullable (ASTAR bs r) = True" |
|
175 |
|
176 abbreviation |
|
177 bnullables :: "arexp list \<Rightarrow> bool" |
|
178 where |
|
179 "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)" |
|
180 |
|
181 fun |
|
182 bmkeps :: "arexp \<Rightarrow> bit list" and |
|
183 bmkepss :: "arexp list \<Rightarrow> bit list" |
|
184 where |
|
185 "bmkeps(AONE bs) = bs" |
|
186 | "bmkeps(ASEQs bs rs) = bs @ concat (map bmkeps rs)" |
|
187 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)" |
|
188 | "bmkeps(ASTAR bs r) = bs @ [S]" |
|
189 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
|
190 |
|
191 lemma bmkepss1: |
|
192 assumes "\<not> bnullables rs1" |
|
193 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
|
194 using assms |
|
195 by (induct rs1) (auto) |
|
196 |
|
197 lemma bmkepss2: |
|
198 assumes "bnullables rs1" |
|
199 shows "bmkepss (rs1 @ rs2) = bmkepss rs1" |
|
200 using assms |
|
201 by (induct rs1) (auto) |
|
202 |
|
203 |
|
204 fun |
|
205 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
|
206 where |
|
207 "bder c (AZERO) = AZERO" |
|
208 | "bder c (AONE bs) = AZERO" |
|
209 | "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" |
|
210 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
|
211 | "bder c (ASEQs bs []) = AZERO" |
|
212 | "bder c (ASEQs bs [r1]) = fuse bs (bder c r1)" |
|
213 | "bder c (ASEQs bs (r1#rs)) = |
|
214 (if bnullable r1 |
|
215 then AALT bs (ASEQs [] ((bder c r1) # rs)) (fuse (bmkeps r1) (bder c (ASEQs [] rs))) |
|
216 else ASEQs bs ((bder c r1) # rs))" |
|
217 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
|
218 |
|
219 |
|
220 fun |
|
221 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
222 where |
|
223 "bders r [] = r" |
|
224 | "bders r (c#s) = bders (bder c r) s" |
|
225 |
|
226 lemma bders_append: |
|
227 "bders c (s1 @ s2) = bders (bders c s1) s2" |
|
228 apply(induct s1 arbitrary: c s2) |
|
229 apply(simp_all) |
|
230 done |
|
231 |
|
232 lemma bnullable_correctness: |
|
233 shows "nullable (erase r) = bnullable r" |
|
234 apply(induct r rule: erase.induct) |
|
235 apply(simp_all) |
|
236 done |
|
237 |
|
238 lemma erase_fuse: |
|
239 shows "erase (fuse bs r) = erase r" |
|
240 apply(induct r rule: erase.induct) |
|
241 apply(simp_all) |
|
242 done |
|
243 |
|
244 lemma erase_intern [simp]: |
|
245 shows "erase (intern r) = r" |
|
246 apply(induct r) |
|
247 apply(simp_all add: erase_fuse) |
|
248 done |
|
249 |
|
250 lemma erase_ASEQs: |
|
251 shows "erase (ASEQs [] rs) = erase (ASEQs bs rs)" |
|
252 apply(induct rs arbitrary: bs) |
|
253 apply(auto) |
|
254 apply(case_tac rs) |
|
255 apply(auto) |
|
256 done |
|
257 |
|
258 lemma erase_bder [simp]: |
|
259 shows "erase (bder a r) = der a (erase r)" |
|
260 apply(induct r rule: erase.induct) |
|
261 apply(simp_all add: erase_fuse bnullable_correctness) |
|
262 apply(case_tac va) |
|
263 apply(simp_all add: erase_fuse bnullable_correctness) |
|
264 apply(auto) |
|
265 apply(simp_all add: erase_fuse bnullable_correctness erase_ASEQs) |
|
266 done |
|
267 |
|
268 lemma erase_bders [simp]: |
|
269 shows "erase (bders r s) = ders s (erase r)" |
|
270 apply(induct s arbitrary: r ) |
|
271 apply(simp_all) |
|
272 done |
|
273 |
|
274 lemma bnullable_fuse: |
|
275 shows "bnullable (fuse bs r) = bnullable r" |
|
276 apply(induct r arbitrary: bs) |
|
277 apply(auto) |
|
278 done |
|
279 |
|
280 lemma retrieve_encode_STARS: |
|
281 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" |
|
282 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
|
283 using assms |
|
284 apply(induct vs) |
|
285 apply(simp_all) |
|
286 done |
|
287 |
|
288 |
|
289 |
|
290 lemma retrieve_fuse2: |
|
291 assumes "\<Turnstile> v : (erase r)" |
|
292 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
293 using assms |
|
294 apply(induct r arbitrary: v bs) |
|
295 apply(auto elim: Prf_elims)[4] |
|
296 defer |
|
297 apply(case_tac x2a) |
|
298 apply(simp) |
|
299 using Prf_elims(1) apply blast |
|
300 apply(simp) |
|
301 apply(case_tac list) |
|
302 apply(simp) |
|
303 apply(simp) |
|
304 apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5)) |
|
305 using retrieve_encode_STARS |
|
306 apply(auto elim!: Prf_elims)[1] |
|
307 apply(case_tac vs) |
|
308 apply(simp) |
|
309 apply(simp) |
|
310 apply(case_tac x2a) |
|
311 apply(simp) |
|
312 apply(simp) |
|
313 apply(case_tac list) |
|
314 apply(simp) |
|
315 apply(simp) |
|
316 by (smt (verit, best) Prf_elims(2) append_assoc retrieve.simps(8)) |
|
317 |
|
318 lemma retrieve_fuse: |
|
319 assumes "\<Turnstile> v : r" |
|
320 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
|
321 using assms |
|
322 by (simp_all add: retrieve_fuse2) |
|
323 |
|
324 |
|
325 lemma retrieve_code: |
|
326 assumes "\<Turnstile> v : r" |
|
327 shows "code v = retrieve (intern r) v" |
|
328 using assms |
|
329 apply(induct v r ) |
|
330 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
|
331 done |
|
332 |
|
333 |
|
334 lemma retrieve_AALTs_bnullable1: |
|
335 assumes "bnullable r" |
|
336 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
|
337 = bs @ retrieve r (mkeps (erase r))" |
|
338 using assms |
|
339 apply(case_tac rs) |
|
340 apply(auto simp add: bnullable_correctness) |
|
341 done |
|
342 |
|
343 lemma retrieve_AALTs_bnullable2: |
|
344 assumes "\<not>bnullable r" "bnullables rs" |
|
345 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
|
346 = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" |
|
347 using assms |
|
348 apply(induct rs arbitrary: r bs) |
|
349 apply(auto) |
|
350 using bnullable_correctness apply blast |
|
351 apply(case_tac rs) |
|
352 apply(auto) |
|
353 using bnullable_correctness apply blast |
|
354 apply(case_tac rs) |
|
355 apply(auto) |
|
356 done |
|
357 |
|
358 lemma bmkeps_retrieve_AALTs: |
|
359 assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" |
|
360 "bnullables rs" |
|
361 shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" |
|
362 using assms |
|
363 apply(induct rs arbitrary: bs) |
|
364 apply(auto) |
|
365 using retrieve_AALTs_bnullable1 apply presburger |
|
366 apply (metis retrieve_AALTs_bnullable2) |
|
367 apply (simp add: retrieve_AALTs_bnullable1) |
|
368 by (metis retrieve_AALTs_bnullable2) |
|
369 |
|
370 lemma bmkeps_retrieve_ASEQs: |
|
371 assumes "\<forall>r \<in> set rs. bmkeps r = retrieve r (mkeps (erase r))" |
|
372 "\<forall>r \<in> set rs. bnullable r" |
|
373 shows "x1 @ concat (map bmkeps rs) = retrieve (ASEQs x1 rs) (mkeps (erase (ASEQs x1 rs)))" |
|
374 using assms |
|
375 apply(induct rs arbitrary: x1) |
|
376 apply(auto) |
|
377 apply(case_tac rs) |
|
378 apply(auto) |
|
379 by (metis erase_ASEQs self_append_conv2) |
|
380 |
|
381 |
|
382 lemma bmkeps_retrieve: |
|
383 assumes "bnullable r" |
|
384 shows "bmkeps r = retrieve r (mkeps (erase r))" |
|
385 using assms |
|
386 apply(induct r) |
|
387 apply(auto) |
|
388 defer |
|
389 using bmkeps_retrieve_AALTs apply auto |
|
390 by (simp add: bmkeps_retrieve_ASEQs) |
|
391 |
|
392 lemma bder_retrieve: |
|
393 assumes "\<Turnstile> v : der c (erase r)" |
|
394 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
|
395 using assms |
|
396 apply(induct r arbitrary: v rule: erase.induct) |
|
397 using Prf_elims(1) apply auto[1] |
|
398 using Prf_elims(1) apply auto[1] |
|
399 apply(auto)[1] |
|
400 apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2)) |
|
401 using Prf_elims(1) apply blast |
|
402 (* AALTs case *) |
|
403 apply(simp) |
|
404 apply(erule Prf_elims) |
|
405 apply(simp) |
|
406 apply(simp) |
|
407 apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v) |
|
408 apply(erule Prf_elims) |
|
409 apply(simp) |
|
410 apply(simp) |
|
411 apply(case_tac rs) |
|
412 apply(simp) |
|
413 apply(simp) |
|
414 using Prf_elims(3) apply fastforce |
|
415 (* ASTAR case *) |
|
416 prefer 4 |
|
417 apply(rename_tac bs r v) |
|
418 apply(simp) |
|
419 apply(erule Prf_elims) |
|
420 apply(clarify) |
|
421 apply(erule Prf_elims) |
|
422 apply(clarify) |
|
423 apply (simp add: retrieve_fuse2) |
|
424 (* ASEQ case *) |
|
425 prefer 2 |
|
426 apply(simp) |
|
427 apply (simp add: erase_fuse retrieve_fuse2) |
|
428 apply(auto)[1] |
|
429 using Prf_elims(1) apply auto[1] |
|
430 apply(simp) |
|
431 apply(auto) |
|
432 apply(subgoal_tac "nullable (erase r)") |
|
433 prefer 2 |
|
434 using bnullable_correctness apply blast |
|
435 apply(simp) |
|
436 apply(erule Prf_elims) |
|
437 apply(simp) |
|
438 using Prf_elims(2) apply force |
|
439 apply(simp) |
|
440 prefer 2 |
|
441 apply(subgoal_tac "\<not>nullable (erase r)") |
|
442 apply(simp) |
|
443 prefer 2 |
|
444 using bnullable_correctness apply presburger |
|
445 using Prf_elims(2) apply force |
|
446 apply (simp add: bmkeps_retrieve erase_fuse retrieve_fuse2) |
|
447 apply(case_tac va) |
|
448 apply(simp) |
|
449 apply (simp add: erase_fuse retrieve_fuse2) |
|
450 apply(simp) |
|
451 apply(auto) |
|
452 apply(subgoal_tac "nullable (erase v)") |
|
453 prefer 2 |
|
454 using bnullable_correctness apply blast |
|
455 apply(simp) |
|
456 apply(erule Prf_elims) |
|
457 apply(simp) |
|
458 apply(erule Prf_elims) |
|
459 apply(simp) |
|
460 apply(case_tac list) |
|
461 apply(simp) |
|
462 apply(rotate_tac 1) |
|
463 apply(drule_tac x="Left v1" in meta_spec) |
|
464 apply(drule meta_mp) |
|
465 apply(rule Prf.intros) |
|
466 apply(simp) |
|
467 apply(rule Prf.intros) |
|
468 apply(simp) |
|
469 apply(simp) |
|
470 apply simp |
|
471 apply(simp) |
|
472 apply(case_tac "bnullable a") |
|
473 apply(simp) |
|
474 apply(subgoal_tac "nullable (erase a)") |
|
475 prefer 2 |
|
476 using bnullable_correctness apply blast |
|
477 apply(simp) |
|
478 apply(rotate_tac 1) |
|
479 apply(drule_tac x="Left v1" in meta_spec) |
|
480 apply(drule meta_mp) |
|
481 apply(rule Prf.intros) |
|
482 apply(simp) |
|
483 apply(rule Prf.intros) |
|
484 apply(simp) |
|
485 apply force |
|
486 apply simp |
|
487 apply(subgoal_tac "\<not>nullable (erase a)") |
|
488 prefer 2 |
|
489 using bnullable_correctness apply presburger |
|
490 apply(simp) |
|
491 apply(rotate_tac 1) |
|
492 apply(drule_tac x="Left v1" in meta_spec) |
|
493 apply(drule meta_mp) |
|
494 apply(rule Prf.intros) |
|
495 using Prf.intros(1) apply blast |
|
496 apply simp |
|
497 using Prf.intros(3) apply fastforce |
|
498 apply(subgoal_tac "\<not>nullable (erase v)") |
|
499 prefer 2 |
|
500 using bnullable_correctness apply presburger |
|
501 apply(simp) |
|
502 using Prf_elims(2) by force |
|
503 |
|
504 lemma MAIN_decode: |
|
505 assumes "\<Turnstile> v : ders s r" |
|
506 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
|
507 using assms |
|
508 proof (induct s arbitrary: v rule: rev_induct) |
|
509 case Nil |
|
510 have "\<Turnstile> v : ders [] r" by fact |
|
511 then have "\<Turnstile> v : r" by simp |
|
512 then have "Some v = decode (retrieve (intern r) v) r" |
|
513 using decode_code retrieve_code by auto |
|
514 then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" |
|
515 by simp |
|
516 next |
|
517 case (snoc c s v) |
|
518 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
|
519 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
|
520 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
|
521 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
|
522 by (simp add: Prf_injval ders_append) |
|
523 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
|
524 by (simp add: flex_append) |
|
525 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
|
526 using asm2 IH by simp |
|
527 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
|
528 using asm by (simp_all add: bder_retrieve ders_append) |
|
529 finally show "Some (flex r id (s @ [c]) v) = |
|
530 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
|
531 qed |
|
532 |
|
533 definition blexer where |
|
534 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
|
535 decode (bmkeps (bders (intern r) s)) r else None" |
|
536 |
|
537 lemma blexer_correctness: |
|
538 shows "blexer r s = lexer r s" |
|
539 proof - |
|
540 { define bds where "bds \<equiv> bders (intern r) s" |
|
541 define ds where "ds \<equiv> ders s r" |
|
542 assume asm: "nullable ds" |
|
543 have era: "erase bds = ds" |
|
544 unfolding ds_def bds_def by simp |
|
545 have mke: "\<Turnstile> mkeps ds : ds" |
|
546 using asm by (simp add: mkeps_nullable) |
|
547 have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" |
|
548 using bmkeps_retrieve |
|
549 using asm era |
|
550 using bnullable_correctness by force |
|
551 also have "... = Some (flex r id s (mkeps ds))" |
|
552 using mke by (simp_all add: MAIN_decode ds_def bds_def) |
|
553 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
|
554 unfolding bds_def ds_def . |
|
555 } |
|
556 then show "blexer r s = lexer r s" |
|
557 unfolding blexer_def lexer_flex |
|
558 by (auto simp add: bnullable_correctness[symmetric]) |
|
559 qed |
|
560 |
|
561 |
|
562 unused_thms |
|
563 |
|
564 end |