equal
deleted
inserted
replaced
177 where |
177 where |
178 "bmkeps(AONE bs) = bs" |
178 "bmkeps(AONE bs) = bs" |
179 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
179 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
180 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)" |
180 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)" |
181 | "bmkeps(ASTAR bs r) = bs @ [S]" |
181 | "bmkeps(ASTAR bs r) = bs @ [S]" |
182 | "bmkepss [] = []" |
182 (*| "bmkepss [] = []"*) |
183 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
183 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
184 |
184 |
185 lemma bmkepss1: |
185 lemma bmkepss1: |
186 assumes "\<not> bnullables rs1" |
186 assumes "\<not> bnullables rs1" |
187 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
187 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
847 next |
847 next |
848 case (ss6 a2 a1 rsa rsb rsc) |
848 case (ss6 a2 a1 rsa rsb rsc) |
849 have as1: "L(erase a2) \<subseteq> L(erase a1)" by fact |
849 have as1: "L(erase a2) \<subseteq> L(erase a1)" by fact |
850 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
850 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
851 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
851 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
852 by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq) |
852 by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(1) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq) |
853 (*next |
853 (*next |
854 case (extra bs0 bs1 r1 bs2 r2 bs4 bs3) |
854 case (extra bs0 bs1 r1 bs2 r2 bs4 bs3) |
855 then show ?case |
855 then show ?case |
856 apply(subst bmkeps.simps) |
856 apply(subst bmkeps.simps) |
857 apply(subst bmkeps.simps) |
857 apply(subst bmkeps.simps) |