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