diff -r 5deefcc8cffa -r e3acf2bf3895 coursework/cw05.tex
--- a/coursework/cw05.tex	Tue Sep 20 12:24:29 2016 +0100
+++ b/coursework/cw05.tex	Tue Sep 20 12:25:09 2016 +0100
@@ -6,13 +6,11 @@
 
 \section*{Coursework (Strand 2)}
 
-\noindent This coursework is worth 25\% and is due on 11
-December at 16: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 
+\noindent This coursework is worth 20\% and is due on 13 December at
+16: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
 
 \begin{center}
 \url{http://isabelle.in.tum.de}
@@ -47,8 +45,8 @@
 
 \noindent If you need more help or you are stuck somewhere,
 please feel free to contact me (christian.urban@kcl.ac.uk). I
-am a main developer of Isabelle and have used it for
-approximately the 14 years. One of the success stories of
+am one of the main developers of Isabelle and have used it for
+approximately the 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
@@ -73,8 +71,8 @@
 
 \begin{lstlisting}[language={},numbers=none]
 datatype rexp =
-  NULL
-| EMPTY
+  ZERO
+| ONE
 | CHAR char
 | SEQ rexp rexp
 | ALT rexp rexp
@@ -86,8 +84,8 @@
 
 \begin{center}
 \begin{tabular}{rcl@{\hspace{10mm}}l}
-$L(\varnothing)$  & $\dn$ & $\varnothing$   & \pcode{NULL}\\
-$L(\epsilon)$     & $\dn$ & $\{[]\}$        & \pcode{EMPTY}\\ 
+$L(\ZERO)$  & $\dn$ & $\varnothing$   & \pcode{ZERO}\\
+$L(\ONE)$     & $\dn$ & $\{[]\}$        & \pcode{ONE}\\ 
 $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}\\
@@ -136,8 +134,8 @@
 fun 
   nullable :: "rexp $\Rightarrow$ bool"
 where
-  "nullable NULL = False"
-| "nullable EMPTY = True"
+  "nullable ZERO = False"
+| "nullable ONE = True"
 | "nullable (CHAR _) = False"
 | "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"
 | "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"
@@ -146,9 +144,9 @@
 fun 
   der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"
 where
-  "der c NULL = NULL"
-| "der c EMPTY = NULL"
-| "der c (CHAR d) = (if c = d then EMPTY else NULL)"
+  "der c ZERO = ZERO"
+| "der c ONE = ZERO"
+| "der c (CHAR d) = (if c = d then ONE else ZERO)"
 | "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)
@@ -175,8 +173,8 @@
 fun 
   zeroable :: "rexp $\Rightarrow$ bool"
 where
-  "zeroable NULL = True"
-| "zeroable EMPTY = False"
+  "zeroable ZERO = True"
+| "zeroable ONE = False"
 | "zeroable (CHAR _) = False"
 | "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"
 | "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"
@@ -185,13 +183,13 @@
 lemma
   "zeroable r $\longleftrightarrow$ L r = {}"
 proof (induct)
-  case (NULL)
-  have "zeroable NULL" "L NULL = {}" by simp_all
-  then show "zeroable NULL $\longleftrightarrow$ (L NULL = {})" by simp
+  case (ZERO)
+  have "zeroable ZERO" "L ZERO = {}" by simp_all
+  then show "zeroable ZERO $\longleftrightarrow$ (L ZERO = {})" by simp
 next
-  case (EMPTY)
-  have "$\neg$ zeroable EMPTY" "L EMPTY = {[]}" by simp_all
-  then show "zeroable EMPTY $\longleftrightarrow$ (L EMPTY = {})" by simp
+  case (ONE)
+  have "$\neg$ zeroable ONE" "L ONE = {[]}" by simp_all
+  then show "zeroable ONE $\longleftrightarrow$ (L ONE = {})" by simp
 next
   case (CHAR c)
   have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all