# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1476819594 -3600
# Node ID 2fddf8ab744f3882a532465bfbaa9f330dc3878e
# Parent  1dbf84ade62c5798896adc847f8c704461063741
updated

diff -r 1dbf84ade62c -r 2fddf8ab744f coursework/cw01.pdf
Binary file coursework/cw01.pdf has changed
diff -r 1dbf84ade62c -r 2fddf8ab744f coursework/cw01.tex
--- a/coursework/cw01.tex	Tue Oct 18 19:14:33 2016 +0100
+++ b/coursework/cw01.tex	Tue Oct 18 20:39:54 2016 +0100
@@ -6,7 +6,7 @@
 
 \section*{Coursework 1 (Strand 1)}
 
-This coursework is worth 4\% and is due on 20 October at
+This coursework is worth 4\% and is due on 25 October at
 16:00. You are asked to implement a regular expression matcher
 and submit a document containing the answers for the questions
 below. You can do the implementation in any programming
diff -r 1dbf84ade62c -r 2fddf8ab744f progs/Matcher2.thy
--- a/progs/Matcher2.thy	Tue Oct 18 19:14:33 2016 +0100
+++ b/progs/Matcher2.thy	Tue Oct 18 20:39:54 2016 +0100
@@ -359,9 +359,8 @@
 done
 
 lemma L_der_NTIMES:
-  shows "L(der c (NTIMES r n)) = (if n = 0 then {} else if nullable r then 
-       L(SEQ (der c r) (UPNTIMES r (n - 1)))
-       else L(SEQ (der c r) (NTIMES r (n - 1))))"
+  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
+         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
 apply(induct n)
 apply(simp)
 apply(simp)
@@ -376,6 +375,9 @@
 apply(simp)
 by (metis Suc_pred atMost_iff le_Suc_eq)
 
+lemma "L(der c (UPNTIMES r 0)) = {}"
+by simp
+
 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 using assms
 proof(induct n)