--- 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"
--- /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))))
+}
+
--- 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
}