# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1540672589 -3600
# Node ID c1de75d20aa410c143a2276dd265cce90cbdd10e
# Parent  1a4e5b94293b46714141fb4c57f3e6204d8cfd08
added_lit

diff -r 1a4e5b94293b -r c1de75d20aa4 Literature/ReDoS1.pdf
Binary file Literature/ReDoS1.pdf has changed
diff -r 1a4e5b94293b -r c1de75d20aa4 Literature/ReDoS2.pdf
Binary file Literature/ReDoS2.pdf has changed
diff -r 1a4e5b94293b -r c1de75d20aa4 progs/scala/re-bit.scala
--- a/progs/scala/re-bit.scala	Sun Sep 30 12:02:04 2018 +0100
+++ b/progs/scala/re-bit.scala	Sat Oct 27 21:36:29 2018 +0100
@@ -134,6 +134,7 @@
   case STAR(r) => ASTAR(Nil, internalise(r))
 }
 
+
 internalise(("a" | "ab") ~ ("b" | ""))
 
 def retrieve(r: ARexp, v: Val) : List[Boolean] = (r, v) match {
diff -r 1a4e5b94293b -r c1de75d20aa4 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Sun Sep 30 12:02:04 2018 +0100
+++ b/thys/SpecExt.thy	Sat Oct 27 21:36:29 2018 +0100
@@ -1,6 +1,6 @@
    
 theory SpecExt
-  imports Main "~~/src/HOL/Library/Sublist"
+  imports Main (*"~~/src/HOL/Library/Sublist"*)
 begin
 
 section {* Sequential Composition of Languages *}
@@ -272,7 +272,7 @@
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))"
 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))"
-| "der c (FROMNTIMES r n) = 
+| "der c (FROMNTIMES r n) =
      (if n = 0 
       then SEQ (der c r) (STAR r)
       else SEQ (der c r) (FROMNTIMES r (n - 1)))"
@@ -282,6 +282,68 @@
                            SEQ (der c r) (UPNTIMES r (m - 1))) else 
                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
 
+lemma
+ "L(der c (UPNTIMES r m))  =
+     L(if (m = 0) then ZERO else ALT ONE (SEQ(der c r) (UPNTIMES r (m - 1))))"
+  apply(case_tac m)
+  apply(simp)
+  apply(simp del: der.simps)
+  apply(simp only: der.simps)
+  apply(simp add: Sequ_def)
+  apply(auto)
+  defer
+  apply blast
+  oops
+
+lemma pow_add:
+  assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m"
+  shows "s1 @ s2 \<in> A \<up> (n + m)"
+  using assms
+  apply(induct n arbitrary: m s1 s2)
+  apply(auto simp add: Sequ_def)
+  by blast
+
+lemma pow_add2:
+  assumes "x \<in> A \<up> (m + n)"
+  shows "x \<in> A \<up> m ;; A \<up> n"
+  using assms
+  apply(induct m arbitrary: n x)
+  apply(auto simp add: Sequ_def)
+  by (metis append.assoc)
+  
+
+
+lemma
+ "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"
+  apply(auto simp add: Sequ_def)
+  defer
+   apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")
+  prefer 2
+    apply (simp add: Star_Pow)
+  apply(auto)
+  apply(rule_tac x="n + m" in bexI)
+    apply (simp add: pow_add)
+   apply simp
+  apply(subgoal_tac "\<exists>m. m + n = xa")
+   apply(auto)
+   prefer 2
+  using le_add_diff_inverse2 apply auto[1]
+  by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)
+  
+lemma
+   "L (der c (FROMNTIMES r n)) = 
+     L (SEQ (der c r) (FROMNTIMES r (n - 1)))"
+  apply(auto simp add: Sequ_def)
+  using Star_Pow apply blast
+  using Pow_Star by blast
+  
+lemma
+ "L (der c (UPNTIMES r n)) = 
+    L(if n = 0 then ZERO  else 
+      ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"
+  apply(auto simp add: Sequ_def)
+  using SpecExt.Pow_empty by blast 
+
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 where