diff -r 454ced557605 -r 692911c0b981 thys3/src/PosixSpec.thy
--- a/thys3/src/PosixSpec.thy	Thu Jul 21 20:21:52 2022 +0100
+++ b/thys3/src/PosixSpec.thy	Thu Jul 21 20:22:35 2022 +0100
@@ -437,9 +437,9 @@
     \<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 (STAR r))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
-| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n;
-    \<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 - 1)))\<rbrakk>
-    \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; flat v \<noteq> [];
+    \<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 (n + 1) \<rightarrow> Stars (v # vs)"
 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
     \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs"  
 
@@ -458,7 +458,6 @@
 using assms
   apply(induct s r v rule: Posix.induct)
   apply(auto simp add: pow_empty_iff)
-  apply (metis Suc_pred concI lang_pow.simps(2))
   by (meson ex_in_conv set_empty)
 
 lemma Posix1a:
@@ -566,17 +565,17 @@
     by (meson in_set_zipE)
 next
   case (Posix_NTIMES1 s1 r v s2 n vs)
-  have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
-       "\<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 - 1 )))" by fact+
-  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')"
+  have "(s1 @ s2) \<in> NTIMES r (n + 1) \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r n \<rightarrow> Stars vs" "flat v \<noteq> []"
+       "\<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))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
     using Posix1(1) apply fastforce
-    apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2)
+    apply (metis L.simps(7) Posix1(1) append.left_neutral append.right_neutral)
   using Posix1(2) by blast
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
-            "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+            "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 qed
 
@@ -590,8 +589,8 @@
   shows "v \<in> LV r s"
   using assms unfolding LV_def
   apply(induct rule: Posix.induct)
-   apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a)
-   apply (smt (verit, best) One_nat_def Posix1a Posix_NTIMES1 L.simps(7))
+          apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a)
+  apply (smt (verit, ccfv_SIG) L.simps(7) Posix1a Posix_NTIMES1 Suc_eq_plus1)
   using Posix1a Posix_NTIMES2 by blast