1 (*<*)

     2 theory Paper

     3 imports 

     4    "../Lexer"

     5    "../Simplifying" 

     6    "../Positions"

     7 

     8    "../SizeBound" 

     9    "HOL-Library.LaTeXsugar"

    10 begin

    11 

    12 lemma Suc_0_fold:

    13   "Suc 0 = 1"

    14 by simp

    15 

    16 

    17 

    18 declare [[show_question_marks = false]]

    19 

    20 syntax (latex output)

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

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

    23 

    24 syntax

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

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

    27 

    28 

    29 abbreviation 

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

    31 

    32 abbreviation 

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

    34 

    35   abbreviation 

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

    37 

    38 abbreviation 

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

    40 

    41 

    42 abbreviation

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

    44 

    45 

    46 

    47 

    48 notation (latex output)

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

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

    51 

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

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

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

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

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

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

    58   

    59   val.Void ("Empty" 78) and

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

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

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

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

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

    65 

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

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

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

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

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

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

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

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

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

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

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

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

    78  

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

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

    81  

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

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

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

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

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

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

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

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

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

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

    92 

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

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

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

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

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

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

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

   100 

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

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

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

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

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

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

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

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

   109 

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

   111 

   112 

   113 definition 

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

   115 

   116 

   117 lemma LV_STAR_ONE_empty: 

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

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

   120 

   121 

   122 

   123 (*

   124 comments not implemented

   125 

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

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

   128 

   129 *)

   130 

   131 

   132 (*>*)

   133 

   134 

   135 

   136 section \<open>Introduction\<close>

   137 

   138 

   139 text \<open>

   140 Trying out after lualatex.

   141 

   142 

   143 uhuhuhu

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

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

   146 is both fast and satisfied the POSIX specification.

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

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

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

   150 built up by the injection funciton.

   151 

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

   153 \begin{lemma}

   154 @{thm [mode=IfThen] bder_retrieve}

   155 \end{lemma}

   156 

   157 This lemma links the regular expression

   158 

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

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

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

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

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

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

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

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

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

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

   169 The beauty of Brzozowski's derivatives is that

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

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

   172 consist of inductive datatypes and simple recursive functions. A

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

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

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

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

   177 

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

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

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

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

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

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

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

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

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

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

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

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

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

   191 longest match.

   192 

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

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

   195 strategy for what programmers consider basic syntactic building blocks

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

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

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

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

   200 

   201 \begin{itemize} 

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

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

   204 next token.\smallskip

   205 

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

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

   208 that can match determines the token.\smallskip

   209 

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

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

   212 

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

   214 be longer than no match at all.

   215 \end{itemize}

   216 

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

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

   219 recognising identifiers (say, a single character followed by

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   234 and the parenthesised subexpression.

   235 

   236 

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

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

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

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

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

   242 expression matches a string, values encode the information of

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

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

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

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

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

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

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

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

   251 suggests to record this matching as

   252 

   253 \begin{center}

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

   255 \end{center}

   256 

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

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

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

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

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

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

   263 would look as follows

   264 

   265 \begin{center}

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

   267 \end{center}

   268 

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

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

   271 by a sequence regular expression.

   272 

   273 %, which we will in what follows 

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

   275 

   276 

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

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

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

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

   281 indeed calculate a value that is correct according to the

   282 specification.  The answer given by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   303 

   304 \begin{quote}

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

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

   307 various subexpressions.''

   308 \end{quote}

   309 

   310 

   311 

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

   313 derivative-based regular expression matching algorithm of

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

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

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

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

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

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

   320 extended version already includes remarks in the appendix that their

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

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

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

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

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

   326 

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

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

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

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

   331 %@{term r} are applied. 

   332 

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

   334 

   335 \<close>

   336 

   337 section \<open>Preliminaries\<close>

   338 

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

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

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

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

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

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

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

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

   347 characters roughly corresponding to the ASCII character set. Regular

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

   349 inductive datatype:

   350 

   351   \begin{center}

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

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

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

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

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

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

   358   @{term "STAR r"} 

   359   \end{center}

   360 

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

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

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

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

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

   366 

   367   \begin{center}

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

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

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

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

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

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

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

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

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

   377   \end{tabular}

   378   \end{center}

   379   

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

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

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

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

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

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

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

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

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

   389   quotient}) of a language defined as

   390   %

   391   \begin{center}

   392   @{thm Der_def}\;.

   393   \end{center}

   394  

   395   \noindent

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

   397   mechanically proved in \cite{Krauss2011}):

   398   %

   399   \begin{equation}\label{SemDer}

   400   \begin{array}{lcl}

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

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

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

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

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

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

   407   \end{array}

   408   \end{equation}

   409 

   410 

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

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

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

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

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

   416   expression:

   417 

   418   \begin{center}

   419   \begin{tabular}{lcl}

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

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

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

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

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

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

   426 

   427 %  \end{tabular}

   428 %  \end{center}

   429 

   430 %  \begin{center}

   431 %  \begin{tabular}{lcl}

   432 

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

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

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

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

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

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

   439   \end{tabular}

   440   \end{center}

   441  

   442   \noindent

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

   444 

   445   \begin{center}

   446   \begin{tabular}{lcl}

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

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

   449   \end{tabular}

   450   \end{center}

   451 

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

   453   exercise in mechanical reasoning to establish that

   454 

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

   456   \begin{tabular}{ll}

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

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

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

   460   \end{tabular}

   461   \end{proposition}

   462 

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

   464   regular expression matcher defined as

   465   %

   466   \begin{center}

   467   @{thm match_def}

   468   \end{center}

   469 

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

   471   Consequently, this regular expression matching algorithm satisfies the

   472   usual specification for regular expression matching. While the matcher

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

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

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

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

   477 

   478 \<close>

   479 

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

   481 

   482 text \<open>

   483 

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

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

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

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

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

   489   are defined as the inductive datatype

   490 

   491   \begin{center}

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

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

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

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

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

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

   498   @{term "Stars vs"} 

   499   \end{center}  

   500 

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

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

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

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

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

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

   507 

   508   \begin{center}

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

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

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

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

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

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

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

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

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

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

   519   \end{tabular}

   520   \end{center}

   521 

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

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

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

   525   the resulting strings.

   526   

   527   Sulzmann and Lu define

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

   529   regular expressions. We define this relation as

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

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

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

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

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

   535   lexical values is convenience later on when reasoning about an

   536   ordering relation for values.}

   537 

   538   \begin{center}

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

   540   \\[-8mm]

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

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

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

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

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

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

   547   \end{tabular}

   548   \end{center}

   549 

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

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

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

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

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

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

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

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

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

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

   560   a regular expression correspond to the language of a regular

   561   expression, namely

   562 

   563   \begin{proposition}\label{inhabs}

   564   @{thm L_flat_Prf}

   565   \end{proposition}

   566 

   567   \noindent

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

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

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

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

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

   573   to our lexical values.}

   574   

   575   \begin{center}

   576   @{thm LV_def}

   577   \end{center}

   578 

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

   580 

   581   \begin{proposition}

   582   @{thm LV_finite}

   583   \end{proposition}

   584 

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

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

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

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

   589   infinitely many values, but according to our more restricted

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

   591 

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

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

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

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

   596   Graphically the POSIX value calculation algorithm by Sulzmann and Lu

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

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

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

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

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

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

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

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

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

   606   to find out whether the resulting derivative regular expression

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

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

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

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

   611   function is defined by the clauses:

   612 

   613 \begin{figure}[t]

   614 \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   634 \end{tikzpicture}

   635 \end{center}

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

   637 

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

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

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

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

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

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

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

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

   646 the values.

   647 \label{Sulz}}

   648 \end{figure} 

   649 

   650   \begin{center}

   651   \begin{tabular}{lcl}

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

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

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

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

   656   \end{tabular}

   657   \end{center}

   658 

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

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

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

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

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

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

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

   666   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

   667   string.

   668 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   684   the derivative regular expressions).

   685   %

   686   \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   701   \end{tabular}

   702   \end{center}

   703 

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

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

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

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

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

   709   for sequence regular expressions:

   710 

   711   \begin{center}

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

   713   \end{center}

   714 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   738   but our deviation is harmless.}

   739 

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

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

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

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

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

   745   string (given the regular expression is nullable since otherwise

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

   747 

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

   749   \begin{tabular}{ll}

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

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

   752   \end{tabular}

   753   \end{lemma}

   754 

   755   \begin{proof}

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

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

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

   759   \end{proof}

   760 

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

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

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

   764 

   765   \begin{center}

   766   \begin{tabular}{lcl}

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

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

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

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

   771   \end{tabular}

   772   \end{center}

   773 

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

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

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

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

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

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

   780 

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

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

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

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

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

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

   787   introduce a simple inductive definition that specifies directly what

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

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

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

   791   The relation we define is ternary and

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

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

   794   Figure~\ref{POSIXrules}.

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

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

   797 

   798   %

   799   \begin{figure}[t]

   800   \begin{center}

   801   \begin{tabular}{c}

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

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

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

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

   806   $\mprset{flushleft}

   807    \inferrule

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

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

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

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

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

   813   $\mprset{flushleft}

   814    \inferrule

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

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

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

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

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

   820   \end{tabular}

   821   \end{center}

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

   823   \end{figure}

   824 

   825    

   826 

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

   828   \begin{tabular}{ll}

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

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

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

   832   \end{tabular}

   833   \end{theorem}

   834 

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

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

   837   the first part.\qed

   838   \end{proof}

   839 

   840   \noindent

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   863   Match Rule is satisfied.

   864 

   865   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

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

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

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

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

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

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

   872   that flatten to the empty string.

   873 

   874   \begin{lemma}\label{LVposix}

   875   @{thm [mode=IfThen] Posix_LV}

   876   \end{lemma}

   877 

   878   \begin{proof}

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

   880   \end{proof}

   881 

   882   \noindent

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

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

   885 

   886   \begin{lemma}\label{lemmkeps}

   887   @{thm[mode=IfThen] Posix_mkeps}

   888   \end{lemma}

   889 

   890   \begin{proof}

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

   892   \end{proof}

   893 

   894   \noindent

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

   896   preserves POSIX values.

   897 

   898   \begin{lemma}\label{Posix2}

   899   @{thm[mode=IfThen] Posix_injval}

   900   \end{lemma}

   901 

   902   \begin{proof}

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

   904 

   905   \begin{itemize}

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

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

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

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

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

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

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

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

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

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

   916 

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

   918   

   919   \begin{quote}

   920   \begin{description}

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

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

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

   924   \end{description}

   925   \end{quote}

   926 

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

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

   929   %

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

   931 

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

   933   %

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

   935 

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

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

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

   939   is similar.

   940 

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

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

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

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

   945   %

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

   947 

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

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

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

   951 

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

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

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

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

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

   957   \end{itemize}

   958   \end{proof}

   959 

   960   \noindent

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

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

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

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

   965 

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

   967   \begin{tabular}{ll}

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

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

   970   \end{tabular}

   971   \end{theorem}

   972 

   973   \begin{proof}

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

   975   \end{proof}

   976 

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

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

   979   of our two theorems is:

   980 

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

   982   \begin{tabular}{ll}

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

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

   985   \end{tabular}

   986   \end{corollary}

   987 

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

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

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

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

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

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

   994 

   995 \<close>

   996 

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

   998 

   999 text \<open>

  1000   

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

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

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

  1004   they introduced an ordering for values and identified POSIX values

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

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

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

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

  1009   ordering has properties such as being transitive or having maximal

  1010   elements. 

  1011  

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

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

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

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

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

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

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

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

  1020   identify and compare subvalues. Positions are lists of natural

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

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

  1023   for example the value @{term v}

  1024 

  1025   \begin{center}

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

  1027   \end{center}

  1028 

  1029   \noindent

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

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

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

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

  1034   

  1035   \begin{center}

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

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

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

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

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

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

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

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

  1044   & \<open>\<equiv>\<close> & 

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

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

  1047   \end{tabular} 

  1048   \end{center}

  1049 

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

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

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

  1053 

  1054   \begin{center}

  1055   \begin{tabular}{lcl}

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

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

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

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

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

  1061   & \<open>\<equiv>\<close> 

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

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

  1064   \end{tabular}

  1065   \end{center}

  1066 

  1067   \noindent 

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

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

  1070  

  1071 

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

  1073   the earlier value

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

  1075 

  1076   \begin{center}

  1077   \begin{tabular}{l}

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

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

  1080   \end{tabular}

  1081   \end{center}

  1082 

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

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

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

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

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

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

  1089   corresponding regular expression). In order to

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

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

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

  1093   integer as follows

  1094   

  1095   \begin{center}

  1096   @{thm pflat_len_def}

  1097   \end{center}

  1098 

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

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

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

  1102   positions is crucial for the POSIX requirement of preferring a

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

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

  1105   consider

  1106 

  1107   \begin{center}

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

  1109   \end{center}

  1110 

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

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

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

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

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

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

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

  1118   will be analysed according to lexicographically ordered

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

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

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

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

  1123   by three inference rules

  1124 

  1125   \begin{center}

  1126   \begin{tabular}{ccc}

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

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

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

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

  1131   \end{tabular}

  1132   \end{center}

  1133 

  1134   With the norm and lexicographic order in place,

  1135   we can state the key definition of Okui and Suzuki