--- a/thys/Spec.thy	Sat Oct 27 21:36:29 2018 +0100
+++ b/thys/Spec.thy	Wed Jan 02 21:09:33 2019 +0000
@@ -163,7 +163,6 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-  apply(induct r)
 by (induct r) (auto simp add: Sequ_def) 
 
 lemma der_correctness:

--- a/thys/Sulzmann.thy	Sat Oct 27 21:36:29 2018 +0100
+++ b/thys/Sulzmann.thy	Wed Jan 02 21:09:33 2019 +0000
@@ -106,7 +106,7 @@
 | "intern ONE = AONE []"
 | "intern (CHAR c) = ACHAR [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
-                                     (fuse [S]  (intern r2))"
+                                (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
 | "intern (STAR r) = ASTAR [] (intern r)"
 
@@ -317,6 +317,42 @@
     done
 qed
 
+
+lemma
+  "[a, a, a, a] \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
+     (Stars [(Stars [Char a, Char a, Char a, Char a])])"
+  oops
+
+lemma
+  "([a,a] @ []) \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
+     (Stars [(Stars [Char a, Char a])])"
+  apply(rule Posix.intros)
+  defer
+  apply (simp add: Posix_STAR2)
+  apply(simp)
+  apply(auto)[1]
+  apply(rule_tac s="[a] @ [a]" in subst)
+  apply(simp)
+  apply(rule Posix_STAR1)
+  apply(rule Posix_CHAR)
+  apply(rule_tac s="[a] @ []" in subst)
+  apply(simp)
+  apply(rule Posix_STAR1)
+       apply(rule Posix_CHAR)
+      apply(rule Posix_STAR2)
+     apply(simp)
+    apply(auto)
+  done
+
+
+lemma "lexer (STAR(STAR(CHAR(a)))) [a, a] = XXX"
+  apply(simp)
+  oops
+
+
+
+
+
 fun simp where
   "simp (AALT bs a AZERO) = fuse bs (simp a)"
 | "simp (AALT bs AZERO a) = fuse bs (simp a)"
@@ -325,6 +361,18 @@
 | "simp a = a"
 
 
+
+
+
+
+
+definition blexers where
+ "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
+                decode (bmkeps (bders (intern r) s)) r else None"
+
 unused_thms
-  
+
+
+
+
 end
\ No newline at end of file