equal
deleted
inserted
replaced
668 "s \<notin> L (der c r\<^sub>1)"} and @{term "s \<in> der c r\<^sub>2 \<rightarrow> v'"}. In @{text "(a)"} we |
668 "s \<notin> L (der c r\<^sub>1)"} and @{term "s \<in> der c r\<^sub>2 \<rightarrow> v'"}. In @{text "(a)"} we |
669 know @{term "s \<in> der c r\<^sub>1 \<rightarrow> v'"}, from which we can infer @{term "(c # s) |
669 know @{term "s \<in> der c r\<^sub>1 \<rightarrow> v'"}, from which we can infer @{term "(c # s) |
670 \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v'"} by induction hypothesis and hence @{term "(c # |
670 \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v'"} by induction hypothesis and hence @{term "(c # |
671 s) \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> injval (ALT r\<^sub>1 r\<^sub>2) c (Left v')"} as needed. Similarly |
671 s) \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> injval (ALT r\<^sub>1 r\<^sub>2) c (Left v')"} as needed. Similarly |
672 in subcase @{text "(b)"} where, however, in addition we have to use |
672 in subcase @{text "(b)"} where, however, in addition we have to use |
673 Prop~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term |
673 Prop.~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term |
674 "s \<notin> L (der c r\<^sub>1)"}. |
674 "s \<notin> L (der c r\<^sub>1)"}. |
675 |
675 |
676 Suppose @{term "r = SEQ r\<^sub>1 r\<^sub>2"}. There are three subcases: |
676 Suppose @{term "r = SEQ r\<^sub>1 r\<^sub>2"}. There are three subcases: |
677 |
677 |
678 \begin{quote} |
678 \begin{quote} |
686 \noindent For @{text "(a)"} we know @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} and |
686 \noindent For @{text "(a)"} we know @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} and |
687 @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} as well as |
687 @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} as well as |
688 |
688 |
689 \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\] |
689 \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\] |
690 |
690 |
691 \noindent From the latter we can infer by Prop~\ref{derprop}(2): |
691 \noindent From the latter we can infer by Prop.~\ref{derprop}(2): |
692 |
692 |
693 \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\] |
693 \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\] |
694 |
694 |
695 \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain |
695 \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain |
696 @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. This allows us to infer |
696 @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. This allows us to infer |
733 \end{proof} |
733 \end{proof} |
734 |
734 |
735 This concludes our correctness proof. Note that we have not changed the |
735 This concludes our correctness proof. Note that we have not changed the |
736 algorithm by Sulzmann and Lu, but introduced our own specification for |
736 algorithm by Sulzmann and Lu, but introduced our own specification for |
737 what a correct result---a POSIX value---should be. |
737 what a correct result---a POSIX value---should be. |
|
738 *} |
|
739 |
|
740 section {* Extensions *} |
|
741 |
|
742 text {* |
|
743 |
|
744 Derivatives as calculated by \Brz's method are usually more complex |
|
745 regular expressions than the initial one; the result is that the matching |
|
746 and lexing algorithms are often absymally slow. |
|
747 |
|
748 |
|
749 various optimisations are |
|
750 possible, such as the simplifications of @{term "ALT ZERO r"}, @{term "ALT |
|
751 r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to @{term r}. One of |
|
752 the advantages of having a simple specification and correctness proof is |
|
753 that the latter can be refined to allow for such optimisations and simple |
|
754 correctness proof. |
|
755 |
|
756 |
738 *} |
757 *} |
739 |
758 |
740 section {* The Argument by Sulzmmann and Lu *} |
759 section {* The Argument by Sulzmmann and Lu *} |
741 |
760 |
742 section {* Conclusion *} |
761 section {* Conclusion *} |