equal
deleted
inserted
replaced
465 | "flts (AZERO # rs) = flts rs" |
465 | "flts (AZERO # rs) = flts rs" |
466 | "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs" |
466 | "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs" |
467 | "flts (r1 # rs) = r1 # flts rs" |
467 | "flts (r1 # rs) = r1 # flts rs" |
468 |
468 |
469 |
469 |
470 |
|
471 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp" |
470 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp" |
472 where |
471 where |
473 "bsimp_ASEQ _ AZERO _ = AZERO" |
472 "bsimp_ASEQ _ AZERO _ = AZERO" |
474 | "bsimp_ASEQ _ _ AZERO = AZERO" |
473 | "bsimp_ASEQ _ _ AZERO = AZERO" |
475 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
474 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
693 apply(simp) |
692 apply(simp) |
694 using ss6[simplified] |
693 using ss6[simplified] |
695 using rs_in_rstar by force |
694 using rs_in_rstar by force |
696 |
695 |
697 lemma ss6_stronger: |
696 lemma ss6_stronger: |
698 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}" |
697 shows "rs s\<leadsto>* distinctBy rs erase {}" |
699 using ss6_stronger_aux[of "[]" _] by auto |
698 using ss6_stronger_aux[of "[]" _] by auto |
700 |
699 |
701 lemma rewrite_preserves_fuse: |
700 lemma rewrite_preserves_fuse: |
702 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
701 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
703 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3" |
702 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3" |