equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports |
3 imports |
4 "../ReStar" |
4 "../Lexer" |
5 "../Simplifying" |
5 "../Simplifying" |
6 "../Sulzmann" |
6 "../Sulzmann" |
7 "~~/src/HOL/Library/LaTeXsugar" |
7 "~~/src/HOL/Library/LaTeXsugar" |
8 begin |
8 begin |
9 |
9 |
65 (* |
65 (* |
66 comments not implemented |
66 comments not implemented |
67 |
67 |
68 p9. The condtion "not exists s3 s4..." appears often enough (in particular in |
68 p9. The condtion "not exists s3 s4..." appears often enough (in particular in |
69 the proof of Lemma 3) to warrant a definition. |
69 the proof of Lemma 3) to warrant a definition. |
70 |
|
71 p10. (proof Lemma 3) : separating the cases with description/itemize would greatly |
|
72 improve readability |
|
73 |
|
74 p11. Theorem 2(2) : Stressing the uniqueness is strange, given that it follows |
|
75 trivially from the fact that "lexer" is a function. Maybe state the existence of |
|
76 a unique POSIX value as corollary. |
|
77 |
70 |
78 *) |
71 *) |
79 |
72 |
80 (*>*) |
73 (*>*) |
81 |
74 |
651 |
644 |
652 \noindent |
645 \noindent |
653 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 |
654 r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}. |
647 r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}. |
655 |
648 |
656 \begin{theorem}\label{posixdeterm} |
649 \begin{theorem}\mbox{}\smallskip\\\label{posixdeterm} |
657 @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]} |
650 \begin{tabular}{ll} |
|
651 @{text "(1)"} & If @{thm (prem 1) Posix1(1)} then @{thm (concl) |
|
652 Posix1(1)} and @{thm (concl) Posix1(2)}.\\ |
|
653 @{text "(2)"} & @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v" "v'"]} |
|
654 \end{tabular} |
658 \end{theorem} |
655 \end{theorem} |
659 |
656 |
660 \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and |
657 \begin{proof} Both by induction on the definition of @{term "s \<in> r \<rightarrow> v"}. |
661 a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the |
658 The second parts follows by a case analysis of @{term "s \<in> r \<rightarrow> v'"} and |
662 auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl) |
659 the first part.\qed |
663 Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily |
|
664 established by inductions.\qed |
|
665 \end{proof} |
660 \end{proof} |
666 |
661 |
667 \noindent |
662 \noindent |
668 We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two |
663 We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two |
669 informal POSIX rules shown in the Introduction: Consider for example the |
664 informal POSIX rules shown in the Introduction: Consider for example the |
791 \begin{proof} |
786 \begin{proof} |
792 By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed |
787 By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed |
793 \end{proof} |
788 \end{proof} |
794 |
789 |
795 \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the |
790 \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the |
796 value returned by the lexer must be unique. This concludes our |
791 value returned by the lexer must be unique. A simple corollary |
|
792 of our two theorems yis: |
|
793 |
|
794 \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect} |
|
795 \begin{tabular}{ll} |
|
796 (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ |
|
797 (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\ |
|
798 \end{tabular} |
|
799 \end{corollary} |
|
800 |
|
801 \noindent |
|
802 This concludes our |
797 correctness proof. Note that we have not changed the algorithm of |
803 correctness proof. Note that we have not changed the algorithm of |
798 Sulzmann and Lu,\footnote{All deviations we introduced are |
804 Sulzmann and Lu,\footnote{All deviations we introduced are |
799 harmless.} but introduced our own specification for what a correct |
805 harmless.} but introduced our own specification for what a correct |
800 result---a POSIX value---should be. A strong point in favour of |
806 result---a POSIX value---should be. A strong point in favour of |
801 Sulzmann and Lu's algorithm is that it can be extended in various |
807 Sulzmann and Lu's algorithm is that it can be extended in various |
1058 relatively easily by induction. |
1064 relatively easily by induction. |
1059 |
1065 |
1060 These properties of GREEDY, however, do not transfer to the POSIX |
1066 These properties of GREEDY, however, do not transfer to the POSIX |
1061 ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. |
1067 ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. |
1062 To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is |
1068 To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is |
1063 not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r |
1069 not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r |
1064 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1 |
1070 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1 |
1065 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1071 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1066 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1072 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1067 formulation, for example: |
1073 formulation, for example: |
1068 |
1074 |
1069 \begin{falsehood} |
1075 \begin{falsehood} |