--- a/progs/scala/re-ext.scala	Sat Mar 11 12:50:01 2017 +0000
+++ b/progs/scala/re-ext.scala	Sat Mar 11 19:33:38 2017 +0000
@@ -2,6 +2,7 @@
 import scala.language.reflectiveCalls
 import scala.annotation.tailrec   
 import scala.io.Source
+import scala.util._
 
 abstract class Rexp 
 case object ZERO extends Rexp
@@ -157,7 +158,8 @@
   case c::cs => inj(r, c, lex(der(c, r), cs))
 }
 
-import scala.util._
+
+
 def lexing(r: Rexp, s: String) : Try[Val] = Try(lex(r, s.toList))
 
 
@@ -218,7 +220,7 @@
   }
 }
 
-def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
+def lexing_simp(r: Rexp, s: String) : Try[Val] = Try(lex_simp(r, s.toList))
 
 
 // Some Tests
@@ -249,10 +251,11 @@
 val ALL = CHARS((c) => true)
 val reg = ALL.% ~ "a" ~ NTIMES(ALL, 3) ~ "bc"
 
-println(lexing(reg, "axaybzbc"))     // true
-println(lexing(reg, "aaaaxaybzbc"))  // true
-println(nullable(ders("axaybzbd".toList, reg)))     // false
-println(lexing(reg, "axaybzbd"))     // false
+println(lexing(reg, "axaybzbc"))                     // true
+println(lexing(reg, "aaaaxaybzbc"))                  // true
+
+println(nullable(ders("axaybzbd".toList, reg)))      // false
+println(lexing(reg, "axaybzbd"))                     // false
 
 
 
@@ -302,12 +305,12 @@
 println("prog0 test")
 
 val prog0 = """read n"""
-println(env(lexing_simp(WHILE_REGS, prog0)))
+println(env(lexing_simp(WHILE_REGS, prog0).get))
 
 println("prog1 test")
 
 val prog1 = """read  n; write (n)"""
-println(env(lexing_simp(WHILE_REGS, prog1)))
+println(env(lexing_simp(WHILE_REGS, prog1).get))
 
 
 // Bigger Test
@@ -327,7 +330,15 @@
 }"""
 
 println("prog2 test - tokens")
-println(env(lexing_simp(WHILE_REGS, prog2)))
+println(env(lexing_simp(WHILE_REGS, prog2).get))
+
+
+// replicate prog2
+
+println("prog2 replicated test")
+for (i <- 1 to 88 by 5) {
+  println(i + ": " + "%.5f".format(time_needed(2, lexing_simp(WHILE_REGS, prog2 * i))))
+}
 
 
 val prog3 = """
@@ -346,13 +357,9 @@
 """
 
 println("prog3 test - tokens")
-println(env(lexing_simp(WHILE_REGS, prog3)))
-
-println("prog2 replicated test")
+println(env(lexing_simp(WHILE_REGS, prog3).get))
 
-for (i <- 1 to 88) {
-  println(i + ": " + "%.5f".format(time_needed(2, lexing_simp(WHILE_REGS, prog2 * i))))
-}
+
 
 
 // Sulzmann's tests
@@ -377,7 +384,7 @@
 val reWord = CHARS("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789" contains _)
 
 val reWordStar = STAR(reWord)
-val reWordPlus = reWord ~ reWordStar
+val reWordPlus = PLUS(reWord)
 val optionSet1 = "-" | "+" | "."
 val optionSet2 = "-" | "."
 val atTheRate = "@"

--- a/thys/LexerExt.thy	Sat Mar 11 12:50:01 2017 +0000
+++ b/thys/LexerExt.thy	Sat Mar 11 19:33:38 2017 +0000
@@ -1159,12 +1159,12 @@
 next
   case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
   have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs"
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" "flat v = [] \<Longrightarrow> flat (Stars vs) = []"
        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
-  by (m etis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2)
+  by (metis Posix1(1) Posix_NMTIMES1.hyps(6) self_append_conv self_append_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1569,6 +1569,8 @@
         apply(blast)
         apply(simp)
         apply(simp add: der_correctness Der_def)
+        using Posix1a Prf_injval_flat list.distinct(1) apply auto[1]
+        apply(simp add: der_correctness Der_def)
         done
 next 
   case (PLUS r)