|
1 theory BlexerSimp |
|
2 imports Blexer |
|
3 begin |
|
4 |
|
5 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list" |
|
6 where |
|
7 "distinctWith [] eq acc = []" |
|
8 | "distinctWith (x # xs) eq acc = |
|
9 (if (\<exists> y \<in> acc. eq x y) then distinctWith xs eq acc |
|
10 else x # (distinctWith xs eq ({x} \<union> acc)))" |
|
11 |
|
12 |
|
13 fun eq1 ("_ ~1 _" [80, 80] 80) where |
|
14 "AZERO ~1 AZERO = True" |
|
15 | "(AONE bs1) ~1 (AONE bs2) = True" |
|
16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)" |
|
17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)" |
|
18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True" |
|
19 | "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))" |
|
20 | "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2" |
|
21 | "(ANTIMES bs1 r1 n1) ~1 (ANTIMES bs2 r2 n2) = (r1 ~1 r2 \<and> n1 = n2)" |
|
22 | "_ ~1 _ = False" |
|
23 |
|
24 |
|
25 |
|
26 lemma eq1_L: |
|
27 assumes "x ~1 y" |
|
28 shows "L (erase x) = L (erase y)" |
|
29 using assms |
|
30 apply(induct rule: eq1.induct) |
|
31 apply(auto elim: eq1.elims) |
|
32 apply presburger |
|
33 done |
|
34 |
|
35 fun flts :: "arexp list \<Rightarrow> arexp list" |
|
36 where |
|
37 "flts [] = []" |
|
38 | "flts (AZERO # rs) = flts rs" |
|
39 | "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs" |
|
40 | "flts (r1 # rs) = r1 # flts rs" |
|
41 |
|
42 |
|
43 |
|
44 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp" |
|
45 where |
|
46 "bsimp_ASEQ _ AZERO _ = AZERO" |
|
47 | "bsimp_ASEQ _ _ AZERO = AZERO" |
|
48 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
|
49 | "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" |
|
50 |
|
51 lemma bsimp_ASEQ0[simp]: |
|
52 shows "bsimp_ASEQ bs r1 AZERO = AZERO" |
|
53 by (case_tac r1)(simp_all) |
|
54 |
|
55 lemma bsimp_ASEQ1: |
|
56 assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs" |
|
57 shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" |
|
58 using assms |
|
59 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
|
60 apply(auto) |
|
61 done |
|
62 |
|
63 lemma bsimp_ASEQ2[simp]: |
|
64 shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
|
65 by (case_tac r2) (simp_all) |
|
66 |
|
67 |
|
68 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp" |
|
69 where |
|
70 "bsimp_AALTs _ [] = AZERO" |
|
71 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
|
72 | "bsimp_AALTs bs1 rs = AALTs bs1 rs" |
|
73 |
|
74 |
|
75 |
|
76 |
|
77 fun bsimp :: "arexp \<Rightarrow> arexp" |
|
78 where |
|
79 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
80 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) " |
|
81 | "bsimp r = r" |
|
82 |
|
83 |
|
84 fun |
|
85 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
86 where |
|
87 "bders_simp r [] = r" |
|
88 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s" |
|
89 |
|
90 definition blexer_simp where |
|
91 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then |
|
92 decode (bmkeps (bders_simp (intern r) s)) r else None" |
|
93 |
|
94 |
|
95 |
|
96 lemma bders_simp_append: |
|
97 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
|
98 apply(induct s1 arbitrary: r s2) |
|
99 apply(simp_all) |
|
100 done |
|
101 |
|
102 lemma bmkeps_fuse: |
|
103 assumes "bnullable r" |
|
104 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
|
105 using assms |
|
106 apply(induct r rule: bnullable.induct) |
|
107 apply(auto) |
|
108 apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
109 apply(case_tac n) |
|
110 apply(auto) |
|
111 done |
|
112 |
|
113 lemma bmkepss_fuse: |
|
114 assumes "bnullables rs" |
|
115 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
|
116 using assms |
|
117 apply(induct rs arbitrary: bs) |
|
118 apply(auto simp add: bmkeps_fuse bnullable_fuse) |
|
119 done |
|
120 |
|
121 lemma bder_fuse: |
|
122 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
|
123 apply(induct a arbitrary: bs c) |
|
124 apply(simp_all) |
|
125 done |
|
126 |
|
127 |
|
128 |
|
129 |
|
130 inductive |
|
131 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
|
132 and |
|
133 srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100) |
|
134 where |
|
135 bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO" |
|
136 | bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO" |
|
137 | bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r" |
|
138 | bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
|
139 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
|
140 | bs6: "AALTs bs [] \<leadsto> AZERO" |
|
141 | bs7: "AALTs bs [r] \<leadsto> fuse bs r" |
|
142 | bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2" |
|
143 | ss1: "[] s\<leadsto> []" |
|
144 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
|
145 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
|
146 | ss4: "(AZERO # rs) s\<leadsto> rs" |
|
147 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
|
148 | ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
|
149 |
|
150 |
|
151 inductive |
|
152 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
|
153 where |
|
154 rs1[intro, simp]:"r \<leadsto>* r" |
|
155 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3" |
|
156 |
|
157 inductive |
|
158 srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100) |
|
159 where |
|
160 sss1[intro, simp]:"rs s\<leadsto>* rs" |
|
161 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3" |
|
162 |
|
163 |
|
164 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
|
165 using rrewrites.intros(1) rrewrites.intros(2) by blast |
|
166 |
|
167 lemma rs_in_rstar: |
|
168 shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<leadsto>* r2" |
|
169 using rrewrites.intros(1) rrewrites.intros(2) by blast |
|
170 |
|
171 |
|
172 lemma rrewrites_trans[trans]: |
|
173 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
|
174 shows "r1 \<leadsto>* r3" |
|
175 using a2 a1 |
|
176 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) |
|
177 apply(auto) |
|
178 done |
|
179 |
|
180 lemma srewrites_trans[trans]: |
|
181 assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3" |
|
182 shows "r1 s\<leadsto>* r3" |
|
183 using a1 a2 |
|
184 apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) |
|
185 apply(auto) |
|
186 done |
|
187 |
|
188 |
|
189 |
|
190 lemma contextrewrites0: |
|
191 "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2" |
|
192 apply(induct rs1 rs2 rule: srewrites.inducts) |
|
193 apply simp |
|
194 using bs10 r_in_rstar rrewrites_trans by blast |
|
195 |
|
196 lemma contextrewrites1: |
|
197 "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)" |
|
198 apply(induct r r' rule: rrewrites.induct) |
|
199 apply simp |
|
200 using bs10 ss3 by blast |
|
201 |
|
202 lemma srewrite1: |
|
203 shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)" |
|
204 apply(induct rs) |
|
205 apply(auto) |
|
206 using ss2 by auto |
|
207 |
|
208 lemma srewrites1: |
|
209 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
|
210 apply(induct rs1 rs2 rule: srewrites.induct) |
|
211 apply(auto) |
|
212 using srewrite1 by blast |
|
213 |
|
214 lemma srewrite2: |
|
215 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
|
216 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
|
217 apply(induct rule: rrewrite_srewrite.inducts) |
|
218 apply(auto) |
|
219 apply (metis append_Cons append_Nil srewrites1) |
|
220 apply(meson srewrites.simps ss3) |
|
221 apply (meson srewrites.simps ss4) |
|
222 apply (meson srewrites.simps ss5) |
|
223 by (metis append_Cons append_Nil srewrites.simps ss6) |
|
224 |
|
225 |
|
226 lemma srewrites3: |
|
227 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
|
228 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
|
229 apply(auto) |
|
230 by (meson srewrite2(2) srewrites_trans) |
|
231 |
|
232 (* |
|
233 lemma srewrites4: |
|
234 assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" |
|
235 shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)" |
|
236 using assms |
|
237 apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct) |
|
238 apply (simp add: srewrites3) |
|
239 using srewrite1 by blast |
|
240 *) |
|
241 |
|
242 lemma srewrites6: |
|
243 assumes "r1 \<leadsto>* r2" |
|
244 shows "[r1] s\<leadsto>* [r2]" |
|
245 using assms |
|
246 apply(induct r1 r2 rule: rrewrites.induct) |
|
247 apply(auto) |
|
248 by (meson srewrites.simps srewrites_trans ss3) |
|
249 |
|
250 lemma srewrites7: |
|
251 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
|
252 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
|
253 using assms |
|
254 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
|
255 |
|
256 lemma ss6_stronger_aux: |
|
257 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctWith rs2 eq1 (set rs1))" |
|
258 apply(induct rs2 arbitrary: rs1) |
|
259 apply(auto) |
|
260 prefer 2 |
|
261 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
|
262 apply(simp) |
|
263 apply(drule_tac x="rs1" in meta_spec) |
|
264 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
265 using srewrites_trans apply blast |
|
266 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
|
267 prefer 2 |
|
268 apply (simp add: split_list) |
|
269 apply(erule exE)+ |
|
270 apply(simp) |
|
271 using eq1_L rs_in_rstar ss6 by force |
|
272 |
|
273 lemma ss6_stronger: |
|
274 shows "rs1 s\<leadsto>* distinctWith rs1 eq1 {}" |
|
275 by (metis append_Nil list.set(1) ss6_stronger_aux) |
|
276 |
|
277 |
|
278 lemma rewrite_preserves_fuse: |
|
279 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
|
280 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
|
281 proof(induct rule: rrewrite_srewrite.inducts) |
|
282 case (bs3 bs1 bs2 r) |
|
283 then show ?case |
|
284 by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) |
|
285 next |
|
286 case (bs7 bs r) |
|
287 then show ?case |
|
288 by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) |
|
289 next |
|
290 case (ss2 rs1 rs2 r) |
|
291 then show ?case |
|
292 using srewrites7 by force |
|
293 next |
|
294 case (ss3 r1 r2 rs) |
|
295 then show ?case by (simp add: r_in_rstar srewrites7) |
|
296 next |
|
297 case (ss5 bs1 rs1 rsb) |
|
298 then show ?case |
|
299 apply(simp) |
|
300 by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps) |
|
301 next |
|
302 case (ss6 a1 a2 rsa rsb rsc) |
|
303 then show ?case |
|
304 apply(simp only: map_append) |
|
305 by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) |
|
306 qed (auto intro: rrewrite_srewrite.intros) |
|
307 |
|
308 |
|
309 lemma rewrites_fuse: |
|
310 assumes "r1 \<leadsto>* r2" |
|
311 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
|
312 using assms |
|
313 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) |
|
314 apply(auto intro: rewrite_preserves_fuse rrewrites_trans) |
|
315 done |
|
316 |
|
317 |
|
318 lemma star_seq: |
|
319 assumes "r1 \<leadsto>* r2" |
|
320 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3" |
|
321 using assms |
|
322 apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct) |
|
323 apply(auto intro: rrewrite_srewrite.intros) |
|
324 done |
|
325 |
|
326 lemma star_seq2: |
|
327 assumes "r3 \<leadsto>* r4" |
|
328 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4" |
|
329 using assms |
|
330 apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct) |
|
331 apply(auto intro: rrewrite_srewrite.intros) |
|
332 done |
|
333 |
|
334 lemma continuous_rewrite: |
|
335 assumes "r1 \<leadsto>* AZERO" |
|
336 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
337 using assms bs1 star_seq by blast |
|
338 |
|
339 (* |
|
340 lemma continuous_rewrite2: |
|
341 assumes "r1 \<leadsto>* AONE bs" |
|
342 shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)" |
|
343 using assms by (meson bs3 rrewrites.simps star_seq) |
|
344 *) |
|
345 |
|
346 lemma bsimp_aalts_simpcases: |
|
347 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
|
348 and "AZERO \<leadsto>* bsimp AZERO" |
|
349 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
|
350 by (simp_all) |
|
351 |
|
352 lemma bsimp_AALTs_rewrites: |
|
353 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
|
354 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
|
355 |
|
356 lemma trivialbsimp_srewrites: |
|
357 "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)" |
|
358 apply(induction rs) |
|
359 apply simp |
|
360 apply(simp) |
|
361 using srewrites7 by auto |
|
362 |
|
363 |
|
364 |
|
365 lemma fltsfrewrites: "rs s\<leadsto>* flts rs" |
|
366 apply(induction rs rule: flts.induct) |
|
367 apply(auto intro: rrewrite_srewrite.intros) |
|
368 apply (meson srewrites.simps srewrites1 ss5) |
|
369 using rs1 srewrites7 apply presburger |
|
370 using srewrites7 apply force |
|
371 apply (simp add: srewrites7) |
|
372 apply(simp add: srewrites7) |
|
373 by (simp add: srewrites7) |
|
374 |
|
375 |
|
376 lemma bnullable0: |
|
377 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
|
378 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
|
379 apply(induct rule: rrewrite_srewrite.inducts) |
|
380 apply(auto simp add: bnullable_fuse) |
|
381 apply (meson UnCI bnullable_fuse imageI) |
|
382 using bnullable_correctness nullable_correctness by blast |
|
383 |
|
384 |
|
385 lemma rewritesnullable: |
|
386 assumes "r1 \<leadsto>* r2" |
|
387 shows "bnullable r1 = bnullable r2" |
|
388 using assms |
|
389 apply(induction r1 r2 rule: rrewrites.induct) |
|
390 apply simp |
|
391 using bnullable0(1) by auto |
|
392 |
|
393 lemma rewrite_bmkeps_aux: |
|
394 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
|
395 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
|
396 proof (induct rule: rrewrite_srewrite.inducts) |
|
397 case (bs3 bs1 bs2 r) |
|
398 then show ?case by (simp add: bmkeps_fuse) |
|
399 next |
|
400 case (bs7 bs r) |
|
401 then show ?case by (simp add: bmkeps_fuse) |
|
402 next |
|
403 case (ss3 r1 r2 rs) |
|
404 then show ?case |
|
405 using bmkepss.simps bnullable0(1) by presburger |
|
406 next |
|
407 case (ss5 bs1 rs1 rsb) |
|
408 then show ?case |
|
409 apply (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
|
410 apply(case_tac rs1) |
|
411 apply(auto simp add: bnullable_fuse) |
|
412 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
413 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
414 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
415 by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
416 next |
|
417 case (ss6 a1 a2 rsa rsb rsc) |
|
418 then show ?case |
|
419 by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) |
|
420 next |
|
421 case (bs10 rs1 rs2 bs) |
|
422 then show ?case |
|
423 by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
424 qed (auto) |
|
425 |
|
426 lemma rewrites_bmkeps: |
|
427 assumes "r1 \<leadsto>* r2" "bnullable r1" |
|
428 shows "bmkeps r1 = bmkeps r2" |
|
429 using assms |
|
430 proof(induction r1 r2 rule: rrewrites.induct) |
|
431 case (rs1 r) |
|
432 then show "bmkeps r = bmkeps r" by simp |
|
433 next |
|
434 case (rs2 r1 r2 r3) |
|
435 then have IH: "bmkeps r1 = bmkeps r2" by simp |
|
436 have a1: "bnullable r1" by fact |
|
437 have a2: "r1 \<leadsto>* r2" by fact |
|
438 have a3: "r2 \<leadsto> r3" by fact |
|
439 have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) |
|
440 then have "bmkeps r2 = bmkeps r3" |
|
441 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
|
442 then show "bmkeps r1 = bmkeps r3" using IH by simp |
|
443 qed |
|
444 |
|
445 |
|
446 lemma rewrites_to_bsimp: |
|
447 shows "r \<leadsto>* bsimp r" |
|
448 proof (induction r rule: bsimp.induct) |
|
449 case (1 bs1 r1 r2) |
|
450 have IH1: "r1 \<leadsto>* bsimp r1" by fact |
|
451 have IH2: "r2 \<leadsto>* bsimp r2" by fact |
|
452 { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO" |
|
453 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
454 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
455 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
456 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto |
|
457 } |
|
458 moreover |
|
459 { assume "\<exists>bs. bsimp r1 = AONE bs" |
|
460 then obtain bs where as: "bsimp r1 = AONE bs" by blast |
|
461 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
462 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
463 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)" |
|
464 using rewrites_fuse by (meson rrewrites_trans) |
|
465 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp |
|
466 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) |
|
467 } |
|
468 moreover |
|
469 { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" |
|
470 then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
471 by (simp add: bsimp_ASEQ1) |
|
472 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 |
|
473 by (metis rrewrites_trans star_seq star_seq2) |
|
474 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp |
|
475 } |
|
476 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast |
|
477 next |
|
478 case (2 bs1 rs) |
|
479 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact |
|
480 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) |
|
481 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) |
|
482 also have "... s\<leadsto>* distinctWith (flts (map bsimp rs)) eq1 {}" by (simp add: ss6_stronger) |
|
483 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
484 using contextrewrites0 by auto |
|
485 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
486 by (simp add: bsimp_AALTs_rewrites) |
|
487 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp |
|
488 qed (simp_all) |
|
489 |
|
490 |
|
491 lemma to_zero_in_alt: |
|
492 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
|
493 by (simp add: bs1 bs10 ss3) |
|
494 |
|
495 |
|
496 |
|
497 lemma bder_fuse_list: |
|
498 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
|
499 apply(induction rs1) |
|
500 apply(simp_all add: bder_fuse) |
|
501 done |
|
502 |
|
503 lemma map1: |
|
504 shows "(map f [a]) = [f a]" |
|
505 by (simp) |
|
506 |
|
507 lemma rewrite_preserves_bder: |
|
508 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
|
509 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
|
510 proof(induction rule: rrewrite_srewrite.inducts) |
|
511 case (bs1 bs r2) |
|
512 then show ?case |
|
513 by (simp add: continuous_rewrite) |
|
514 next |
|
515 case (bs2 bs r1) |
|
516 then show ?case |
|
517 apply(auto) |
|
518 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
|
519 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
|
520 next |
|
521 case (bs3 bs1 bs2 r) |
|
522 then show ?case |
|
523 apply(simp) |
|
524 |
|
525 by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
|
526 next |
|
527 case (bs4 r1 r2 bs r3) |
|
528 have as: "r1 \<leadsto> r2" by fact |
|
529 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
530 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)" |
|
531 by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq) |
|
532 next |
|
533 case (bs5 r3 r4 bs r1) |
|
534 have as: "r3 \<leadsto> r4" by fact |
|
535 have IH: "bder c r3 \<leadsto>* bder c r4" by fact |
|
536 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" |
|
537 apply(simp) |
|
538 apply(auto) |
|
539 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
|
540 using star_seq2 by blast |
|
541 next |
|
542 case (bs6 bs) |
|
543 then show ?case |
|
544 using rrewrite_srewrite.bs6 by force |
|
545 next |
|
546 case (bs7 bs r) |
|
547 then show ?case |
|
548 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
|
549 next |
|
550 case (bs10 rs1 rs2 bs) |
|
551 then show ?case |
|
552 using contextrewrites0 by force |
|
553 next |
|
554 case ss1 |
|
555 then show ?case by simp |
|
556 next |
|
557 case (ss2 rs1 rs2 r) |
|
558 then show ?case |
|
559 by (simp add: srewrites7) |
|
560 next |
|
561 case (ss3 r1 r2 rs) |
|
562 then show ?case |
|
563 by (simp add: srewrites7) |
|
564 next |
|
565 case (ss4 rs) |
|
566 then show ?case |
|
567 using rrewrite_srewrite.ss4 by fastforce |
|
568 next |
|
569 case (ss5 bs1 rs1 rsb) |
|
570 then show ?case |
|
571 apply(simp) |
|
572 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
|
573 next |
|
574 case (ss6 a1 a2 bs rsa rsb) |
|
575 then show ?case |
|
576 apply(simp only: map_append map1) |
|
577 apply(rule srewrites_trans) |
|
578 apply(rule rs_in_rstar) |
|
579 apply(rule_tac rrewrite_srewrite.ss6) |
|
580 using Der_def der_correctness apply auto[1] |
|
581 by blast |
|
582 qed |
|
583 |
|
584 lemma rewrites_preserves_bder: |
|
585 assumes "r1 \<leadsto>* r2" |
|
586 shows "bder c r1 \<leadsto>* bder c r2" |
|
587 using assms |
|
588 apply(induction r1 r2 rule: rrewrites.induct) |
|
589 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
|
590 done |
|
591 |
|
592 |
|
593 lemma central: |
|
594 shows "bders r s \<leadsto>* bders_simp r s" |
|
595 proof(induct s arbitrary: r rule: rev_induct) |
|
596 case Nil |
|
597 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
|
598 next |
|
599 case (snoc x xs) |
|
600 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
|
601 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
|
602 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
|
603 by (simp add: rewrites_preserves_bder) |
|
604 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
|
605 by (simp add: rewrites_to_bsimp) |
|
606 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
|
607 by (simp add: bders_simp_append) |
|
608 qed |
|
609 |
|
610 lemma main_aux: |
|
611 assumes "bnullable (bders r s)" |
|
612 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
|
613 proof - |
|
614 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
|
615 then |
|
616 show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms |
|
617 by (rule rewrites_bmkeps) |
|
618 qed |
|
619 |
|
620 |
|
621 |
|
622 |
|
623 theorem main_blexer_simp: |
|
624 shows "blexer r s = blexer_simp r s" |
|
625 unfolding blexer_def blexer_simp_def |
|
626 by (metis central main_aux rewritesnullable) |
|
627 |
|
628 theorem blexersimp_correctness: |
|
629 shows "lexer r s = blexer_simp r s" |
|
630 using blexer_correctness main_blexer_simp by simp |
|
631 |
|
632 |
|
633 unused_thms |
|
634 |
|
635 end |