--- a/coursework/cw05.tex	Mon Oct 01 01:11:42 2018 +0100
+++ b/coursework/cw05.tex	Mon Oct 01 14:04:48 2018 +0100
@@ -7,7 +7,7 @@
 \section*{Coursework (Strand 2)}
 
 \noindent This coursework is worth 20\% and is due on 14 December at
-16:00. You are asked to prove the correctness of the regular
+18:00. You are asked to prove the correctness of the regular
 expression matcher from the lectures using the Isabelle theorem
 prover. You need to submit a theory file containing this proof. The
 Isabelle theorem prover is available from
@@ -19,7 +19,7 @@
 \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
+are also completely automatic. There is a shortish user guide for
 Isabelle, called ``Programming and Proving in Isabelle/HOL''
 at
 
@@ -44,29 +44,49 @@
 
 
 \noindent If you need more help or you are stuck somewhere,
-please feel free to contact me (christian.urban@kcl.ac.uk). I
+please feel free to contact me (christian.urban at kcl.ac.uk). I
 am one of the main developers of Isabelle and have used it for
-approximately the 16 years. One of the success stories of
+approximately 16 years. One of the success stories of
 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. 
+needed (like in helicopters which fly over enemy territory).
 
 
 \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
+In this coursework you are asked to prove the correctness of the
+regular expression matcher from the lectures in Isabelle.  The matcher
+should be able to deal with the usual (basic) regular expressions
+
+\[
+\ZERO,\; \ONE,\; c,\; r_1 + r_2,\; r_1 \cdot r_2,\; r^*
+\]
+
+\noindent
+but also with the following extended regular expressions:
+
+\begin{center}
+\begin{tabular}{ll}
+  $r^{\{n\}}$ & exactly $n$-times\\
+  $r^{\{..m\}}$ & zero or more times $r$ but no more than $m$-times\\
+  $r^{\{n..\}}$ & at least $n$-times $r$\\
+  $r^{\{n..m\}}$ & at least $n$-times $r$ but no more than $m$-times\\
+  $\sim{}r$ & not-regular-expression of $r$\\
+\end{tabular}
+\end{center}
+
+
+\noindent
+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]