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

diff -r edb4ad356c56 -r 1dbf84ade62c progs/Matcher2.thy
--- a/progs/Matcher2.thy	Tue Oct 18 11:13:37 2016 +0100
+++ b/progs/Matcher2.thy	Tue Oct 18 19:14:33 2016 +0100
@@ -25,6 +25,7 @@
 | OPT rexp
 | NTIMES rexp nat
 | NMTIMES rexp nat nat
+| UPNTIMES rexp nat
 
 
 section {* Sequential Composition of Sets *}
@@ -147,7 +148,7 @@
 | "L (OPT r) = (L r) \<union> {[]}"
 | "L (NTIMES r n) = (L r) \<up> n"
 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
-
+| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
 lemma "L (NOT NULL) = UNIV"
 apply(simp)
@@ -169,6 +170,7 @@
 | "nullable (OPT r) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
+| "nullable (UPNTIMES r n) = True"
 
 fun M :: "rexp \<Rightarrow> nat"
 where
@@ -183,7 +185,7 @@
 | "M (OPT r) = Suc (M r)"
 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
-
+| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
@@ -202,6 +204,8 @@
         (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))))"
+| "der c (UPNTIMES r 0) = NULL"
+| "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))"
 by pat_completeness auto
 
 lemma bigger1:
@@ -224,9 +228,12 @@
 apply(simp_all del: M.simps)
 apply(simp_all only: M.simps)
 defer
+defer
+defer
 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 prefer 2
 apply(auto)[1]
+(*
 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 prefer 2
@@ -252,6 +259,8 @@
 apply (metis zero_less_one)
 apply(simp)
 done
+*)
+sorry
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -346,8 +355,73 @@
     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
 apply(rule impI)+
 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
+apply(auto simp add: Seq_def)
+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))))"
+apply(induct n)
+apply(simp)
+apply(simp)
 apply(auto)
-done
+apply(auto simp add: Seq_def)
+apply(rule_tac x="s1" in exI)
+apply(simp)
+apply(rule_tac x="xa" in bexI)
+apply(simp)
+apply(simp)
+apply(rule_tac x="s1" in exI)
+apply(simp)
+by (metis Suc_pred atMost_iff le_Suc_eq)
+
+lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
+using assms
+proof(induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
+  { assume a: "nullable r"
+    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by(simp only: L.simps Suc_Union)
+    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
+    by(auto simp add: Seq_def)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using IH by simp
+    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using a unfolding L_der_NTIMES by simp
+    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+    by (auto, metis Suc_Union Un_iff seq_Union)
+    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
+    } 
+  moreover
+  { assume a: "\<not>nullable r"
+    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by(simp only: L.simps Suc_Union)
+    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
+    by (simp only: der_correctness)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
+    by(auto simp add: Seq_def)
+    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using IH by simp
+    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
+    using a unfolding L_der_NTIMES by simp
+    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+    by (simp add: Suc_Union seq_union(1))
+    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
+  }
+  ultimately  
+  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
+  by blast
+qed
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"
diff -r edb4ad356c56 -r 1dbf84ade62c progs/re3a.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progs/re3a.scala	Tue Oct 18 19:14:33 2016 +0100
@@ -0,0 +1,105 @@
+
+abstract class Rexp
+case object ZERO extends Rexp
+case object ONE extends Rexp
+case class CHAR(c: Char) extends Rexp
+case class ALT(r1: Rexp, r2: Rexp) extends Rexp 
+case class SEQ(r1: Rexp, r2: Rexp) extends Rexp 
+case class STAR(r: Rexp) extends Rexp 
+case class NTIMES(r: Rexp, n: Int) extends Rexp 
+case class UPNTIMES(r: Rexp, n: Int) extends Rexp 
+
+// nullable function: tests whether the regular 
+// expression can recognise the empty string
+def nullable (r: Rexp) : Boolean = r match {
+  case ZERO => false
+  case ONE => true
+  case CHAR(_) => false
+  case ALT(r1, r2) => nullable(r1) || nullable(r2)
+  case SEQ(r1, r2) => nullable(r1) && nullable(r2)
+  case STAR(_) => true
+  case NTIMES(r, i) => if (i == 0) true else nullable(r)
+  case UPNTIMES(r: Rexp, n: Int) => true
+}
+
+// derivative of a regular expression w.r.t. a character
+def der (c: Char, r: Rexp) : Rexp = r match {
+  case ZERO => ZERO
+  case ONE => ZERO
+  case CHAR(d) => if (c == d) ONE else ZERO
+  case ALT(r1, r2) => ALT(der(c, r1), der(c, r2))
+  case SEQ(r1, r2) => 
+    if (nullable(r1)) ALT(SEQ(der(c, r1), r2), der(c, r2))
+    else SEQ(der(c, r1), r2)
+  case STAR(r1) => SEQ(der(c, r1), STAR(r1))
+  case NTIMES(r1, i) => 
+    if (i == 0) ZERO else
+    if (nullable(r1)) SEQ(der(c, r1), UPNTIMES(r1, i - 1))
+    else SEQ(der(c, r1), NTIMES(r1, i))
+  case UPNTIMES(r1, i) => 
+    if (i == 0) ZERO
+    else SEQ(der(c, r1), UPNTIMES(r1, i - 1)) 
+}
+
+def simp(r: Rexp) : Rexp = r match {
+  case ALT(r1, r2) => (simp(r1), simp(r2)) match {
+    case (ZERO, r2s) => r2s
+    case (r1s, ZERO) => r1s
+    case (r1s, r2s) => if (r1s == r2s) r1s else ALT (r1s, r2s)
+  }
+  case SEQ(r1, r2) =>  (simp(r1), simp(r2)) match {
+    case (ZERO, _) => ZERO
+    case (_, ZERO) => ZERO
+    case (ONE, r2s) => r2s
+    case (r1s, ONE) => r1s
+    case (r1s, r2s) => SEQ(r1s, r2s)
+  }
+  case r => r
+}
+
+
+// derivative w.r.t. a string (iterates der)
+def ders (s: List[Char], r: Rexp) : Rexp = s match {
+  case Nil => r
+  case c::s => ders(s, simp(der(c, r)))
+}
+
+
+// main matcher function
+def matcher(r: Rexp, s: String) : Boolean = nullable(ders(s.toList, r))
+
+
+//one or zero
+def OPT(r: Rexp) = ALT(r, ONE)
+
+//evil regular expressions
+def EVIL1(n: Int) = SEQ(NTIMES(OPT(CHAR('a')), n), NTIMES(CHAR('a'), n))
+val EVIL2 = SEQ(STAR(STAR(CHAR('a'))), CHAR('b'))
+
+
+def time_needed[T](i: Int, code: => T) = {
+  val start = System.nanoTime()
+  for (j <- 1 to i) code
+  val end = System.nanoTime()
+  (end - start)/(i * 1.0e9)
+}
+
+
+//test: (a?{n}) (a{n})
+for (i <- 1 to 8001 by 1000) {
+  println(i + " " + "%.5f".format(time_needed(2, matcher(EVIL1(i), "a" * i))))
+}
+
+for (i <- 1 to 8001 by 1000) {
+  println(i + " " + "%.5f".format(time_needed(2, matcher(EVIL1(i), "a" * i))))
+}
+
+//test: (a*)* b
+for (i <- 1 to 7000001 by 500000) {
+  println(i + " " + "%.5f".format(time_needed(2, matcher(EVIL2, "a" * i))))
+}
+
+for (i <- 1 to 7000001 by 500000) {
+  println(i + " " + "%.5f".format(time_needed(2, matcher(EVIL2, "a" * i))))
+}
+
diff -r edb4ad356c56 -r 1dbf84ade62c progs/re4.scala
--- a/progs/re4.scala	Tue Oct 18 11:13:37 2016 +0100
+++ b/progs/re4.scala	Tue Oct 18 19:14:33 2016 +0100
@@ -30,8 +30,8 @@
     if (nullable(r1)) ALT(SEQ(der(c, r1), r2), der(c, r2))
     else SEQ(der(c, r1), r2)
   case STAR(r1) => SEQ(der(c, r1), STAR(r1))
-  case NTIMES(r, i) => 
-    if (i == 0) ZERO else SEQ(der(c, r), NTIMES(r, i - 1))
+  case NTIMES(r1, i) => 
+    if (i == 0) ZERO else der(c, SEQ(r1, NTIMES(r1, i - 1)))
 }
 
 def simp(r: Rexp) : Rexp = r match {
@@ -47,11 +47,6 @@
     case (r1s, ONE) => r1s
     case (r1s, r2s) => SEQ(r1s, r2s)
   }
-  case NTIMES(r1, n) => simp(r1) match {
-    case ZERO => ZERO
-    case ONE => ONE
-    case r1s => NTIMES(r1s, n)
-  }
   case r => r
 }