\documentclass{article}

\usepackage{../style}

\usepackage{../langs}

\begin{document}

\section*{Coursework (Strand 2)}

\begin{center}

\url{http://isabelle.in.tum.de}

\end{center}

\noindent This is an interactive theorem prover, meaning that

you can make definitions and state properties, and then help

the system with proving these properties. Sometimes the proofs

are also automatic. There is a shortish user guide for

Isabelle, called ``Programming and Proving in Isabelle/HOL''

at

\begin{center}

\url{http://isabelle.in.tum.de/documentation.html}

\end{center}

\noindent

and also a longer (free) book at

\begin{center}

\url{http://www.concrete-semantics.org}

\end{center}

\noindent The Isabelle theorem prover is operated through the

jEdit IDE, which might not be an editor that is widely known.

JEdit is documented in

\begin{center}

\url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf}

\end{center}

\noindent If you need more help or you are stuck somewhere,

please feel free to contact me (christian.urban@kcl.ac.uk). I

Isabelle is the recent verification of a microkernel operating

system by an Australian group, see \url{http://sel4.systems}.

Their operating system is the only one that has been proved

correct according to its specification and is used for

application where high assurance, security and reliability is

needed. 

\subsection*{The Task}

In this coursework you are asked to prove the correctness of

the regular expression matcher from the lectures in Isabelle.

For this you need to first specify what the matcher is

supposed to do and then to implement the algorithm. Finally

you need to prove that the algorithm meets the specification.

The first two parts are relatively easy, because the

definitions in Isabelle will look very similar to the

mathematical definitions from the lectures or the Scala code

that is supplied at KEATS. For example very similar to Scala,

regular expressions are defined in Isabelle as an inductive

datatype:

\begin{lstlisting}[language={},numbers=none]

datatype rexp =

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

\end{lstlisting}

\noindent The meaning of regular expressions is given as 

usual:

\begin{center}

\begin{tabular}{rcl@{\hspace{10mm}}l}

$L(c)$            & $\dn$ & $\{[c]\}$       & \pcode{CHAR}\\

$L(r_1 + r_2)$     & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\

$L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\

$L(r^*)$           & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\

\end{tabular}

\end{center}

\noindent You would need to implement this function in order

to state the theorem about the correctness of the algorithm.

The function $L$ should in Isabelle take a \pcode{rexp} as

input and return a set of strings. Its type is

therefore 

\begin{center}

\pcode{L} \pcode{::} \pcode{rexp} $\Rightarrow$ \pcode{string set}

\end{center}

\noindent Isabelle treats strings as an abbreviation for lists

of characters. This means you can pattern-match strings like

lists. The union operation on sets (for the \pcode{ALT}-case)

is a standard definition in Isabelle, but not the

concatenation operation on sets and also not the

star-operation. You would have to supply these definitions.

The concatenation operation can be defined in terms of the

append function, written \code{_ @ _} in Isabelle, for lists.

The star-operation can be defined as a ``big-union'' of 

powers, like in the lectures, or directly as an inductive set.

The functions for the matcher are shown in

Figure~\ref{matcher}. The theorem that needs to be proved is

\begin{lstlisting}[numbers=none,language={},keywordstyle=\color{black}\ttfamily,mathescape]

theorem 

  "matches r s $\longleftrightarrow$ s $\in$ L r"

\end{lstlisting}

\noindent which states that the function \emph{matches} is

true if and only if the string is in the language of the

regular expression. A proof for this lemma will need

side-lemmas about \pcode{nullable} and \pcode{der}. An example

proof in Isabelle that will not be relevant for the theorem

above is given in Figure~\ref{proof}.

\begin{figure}[p]

\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]

fun 

  nullable :: "rexp $\Rightarrow$ bool"

where

| "nullable (CHAR _) = False"

| "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"

| "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"

| "nullable (STAR _) = True"

fun 

  der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"

where

| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

| "der c (SEQ r1 r2) = 

     (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2)

                       else SEQ (der c r1) r2)"

| "der c (STAR r) = SEQ (der c r) (STAR r)"

fun 

  ders :: "rexp $\Rightarrow$ string $\Rightarrow$ rexp"

where

  "ders r [] = r"

| "ders r (c # s) = ders (der c r) s"

fun 

  matches :: "rexp $\Rightarrow$ string $\Rightarrow$ bool"

where

  "matches r s = nullable (ders r s)" 

\end{lstlisting}

\caption{The definition of the matcher algorithm in 

Isabelle.\label{matcher}}

\end{figure}

\begin{figure}[p]

\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]

fun 

  zeroable :: "rexp $\Rightarrow$ bool"

where

| "zeroable (CHAR _) = False"

| "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"

| "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"

| "zeroable (STAR _) = False"

lemma

  "zeroable r $\longleftrightarrow$ L r = {}"

proof (induct)

next

next

  case (CHAR c)

  have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all

  then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp

next 

  case (ALT r1 r2)

  have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact

  have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact

  show "zeroable (ALT r1 r2) $\longleftrightarrow$ (L (ALT r1 r2) = {})" 

    using ih1 ih2 by simp

next

  case (SEQ r1 r2)

  have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact

  have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact

  show "zeroable (SEQ r1 r2) $\longleftrightarrow$ (L (SEQ r1 r2) = {})" 

    using ih1 ih2 by (auto simp add: Conc_def)

next

  case (STAR r)

  have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all

  then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})" 

    by (simp (no_asm) add: Star_def) blast

qed

\end{lstlisting}

\caption{An Isabelle proof about the function \texttt{zeroable}.\label{proof}}

\end{figure}

\end{document}

%%% Local Variables: 

%%% mode: latex

%%% TeX-master: t

%%% End: