diff -r a3134f7de065 -r 42268a284ea6 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/LexerExt.thy	Sun Oct 08 14:21:24 2017 +0100
@@ -170,7 +170,6 @@
      apply(simp add: Prf_injval_flat)
      apply(simp)
    apply(simp)
-  using Prf.intros(10) Prf_injval_flat apply auto
 done
 
 
@@ -190,15 +189,6 @@
       apply(auto)
   done
     
-lemma test:
-  assumes "s \<in> der c (FROMNTIMES r 0) \<rightarrow> v"
-  shows "XXX"
-using assms    
-  apply(simp)
-  apply(erule Posix_elims)
-  apply(drule FROMNTIMES_0)
-  apply(auto)
-oops    
 
 lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v" 
@@ -454,18 +444,15 @@
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
         "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))"
-     | (null)  v1 where 
-        "v = Seq v1 (Stars [])"  
-        "s \<in> der c r \<rightarrow> v1" "[] \<in> (FROMNTIMES r 0) \<rightarrow> (Stars [])" "n = 0"
+     | (null) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2"  "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" 
+        "s1 \<in> der c r \<rightarrow> v1" "n = 0"
+         "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
     (* here *)    
     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+    prefer 2
     apply(erule Posix_elims)
     apply(simp)
-    apply(case_tac "n = 0")
-     apply(simp)
-     apply(drule FROMNTIMES_0)
-     apply(simp)
-    using FROMNTIMES_0 Posix_mkeps apply force
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
     apply(drule_tac x="v1" in meta_spec)
@@ -473,13 +460,22 @@
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
      apply(simp add: der_correctness Der_def)
-     apply(case_tac "n = 0")
-      apply(simp)
-      apply(simp)
-      apply(rotate_tac 4)
+      apply(rotate_tac 5)
     apply(erule Posix_elims)
       apply(auto)[2]
-      done
+    apply(erule Posix_elims)
+      apply(simp)
+     apply blast
+    apply(erule Posix_elims)
+    apply(auto)
+      apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)      
+    apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+     apply(clarify)
+    apply simp
+      apply(rotate_tac 6)
+    apply(erule Posix_elims)
+      apply(auto)[2]
+    done
     then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v" 
     proof (cases)
       case cons
@@ -508,27 +504,27 @@
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
       next 
        case null
-          have "s \<in> der c r \<rightarrow> v1" by fact
-          then have "(c # s) \<in> r \<rightarrow> injval r c v1" using IH by simp
-        moreover
-          have "[] \<in> (FROMNTIMES r 0) \<rightarrow> Stars []" by fact
-        moreover 
-          have "(c # s) \<in> r \<rightarrow> injval r c v1" by fact 
-          then have "flat (injval r c v1) = (c # s)" by (rule Posix1)
+          have "s1 \<in> der c r \<rightarrow> v1" by fact
+          then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+          moreover 
+            have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
+          moreover 
+          have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
+          then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
           then have "flat (injval r c v1) \<noteq> []" by simp
+          moreover
+             moreover 
+          have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
+          then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
+            by (simp add: der_correctness Der_def)
         ultimately 
-        have "((c # s) @ []) \<in> FROMNTIMES r 1 \<rightarrow> Stars [injval r c v1]" 
-           apply (rule_tac Posix.intros)
-              apply(simp_all)
+        have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" 
+           apply (rule_tac Posix.intros) back
+             apply(simp_all)
            done
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null 
           apply(simp)
-          apply(erule Posix_elims)
-           apply(auto)
-           apply(rotate_tac 6) 
-          apply(drule FROMNTIMES_0)
-          apply(simp)  
-            sorry
+          done  
       qed  
   next
     case (NMTIMES x1 x2 m s v)