# HG changeset patch
# User cu
# Date 1507628444 -3600
# Node ID 424bdcd01016b740c408ab85210b40ec6289cda3
# Parent  42268a284ea6274b7327a30c371099bf5c0a91ab
updated

diff -r 42268a284ea6 -r 424bdcd01016 thys/LexerExt.thy
--- 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:
diff -r 42268a284ea6 -r 424bdcd01016 thys/PositionsExt.thy
--- a/thys/PositionsExt.thy	Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/PositionsExt.thy	Tue Oct 10 10:40:44 2017 +0100
@@ -940,10 +940,123 @@
     qed      
 next
   case (Posix_NMTIMES2 vs r n m v2) 
-  then show "Stars vs :\<sqsubseteq>val v2" sorry
+  then show "Stars vs :\<sqsubseteq>val v2" 
+    apply(auto simp add: LV_def)
+    apply(erule Prf_elims)
+     apply(simp)
+     apply(rule PosOrd_eq_Stars_zipI) 
+       apply(auto)
+     apply (meson in_set_zipE)
+    by (metis Posix1(2) flats_empty)
 next
-  case (Posix_NMTIMES1 s1 r v s2 n m vs v2) 
-  then show "Stars (v # vs) :\<sqsubseteq>val v2" sorry      
+  case (Posix_NMTIMES1 s1 r v s2 n m vs v3) 
+  have "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" by fact+
+  then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
+  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  have cond: "\<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 (NMTIMES r (n - 1) (m - 1)))" by fact
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (NMTIMES r n m) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NMTIMES r (n - 1) (m - 1)"
+    "flats (v3a # vs3) = s1 @ s2"
+  | (Empty) "v3 = Stars []" 
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf.cases)
+             apply(auto)  
+  apply(case_tac n)
+    apply(auto intro: Prf.intros)
+   apply(case_tac vs1)
+    apply(auto intro: Prf.intros)
+   apply (simp add: as1(1) cond2 flats_empty)
+   apply (simp add: Prf.intros(11))
+  apply(case_tac n)
+   apply(simp)
+  using Posix_NMTIMES1.hyps(6) apply blast
+  apply(simp)
+  apply(case_tac vs)
+   apply(auto)
+  by (simp add: Prf.intros(12))
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars)
+      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+        by (simp add: sprefix_list_def append_eq_conv_conj)
+      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
+        using PosOrd_spreI as1(1) NonEmpty(4) by blast
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2)" 
+        using NonEmpty(2,3) by (auto simp add: LV_def)
+      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
+         unfolding PosOrd_ex_eq_def by auto     
+      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+        unfolding  PosOrd_ex_eq_def
+        using PosOrd_StarsI PosOrd_StarsI2 by auto 
+      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+    next 
+      case Empty
+      have "v3 = Stars []" by fact
+      then show "Stars (v # vs) :\<sqsubseteq>val v3"
+      unfolding PosOrd_ex_eq_def using cond2
+      by (simp add: PosOrd_shorterI)
+  qed        
+next
+  case (Posix_NMTIMES3 s1 r v s2 m vs v3) 
+  have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact+
+  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
+  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  have cond: "\<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 (UPNTIMES r (m - 1)))" by fact
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (NMTIMES r 0 m) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (m - 1)" 
+    "flats (v3a # vs3) = s1 @ s2"
+  | (Empty) "v3 = Stars []"
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf.cases)
+  apply(auto)
+  apply(case_tac vs)
+   apply(auto intro: Prf.intros)
+  by (simp add: Prf.intros(7) as1(1) cond2)
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        apply(simp)
+        apply(simp add: append_eq_append_conv2)
+        apply(auto)
+        by (metis L_flat_Prf1 One_nat_def cond flat_Stars)
+      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+        by (simp add: sprefix_list_def append_eq_conv_conj)
+      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
+        using PosOrd_spreI as1(1) NonEmpty(4) by blast
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (m - 1)) s2)" 
+        using NonEmpty(2,3) by (auto simp add: LV_def)
+      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
+         unfolding PosOrd_ex_eq_def by auto     
+      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+        unfolding  PosOrd_ex_eq_def
+        using PosOrd_StarsI PosOrd_StarsI2 by auto 
+      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+    next 
+      case Empty
+      have "v3 = Stars []" by fact
+      then show "Stars (v # vs) :\<sqsubseteq>val v3"
+      unfolding PosOrd_ex_eq_def using cond2
+      by (simp add: PosOrd_shorterI)
+  qed          
 qed
 
 
diff -r 42268a284ea6 -r 424bdcd01016 thys/ROOT
--- a/thys/ROOT	Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/ROOT	Tue Oct 10 10:40:44 2017 +0100
@@ -1,11 +1,13 @@
 session "Lex" = HOL +
   theories [document = false]
         "Spec"
+	"SpecExt"
         "Lexer"
         "LexerExt"
         "Simplifying"
         (*"Sulzmann"*) 
         "Positions"
+	"PositionsExt"
         "Exercises"
 
 session Paper in "Paper" = Lex +
diff -r 42268a284ea6 -r 424bdcd01016 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/SpecExt.thy	Tue Oct 10 10:40:44 2017 +0100
@@ -1173,9 +1173,12 @@
     \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (v # vs)"  
 | Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk>
     \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs"  
-| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; 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 r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))\<rbrakk>
-    \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"  
+| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 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 r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (v # vs)"  
+| Posix_NMTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 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 r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (v # vs)"    
   
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -1220,9 +1223,14 @@
    apply(rule_tac x="Suc x" in bexI)
     apply(auto simp add: Sequ_def)[2]
    apply(simp)
-  apply(simp)
-  by (simp add: Star.step Star_Pow)
-  
+    apply(simp)
+    apply(clarify)
+     apply(rule_tac x="Suc x" in bexI)
+    apply(auto simp add: Sequ_def)[2]
+   apply(simp)
+  apply(simp add: Star.step Star_Pow)
+done  
+    
 text {*
   Our Posix definition determines a unique value.
 *}
@@ -1396,12 +1404,59 @@
   ultimately show "Stars (v # vs) = v2" by auto     
 next    
   case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
-  then show "Stars (v # vs) = v2"
-    sorry
+  have "(s1 @ s2) \<in> NMTIMES r n m \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" 
+       "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 r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" 
+    "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+    using Posix1(1) Posix1(2) apply blast 
+     apply(case_tac n)
+      apply(simp)
+     apply(simp)
+       apply(case_tac m)
+      apply(simp)
+     apply(simp)
+    apply(drule_tac x="va" in meta_spec)
+    apply(drule_tac x="vs" in meta_spec)
+    apply(simp)
+     apply(drule meta_mp)
+      apply (smt L.simps(10) Posix1(1) Posix1(2) Posix_NMTIMES1.hyps(4) UN_E append.right_neutral
+             append_eq_append_conv2 diff_Suc_1 val.inject(5))
+     apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
+    by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)      
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto     
 next
   case (Posix_NMTIMES2 vs r n m v2)
   then show "Stars vs = v2"
-    sorry
+    apply(erule_tac Posix_elims)
+      apply(simp)
+      apply(rule List_eq_zipI)
+       apply(auto)
+      apply (meson in_set_zipE)
+    apply (simp add: Posix1(2))
+    apply(erule_tac Posix_elims)
+     apply(auto)
+    apply (simp add: Posix1(2))+
+    done  
+next
+  case (Posix_NMTIMES3 s1 r v s2 m vs v2)
+   have "(s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "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 r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1 )))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs')"
+    apply(cases) apply (auto simp add: append_eq_append_conv2)
+    using Posix1(2) apply blast
+    apply (smt L.simps(7) Posix1(1) UN_E append_eq_append_conv2)
+    by (metis One_nat_def Posix1(1) Posix_NMTIMES3.hyps(7) append.right_neutral append_Nil)
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> UPNTIMES r (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto  
 qed
 
 
@@ -1441,9 +1496,52 @@
       apply(simp)
   apply(rule Prf.intros)  
        apply(simp)
+     apply(simp)
+  (* NTIMES *)
+   prefer 4
+   apply(simp)
+   apply(case_tac n)
     apply(simp)
+   apply(simp)
+   apply(clarify)
+   apply(rotate_tac 5)
+   apply(erule Prf_elims)
+   apply(simp)
+  apply(subst append.simps(2)[symmetric])
+      apply(rule Prf.intros) 
+        apply(simp)
+       apply(simp)
+   apply(simp)
+  prefer 4
+  apply(simp)
+  apply (metis Prf.intros(8) length_removeAll_less less_irrefl_nat removeAll.simps(1) self_append_conv2)
   (* NMTIMES *)
-  sorry
-    
+  apply(simp)
+  apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
+  apply(simp)
+  apply(clarify)
+  apply(rotate_tac 6)
+  apply(erule Prf_elims)
+   apply(simp)
+  apply(subst append.simps(2)[symmetric])
+      apply(rule Prf.intros) 
+        apply(simp)
+       apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(rule Prf.intros) 
+        apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(clarify)
+  apply(rotate_tac 6)
+  apply(erule Prf_elims)
+   apply(simp)
+      apply(rule Prf.intros) 
+        apply(simp)
+       apply(simp)
+  apply(simp)
+done    
   
 end
\ No newline at end of file