diff -r 4c02878e2fe0 -r 17c079699ea0 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Tue Feb 28 00:26:34 2017 +0000
+++ b/thys/LexerExt.thy	Tue Feb 28 13:35:12 2017 +0000
@@ -159,6 +159,7 @@
 | STAR rexp
 | UPNTIMES rexp nat
 | NTIMES rexp nat
+| FROMNTIMES rexp nat
 
 section {* Semantics of Regular Expressions *}
  
@@ -173,7 +174,7 @@
 | "L (STAR r) = (L r)\<star>"
 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"
 | "L (NTIMES r n) = ((L r) \<up> n)"
-
+| "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
 
 section {* Nullable, Derivatives *}
 
@@ -188,6 +189,7 @@
 | "nullable (STAR r) = True"
 | "nullable (UPNTIMES r n) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
+| "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -205,7 +207,8 @@
 | "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 (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -306,8 +309,17 @@
 apply(simp only: L.simps der.simps)
 apply(simp)
 apply(rule impI)
-by (simp add: Der_Pow_subseteq sup_absorb1)
-
+apply (simp add: Der_Pow_subseteq sup_absorb1)
+(* 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 only: der.simps)
+apply(simp only: L.simps)
+apply(simp add: Der_UNION)
+by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
@@ -379,14 +391,10 @@
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 | "\<turnstile> Void : ONE"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
-| "\<turnstile> Stars [] : UPNTIMES r 0"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)"
-| "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)"
-| "\<turnstile> Stars [] : NTIMES r 0"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : NTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : NTIMES r (Suc n)"
-
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"
 
 inductive_cases Prf_elims:
   "\<turnstile> v : ZERO"
@@ -396,68 +404,39 @@
   "\<turnstile> v : CHAR c"
 (*  "\<turnstile> vs : STAR r"*)
 
+lemma Prf_STAR:
+   assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"  
+   shows "concat (map flat vs) \<in> L r\<star>"
+using assms 
+apply(induct vs)
+apply(auto)
+done
+
+lemma Prf_Pow:
+  assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" 
+  shows "concat (map flat vs) \<in> L r \<up> length vs"
+using assms
+apply(induct vs)
+apply(auto simp add: Sequ_def)
+done
+
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
 apply(induct v r rule: Prf.induct)
 apply(auto simp add: Sequ_def)
-apply(rotate_tac 2)
-apply(rule_tac x="Suc x" in bexI)
-apply(auto simp add: Sequ_def)[2]
-done
-
-lemma Prf_Stars:
-  assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
-  shows "\<turnstile> Stars vs : STAR r"
-using assms
-by(induct vs) (auto intro: Prf.intros)
-
-lemma Prf_Stars_NTIMES:
-  assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
-  shows "\<turnstile> Stars vs : NTIMES r n"
-using assms
-apply(induct vs arbitrary: n) 
-apply(auto intro: Prf.intros)
-done
-
-lemma Prf_Stars_UPNTIMES:
-  assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
-  shows "\<turnstile> Stars vs : UPNTIMES r n"
-using assms
-apply(induct vs arbitrary: n) 
-apply(auto intro: Prf.intros)
-done
-
-lemma Prf_UPNTIMES_bigger:
-  assumes "\<turnstile> Stars vs : UPNTIMES r n" "n \<le> m" 
-  shows "\<turnstile> Stars vs : UPNTIMES r m"
-using assms
-apply(induct m arbitrary:)
-apply(auto)
-using Prf.intros(10) le_Suc_eq by blast
-
-lemma UPNTIMES_Stars:
- assumes "\<turnstile> v : UPNTIMES r n"
- shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n"
-using assms
-apply(induct n arbitrary: v)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)
-using le_SucI by blast
-
-lemma NTIMES_Stars:
- assumes "\<turnstile> v : NTIMES r n"
- shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"
-using assms
-apply(induct n arbitrary: v)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)
+apply(rule Prf_STAR)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
+apply(rule Prf_Pow)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
 done
 
 lemma Star_string:
@@ -502,14 +481,6 @@
 apply(simp)
 done
 
-lemma L_flat_Prf1:
-  assumes "\<turnstile> v : r" shows "flat v \<in> L r"
-using assms
-apply(induct)
-apply(auto simp add: Sequ_def)
-apply(rule_tac x="Suc x" in bexI)
-apply(auto simp add: Sequ_def)[2]
-done
 
 lemma L_flat_Prf2:
   assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
@@ -523,34 +494,38 @@
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply (simp add: Prf_Stars)
-apply(drule Star_string)
-apply(auto)
-apply(rule Star_val)
-apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+using Star_string Star_val apply force
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(drule_tac n="length vs" in Prf_Stars_UPNTIMES)
+apply(rule Prf.intros)
 apply(simp)
-using Prf_UPNTIMES_bigger apply blast
-apply(drule Star_Pow)
-apply(auto)
-using Star_val_length apply blast
+apply(simp)
+using Star_Pow Star_val_length apply blast
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(rule Prf_Stars_NTIMES)
+apply(rule Prf.intros)
 apply(simp)
 apply(simp)
-using Star_Pow Star_val_length by blast
-
+using Star_Pow Star_val_length apply blast
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+using Star_Pow Star_val_length apply blast
+done
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
-using L_flat_Prf1 L_flat_Prf2 by blast
+using Prf_flat_L L_flat_Prf2 by blast
 
 
 section {* Sulzmann and Lu functions *}
@@ -564,7 +539,7 @@
 | "mkeps(STAR r) = Stars []"
 | "mkeps(UPNTIMES r n) = Stars []"
 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
-
+| "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
@@ -577,7 +552,7 @@
 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
-
+| "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 
 section {* Mkeps, injval *}
 
@@ -587,13 +562,6 @@
 using assms
 apply(induct r rule: mkeps.induct) 
 apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger apply blast
-apply(case_tac n)
-apply(auto)
-apply(rule Prf.intros)
-apply(rule Prf_Stars_NTIMES)
-apply(simp)
-apply(simp)
 done
 
 lemma mkeps_flat:
@@ -612,10 +580,9 @@
 (* STAR *)
 apply(rotate_tac 2)
 apply(erule Prf.cases)
-apply(simp_all)[7]
+apply(simp_all)
 apply(auto)
-apply (metis Prf.intros(6) Prf.intros(7))
-apply (metis Prf.intros(7))
+using Prf.intros(6) apply auto[1]
 (* UPNTIMES *)
 apply(case_tac x2)
 apply(simp)
@@ -624,12 +591,11 @@
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
-apply(drule UPNTIMES_Stars)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(clarify)
-apply(simp)
-apply(rule Prf.intros(9))
-apply(simp)
-using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger apply blast
+using Prf.intros(7) apply auto[1]
 (* NTIMES *)
 apply(case_tac x2)
 apply(simp)
@@ -638,12 +604,32 @@
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
-apply(drule NTIMES_Stars)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(clarify)
+using Prf.intros(8) apply auto[1]
+(* FROMNTIMES *)
+apply(case_tac x2)
 apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-using Prf_Stars_NTIMES by blast
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+using Prf.intros(9) apply auto[1]
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+using Prf.intros(9) by auto
+
 
 lemma Prf_injval_flat:
   assumes "\<turnstile> v : der c r" 
@@ -655,16 +641,21 @@
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)
-apply(drule UPNTIMES_Stars)
-apply(clarify)
-apply(simp)
-apply(drule NTIMES_Stars)
-apply(clarify)
-apply(simp)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 done
 
 
-
 section {* Our Alternative Posix definition *}
 
 inductive 
@@ -689,7 +680,10 @@
     \<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 (NTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []"
-
+| 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 []"
 
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -707,6 +701,8 @@
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
+apply(rule_tac x="Suc x" in bexI)
+apply(auto simp add: Sequ_def)
 done
 
 
@@ -716,20 +712,29 @@
 using assms
 apply(induct s r v rule: Posix.induct)
 apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger by blast
-
-lemma Posix_NTIMES_length:
-  assumes "s \<in> NTIMES r n \<rightarrow> Stars vs"
-  shows "length vs = n"
-using assms
-using NTIMES_Stars Posix1a val.inject(5) by blast
-
-lemma Posix_UPNTIMES_length:
-  assumes "s \<in> UPNTIMES r n \<rightarrow> Stars vs"
-  shows "length vs \<le> n"
-using assms
-using Posix1a UPNTIMES_Stars val.inject(5) by blast
-
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (smt Posix_UPNTIMES2 Posix_elims(2) Prf.simps le_0_eq le_Suc_eq length_0_conv nat_induct nullable.simps(3) nullable.simps(7) rexp.distinct(61) rexp.distinct(67) rexp.distinct(69) rexp.inject(5) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (smt Prf.simps rexp.distinct(63) rexp.distinct(67) rexp.distinct(71) rexp.inject(6) val.distinct(17) val.distinct(9) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+using Prf.simps by blast
 
 lemma  Posix_NTIMES_mkeps:
   assumes "[] \<in> r \<rightarrow> mkeps r"
@@ -744,6 +749,20 @@
 apply(rule assms)
 done
 
+lemma  Posix_FROMNTIMES_mkeps:
+  assumes "[] \<in> r \<rightarrow> mkeps r"
+  shows "[] \<in> FROMNTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"
+apply(induct n)
+apply(simp)
+apply (rule Posix_FROMNTIMES2)
+apply(simp)
+apply(subst append_Nil[symmetric])
+apply (rule Posix_FROMNTIMES1)
+apply(auto)
+apply(rule assms)
+done
+
+
 lemma Posix_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
@@ -756,8 +775,21 @@
 apply(case_tac n)
 apply(simp)
 apply (simp add: Posix_NTIMES2)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
 apply(rule Posix_NTIMES_mkeps)
 apply(simp)
+apply(case_tac n)
+apply(simp)
+apply (simp add: Posix_FROMNTIMES2)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule Posix_FROMNTIMES_mkeps)
+apply(simp)
 done
 
 
@@ -861,8 +893,58 @@
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<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)
+next
+  case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
+  have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" 
+       "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))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  using Posix1(1) apply fastforce
+  by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2)
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
 qed
 
+lemma NTIMES_Stars:
+ assumes "\<turnstile> v : NTIMES r n"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
+lemma UPNTIMES_Stars:
+ assumes "\<turnstile> v : UPNTIMES r n"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
+lemma FROMNTIMES_Stars:
+ assumes "\<turnstile> v : FROMNTIMES r n"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
 
 lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v"
@@ -1025,7 +1107,7 @@
         apply(simp)
         using Posix_elims(1) apply blast
         apply(simp)
-        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)        
         by (metis Posix1a UPNTIMES_Stars)
     then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" 
     proof (cases)
@@ -1087,6 +1169,61 @@
           done
         then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp)
     qed
+next 
+  case (FROMNTIMES r n)
+  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 (FROMNTIMES r n) \<rightarrow> v" by fact
+  then consider
+        (null) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "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"
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<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 m))" 
+        apply(case_tac n)
+        apply(simp)
+        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+        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)
+        defer
+        using Pow_in_Star apply blast
+        apply (meson Posix_FROMNTIMES2 append_is_Nil_conv self_append_conv)
+        sorry
+    then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" 
+    proof (cases)
+      case cons
+        have "n = Suc m" by fact
+        moreover
+          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> FROMNTIMES r m \<rightarrow> Stars vs" by fact
+        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 (FROMNTIMES r m))" 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 (FROMNTIMES r m))" 
+            by (simp add: der_correctness Der_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" 
+          apply(rule_tac Posix.intros(12))
+          apply(simp_all)
+          done
+        then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
+    qed
 qed