--- a/thys/LexerExt.thy	Tue Feb 28 13:47:36 2017 +0000
+++ b/thys/LexerExt.thy	Tue Feb 28 23:40:37 2017 +0000
@@ -207,7 +207,7 @@
 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)"
 | "der c (NTIMES r 0) = ZERO"
 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
-| "der c (FROMNTIMES r 0) = SEQ (der c r) (STAR r)"
+| "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 
 fun 
@@ -313,9 +313,8 @@
 (* FROMNTIMES *)
 apply(simp only: der.simps)
 apply(simp only: L.simps)
-apply(subst Der_star[symmetric])
-apply(subst Star_def2)
-apply(auto)[1]
+apply(simp)
+using Der_star Star_def2 apply auto[1]
 apply(simp only: der.simps)
 apply(simp only: L.simps)
 apply(simp add: Der_UNION)
@@ -683,7 +682,8 @@
 | 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: "[] \<in> FROMNTIMES r 0 \<rightarrow> Stars []"
+| Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow>  s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs"
+
 
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -703,7 +703,7 @@
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
-done
+by (simp add: Star_in_Pow)
 
 
 lemma Posix1a:
@@ -734,7 +734,8 @@
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)
-using Prf.simps by blast
+using Prf.simps apply blast
+by (smt Prf.simps le0 rexp.distinct(61) rexp.distinct(63) rexp.distinct(65) rexp.inject(4) val.distinct(17) val.distinct(9) val.simps(29) val.simps(33) val.simps(35))
 
 lemma  Posix_NTIMES_mkeps:
   assumes "[] \<in> r \<rightarrow> mkeps r"
@@ -755,6 +756,7 @@
 apply(induct n)
 apply(simp)
 apply (rule Posix_FROMNTIMES2)
+apply (rule Posix.intros)
 apply(simp)
 apply(subst append_Nil[symmetric])
 apply (rule Posix_FROMNTIMES1)
@@ -781,9 +783,12 @@
 apply(auto)
 apply(rule Posix_NTIMES_mkeps)
 apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
 apply(case_tac n)
 apply(simp)
-apply (simp add: Posix_FROMNTIMES2)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
 apply(simp)
 apply(subst append.simps(1)[symmetric])
 apply(rule Posix.intros)
@@ -894,9 +899,13 @@
             "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 next
-  case (Posix_FROMNTIMES2 r v2)
-  have "[] \<in> FROMNTIMES r 0 \<rightarrow> v2" by fact
-  then show "Stars [] = v2" by cases (auto simp add: Posix1)
+  case (Posix_FROMNTIMES2 s r v1 v2)
+  have "s \<in> FROMNTIMES r 0 \<rightarrow> v2" "s \<in> STAR r \<rightarrow> Stars v1" 
+       "\<And>v3. s \<in> STAR r \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+
+  then show ?case 
+  apply(cases)
+  apply(auto)
+  done
 next
   case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
   have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" 
@@ -1177,7 +1186,7 @@
         (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> (STAR r) \<rightarrow> (Stars vs)"
+        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<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"
@@ -1190,24 +1199,10 @@
         defer
         apply (metis FROMNTIMES_Stars Posix1a)
         apply(rotate_tac 5)
-        apply(erule_tac Posix_elims(6))
-        apply(auto)
-        apply(drule_tac x="v1" in meta_spec)
-        apply(simp)
-        apply(drule_tac x="v # vs" in meta_spec)
-        apply(simp)
-        apply(drule_tac x="s1" in meta_spec)
-        apply(simp)
-        apply(drule_tac x="s1a @ s2a" in meta_spec)
-        apply(simp)
-        apply(drule meta_mp)
-        apply(rule Posix.intros)
-        apply(simp)
-        apply(simp)
-        apply(simp)
-        apply(simp)
-        using Pow_in_Star apply blast
-        by (meson Posix_STAR2 append_is_Nil_conv self_append_conv)
+        apply(erule Posix.cases)
+        apply(simp_all)
+        apply(clarify)
+        by (simp add: Posix_FROMNTIMES2)
     then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" 
     proof (cases)
       case cons
@@ -1229,9 +1224,20 @@
         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
+      then have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)"
+      apply(rule_tac Posix.intros)
+      apply(rule_tac Posix.intros)
+      apply(rule IH)
       apply(simp)
-      sorry
+      apply(rotate_tac 4)
+      apply(erule Posix.cases)
+      apply(simp_all)
+      apply (simp add: Posix1a Prf_injval_flat)
+      apply(simp only: Star_def2)
+      apply(simp only: der_correctness Der_def)
+      apply(simp)
+      done
+      then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp
     qed
 qed