equal
deleted
inserted
replaced
210 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
210 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
211 | "bder c (ASEQs bs []) = AZERO" |
211 | "bder c (ASEQs bs []) = AZERO" |
212 | "bder c (ASEQs bs [r1]) = fuse bs (bder c r1)" |
212 | "bder c (ASEQs bs [r1]) = fuse bs (bder c r1)" |
213 | "bder c (ASEQs bs (r1#rs)) = |
213 | "bder c (ASEQs bs (r1#rs)) = |
214 (if bnullable r1 |
214 (if bnullable r1 |
215 then AALT bs (ASEQs [] ((bder c r1) # rs)) (fuse (bmkeps r1) (bder c (ASEQs [] rs))) |
215 then AALT bs (ASEQs [] ((bder c r1) # rs)) (bder c (ASEQs (bmkeps r1) rs)) |
216 else ASEQs bs ((bder c r1) # rs))" |
216 else ASEQs bs ((bder c r1) # rs))" |
217 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
217 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
218 |
218 |
219 |
219 |
220 fun |
220 fun |
260 apply(induct r rule: erase.induct) |
260 apply(induct r rule: erase.induct) |
261 apply(simp_all add: erase_fuse bnullable_correctness) |
261 apply(simp_all add: erase_fuse bnullable_correctness) |
262 apply(case_tac va) |
262 apply(case_tac va) |
263 apply(simp_all add: erase_fuse bnullable_correctness) |
263 apply(simp_all add: erase_fuse bnullable_correctness) |
264 apply(auto) |
264 apply(auto) |
265 apply(simp_all add: erase_fuse bnullable_correctness erase_ASEQs) |
265 apply(simp_all add: erase_fuse bnullable_correctness erase_ASEQs) |
266 done |
266 by (metis erase_ASEQs) |
267 |
267 |
268 lemma erase_bders [simp]: |
268 lemma erase_bders [simp]: |
269 shows "erase (bders r s) = ders s (erase r)" |
269 shows "erase (bders r s) = ders s (erase r)" |
270 apply(induct s arbitrary: r ) |
270 apply(induct s arbitrary: r ) |
271 apply(simp_all) |
271 apply(simp_all) |
272 done |
272 done |
273 |
273 |
274 lemma bnullable_fuse: |
274 lemma bnullable_fuse: |
275 shows "bnullable (fuse bs r) = bnullable r" |
275 shows "bnullable (fuse bs r) = bnullable r" |
276 apply(induct r arbitrary: bs) |
276 apply(induct r arbitrary: bs) |