equal
deleted
inserted
replaced
310 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
310 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
311 unfolding bds_def ds_def . |
311 unfolding bds_def ds_def . |
312 } |
312 } |
313 then show "blexer r s = lexer r s" |
313 then show "blexer r s = lexer r s" |
314 unfolding blexer_def lexer_flex |
314 unfolding blexer_def lexer_flex |
315 by(auto simp add: bnullable_correctness[symmetric]) |
315 apply(subst bnullable_correctness[symmetric]) |
|
316 apply(simp) |
|
317 done |
316 qed |
318 qed |
|
319 |
|
320 fun simp where |
|
321 "simp (AALT bs a AZERO) = fuse bs (simp a)" |
|
322 | "simp (AALT bs AZERO a) = fuse bs (simp a)" |
|
323 | "simp (ASEQ bs a AZERO) = AZERO" |
|
324 | "simp (ASEQ bs AZERO a) = AZERO" |
|
325 | "simp a = a" |
|
326 |
317 |
327 |
318 unused_thms |
328 unused_thms |
319 |
329 |
320 end |
330 end |