1 (*<*)

     2 theory Paper

     3 imports 

     4    "../Lexer"

     5    "../Simplifying" 

     6    "../Positions"

     7 

     8    "../SizeBound" 

     9    "HOL-Library.LaTeXsugar"

    10 begin

    11 

    12 lemma Suc_0_fold:

    13   "Suc 0 = 1"

    14 by simp

    15 

    16 

    17 

    18 declare [[show_question_marks = false]]

    19 

    20 syntax (latex output)

    21   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^latex>\<open>\\mbox{\\boldmath$\\mid$}\<close> _})")

    22   "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ |e _})")

    23 

    24 syntax

    25   "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_.a./ _)" [0, 10] 10)

    26   "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_.a./ _)" [0, 10] 10)

    27 

    28 

    29 abbreviation 

    30   "der_syn r c \<equiv> der c r"

    31 

    32 abbreviation 

    33   "ders_syn r s \<equiv> ders s r"

    34 

    35   abbreviation 

    36   "bder_syn r c \<equiv> bder c r"

    37 

    38 abbreviation 

    39   "bders_syn r s \<equiv> bders r s"

    40 

    41 

    42 abbreviation

    43   "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"

    44 

    45 

    46 

    47 

    48 notation (latex output)

    49   If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and

    50   Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and  

    51 

    52   ZERO ("\<^bold>0" 81) and 

    53   ONE ("\<^bold>1" 81) and 

    54   CH ("_" [1000] 80) and

    55   ALT ("_ + _" [77,77] 78) and

    56   SEQ ("_ \<cdot> _" [77,77] 78) and

    57   STAR ("_\<^sup>\<star>" [79] 78) and

    58   

    59   val.Void ("Empty" 78) and

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

    61   val.Left ("Left _" [79] 78) and

    62   val.Right ("Right _" [1000] 78) and

    63   val.Seq ("Seq _ _" [79,79] 78) and

    64   val.Stars ("Stars _" [79] 78) and

    65 

    66   L ("L'(_')" [10] 78) and

    67   LV ("LV _ _" [80,73] 78) and

    68   der_syn ("_\\_" [79, 1000] 76) and  

    69   ders_syn ("_\\_" [79, 1000] 76) and

    70   flat ("|_|" [75] 74) and

    71   flats ("|_|" [72] 74) and

    72   Sequ ("_ @ _" [78,77] 63) and

    73   injval ("inj _ _ _" [79,77,79] 76) and 

    74   mkeps ("mkeps _" [79] 76) and 

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

    76   intlen ("len _" [73] 73) and

    77   set ("_" [73] 73) and

    78  

    79   Prf ("_ : _" [75,75] 75) and

    80   Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and

    81  

    82   lexer ("lexer _ _" [78,78] 77) and 

    83   F_RIGHT ("F\<^bsub>Right\<^esub> _") and

    84   F_LEFT ("F\<^bsub>Left\<^esub> _") and  

    85   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

    86   F_SEQ1 ("F\<^bsub>Seq1\<^esub> _ _") and

    87   F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and

    88   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and

    89   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and

    90   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and

    91   slexer ("lexer\<^sup>+" 1000) and

    92 

    93   at ("_\<^latex>\<open>\\mbox{$\\downharpoonleft$}\<close>\<^bsub>_\<^esub>") and

    94   lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and

    95   PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and

    96   PosOrd_ex ("_ \<prec> _" [77,77] 77) and

    97   PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and

    98   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and

    99   nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and

   100 

   101   bder_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and  

   102   bders_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and

   103   intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and

   104   erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and

   105   bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and

   106   bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and

   107   blexer ("lexer\<^latex>\<open>\\mbox{$_b$}\<close> _ _" [77, 77] 80) and

   108   code ("code _" [79] 74) and

   109 

   110   DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")

   111 

   112 

   113 definition 

   114   "match r s \<equiv> nullable (ders s r)"

   115 

   116 

   117 lemma LV_STAR_ONE_empty: 

   118   shows "LV (STAR ONE) [] = {Stars []}"

   119 by(auto simp add: LV_def elim: Prf.cases intro: Prf.intros)

   120 

   121 

   122 

   123 (*

   124 comments not implemented

   125 

   126 p9. The condition "not exists s3 s4..." appears often enough (in particular in

   127 the proof of Lemma 3) to warrant a definition.

   128 

   129 *)

   130 

   131 

   132 (*>*)

   133 

   134 

   135 

   136 section \<open>Introduction\<close>

   137 

   138 

   139 text \<open>

   140 

   141 This works builds on previous work by Ausaf and Urban using 

   142 regular expression'd bit-coded derivatives to do lexing that 

   143 is both fast and satisfied the POSIX specification.

   144 In their work, a bit-coded algorithm introduced by Sulzmann and Lu

   145 was formally verified in Isabelle, by a very clever use of

   146 flex function and retrieve to carefully mimic the way a value is 

   147 built up by the injection funciton.

   148 

   149 In the previous work, Ausaf and Urban established the below equality:

   150 \begin{lemma}

   151 @{thm [mode=IfThen] bder_retrieve}

   152 \end{lemma}

   153 

   154 This lemma links the derivative of a bit-coded regular expression with

   155 the regular expression itself before the derivative. 

   156 

   157 Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em

   158 derivative} @{term "der c r"} of a regular expression \<open>r\<close> w.r.t.\

   159 a character~\<open>c\<close>, and showed that it gave a simple solution to the

   160 problem of matching a string @{term s} with a regular expression @{term

   161 r}: if the derivative of @{term r} w.r.t.\ (in succession) all the

   162 characters of the string matches the empty string, then @{term r}

   163 matches @{term s} (and {\em vice versa}). The derivative has the

   164 property (which may almost be regarded as its specification) that, for

   165 every string @{term s} and regular expression @{term r} and character

   166 @{term c}, one has @{term "cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}. 

   167 The beauty of Brzozowski's derivatives is that

   168 they are neatly expressible in any functional language, and easily

   169 definable and reasoned about in theorem provers---the definitions just

   170 consist of inductive datatypes and simple recursive functions. A

   171 mechanised correctness proof of Brzozowski's matcher in for example HOL4

   172 has been mentioned by Owens and Slind~\cite{Owens2008}. Another one in

   173 Isabelle/HOL is part of the work by Krauss and Nipkow \cite{Krauss2011}.

   174 And another one in Coq is given by Coquand and Siles \cite{Coquand2012}.

   175 

   176 If a regular expression matches a string, then in general there is more

   177 than one way of how the string is matched. There are two commonly used

   178 disambiguation strategies to generate a unique answer: one is called

   179 GREEDY matching \cite{Frisch2004} and the other is POSIX

   180 matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}.

   181 For example consider the string @{term xy} and the regular expression

   182 \mbox{@{term "STAR (ALT (ALT x y) xy)"}}. Either the string can be

   183 matched in two `iterations' by the single letter-regular expressions

   184 @{term x} and @{term y}, or directly in one iteration by @{term xy}. The

   185 first case corresponds to GREEDY matching, which first matches with the

   186 left-most symbol and only matches the next symbol in case of a mismatch

   187 (this is greedy in the sense of preferring instant gratification to

   188 delayed repletion). The second case is POSIX matching, which prefers the

   189 longest match.

   190 

   191 In the context of lexing, where an input string needs to be split up

   192 into a sequence of tokens, POSIX is the more natural disambiguation

   193 strategy for what programmers consider basic syntactic building blocks

   194 in their programs.  These building blocks are often specified by some

   195 regular expressions, say \<open>r\<^bsub>key\<^esub>\<close> and \<open>r\<^bsub>id\<^esub>\<close> for recognising keywords and identifiers,

   196 respectively. There are a few underlying (informal) rules behind

   197 tokenising a string in a POSIX \cite{POSIX} fashion:

   198 

   199 \begin{itemize} 

   200 \item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``{M}aximal {M}unch {R}ule''}):

   201 The longest initial substring matched by any regular expression is taken as

   202 next token.\smallskip

   203 

   204 \item[$\bullet$] \emph{Priority Rule:}

   205 For a particular longest initial substring, the first (leftmost) regular expression

   206 that can match determines the token.\smallskip

   207 

   208 \item[$\bullet$] \emph{Star Rule:} A subexpression repeated by ${}^\star$ shall 

   209 not match an empty string unless this is the only match for the repetition.\smallskip

   210 

   211 \item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to 

   212 be longer than no match at all.

   213 \end{itemize}

   214 

   215 \noindent Consider for example a regular expression \<open>r\<^bsub>key\<^esub>\<close> for recognising keywords such as \<open>if\<close>,

   216 \<open>then\<close> and so on; and \<open>r\<^bsub>id\<^esub>\<close>

   217 recognising identifiers (say, a single character followed by

   218 characters or numbers).  Then we can form the regular expression

   219 \<open>(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>\<close>

   220 and use POSIX matching to tokenise strings, say \<open>iffoo\<close> and

   221 \<open>if\<close>.  For \<open>iffoo\<close> we obtain by the Longest Match Rule

   222 a single identifier token, not a keyword followed by an

   223 identifier. For \<open>if\<close> we obtain by the Priority Rule a keyword

   224 token, not an identifier token---even if \<open>r\<^bsub>id\<^esub>\<close>

   225 matches also. By the Star Rule we know \<open>(r\<^bsub>key\<^esub> +

   226 r\<^bsub>id\<^esub>)\<^sup>\<star>\<close> matches \<open>iffoo\<close>,

   227 respectively \<open>if\<close>, in exactly one `iteration' of the star. The

   228 Empty String Rule is for cases where, for example, the regular expression 

   229 \<open>(a\<^sup>\<star>)\<^sup>\<star>\<close> matches against the

   230 string \<open>bc\<close>. Then the longest initial matched substring is the

   231 empty string, which is matched by both the whole regular expression

   232 and the parenthesised subexpression.

   233 

   234 

   235 One limitation of Brzozowski's matcher is that it only generates a

   236 YES/NO answer for whether a string is being matched by a regular

   237 expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher

   238 to allow generation not just of a YES/NO answer but of an actual

   239 matching, called a [lexical] {\em value}. Assuming a regular

   240 expression matches a string, values encode the information of

   241 \emph{how} the string is matched by the regular expression---that is,

   242 which part of the string is matched by which part of the regular

   243 expression. For this consider again the string \<open>xy\<close> and

   244 the regular expression \mbox{\<open>(x + (y + xy))\<^sup>\<star>\<close>}

   245 (this time fully parenthesised). We can view this regular expression

   246 as tree and if the string \<open>xy\<close> is matched by two Star

   247 `iterations', then the \<open>x\<close> is matched by the left-most

   248 alternative in this tree and the \<open>y\<close> by the right-left alternative. This

   249 suggests to record this matching as

   250 

   251 \begin{center}

   252 @{term "Stars [Left(Char x), Right(Left(Char y))]"}

   253 \end{center}

   254 

   255 \noindent where @{const Stars}, \<open>Left\<close>, \<open>Right\<close> and \<open>Char\<close> are constructors for values. \<open>Stars\<close> records how many

   256 iterations were used; \<open>Left\<close>, respectively \<open>Right\<close>, which

   257 alternative is used. This `tree view' leads naturally to the idea that

   258 regular expressions act as types and values as inhabiting those types

   259 (see, for example, \cite{HosoyaVouillonPierce2005}).  The value for

   260 matching \<open>xy\<close> in a single `iteration', i.e.~the POSIX value,

   261 would look as follows

   262 

   263 \begin{center}

   264 @{term "Stars [Seq (Char x) (Char y)]"}

   265 \end{center}

   266 

   267 \noindent where @{const Stars} has only a single-element list for the

   268 single iteration and @{const Seq} indicates that @{term xy} is matched 

   269 by a sequence regular expression.

   270 

   271 %, which we will in what follows 

   272 %write more formally as @{term "SEQ x y"}.

   273 

   274 

   275 Sulzmann and Lu give a simple algorithm to calculate a value that

   276 appears to be the value associated with POSIX matching.  The challenge

   277 then is to specify that value, in an algorithm-independent fashion,

   278 and to show that Sulzmann and Lu's derivative-based algorithm does

   279 indeed calculate a value that is correct according to the

   280 specification.  The answer given by Sulzmann and Lu

   281 \cite{Sulzmann2014} is to define a relation (called an ``order

   282 relation'') on the set of values of @{term r}, and to show that (once

   283 a string to be matched is chosen) there is a maximum element and that

   284 it is computed by their derivative-based algorithm. This proof idea is

   285 inspired by work of Frisch and Cardelli \cite{Frisch2004} on a GREEDY

   286 regular expression matching algorithm. However, we were not able to

   287 establish transitivity and totality for the ``order relation'' by

   288 Sulzmann and Lu.  There are some inherent problems with their approach

   289 (of which some of the proofs are not published in

   290 \cite{Sulzmann2014}); perhaps more importantly, we give in this paper

   291 a simple inductive (and algorithm-independent) definition of what we

   292 call being a {\em POSIX value} for a regular expression @{term r} and

   293 a string @{term s}; we show that the algorithm by Sulzmann and Lu

   294 computes such a value and that such a value is unique. Our proofs are

   295 both done by hand and checked in Isabelle/HOL.  The experience of

   296 doing our proofs has been that this mechanical checking was absolutely

   297 essential: this subject area has hidden snares. This was also noted by

   298 Kuklewicz \cite{Kuklewicz} who found that nearly all POSIX matching

   299 implementations are ``buggy'' \cite[Page 203]{Sulzmann2014} and by

   300 Grathwohl et al \cite[Page 36]{CrashCourse2014} who wrote:

   301 

   302 \begin{quote}

   303 \it{}``The POSIX strategy is more complicated than the greedy because of 

   304 the dependence on information about the length of matched strings in the 

   305 various subexpressions.''

   306 \end{quote}

   307 

   308 

   309 

   310 \noindent {\bf Contributions:} We have implemented in Isabelle/HOL the

   311 derivative-based regular expression matching algorithm of

   312 Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this

   313 algorithm according to our specification of what a POSIX value is (inspired

   314 by work of Vansummeren \cite{Vansummeren2006}). Sulzmann

   315 and Lu sketch in \cite{Sulzmann2014} an informal correctness proof: but to

   316 us it contains unfillable gaps.\footnote{An extended version of

   317 \cite{Sulzmann2014} is available at the website of its first author; this

   318 extended version already includes remarks in the appendix that their

   319 informal proof contains gaps, and possible fixes are not fully worked out.}

   320 Our specification of a POSIX value consists of a simple inductive definition

   321 that given a string and a regular expression uniquely determines this value.

   322 We also show that our definition is equivalent to an ordering 

   323 of values based on positions by Okui and Suzuki \cite{OkuiSuzuki2010}.

   324 

   325 %Derivatives as calculated by Brzozowski's method are usually more complex

   326 %regular expressions than the initial one; various optimisations are

   327 %possible. We prove the correctness when simplifications of @{term "ALT ZERO r"}, 

   328 %@{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to

   329 %@{term r} are applied. 

   330 

   331 We extend our results to ??? Bitcoded version??

   332 

   333 \<close>

   334 

   335 section \<open>Preliminaries\<close>

   336 

   337 text \<open>\noindent Strings in Isabelle/HOL are lists of characters with

   338 the empty string being represented by the empty list, written @{term

   339 "[]"}, and list-cons being written as @{term "DUMMY # DUMMY"}. Often

   340 we use the usual bracket notation for lists also for strings; for

   341 example a string consisting of just a single character @{term c} is

   342 written @{term "[c]"}. We use the usual definitions for 

   343 \emph{prefixes} and \emph{strict prefixes} of strings.  By using the

   344 type @{type char} for characters we have a supply of finitely many

   345 characters roughly corresponding to the ASCII character set. Regular

   346 expressions are defined as usual as the elements of the following

   347 inductive datatype:

   348 

   349   \begin{center}

   350   \<open>r :=\<close>

   351   @{const "ZERO"} $\mid$

   352   @{const "ONE"} $\mid$

   353   @{term "CH c"} $\mid$

   354   @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$

   355   @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$

   356   @{term "STAR r"} 

   357   \end{center}

   358 

   359   \noindent where @{const ZERO} stands for the regular expression that does

   360   not match any string, @{const ONE} for the regular expression that matches

   361   only the empty string and @{term c} for matching a character literal. The

   362   language of a regular expression is also defined as usual by the

   363   recursive function @{term L} with the six clauses:

   364 

   365   \begin{center}

   366   \begin{tabular}{l@ {\hspace{4mm}}rcl}

   367   \textit{(1)} & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\

   368   \textit{(2)} & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\

   369   \textit{(3)} & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\

   370   \textit{(4)} & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & 

   371         @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\

   372   \textit{(5)} & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & 

   373         @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\

   374   \textit{(6)} & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\

   375   \end{tabular}

   376   \end{center}

   377   

   378   \noindent In clause \textit{(4)} we use the operation @{term "DUMMY ;;

   379   DUMMY"} for the concatenation of two languages (it is also list-append for

   380   strings). We use the star-notation for regular expressions and for

   381   languages (in the last clause above). The star for languages is defined

   382   inductively by two clauses: \<open>(i)\<close> the empty string being in

   383   the star of a language and \<open>(ii)\<close> if @{term "s\<^sub>1"} is in a

   384   language and @{term "s\<^sub>2"} in the star of this language, then also @{term

   385   "s\<^sub>1 @ s\<^sub>2"} is in the star of this language. It will also be convenient

   386   to use the following notion of a \emph{semantic derivative} (or \emph{left

   387   quotient}) of a language defined as

   388   %

   389   \begin{center}

   390   @{thm Der_def}\;.

   391   \end{center}

   392  

   393   \noindent

   394   For semantic derivatives we have the following equations (for example

   395   mechanically proved in \cite{Krauss2011}):

   396   %

   397   \begin{equation}\label{SemDer}

   398   \begin{array}{lcl}

   399   @{thm (lhs) Der_null}  & \dn & @{thm (rhs) Der_null}\\

   400   @{thm (lhs) Der_empty}  & \dn & @{thm (rhs) Der_empty}\\

   401   @{thm (lhs) Der_char}  & \dn & @{thm (rhs) Der_char}\\

   402   @{thm (lhs) Der_union}  & \dn & @{thm (rhs) Der_union}\\

   403   @{thm (lhs) Der_Sequ}  & \dn & @{thm (rhs) Der_Sequ}\\

   404   @{thm (lhs) Der_star}  & \dn & @{thm (rhs) Der_star}

   405   \end{array}

   406   \end{equation}

   407 

   408 

   409   \noindent \emph{\Brz's derivatives} of regular expressions

   410   \cite{Brzozowski1964} can be easily defined by two recursive functions:

   411   the first is from regular expressions to booleans (implementing a test

   412   when a regular expression can match the empty string), and the second

   413   takes a regular expression and a character to a (derivative) regular

   414   expression:

   415 

   416   \begin{center}

   417   \begin{tabular}{lcl}

   418   @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\

   419   @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\

   420   @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\

   421   @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\

   422   @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\

   423   @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\

   424 

   425 %  \end{tabular}

   426 %  \end{center}

   427 

   428 %  \begin{center}

   429 %  \begin{tabular}{lcl}

   430 

   431   @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\

   432   @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\

   433   @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\

   434   @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\

   435   @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\

   436   @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}

   437   \end{tabular}

   438   \end{center}

   439  

   440   \noindent

   441   We may extend this definition to give derivatives w.r.t.~strings:

   442 

   443   \begin{center}

   444   \begin{tabular}{lcl}

   445   @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\

   446   @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\

   447   \end{tabular}

   448   \end{center}

   449 

   450   \noindent Given the equations in \eqref{SemDer}, it is a relatively easy

   451   exercise in mechanical reasoning to establish that

   452 

   453   \begin{proposition}\label{derprop}\mbox{}\\ 

   454   \begin{tabular}{ll}

   455   \textit{(1)} & @{thm (lhs) nullable_correctness} if and only if

   456   @{thm (rhs) nullable_correctness}, and \\ 

   457   \textit{(2)} & @{thm[mode=IfThen] der_correctness}.

   458   \end{tabular}

   459   \end{proposition}

   460 

   461   \noindent With this in place it is also very routine to prove that the

   462   regular expression matcher defined as

   463   %

   464   \begin{center}

   465   @{thm match_def}

   466   \end{center}

   467 

   468   \noindent gives a positive answer if and only if @{term "s \<in> L r"}.

   469   Consequently, this regular expression matching algorithm satisfies the

   470   usual specification for regular expression matching. While the matcher

   471   above calculates a provably correct YES/NO answer for whether a regular

   472   expression matches a string or not, the novel idea of Sulzmann and Lu

   473   \cite{Sulzmann2014} is to append another phase to this algorithm in order

   474   to calculate a [lexical] value. We will explain the details next.

   475 

   476 \<close>

   477 

   478 section \<open>POSIX Regular Expression Matching\label{posixsec}\<close>

   479 

   480 text \<open>

   481 

   482   There have been many previous works that use values for encoding 

   483   \emph{how} a regular expression matches a string.

   484   The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to 

   485   define a function on values that mirrors (but inverts) the

   486   construction of the derivative on regular expressions. \emph{Values}

   487   are defined as the inductive datatype

   488 

   489   \begin{center}

   490   \<open>v :=\<close>

   491   @{const "Void"} $\mid$

   492   @{term "val.Char c"} $\mid$

   493   @{term "Left v"} $\mid$

   494   @{term "Right v"} $\mid$

   495   @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ 

   496   @{term "Stars vs"} 

   497   \end{center}  

   498 

   499   \noindent where we use @{term vs} to stand for a list of

   500   values. (This is similar to the approach taken by Frisch and

   501   Cardelli for GREEDY matching \cite{Frisch2004}, and Sulzmann and Lu

   502   for POSIX matching \cite{Sulzmann2014}). The string underlying a

   503   value can be calculated by the @{const flat} function, written

   504   @{term "flat DUMMY"} and defined as:

   505 

   506   \begin{center}

   507   \begin{tabular}[t]{lcl}

   508   @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\

   509   @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\

   510   @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\

   511   @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}

   512   \end{tabular}\hspace{14mm}

   513   \begin{tabular}[t]{lcl}

   514   @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\

   515   @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\

   516   @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\

   517   \end{tabular}

   518   \end{center}

   519 

   520   \noindent We will sometimes refer to the underlying string of a

   521   value as \emph{flattened value}.  We will also overload our notation and 

   522   use @{term "flats vs"} for flattening a list of values and concatenating

   523   the resulting strings.

   524   

   525   Sulzmann and Lu define

   526   inductively an \emph{inhabitation relation} that associates values to

   527   regular expressions. We define this relation as

   528   follows:\footnote{Note that the rule for @{term Stars} differs from

   529   our earlier paper \cite{AusafDyckhoffUrban2016}. There we used the

   530   original definition by Sulzmann and Lu which does not require that

   531   the values @{term "v \<in> set vs"} flatten to a non-empty

   532   string. The reason for introducing the more restricted version of

   533   lexical values is convenience later on when reasoning about an

   534   ordering relation for values.}

   535 

   536   \begin{center}

   537   \begin{tabular}{c@ {\hspace{12mm}}c}\label{prfintros}

   538   \\[-8mm]

   539   @{thm[mode=Axiom] Prf.intros(4)} & 

   540   @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm]

   541   @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} &

   542   @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]

   543   @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}  &

   544   @{thm[mode=Rule] Prf.intros(6)[of "vs"]}

   545   \end{tabular}

   546   \end{center}

   547 

   548   \noindent where in the clause for @{const "Stars"} we use the

   549   notation @{term "v \<in> set vs"} for indicating that \<open>v\<close> is a

   550   member in the list \<open>vs\<close>.  We require in this rule that every

   551   value in @{term vs} flattens to a non-empty string. The idea is that

   552   @{term "Stars"}-values satisfy the informal Star Rule (see Introduction)

   553   where the $^\star$ does not match the empty string unless this is

   554   the only match for the repetition.  Note also that no values are

   555   associated with the regular expression @{term ZERO}, and that the

   556   only value associated with the regular expression @{term ONE} is

   557   @{term Void}.  It is routine to establish how values ``inhabiting''

   558   a regular expression correspond to the language of a regular

   559   expression, namely

   560 

   561   \begin{proposition}\label{inhabs}

   562   @{thm L_flat_Prf}

   563   \end{proposition}

   564 

   565   \noindent

   566   Given a regular expression \<open>r\<close> and a string \<open>s\<close>, we define the 

   567   set of all \emph{Lexical Values} inhabited by \<open>r\<close> with the underlying string 

   568   being \<open>s\<close>:\footnote{Okui and Suzuki refer to our lexical values 

   569   as \emph{canonical values} in \cite{OkuiSuzuki2010}. The notion of \emph{non-problematic

   570   values} by Cardelli and Frisch \cite{Frisch2004} is related, but not identical

   571   to our lexical values.}

   572   

   573   \begin{center}

   574   @{thm LV_def}

   575   \end{center}

   576 

   577   \noindent The main property of @{term "LV r s"} is that it is alway finite.

   578 

   579   \begin{proposition}

   580   @{thm LV_finite}

   581   \end{proposition}

   582 

   583   \noindent This finiteness property does not hold in general if we

   584   remove the side-condition about @{term "flat v \<noteq> []"} in the

   585   @{term Stars}-rule above. For example using Sulzmann and Lu's

   586   less restrictive definition, @{term "LV (STAR ONE) []"} would contain

   587   infinitely many values, but according to our more restricted

   588   definition only a single value, namely @{thm LV_STAR_ONE_empty}.

   589 

   590   If a regular expression \<open>r\<close> matches a string \<open>s\<close>, then

   591   generally the set @{term "LV r s"} is not just a singleton set.  In

   592   case of POSIX matching the problem is to calculate the unique lexical value

   593   that satisfies the (informal) POSIX rules from the Introduction.

   594   Graphically the POSIX value calculation algorithm by Sulzmann and Lu

   595   can be illustrated by the picture in Figure~\ref{Sulz} where the

   596   path from the left to the right involving @{term

   597   derivatives}/@{const nullable} is the first phase of the algorithm

   598   (calculating successive \Brz's derivatives) and @{const

   599   mkeps}/\<open>inj\<close>, the path from right to left, the second

   600   phase. This picture shows the steps required when a regular

   601   expression, say \<open>r\<^sub>1\<close>, matches the string @{term

   602   "[a,b,c]"}. We first build the three derivatives (according to

   603   @{term a}, @{term b} and @{term c}). We then use @{const nullable}

   604   to find out whether the resulting derivative regular expression

   605   @{term "r\<^sub>4"} can match the empty string. If yes, we call the

   606   function @{const mkeps} that produces a value @{term "v\<^sub>4"}

   607   for how @{term "r\<^sub>4"} can match the empty string (taking into

   608   account the POSIX constraints in case there are several ways). This

   609   function is defined by the clauses:

   610 

   611 \begin{figure}[t]

   612 \begin{center}

   613 \begin{tikzpicture}[scale=2,node distance=1.3cm,

   614                     every node/.style={minimum size=6mm}]

   615 \node (r1)  {@{term "r\<^sub>1"}};

   616 \node (r2) [right=of r1]{@{term "r\<^sub>2"}};

   617 \draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};

   618 \node (r3) [right=of r2]{@{term "r\<^sub>3"}};

   619 \draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}};

   620 \node (r4) [right=of r3]{@{term "r\<^sub>4"}};

   621 \draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}};

   622 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}};

   623 \node (v4) [below=of r4]{@{term "v\<^sub>4"}};

   624 \draw[->,line width=1mm](r4) -- (v4);

   625 \node (v3) [left=of v4] {@{term "v\<^sub>3"}};

   626 \draw[->,line width=1mm](v4)--(v3) node[below,midway] {\<open>inj r\<^sub>3 c\<close>};

   627 \node (v2) [left=of v3]{@{term "v\<^sub>2"}};

   628 \draw[->,line width=1mm](v3)--(v2) node[below,midway] {\<open>inj r\<^sub>2 b\<close>};

   629 \node (v1) [left=of v2] {@{term "v\<^sub>1"}};

   630 \draw[->,line width=1mm](v2)--(v1) node[below,midway] {\<open>inj r\<^sub>1 a\<close>};

   631 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};

   632 \end{tikzpicture}

   633 \end{center}

   634 \mbox{}\\[-13mm]

   635 

   636 \caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},

   637 matching the string @{term "[a,b,c]"}. The first phase (the arrows from 

   638 left to right) is \Brz's matcher building successive derivatives. If the 

   639 last regular expression is @{term nullable}, then the functions of the 

   640 second phase are called (the top-down and right-to-left arrows): first 

   641 @{term mkeps} calculates a value @{term "v\<^sub>4"} witnessing

   642 how the empty string has been recognised by @{term "r\<^sub>4"}. After

   643 that the function @{term inj} ``injects back'' the characters of the string into

   644 the values.

   645 \label{Sulz}}

   646 \end{figure} 

   647 

   648   \begin{center}

   649   \begin{tabular}{lcl}

   650   @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\

   651   @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\

   652   @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\

   653   @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\

   654   \end{tabular}

   655   \end{center}

   656 

   657   \noindent Note that this function needs only to be partially defined,

   658   namely only for regular expressions that are nullable. In case @{const

   659   nullable} fails, the string @{term "[a,b,c]"} cannot be matched by @{term

   660   "r\<^sub>1"} and the null value @{term "None"} is returned. Note also how this function

   661   makes some subtle choices leading to a POSIX value: for example if an

   662   alternative regular expression, say @{term "ALT r\<^sub>1 r\<^sub>2"}, can

   663   match the empty string and furthermore @{term "r\<^sub>1"} can match the

   664   empty string, then we return a \<open>Left\<close>-value. The \<open>Right\<close>-value will only be returned if @{term "r\<^sub>1"} cannot match the empty

   665   string.

   666 

   667   The most interesting idea from Sulzmann and Lu \cite{Sulzmann2014} is

   668   the construction of a value for how @{term "r\<^sub>1"} can match the

   669   string @{term "[a,b,c]"} from the value how the last derivative, @{term

   670   "r\<^sub>4"} in Fig.~\ref{Sulz}, can match the empty string. Sulzmann and

   671   Lu achieve this by stepwise ``injecting back'' the characters into the

   672   values thus inverting the operation of building derivatives, but on the level

   673   of values. The corresponding function, called @{term inj}, takes three

   674   arguments, a regular expression, a character and a value. For example in

   675   the first (or right-most) @{term inj}-step in Fig.~\ref{Sulz} the regular

   676   expression @{term "r\<^sub>3"}, the character @{term c} from the last

   677   derivative step and @{term "v\<^sub>4"}, which is the value corresponding

   678   to the derivative regular expression @{term "r\<^sub>4"}. The result is

   679   the new value @{term "v\<^sub>3"}. The final result of the algorithm is

   680   the value @{term "v\<^sub>1"}. The @{term inj} function is defined by recursion on regular

   681   expressions and by analysing the shape of values (corresponding to 

   682   the derivative regular expressions).

   683   %

   684   \begin{center}

   685   \begin{tabular}{l@ {\hspace{5mm}}lcl}

   686   \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\

   687   \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 

   688       @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\

   689   \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 

   690       @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

   691   \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

   692       & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

   693   \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

   694       & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

   695   \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 

   696       & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

   697   \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 

   698       & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\

   699   \end{tabular}

   700   \end{center}

   701 

   702   \noindent To better understand what is going on in this definition it

   703   might be instructive to look first at the three sequence cases (clauses

   704   \textit{(4)} -- \textit{(6)}). In each case we need to construct an ``injected value'' for

   705   @{term "SEQ r\<^sub>1 r\<^sub>2"}. This must be a value of the form @{term

   706   "Seq DUMMY DUMMY"}\,. Recall the clause of the \<open>derivative\<close>-function

   707   for sequence regular expressions:

   708 

   709   \begin{center}

   710   @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}

   711   \end{center}

   712 

   713   \noindent Consider first the \<open>else\<close>-branch where the derivative is @{term

   714   "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore

   715   be of the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand

   716   side in clause~\textit{(4)} of @{term inj}. In the \<open>if\<close>-branch the derivative is an

   717   alternative, namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c

   718   r\<^sub>2)"}. This means we either have to consider a \<open>Left\<close>- or

   719   \<open>Right\<close>-value. In case of the \<open>Left\<close>-value we know further it

   720   must be a value for a sequence regular expression. Therefore the pattern

   721   we match in the clause \textit{(5)} is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"},

   722   while in \textit{(6)} it is just @{term "Right v\<^sub>2"}. One more interesting

   723   point is in the right-hand side of clause \textit{(6)}: since in this case the

   724   regular expression \<open>r\<^sub>1\<close> does not ``contribute'' to

   725   matching the string, that means it only matches the empty string, we need to

   726   call @{const mkeps} in order to construct a value for how @{term "r\<^sub>1"}

   727   can match this empty string. A similar argument applies for why we can

   728   expect in the left-hand side of clause \textit{(7)} that the value is of the form

   729   @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ (der c r)

   730   (STAR r)"}. Finally, the reason for why we can ignore the second argument

   731   in clause \textit{(1)} of @{term inj} is that it will only ever be called in cases

   732   where @{term "c=d"}, but the usual linearity restrictions in patterns do

   733   not allow us to build this constraint explicitly into our function

   734   definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs)

   735   injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]},

   736   but our deviation is harmless.}

   737 

   738   The idea of the @{term inj}-function to ``inject'' a character, say

   739   @{term c}, into a value can be made precise by the first part of the

   740   following lemma, which shows that the underlying string of an injected

   741   value has a prepended character @{term c}; the second part shows that

   742   the underlying string of an @{const mkeps}-value is always the empty

   743   string (given the regular expression is nullable since otherwise

   744   \<open>mkeps\<close> might not be defined).

   745 

   746   \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat}

   747   \begin{tabular}{ll}

   748   (1) & @{thm[mode=IfThen] Prf_injval_flat}\\

   749   (2) & @{thm[mode=IfThen] mkeps_flat}

   750   \end{tabular}

   751   \end{lemma}

   752 

   753   \begin{proof}

   754   Both properties are by routine inductions: the first one can, for example,

   755   be proved by induction over the definition of @{term derivatives}; the second by

   756   an induction on @{term r}. There are no interesting cases.\qed

   757   \end{proof}

   758 

   759   Having defined the @{const mkeps} and \<open>inj\<close> function we can extend

   760   \Brz's matcher so that a value is constructed (assuming the

   761   regular expression matches the string). The clauses of the Sulzmann and Lu lexer are

   762 

   763   \begin{center}

   764   \begin{tabular}{lcl}

   765   @{thm (lhs) lexer.simps(1)} & $\dn$ & @{thm (rhs) lexer.simps(1)}\\

   766   @{thm (lhs) lexer.simps(2)} & $\dn$ & \<open>case\<close> @{term "lexer (der c r) s"} \<open>of\<close>\\

   767                      & & \phantom{$|$} @{term "None"}  \<open>\<Rightarrow>\<close> @{term None}\\

   768                      & & $|$ @{term "Some v"} \<open>\<Rightarrow>\<close> @{term "Some (injval r c v)"}                          

   769   \end{tabular}

   770   \end{center}

   771 

   772   \noindent If the regular expression does not match the string, @{const None} is

   773   returned. If the regular expression \emph{does}

   774   match the string, then @{const Some} value is returned. One important

   775   virtue of this algorithm is that it can be implemented with ease in any

   776   functional programming language and also in Isabelle/HOL. In the remaining

   777   part of this section we prove that this algorithm is correct.

   778 

   779   The well-known idea of POSIX matching is informally defined by some

   780   rules such as the Longest Match and Priority Rules (see

   781   Introduction); as correctly argued in \cite{Sulzmann2014}, this

   782   needs formal specification. Sulzmann and Lu define an ``ordering

   783   relation'' between values and argue that there is a maximum value,

   784   as given by the derivative-based algorithm.  In contrast, we shall

   785   introduce a simple inductive definition that specifies directly what

   786   a \emph{POSIX value} is, incorporating the POSIX-specific choices

   787   into the side-conditions of our rules. Our definition is inspired by

   788   the matching relation given by Vansummeren~\cite{Vansummeren2006}. 

   789   The relation we define is ternary and

   790   written as \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating

   791   strings, regular expressions and values; the inductive rules are given in 

   792   Figure~\ref{POSIXrules}.

   793   We can prove that given a string @{term s} and regular expression @{term

   794    r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.

   795 

   796   %

   797   \begin{figure}[t]

   798   \begin{center}

   799   \begin{tabular}{c}

   800   @{thm[mode=Axiom] Posix.intros(1)}\<open>P\<close>@{term "ONE"} \qquad

   801   @{thm[mode=Axiom] Posix.intros(2)}\<open>P\<close>@{term "c"}\medskip\\

   802   @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\<open>P+L\<close>\qquad

   803   @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\<open>P+R\<close>\medskip\\

   804   $\mprset{flushleft}

   805    \inferrule

   806    {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad

   807     @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\

   808     @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}

   809    {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$\<open>PS\<close>\\

   810   @{thm[mode=Axiom] Posix.intros(7)}\<open>P[]\<close>\medskip\\

   811   $\mprset{flushleft}

   812    \inferrule

   813    {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

   814     @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

   815     @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\

   816     @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}

   817    {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$\<open>P\<star>\<close>

   818   \end{tabular}

   819   \end{center}

   820   \caption{Our inductive definition of POSIX values.}\label{POSIXrules}

   821   \end{figure}

   822 

   823    

   824 

   825   \begin{theorem}\mbox{}\smallskip\\\label{posixdeterm}

   826   \begin{tabular}{ll}

   827   (1) & If @{thm (prem 1) Posix1(1)} then @{thm (concl)

   828   Posix1(1)} and @{thm (concl) Posix1(2)}.\\

   829   (2) & @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v" "v'"]}

   830   \end{tabular}

   831   \end{theorem}

   832 

   833   \begin{proof} Both by induction on the definition of @{term "s \<in> r \<rightarrow> v"}. 

   834   The second parts follows by a case analysis of @{term "s \<in> r \<rightarrow> v'"} and

   835   the first part.\qed

   836   \end{proof}

   837 

   838   \noindent

   839   We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the four

   840   informal POSIX rules shown in the Introduction: Consider for example the

   841   rules \<open>P+L\<close> and \<open>P+R\<close> where the POSIX value for a string

   842   and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"},

   843   is specified---it is always a \<open>Left\<close>-value, \emph{except} when the

   844   string to be matched is not in the language of @{term "r\<^sub>1"}; only then it

   845   is a \<open>Right\<close>-value (see the side-condition in \<open>P+R\<close>).

   846   Interesting is also the rule for sequence regular expressions (\<open>PS\<close>). The first two premises state that @{term "v\<^sub>1"} and @{term "v\<^sub>2"}

   847   are the POSIX values for @{term "(s\<^sub>1, r\<^sub>1)"} and @{term "(s\<^sub>2, r\<^sub>2)"}

   848   respectively. Consider now the third premise and note that the POSIX value

   849   of this rule should match the string \mbox{@{term "s\<^sub>1 @ s\<^sub>2"}}. According to the

   850   Longest Match Rule, we want that the @{term "s\<^sub>1"} is the longest initial

   851   split of \mbox{@{term "s\<^sub>1 @ s\<^sub>2"}} such that @{term "s\<^sub>2"} is still recognised

   852   by @{term "r\<^sub>2"}. Let us assume, contrary to the third premise, that there

   853   \emph{exist} an @{term "s\<^sub>3"} and @{term "s\<^sub>4"} such that @{term "s\<^sub>2"}

   854   can be split up into a non-empty string @{term "s\<^sub>3"} and a possibly empty

   855   string @{term "s\<^sub>4"}. Moreover the longer string @{term "s\<^sub>1 @ s\<^sub>3"} can be

   856   matched by \<open>r\<^sub>1\<close> and the shorter @{term "s\<^sub>4"} can still be

   857   matched by @{term "r\<^sub>2"}. In this case @{term "s\<^sub>1"} would \emph{not} be the

   858   longest initial split of \mbox{@{term "s\<^sub>1 @ s\<^sub>2"}} and therefore @{term "Seq v\<^sub>1

   859   v\<^sub>2"} cannot be a POSIX value for @{term "(s\<^sub>1 @ s\<^sub>2, SEQ r\<^sub>1 r\<^sub>2)"}. 

   860   The main point is that our side-condition ensures the Longest 

   861   Match Rule is satisfied.

   862 

   863   A similar condition is imposed on the POSIX value in the \<open>P\<star>\<close>-rule. Also there we want that @{term "s\<^sub>1"} is the longest initial

   864   split of @{term "s\<^sub>1 @ s\<^sub>2"} and furthermore the corresponding value

   865   @{term v} cannot be flattened to the empty string. In effect, we require

   866   that in each ``iteration'' of the star, some non-empty substring needs to

   867   be ``chipped'' away; only in case of the empty string we accept @{term

   868   "Stars []"} as the POSIX value. Indeed we can show that our POSIX values

   869   are lexical values which exclude those \<open>Stars\<close> that contain subvalues 

   870   that flatten to the empty string.

   871 

   872   \begin{lemma}\label{LVposix}

   873   @{thm [mode=IfThen] Posix_LV}

   874   \end{lemma}

   875 

   876   \begin{proof}

   877   By routine induction on @{thm (prem 1) Posix_LV}.\qed 

   878   \end{proof}

   879 

   880   \noindent

   881   Next is the lemma that shows the function @{term "mkeps"} calculates

   882   the POSIX value for the empty string and a nullable regular expression.

   883 

   884   \begin{lemma}\label{lemmkeps}

   885   @{thm[mode=IfThen] Posix_mkeps}

   886   \end{lemma}

   887 

   888   \begin{proof}

   889   By routine induction on @{term r}.\qed 

   890   \end{proof}

   891 

   892   \noindent

   893   The central lemma for our POSIX relation is that the \<open>inj\<close>-function

   894   preserves POSIX values.

   895 

   896   \begin{lemma}\label{Posix2}

   897   @{thm[mode=IfThen] Posix_injval}

   898   \end{lemma}

   899 

   900   \begin{proof}

   901   By induction on \<open>r\<close>. We explain two cases.

   902 

   903   \begin{itemize}

   904   \item[$\bullet$] Case @{term "r = ALT r\<^sub>1 r\<^sub>2"}. There are

   905   two subcases, namely \<open>(a)\<close> \mbox{@{term "v = Left v'"}} and @{term

   906   "s \<in> der c r\<^sub>1 \<rightarrow> v'"}; and \<open>(b)\<close> @{term "v = Right v'"}, @{term

   907   "s \<notin> L (der c r\<^sub>1)"} and @{term "s \<in> der c r\<^sub>2 \<rightarrow> v'"}. In \<open>(a)\<close> we

   908   know @{term "s \<in> der c r\<^sub>1 \<rightarrow> v'"}, from which we can infer @{term "(c # s)

   909   \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v'"} by induction hypothesis and hence @{term "(c #

   910   s) \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> injval (ALT r\<^sub>1 r\<^sub>2) c (Left v')"} as needed. Similarly

   911   in subcase \<open>(b)\<close> where, however, in addition we have to use

   912   Proposition~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term

   913   "s \<notin> L (der c r\<^sub>1)"}.\smallskip

   914 

   915   \item[$\bullet$] Case @{term "r = SEQ r\<^sub>1 r\<^sub>2"}. There are three subcases:

   916   

   917   \begin{quote}

   918   \begin{description}

   919   \item[\<open>(a)\<close>] @{term "v = Left (Seq v\<^sub>1 v\<^sub>2)"} and @{term "nullable r\<^sub>1"} 

   920   \item[\<open>(b)\<close>] @{term "v = Right v\<^sub>1"} and @{term "nullable r\<^sub>1"} 

   921   \item[\<open>(c)\<close>] @{term "v = Seq v\<^sub>1 v\<^sub>2"} and @{term "\<not> nullable r\<^sub>1"} 

   922   \end{description}

   923   \end{quote}

   924 

   925   \noindent For \<open>(a)\<close> we know @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} and

   926   @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} as well as

   927   %

   928   \[@{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)"}\]

   929 

   930   \noindent From the latter we can infer by Proposition~\ref{derprop}(2):

   931   %

   932   \[@{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)"}\]

   933 

   934   \noindent We can use the induction hypothesis for \<open>r\<^sub>1\<close> to obtain

   935   @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer

   936   @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}. The case \<open>(c)\<close>

   937   is similar.

   938 

   939   For \<open>(b)\<close> we know @{term "s \<in> der c r\<^sub>2 \<rightarrow> v\<^sub>1"} and 

   940   @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former

   941   we have @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> (injval r\<^sub>2 c v\<^sub>1)"} by induction hypothesis

   942   for @{term "r\<^sub>2"}. From the latter we can infer

   943   %

   944   \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]

   945 

   946   \noindent By Lemma~\ref{lemmkeps} we know @{term "[] \<in> r\<^sub>1 \<rightarrow> (mkeps r\<^sub>1)"}

   947   holds. Putting this all together, we can conclude with @{term "(c #

   948   s) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (mkeps r\<^sub>1) (injval r\<^sub>2 c v\<^sub>1)"}, as required.

   949 

   950   Finally suppose @{term "r = STAR r\<^sub>1"}. This case is very similar to the

   951   sequence case, except that we need to also ensure that @{term "flat (injval r\<^sub>1

   952   c v\<^sub>1) \<noteq> []"}. This follows from @{term "(c # s\<^sub>1)

   953   \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}  (which in turn follows from @{term "s\<^sub>1 \<in> der c

   954   r\<^sub>1 \<rightarrow> v\<^sub>1"} and the induction hypothesis).\qed

   955   \end{itemize}

   956   \end{proof}

   957 

   958   \noindent

   959   With Lemma~\ref{Posix2} in place, it is completely routine to establish

   960   that the Sulzmann and Lu lexer satisfies our specification (returning

   961   the null value @{term "None"} iff the string is not in the language of the regular expression,

   962   and returning a unique POSIX value iff the string \emph{is} in the language):

   963 

   964   \begin{theorem}\mbox{}\smallskip\\\label{lexercorrect}

   965   \begin{tabular}{ll}

   966   (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\

   967   (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\

   968   \end{tabular}

   969   \end{theorem}

   970 

   971   \begin{proof}

   972   By induction on @{term s} using Lemma~\ref{lemmkeps} and \ref{Posix2}.\qed  

   973   \end{proof}

   974 

   975   \noindent In \textit{(2)} we further know by Theorem~\ref{posixdeterm} that the

   976   value returned by the lexer must be unique.   A simple corollary 

   977   of our two theorems is:

   978 

   979   \begin{corollary}\mbox{}\smallskip\\\label{lexercorrectcor}

   980   \begin{tabular}{ll}

   981   (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 

   982   (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\

   983   \end{tabular}

   984   \end{corollary}

   985 

   986   \noindent This concludes our correctness proof. Note that we have

   987   not changed the algorithm of Sulzmann and Lu,\footnote{All

   988   deviations we introduced are harmless.} but introduced our own

   989   specification for what a correct result---a POSIX value---should be.

   990   In the next section we show that our specification coincides with

   991   another one given by Okui and Suzuki using a different technique.

   992 

   993 \<close>

   994 

   995 section \<open>Ordering of Values according to Okui and Suzuki\<close>

   996 

   997 text \<open>

   998   

   999   While in the previous section we have defined POSIX values directly

  1000   in terms of a ternary relation (see inference rules in Figure~\ref{POSIXrules}),

  1001   Sulzmann and Lu took a different approach in \cite{Sulzmann2014}:

  1002   they introduced an ordering for values and identified POSIX values

  1003   as the maximal elements.  An extended version of \cite{Sulzmann2014}

  1004   is available at the website of its first author; this includes more

  1005   details of their proofs, but which are evidently not in final form

  1006   yet. Unfortunately, we were not able to verify claims that their

  1007   ordering has properties such as being transitive or having maximal

  1008   elements. 

  1009  

  1010   Okui and Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech} described

  1011   another ordering of values, which they use to establish the

  1012   correctness of their automata-based algorithm for POSIX matching.

  1013   Their ordering resembles some aspects of the one given by Sulzmann

  1014   and Lu, but overall is quite different. To begin with, Okui and

  1015   Suzuki identify POSIX values as minimal, rather than maximal,

  1016   elements in their ordering. A more substantial difference is that

  1017   the ordering by Okui and Suzuki uses \emph{positions} in order to

  1018   identify and compare subvalues. Positions are lists of natural

  1019   numbers. This allows them to quite naturally formalise the Longest

  1020   Match and Priority rules of the informal POSIX standard.  Consider

  1021   for example the value @{term v}

  1022 

  1023   \begin{center}

  1024   @{term "v == Stars [Seq (Char x) (Char y), Char z]"}

  1025   \end{center}

  1026 

  1027   \noindent

  1028   At position \<open>[0,1]\<close> of this value is the

  1029   subvalue \<open>Char y\<close> and at position \<open>[1]\<close> the

  1030   subvalue @{term "Char z"}.  At the `root' position, or empty list

  1031   @{term "[]"}, is the whole value @{term v}. Positions such as \<open>[0,1,0]\<close> or \<open>[2]\<close> are outside of \<open>v\<close>. If it exists, the subvalue of @{term v} at a position \<open>p\<close>, written @{term "at v p"}, can be recursively defined by

  1032   

  1033   \begin{center}

  1034   \begin{tabular}{r@ {\hspace{0mm}}lcl}

  1035   @{term v} &  \<open>\<downharpoonleft>\<^bsub>[]\<^esub>\<close> & \<open>\<equiv>\<close>& @{thm (rhs) at.simps(1)}\\

  1036   @{term "Left v"} & \<open>\<downharpoonleft>\<^bsub>0::ps\<^esub>\<close> & \<open>\<equiv>\<close>& @{thm (rhs) at.simps(2)}\\

  1037   @{term "Right v"} & \<open>\<downharpoonleft>\<^bsub>1::ps\<^esub>\<close> & \<open>\<equiv>\<close> & 

  1038   @{thm (rhs) at.simps(3)[simplified Suc_0_fold]}\\

  1039   @{term "Seq v\<^sub>1 v\<^sub>2"} & \<open>\<downharpoonleft>\<^bsub>0::ps\<^esub>\<close> & \<open>\<equiv>\<close> & 

  1040   @{thm (rhs) at.simps(4)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \\

  1041   @{term "Seq v\<^sub>1 v\<^sub>2"} & \<open>\<downharpoonleft>\<^bsub>1::ps\<^esub>\<close>

  1042   & \<open>\<equiv>\<close> & 

  1043   @{thm (rhs) at.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2", simplified Suc_0_fold]} \\

  1044   @{term "Stars vs"} & \<open>\<downharpoonleft>\<^bsub>n::ps\<^esub>\<close> & \<open>\<equiv>\<close>& @{thm (rhs) at.simps(6)}\\

  1045   \end{tabular} 

  1046   \end{center}

  1047 

  1048   \noindent In the last clause we use Isabelle's notation @{term "vs ! n"} for the

  1049   \<open>n\<close>th element in a list.  The set of positions inside a value \<open>v\<close>,

  1050   written @{term "Pos v"}, is given by 

  1051 

  1052   \begin{center}

  1053   \begin{tabular}{lcl}

  1054   @{thm (lhs) Pos.simps(1)} & \<open>\<equiv>\<close> & @{thm (rhs) Pos.simps(1)}\\

  1055   @{thm (lhs) Pos.simps(2)} & \<open>\<equiv>\<close> & @{thm (rhs) Pos.simps(2)}\\

  1056   @{thm (lhs) Pos.simps(3)} & \<open>\<equiv>\<close> & @{thm (rhs) Pos.simps(3)}\\

  1057   @{thm (lhs) Pos.simps(4)} & \<open>\<equiv>\<close> & @{thm (rhs) Pos.simps(4)}\\

  1058   @{thm (lhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}

  1059   & \<open>\<equiv>\<close> 

  1060   & @{thm (rhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\

  1061   @{thm (lhs) Pos_stars} & \<open>\<equiv>\<close> & @{thm (rhs) Pos_stars}\\

  1062   \end{tabular}

  1063   \end{center}

  1064 

  1065   \noindent 

  1066   whereby \<open>len\<close> in the last clause stands for the length of a list. Clearly

  1067   for every position inside a value there exists a subvalue at that position.

  1068  

  1069 

  1070   To help understanding the ordering of Okui and Suzuki, consider again 

  1071   the earlier value

  1072   \<open>v\<close> and compare it with the following \<open>w\<close>:

  1073 

  1074   \begin{center}

  1075   \begin{tabular}{l}

  1076   @{term "v == Stars [Seq (Char x) (Char y), Char z]"}\\

  1077   @{term "w == Stars [Char x, Char y, Char z]"}  

  1078   \end{tabular}

  1079   \end{center}

  1080 

  1081   \noindent Both values match the string \<open>xyz\<close>, that means if

  1082   we flatten these values at their respective root position, we obtain

  1083   \<open>xyz\<close>. However, at position \<open>[0]\<close>, \<open>v\<close> matches

  1084   \<open>xy\<close> whereas \<open>w\<close> matches only the shorter \<open>x\<close>. So

  1085   according to the Longest Match Rule, we should prefer \<open>v\<close>,

  1086   rather than \<open>w\<close> as POSIX value for string \<open>xyz\<close> (and

  1087   corresponding regular expression). In order to

  1088   formalise this idea, Okui and Suzuki introduce a measure for

  1089   subvalues at position \<open>p\<close>, called the \emph{norm} of \<open>v\<close>

  1090   at position \<open>p\<close>. We can define this measure in Isabelle as an

  1091   integer as follows

  1092   

  1093   \begin{center}

  1094   @{thm pflat_len_def}

  1095   \end{center}

  1096 

  1097   \noindent where we take the length of the flattened value at

  1098   position \<open>p\<close>, provided the position is inside \<open>v\<close>; if

  1099   not, then the norm is \<open>-1\<close>. The default for outside

  1100   positions is crucial for the POSIX requirement of preferring a

  1101   \<open>Left\<close>-value over a \<open>Right\<close>-value (if they can match the

  1102   same string---see the Priority Rule from the Introduction). For this

  1103   consider

  1104 

  1105   \begin{center}

  1106   @{term "v == Left (Char x)"} \qquad and \qquad @{term "w == Right (Char x)"}

  1107   \end{center}

  1108 

  1109   \noindent Both values match \<open>x\<close>. At position \<open>[0]\<close>

  1110   the norm of @{term v} is \<open>1\<close> (the subvalue matches \<open>x\<close>),

  1111   but the norm of \<open>w\<close> is \<open>-1\<close> (the position is outside

  1112   \<open>w\<close> according to how we defined the `inside' positions of

  1113   \<open>Left\<close>- and \<open>Right\<close>-values).  Of course at position

  1114   \<open>[1]\<close>, the norms @{term "pflat_len v [1]"} and @{term

  1115   "pflat_len w [1]"} are reversed, but the point is that subvalues

  1116   will be analysed according to lexicographically ordered

  1117   positions. According to this ordering, the position \<open>[0]\<close>

  1118   takes precedence over \<open>[1]\<close> and thus also \<open>v\<close> will be 

  1119   preferred over \<open>w\<close>.  The lexicographic ordering of positions, written

  1120   @{term "DUMMY \<sqsubset>lex DUMMY"}, can be conveniently formalised

  1121   by three inference rules

  1122 

  1123   \begin{center}

  1124   \begin{tabular}{ccc}

  1125   @{thm [mode=Axiom] lex_list.intros(1)}\hspace{1cm} &

  1126   @{thm [mode=Rule] lex_list.intros(3)[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2" and

  1127                                             ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}\hspace{1cm} &

  1128   @{thm [mode=Rule] lex_list.intros(2)[where ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}

  1129   \end{tabular}

  1130   \end{center}

  1131 

  1132   With the norm and lexicographic order in place,

  1133   we can state the key definition of Okui and Suzuki

  1134   \cite{OkuiSuzuki2010}: a value @{term "v\<^sub>1"} is \emph{smaller at position \<open>p\<close>} than

  1135   @{term "v\<^sub>2"}, written @{term "v\<^sub>1 \<sqsubset>val p v\<^sub>2"},