462 inj} function is by recursion on the regular expression and by analysing |
462 inj} function is by recursion on the regular expression and by analysing |
463 the shape of values. |
463 the shape of values. |
464 |
464 |
465 \begin{center} |
465 \begin{center} |
466 \begin{tabular}{lcl} |
466 \begin{tabular}{lcl} |
467 @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
467 @{thm (lhs) injval.simps(1)[of "d" "DUMMY"]} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
468 @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
468 @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
469 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
469 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
470 @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
470 @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
471 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
471 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
472 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
472 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
480 \end{tabular} |
480 \end{tabular} |
481 \end{center} |
481 \end{center} |
482 |
482 |
483 \noindent To better understand what is going on in this definition it |
483 \noindent To better understand what is going on in this definition it |
484 might be instructive to look first at the three sequence cases (clauses |
484 might be instructive to look first at the three sequence cases (clauses |
485 4--6). Recall the corresponding clause of the derivative |
485 4--6). In each case we need to construct an ``injected value'' for @{term |
|
486 "SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function |
|
487 for sequence regular expressions: |
486 |
488 |
487 \begin{center} |
489 \begin{center} |
488 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} |
490 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} |
489 \end{center} |
491 \end{center} |
490 |
492 |
491 \noindent |
493 \noindent Consider first the else-branch where the derivative is @{term |
|
494 "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore |
|
495 be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the fourth |
|
496 clause of @{term inj}. In the if-branch the derivative is an alternative, |
|
497 namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. |
|
498 This means we either have to consider a @{text Left}- or @{text |
|
499 Right}-value. In case of the @{text Left}-value we know further it must be |
|
500 a value for a sequence regular expression. Therefore the pattern we |
|
501 match in the fifth clause is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while |
|
502 in the sixth it is just @{term "Right v\<^sub>2"}. One more interesting point |
|
503 is in the right-hand side of the sixth clause: since in this case the regular |
|
504 expression @{text "r\<^sub>1"} does not ``contribute'' in matching the string, |
|
505 that is only matches the empty string, we need to call @{const mkeps} in order |
|
506 to construct a value how @{term "r\<^sub>1"} can match this empty string. |
|
507 |
|
508 |
492 NOT DONE YET |
509 NOT DONE YET |
493 |
510 |
494 Therefore there are, for example, three |
511 Therefore there are, for example, three |
495 cases for sequence regular expressions (for all possible shapes of the |
512 cases for sequence regular expressions (for all possible shapes of the |
496 value). |
513 value). |