525 expect in the left-hand side of clause (7) that the value is of the form |
525 expect in the left-hand side of clause (7) that the value is of the form |
526 @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ r |
526 @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ r |
527 (STAR r)"}. Finally, the reason for why we can ignore the second argument |
527 (STAR r)"}. Finally, the reason for why we can ignore the second argument |
528 in clause (1) of @{term inj} is that it will only ever be called in cases |
528 in clause (1) of @{term inj} is that it will only ever be called in cases |
529 where @{term "c=d"}, but the usual linearity restrictions in patterns do |
529 where @{term "c=d"}, but the usual linearity restrictions in patterns do |
530 not allow is to build this constraint explicitly into our function |
530 not allow us to build this constraint explicitly into our function |
531 definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs) |
531 definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs) |
532 injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]}, |
532 injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]}, |
533 but our deviation is harmless.} |
533 but our deviation is harmless.} |
534 |
534 |
535 The idea of the @{term inj}-function to ``inject'' a character, say |
535 The idea of the @{term inj}-function to ``inject'' a character, say |
636 match rule is satisfied. |
636 match rule is satisfied. |
637 |
637 |
638 A similar condition is imposed on the POSIX value in the @{text |
638 A similar condition is imposed on the POSIX value in the @{text |
639 "P\<star>"}-rule. Also there we want that @{term "s\<^sub>1"} is the longest initial |
639 "P\<star>"}-rule. Also there we want that @{term "s\<^sub>1"} is the longest initial |
640 split of @{term "s\<^sub>1 @ s\<^sub>2"} and furthermore the corresponding value |
640 split of @{term "s\<^sub>1 @ s\<^sub>2"} and furthermore the corresponding value |
641 @{term v} cannot be flatten to the empty string. In effect, we require |
641 @{term v} cannot be flattened to the empty string. In effect, we require |
642 that in each ``iteration'' of the star, some non-empty substring need to |
642 that in each ``iteration'' of the star, some non-empty substring need to |
643 be ``chipped'' away; only in case of the empty string we accept @{term |
643 be ``chipped'' away; only in case of the empty string we accept @{term |
644 "Stars []"} as the POSIX value. |
644 "Stars []"} as the POSIX value. |
645 |
645 |
646 We can prove that given a string @{term s} and regular expression @{term |
646 We can prove that given a string @{term s} and regular expression @{term |
647 r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> |
647 r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> |
648 v"} (albeilt in an uncomputable fashion---for example rule @{term "P+R"} |
648 v"}. |
649 would require the calculation of the potentially infinite set @{term "L |
|
650 r\<^sub>1"}). |
|
651 |
649 |
652 \begin{theorem} |
650 \begin{theorem} |
653 @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]} |
651 @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]} |
654 \end{theorem} |
652 \end{theorem} |
655 |
653 |
659 PMatch1(1)} and @{thm (concl) PMatch1(2)}, which are both easily |
657 PMatch1(1)} and @{thm (concl) PMatch1(2)}, which are both easily |
660 established by inductions.\qed \end{proof} |
658 established by inductions.\qed \end{proof} |
661 |
659 |
662 \noindent |
660 \noindent |
663 Next is the lemma that shows the function @{term "mkeps"} calculates |
661 Next is the lemma that shows the function @{term "mkeps"} calculates |
664 the posix value for the empty string and a nullable regular expression. |
662 the POSIX value for the empty string and a nullable regular expression. |
665 |
663 |
666 \begin{lemma}\label{lemmkeps} |
664 \begin{lemma}\label{lemmkeps} |
667 @{thm[mode=IfThen] PMatch_mkeps} |
665 @{thm[mode=IfThen] PMatch_mkeps} |
668 \end{lemma} |
666 \end{lemma} |
669 |
667 |