(*<*)

theory Paper

imports 

   "../Lexer"

   "../Simplifying" 

   "../Positions"

   "../SizeBound" 

   "HOL-Library.LaTeXsugar"

begin

lemma Suc_0_fold:

  "Suc 0 = 1"

by simp

declare [[show_question_marks = false]]

syntax (latex output)

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

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

syntax

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

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

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"

abbreviation 

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

abbreviation

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

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) and  

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

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

  CH ("_" [1000] 80) and

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

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

  STAR ("_\<^sup>\<star>" [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 _" [79] 78) and

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

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

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

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

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

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

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

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

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

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

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

  set ("_" [73] 73) and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

definition 

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

lemma LV_STAR_ONE_empty: 

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

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

(*

comments not implemented

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

the proof of Lemma 3) to warrant a definition.

*)

(*>*)

section\<open>Core of the proof\<close>

text \<open>

This paper builds on previous work by Ausaf and Urban using 

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

is both fast and satisfies the POSIX specification.

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

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

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

built up by the injection funciton.

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

\begin{lemma}

@{thm [mode=IfThen] MAIN_decode}

\end{lemma}

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

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

\begin{lemma}

@{thm [mode=IfThen] blexer_correctness}

\end{lemma}

However what is not certain is whether we can add simplification

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

The reason that we do need to add a simplification phase

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

because it produces intermediate

regular expressions that can grow exponentially.

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

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

%TODO: add figure for this?

Therefore, we insert a simplification phase

after each derivation step, as defined below:

\begin{lemma}

@{thm blexer_simp_def}

\end{lemma}

The simplification function is given as follows:

\begin{center}

  \begin{tabular}{lcl}

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

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

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

\end{tabular}

\end{center}

And the two helper functions are:

\begin{center}

  \begin{tabular}{lcl}

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

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

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

\end{tabular}

\end{center}

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

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

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

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

to the POSIX standard.

By simplification, we mean specifically the following rules:

\begin{center}

  \begin{tabular}{lcl}

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tabular}

\end{center}

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

where the function $\mathit{bsimp_AALTs}$

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

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

remain "isomorphic" when we take the same sequence of

derivatives on both of them.

This can be expressed by the following rewrite relation lemma:

\begin{lemma}

@{thm [mode=IfThen] central}

\end{lemma}

This isomorphic relation implies a property that leads to the 

correctness result: 

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

from one another, 

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

bit-sequence :

\begin{lemma}

@{thm [mode=IfThen] rewrites_bmkeps}

\end{lemma}

Given the same bit-sequence, the decode function

will give out the same value, which is the output

of both lexers:

\begin{lemma}

@{thm blexer_def}

\end{lemma}

\begin{lemma}

@{thm blexer_simp_def}

\end{lemma}

And that yields the correctness result:

\begin{lemma}

@{thm blexersimp_correctness}

\end{lemma}

The nice thing about the above

\<close>

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

text  \<open>

One question someone would ask is:

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

so the simplification is even more aggressive, making

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

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

of a sequence:

\begin{center}

  \begin{tabular}{lcl}

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

  \end{tabular}

\end{center}

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

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

which  cannot be done under the rrewrite rule because only alternatives which are

children of another alternative can be spilled out.

\<close>

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

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

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

children of another alternative can be spilled out.*)

section \<open>Introduction\<close>

text \<open>

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

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

a character~\<open>c\<close>, and showed that it gave 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 derivative has the

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

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

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

The beauty of Brzozowski's derivatives 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. A

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

has been mentioned 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}.

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

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

disambiguation strategies to generate a unique answer: one is called

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

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

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

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

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

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

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

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

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

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

longest match.

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

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

strategy for what programmers consider basic syntactic building blocks

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

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

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

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

\begin{itemize} 

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

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

next token.\smallskip

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

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

that can match determines the token.\smallskip

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

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

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

be longer than no match at all.

\end{itemize}

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

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

recognising identifiers (say, a single character followed by

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

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

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

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

a single identifier token, not a keyword followed by an

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

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

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

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

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

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

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

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

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

and the parenthesised subexpression.

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

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

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

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

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

expression matches a string, values encode the information of

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

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

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

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

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

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

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

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

suggests to record this matching as

\begin{center}

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

\end{center}

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

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

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

regular expressions act as types and values as inhabiting those types

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

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

would look as follows

\begin{center}

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

\end{center}

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

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

by a sequence regular expression.