3 imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar"

     3 imports 

     4    "../ReStar"

     5    "../Sulzmann" 

     6    "~~/src/HOL/Library/LaTeXsugar"

    26   val.Char ("Char _" [1000] 79) and

    29   val.Char ("Char _" [1000] 78) and

    39   length ("len _" [78] 73) and

    42   length ("len _" [73] 73) and

    53   slexer ("lexer\<^sup>+ _ _" [78,78] 77)

    56   slexer ("lexer\<^sup>+ _ _" [78,78] 77) and

    57 

    58   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and

    59   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)

   900   \newcommand{\greedy}{\succcurlyeq_{gr}}

   906 %  \newcommand{\greedy}{\succcurlyeq_{gr}}

   901   \newcommand{\posix}{>}

   907  \newcommand{\posix}{>}

   912 \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}		 

   918 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	

   913 $\infer{v_{1} \posix_{r_{1}} v'_{1}} 

   919 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]}(C2) &

   914        {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$

   920 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}(C1)\smallskip\\

   915 &

   921 

   916 $\infer{v_{2} \posix_{r_{2}} v'_{2}} 

   922 @{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}(A1) &

   917        {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$

   923 @{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}(A2)\smallskip\\

   918 \smallskip\\

   924 

   919 		

   925 @{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}(A3) &

   920 		

   926 @{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}(A4)\smallskip\\

   921 $\infer{ len |v_{2}| > len |v_{1}|} 

   927 

   922        {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$ 

   928 @{thm[mode=Rule] K1[of "v" "vs" "r"]}(K1) &

   923 &

   929 @{thm[mode=Rule] K2[of "v" "vs" "r"]}(K2)\smallskip\\

   924 $\infer{ len |v_{1}| \geq len |v_{2}|} 

   930 

   925        {Left \; v_{1} \posix_{r_{1}+r_{2}} Right \; v_{2}} (A2)$ 

   931 @{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}(K3) &

   926 \smallskip\\	

   932 @{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}(K4)

   927 

   928 $\infer{ v_{2} \posix_{r_{2}} v'_{2}} 

   929        {Right \; v_{2} \posix_{r_{1}+r_{2}} Right \; v'_{2}}(A3)$ & 

   930 

   931 $\infer{ v_{1} \posix_{r_{1}} v'_{1}} 

   932        {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ 

   933 \smallskip\\

   934 

   935  $\infer{|v :: vs| = []} {Stars\,[] \posix_{r^{\star}} Stars\,(v :: vs)}(K1)$ & 

   936  $\infer{|v :: vs| \neq []} {Stars\,(v :: vs) \posix_{r^{\star}} Stars\,[]}(K2)$

   937 \smallskip\\

   938 	

   939 $\infer{ v_{1} \posix_{r} v_{2}} 

   940        {Stars\,(v_{1} :: vs_{1}) \posix_{r^{\star}} Stars\,(v_{2} :: vs_{2})}(K3)$ & 

   941 $\infer{ Stars\,vs_{1} \posix_{r^{\star}} Stars\,vs_{2}} 

   942        {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$	

   946   \noindent

   936   \noindent The idea behind the rules (A1) and (A2), for example, is that a

   947   The idea behind the rules $(A1)$ and $(A2)$, for example, is that a $Left$-value is

   937   @{text Left}-value is bigger than a @{text Right}-value, if the underlying

   948   bigger than a $Right$-value, if the underlying string of the $Left$-value is

   938   string of the @{text Left}-value is longer or of equal length to the

   949   longer or of equal length to the underlying string of the $Right$-value. The order

   939   underlying string of the @{text Right}-value. The order is reversed,

   950   is reversed, however, if the $Right$-value can match longer string than a $Left$-value.

   940   however, if the @{text Right}-value can match a longer string than a

   951   In this way the POSIX value is supposed to be the biggest value

   941   @{text Left}-value. In this way the POSIX value is supposed to be the

   952   for a given string and regular expression.

   942   biggest value for a given string and regular expression.

   956   proof. Frisch and Cardelli introduced a

   946   proof. Frisch and Cardelli introduced a similar ordering for GREEDY

   957   similar ordering for GREEDY matching and they show that their GREEDY

   947   matching and they showed that their GREEDY matching algorithm always

   958   matching algorithm always produces a maximal element according to this

   948   produces a maximal element according to this ordering (from all possible

   959   ordering (from all possible solutions). The only difference between their

   949   solutions). The only difference between their GREEDY ordering and the

   960   GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if

   950   ``ordering'' by Sulzmann and Lu is that GREEDY always prefers a @{text

   961   possible, always prefers a $Left$-value over a $Right$-value, no matter

   951   Left}-value over a @{text Right}-value, no matter what the underlying

   962   what the underlying string is. This seems to be only a very minor

   952   string is. This seems to be only a very minor difference, but it has

   963   difference, but it has drastic consequences in terms of what

   953   drastic consequences in terms of what properties both orderings enjoy.

   964   properties both orderings enjoy. What is interesting for our purposes is

   954   What is interesting for our purposes is that the properties reflexivity,

   965   that the properties reflexivity, totality and transitivity for this GREEDY

   955   totality and transitivity for this GREEDY ordering can be proved

   966   ordering can be proved relatively easily by induction.

   956   relatively easily by induction.

   969   ``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v'$ is not

   959   ``ordering'' by Sulzmann and Lu. To start with, @{text "v\<^sub>1 \<ge>r v\<^sub>2"} is

   970   defined inductively, but as $v = v'$ or $v >_r v' \wedge |v| = |v'|$. This

   960   not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r

   971   means that $v >_r v'$ does not imply $v \geq_r v'$. Moreover, transitivity

   961   v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1

   972   does not hold in the ``usual'' formulation, for example:

   962   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)

   973 

   963   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''

   974 \begin{proposition}

   964   formulation, for example:

   975 Suppose $v_1 : r$, $v_2 : r$ and $v_3 : r$.

   965 

   976 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$

   966   \begin{proposition}

   977 then $v_1 \posix_r v_3$.

   967   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.

   978 \end{proposition}

   968   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}

   979 

   969   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.

   980 \noindent If formulated in this way, then there are various counter examples:

   970   \end{proposition}

   981 For example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,

   971 

   982 $v_2$ and $v_3$ below are values of $r$:

   972   \noindent If formulated in this way, then there are various counter

   973   examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}

   974   then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values

   975   of @{term r}:

   976 

   977   \begin{center}

   978   \begin{tabular}{lcl}

   979   @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\

   980   @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\

   981   @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"}

   982   \end{tabular}

   983   \end{center}

   984 

   985   \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp)

   986   v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that

   987   although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer

   988   string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and

   989   @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this

   990   formulation does not hold---in this example actually @{term "v\<^sub>3

   991   >(r::rexp) v\<^sub>1"}!

   992 

   993   Sulzmann and Lu ``fix'' this problem by weakening the transitivity

   994   property. They require in addition that the underlying strings are of the

   995   same length. This excludes the counter example above and any

   996   counter-example we were able to find (by hand and by machine). Thus the

   997   transitivity lemma should be formulated as:

   998 

   999   \begin{proposition}

  1000   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},

  1001   and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\

  1002   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}

  1003   then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.

  1004   \end{proposition}

  1005 

  1006   \noindent While we agree with Sulzmann and Lu that this property

  1007   probably(!) holds, proving it seems not so straightforward: although one

  1008   begins with the assumption that the values have the same flattening, this

  1009   cannot be maintained as one descends into the induction. This is a problem

  1010   that occurs in a number of places in the proofs by Sulzmann and Lu.

  1011 

  1012   Although they do not give an explicit proof of the transitivity property,

  1013   they give a closely related property about the existence of maximal

  1014   elements. They state that this can be verified by an induction on $r$. We

  1015   disagree with this as we shall show next in case of transitivity. The case

  1016   where the reasoning breaks down is the sequence case, say @{term "SEQ r\<^sub>1 r\<^sub>2"}.

  1017   The induction hypotheses in this case are

   985 \begin{tabular}{lcl}

  1020 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}

   986  $v_1$ & $=$ & $Left(Char\;a)$\\

  1021 \begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}

   987  $v_2$ & $=$ & $Right((Left(Char\;a), Right()))$\\

  1022 IH @{term "r\<^sub>1"}:\\

   988  $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$

  1023 @{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\

   989 \end{tabular}

  1024   & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}

   990 \end{center}

  1025     @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}

   991 

  1026     @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\

   992 \noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,

  1027   & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\

   993 but \emph{not} $v_1 \posix_r v_3$! The reason is that although

  1028   & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\

   994 $v_3$ is a $Right$-value, it can match a longer string, namely

  1029   & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"}

   995 $|v_3| = [a,a]$, while $|v_1|$ (and $|v_2|$) matches only $[a]$. So

   996 transitivity in this formulation does not hold---in this

   997 example actually $v_3 \posix_r v_1$!

   998 

   999 Sulzmann and Lu ``fix'' this problem by weakening the

  1000 transitivity property. They require in addition that the

  1001 underlying strings are of the same length. This excludes the

  1002 counter example above and any counter-example we were able 

  1003 to find (by hand and by machine). Thus the transitivity 

  1004 lemma should be formulated as:

  1005 

  1006 \begin{proposition}

  1007 Suppose $v_1 : r$, $v_2 : r$ and 

  1008 $v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\

  1009 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$

  1010 then $v_1 \posix_r v_3$.

  1011 \end{proposition}

  1012 

  1013 \noindent While we agree with Sulzmann and Lu that this property probably(!)

  1014 holds, proving it seems not so straightforward: although one begins with the

  1015 assumption that the values have the same flattening, this

  1016 cannot be maintained as one descends into the induction. This is 

  1017 a problem that occurs in a number of places in the proofs by Sulzmann and Lu.

  1018 

  1019 Although they do not give an explicit proof

  1020 of the transitivity property, they give a closely related

  1021 property about the existence of maximal elements. They state

  1022 that this can be verified by an induction on $r$. We disagree

  1023 with this as we shall show next in case of transitivity.

  1024 The case where the reasoning breaks down is the sequence case,

  1025 say $r_1\cdot r_2$. The induction hypotheses in this case

  1026 are

  1027 

  1028 \begin{center}

  1029 \begin{tabular}{@ {}cc@ {}}

  1030 \begin{tabular}{@ {}ll@ {}}

  1031 IH $r_1$:\\

  1032 $\forall v_1, v_2, v_3.$ 

  1033   & $v_1 : r_1\;\wedge$

  1034     $v_2 : r_1\;\wedge$

  1035     $v_3 : r_1\;\wedge$\\

  1036   & $|v_1|=|v_2|=|v_3|\;\wedge$\\

  1037   & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\

  1038   & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$

  1040 \begin{tabular}{@ {}ll@ {}}

  1031 \begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}

  1041 IH $r_2$:\\

  1032 IH @{term "r\<^sub>2"}:\\

  1042 $\forall v_1, v_2, v_3.$ 

  1033 @{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ 

  1043   & $v_1 : r_2\;\wedge$

  1034   & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}

  1044     $v_2 : r_2\;\wedge$

  1035     @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}

  1045     $v_3 : r_2\;\wedge$\\

  1036     @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\

  1046   & $|v_1|=|v_2|=|v_3|\;\wedge$\\

  1037   & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\

  1047   & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\

  1038   & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\

  1048   & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$

  1039   & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"}

  1053 \noindent

  1044   \noindent We can assume that

  1054 We can assume that 

  1045   %

  1055 

  1046   \begin{equation}

  1056 \begin{equation}

  1047   @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}

  1057 Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\,v_{2l}\, v_{2r}

  1048   \qquad\textrm{and}\qquad

  1058 \qquad\textrm{and}\qquad

  1049   @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}

  1059 Seq\,v_{2l}\, v_{2r} \posix_{r_1\cdot r_2} Seq\,v_{3l}\, v_{3r}

  1050   \label{assms}

  1060 \label{assms}

  1051   \end{equation}

  1061 \end{equation}

  1052 

  1062 

  1053   \noindent hold, and furthermore that the values have equal length, namely:

  1063 \noindent

  1054   %

  1064 hold, and furthermore that the values have equal length, 

  1055   \begin{equation}

  1065 namely:

  1056   @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}

  1066 

  1057   \qquad\textrm{and}\qquad

  1067 \begin{equation}

  1058   @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}

  1068 |Seq\,v_{1l}\, v_{1r}| = |Seq\,v_{2l}\, v_{2r}|

  1059   \label{lens}

  1069 \qquad\textrm{and}\qquad

  1060   \end{equation} 

  1070 |Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}|

  1061 

  1071 \label{lens}

  1062   \noindent We need to show that @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2)

  1072 \end{equation}

  1063   (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} holds. We can proceed by analysing how the

  1073 

  1064   assumptions in \eqref{assms} have arisen. There are four cases. Let us

  1074 \noindent We need to show that $Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2}

  1065   assume we are in the case where we know

  1075 Seq\, v_{3l}\, v_{3r}$ holds. We can proceed by analysing how the

  1066 

  1076 assumptions in \eqref{assms} have arisen. There are four cases. Let us

  1067   \[

  1077 assume we are in the case where we know

  1068   @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"}

  1078 

  1069   \qquad\textrm{and}\qquad

  1079 \[

  1070   @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"}

  1080 v_{1l} \posix_{r_1} v_{2l}

  1071   \]

  1081 \qquad\textrm{and}\qquad

  1072 

  1082 v_{2l} \posix_{r_1} v_{3l}

  1073   \noindent and also know the corresponding inhabitation judgements. This is

  1083 \]

  1074   exactly a case where we would like to apply the induction hypothesis

  1084 

  1075   IH~$r_1$. But we cannot! We still need to show that @{term "flat (v\<^sub>1\<^sub>l) =

  1085 \noindent and also know the corresponding inhabitation judgements.

  1076   flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. We know from

  1086 This is exactly a case where we would like to apply the

  1077   \eqref{lens} that the lengths of the sequence values are equal, but from

  1087 induction hypothesis IH~$r_1$. But we cannot! We still need to

  1078   this we cannot infer anything about the lengths of the component values.

  1088 show that $|v_{1l}| = |v_{2l}|$ and $|v_{2l}| = |v_{3l}|$. We

  1079   Indeed in general they will be unequal, that is

  1089 know from \eqref{lens} that the lengths of the sequence values

  1080 

  1090 are equal, but from this we cannot infer anything about the

  1081   \[

  1091 lengths of the component values. Indeed in general they will

  1082   @{term "flat(v\<^sub>1\<^sub>l) \<noteq> flat(v\<^sub>2\<^sub>l)"}  

  1092 be unequal, that is 

  1083   \qquad\textrm{and}\qquad

  1093 

  1084   @{term "flat(v\<^sub>1\<^sub>r) \<noteq> flat(v\<^sub>2\<^sub>r)"}

  1094 \[

  1085   \]

  1095 |v_{1l}| \not= |v_{2l}|  

  1086 

  1096 \qquad\textrm{and}\qquad

  1087   \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH

  1097 |v_{1r}| \not= |v_{2r}|

  1088   does not apply. As said, this problem where the induction hypothesis does

  1098 \]

  1089   not apply arises in several places in the proof of Sulzmann and Lu, not

  1099 

  1090   just for proving transitivity.

  1100 \noindent but still \eqref{lens} will hold. Now we are stuck,

  1101 since the IH does not apply. As said, this problem where the

  1102 induction hypothesis does not apply arises in several places in

  1103 the proof of Sulzmann and Lu, not just for proving transitivity.