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 aove

   269 \<close>

   270 

   271 

   272 

   273 section \<open>Introduction\<close>

   274 

   275 

   276 text \<open>

   277 

   278 

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

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

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

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

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

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

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

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

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

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

   289 The beauty of Brzozowski's derivatives is that

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

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

   292 consist of inductive datatypes and simple recursive functions. A

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

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

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

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

   297 

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

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

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

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

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

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

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

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

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

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

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

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

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

   311 longest match.

   312 

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

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

   315 strategy for what programmers consider basic syntactic building blocks

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

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

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

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

   320 

   321 \begin{itemize} 

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

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

   324 next token.\smallskip

   325 

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

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

   328 that can match determines the token.\smallskip

   329 

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

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

   332 

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

   334 be longer than no match at all.

   335 \end{itemize}

   336 

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

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

   339 recognising identifiers (say, a single character followed by

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   354 and the parenthesised subexpression.

   355 

   356 

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

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

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

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

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

   362 expression matches a string, values encode the information of

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

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

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

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

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

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

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

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

   371 suggests to record this matching as

   372 

   373 \begin{center}

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

   375 \end{center}

   376 

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

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

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

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

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

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

   383 would look as follows

   384 

   385 \begin{center}

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

   387 \end{center}

   388 

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

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

   391 by a sequence regular expression.

   392 

   393 %, which we will in what follows 

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

   395 

   396 

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

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

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

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

   401 indeed calculate a value that is correct according to the

   402 specification.  The answer given by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   423 

   424 \begin{quote}

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

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

   427 various subexpressions.''

   428 \end{quote}

   429 

   430 

   431 

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

   433 derivative-based regular expression matching algorithm of

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

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

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

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

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

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

   440 extended version already includes remarks in the appendix that their

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

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

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

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

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

   446 

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

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

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

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

   451 %@{term r} are applied. 

   452 

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

   454 

   455 \<close>

   456 

   457 

   458 

   459 

   460 section \<open>Preliminaries\<close>

   461 

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

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

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

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

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

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

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

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

   470 characters roughly corresponding to the ASCII character set. Regular

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

   472 inductive datatype:

   473 

   474   \begin{center}

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

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

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

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

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

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

   481   @{term "STAR r"} 

   482   \end{center}

   483 

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

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

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

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

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

   489 

   490   \begin{center}

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

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

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

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

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

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

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

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

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

   500   \end{tabular}

   501   \end{center}

   502   

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

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

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

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

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

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

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

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

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

   512   quotient}) of a language defined as

   513   %

   514   \begin{center}

   515   @{thm Der_def}\;.

   516   \end{center}

   517  

   518   \noindent

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

   520   mechanically proved in \cite{Krauss2011}):

   521   %

   522   \begin{equation}\label{SemDer}

   523   \begin{array}{lcl}

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

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

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

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

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

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

   530   \end{array}

   531   \end{equation}

   532 

   533 

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

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

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

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

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

   539   expression:

   540 

   541   \begin{center}

   542   \begin{tabular}{lcl}

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

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

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

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

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

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

   549 

   550 %  \end{tabular}

   551 %  \end{center}

   552 

   553 %  \begin{center}

   554 %  \begin{tabular}{lcl}

   555 

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

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

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

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

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

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

   562   \end{tabular}

   563   \end{center}

   564  

   565   \noindent

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

   567 

   568   \begin{center}

   569   \begin{tabular}{lcl}

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

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

   572   \end{tabular}

   573   \end{center}

   574 

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

   576   exercise in mechanical reasoning to establish that

   577 

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

   579   \begin{tabular}{ll}

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

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

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

   583   \end{tabular}

   584   \end{proposition}

   585 

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

   587   regular expression matcher defined as

   588   %

   589   \begin{center}

   590   @{thm match_def}

   591   \end{center}

   592 

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

   594   Consequently, this regular expression matching algorithm satisfies the

   595   usual specification for regular expression matching. While the matcher

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

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

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

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

   600 

   601 \<close>

   602 

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

   604 

   605 text \<open>

   606 

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

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

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

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

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

   612   are defined as the inductive datatype

   613 

   614   \begin{center}

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

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

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

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

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

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

   621   @{term "Stars vs"} 

   622   \end{center}  

   623 

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

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

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

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

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

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

   630 

   631   \begin{center}

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

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

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

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

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

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

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

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

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

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

   642   \end{tabular}

   643   \end{center}

   644 

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

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

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

   648   the resulting strings.

   649   

   650   Sulzmann and Lu define

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

   652   regular expressions. We define this relation as

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

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

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

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

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

   658   lexical values is convenience later on when reasoning about an

   659   ordering relation for values.}

   660 

   661   \begin{center}

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

   663   \\[-8mm]

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

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

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

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

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

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

   670   \end{tabular}

   671   \end{center}

   672 

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

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

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

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

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

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

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

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

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

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

   683   a regular expression correspond to the language of a regular

   684   expression, namely

   685 

   686   \begin{proposition}\label{inhabs}

   687   @{thm L_flat_Prf}

   688   \end{proposition}

   689 

   690   \noindent

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

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

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

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

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

   696   to our lexical values.}

   697   

   698   \begin{center}

   699   @{thm LV_def}

   700   \end{center}

   701 

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

   703 

   704   \begin{proposition}

   705   @{thm LV_finite}

   706   \end{proposition}

   707 

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

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

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

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

   712   infinitely many values, but according to our more restricted

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

   714 

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

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

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

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

   719   Graphically the POSIX value calculation algorithm by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

   729   to find out whether the resulting derivative regular expression

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

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

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

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

   734   function is defined by the clauses:

   735 

   736 \begin{figure}[t]

   737 \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   757 \end{tikzpicture}

   758 \end{center}

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

   760 

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

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

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

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

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

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

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

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

   769 the values.

   770 \label{Sulz}}

   771 \end{figure} 

   772 

   773   \begin{center}

   774   \begin{tabular}{lcl}

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

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

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

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

   779   \end{tabular}

   780   \end{center}

   781 

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

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

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

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

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

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

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

   789   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

   790   string.

   791 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   807   the derivative regular expressions).

   808   %

   809   \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   824   \end{tabular}

   825   \end{center}

   826 

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

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

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

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

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

   832   for sequence regular expressions:

   833 

   834   \begin{center}

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

   836   \end{center}

   837 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   861   but our deviation is harmless.}

   862 

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

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

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

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

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

   868   string (given the regular expression is nullable since otherwise

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

   870 

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

   872   \begin{tabular}{ll}

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

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

   875   \end{tabular}

   876   \end{lemma}

   877 

   878   \begin{proof}

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

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

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

   882   \end{proof}

   883 

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

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

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

   887 

   888   \begin{center}

   889   \begin{tabular}{lcl}

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

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

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

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

   894   \end{tabular}

   895   \end{center}

   896 

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

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

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

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

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

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

   903 

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

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

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

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

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

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

   910   introduce a simple inductive definition that specifies directly what

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

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

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

   914   The relation we define is ternary and

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

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

   917   Figure~\ref{POSIXrules}.

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

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

   920 

   921   %

   922   \begin{figure}[t]

   923   \begin{center}

   924   \begin{tabular}{c}

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

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

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

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

   929   $\mprset{flushleft}

   930    \inferrule

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

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

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

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

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

   936   $\mprset{flushleft}

   937    \inferrule

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

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

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

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

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

   943   \end{tabular}

   944   \end{center}

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

   946   \end{figure}

   947 

   948    

   949 

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

   951   \begin{tabular}{ll}

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

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

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

   955   \end{tabular}

   956   \end{theorem}

   957 

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

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

   960   the first part.\qed

   961   \end{proof}

   962 

   963   \noindent

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   986   Match Rule is satisfied.

   987 

   988   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

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

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

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

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

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

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

   995   that flatten to the empty string.

   996 

   997   \begin{lemma}\label{LVposix}

   998   @{thm [mode=IfThen] Posix_LV}

   999   \end{lemma}

  1000 

  1001   \begin{proof}

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

  1003   \end{proof}

  1004 

  1005   \noindent

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

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

  1008 

  1009   \begin{lemma}\label{lemmkeps}

  1010   @{thm[mode=IfThen] Posix_mkeps}

  1011   \end{lemma}

  1012 

  1013   \begin{proof}

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

  1015   \end{proof}

  1016 

  1017   \noindent

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

  1019   preserves POSIX values.

  1020 

  1021   \begin{lemma}\label{Posix2}

  1022   @{thm[mode=IfThen] Posix_injval}

  1023   \end{lemma}

  1024 

  1025   \begin{proof}

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

  1027 

  1028   \begin{itemize}

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

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

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

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

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

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

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

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

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

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

  1039 

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

  1041   

  1042   \begin{quote}

  1043   \begin{description}

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

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

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

  1047   \end{description}

  1048   \end{quote}

  1049 

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

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

  1052   %

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

  1054 

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

  1056   %

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

  1058 

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

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

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

  1062   is similar.

  1063 

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

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

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

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

  1068   %

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

  1070 

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

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

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

  1074 

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

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

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

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

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

  1080   \end{itemize}

  1081   \end{proof}

  1082 

  1083   \noindent

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

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

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

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

  1088 

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

  1090   \begin{tabular}{ll}

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

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

  1093   \end{tabular}

  1094   \end{theorem}

  1095 

  1096   \begin{proof}

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

  1098   \end{proof}

  1099 

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

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

  1102   of our two theorems is:

  1103 

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

  1105   \begin{tabular}{ll}

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

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

  1108   \end{tabular}

  1109   \end{corollary}

  1110 

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

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

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

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

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

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

  1117 

  1118 \<close>

  1119 

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

  1121 

  1122 text \<open>

  1123   

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

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

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

  1127   they introduced an ordering for values and identified POSIX values

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

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

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

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

  1132   ordering has properties such as being transitive or having maximal

  1133   elements. 

  1134  

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