646 |
646 |
647 \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and |
647 \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and |
648 a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the |
648 a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the |
649 auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl) |
649 auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl) |
650 Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily |
650 Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily |
651 established by inductions.\qed \end{proof} |
651 established by inductions.\qed |
652 |
652 \end{proof} |
653 |
653 |
|
654 \noindent |
654 We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two |
655 We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two |
655 informal POSIX rules shown in the Introduction: Consider for example the |
656 informal POSIX rules shown in the Introduction: Consider for example the |
656 rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string |
657 rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string |
657 and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"}, |
658 and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"}, |
658 is specified---it is always a @{text "Left"}-value, \emph{except} when the |
659 is specified---it is always a @{text "Left"}-value, \emph{except} when the |