equal
deleted
inserted
replaced
343 apply(simp) |
343 apply(simp) |
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 apply(simp) |
349 apply(simp) |
349 apply(erule disjE) |
350 apply(erule disjE) |
350 apply(simp) |
351 apply(simp) |
351 apply (metis POSIX_ALT_I1) |
352 apply (metis POSIX_ALT_I1) |
352 apply(auto) |
353 (* *) |
|
354 apply(auto)[1] |
|
355 thm POSIX_ALT_I1 |
353 apply (metis POSIX_ALT_I1) |
356 apply (metis POSIX_ALT_I1) |
354 apply(simp add: POSIX_def) |
357 apply(simp (no_asm) add: POSIX_def) |
355 apply(auto)[1] |
358 apply(auto)[1] |
356 apply (metis Prf.intros(3)) |
359 apply(rule Prf.intros(3)) |
357 apply(rotate_tac 5) |
360 apply(simp only: POSIX_def) |
|
361 apply(rotate_tac 4) |
358 apply(erule Prf.cases) |
362 apply(erule Prf.cases) |
359 apply(simp_all)[5] |
363 apply(simp_all)[5] |
360 apply(simp add: mkeps_flat) |
364 apply(simp add: mkeps_flat) |
361 apply(auto)[1] |
365 apply(auto)[1] |
|
366 thm Prf_flat_L nullable_correctness |
362 apply (metis Prf_flat_L nullable_correctness) |
367 apply (metis Prf_flat_L nullable_correctness) |
363 apply(rule ValOrd.intros) |
368 apply(rule ValOrd.intros) |
|
369 apply(subst (asm) POSIX_def) |
|
370 apply(clarify) |
|
371 apply(drule_tac x="v2" in spec) |
364 by metis |
372 by metis |
365 |
373 |
366 |
374 |
367 section {* Derivatives *} |
375 section {* Derivatives *} |
368 |
376 |
399 section {* Projection function *} |
407 section {* Projection function *} |
400 |
408 |
401 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
409 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
402 where |
410 where |
403 "projval (CHAR d) c _ = Void" |
411 "projval (CHAR d) c _ = Void" |
404 | "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)" |
412 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)" |
405 | "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)" |
413 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)" |
406 | "projval (SEQ r1 r2) c (Seq v1 v2) = |
414 | "projval (SEQ r1 r2) c (Seq v1 v2) = |
407 (if flat v1 = [] then Right(projval r2 c v2) |
415 (if flat v1 = [] then Right(projval r2 c v2) |
408 else if nullable r1 then Left (Seq (projval r1 c v1) v2) |
416 else if nullable r1 then Left (Seq (projval r1 c v1) v2) |
409 else Seq (projval r1 c v1) v2)" |
417 else Seq (projval r1 c v1) v2)" |
410 |
418 |