--- a/thys/LexerExt.thy	Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/LexerExt.thy	Tue Oct 10 10:40:44 2017 +0100
@@ -447,8 +447,7 @@
      | (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 *)    
+         "\<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))"  
     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
     prefer 2
     apply(erule Posix_elims)
@@ -527,11 +526,100 @@
           done  
       qed  
   next
-    case (NMTIMES x1 x2 m s v)
-    then show ?case sorry      
+    case (NMTIMES r n m s v)
+      have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+  have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact
+  then consider
+      (cons) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs)" "0 < n" "n \<le> m"
+        "\<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 (NMTIMES r (n - 1) (m - 1)))"
+     | (null) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2"  "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs)" 
+        "s1 \<in> der c r \<rightarrow> v1" "n = 0" "0 < m"
+         "\<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 (UPNTIMES r (m - 1)))"  
+    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(subgoal_tac "\<exists>vss. v2 = Stars vss")
+    apply(clarify)
+    apply(drule_tac x="v1" in meta_spec)
+    apply(drule_tac x="vss" in meta_spec)
+    apply(drule_tac x="s1" in meta_spec)
+    apply(drule_tac x="s2" in meta_spec)
+     apply(simp add: der_correctness Der_def)
+      apply(rotate_tac 5)
+    apply(erule Posix_elims)
+      apply(auto)[2]
+    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> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v" 
+    proof (cases)
+      case cons
+          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> (NMTIMES r (n - 1) (m - 1)) \<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 
+          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 (NMTIMES r (n - 1) (m - 1)))" 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 (NMTIMES r (n - 1) (m - 1)))" 
+            by (simp add: der_correctness Der_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (injval r c v1 # vs)" 
+           apply (rule_tac Posix.intros)
+               apply(simp_all)
+              apply(case_tac n)
+            apply(simp)
+          using Posix_elims(1) NMTIMES.prems apply auto[1]
+          using cons(5) apply blast
+           apply(simp)
+            apply(rule cons)
+             done
+        then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using cons by(simp)
+      next 
+       case null
+          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> UPNTIMES r (m - 1) \<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 (UPNTIMES r (m - 1)))" 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 (UPNTIMES r (m - 1)))" 
+            by (simp add: der_correctness Der_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (injval r c v1 # vs)" 
+           apply (rule_tac Posix.intros) back
+              apply(simp_all)
+              apply(rule null)
+           done
+        then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null 
+          apply(simp)
+          done  
+      qed    
 qed
 
-
 section {* Lexer Correctness *}
 
 lemma lexer_correct_None: