equal
deleted
inserted
replaced
16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)" |
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)" |
17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)" |
18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True" |
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))" |
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" |
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)" |
21 | "_ ~1 _ = False" |
22 | "_ ~1 _ = False" |
22 |
23 |
23 |
24 |
24 |
25 |
25 lemma eq1_L: |
26 lemma eq1_L: |
100 |
101 |
101 lemma bmkeps_fuse: |
102 lemma bmkeps_fuse: |
102 assumes "bnullable r" |
103 assumes "bnullable r" |
103 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
104 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
104 using assms |
105 using assms |
105 by (induct r rule: bnullable.induct) (auto) |
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 |
106 |
112 |
107 lemma bmkepss_fuse: |
113 lemma bmkepss_fuse: |
108 assumes "bnullables rs" |
114 assumes "bnullables rs" |
109 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
115 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
110 using assms |
116 using assms |
361 apply(auto intro: rrewrite_srewrite.intros) |
367 apply(auto intro: rrewrite_srewrite.intros) |
362 apply (meson srewrites.simps srewrites1 ss5) |
368 apply (meson srewrites.simps srewrites1 ss5) |
363 using rs1 srewrites7 apply presburger |
369 using rs1 srewrites7 apply presburger |
364 using srewrites7 apply force |
370 using srewrites7 apply force |
365 apply (simp add: srewrites7) |
371 apply (simp add: srewrites7) |
|
372 apply(simp add: srewrites7) |
366 by (simp add: srewrites7) |
373 by (simp add: srewrites7) |
|
374 |
367 |
375 |
368 lemma bnullable0: |
376 lemma bnullable0: |
369 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
377 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
370 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
378 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
371 apply(induct rule: rrewrite_srewrite.inducts) |
379 apply(induct rule: rrewrite_srewrite.inducts) |
396 then show ?case |
404 then show ?case |
397 using bmkepss.simps bnullable0(1) by presburger |
405 using bmkepss.simps bnullable0(1) by presburger |
398 next |
406 next |
399 case (ss5 bs1 rs1 rsb) |
407 case (ss5 bs1 rs1 rsb) |
400 then show ?case |
408 then show ?case |
401 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
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)) |
402 next |
416 next |
403 case (ss6 a1 a2 rsa rsb rsc) |
417 case (ss6 a1 a2 rsa rsb rsc) |
404 then show ?case |
418 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) |
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)) |
406 qed (auto) |
424 qed (auto) |
407 |
425 |
408 lemma rewrites_bmkeps: |
426 lemma rewrites_bmkeps: |
409 assumes "r1 \<leadsto>* r2" "bnullable r1" |
427 assumes "r1 \<leadsto>* r2" "bnullable r1" |
410 shows "bmkeps r1 = bmkeps r2" |
428 shows "bmkeps r1 = bmkeps r2" |