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