(*<*)

theory Paper

  imports

   "Posix.LexerSimp" 

   "Posix.FBound" 

   "HOL-Library.LaTeXsugar"

begin

declare [[show_question_marks = false]]

notation (latex output)

  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

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

abbreviation 

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

abbreviation 

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

abbreviation 

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

notation (latex output)

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

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

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

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

  bders_simp ("_\\\<^sub>b\<^sub>s\<^sub>i\<^sub>m\<^sub>p _" [79, 1000] 76) and

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

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

  CH ("_" [1000] 80) and

  ALT ("_ + _" [76,76] 77) and

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

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

  NTIMES ("_\<^sup>{\<^bsup>_\<^esup>\<^sup>}" [79] 78) and

  val.Void ("Empty" 78) and

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

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

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

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

  val.Stars ("Stars _" [1000] 78) and

  Prf ("\<turnstile> _ : _" [75,75] 75) and  

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

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

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

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

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

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

  set ("_" [73] 73) and

  AZERO ("ZERO" 81) and 

  AONE ("ONE _" [79] 78) and 

  ACHAR ("CHAR _ _" [79, 79] 80) and

  AALTs ("ALTs _ _" [77,77] 78) and

  ASEQ ("SEQ _ _ _" [79, 79,79] 78) and

  ASTAR ("STAR _ _" [79, 79] 78) and

  ANTIMES ("NT _ _ _" [79, 79, 79] 78) and

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

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

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

  bnullable ("bnullable _" [1000] 80) and

  bsimp_AALTs ("bsimpALT _ _" [10,1000] 80) and

  bsimp_ASEQ ("bsimpSEQ _ _ _" [10,1000,1000] 80) and

  bmkeps ("bmkeps _" [1000] 80) and

  eq1 ("_ \<approx> _" [77,77] 76) and 

  srewrite ("_\<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}$}\<close> _" [71, 71] 80) and

  rrewrites ("_ \<^latex>\<open>\\mbox{$\\,\\leadsto^*$}\<close> _" [71, 71] 80) and

  srewrites ("_ \<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}^*$}\<close> _" [71, 71] 80) and

  blexer_simp ("blexer\<^sup>+" 1000) 

lemma better_retrieve:

   shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

   and   "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

  apply (metis list.exhaust retrieve.simps(4))

  by (metis list.exhaust retrieve.simps(5))

lemma better_retrieve2:

  shows "retrieve (ANTIMES bs r (n + 1)) (Stars (v#vs)) = 

     bs @ [Z] @ retrieve r v @ retrieve (ANTIMES [] r n) (Stars vs)"

by auto

(*>*)

section {* Introduction *}

text {*

In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.

Derivatives of a

regular expression, written @{term "der c r"}, give a simple solution

to the problem of matching a string @{term s} with a regular

expression @{term r}: if the derivative of @{term r} w.r.t.\ (in

succession) all the characters of the string matches the empty string,

then @{term r} matches @{term s} (and {\em vice versa}).  

The beauty of

Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions. Another attractive

feature of derivatives is that they can be easily extended to \emph{bounded}

regular expressions, such as @{term "r"}$^{\{@{text n}\}}$ or @{term r}$^{\{..@{text n}\}}$, where numbers or

intervals of numbers specify how many times a regular expression should be used

during matching.

However, there are two difficulties with derivative-based matchers:

First, Brzozowski's original matcher only generates a yes/no answer

for whether a regular expression matches a string or not.  This is too

little information in the context of lexing where separate tokens must

be identified and also classified (for example as keywords

or identifiers).  Sulzmann and Lu~\cite{Sulzmann2014} overcome this

difficulty by cleverly extending Brzozowski's matching

algorithm. Their extended version generates additional information on

\emph{how} a regular expression matches a string following the POSIX

rules for regular expression matching. They achieve this by adding a

second ``phase'' to Brzozowski's algorithm involving an injection

function.  In our own earlier work we provided the formal

specification of what POSIX matching means and proved in Isabelle/HOL

the correctness

of Sulzmann and Lu's extended algorithm accordingly

\cite{AusafDyckhoffUrban2016}.

The second difficulty is that Brzozowski's derivatives can 

grow to arbitrarily big sizes. For example if we start with the

regular expression \mbox{@{text "(a + aa)\<^sup>*"}} and take

successive derivatives according to the character $a$, we end up with

a sequence of ever-growing derivatives like 

\def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}}

\begin{center}

\begin{tabular}{rll}

$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\

& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)

\end{tabular}

\end{center}

\noindent where after around 35 steps we run out of memory on a

typical computer (we shall define shortly the precise details of our

regular expressions and the derivative operation).  Clearly, the

notation involving $\ZERO$s and $\ONE$s already suggests

simplification rules that can be applied to regular regular

expressions, for example $\ZERO{}\,r \Rightarrow \ZERO$, $\ONE{}\,r

\Rightarrow r$, $\ZERO{} + r \Rightarrow r$ and $r + r \Rightarrow

r$. While such simple-minded simplifications have been proved in our

earlier work to preserve the correctness of Sulzmann and Lu's

algorithm \cite{AusafDyckhoffUrban2016}, they unfortunately do

\emph{not} help with limiting the growth of the derivatives shown

above: the growth is slowed, but some derivatives can still grow rather

quickly beyond any finite bound.

Sulzmann and Lu address this ``growth problem'' in a second algorithm

\cite{Sulzmann2014} where they introduce bitcoded

regular expressions. In this version, POSIX values are

represented as bitsequences and such sequences are incrementally generated

when derivatives are calculated. The compact representation

of bitsequences and regular expressions allows them to define a more

``aggressive'' simplification method that keeps the size of the

derivatives finitely bounded no matter what the length of the string is.

They make some informal claims about the correctness and linear behaviour

of this version, but do not provide any supporting proof arguments, not

even ``pencil-and-paper'' arguments. They write about their bitcoded

\emph{incremental parsing method} (that is the algorithm to be fixed and formalised

in this paper):

%

\begin{quote}\it

  ``Correctness Claim: We further claim that the incremental parsing

  method [..] in combination with the simplification steps [..]

  yields POSIX parse trees. We have tested this claim

  extensively [..] but yet

  have to work out all proof details.'' \cite[Page 14]{Sulzmann2014}

\end{quote}  

\noindent{}\textbf{Contributions:} We fill this gap by implementing in Isabelle/HOL

our version of the derivative-based lexing algorithm of Sulzmann and Lu

\cite{Sulzmann2014} where regular expressions are annotated with

bitsequences. We define the crucial simplification function as a

recursive function, without the need of a fixpoint operation. One objective of

the simplification function is to remove duplicates of regular

expressions.  For this Sulzmann and Lu use in their paper the standard

@{text nub} function from Haskell's list library, but this function

does not achieve the intended objective with bitcoded regular expressions.  The

reason is that in the bitcoded setting, each copy generally has a

different bitcode annotation---so @{text nub} would never ``fire''.

Inspired by Scala's library for lists, we shall instead use a @{text

distinctWith} function that finds duplicates under an ``erasing'' function

that deletes bitcodes before comparing regular expressions.

We shall also introduce our \emph{own} arguments and definitions for

establishing the correctness of the bitcoded algorithm when 

simplifications are included. Finally we

establish that the size of derivatives can be finitely bounded.\medskip%\footnote{ In this paper, we shall first briefly introduce the basic notions

%of regular expressions and describe the definition

%of POSIX lexing from our earlier work \cite{AusafDyckhoffUrban2016}. This serves

%as a reference point for what correctness means in our Isabelle/HOL proofs. We shall then prove

%the correctness for the bitcoded algorithm without simplification, and

%after that extend the proof to include simplification.}\smallskip

%\mbox{}\\[-10mm]

\noindent In this paper, we shall first briefly introduce the basic notions

of regular expressions and describe the definition

of POSIX lexing from our earlier work \cite{AusafDyckhoffUrban2016}. This serves

as a reference point for what correctness means in our Isabelle/HOL proofs. We shall then prove

the correctness for the bitcoded algorithm without simplification, and

after that extend the proof to include simplification.\mbox{}\\[-6mm]

*}

section {* Background *}

text {*

  In our Isabelle/HOL formalisation strings are lists of characters with

  the empty string being represented by the empty list, written $[]$,

  and list-cons being written as $\_\!::\!\_\,$; string

  concatenation is $\_ \,@\, \_\,$. We often use the usual

  bracket notation for lists also for strings; for example a string

  consisting of just a single character $c$ is written $[c]$.   

  Our regular expressions are defined as the following inductive

  datatype:\\[-4mm]

  %

  \begin{center}

  @{text "r ::="} \;

  @{const "ZERO"} $\mid$

  @{const "ONE"} $\mid$

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

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

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

  @{term "STAR r"} $\mid$

  @{term "NTIMES r n"}

  \end{center}

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

  does not match any string, @{const ONE} for the regular expression

  that matches only the empty string and @{term c} for matching a

  character literal.  The constructors $+$ and $\cdot$ represent

  alternatives and sequences, respectively.  We sometimes omit the

  $\cdot$ in a sequence regular expression for brevity.  The

  \emph{language} of a regular expression, written $L(r)$, is defined

  as usual and we omit giving the definition here (see for example

  \cite{AusafDyckhoffUrban2016}).

  In our work here we also add to the usual ``basic'' regular

  expressions the \emph{bounded} regular expression @{term "NTIMES r

  n"} where the @{term n} specifies that @{term r} should match

  exactly @{term n}-times. Again for brevity we omit the other bounded

  regular expressions @{text "r"}$^{\{..n\}}$, @{text "r"}$^{\{n..\}}$

  and @{text "r"}$^{\{n..m\}}$ which specify intervals for how many

  times @{text r} should match. The results presented in this paper

  extend straightforwardly to them too. The importance of the bounded

  regular expressions is that they are often used in practical

  applications, such as Snort (a system for detecting network

  intrusions) and also in XML Schema definitions. According to Bj\"{o}rklund et

  al~\cite{BjorklundMartensTimm2015}, bounded regular expressions 

  occur frequently in the latter and can have counters of up to

  ten million.  The problem is that tools based on the classic notion

  of automata need to expand @{text "r"}$^{\{n\}}$ into @{text n}

  connected copies of the automaton for @{text r}. This leads to very

  inefficient matching algorithms or algorithms that consume large

  amounts of memory.  A classic example is the regular expression

  \mbox{@{term "SEQ (SEQ (STAR (ALT a b)) a) (NTIMES (ALT a b) n)"}}

  where the minimal DFA requires at least $2^{n + 1}$ states (see

  \cite{CountingSet2020}). Therefore regular expression matching

  libraries that rely on the classic notion of DFAs often impose 

  adhoc limits for bounded regular expressions: For example in the

  regular expression matching library in the Go language and also in Google's RE2 library the regular expression

  @{term "NTIMES a 1001"} is not permitted, because no counter can be

  above 1000; and in the built-in regular expression library in Rust

  expressions such as @{text "a\<^bsup>{1000}{100}{5}\<^esup>"} give an error

  message for being too big.  These problems can of course be solved in matching

  algorithms where automata go beyond the classic notion and for

  instance include explicit counters (see~\cite{CountingSet2020}).

  The point here is that Brzozowski derivatives and the algorithms by

  Sulzmann and Lu can be straightforwardly extended to deal with

  bounded regular expressions and moreover the resulting code

  still consists of only simple recursive functions and inductive

  datatypes. Finally, bounded regular expressions 

  do not destroy our finite boundedness property, which we shall

  prove later on.%, because during the lexing process counters will only be

  %decremented.

  Central to Brzozowski's regular expression matcher are two functions

  called @{text nullable} and \emph{derivative}. The latter is written

  $r\backslash c$ for the derivative of the regular expression $r$

  w.r.t.~the character $c$. Both functions are defined by recursion over

  regular expressions.  

%

\begin{center}

\begin{tabular}{c @ {\hspace{-9mm}}c}

  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

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

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

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

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

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

  & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\

  & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\

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

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

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

  \end{tabular}

  &

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

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

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

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

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

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

  @{thm (lhs) nullable.simps(7)} & $\dn$ & @{text "if"} @{text "n = 0"}\\

  & & @{text "then"} @{const "True"}\\

  & & @{text "else"} @{term "nullable r"}

  \end{tabular}  

\end{tabular}  

\end{center}

  \noindent

  We can extend this definition to give derivatives w.r.t.~strings,

  namely as @{thm (lhs) ders.simps(1)}$\dn$@{thm (rhs) ders.simps(1)}

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

  Using @{text nullable} and the derivative operation, we can

define a simple regular expression matcher, namely

$@{text "match s r"} \dn @{term nullable}(r\backslash s)$.

This is essentially Brzozowski's algorithm from 1964. Its

main virtue is that the algorithm can be easily implemented as a

functional program (either in a functional programming language or in

a theorem prover). The correctness of @{text match} amounts to

establishing the property:%\footnote{It is a fun exercise to formally prove this property in a theorem prover.}

%

\begin{proposition}\label{matchcorr} 

@{text "match s r"} \;\;\text{if and only if}\;\; $s \in L(r)$

\end{proposition}

\noindent

It is a fun exercise to formally prove this property in a theorem prover.

We are aware

of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by

Owens and Slind~\cite{Owens2008}. Another one in Isabelle/HOL is part

of the work by Krauss and Nipkow~\cite{Krauss2011}.  And another one

in Coq is given by Coquand and Siles \cite{Coquand2012}.

Also Ribeiro and Du Bois give one in Agda~\cite{RibeiroAgda2017}.

The novel idea of Sulzmann and Lu is to extend this algorithm for 

lexing, where it is important to find out which part of the string

is matched by which part of the regular expression.

For this Sulzmann and Lu presented two lexing algorithms in their

paper~\cite{Sulzmann2014}. The first algorithm consists of two phases: first a

  matching phase (which is Brzozowski's algorithm) and then a value

  construction phase. The values encode \emph{how} a regular expression

  matches a string. \emph{Values} are defined as the inductive datatype

  %

  \begin{center}

  @{text "v ::="}

  @{const "Void"} $\mid$

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

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

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

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

  @{term "Stars vs"} 

  \end{center}  

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

  string underlying a value can be calculated by a @{const flat}

  function, written @{term "flat DUMMY"}. It traverses a value and

  collects the characters contained in it (see \cite{AusafDyckhoffUrban2016}).

  Sulzmann and Lu also define inductively an

  inhabitation relation that associates values to regular expressions. Our

  version of this relation is defined by the following six rules:

  %

  \begin{center}

  \begin{tabular}{@ {}l@ {}}

  @{thm[mode=Axiom] Prf.intros(4)}\quad

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

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

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

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

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

  $\mprset{flushleft}\inferrule{

  @{thm (prem 1) Prf.intros(7)[of "vs\<^sub>1" "r"  "vs\<^sub>2" "n"]}\\\\

  @{thm (prem 2) Prf.intros(7)[of "vs\<^sub>1" "r"  "vs\<^sub>2" "n"]}\\\\

  @{thm (prem 3) Prf.intros(7)[of "vs\<^sub>1" "r"  "vs\<^sub>2" "n"]}

  }

  {@{thm (concl) Prf.intros(7)[of "vs\<^sub>1" "r"  "vs\<^sub>2" "n"]}}

  $

  \end{tabular}

  \end{center}

  \noindent Note that no values are associated with the regular expression

  @{term ZERO}, since it cannot match any string. Interesting is our version

  of the rule for @{term "STAR r"} where we require that each value

  in  @{term vs} flattens to a non-empty string. This means if @{term "STAR r"} ``fires''

  one or more times, then each copy needs to match a non-empty string.

  Similarly, in the rule

  for @{term "NTIMES r n"} we require that the length of the list

  @{term "vs\<^sub>1 @ vs\<^sub>2"} equals @{term n} (meaning the regular expression

  @{text r} matches @{text n}-times) and that the first segment of this list

  contains values that flatten to non-empty strings followed by a segment that

  only contains values that flatten to the empty string. 

  It is routine to establish how values ``inhabiting'' a regular

  expression correspond to the language of a regular expression, namely

  @{thm L_flat_Prf}.

  In general there is more than one value inhabiting a regular

  expression (meaning regular expressions can typically match more

  than one string). But even when fixing a string from the language of the

  regular expression, there are generally more than one way of how the

  regular expression can match this string. POSIX lexing is about

  identifying the unique value for a given regular expression and a

  string that satisfies the informal POSIX rules (see

  \cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}).

  %\footnote{POSIX

  %	lexing acquired its name from the fact that the corresponding

  %	rules were described as part of the POSIX specification for

  %	Unix-like operating systems \cite{POSIX}.}

  Sometimes these

  informal rules are called \emph{maximal munch rule} and \emph{rule priority}.

  One contribution of our earlier paper is to give a convenient

 specification for what POSIX values are (the inductive rules are shown in

  Fig~\ref{POSIXrules}).

\begin{figure}[t]

  \begin{center}\small%

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

  \\[-4.5mm]

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

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

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

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

  $\mprset{flushleft}

   \inferrule

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

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

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

   {@{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>\medskip\smallskip\\

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

  $\mprset{flushleft}

   \inferrule

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

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

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

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

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

  \mprset{sep=4mm} 

  @{thm[mode=Rule] Posix.intros(9)}\<open>Pn[]\<close>\quad 

  $\mprset{flushleft}

   \inferrule

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

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

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

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

   {@{thm (concl) Posix.intros(8)[of "s\<^sub>1" "r" "v" "s\<^sub>2" n "vs"]}}$\<open>Pn+\<close>

  \\[-4mm]   

  \end{tabular}

  \end{center}

  \caption{The inductive definition of POSIX values taken from our earlier paper \cite{AusafDyckhoffUrban2016}. The ternary relation, written $(s, r) \rightarrow v$, formalises the notion

  of given a string $s$ and a regular

  expression $r$ what is the unique value $v$ that satisfies the informal POSIX constraints for

  regular expression matching.\smallskip}\label{POSIXrules}

  \end{figure}

  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} in their first algorithm is to define

  an injection function on values that mirrors (but inverts) the

  construction of the derivative on regular expressions. Essentially it

  injects back a character into a value.

  For this they define two functions called @{text mkeps} and @{text inj}:

 %

  \begin{center}

  \begin{tabular}{@ {}l@ {}}

  \begin{tabular}{@ {}lcl@ {}}

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

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

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

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

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

  \end{tabular}

  \medskip\\

  %!\begin{tabular}{@ {}cc@ {}}

  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}@ {}}

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

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

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

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

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

  %!

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

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

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

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

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

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

  %!

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

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

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