equal
deleted
inserted
replaced
288 by meson |
288 by meson |
289 |
289 |
290 lemma flex_append: |
290 lemma flex_append: |
291 shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2" |
291 shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2" |
292 apply(induct s1 arbitrary: s2 r f) |
292 apply(induct s1 arbitrary: s2 r f) |
293 apply(simp) |
293 apply(simp_all) |
294 apply(drule_tac x="s2" in meta_spec) |
|
295 apply(drule_tac x="der a r" in meta_spec) |
|
296 apply(simp) |
|
297 done |
294 done |
298 |
295 |
299 lemma lexer_flex: |
296 lemma lexer_flex: |
300 shows "lexer r s = (if nullable (ders s r) |
297 shows "lexer r s = (if nullable (ders s r) |
301 then Some(flex r id s (mkeps (ders s r))) else None)" |
298 then Some(flex r id s (mkeps (ders s r))) else None)" |
302 apply(induct s arbitrary: r) |
299 apply(induct s arbitrary: r) |
303 apply(simp) |
300 apply(simp_all add: flex_fun_apply) |
304 apply(simp add: flex_fun_apply) |
|
305 done |
301 done |
306 |
302 |
307 unused_thms |
303 unused_thms |
308 |
304 |
309 end |
305 end |