equal
deleted
inserted
replaced
286 apply(rule Posix.intros) |
286 apply(rule Posix.intros) |
287 prefer 2 |
287 prefer 2 |
288 apply(blast) |
288 apply(blast) |
289 prefer 2 |
289 prefer 2 |
290 apply(auto)[1] |
290 apply(auto)[1] |
291 apply (metis L_fst_simp Posix_elims(2) lex_correct3a) |
291 apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some) |
292 apply(subst Posix_simp_nullable) |
292 apply(subst Posix_simp_nullable) |
293 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
293 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
294 apply(simp) |
294 apply(simp) |
295 apply(rule Posix.intros) |
295 apply(rule Posix.intros) |
296 apply(rule Posix_mkeps) |
296 apply(rule Posix_mkeps) |
311 shows "slexer r s = lexer r s" |
311 shows "slexer r s = lexer r s" |
312 apply(induct s arbitrary: r) |
312 apply(induct s arbitrary: r) |
313 apply(simp) |
313 apply(simp) |
314 apply(simp) |
314 apply(simp) |
315 apply(auto split: option.split prod.split) |
315 apply(auto split: option.split prod.split) |
316 apply (metis L_fst_simp fst_conv lex_correct1a) |
316 apply (metis L_fst_simp fst_conv lexer_correct_None) |
317 using L_fst_simp lex_correct1a apply fastforce |
317 using L_fst_simp lexer_correct_None apply fastforce |
318 by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv) |
318 by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv) |
319 |
319 |
320 |
320 |
321 |
321 |
322 end |
322 end |