|
1 |
|
2 theory SizeBound4CT |
|
3 imports |
|
4 "Lexer" |
|
5 "PDerivs" |
|
6 |
|
7 begin |
|
8 |
|
9 section \<open>Bit-Encodings\<close> |
|
10 |
|
11 datatype bit = Z | S |
|
12 |
|
13 fun code :: "val \<Rightarrow> bit list" |
|
14 where |
|
15 "code Void = []" |
|
16 | "code (Char c) = []" |
|
17 | "code (Left v) = Z # (code v)" |
|
18 | "code (Right v) = S # (code v)" |
|
19 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
|
20 | "code (Stars []) = [S]" |
|
21 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
|
22 |
|
23 |
|
24 fun |
|
25 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
|
26 where |
|
27 "Stars_add v (Stars vs) = Stars (v # vs)" |
|
28 |
|
29 function |
|
30 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
|
31 where |
|
32 "decode' ds ZERO = (Void, [])" |
|
33 | "decode' ds ONE = (Void, ds)" |
|
34 | "decode' ds (CH d) = (Char d, ds)" |
|
35 | "decode' [] (ALT r1 r2) = (Void, [])" |
|
36 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
|
37 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
|
38 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
|
39 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
|
40 | "decode' [] (STAR r) = (Void, [])" |
|
41 | "decode' (S # ds) (STAR r) = (Stars [], ds)" |
|
42 | "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in |
|
43 let (vs, ds'') = decode' ds' (STAR r) |
|
44 in (Stars_add v vs, ds''))" |
|
45 by pat_completeness auto |
|
46 |
|
47 lemma decode'_smaller: |
|
48 assumes "decode'_dom (ds, r)" |
|
49 shows "length (snd (decode' ds r)) \<le> length ds" |
|
50 using assms |
|
51 apply(induct ds r) |
|
52 apply(auto simp add: decode'.psimps split: prod.split) |
|
53 using dual_order.trans apply blast |
|
54 by (meson dual_order.trans le_SucI) |
|
55 |
|
56 termination "decode'" |
|
57 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") |
|
58 apply(auto dest!: decode'_smaller) |
|
59 by (metis less_Suc_eq_le snd_conv) |
|
60 |
|
61 definition |
|
62 decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option" |
|
63 where |
|
64 "decode ds r \<equiv> (let (v, ds') = decode' ds r |
|
65 in (if ds' = [] then Some v else None))" |
|
66 |
|
67 lemma decode'_code_Stars: |
|
68 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" |
|
69 shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" |
|
70 using assms |
|
71 apply(induct vs) |
|
72 apply(auto) |
|
73 done |
|
74 |
|
75 lemma decode'_code: |
|
76 assumes "\<Turnstile> v : r" |
|
77 shows "decode' ((code v) @ ds) r = (v, ds)" |
|
78 using assms |
|
79 apply(induct v r arbitrary: ds) |
|
80 apply(auto) |
|
81 using decode'_code_Stars by blast |
|
82 |
|
83 lemma decode_code: |
|
84 assumes "\<Turnstile> v : r" |
|
85 shows "decode (code v) r = Some v" |
|
86 using assms unfolding decode_def |
|
87 by (smt append_Nil2 decode'_code old.prod.case) |
|
88 |
|
89 |
|
90 section {* Annotated Regular Expressions *} |
|
91 |
|
92 datatype arexp = |
|
93 AZERO |
|
94 | AONE "bit list" |
|
95 | ACHAR "bit list" char |
|
96 | ASEQ "bit list" arexp arexp |
|
97 | AALTs "bit list" "arexp list" |
|
98 | ASTAR "bit list" arexp |
|
99 |
|
100 abbreviation |
|
101 "AALT bs r1 r2 \<equiv> AALTs 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 (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)" |
|
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 (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
|
121 | "erase (ASTAR _ r) = STAR (erase r)" |
|
122 |
|
123 |
|
124 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
|
125 "fuse bs AZERO = AZERO" |
|
126 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
|
127 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
|
128 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs" |
|
129 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
|
130 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
|
131 |
|
132 lemma fuse_append: |
|
133 shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)" |
|
134 apply(induct r) |
|
135 apply(auto) |
|
136 done |
|
137 |
|
138 |
|
139 fun intern :: "rexp \<Rightarrow> arexp" where |
|
140 "intern ZERO = AZERO" |
|
141 | "intern ONE = AONE []" |
|
142 | "intern (CH c) = ACHAR [] c" |
|
143 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
|
144 (fuse [S] (intern r2))" |
|
145 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
|
146 | "intern (STAR r) = ASTAR [] (intern r)" |
|
147 |
|
148 |
|
149 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
|
150 "retrieve (AONE bs) Void = bs" |
|
151 | "retrieve (ACHAR bs c) (Char d) = bs" |
|
152 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" |
|
153 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
|
154 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
|
155 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
|
156 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
|
157 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
|
158 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
|
159 |
|
160 |
|
161 |
|
162 fun |
|
163 bnullable :: "arexp \<Rightarrow> bool" |
|
164 where |
|
165 "bnullable (AZERO) = False" |
|
166 | "bnullable (AONE bs) = True" |
|
167 | "bnullable (ACHAR bs c) = False" |
|
168 | "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
|
169 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
|
170 | "bnullable (ASTAR bs r) = True" |
|
171 |
|
172 abbreviation |
|
173 bnullables :: "arexp list \<Rightarrow> bool" |
|
174 where |
|
175 "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)" |
|
176 |
|
177 fun |
|
178 bmkeps :: "arexp \<Rightarrow> bit list" and |
|
179 bmkepss :: "arexp list \<Rightarrow> bit list" |
|
180 where |
|
181 "bmkeps(AONE bs) = bs" |
|
182 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
|
183 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)" |
|
184 | "bmkeps(ASTAR bs r) = bs @ [S]" |
|
185 | "bmkepss [] = []" |
|
186 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
|
187 |
|
188 lemma bmkepss1: |
|
189 assumes "\<not> bnullables rs1" |
|
190 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
|
191 using assms |
|
192 by (induct rs1) (auto) |
|
193 |
|
194 lemma bmkepss2: |
|
195 assumes "bnullables rs1" |
|
196 shows "bmkepss (rs1 @ rs2) = bmkepss rs1" |
|
197 using assms |
|
198 by (induct rs1) (auto) |
|
199 |
|
200 |
|
201 fun |
|
202 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
|
203 where |
|
204 "bder c (AZERO) = AZERO" |
|
205 | "bder c (AONE bs) = AZERO" |
|
206 | "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" |
|
207 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
|
208 | "bder c (ASEQ bs r1 r2) = |
|
209 (if bnullable r1 |
|
210 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
|
211 else ASEQ bs (bder c r1) r2)" |
|
212 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" |
|
213 |
|
214 |
|
215 fun |
|
216 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
217 where |
|
218 "bders r [] = r" |
|
219 | "bders r (c#s) = bders (bder c r) s" |
|
220 |
|
221 lemma bders_append: |
|
222 "bders c (s1 @ s2) = bders (bders c s1) s2" |
|
223 apply(induct s1 arbitrary: c s2) |
|
224 apply(simp_all) |
|
225 done |
|
226 |
|
227 lemma bnullable_correctness: |
|
228 shows "nullable (erase r) = bnullable r" |
|
229 apply(induct r rule: erase.induct) |
|
230 apply(simp_all) |
|
231 done |
|
232 |
|
233 lemma erase_fuse: |
|
234 shows "erase (fuse bs r) = erase r" |
|
235 apply(induct r rule: erase.induct) |
|
236 apply(simp_all) |
|
237 done |
|
238 |
|
239 lemma erase_intern [simp]: |
|
240 shows "erase (intern r) = r" |
|
241 apply(induct r) |
|
242 apply(simp_all add: erase_fuse) |
|
243 done |
|
244 |
|
245 lemma erase_bder [simp]: |
|
246 shows "erase (bder a r) = der a (erase r)" |
|
247 apply(induct r rule: erase.induct) |
|
248 apply(simp_all add: erase_fuse bnullable_correctness) |
|
249 done |
|
250 |
|
251 lemma erase_bders [simp]: |
|
252 shows "erase (bders r s) = ders s (erase r)" |
|
253 apply(induct s arbitrary: r ) |
|
254 apply(simp_all) |
|
255 done |
|
256 |
|
257 lemma bnullable_fuse: |
|
258 shows "bnullable (fuse bs r) = bnullable r" |
|
259 apply(induct r arbitrary: bs) |
|
260 apply(auto) |
|
261 done |
|
262 |
|
263 lemma retrieve_encode_STARS: |
|
264 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" |
|
265 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
|
266 using assms |
|
267 apply(induct vs) |
|
268 apply(simp_all) |
|
269 done |
|
270 |
|
271 lemma retrieve_fuse2: |
|
272 assumes "\<Turnstile> v : (erase r)" |
|
273 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
274 using assms |
|
275 apply(induct r arbitrary: v bs) |
|
276 apply(auto elim: Prf_elims)[4] |
|
277 apply(case_tac x2a) |
|
278 apply(simp) |
|
279 using Prf_elims(1) apply blast |
|
280 apply(case_tac x2a) |
|
281 apply(simp) |
|
282 apply(simp) |
|
283 apply(case_tac list) |
|
284 apply(simp) |
|
285 apply(simp) |
|
286 apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5)) |
|
287 apply(simp) |
|
288 using retrieve_encode_STARS |
|
289 apply(auto elim!: Prf_elims)[1] |
|
290 apply(case_tac vs) |
|
291 apply(simp) |
|
292 apply(simp) |
|
293 done |
|
294 |
|
295 lemma retrieve_fuse: |
|
296 assumes "\<Turnstile> v : r" |
|
297 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
|
298 using assms |
|
299 by (simp_all add: retrieve_fuse2) |
|
300 |
|
301 |
|
302 lemma retrieve_code: |
|
303 assumes "\<Turnstile> v : r" |
|
304 shows "code v = retrieve (intern r) v" |
|
305 using assms |
|
306 apply(induct v r ) |
|
307 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
|
308 done |
|
309 |
|
310 |
|
311 lemma retrieve_AALTs_bnullable1: |
|
312 assumes "bnullable r" |
|
313 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
|
314 = bs @ retrieve r (mkeps (erase r))" |
|
315 using assms |
|
316 apply(case_tac rs) |
|
317 apply(auto simp add: bnullable_correctness) |
|
318 done |
|
319 |
|
320 lemma retrieve_AALTs_bnullable2: |
|
321 assumes "\<not>bnullable r" "bnullables rs" |
|
322 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
|
323 = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" |
|
324 using assms |
|
325 apply(induct rs arbitrary: r bs) |
|
326 apply(auto) |
|
327 using bnullable_correctness apply blast |
|
328 apply(case_tac rs) |
|
329 apply(auto) |
|
330 using bnullable_correctness apply blast |
|
331 apply(case_tac rs) |
|
332 apply(auto) |
|
333 done |
|
334 |
|
335 lemma bmkeps_retrieve_AALTs: |
|
336 assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" |
|
337 "bnullables rs" |
|
338 shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" |
|
339 using assms |
|
340 apply(induct rs arbitrary: bs) |
|
341 apply(auto) |
|
342 using retrieve_AALTs_bnullable1 apply presburger |
|
343 apply (metis retrieve_AALTs_bnullable2) |
|
344 apply (simp add: retrieve_AALTs_bnullable1) |
|
345 by (metis retrieve_AALTs_bnullable2) |
|
346 |
|
347 |
|
348 lemma bmkeps_retrieve: |
|
349 assumes "bnullable r" |
|
350 shows "bmkeps r = retrieve r (mkeps (erase r))" |
|
351 using assms |
|
352 apply(induct r) |
|
353 apply(auto) |
|
354 using bmkeps_retrieve_AALTs by auto |
|
355 |
|
356 lemma bder_retrieve: |
|
357 assumes "\<Turnstile> v : der c (erase r)" |
|
358 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
|
359 using assms |
|
360 apply(induct r arbitrary: v rule: erase.induct) |
|
361 using Prf_elims(1) apply auto[1] |
|
362 using Prf_elims(1) apply auto[1] |
|
363 apply(auto)[1] |
|
364 apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2)) |
|
365 using Prf_elims(1) apply blast |
|
366 (* AALTs case *) |
|
367 apply(simp) |
|
368 apply(erule Prf_elims) |
|
369 apply(simp) |
|
370 apply(simp) |
|
371 apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v) |
|
372 apply(erule Prf_elims) |
|
373 apply(simp) |
|
374 apply(simp) |
|
375 apply(case_tac rs) |
|
376 apply(simp) |
|
377 apply(simp) |
|
378 using Prf_elims(3) apply fastforce |
|
379 (* ASEQ case *) |
|
380 apply(simp) |
|
381 apply(case_tac "nullable (erase r1)") |
|
382 apply(simp) |
|
383 apply(erule Prf_elims) |
|
384 using Prf_elims(2) bnullable_correctness apply force |
|
385 apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2) |
|
386 apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2) |
|
387 using Prf_elims(2) apply force |
|
388 (* ASTAR case *) |
|
389 apply(rename_tac bs r v) |
|
390 apply(simp) |
|
391 apply(erule Prf_elims) |
|
392 apply(clarify) |
|
393 apply(erule Prf_elims) |
|
394 apply(clarify) |
|
395 by (simp add: retrieve_fuse2) |
|
396 |
|
397 |
|
398 lemma MAIN_decode: |
|
399 assumes "\<Turnstile> v : ders s r" |
|
400 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
|
401 using assms |
|
402 proof (induct s arbitrary: v rule: rev_induct) |
|
403 case Nil |
|
404 have "\<Turnstile> v : ders [] r" by fact |
|
405 then have "\<Turnstile> v : r" by simp |
|
406 then have "Some v = decode (retrieve (intern r) v) r" |
|
407 using decode_code retrieve_code by auto |
|
408 then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" |
|
409 by simp |
|
410 next |
|
411 case (snoc c s v) |
|
412 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
|
413 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
|
414 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
|
415 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
|
416 by (simp add: Prf_injval ders_append) |
|
417 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
|
418 by (simp add: flex_append) |
|
419 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
|
420 using asm2 IH by simp |
|
421 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
|
422 using asm by (simp_all add: bder_retrieve ders_append) |
|
423 finally show "Some (flex r id (s @ [c]) v) = |
|
424 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
|
425 qed |
|
426 |
|
427 definition blexer where |
|
428 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
|
429 decode (bmkeps (bders (intern r) s)) r else None" |
|
430 |
|
431 lemma blexer_correctness: |
|
432 shows "blexer r s = lexer r s" |
|
433 proof - |
|
434 { define bds where "bds \<equiv> bders (intern r) s" |
|
435 define ds where "ds \<equiv> ders s r" |
|
436 assume asm: "nullable ds" |
|
437 have era: "erase bds = ds" |
|
438 unfolding ds_def bds_def by simp |
|
439 have mke: "\<Turnstile> mkeps ds : ds" |
|
440 using asm by (simp add: mkeps_nullable) |
|
441 have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" |
|
442 using bmkeps_retrieve |
|
443 using asm era |
|
444 using bnullable_correctness by force |
|
445 also have "... = Some (flex r id s (mkeps ds))" |
|
446 using mke by (simp_all add: MAIN_decode ds_def bds_def) |
|
447 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
|
448 unfolding bds_def ds_def . |
|
449 } |
|
450 then show "blexer r s = lexer r s" |
|
451 unfolding blexer_def lexer_flex |
|
452 by (auto simp add: bnullable_correctness[symmetric]) |
|
453 qed |
|
454 |
|
455 |
|
456 fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list" |
|
457 where |
|
458 "distinctBy [] f acc = []" |
|
459 | "distinctBy (x#xs) f acc = |
|
460 (if (f x) \<in> acc then distinctBy xs f acc |
|
461 else x # (distinctBy xs f ({f x} \<union> acc)))" |
|
462 |
|
463 |
|
464 |
|
465 fun flts :: "arexp list \<Rightarrow> arexp list" |
|
466 where |
|
467 "flts [] = []" |
|
468 | "flts (AZERO # rs) = flts rs" |
|
469 | "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs" |
|
470 | "flts (r1 # rs) = r1 # flts rs" |
|
471 |
|
472 |
|
473 |
|
474 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp" |
|
475 where |
|
476 "bsimp_ASEQ _ AZERO _ = AZERO" |
|
477 | "bsimp_ASEQ _ _ AZERO = AZERO" |
|
478 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
|
479 | "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" |
|
480 |
|
481 lemma bsimp_ASEQ0[simp]: |
|
482 shows "bsimp_ASEQ bs r1 AZERO = AZERO" |
|
483 by (case_tac r1)(simp_all) |
|
484 |
|
485 lemma bsimp_ASEQ1: |
|
486 assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs" |
|
487 shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" |
|
488 using assms |
|
489 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
|
490 apply(auto) |
|
491 done |
|
492 |
|
493 lemma bsimp_ASEQ2[simp]: |
|
494 shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
|
495 by (case_tac r2) (simp_all) |
|
496 |
|
497 |
|
498 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp" |
|
499 where |
|
500 "bsimp_AALTs _ [] = AZERO" |
|
501 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
|
502 | "bsimp_AALTs bs1 rs = AALTs bs1 rs" |
|
503 |
|
504 |
|
505 fun bsimp :: "arexp \<Rightarrow> arexp" |
|
506 where |
|
507 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
508 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) " |
|
509 | "bsimp r = r" |
|
510 |
|
511 |
|
512 fun |
|
513 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
514 where |
|
515 "bders_simp r [] = r" |
|
516 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s" |
|
517 |
|
518 definition blexer_simp where |
|
519 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then |
|
520 decode (bmkeps (bders_simp (intern r) s)) r else None" |
|
521 |
|
522 |
|
523 |
|
524 lemma bders_simp_append: |
|
525 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
|
526 apply(induct s1 arbitrary: r s2) |
|
527 apply(simp_all) |
|
528 done |
|
529 |
|
530 |
|
531 lemma bmkeps_fuse: |
|
532 assumes "bnullable r" |
|
533 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
|
534 using assms |
|
535 by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2) |
|
536 |
|
537 lemma bmkepss_fuse: |
|
538 assumes "bnullables rs" |
|
539 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
|
540 using assms |
|
541 apply(induct rs arbitrary: bs) |
|
542 apply(auto simp add: bmkeps_fuse bnullable_fuse) |
|
543 done |
|
544 |
|
545 lemma bder_fuse: |
|
546 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
|
547 apply(induct a arbitrary: bs c) |
|
548 apply(simp_all) |
|
549 done |
|
550 |
|
551 |
|
552 |
|
553 |
|
554 inductive |
|
555 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
|
556 and |
|
557 srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100) |
|
558 where |
|
559 bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO" |
|
560 | bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO" |
|
561 | bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r" |
|
562 | bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
|
563 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
|
564 | bs6: "AALTs bs [] \<leadsto> AZERO" |
|
565 | bs7: "AALTs bs [r] \<leadsto> fuse bs r" |
|
566 | bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2" |
|
567 | ss1: "[] s\<leadsto> []" |
|
568 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
|
569 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
|
570 | ss4: "(AZERO # rs) s\<leadsto> rs" |
|
571 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
|
572 | ss6: "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
|
573 | ss7: "erase a01 = erase a02 \<and> (distinctBy as2 erase (set (map erase as1)) = as2p) \<Longrightarrow> |
|
574 (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2) (ASTAR bs02 a02)]@rsc) s\<leadsto> |
|
575 (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2p) (ASTAR bs02 a02)]@rsc)" |
|
576 | ss8: "erase a01 = erase a02 \<and> (distinctBy [a2] erase (set (map erase as1)) = []) \<Longrightarrow> |
|
577 (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@[ASEQ bs a2 (ASTAR bs02 a02)]@rsc) s\<leadsto> |
|
578 (rsa@[ASEQ bs (AALTs bs1 as1) (ASTAR bs01 a01)]@rsb@rsc)" |
|
579 | ss9: "erase a01 = erase a02 \<and> (distinctBy as2 erase {erase a1} = as2p) \<Longrightarrow> |
|
580 (rsa@[ASEQ bs a1 (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2) (ASTAR bs02 a02)]@rsc) s\<leadsto> |
|
581 (rsa@[ASEQ bs a1 (ASTAR bs01 a01)]@rsb@[ASEQ bs (AALTs bs2 as2p) (ASTAR bs02 a02)]@rsc)" |
|
582 |
|
583 |
|
584 inductive |
|
585 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
|
586 where |
|
587 rs1[intro, simp]:"r \<leadsto>* r" |
|
588 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3" |
|
589 |
|
590 inductive |
|
591 srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100) |
|
592 where |
|
593 sss1[intro, simp]:"rs s\<leadsto>* rs" |
|
594 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3" |
|
595 |
|
596 |
|
597 |
|
598 |
|
599 fun fmap :: "arexp \<Rightarrow> rexp set" |
|
600 where |
|
601 "fmap AALTs bs rs = flatten (map fmap rs)" |
|
602 | "fmap ASEQ bs (AALTs bs1 rs1) r2 = (flatten (map fmap rs1)) ` (ASEQ bs _ r2)" |
|
603 | "fmap (ASTAR bs r0) = {ASTAR bs r0}" |
|
604 |
|
605 (*r1~r2 --\c> r1c~r2 \<longrightarrow> r1\s~r2 + r2\s1 ... \<longrightarrow> (r1\s ~ r2) +r2\s'+r2\s''+........ *) |
|
606 (* r* \<longrightarrow>r\c ~ r* ---> r\s1 ~ r* + r\s1' ~ r* \<longrightarrow> s1, s1' \<in> suffix s *) |
|
607 (* {r1, r2', r3} {r2,r3,r4} pders\<longrightarrow> {r1-r*, r2-r*, r3-r*, r4-r*} *) |
|
608 |
|
609 lemma iso_pder: |
|
610 "fmap (bders_simp r s) \<subseteq> pderss UNIV r" |
|
611 apply(induction r) |
|
612 prefer 4 |
|
613 oops |
|
614 |
|
615 lemma shape_of_star_after_derssimp: |
|
616 shows "\<forall>bs r s. \<exists>bs1 r1 r2 rs bs2 bsp. (bders_simp (ASTAR bs r) s = (ASEQ bs1 r1 r2)) \<or> |
|
617 (bders_simp (ASTAR bs r) s = (AALTs bs2 rs)) \<or> |
|
618 (bders_simp (ASTAR bs r) s = (ASTAR bsp r))" |
|
619 |
|
620 oops |
|
621 |
|
622 |
|
623 |
|
624 lemma notManyTerms: |
|
625 shows "card {(bders_simp r (Suffix s))| r s. s \<in> L (erase r) } < (size r)" |
|
626 |
|
627 oops |
|
628 |
|
629 lemma rtozero: |
|
630 shows "\<lbrakk>s \<notin> L (erase r); s \<noteq> Nil\<rbrakk> \<Longrightarrow> bders_simp r s = AZERO" |
|
631 apply(induct r) |
|
632 |
|
633 oops |
|
634 |
|
635 lemma r_in_rstar: |
|
636 shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
|
637 using rrewrites.intros(1) rrewrites.intros(2) by blast |
|
638 |
|
639 lemma rrewrites_trans[trans]: |
|
640 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
|
641 shows "r1 \<leadsto>* r3" |
|
642 using a2 a1 |
|
643 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) |
|
644 apply(auto) |
|
645 done |
|
646 |
|
647 lemma srewrites_trans[trans]: |
|
648 assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3" |
|
649 shows "r1 s\<leadsto>* r3" |
|
650 using a1 a2 |
|
651 apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) |
|
652 apply(auto) |
|
653 done |
|
654 |
|
655 |
|
656 |
|
657 lemma contextrewrites0: |
|
658 "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2" |
|
659 apply(induct rs1 rs2 rule: srewrites.inducts) |
|
660 apply simp |
|
661 using bs8 r_in_rstar rrewrites_trans by blast |
|
662 |
|
663 lemma contextrewrites1: |
|
664 "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)" |
|
665 apply(induct r r' rule: rrewrites.induct) |
|
666 apply simp |
|
667 using bs8 ss3 by blast |
|
668 |
|
669 lemma srewrite1: |
|
670 shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)" |
|
671 apply(induct rs) |
|
672 apply(auto) |
|
673 using ss2 by auto |
|
674 |
|
675 lemma srewrites1: |
|
676 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
|
677 apply(induct rs1 rs2 rule: srewrites.induct) |
|
678 apply(auto) |
|
679 using srewrite1 by blast |
|
680 |
|
681 lemma srewrite2: |
|
682 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
|
683 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
|
684 apply(induct rule: rrewrite_srewrite.inducts) |
|
685 apply(auto) |
|
686 apply (metis append_Cons append_Nil srewrites1) |
|
687 apply(meson srewrites.simps ss3) |
|
688 apply (meson srewrites.simps ss4) |
|
689 apply (meson srewrites.simps ss5) |
|
690 by (metis append_Cons append_Nil srewrites.simps ss6) |
|
691 |
|
692 |
|
693 lemma srewrites3: |
|
694 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
|
695 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
|
696 apply(auto) |
|
697 by (meson srewrite2(2) srewrites_trans) |
|
698 |
|
699 (* |
|
700 lemma srewrites4: |
|
701 assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" |
|
702 shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)" |
|
703 using assms |
|
704 apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct) |
|
705 apply (simp add: srewrites3) |
|
706 using srewrite1 by blast |
|
707 *) |
|
708 |
|
709 lemma srewrites6: |
|
710 assumes "r1 \<leadsto>* r2" |
|
711 shows "[r1] s\<leadsto>* [r2]" |
|
712 using assms |
|
713 apply(induct r1 r2 rule: rrewrites.induct) |
|
714 apply(auto) |
|
715 by (meson srewrites.simps srewrites_trans ss3) |
|
716 |
|
717 lemma srewrites7: |
|
718 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
|
719 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
|
720 using assms |
|
721 by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans) |
|
722 |
|
723 lemma ss6_stronger_aux: |
|
724 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))" |
|
725 apply(induct rs2 arbitrary: rs1) |
|
726 apply(auto) |
|
727 apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6) |
|
728 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
|
729 apply(simp) |
|
730 done |
|
731 |
|
732 lemma ss6_stronger: |
|
733 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}" |
|
734 using ss6_stronger_aux[of "[]" _] by auto |
|
735 |
|
736 lemma rewrite_preserves_fuse: |
|
737 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
|
738 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3" |
|
739 proof(induct rule: rrewrite_srewrite.inducts) |
|
740 case (bs3 bs1 bs2 r) |
|
741 then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)" |
|
742 by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) |
|
743 next |
|
744 case (bs7 bs1 r) |
|
745 then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)" |
|
746 by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) |
|
747 next |
|
748 case (ss2 rs1 rs2 r) |
|
749 then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)" |
|
750 by (simp add: rrewrite_srewrite.ss2) |
|
751 next |
|
752 case (ss3 r1 r2 rs) |
|
753 then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)" |
|
754 by (simp add: rrewrite_srewrite.ss3) |
|
755 next |
|
756 case (ss5 bs1 rs1 rsb) |
|
757 have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp |
|
758 also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))" |
|
759 by (simp add: rrewrite_srewrite.ss5) |
|
760 finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)" |
|
761 by (simp add: comp_def fuse_append) |
|
762 next |
|
763 case (ss6 a1 a2 rsa rsb rsc) |
|
764 then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)" |
|
765 apply(simp) |
|
766 apply(rule rrewrite_srewrite.ss6[simplified]) |
|
767 apply(simp add: erase_fuse) |
|
768 done |
|
769 qed (auto intro: rrewrite_srewrite.intros) |
|
770 |
|
771 lemma rewrites_fuse: |
|
772 assumes "r1 \<leadsto>* r2" |
|
773 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
|
774 using assms |
|
775 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) |
|
776 apply(auto intro: rewrite_preserves_fuse) |
|
777 done |
|
778 |
|
779 |
|
780 lemma star_seq: |
|
781 assumes "r1 \<leadsto>* r2" |
|
782 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3" |
|
783 using assms |
|
784 apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct) |
|
785 apply(auto intro: rrewrite_srewrite.intros) |
|
786 done |
|
787 |
|
788 lemma star_seq2: |
|
789 assumes "r3 \<leadsto>* r4" |
|
790 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4" |
|
791 using assms |
|
792 apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct) |
|
793 apply(auto intro: rrewrite_srewrite.intros) |
|
794 done |
|
795 |
|
796 lemma continuous_rewrite: |
|
797 assumes "r1 \<leadsto>* AZERO" |
|
798 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
799 using assms bs1 star_seq by blast |
|
800 |
|
801 (* |
|
802 lemma continuous_rewrite2: |
|
803 assumes "r1 \<leadsto>* AONE bs" |
|
804 shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)" |
|
805 using assms by (meson bs3 rrewrites.simps star_seq) |
|
806 *) |
|
807 |
|
808 lemma bsimp_aalts_simpcases: |
|
809 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
|
810 and "AZERO \<leadsto>* bsimp AZERO" |
|
811 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
|
812 by (simp_all) |
|
813 |
|
814 lemma bsimp_AALTs_rewrites: |
|
815 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
|
816 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
|
817 |
|
818 lemma trivialbsimp_srewrites: |
|
819 assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x" |
|
820 shows "rs s\<leadsto>* (map f rs)" |
|
821 using assms |
|
822 apply(induction rs) |
|
823 apply(simp_all add: srewrites7) |
|
824 done |
|
825 |
|
826 lemma fltsfrewrites: "rs s\<leadsto>* flts rs" |
|
827 apply(induction rs rule: flts.induct) |
|
828 apply(auto intro: rrewrite_srewrite.intros) |
|
829 apply (meson srewrites.simps srewrites1 ss5) |
|
830 using rs1 srewrites7 apply presburger |
|
831 using srewrites7 apply force |
|
832 apply (simp add: srewrites7) |
|
833 by (simp add: srewrites7) |
|
834 |
|
835 lemma bnullable0: |
|
836 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
|
837 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
|
838 apply(induct rule: rrewrite_srewrite.inducts) |
|
839 apply(auto simp add: bnullable_fuse) |
|
840 apply (meson UnCI bnullable_fuse imageI) |
|
841 by (metis bnullable_correctness) |
|
842 |
|
843 |
|
844 lemma rewrites_bnullable_eq: |
|
845 assumes "r1 \<leadsto>* r2" |
|
846 shows "bnullable r1 = bnullable r2" |
|
847 using assms |
|
848 apply(induction r1 r2 rule: rrewrites.induct) |
|
849 apply simp |
|
850 using bnullable0(1) by auto |
|
851 |
|
852 lemma rewrite_bmkeps_aux: |
|
853 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" |
|
854 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 \<Longrightarrow> bmkepss rs1 = bmkepss rs2" |
|
855 proof (induct rule: rrewrite_srewrite.inducts) |
|
856 case (bs3 bs1 bs2 r) |
|
857 have IH2: "bnullable (ASEQ bs1 (AONE bs2) r)" by fact |
|
858 then show "bmkeps (ASEQ bs1 (AONE bs2) r) = bmkeps (fuse (bs1 @ bs2) r)" |
|
859 by (simp add: bmkeps_fuse) |
|
860 next |
|
861 case (bs7 bs r) |
|
862 have IH2: "bnullable (AALTs bs [r])" by fact |
|
863 then show "bmkeps (AALTs bs [r]) = bmkeps (fuse bs r)" |
|
864 by (simp add: bmkeps_fuse) |
|
865 next |
|
866 case (ss3 r1 r2 rs) |
|
867 have IH1: "bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" by fact |
|
868 have as: "r1 \<leadsto> r2" by fact |
|
869 from IH1 as show "bmkepss (r1 # rs) = bmkepss (r2 # rs)" |
|
870 by (simp add: bnullable0) |
|
871 next |
|
872 case (ss5 bs1 rs1 rsb) |
|
873 have "bnullables (AALTs bs1 rs1 # rsb)" by fact |
|
874 then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)" |
|
875 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
|
876 next |
|
877 case (ss6 a1 a2 rsa rsb rsc) |
|
878 have as1: "erase a1 = erase a2" by fact |
|
879 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
|
880 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
|
881 by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) |
|
882 qed (auto) |
|
883 |
|
884 lemma rewrites_bmkeps: |
|
885 assumes "r1 \<leadsto>* r2" "bnullable r1" |
|
886 shows "bmkeps r1 = bmkeps r2" |
|
887 using assms |
|
888 proof(induction r1 r2 rule: rrewrites.induct) |
|
889 case (rs1 r) |
|
890 then show "bmkeps r = bmkeps r" by simp |
|
891 next |
|
892 case (rs2 r1 r2 r3) |
|
893 then have IH: "bmkeps r1 = bmkeps r2" by simp |
|
894 have a1: "bnullable r1" by fact |
|
895 have a2: "r1 \<leadsto>* r2" by fact |
|
896 have a3: "r2 \<leadsto> r3" by fact |
|
897 have a4: "bnullable r2" using a1 a2 by (simp add: rewrites_bnullable_eq) |
|
898 then have "bmkeps r2 = bmkeps r3" |
|
899 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
|
900 then show "bmkeps r1 = bmkeps r3" using IH by simp |
|
901 qed |
|
902 |
|
903 |
|
904 lemma rewrites_to_bsimp: |
|
905 shows "r \<leadsto>* bsimp r" |
|
906 proof (induction r rule: bsimp.induct) |
|
907 case (1 bs1 r1 r2) |
|
908 have IH1: "r1 \<leadsto>* bsimp r1" by fact |
|
909 have IH2: "r2 \<leadsto>* bsimp r2" by fact |
|
910 { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO" |
|
911 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
912 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
913 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
914 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto |
|
915 } |
|
916 moreover |
|
917 { assume "\<exists>bs. bsimp r1 = AONE bs" |
|
918 then obtain bs where as: "bsimp r1 = AONE bs" by blast |
|
919 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
920 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
921 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)" |
|
922 using rewrites_fuse by (meson rrewrites_trans) |
|
923 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp |
|
924 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) |
|
925 } |
|
926 moreover |
|
927 { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" |
|
928 then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
929 by (simp add: bsimp_ASEQ1) |
|
930 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 |
|
931 by (metis rrewrites_trans star_seq star_seq2) |
|
932 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp |
|
933 } |
|
934 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast |
|
935 next |
|
936 case (2 bs1 rs) |
|
937 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact |
|
938 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) |
|
939 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) |
|
940 also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger) |
|
941 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" |
|
942 using contextrewrites0 by blast |
|
943 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" |
|
944 by (simp add: bsimp_AALTs_rewrites) |
|
945 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp |
|
946 qed (simp_all) |
|
947 |
|
948 |
|
949 lemma to_zero_in_alt: |
|
950 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
|
951 by (simp add: bs1 bs8 ss3) |
|
952 |
|
953 |
|
954 |
|
955 lemma bder_fuse_list: |
|
956 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
|
957 apply(induction rs1) |
|
958 apply(simp_all add: bder_fuse) |
|
959 done |
|
960 |
|
961 lemma rewrite_preserves_bder: |
|
962 shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2" |
|
963 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
|
964 proof(induction rule: rrewrite_srewrite.inducts) |
|
965 case (bs1 bs r2) |
|
966 show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO" |
|
967 by (simp add: continuous_rewrite) |
|
968 next |
|
969 case (bs2 bs r1) |
|
970 show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO" |
|
971 apply(auto) |
|
972 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
|
973 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
|
974 next |
|
975 case (bs3 bs1 bs2 r) |
|
976 show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)" |
|
977 apply(simp) |
|
978 by (metis (no_types, lifting) bder_fuse bs8 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
|
979 next |
|
980 case (bs4 r1 r2 bs r3) |
|
981 have as: "r1 \<leadsto> r2" by fact |
|
982 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
983 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)" |
|
984 by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq) |
|
985 next |
|
986 case (bs5 r3 r4 bs r1) |
|
987 have as: "r3 \<leadsto> r4" by fact |
|
988 have IH: "bder c r3 \<leadsto>* bder c r4" by fact |
|
989 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" |
|
990 apply(simp) |
|
991 apply(auto) |
|
992 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
|
993 using star_seq2 by blast |
|
994 next |
|
995 case (bs6 bs) |
|
996 show "bder c (AALTs bs []) \<leadsto>* bder c AZERO" |
|
997 using rrewrite_srewrite.bs6 by force |
|
998 next |
|
999 case (bs7 bs r) |
|
1000 show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)" |
|
1001 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
|
1002 next |
|
1003 case (bs8 rs1 rs2 bs) |
|
1004 have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact |
|
1005 then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)" |
|
1006 using contextrewrites0 by force |
|
1007 next |
|
1008 case ss1 |
|
1009 show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp |
|
1010 next |
|
1011 case (ss2 rs1 rs2 r) |
|
1012 have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact |
|
1013 then show "map (bder c) (r # rs1) s\<leadsto>* map (bder c) (r # rs2)" |
|
1014 by (simp add: srewrites7) |
|
1015 next |
|
1016 case (ss3 r1 r2 rs) |
|
1017 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
1018 then show "map (bder c) (r1 # rs) s\<leadsto>* map (bder c) (r2 # rs)" |
|
1019 by (simp add: srewrites7) |
|
1020 next |
|
1021 case (ss4 rs) |
|
1022 show "map (bder c) (AZERO # rs) s\<leadsto>* map (bder c) rs" |
|
1023 using rrewrite_srewrite.ss4 by fastforce |
|
1024 next |
|
1025 case (ss5 bs1 rs1 rsb) |
|
1026 show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)" |
|
1027 apply(simp) |
|
1028 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
|
1029 next |
|
1030 case (ss6 a1 a2 bs rsa rsb) |
|
1031 have as: "erase a1 = erase a2" by fact |
|
1032 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
|
1033 apply(simp only: map_append) |
|
1034 by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps) |
|
1035 qed |
|
1036 |
|
1037 lemma rewrites_preserves_bder: |
|
1038 assumes "r1 \<leadsto>* r2" |
|
1039 shows "bder c r1 \<leadsto>* bder c r2" |
|
1040 using assms |
|
1041 apply(induction r1 r2 rule: rrewrites.induct) |
|
1042 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
|
1043 done |
|
1044 |
|
1045 |
|
1046 lemma central: |
|
1047 shows "bders r s \<leadsto>* bders_simp r s" |
|
1048 proof(induct s arbitrary: r rule: rev_induct) |
|
1049 case Nil |
|
1050 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
|
1051 next |
|
1052 case (snoc x xs) |
|
1053 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
|
1054 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
|
1055 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
|
1056 by (simp add: rewrites_preserves_bder) |
|
1057 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
|
1058 by (simp add: rewrites_to_bsimp) |
|
1059 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
|
1060 by (simp add: bders_simp_append) |
|
1061 qed |
|
1062 |
|
1063 lemma main_aux: |
|
1064 assumes "bnullable (bders r s)" |
|
1065 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
|
1066 proof - |
|
1067 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
|
1068 then |
|
1069 show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms |
|
1070 by (rule rewrites_bmkeps) |
|
1071 qed |
|
1072 |
|
1073 |
|
1074 theorem main_blexer_simp: |
|
1075 shows "blexer r s = blexer_simp r s" |
|
1076 unfolding blexer_def blexer_simp_def |
|
1077 by (metis central main_aux rewrites_bnullable_eq) |
|
1078 |
|
1079 |
|
1080 theorem blexersimp_correctness: |
|
1081 shows "lexer r s = blexer_simp r s" |
|
1082 using blexer_correctness main_blexer_simp by simp |
|
1083 |
|
1084 |
|
1085 (* below is the idempotency of bsimp *) |
|
1086 |
|
1087 lemma bsimp_ASEQ_fuse: |
|
1088 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
|
1089 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |
|
1090 apply(auto) |
|
1091 done |
|
1092 |
|
1093 lemma bsimp_AALTs_fuse: |
|
1094 assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r" |
|
1095 shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs" |
|
1096 using assms |
|
1097 apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct) |
|
1098 apply(auto) |
|
1099 done |
|
1100 |
|
1101 lemma bsimp_fuse: |
|
1102 shows "fuse bs (bsimp r) = bsimp (fuse bs r)" |
|
1103 apply(induct r arbitrary: bs) |
|
1104 apply(simp_all add: bsimp_ASEQ_fuse bsimp_AALTs_fuse fuse_append) |
|
1105 done |
|
1106 |
|
1107 lemma bsimp_ASEQ_idem: |
|
1108 assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2" |
|
1109 shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)" |
|
1110 using assms |
|
1111 apply(case_tac "bsimp r1 = AZERO") |
|
1112 apply(simp) |
|
1113 apply(case_tac "bsimp r2 = AZERO") |
|
1114 apply(simp) |
|
1115 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1116 apply(auto)[1] |
|
1117 apply (metis bsimp_fuse) |
|
1118 apply(simp add: bsimp_ASEQ1) |
|
1119 done |
|
1120 |
|
1121 lemma bsimp_AALTs_idem: |
|
1122 assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" |
|
1123 shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (map bsimp rs)" |
|
1124 using assms |
|
1125 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
1126 apply(simp) |
|
1127 apply(simp) |
|
1128 using bsimp_fuse apply presburger |
|
1129 oops |
|
1130 |
|
1131 lemma bsimp_idem_rev: |
|
1132 shows "\<nexists>r2. bsimp r1 \<leadsto> r2" |
|
1133 apply(induct r1 rule: bsimp.induct) |
|
1134 apply(auto) |
|
1135 defer |
|
1136 defer |
|
1137 using rrewrite.simps apply blast |
|
1138 using rrewrite.cases apply blast |
|
1139 using rrewrite.simps apply blast |
|
1140 using rrewrite.cases apply blast |
|
1141 apply(case_tac "bsimp r1 = AZERO") |
|
1142 apply(simp) |
|
1143 apply(case_tac "bsimp r2 = AZERO") |
|
1144 apply(simp) |
|
1145 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1146 apply(auto)[1] |
|
1147 prefer 2 |
|
1148 apply (smt (verit, best) arexp.distinct(25) arexp.inject(3) bsimp_ASEQ1 rrewrite.simps) |
|
1149 defer |
|
1150 oops |
|
1151 |
|
1152 lemma bsimp_idem: |
|
1153 shows "bsimp (bsimp r) = bsimp r" |
|
1154 apply(induct r rule: bsimp.induct) |
|
1155 apply(auto) |
|
1156 using bsimp_ASEQ_idem apply presburger |
|
1157 oops |
|
1158 |
|
1159 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
|
1160 |
|
1161 |
|
1162 unused_thms |
|
1163 |
|
1164 |
|
1165 fun concatLen:: "arexp \<Rightarrow> int" |
|
1166 where |
|
1167 "concatLen AZERO = 0" |
|
1168 | "concatLen (AONE bs) = 0" |
|
1169 | "concatLen (ACHAR bs a) = 0" |
|
1170 | "concatLen (ASEQ bs a1 a2) = 1 + (max (concatLen a1) ( concatLen a2))" |
|
1171 | "concatLen (ASTAR bs r0) = 1 + (concatLen r0)" |
|
1172 | "concatLen (AALTS bs as) = foldl max (map concatLen as)" |
|
1173 |
|
1174 |
|
1175 |
|
1176 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
|
1177 where |
|
1178 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
|
1179 |
|
1180 |
|
1181 |
|
1182 end |