equal
deleted
inserted
replaced
344 apply (metis ValOrd.intros(1)) |
344 apply (metis ValOrd.intros(1)) |
345 apply (rule ValOrd.intros(2)) |
345 apply (rule ValOrd.intros(2)) |
346 apply metis |
346 apply metis |
347 apply(simp) |
347 apply(simp) |
348 (* ALT case *) |
348 (* ALT case *) |
|
349 thm mkeps.simps |
349 apply(simp) |
350 apply(simp) |
350 apply(erule disjE) |
351 apply(erule disjE) |
351 apply(simp) |
352 apply(simp) |
352 apply (metis POSIX_ALT_I1) |
353 apply (metis POSIX_ALT_I1) |
353 (* *) |
354 (* *) |
359 apply(rule Prf.intros(3)) |
360 apply(rule Prf.intros(3)) |
360 apply(simp only: POSIX_def) |
361 apply(simp only: POSIX_def) |
361 apply(rotate_tac 4) |
362 apply(rotate_tac 4) |
362 apply(erule Prf.cases) |
363 apply(erule Prf.cases) |
363 apply(simp_all)[5] |
364 apply(simp_all)[5] |
|
365 thm mkeps_flat |
364 apply(simp add: mkeps_flat) |
366 apply(simp add: mkeps_flat) |
365 apply(auto)[1] |
367 apply(auto)[1] |
366 thm Prf_flat_L nullable_correctness |
368 thm Prf_flat_L nullable_correctness |
367 apply (metis Prf_flat_L nullable_correctness) |
369 apply (metis Prf_flat_L nullable_correctness) |
368 apply(rule ValOrd.intros) |
370 apply(rule ValOrd.intros) |
369 apply(subst (asm) POSIX_def) |
371 apply(subst (asm) POSIX_def) |
370 apply(clarify) |
372 apply(clarify) |
371 apply(drule_tac x="v2" in spec) |
373 apply(drule_tac x="v2" in spec) |
372 by metis |
374 by simp |
373 |
375 |
374 |
376 |
375 section {* Derivatives *} |
377 section {* Derivatives *} |
376 |
378 |
377 fun |
379 fun |
725 (* NULL case *) |
727 (* NULL case *) |
726 apply(simp) |
728 apply(simp) |
727 apply(erule ValOrd.cases) |
729 apply(erule ValOrd.cases) |
728 apply(simp_all)[8] |
730 apply(simp_all)[8] |
729 (* EMPTY case *) |
731 (* EMPTY case *) |
|
732 apply(simp) |
730 apply(erule ValOrd.cases) |
733 apply(erule ValOrd.cases) |
731 apply(simp_all)[8] |
734 apply(simp_all)[8] |
732 (* CHAR case *) |
735 (* CHAR case *) |
733 apply(case_tac "c = c'") |
736 apply(case_tac "c = c'") |
734 apply(simp) |
737 apply(simp) |