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 section\<open>Core of the proof\<close>

   135 text \<open>

   136 This paper builds on previous work by Ausaf and Urban using 

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

   138 is both fast and satisfies the POSIX specification.

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

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

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

   142 built up by the injection funciton.

   143 

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

   145 \begin{lemma}

   146 @{thm [mode=IfThen] MAIN_decode}

   147 \end{lemma}

   148 

   149 This lemma establishes a link with the lexer without bit-codes.

   150 

   151 With it we get the correctness of bit-coded algorithm.

   152 \begin{lemma}

   153 @{thm [mode=IfThen] blexer_correctness}

   154 \end{lemma}

   155 

   156 However what is not certain is whether we can add simplification

   157 to the bit-coded algorithm, without breaking the correct lexing output.

   158 

   159 

   160 The reason that we do need to add a simplification phase

   161 after each derivative step of  $\textit{blexer}$ is

   162 because it produces intermediate

   163 regular expressions that can grow exponentially.

   164 For example, the regular expression $(a+aa)^*$ after taking

   165 derivative against just 10 $a$s will have size 8192.

   166 

   167 %TODO: add figure for this?

   168 

   169 

   170 Therefore, we insert a simplification phase

   171 after each derivation step, as defined below:

   172 \begin{lemma}

   173 @{thm blexer_simp_def}

   174 \end{lemma}

   175 

   176 The simplification function is given as follows:

   177 

   178 \begin{center}

   179   \begin{tabular}{lcl}

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

   181   @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\

   182   @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\

   183 

   184 \end{tabular}

   185 \end{center}

   186 

   187 And the two helper functions are:

   188 \begin{center}

   189   \begin{tabular}{lcl}

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

   191   @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\

   192   @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\

   193 

   194 \end{tabular}

   195 \end{center}

   196 

   197 

   198 This might sound trivial in the case of producing a YES/NO answer,

   199 but once we require a lexing output to be produced (which is required

   200 in applications like compiler front-end, malicious attack domain extraction, 

   201 etc.), it is not straightforward if we still extract what is needed according

   202 to the POSIX standard.

   203 

   204 

   205 

   206 

   207 

   208 By simplification, we mean specifically the following rules:

   209 

   210 \begin{center}

   211   \begin{tabular}{lcl}

   212   @{thm[mode=Axiom] rrewrite.intros(1)[of "bs" "r\<^sub>2"]}\\

   213   @{thm[mode=Axiom] rrewrite.intros(2)[of "bs" "r\<^sub>1"]}\\

   214   @{thm[mode=Axiom] rrewrite.intros(3)[of  "bs" "bs\<^sub>1" "r\<^sub>1"]}\\

   215   @{thm[mode=Rule] rrewrite.intros(4)[of  "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\

   216   @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\

   217   @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\

   218   @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\

   219   @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\

   220   @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\

   221   @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\

   222   @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\

   223   @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\

   224 

   225   \end{tabular}

   226 \end{center}

   227 

   228 

   229 And these can be made compact by the following simplification function:

   230 

   231 where the function $\mathit{bsimp_AALTs}$

   232 

   233 The core idea of the proof is that two regular expressions,

   234 if "isomorphic" up to a finite number of rewrite steps, will

   235 remain "isomorphic" when we take the same sequence of

   236 derivatives on both of them.

   237 This can be expressed by the following rewrite relation lemma:

   238 \begin{lemma}

   239 @{thm [mode=IfThen] central}

   240 \end{lemma}

   241 

   242 This isomorphic relation implies a property that leads to the 

   243 correctness result: 

   244 if two (nullable) regular expressions are "rewritable" in many steps

   245 from one another, 

   246 then a call to function $\textit{bmkeps}$ gives the same

   247 bit-sequence :

   248 \begin{lemma}

   249 @{thm [mode=IfThen] rewrites_bmkeps}

   250 \end{lemma}

   251 

   252 Given the same bit-sequence, the decode function

   253 will give out the same value, which is the output

   254 of both lexers:

   255 \begin{lemma}

   256 @{thm blexer_def}

   257 \end{lemma}

   258 

   259 \begin{lemma}

   260 @{thm blexer_simp_def}

   261 \end{lemma}

   262 

   263 And that yields the correctness result:

   264 \begin{lemma}

   265 @{thm blexersimp_correctness}

   266 \end{lemma}

   267 

   268 The nice thing about the above

   269 \<close>

   270 

   271 

   272 section \<open> Additional Simp Rules?\<close>

   273 

   274 

   275 text  \<open>

   276 One question someone would ask is:

   277 can we add more "atomic" simplification/rewriting rules,

   278 so the simplification is even more aggressive, making

   279 the intermediate results smaller, and therefore more space-efficient? 

   280 For example, one might want to do open up alternatives who is a child

   281 of a sequence:

   282 

   283 \begin{center}

   284   \begin{tabular}{lcl}

   285     @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\

   286   \end{tabular}

   287 \end{center}

   288 

   289 This rule allows us to simplify \mbox{@{term "(ALT (SEQ (ALT a b) c)  (SEQ a c))"}}

   290  into  \mbox{@{term "ALT (SEQ a c)  (SEQ b c)"}},

   291 which is cannot be done under the \mbox{ \<leadsto>} rule because only alternatives which are

   292 children of another alternative can be spilled out.

   293 \<close>

   294 

   295 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}

   296  into  \mbox{@{term "ALT (SEQ a c)  (SEQ b c)"}},

   297 which is cannot be done under the  \<leadsto> rule because only alternatives which are 

   298 children of another alternative can be spilled out.*)

   299 section \<open>Introduction\<close>

   300 

   301 

   302 text \<open>

   303 

   304 

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

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

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

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

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

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

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

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

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

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

   315 The beauty of Brzozowski's derivatives is that

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

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

   318 consist of inductive datatypes and simple recursive functions. A

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

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

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

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

   323 

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

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

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

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

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

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

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

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

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

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

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

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

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

   337 longest match.

   338 

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

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

   341 strategy for what programmers consider basic syntactic building blocks

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

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

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

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

   346 

   347 \begin{itemize} 

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

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

   350 next token.\smallskip

   351 

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

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

   354 that can match determines the token.\smallskip

   355 

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

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

   358 

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

   360 be longer than no match at all.

   361 \end{itemize}

   362 

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

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

   365 recognising identifiers (say, a single character followed by

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   380 and the parenthesised subexpression.

   381 

   382 

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

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

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

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

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

   388 expression matches a string, values encode the information of

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

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

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

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

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

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

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

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

   397 suggests to record this matching as

   398 

   399 \begin{center}

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

   401 \end{center}

   402 

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

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

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

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

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

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

   409 would look as follows

   410 

   411 \begin{center}

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

   413 \end{center}

   414 

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

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

   417 by a sequence regular expression.

   418 

   419 %, which we will in what follows 

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

   421 

   422 

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

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

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

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

   427 indeed calculate a value that is correct according to the

   428 specification.  The answer given by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   449 

   450 \begin{quote}

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

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

   453 various subexpressions.''

   454 \end{quote}

   455 

   456 

   457 

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

   459 derivative-based regular expression matching algorithm of

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

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

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

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

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

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

   466 extended version already includes remarks in the appendix that their

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

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

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

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

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

   472 

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

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

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

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

   477 %@{term r} are applied. 

   478 

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

   480 

   481 \<close>

   482 

   483 

   484 

   485 

   486 section \<open>Preliminaries\<close>

   487 

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

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

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

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

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

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

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

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

   496 characters roughly corresponding to the ASCII character set. Regular

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

   498 inductive datatype:

   499 

   500   \begin{center}

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

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

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

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

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

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

   507   @{term "STAR r"} 

   508   \end{center}

   509 

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

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

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

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

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

   515 

   516   \begin{center}

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

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

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

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

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

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

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

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

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

   526   \end{tabular}

   527   \end{center}

   528   

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

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

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

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

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

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

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

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

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

   538   quotient}) of a language defined as

   539   %

   540   \begin{center}

   541   @{thm Der_def}\;.

   542   \end{center}

   543  

   544   \noindent

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

   546   mechanically proved in \cite{Krauss2011}):

   547   %

   548   \begin{equation}\label{SemDer}

   549   \begin{array}{lcl}

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

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

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

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

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

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

   556   \end{array}

   557   \end{equation}

   558 

   559 

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

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

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

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

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

   565   expression:

   566 

   567   \begin{center}

   568   \begin{tabular}{lcl}

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

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

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

   572   @{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"]}\\

   573   @{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"]}\\

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

   575 

   576 %  \end{tabular}

   577 %  \end{center}

   578 

   579 %  \begin{center}

   580 %  \begin{tabular}{lcl}

   581 

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

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

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

   585   @{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"]}\\

   586   @{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"]}\\

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

   588   \end{tabular}

   589   \end{center}

   590  

   591   \noindent

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

   593 

   594   \begin{center}

   595   \begin{tabular}{lcl}

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

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

   598   \end{tabular}

   599   \end{center}

   600 

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

   602   exercise in mechanical reasoning to establish that

   603 

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

   605   \begin{tabular}{ll}

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

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

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

   609   \end{tabular}

   610   \end{proposition}

   611 

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

   613   regular expression matcher defined as

   614   %

   615   \begin{center}

   616   @{thm match_def}

   617   \end{center}

   618 

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

   620   Consequently, this regular expression matching algorithm satisfies the

   621   usual specification for regular expression matching. While the matcher

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

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

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

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

   626 

   627 \<close>

   628 

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

   630 

   631 text \<open>

   632 

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

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

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

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

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

   638   are defined as the inductive datatype

   639 

   640   \begin{center}

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

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

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

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

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

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

   647   @{term "Stars vs"} 

   648   \end{center}  

   649 

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

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

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

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

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

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

   656 

   657   \begin{center}

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

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

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

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

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

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

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

   665   @{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"]}\\

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

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

   668   \end{tabular}

   669   \end{center}

   670 

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

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

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

   674   the resulting strings.

   675   

   676   Sulzmann and Lu define

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

   678   regular expressions. We define this relation as

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

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

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

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

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

   684   lexical values is convenience later on when reasoning about an

   685   ordering relation for values.}

   686 

   687   \begin{center}

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

   689   \\[-8mm]

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

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

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

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

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

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

   696   \end{tabular}

   697   \end{center}

   698 

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

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

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

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

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

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

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

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

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

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

   709   a regular expression correspond to the language of a regular

   710   expression, namely

   711 

   712   \begin{proposition}\label{inhabs}

   713   @{thm L_flat_Prf}

   714   \end{proposition}

   715 

   716   \noindent

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

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

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

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

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

   722   to our lexical values.}

   723   

   724   \begin{center}

   725   @{thm LV_def}

   726   \end{center}

   727 

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

   729 

   730   \begin{proposition}

   731   @{thm LV_finite}

   732   \end{proposition}

   733 

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

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

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

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

   738   infinitely many values, but according to our more restricted

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

   740 

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

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

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

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

   745   Graphically the POSIX value calculation algorithm by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

   755   to find out whether the resulting derivative regular expression

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

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

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

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

   760   function is defined by the clauses:

   761 

   762 \begin{figure}[t]

   763 \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   783 \end{tikzpicture}

   784 \end{center}

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

   786 

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

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

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

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

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

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

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

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

   795 the values.

   796 \label{Sulz}}

   797 \end{figure} 

   798 

   799   \begin{center}

   800   \begin{tabular}{lcl}

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

   802   @{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"]}\\

   803   @{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"]}\\

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

   805   \end{tabular}

   806   \end{center}

   807 

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

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

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

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

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

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

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

   815   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

   816   string.

   817 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   833   the derivative regular expressions).

   834   %

   835   \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   850   \end{tabular}

   851   \end{center}

   852 

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

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

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

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

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

   858   for sequence regular expressions:

   859 

   860   \begin{center}

   861   @{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"]}

   862   \end{center}

   863 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   887   but our deviation is harmless.}

   888 

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

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

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

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

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

   894   string (given the regular expression is nullable since otherwise

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

   896 

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

   898   \begin{tabular}{ll}

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

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

   901   \end{tabular}

   902   \end{lemma}

   903 

   904   \begin{proof}

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

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

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

   908   \end{proof}

   909 

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

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

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

   913 

   914   \begin{center}

   915   \begin{tabular}{lcl}

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

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

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

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

   920   \end{tabular}

   921   \end{center}

   922 

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

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

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

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

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

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

   929 

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

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

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

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

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

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

   936   introduce a simple inductive definition that specifies directly what

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

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

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

   940   The relation we define is ternary and

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

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

   943   Figure~\ref{POSIXrules}.

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

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

   946 

   947   %

   948   \begin{figure}[t]

   949   \begin{center}

   950   \begin{tabular}{c}

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

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

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

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

   955   $\mprset{flushleft}

   956    \inferrule

   957    {@{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

   958     @{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"]} \\\\

   959     @{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"]}}

   960    {@{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>\\

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

   962   $\mprset{flushleft}

   963    \inferrule

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

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

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

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

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

   969   \end{tabular}

   970   \end{center}

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

   972   \end{figure}

   973 

   974    

   975 

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

   977   \begin{tabular}{ll}

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

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

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

   981   \end{tabular}

   982   \end{theorem}

   983 

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

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

   986   the first part.\qed

   987   \end{proof}

   988 

   989   \noindent

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

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

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

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

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

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

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

   997   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"}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1012   Match Rule is satisfied.

  1013 

  1014   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

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

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

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

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

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

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

  1021   that flatten to the empty string.

  1022 

  1023   \begin{lemma}\label{LVposix}

  1024   @{thm [mode=IfThen] Posix_LV}

  1025   \end{lemma}

  1026 

  1027   \begin{proof}

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

  1029   \end{proof}

  1030 

  1031   \noindent

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

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

  1034 

  1035   \begin{lemma}\label{lemmkeps}

  1036   @{thm[mode=IfThen] Posix_mkeps}

  1037   \end{lemma}

  1038 

  1039   \begin{proof}

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

  1041   \end{proof}

  1042 

  1043   \noindent

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

  1045   preserves POSIX values.

  1046 

  1047   \begin{lemma}\label{Posix2}

  1048   @{thm[mode=IfThen] Posix_injval}

  1049   \end{lemma}

  1050 

  1051   \begin{proof}

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

  1053 

  1054   \begin{itemize}

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

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

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

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

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

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

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

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

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

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

  1065 

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

  1067   

  1068   \begin{quote}

  1069   \begin{description}

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

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

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

  1073   \end{description}

  1074   \end{quote}

  1075 

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

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

  1078   %

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

  1080 

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

  1082   %

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

  1084 

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

  1086   @{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

  1087   @{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>

  1088   is similar.

  1089 

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

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

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

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

  1094   %

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

  1096 

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

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

  1099   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.

  1100 

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

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

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

  1104   \<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

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

  1106   \end{itemize}

  1107   \end{proof}

  1108 

  1109   \noindent

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

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

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

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

  1114 

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

  1116   \begin{tabular}{ll}

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

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

  1119   \end{tabular}

  1120   \end{theorem}

  1121 

  1122   \begin{proof}

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

  1124   \end{proof}

  1125 

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

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

  1128   of our two theorems is:

  1129 

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

  1131   \begin{tabular}{ll}

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

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

  1134   \end{tabular}

  1135   \end{corollary}