877 @{thm (lhs) F_ALT.simps(2)} & $\dn$ & @{text "Left (f\<^sub>1 v)"}\\ |
877 @{thm (lhs) F_ALT.simps(2)} & $\dn$ & @{text "Left (f\<^sub>1 v)"}\\ |
878 |
878 |
879 @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\ |
879 @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\ |
880 @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\ |
880 @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\ |
881 @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\ |
881 @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\ |
882 \end{tabular} |
882 %\end{tabular} |
883 |
883 % |
884 \begin{tabular}{lcl} |
884 %\begin{tabular}{lcl} |
885 @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\ |
885 @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\ |
886 @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\ |
886 @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\ |
887 @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"}\\ |
887 @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"}\\ |
888 @{term "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"}\\ |
888 @{term "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"}\\ |
889 @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"}\\ |
889 @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"}\\ |
902 @{term "simp (SEQ r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_SEQ (simp r\<^sub>1) (simp r\<^sub>2)"}\\ |
902 @{term "simp (SEQ r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_SEQ (simp r\<^sub>1) (simp r\<^sub>2)"}\\ |
903 @{term "simp r"} & $\dn$ & @{term "(r, id)"}\\ |
903 @{term "simp r"} & $\dn$ & @{term "(r, id)"}\\ |
904 \end{tabular} |
904 \end{tabular} |
905 \end{center} |
905 \end{center} |
906 |
906 |
907 \noindent where @{term "id"} stands for the identity function. This |
907 \noindent where @{term "id"} stands for the identity function. The |
908 function returns a simplified regular expression and a corresponding |
908 function @{const simp} returns a simplified regular expression and a corresponding |
909 rectification function. Note that we do not simplify under stars: this |
909 rectification function. Note that we do not simplify under stars: this |
910 seems to slow down the algorithm, rather than speed up. The optimised |
910 seems to slow down the algorithm, rather than speed it up. The optimised |
911 lexer is then given by the clauses: |
911 lexer is then given by the clauses: |
912 |
912 |
913 \begin{center} |
913 \begin{center} |
914 \begin{tabular}{lcl} |
914 \begin{tabular}{lcl} |
915 @{thm (lhs) slexer.simps(1)} & $\dn$ & @{thm (rhs) slexer.simps(1)}\\ |
915 @{thm (lhs) slexer.simps(1)} & $\dn$ & @{thm (rhs) slexer.simps(1)}\\ |
943 interesting case for the first statement. For the second statement, |
943 interesting case for the first statement. For the second statement, |
944 of interest are the @{term "r = ALT r\<^sub>1 r\<^sub>2"} and @{term "r = SEQ r\<^sub>1 |
944 of interest are the @{term "r = ALT r\<^sub>1 r\<^sub>2"} and @{term "r = SEQ r\<^sub>1 |
945 r\<^sub>2"} cases. In each case we have to analyse four subcases whether |
945 r\<^sub>2"} cases. In each case we have to analyse four subcases whether |
946 @{term "fst (simp r\<^sub>1)"} and @{term "fst (simp r\<^sub>2)"} equals @{const |
946 @{term "fst (simp r\<^sub>1)"} and @{term "fst (simp r\<^sub>2)"} equals @{const |
947 ZERO} (respectively @{const ONE}). For example for @{term "r = ALT |
947 ZERO} (respectively @{const ONE}). For example for @{term "r = ALT |
948 r\<^sub>1 r\<^sub>2"}, considder the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and |
948 r\<^sub>1 r\<^sub>2"}, consider the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and |
949 @{term "fst (simp r\<^sub>2) \<noteq> ZERO"}. By assumption we know @{term "s \<in> |
949 @{term "fst (simp r\<^sub>2) \<noteq> ZERO"}. By assumption we know @{term "s \<in> |
950 fst (simp (ALT r\<^sub>1 r\<^sub>2)) \<rightarrow> v"}. From this we can infer @{term "s \<in> fst (simp r\<^sub>2) \<rightarrow> v"} |
950 fst (simp (ALT r\<^sub>1 r\<^sub>2)) \<rightarrow> v"}. From this we can infer @{term "s \<in> fst (simp r\<^sub>2) \<rightarrow> v"} |
951 and by IH also (*) @{term "s \<in> r\<^sub>2 \<rightarrow> (snd (simp r\<^sub>2) v)"}. Given @{term "fst (simp r\<^sub>1) = ZERO"} |
951 and by IH also (*) @{term "s \<in> r\<^sub>2 \<rightarrow> (snd (simp r\<^sub>2) v)"}. Given @{term "fst (simp r\<^sub>1) = ZERO"} |
952 we know @{term "L (fst (simp r\<^sub>1)) = {}"}. By the first statement |
952 we know @{term "L (fst (simp r\<^sub>1)) = {}"}. By the first statement |
953 @{term "L r\<^sub>1"} is the empty set, meaning (**) @{term "s \<notin> L r\<^sub>1"}. |
953 @{term "L r\<^sub>1"} is the empty set, meaning (**) @{term "s \<notin> L r\<^sub>1"}. |
1050 What is interesting for our purposes is that the properties reflexivity, |
1050 What is interesting for our purposes is that the properties reflexivity, |
1051 totality and transitivity for this GREEDY ordering can be proved |
1051 totality and transitivity for this GREEDY ordering can be proved |
1052 relatively easily by induction. |
1052 relatively easily by induction. |
1053 |
1053 |
1054 These properties of GREEDY, however, do not transfer to the POSIX |
1054 These properties of GREEDY, however, do not transfer to the POSIX |
1055 ``ordering'' by Sulzmann and Lu. To start with, @{text "v\<^sub>1 \<ge>r v\<^sub>2"} is |
1055 ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. |
|
1056 To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is |
1056 not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r |
1057 not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r |
1057 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1 |
1058 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1 |
1058 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1059 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1059 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1060 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1060 formulation, for example: |
1061 formulation, for example: |