Binary file Literature/automata-explosion-gpu.pdf has changed

Binary file Literature/automata-explosion2.pdf has changed

Binary file Literature/regex-low-lewel-code-verify.pdf has changed

--- a/progs/scala/re-ext.scala	Wed Mar 08 10:32:51 2017 +0000
+++ b/progs/scala/re-ext.scala	Sat Mar 11 12:50:01 2017 +0000
@@ -157,7 +157,8 @@
   case c::cs => inj(r, c, lex(der(c, r), cs))
 }
 
-def lexing(r: Rexp, s: String) : Val = lex(r, s.toList)
+import scala.util._
+def lexing(r: Rexp, s: String) : Try[Val] = Try(lex(r, s.toList))
 
 
 // some "rectification" functions for simplification
@@ -243,6 +244,18 @@
 println(lexing_simp((("" | "a") ~ ("c" | "ab")), "ab"))
 
 
+// Some more Tests
+//=================
+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
+
+
+
 
 // Two Simple Tests for the While Language
 //========================================

--- a/thys/LexerExt.thy	Wed Mar 08 10:32:51 2017 +0000
+++ b/thys/LexerExt.thy	Sat Mar 11 12:50:01 2017 +0000
@@ -781,11 +781,11 @@
     \<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 (NTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []"
-| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs;
+| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> 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 (FROMNTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow>  s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs"
-| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs;
+| Posix_NMTIMES1: "\<lbrakk>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))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow>  s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"
@@ -1164,7 +1164,7 @@
   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 (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2)
+  by (m etis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2)
   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+