# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1446290212 0
# Node ID 0d6deecdb2ebbec658c7dc406d8e2b3106cf4570
# Parent  57ea439feaffda778755a58bd9fad38d12aed409
updated

diff -r 57ea439feaff -r 0d6deecdb2eb coursework/cw02.pdf
Binary file coursework/cw02.pdf has changed
diff -r 57ea439feaff -r 0d6deecdb2eb coursework/cw02.tex
--- a/coursework/cw02.tex	Fri Oct 23 14:45:57 2015 +0100
+++ b/coursework/cw02.tex	Sat Oct 31 11:16:52 2015 +0000
@@ -19,9 +19,9 @@
 
 It should be understood that the work you submit represents
 your own effort. You have not copied from anyone else. An
-exception is the Scala code I showed during the lectures,
-which you can use. You can also use your own code from the
-CW~1.
+exception is the Scala code from KEATS and the code I showed
+during the lectures, which you can both use. You can also use
+your own code from the CW~1.
 
 \subsection*{Question 1 (marked with 1\%)}
 
diff -r 57ea439feaff -r 0d6deecdb2eb handouts/ho01.tex
--- a/handouts/ho01.tex	Fri Oct 23 14:45:57 2015 +0100
+++ b/handouts/ho01.tex	Sat Oct 31 11:16:52 2015 +0000
@@ -384,9 +384,9 @@
 
 \begin{center}
 \begin{tabular}{rcl}
-$L(\varnothing)$  & $\dn$ & $\varnothing$\\
+$L(\varnothing)$  & $\dn$ & $\{\}$\\
 $L(\epsilon)$     & $\dn$ & $\{[]\}$\\
-$L(c)$            & $\dn$ & $\{"c"\}$\\
+$L(c)$            & $\dn$ & $\{[c]\}$\\
 $L(r_1+ r_2)$     & $\dn$ & $L(r_1) \cup L(r_2)$\\
 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$\\
 $L(r^*)$           & $\dn$ & $(L(r))^*$\\
diff -r 57ea439feaff -r 0d6deecdb2eb progs/Matcher2.thy
--- a/progs/Matcher2.thy	Fri Oct 23 14:45:57 2015 +0100
+++ b/progs/Matcher2.thy	Sat Oct 31 11:16:52 2015 +0000
@@ -196,9 +196,16 @@
 | "der c (OPT r) = der c r"
 | "der c (NTIMES r 0) = NULL"
 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
-| "der c (NMTIMES r n m) = (if m < n then NULL else 
+| "der c (NMTIMES r n m) = 
+     (if m < n then NULL else 
+     (if m = 0 then NULL else
+     (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))"
+(*
+
+  (if m < n then NULL else 
                               (if n = m then der c (NTIMES r n) else
                                 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
+*)
 by pat_completeness auto
 
 termination der 
@@ -294,8 +301,25 @@
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 by (auto simp add: Der_def)
 
+lemma der_correctness:
+  shows "L (der c r) = Der c (L r)"
+apply(induct rule: der.induct) 
+apply(simp_all add: nullable_correctness 
+    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
+apply(case_tac "[] \<in> L r")
+apply(simp)
+apply(case_tac n)
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(auto simp add: )[1]
+apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq)
 
+apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
+apply (metis Suc_leD atLeastAtMost_iff)
+by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
 
+(*
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
 apply(induct rule: der.induct) 
@@ -308,7 +332,7 @@
 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
 apply (metis Suc_leD atLeastAtMost_iff)
 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
-
+*)
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"
@@ -316,4 +340,88 @@
    (simp_all add: nullable_correctness der_correctness Der_def)
 
 
+lemma "L (der c (NMTIMES r n m)) = 
+  L ((if m < n then NULL else 
+     (if m = 0 then NULL else
+     (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))"
+apply(subst der.simps(12))
+apply(auto simp del: der.simps)
+apply(simp)
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subst (asm) der.simps(12))
+apply(auto)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(auto simp del: der.simps(12))[1]
+apply(subst (asm) der.simps(12))
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(case_tac "Suc nat = nata")
+apply(simp)
+apply(auto simp del: der.simps(12))[1]
+apply(auto)[1]
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp add: Seq_def)
+apply(auto)[1]
+apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat)
+apply(simp (no_asm) del: der.simps(12))
+apply(auto simp del: der.simps(12))[1]
+apply(case_tac "m = Suc n")
+apply(simp)
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(auto simp add: Seq_def del: der.simps(12))[1]
+
+apply(case_tac n)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(simp add: Seq_def)
+apply(auto)[1]
+apply(case_tac "nat = 0")
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(case_tac "Suc 0 = nat")
+apply(simp)
+apply(auto simp del: der.simps(12))[1]
+apply(simp)
+apply(case_tac "Suc 0 = nat")
+apply(simp)
+apply(auto simp add: Seq_def del: der.simps(12))[1]
+apply(rule_tac x="s1" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+apply(rule_tac x="1" in bexI)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto simp add: Seq_def)[1]
+apply(case_tac m)
+apply(simp)
+apply(simp)
+
 end    
\ No newline at end of file
diff -r 57ea439feaff -r 0d6deecdb2eb progs/re1.scala
--- a/progs/re1.scala	Fri Oct 23 14:45:57 2015 +0100
+++ b/progs/re1.scala	Sat Oct 31 11:16:52 2015 +0000
@@ -65,6 +65,9 @@
   (end - start)/(i * 1.0e9)
 }
 
+
 for (i <- 1 to 29) {
   println(i + ": " + "%.5f".format(time_needed(1, matches(EVIL(i), "a" * i))))
 }
+
+
diff -r 57ea439feaff -r 0d6deecdb2eb progs/re3.scala
--- a/progs/re3.scala	Fri Oct 23 14:45:57 2015 +0100
+++ b/progs/re3.scala	Sat Oct 31 11:16:52 2015 +0000
@@ -77,3 +77,64 @@
 }
 
 
+// some convenience for typing in regular expressions
+import scala.language.implicitConversions    
+import scala.language.reflectiveCalls 
+def charlist2rexp(s : List[Char]) : Rexp = s match {
+  case Nil => EMPTY
+  case c::Nil => CHAR(c)
+  case c::s => SEQ(CHAR(c), charlist2rexp(s))
+}
+implicit def string2rexp(s : String) : Rexp = charlist2rexp(s.toList)
+
+implicit def RexpOps (r: Rexp) = new {
+  def | (s: Rexp) = ALT(r, s)
+  def % = STAR(r)
+  def ~ (s: Rexp) = SEQ(r, s)
+}
+
+implicit def stringOps (s: String) = new {
+  def | (r: Rexp) = ALT(s, r)
+  def | (r: String) = ALT(s, r)
+  def % = STAR(s)
+  def ~ (r: Rexp) = SEQ(s, r)
+  def ~ (r: String) = SEQ(s, r)
+}
+
+
+
+def PLUS(r: Rexp) = SEQ(r, STAR(r))
+def RANGE(s: List[Char]) : Rexp = s match {
+  case Nil => NULL
+  case c::s => ALT(CHAR(c), RANGE(s))
+} 
+
+println("EVILS:")
+val EVIL1 = PLUS(PLUS("a" ~ "a" ~ "a"))
+val EVIL2 = PLUS(PLUS("aaaaaaaaaaaaaaaaaaa" ~ OPT("a")))  // 19 as ~ a?
+
+
+//40 * aaa matches
+//43 * aaa + aa does not
+//45 * aaa + a
+
+println("EVIL1:")
+println(matches(EVIL1, "aaa" * 40))
+println(matches(EVIL1, "aaa" * 43 + "aa"))
+println(matches(EVIL1, "aaa" * 45 + "a"))
+println("EVIL2:")
+println(matches(EVIL2, "aaa" * 40))
+println(matches(EVIL2, "aaa" * 43 + "aa"))
+println(matches(EVIL2, "aaa" * 45 + "a"))
+
+
+
+
+println("EMAIL:")
+val LOWERCASE = "abcdefghijklmnopqrstuvwxyz"
+val DIGITS = "0123456789"
+val EMAIL = PLUS(RANGE((LOWERCASE + DIGITS + "_" + "." + "-").toList)) ~ "@" ~ 
+            PLUS(RANGE((LOWERCASE + DIGITS + "." + "-").toList)) ~ "." ~
+            NMTIMES(RANGE((LOWERCASE + ".").toList), 2, 6)
+
+val my_email = "christian.urban@kcl.ac.uk"