# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1488289656 0
# Node ID 624b4154325b593614c2253e4167ac2974233973
# Parent  17c079699ea0a713cad68a93b6d40cd736a6c64b
FROMNTIMES not yet done

diff -r 17c079699ea0 -r 624b4154325b thys/LexerExt.thy
--- a/thys/LexerExt.thy	Tue Feb 28 13:35:12 2017 +0000
+++ b/thys/LexerExt.thy	Tue Feb 28 13:47:36 2017 +0000
@@ -1175,8 +1175,9 @@
   have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact
   then consider
         (null) v1 vs s1 s2 where 
+        "n = 0"
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
-        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)"
+        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" 
       | (cons) m v1 vs s1 s2 where 
         "n = Suc m"
@@ -1200,10 +1201,13 @@
         apply(drule_tac x="s1a @ s2a" in meta_spec)
         apply(simp)
         apply(drule meta_mp)
-        defer
+        apply(rule Posix.intros)
+        apply(simp)
+        apply(simp)
+        apply(simp)
+        apply(simp)
         using Pow_in_Star apply blast
-        apply (meson Posix_FROMNTIMES2 append_is_Nil_conv self_append_conv)
-        sorry
+        by (meson Posix_STAR2 append_is_Nil_conv self_append_conv)
     then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" 
     proof (cases)
       case cons
@@ -1223,6 +1227,11 @@
           apply(simp_all)
           done
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
+      next
+      case null
+      then show ?thesis
+      apply(simp)
+      sorry
     qed
 qed