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