diff --git a/thys/Posix-Lexing/Extensions/Derivatives3.thy b/thys/Posix-Lexing/Extensions/Derivatives3.thy
--- a/thys/Posix-Lexing/Extensions/Derivatives3.thy
+++ b/thys/Posix-Lexing/Extensions/Derivatives3.thy
@@ -1,62 +1,67 @@
 section "Derivatives of Extended Regular Expressions"
 
 (* Author: Christian Urban *)
 
 theory Derivatives3
 imports Regular_Exps3
 begin
 
 text\<open>This theory is based on work by Brozowski \cite{Brzozowski64}.\<close>
 
 subsection \<open>Brzozowski's derivatives of regular expressions\<close>
 
 fun
   deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
   "deriv c (Zero) = Zero"
 | "deriv c (One) = Zero"
 | "deriv c (Atom c') = (if c = c' then One else Zero)"
 | "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
 | "deriv c (Times r1 r2) = 
     (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
 | "deriv c (Star r) = Times (deriv c r) (Star r)"
-| "deriv c (NTimes r n) = (if n = 0 then Zero else Times (deriv c r) (NTimes r (n-1)))"
+| "deriv c (NTimes r n) = (if n = 0 then Zero else Times (deriv c r) (NTimes r (n - 1)))"
+| "deriv c (Upto r n) = (if n = 0 then Zero else Times (deriv c r) (Upto r (n - 1)))"
 
 fun 
   derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
   "derivs [] r = r"
 | "derivs (c # s) r = derivs s (deriv c r)"
 
 
 lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
 by (induction r) (auto)
 
 lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> atoms r"
 by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD])
 
 
 
 lemma deriv_pow [simp]:
   shows "Deriv c (A ^^ n) = (if n = 0 then {} else (Deriv c A) @@ (A ^^ (n - 1)))"
   apply(induct n arbitrary: A)
   apply(auto)
   by (metis Suc_pred concI_if_Nil2 conc_assoc conc_pow_comm lang_pow.simps(2))
 
 lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
-  by (induct r) (simp_all add: nullable_iff)
+  apply (induct r rule: lang.induct) 
+  apply(auto simp add: nullable_iff conc_UNION_distrib)
+  apply (metis IntI Suc_pred atMost_iff diff_Suc_1 mem_Collect_eq not_less_eq_eq zero_less_Suc)
+  apply(auto)
+  done    
   
 
 lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)"
 by (induct s arbitrary: r) (simp_all add: lang_deriv)
 
 text \<open>A regular expression matcher:\<close>
 
 definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
 "matcher r s = nullable (derivs s r)"
 
 lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
 by (induct s arbitrary: r)
    (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
 
 end
diff --git a/thys/Posix-Lexing/Extensions/Lexer3.thy b/thys/Posix-Lexing/Extensions/Lexer3.thy
--- a/thys/Posix-Lexing/Extensions/Lexer3.thy
+++ b/thys/Posix-Lexing/Extensions/Lexer3.thy
@@ -1,701 +1,794 @@
 (*  Title:       POSIX Lexing with Derivatives of Extended Regular Expressions
     Author:      Christian Urban <christian.urban at kcl.ac.uk>, 2022
     Maintainer:  Christian Urban <christian.urban at kcl.ac.uk>
 *) 
 
 theory Lexer3
   imports "Derivatives3"
 begin
 
 section \<open>Values\<close>
 
 datatype 'a val = 
   Void
 | Atm 'a
 | Seq "'a val" "'a val"
 | Right "'a val"
 | Left "'a val"
 | Stars "('a val) list"
 
 
 section \<open>The string behind a value\<close>
 
 fun 
   flat :: "'a val \<Rightarrow> 'a list"
 where
   "flat (Void) = []"
 | "flat (Atm c) = [c]"
 | "flat (Left v) = flat v"
 | "flat (Right v) = flat v"
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
 
 abbreviation
   "flats vs \<equiv> concat (map flat vs)"
 
 lemma flat_Stars [simp]:
  "flat (Stars vs) = concat (map flat vs)"
 by (induct vs) (auto)
 
 section \<open>Relation between values and regular expressions\<close>
 
 inductive 
   Prf :: "'a val \<Rightarrow> 'a rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : Times r1 r2"
 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : Plus r1 r2"
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : Plus r1 r2"
 | "\<turnstile> Void : One"
 | "\<turnstile> Atm c : Atom c"
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : Star r"
 | "\<lbrakk>\<forall>v \<in> set vs1. \<turnstile> v : r \<and> flat v \<noteq> []; 
     \<forall>v \<in> set vs2. \<turnstile> v : r \<and> flat v = []; 
     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (vs1 @ vs2) : NTimes r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : Upto r n"
 
 inductive_cases Prf_elims:
   "\<turnstile> v : Zero"
   "\<turnstile> v : Times r1 r2"
   "\<turnstile> v : Plus r1 r2"
   "\<turnstile> v : One"
   "\<turnstile> v : Atom c"
   "\<turnstile> vs : Star r"
   "\<turnstile> vs : NTimes r n"
+  "\<turnstile> vs : Upto r n"
 
 lemma Prf_NTimes_empty:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r \<and> flat v = []" 
   and     "length vs = n"
   shows "\<turnstile> Stars vs : NTimes r n"
   using assms
   by (metis Prf.intros(7) empty_iff eq_Nil_appendI list.set(1))
   
 
 lemma Seq_decomp:
   assumes "s \<in> A @@ B"
   shows "\<exists>s1 s2. s = s1 @ s2 \<and> s1 \<in> A \<and> s2 \<in> B"
   using assms
   by blast
 
 lemma NTimes_string:
   assumes "s \<in> A ^^ n"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> length ss = n"
 using assms
   apply(induct n arbitrary: s)
   apply(auto dest!: Seq_decomp)
   apply(drule_tac x="s2" in meta_spec)
   apply(auto)
   apply(rule_tac x="s1 # ss" in exI)
   apply(simp)
   done
 
 lemma pow_Prf:
   assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> A"
   shows "flats vs \<in> A ^^ (length vs)"
   using assms
   by (induct vs) (auto)
 
 lemma Star_string:
   assumes "s \<in> star A"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 using assms
 by (metis in_star_iff_concat subsetD)
 
 lemma Star_val:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
   shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> [])"
 using assms
 apply(induct ss)
 apply(auto)
 apply (metis empty_iff list.set(1))
 by (metis append.simps(1) flat.simps(7) flat_Stars set_ConsD)
 
 lemma Aux:
   assumes "\<forall>s\<in>set ss. s = []"
   shows "concat ss = []"
 using assms
 by (induct ss) (auto)
 
 lemma Pow_cstring:
   assumes "s \<in> A ^^ n"
   shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> 
          (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])"
 using assms
 apply(induct n arbitrary: s)
   apply(auto)[1]
   apply(auto dest!: Seq_decomp simp add: Seq_def)
   apply(drule_tac x="s2" in meta_spec)
   apply(simp)
 apply(erule exE)+
   apply(clarify)
 apply(case_tac "s1 = []")
 apply(simp)
 apply(rule_tac x="ss1" in exI)
 apply(rule_tac x="s1 # ss2" in exI)
 apply(simp)
 apply(rule_tac x="s1 # ss1" in exI)
 apply(rule_tac x="ss2" in exI)
   apply(simp)
   done
 
 lemma flats_cval:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
-  shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> 
+  shows "\<exists>vs1 vs2. flats vs1 = concat ss \<and> length (vs1 @ vs2) = length ss \<and> 
           (\<forall>v\<in>set vs1. \<turnstile> v : r \<and> flat v \<noteq> []) \<and>
           (\<forall>v\<in>set vs2. \<turnstile> v : r \<and> flat v = [])"
 using assms
 apply(induct ss rule: rev_induct)
 apply(rule_tac x="[]" in exI)+
 apply(simp)
 apply(simp)
-apply(clarify)
-apply(case_tac "flat v = []")
-apply(rule_tac x="vs1" in exI)
+  apply(clarify)
+  apply(case_tac "flat v = []")
+  apply(rule_tac x="vs1" in exI)
+  apply(simp)
 apply(rule_tac x="v#vs2" in exI)
 apply(simp)
-apply(rule_tac x="vs1 @ [v]" in exI)
+  apply(rule_tac x="vs1 @ [v]" in exI)
+  apply(simp)
 apply(rule_tac x="vs2" in exI)
 apply(simp)
-by (simp add: Aux)
+  done
+
+lemma flats_cval2:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+  shows "\<exists>vs. flats vs = concat ss \<and> length vs \<le> length ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> [])"
+  using assms
+  apply -
+  apply(drule flats_cval)
+  apply(auto)
+  done
+
 
 lemma Prf_flat_lang:
   assumes "\<turnstile> v : r" shows "flat v \<in> lang r"
 using assms
   apply (induct v r rule: Prf.induct) 
   apply (auto simp add: concat_in_star subset_eq lang_pow_add)
-  by (meson concI pow_Prf)
-    
+  apply(meson concI pow_Prf)
+  by (meson atMost_iff pow_Prf)
+  
+
 lemma L_flat_Prf2:
   assumes "s \<in> lang r" 
   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
 proof(induct r arbitrary: s)
   case (Star r s)
   have IH: "\<And>s. s \<in> lang r \<Longrightarrow> \<exists>v.\<turnstile> v : r \<and> flat v = s" by fact
   have "s \<in> lang (Star r)" by fact
   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> lang r \<and> s \<noteq> []"
     by (smt (z3) IH Prf_flat_lang Star_val imageE in_star_iff_concat lang.simps(6) list.set_map subset_iff)  
   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> []"
   using IH by (metis Star_val) 
   then show "\<exists>v. \<turnstile> v : Star r \<and> flat v = s"
   using Prf.intros(6) flat_Stars by blast
 next 
   case (Times r1 r2 s)
   then show "\<exists>v. \<turnstile> v : Times r1 r2 \<and> flat v = s"
   unfolding Seq_def lang.simps by (fastforce intro: Prf.intros)
 next
   case (Plus r1 r2 s)
   then show "\<exists>v. \<turnstile> v : Plus r1 r2 \<and> flat v = s"
   unfolding lang.simps by (fastforce intro: Prf.intros)
 next
   case (NTimes r n)
   have IH: "\<And>s. s \<in> lang r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
   have "s \<in> lang (NTimes r n)" by fact
   then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" 
     "\<forall>s \<in> set ss1. s \<in> lang r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> lang r \<and> s = []"
   using Pow_cstring by force
   then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" 
       "\<forall>v\<in>set vs1. \<turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<turnstile> v : r \<and> flat v = []"
-    using IH flats_cval 
+    using IH flats_cval  
   apply -
   apply(drule_tac x="ss1 @ ss2" in meta_spec)
   apply(drule_tac x="r" in meta_spec)
   apply(drule meta_mp)
   apply(simp)
   apply (metis Un_iff)
   apply(clarify)
   apply(drule_tac x="vs1" in meta_spec)
   apply(drule_tac x="vs2" in meta_spec)
   apply(simp)
   done
   then show "\<exists>v. \<turnstile> v : NTimes r n \<and> flat v = s"
-  using Prf.intros(7) flat_Stars by blast
+    using Prf.intros(7) flat_Stars by blast
+next
+  case (Upto r n)
+  have IH: "\<And>s. s \<in> lang r \<Longrightarrow> \<exists>v.\<turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> lang (Upto r n)" by fact
+  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> lang r \<and> s \<noteq> []" "length ss \<le> n"
+    apply(auto)
+    by (smt (verit) Nil_eq_concat_conv Pow_cstring concat_append le0 le_add_same_cancel1 le_trans length_append self_append_conv)    
+  then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
+  using IH flats_cval2
+  by (smt (verit, best) le_trans) 
+  then show "\<exists>v. \<turnstile> v : Upto r n \<and> flat v = s"
+  by (meson Prf.intros(8) flat_Stars) 
 qed (auto intro: Prf.intros)
 
 lemma L_flat_Prf:
   "lang r = {flat v | v. \<turnstile> v : r}"
   using L_flat_Prf2 Prf_flat_lang by blast
 
 
 section \<open>Sulzmann and Lu functions\<close>
 
 fun 
   mkeps :: "'a rexp \<Rightarrow> 'a val"
 where
   "mkeps(One) = Void"
 | "mkeps(Times r1 r2) = Seq (mkeps r1) (mkeps r2)"
 | "mkeps(Plus r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 | "mkeps(Star r) = Stars []"
-| "mkeps(NTimes r n) = Stars (replicate n (mkeps r))"  
+| "mkeps(Upto r n) = Stars []"
+| "mkeps(NTimes r n) = Stars (replicate n (mkeps r))"
+
 
 fun injval :: "'a rexp \<Rightarrow> 'a \<Rightarrow> 'a val \<Rightarrow> 'a val"
 where
   "injval (Atom d) c Void = Atm d"
 | "injval (Plus r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (Plus r1 r2) c (Right v2) = Right(injval r2 c v2)"
 | "injval (Times r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 | "injval (Times r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 | "injval (Times r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 | "injval (Star r) 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 (Upto r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
 
 section \<open>Mkeps, injval\<close>
 
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
 using assms
   by (induct rule: mkeps.induct) (auto)
 
 lemma mkeps_nullable:
   assumes "nullable r" 
   shows "\<turnstile> mkeps r : r"
 using assms
   apply (induct r) 
   apply (auto intro: Prf.intros split: if_splits)
   apply (metis Prf.intros(7) append_Nil2 in_set_replicate list.size(3) replicate_0)
   apply(rule Prf_NTimes_empty)
   apply(auto simp add: mkeps_flat)
   done
 
 lemma Prf_injval_flat:
   assumes "\<turnstile> v : deriv c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct c r arbitrary: v rule: deriv.induct)
 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
 lemma Prf_injval:
   assumes "\<turnstile> v : deriv c r" 
   shows "\<turnstile> (injval r c v) : r"
 using assms
 apply(induct r arbitrary: c v rule: rexp.induct)
 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
 (* Star *)
 apply (simp add: Prf_injval_flat)
 (* NTimes *)
   apply(case_tac x2)
     apply(simp)
   apply(simp)
   apply(subst append.simps(2)[symmetric])
   apply(rule Prf.intros)
   apply(auto simp add: Prf_injval_flat)
   done
 
 section \<open>Our Alternative Posix definition\<close>
 
 inductive 
   Posix :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
   Posix_One: "[] \<in> One \<rightarrow> Void"
 | Posix_Atom: "[c] \<in> (Atom c) \<rightarrow> (Atm c)"
 | Posix_Plus1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Left v)"
 | Posix_Plus2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> lang r1\<rbrakk> \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Right v)"
 | Posix_Times: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
     \<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> lang r1 \<and> s\<^sub>4 \<in> lang r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (Times r1 r2) \<rightarrow> (Seq v1 v2)"
 | Posix_Star1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> Star r \<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> lang r \<and> s\<^sub>4 \<in> lang (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> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NTimes r n \<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"  
+    \<Longrightarrow> [] \<in> NTimes r n \<rightarrow> Stars vs" 
+| Posix_Upto1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> Upto 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> Upto r n \<rightarrow> Stars (v # vs)"
+| Posix_Upto2: "[] \<in> Upto r n \<rightarrow> Stars []"
 
 inductive_cases Posix_elims:
   "s \<in> Zero \<rightarrow> v"
   "s \<in> One \<rightarrow> v"
   "s \<in> Atom c \<rightarrow> v"
   "s \<in> Plus r1 r2 \<rightarrow> v"
   "s \<in> Times r1 r2 \<rightarrow> v"
   "s \<in> Star r \<rightarrow> v"
   "s \<in> NTimes r n \<rightarrow> v"
+  "s \<in> Upto r n \<rightarrow> v"
 
 lemma Posix1:
   assumes "s \<in> r \<rightarrow> v"
   shows "s \<in> lang r" "flat v = s"
 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)
+  apply(meson ex_in_conv set_empty)
+  by (metis Suc_pred atMost_iff concI lang_pow.simps(2) not_less_eq_eq)
+  
 
 lemma Posix1a:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
 using assms
   apply(induct s r v rule: Posix.induct)
   apply(auto intro: Prf.intros)
   apply (metis Prf.intros(6) Prf_elims(6) set_ConsD val.inject(5))
   prefer 2
   using Posix1(2) Prf_NTimes_empty apply blast
   apply(erule Prf_elims)
   apply(auto)
   apply(subst append.simps(2)[symmetric])
   apply(rule Prf.intros)
   apply(auto)
+  apply (metis (mono_tags, lifting) Prf.intros(8) Prf_elims(8) Suc_le_mono Suc_pred length_Cons set_ConsD val.inject(5))
   done
       
 
 lemma Posix_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(induct r)
 apply(auto intro: Posix.intros simp add: nullable_iff)
 apply(subst append.simps(1)[symmetric])
 apply(rule Posix.intros)
 apply(auto)
-  by (simp add: Posix_NTimes2 pow_empty_iff)
+apply(simp add: Posix_NTimes2 pow_empty_iff)
+done
 
 lemma List_eq_zipI:
   assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 = v2" 
   and "length vs1 = length vs2"
   shows "vs1 = vs2"  
  using assms
   apply(induct vs1 arbitrary: vs2)
    apply(case_tac vs2)
    apply(simp)    
    apply(simp)
    apply(case_tac vs2)
    apply(simp)
   apply(simp)
 done  
 
 
 text \<open>Our Posix definition determines a unique value.\<close>
 
 lemma Posix_determ:
   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
   shows "v1 = v2"
 using assms
 proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
   case (Posix_One v2)
   have "[] \<in> One \<rightarrow> v2" by fact
   then show "Void = v2" by cases auto
 next 
   case (Posix_Atom c v2)
   have "[c] \<in> Atom c \<rightarrow> v2" by fact
   then show "Atm c = v2" by cases auto
 next 
   case (Posix_Plus1 s r1 v r2 v2)
   have "s \<in> Plus r1 r2 \<rightarrow> v2" by fact
   moreover
   have "s \<in> r1 \<rightarrow> v" by fact
   then have "s \<in> lang r1" by (simp add: Posix1)
   ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto 
   moreover
   have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
   ultimately have "v = v'" by simp
   then show "Left v = v2" using eq by simp
 next 
   case (Posix_Plus2 s r2 v r1 v2)
   have "s \<in> Plus r1 r2 \<rightarrow> v2" by fact
   moreover
   have "s \<notin> lang r1" by fact
   ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" 
     by cases (auto simp add: Posix1) 
   moreover
   have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
   ultimately have "v = v'" by simp
   then show "Right v = v2" using eq by simp
 next
   case (Posix_Times s1 r1 v1 s2 r2 v2 v')
   have "(s1 @ s2) \<in> Times r1 r2 \<rightarrow> v'" 
        "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2"
        "\<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> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by fact+
   then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) by fastforce+
   moreover
   have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
             "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
   ultimately show "Seq v1 v2 = v'" by simp
 next
   case (Posix_Star1 s1 r v s2 vs v2)
   have "(s1 @ s2) \<in> Star r \<rightarrow> v2" 
        "s1 \<in> r \<rightarrow> v" "s2 \<in> Star r \<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> lang r \<and> s\<^sub>4 \<in> lang (Star r))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (Star r) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
   apply (metis Posix1(1) Posix_Star1.hyps(6) append_Nil append_Nil2)
   using Posix1(2) by blast
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> Star r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 next
   case (Posix_Star2 r v2)
   have "[] \<in> Star r \<rightarrow> v2" by fact
   then show "Stars [] = v2" by cases (auto simp add: Posix1)
 next
   case (Posix_NTimes2 vs r n v2)
   then show "Stars vs = v2"
     apply(erule_tac Posix_elims)
      apply(auto)
      apply (simp add: Posix1(2))    
     apply(rule List_eq_zipI)
      apply(auto)
     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> lang r \<and> s\<^sub>4 \<in> lang (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')"
   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)
   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+
   ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_Upto1 s1 r v s2 n vs)
+  have "(s1 @ s2) \<in> Upto r n \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (Upto r (n - 1)) \<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_Upto1.hyps(7) append_Nil2 self_append_conv2)
+  using Posix1(2) by blast
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> Upto r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_Upto2 r n)
+  have "[] \<in> Upto r n \<rightarrow> v2" by fact
+  then show "Stars [] = v2" by cases (auto simp add: Posix1)
 qed
 
 
 lemma Posix_injval:
   assumes "s \<in> (deriv c r) \<rightarrow> v"
   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
 proof(induct r arbitrary: s v rule: rexp.induct)
   case Zero
   have "s \<in> deriv c Zero \<rightarrow> v" by fact
   then have "s \<in> Zero \<rightarrow> v" by simp
   then have "False" by cases
   then show "(c # s) \<in> Zero \<rightarrow> (injval Zero c v)" by simp
 next
   case One
   have "s \<in> deriv c One \<rightarrow> v" by fact
   then have "s \<in> Zero \<rightarrow> v" by simp
   then have "False" by cases
   then show "(c # s) \<in> One \<rightarrow> (injval One c v)" by simp
 next 
   case (Atom d)
   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
   then show "(c # s) \<in> (Atom d) \<rightarrow> (injval (Atom d) c v)"
   proof (cases)
     case eq
     have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact
     then have "s \<in> One \<rightarrow> v" using eq by simp
     then have eqs: "s = [] \<and> v = Void" by cases simp
     show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" using eq eqs 
     by (auto intro: Posix.intros)
   next
     case ineq
     have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact
     then have "s \<in> Zero \<rightarrow> v" using ineq by simp
     then have "False" by cases
     then show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" by simp
   qed
 next
   case (Plus r1 r2)
   have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
   have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
   have "s \<in> deriv c (Plus r1 r2) \<rightarrow> v" by fact
   then have "s \<in> Plus (deriv c r1) (deriv c r2) \<rightarrow> v" by simp
   then consider (left) v' where "v = Left v'" "s \<in> deriv c r1 \<rightarrow> v'" 
               | (right) v' where "v = Right v'" "s \<notin> lang (deriv c r1)" "s \<in> deriv c r2 \<rightarrow> v'" 
               by cases auto
   then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v"
   proof (cases)
     case left
     have "s \<in> deriv c r1 \<rightarrow> v'" by fact
     then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
     then have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Left v')" by (auto intro: Posix.intros)
     then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using left by simp
   next 
     case right
     have "s \<notin> lang (deriv c r1)" by fact
     then have "c # s \<notin> lang r1" by (simp add: lang_deriv Deriv_def)
     moreover 
     have "s \<in> deriv c r2 \<rightarrow> v'" by fact
     then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
     ultimately have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Right v')" 
       by (auto intro: Posix.intros)
     then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using right by simp
   qed
 next
   case (Times r1 r2)
   have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
   have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
   have "s \<in> deriv c (Times r1 r2) \<rightarrow> v" by fact
   then consider 
         (left_nullable) v1 v2 s1 s2 where 
         "v = Left (Seq v1 v2)"  "s = s1 @ s2" 
         "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" 
         "\<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> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)"
       | (right_nullable) v1 s1 s2 where 
         "v = Right v1" "s = s1 @ s2"  
         "s \<in> deriv c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)"
       | (not_nullable) v1 v2 s1 s2 where
         "v = Seq v1 v2" "s = s1 @ s2" 
         "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" 
         "\<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> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)"
         by (force split: if_splits elim!: Posix_elims simp add: lang_deriv Deriv_def)   
   then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" 
     proof (cases)
       case left_nullable
       have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact
       then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 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> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" 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> lang r1 \<and> s\<^sub>4 \<in> lang r2)" 
          by (simp add: lang_deriv Deriv_def)
       ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
       then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using left_nullable by simp
     next
       case right_nullable
       have "nullable r1" by fact
       then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
       moreover
       have "s \<in> deriv c r2 \<rightarrow> v1" by fact
       then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
       moreover
       have "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)" by fact
       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" 
         using right_nullable 
         apply (auto simp add: lang_deriv Deriv_def append_eq_Cons_conv)
         by (metis concI mem_Collect_eq)
       ultimately have "([] @ (c # s)) \<in> Times r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
       by(rule Posix.intros)
       then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using right_nullable by simp
     next
       case not_nullable
       have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact
       then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 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> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" 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> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by (simp add: lang_deriv Deriv_def)
       ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable 
         by (rule_tac Posix.intros) (simp_all) 
       then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using not_nullable by simp
     qed
 next
   case (Star r)
   have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
   have "s \<in> deriv c (Star r) \<rightarrow> v" by fact
   then consider
       (cons) v1 vs s1 s2 where 
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (Star r) \<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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" 
         apply(auto elim!: Posix_elims(1-5) simp add: lang_deriv Deriv_def intro: Posix.intros)
         apply(rotate_tac 3)
         apply(erule_tac Posix_elims(6))
         apply (simp add: Posix.intros(6))
         using Posix.intros(7) by blast
     then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" 
     proof (cases)
       case cons
           have "s1 \<in> deriv 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> Star r \<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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" 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> lang r \<and> s\<^sub>4 \<in> lang (Star r))" 
             by (simp add: lang_deriv Deriv_def)
         ultimately 
         have "((c # s1) @ s2) \<in> Star r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
         then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" using cons by(simp)
       qed
 next
   case (NTimes r n)
   have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
   have "s \<in> deriv c (NTimes r n) \<rightarrow> v" by fact
   then consider
       (cons) v1 vs s1 s2 where 
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (NTimes r (n - 1)) \<rightarrow> (Stars vs)" "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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))" 
     apply(auto elim: Posix_elims simp add: lang_derivs Deriv_def intro: Posix.intros split: if_splits)
     apply(erule Posix_elims)
     apply(simp)
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
     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: lang_derivs Deriv_def)
     apply(erule Posix_elims)
      apply(auto)
       done
     then show "(c # s) \<in> (NTimes r n) \<rightarrow> injval (NTimes r n) c v" 
     proof (cases)
       case cons
           have "s1 \<in> deriv 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> (NTimes r (n - 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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (NTimes r (n - 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> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))"
             by (simp add: lang_deriv Deriv_def)
         ultimately 
         have "((c # s1) @ s2) \<in> NTimes r n \<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) NTimes.prems apply auto[1]
              apply(simp)
              done
         then show "(c # s) \<in> NTimes r n \<rightarrow> injval (NTimes r n) c v" using cons by(simp)
       qed  
+next
+  case (Upto r n)
+  have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+  have "s \<in> deriv c (Upto r n) \<rightarrow> v" by fact
+  then consider
+      (cons) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" "0 < n"
+        "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (Upto r (n - 1)) \<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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" 
+    apply(auto elim!: Posix_elims simp add: lang_deriv Deriv_def intro: Posix.intros)
+    apply(case_tac n)
+     apply(auto)
+    using Posix_elims(1) apply blast
+    apply(erule_tac Posix_elims)
+    apply(auto)
+    by (metis Posix1a Prf_elims(8) UN_E cons diff_Suc_1 lang.simps(8) zero_less_Suc)
+    then show "(c # s) \<in> Upto r n \<rightarrow> injval (Upto r n) c v" 
+    proof (cases)
+      case cons
+          have "s1 \<in> deriv 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> Upto r (n - 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> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Upto r (n - 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" 
+            by (simp add: lang_deriv Deriv_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> Upto r n \<rightarrow> Stars (injval r c v1 # vs)"
+          by (meson Posix_Upto1 cons(3)) 
+        then show "(c # s) \<in> Upto r n \<rightarrow> injval (Upto r n) c v" using cons by(simp)
+      qed
 qed
 
 
 section \<open>The Lexer by Sulzmann and Lu\<close>
 
 fun 
   lexer :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) option"
 where
   "lexer r [] = (if nullable r then Some(mkeps r) else None)"
 | "lexer r (c#s) = (case (lexer (deriv c r) s) of  
                     None \<Rightarrow> None
                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
 
 lemma lexer_correct_None:
   shows "s \<notin> lang r \<longleftrightarrow> lexer r s = None"
 apply(induct s arbitrary: r)
 apply(simp add: nullable_iff)
 apply(drule_tac x="deriv a r" in meta_spec)
 apply(auto simp add: lang_deriv Deriv_def)
 done
 
 lemma lexer_correct_Some:
   shows "s \<in> lang r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
 apply(induct s arbitrary: r)
 apply(auto simp add: Posix_mkeps nullable_iff)[1]
 apply(drule_tac x="deriv a r" in meta_spec)
 apply(simp add: lang_deriv Deriv_def)
 apply(rule iffI)
 apply(auto intro: Posix_injval simp add: Posix1(1))
 done 
 
 lemma lexer_correctness:
   shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
   and   "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
 apply(auto)
 using lexer_correct_None lexer_correct_Some apply fastforce
 using Posix1(1) Posix_determ lexer_correct_Some apply blast
 using Posix1(1) lexer_correct_None apply blast
 using lexer_correct_None lexer_correct_Some by blast
 
 
 
-
 end
diff --git a/thys/Posix-Lexing/Extensions/LexicalVals3.thy b/thys/Posix-Lexing/Extensions/LexicalVals3.thy
--- a/thys/Posix-Lexing/Extensions/LexicalVals3.thy
+++ b/thys/Posix-Lexing/Extensions/LexicalVals3.thy
@@ -1,248 +1,263 @@
 theory LexicalVals3
   imports Lexer3 "HOL-Library.Sublist"
 begin
 
 section \<open> Sets of Lexical Values \<close>
 
 text \<open>
   Shows that lexical values are finite for a given regex and string.
 \<close>
 
 definition
   LV :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) set"
 where  "LV r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
 
 lemma LV_simps:
   shows "LV Zero s = {}"
   and   "LV One s = (if s = [] then {Void} else {})"
   and   "LV (Atom c) s = (if s = [c] then {Atm c} else {})"
   and   "LV (Plus r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
   and   "LV (NTimes r 0) s = (if s = [] then {Stars []} else {})"
 unfolding LV_def
   apply(auto intro: Prf.intros elim: Prf.cases)
   by (simp add: Prf_NTimes_empty)
   
 
 abbreviation
   "Prefixes s \<equiv> {s'. prefix s' s}"
 
 abbreviation
   "Suffixes s \<equiv> {s'. suffix s' s}"
 
 abbreviation
   "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
 
 lemma Suffixes_cons [simp]:
   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
 by (auto simp add: suffix_def Cons_eq_append_conv)
 
 
 lemma finite_Suffixes: 
   shows "finite (Suffixes s)"
 by (induct s) (simp_all)
 
 lemma finite_SSuffixes: 
   shows "finite (SSuffixes s)"
 proof -
   have "SSuffixes s \<subseteq> Suffixes s"
    unfolding strict_suffix_def suffix_def by auto
   then show "finite (SSuffixes s)"
    using finite_Suffixes finite_subset by blast
 qed
 
 lemma finite_Prefixes: 
   shows "finite (Prefixes s)"
 proof -
   have "finite (Suffixes (rev s))" 
     by (rule finite_Suffixes)
   then have "finite (rev ` Suffixes (rev s))" by simp
   moreover
   have "rev ` (Suffixes (rev s)) = Prefixes s"
   unfolding suffix_def prefix_def image_def
    by (auto)(metis rev_append rev_rev_ident)+
   ultimately show "finite (Prefixes s)" by simp
 qed
 
 lemma LV_STAR_finite:
   assumes "\<forall>s. finite (LV r s)"
   shows "finite (LV (Star r) s)"
 proof(induct s rule: length_induct)
   fix s::"'a list"
   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (Star r) s')"
   then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (Star r) s')"
     by (force simp add: strict_suffix_def suffix_def) 
   define f where "f \<equiv> \<lambda>(v::'a val, vs). Stars (v # vs)"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
   define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (Star r) s2)"
   have "finite S1" using assms
     unfolding S1_def by (simp_all add: finite_Prefixes)
   moreover 
   with IH have "finite S2" unfolding S2_def
     by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
   ultimately 
   have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
   moreover 
   have "LV (Star r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
   unfolding S1_def S2_def f_def
   unfolding LV_def image_def prefix_def strict_suffix_def 
   apply(auto)
   apply(case_tac x)
   apply(auto elim: Prf_elims)
   apply(erule Prf_elims)
   apply(auto)
   apply(case_tac vs)
   apply(auto intro: Prf.intros)  
   apply(rule exI)
   apply(rule conjI)
   apply(rule_tac x="flat a" in exI)
   apply(rule conjI)
   apply(rule_tac x="flats list" in exI)
   apply(simp)
   apply(blast)
   apply(simp add: suffix_def)
   using Prf.intros(6) by blast  
   ultimately
   show "finite (LV (Star r) s)" by (simp add: finite_subset)
 qed  
 
 definition
   "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
 
 lemma finite_Stars_Append:
   assumes "finite Vs1" "finite Vs2"
   shows "finite (Stars_Append Vs1 Vs2)"
   using assms  
 proof -
   define UVs1 where "UVs1 \<equiv> Stars -` Vs1"
   define UVs2 where "UVs2 \<equiv> Stars -` Vs2"  
   from assms have "finite UVs1" "finite UVs2"
     unfolding UVs1_def UVs2_def
     by(simp_all add: finite_vimageI inj_on_def) 
   then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"
     by simp
   moreover 
     have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"
     unfolding Stars_Append_def UVs1_def UVs2_def by auto    
   ultimately show "finite (Stars_Append Vs1 Vs2)"   
     by simp
 qed 
 
 lemma LV_NTimes_5:
   "LV (NTimes r n) s \<subseteq> Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (NTimes r i) [])"
 apply(auto simp add: LV_def)
 apply(auto elim!: Prf_elims)
   apply(auto simp add: Stars_Append_def)
   apply(rule_tac x="vs1" in exI)
   apply(rule_tac x="vs2" in exI)  
   apply(auto)
     using Prf.intros(6) apply(auto)
       apply(rule_tac x="length vs2" in bexI)
     thm Prf.intros
       apply(subst append.simps(1)[symmetric])
     apply(rule Prf.intros)
       apply(auto)[1]
       apply(auto)[1]
      apply(simp)
     apply(simp)
       done
 
 lemma LV_NTIMES_3:
   shows "LV (NTimes r (Suc n)) [] = 
      (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTimes r n) [])))"
 unfolding LV_def
 apply(auto elim!: Prf_elims simp add: image_def)
 apply(case_tac vs1)
 apply(auto)
 apply(case_tac vs2)
 apply(auto)
 apply(subst append.simps(1)[symmetric])
 apply(rule Prf.intros)
 apply(auto)
 apply(subst append.simps(1)[symmetric])
 apply(rule Prf.intros)
 apply(auto)
   done 
 
 lemma finite_NTimes_empty:
   assumes "\<And>s. finite (LV r s)" 
   shows "finite (LV (NTimes r n) [])"
   using assms
   apply(induct n)
    apply(auto simp add: LV_simps)
   apply(subst LV_NTIMES_3)
   apply(rule finite_imageI)
   apply(rule finite_cartesian_product)
   using assms apply simp 
   apply(rule finite_vimageI)
   apply(simp)
   apply(simp add: inj_on_def)
   done
 
+lemma subseteq_Upto_Star:
+  shows "LV (Upto r n) s \<subseteq> LV (Star r) s"
+  apply(auto simp add: LV_def)
+  by (metis Prf.intros(6) Prf_elims(8))
+
 lemma LV_finite:
   shows "finite (LV r s)"
 proof(induct r arbitrary: s)
   case (Zero s) 
   show "finite (LV Zero s)" by (simp add: LV_simps)
 next
   case (One s)
   show "finite (LV One s)" by (simp add: LV_simps)
 next
   case (Atom c s)
   show "finite (LV (Atom c) s)" by (simp add: LV_simps)
 next 
   case (Plus r1 r2 s)
   then show "finite (LV (Plus r1 r2) s)" by (simp add: LV_simps)
 next 
   case (Times r1 r2 s)
   define f where "f \<equiv> \<lambda>(v1::'a val, v2). Seq v1 v2"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'"
   define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'"
   have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+
   then have "finite S1" "finite S2" unfolding S1_def S2_def
     by (simp_all add: finite_Prefixes finite_Suffixes)
   moreover
   have "LV (Times r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
     unfolding f_def S1_def S2_def 
     unfolding LV_def image_def prefix_def suffix_def
     apply (auto elim!: Prf_elims)
     by (metis (mono_tags, lifting) mem_Collect_eq)  
   ultimately 
   show "finite (LV (Times r1 r2) s)"
     by (simp add: finite_subset)
 next
   case (Star r s)
   then show "finite (LV (Star r) s)" by (simp add: LV_STAR_finite)
 next
   case (NTimes r n s)
   have "\<And>s. finite (LV r s)" by fact
   then have "finite (Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (NTimes r i) []))" 
     apply(rule_tac finite_Stars_Append)
      apply (simp add: LV_STAR_finite)
     using finite_NTimes_empty by blast
   then show "finite (LV (NTimes r n) s)"
     by (metis LV_NTimes_5 finite_subset)
+next
+  case (Upto r n s)
+  then have "finite (LV (Star r) s)" by (simp add: LV_STAR_finite)
+  moreover
+  have "LV (Upto r n) s \<subseteq> LV (Star r) s"
+    by (meson subseteq_Upto_Star) 
+  ultimately show "finite (LV (Upto r n) s)"
+    using rev_finite_subset by blast    
 qed
 
 
 
 text \<open>
   Our POSIX values are lexical values.
 \<close>
 
+
 lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"
   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 lang.simps(7))
   using Prf_NTimes_empty by blast
 
 lemma Posix_Prf:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
   using assms Posix_LV LV_def
   by blast
 
+thm Posix1a
 
 end
\ No newline at end of file
diff --git a/thys/Posix-Lexing/Extensions/Positions3.thy b/thys/Posix-Lexing/Extensions/Positions3.thy
--- a/thys/Posix-Lexing/Extensions/Positions3.thy
+++ b/thys/Posix-Lexing/Extensions/Positions3.thy
@@ -1,861 +1,916 @@
    
 theory Positions3
   imports Lexer3 LexicalVals3
 begin
 
 section \<open>An alternative definition for POSIX values by Okui \& Suzuki\<close>
 
 section \<open>Positions in Values\<close>
 
 fun 
   at :: "'a val \<Rightarrow> nat list \<Rightarrow> 'a val"
 where
   "at v [] = v"
 | "at (Left v) (0#ps)= at v ps"
 | "at (Right v) (Suc 0#ps)= at v ps"
 | "at (Seq v1 v2) (0#ps)= at v1 ps"
 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
 | "at (Stars vs) (n#ps)= at (nth vs n) ps"
 
 
 
 fun Pos :: "'a val \<Rightarrow> (nat list) set"
 where
   "Pos (Void) = {[]}"
 | "Pos (Atm c) = {[]}"
 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 
 | "Pos (Stars []) = {[]}"
 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 
 
 lemma Pos_stars:
   "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 apply(induct vs)
 apply(auto simp add: insert_ident less_Suc_eq_0_disj)
 done
 
 lemma Pos_empty:
   shows "[] \<in> Pos v"
 by (induct v rule: Pos.induct)(auto)
 
 
 abbreviation
   "intlen vs \<equiv> int (length vs)"
 
 
 definition pflat_len :: "'a val \<Rightarrow> nat list => int"
 where
   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
 
 lemma pflat_len_simps:
   shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
   and   "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
   and   "pflat_len (Left v) (0#p) = pflat_len v p"
   and   "pflat_len (Left v) (Suc 0#p) = -1"
   and   "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
   and   "pflat_len (Right v) (0#p) = -1"
   and   "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
   and   "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
   and   "pflat_len v [] = intlen (flat v)"
 by (auto simp add: pflat_len_def Pos_empty)
 
 lemma pflat_len_Stars_simps:
   assumes "n < length vs"
   shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
 using assms
 apply(induct vs arbitrary: n p)
 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
 
 lemma pflat_len_outside:
   assumes "p \<notin> Pos v1"
   shows "pflat_len v1 p = -1 "
 using assms by (simp add: pflat_len_def)
 
 
 
 section \<open>Orderings\<close>
 
 
 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
 where
   "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
 
 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
 where
   "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
 
 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
 where
   "[] \<sqsubset>lex (p#ps)"
 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
 
 lemma lex_irrfl:
   fixes ps1 ps2 :: "nat list"
   assumes "ps1 \<sqsubset>lex ps2"
   shows "ps1 \<noteq> ps2"
 using assms
 by(induct rule: lex_list.induct)(auto)
 
 lemma lex_simps [simp]:
   fixes xs ys :: "nat list"
   shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
   and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
   and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
 by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
 
 lemma lex_trans:
   fixes ps1 ps2 ps3 :: "nat list"
   assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
   shows "ps1 \<sqsubset>lex ps3"
 using assms
 by (induct arbitrary: ps3 rule: lex_list.induct)
    (auto elim: lex_list.cases)
 
 
 lemma lex_trichotomous:
   fixes p q :: "nat list"
   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 apply(induct p arbitrary: q)
 apply(auto elim: lex_list.cases)
 apply(case_tac q)
 apply(auto)
 done
 
 
 
 
 section \<open>POSIX Ordering of Values According to Okui \& Suzuki\<close>
 
 
 definition PosOrd:: "'a val \<Rightarrow> nat list \<Rightarrow> 'a val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
 where
   "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
 lemma PosOrd_def2:
   shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> 
          pflat_len v1 p > pflat_len v2 p \<and>
          (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and>
          (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 unfolding PosOrd_def
 apply(auto)
 done
 
 
 definition PosOrd_ex:: "'a val \<Rightarrow> 'a val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
 where
   "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
 
 definition PosOrd_ex_eq:: "'a val \<Rightarrow> 'a val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
 
 lemma PosOrd_trans:
   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
   shows "v1 :\<sqsubset>val v3"
 proof -
   from assms obtain p p'
     where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
   then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def
     by (smt not_int_zless_negative)+
   have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
     by (rule lex_trichotomous)
   moreover
     { assume "p = p'"
       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       by (smt Un_iff)
       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
     }   
   moreover
     { assume "p \<sqsubset>lex p'"
       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       by (smt Un_iff lex_trans)
       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
     }
   moreover
     { assume "p' \<sqsubset>lex p"
       with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
       by (smt Un_iff lex_trans pflat_len_def)
       then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
     }
   ultimately show "v1 :\<sqsubset>val v3" by blast
 qed
 
 lemma PosOrd_irrefl:
   assumes "v :\<sqsubset>val v"
   shows "False"
 using assms unfolding PosOrd_ex_def PosOrd_def
 by auto
 
 lemma PosOrd_assym:
   assumes "v1 :\<sqsubset>val v2" 
   shows "\<not>(v2 :\<sqsubset>val v1)"
 using assms
 using PosOrd_irrefl PosOrd_trans by blast 
 
 (*
   :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
 *)
 
 lemma PosOrd_ordering:
   shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
 unfolding ordering_def PosOrd_ex_eq_def
 apply(auto)
 using PosOrd_trans partial_preordering_def apply blast
 using PosOrd_assym ordering_axioms_def by blast
 
 lemma PosOrd_order:
   shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
   using PosOrd_ordering
   apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
   by (smt (verit) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans)
 
 
 lemma PosOrd_ex_eq2:
   shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
   using PosOrd_ordering
   using PosOrd_ex_eq_def PosOrd_irrefl by blast 
 
 lemma PosOrdeq_trans:
   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
   shows "v1 :\<sqsubseteq>val v3"
 using assms PosOrd_ordering 
   unfolding ordering_def
   by (metis partial_preordering.trans)
 
 lemma PosOrdeq_antisym:
   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
   shows "v1 = v2"
 using assms PosOrd_ordering 
   by (metis ordering.eq_iff)
 
 lemma PosOrdeq_refl:
   shows "v :\<sqsubseteq>val v" 
 unfolding PosOrd_ex_eq_def
 by auto
 
 
 lemma PosOrd_shorterE:
   assumes "v1 :\<sqsubset>val v2" 
   shows "length (flat v2) \<le> length (flat v1)"
 using assms unfolding PosOrd_ex_def PosOrd_def
 apply(auto)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
 apply(drule_tac x="[]" in bspec)
 apply(simp add: Pos_empty)
 apply(simp add: pflat_len_simps)
 done
 
 lemma PosOrd_shorterI:
   assumes "length (flat v2) < length (flat v1)"
   shows "v1 :\<sqsubset>val v2"
 unfolding PosOrd_ex_def PosOrd_def pflat_len_def 
 using assms Pos_empty by force
 
 lemma PosOrd_spreI:
   assumes "flat v' \<sqsubset>spre flat v"
   shows "v :\<sqsubset>val v'" 
 using assms
 apply(rule_tac PosOrd_shorterI)
 unfolding prefix_list_def sprefix_list_def
 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
 
 lemma pflat_len_inside:
   assumes "pflat_len v2 p < pflat_len v1 p"
   shows "p \<in> Pos v1"
 using assms 
 unfolding pflat_len_def
 by (auto split: if_splits)
 
 
 lemma PosOrd_Left_Right:
   assumes "flat v1 = flat v2"
   shows "Left v1 :\<sqsubset>val Right v2" 
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
 apply(auto simp add: PosOrd_def pflat_len_simps assms)
 done
 
 lemma PosOrd_LeftE:
   assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
   shows "v1 :\<sqsubset>val v2"
 using assms
 unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 apply(frule pflat_len_inside)
 apply(auto simp add: pflat_len_simps)
 by (metis lex_simps(3) pflat_len_simps(3))
 
 lemma PosOrd_LeftI:
   assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
   shows  "Left v1 :\<sqsubset>val Left v2"
 using assms
 unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
 
 lemma PosOrd_Left_eq:
   assumes "flat v1 = flat v2"
   shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
 using assms PosOrd_LeftE PosOrd_LeftI
 by blast
 
 
 lemma PosOrd_RightE:
   assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
   shows "v1 :\<sqsubset>val v2"
 using assms
 unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 apply(frule pflat_len_inside)
 apply(auto simp add: pflat_len_simps)
 by (metis lex_simps(3) pflat_len_simps(5))
 
 lemma PosOrd_RightI:
   assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
   shows  "Right v1 :\<sqsubset>val Right v2"
 using assms
 unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
 
 
 lemma PosOrd_Right_eq:
   assumes "flat v1 = flat v2"
   shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
 using assms PosOrd_RightE PosOrd_RightI
 by blast
 
 
 lemma PosOrd_SeqI1:
   assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
   shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
 apply(clarify)
 apply(subst PosOrd_ex_def)
 apply(rule_tac x="0#p" in exI)
 apply(subst PosOrd_def)
 apply(rule conjI)
 apply(simp add: pflat_len_simps)
 apply(rule ballI)
 apply(rule impI)
 apply(simp only: Pos.simps)
 apply(auto)[1]
 apply(simp add: pflat_len_simps)
 apply(auto simp add: pflat_len_simps)
 using assms(2)
 apply(simp)
 apply(metis length_append of_nat_add)
 done
 
 lemma PosOrd_SeqI2:
   assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2"
   shows "Seq v v2 :\<sqsubset>val Seq v w2" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
 apply(clarify)
 apply(subst PosOrd_ex_def)
 apply(rule_tac x="Suc 0#p" in exI)
 apply(subst PosOrd_def)
 apply(rule conjI)
 apply(simp add: pflat_len_simps)
 apply(rule ballI)
 apply(rule impI)
 apply(simp only: Pos.simps)
 apply(auto)[1]
 apply(simp add: pflat_len_simps)
 using assms(2)
 apply(simp)
 apply(auto simp add: pflat_len_simps)
 done
 
 lemma PosOrd_Seq_eq:
   assumes "flat v2 = flat w2"
   shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2"
 using assms 
 apply(auto)
 prefer 2
 apply(simp add: PosOrd_SeqI2)
 apply(simp add: PosOrd_ex_def)
 apply(auto)
 apply(case_tac p)
 apply(simp add: PosOrd_def pflat_len_simps)
 apply(case_tac a)
 apply(simp add: PosOrd_def pflat_len_simps)
 apply(clarify)
 apply(case_tac nat)
 prefer 2
 apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
 apply(rule_tac x="list" in exI)
 apply(auto simp add: PosOrd_def2 pflat_len_simps)
 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
 done
 
 
 
 lemma PosOrd_StarsI:
   assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
   shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
 apply(clarify)
 apply(subst PosOrd_ex_def)
 apply(subst PosOrd_def)
 apply(rule_tac x="0#p" in exI)
 apply(simp add: pflat_len_Stars_simps pflat_len_simps)
 using assms(2)
 apply(simp add: pflat_len_simps)
 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 by (metis length_append of_nat_add)
 
 lemma PosOrd_StarsI2:
   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2"
   shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
 apply(clarify)
 apply(subst PosOrd_ex_def)
 apply(subst PosOrd_def)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
 apply(rule_tac x="Suc a#list" in exI)
 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
 done
 
 lemma PosOrd_Stars_appendI:
   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
 using assms
 apply(induct vs)
 apply(simp)
 apply(simp add: PosOrd_StarsI2)
 done
 
 lemma PosOrd_StarsE2:
   assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
   shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(subst (asm) PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac p)
 apply(simp)
 apply(simp add: PosOrd_def pflat_len_simps)
 apply(subst PosOrd_ex_def)
 apply(rule_tac x="[]" in exI)
 apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
 apply(simp)
 apply(case_tac a)
 apply(clarify)
 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
 apply(clarify)
 apply(simp add: PosOrd_ex_def)
 apply(rule_tac x="nat#list" in exI)
 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 apply(case_tac q)
 apply(simp add: PosOrd_def pflat_len_simps)
 apply(clarify)
 apply(drule_tac x="Suc a # lista" in bspec)
 apply(simp)
 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 apply(case_tac q)
 apply(simp add: PosOrd_def pflat_len_simps)
 apply(clarify)
 apply(drule_tac x="Suc a # lista" in bspec)
 apply(simp)
 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 done
 
 lemma PosOrd_Stars_appendE:
   assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(induct vs)
 apply(simp)
 apply(simp add: PosOrd_StarsE2)
 done
 
 lemma PosOrd_Stars_append_eq:
   assumes "flats vs1 = flats vs2"
   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(rule_tac iffI)
 apply(erule PosOrd_Stars_appendE)
 apply(rule PosOrd_Stars_appendI)
 apply(auto)
   done  
 
 lemma PosOrd_Stars_equalsI:
   assumes "flats vs1 = flats vs2" "length vs1 = length vs2"
   and     "list_all2 (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) vs1 vs2"
   shows "Stars vs1 :\<sqsubseteq>val Stars vs2"
   using assms(3) assms(2,1)
   apply(induct rule: list_all2_induct)
   apply (simp add: PosOrdeq_refl)
   apply(case_tac "Stars (x # xs) = Stars (y # ys)")
   apply (simp add: PosOrdeq_refl)
   apply(case_tac "x = y")
    apply(subgoal_tac "Stars xs :\<sqsubset>val Stars ys")
   apply (simp add: PosOrd_StarsI2 PosOrd_ex_eq_def)
   apply (simp add: PosOrd_ex_eq2)
   by (meson PosOrd_StarsI PosOrd_ex_eq_def)
 
 lemma PosOrd_almost_trichotomous:
   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))"
 apply(auto simp add: PosOrd_ex_def)
 apply(auto simp add: PosOrd_def)
 apply(rule_tac x="[]" in exI)
 apply(auto simp add: Pos_empty pflat_len_simps)
 apply(drule_tac x="[]" in spec)
 apply(auto simp add: Pos_empty pflat_len_simps)
 done
 
 
 section \<open>The Posix Value is smaller than any other lexical value\<close>
 
 
 lemma Posix_PosOrd:
   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" 
   shows "v1 :\<sqsubseteq>val v2"
 using assms
 proof (induct arbitrary: v2 rule: Posix.induct)
   case (Posix_One v)
   have "v \<in> LV One []" by fact
   then have "v = Void"
     by (simp add: LV_simps)
   then show "Void :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_Atom c v)
   have "v \<in> LV (Atom c) [c]" by fact
   then have "v = Atm c"
     by (simp add: LV_simps)
   then show "Atm c :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_Plus1 s r1 v r2 v2)
   have as1: "s \<in> r1 \<rightarrow> v" by fact
   have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   have "v2 \<in> LV (Plus r1 r2) s" by fact
   then have "\<turnstile> v2 : Plus r1 r2" "flat v2 = s"
     by(auto simp add: LV_def prefix_list_def)
   then consider
     (Left) v3 where "v2 = Left v3" "\<turnstile> v3 : r1" "flat v3 = s" 
   | (Right) v3 where "v2 = Right v3" "\<turnstile> v3 : r2" "flat v3 = s"
   by (auto elim: Prf.cases)
   then show "Left v :\<sqsubseteq>val v2"
   proof(cases)
      case (Left v3)
      have "v3 \<in> LV r1 s" using Left(2,3) 
        by (auto simp add: LV_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
      have "flat v3 = flat v" using as1 Left(3)
        by (simp add: Posix1(2)) 
      ultimately have "Left v :\<sqsubseteq>val Left v3"
        by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
   next
      case (Right v3)
      have "flat v3 = flat v" using as1 Right(3)
        by (simp add: Posix1(2)) 
      then have "Left v :\<sqsubseteq>val Right v3" 
        unfolding PosOrd_ex_eq_def
        by (simp add: PosOrd_Left_Right)
      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
   qed
 next
   case (Posix_Plus2 s r2 v r1 v2)
   have as1: "s \<in> r2 \<rightarrow> v" by fact
   have as2: "s \<notin> lang r1" by fact
   have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   have "v2 \<in> LV (Plus r1 r2) s" by fact
   then have "\<turnstile> v2 : Plus r1 r2" "flat v2 = s"
     by(auto simp add: LV_def prefix_list_def)
   then consider
     (Left) v3 where "v2 = Left v3" "\<turnstile> v3 : r1" "flat v3 = s" 
   | (Right) v3 where "v2 = Right v3" "\<turnstile> v3 : r2" "flat v3 = s"
   by (auto elim: Prf.cases)
   then show "Right v :\<sqsubseteq>val v2"
   proof (cases)
     case (Right v3)
      have "v3 \<in> LV r2 s" using Right(2,3) 
        by (auto simp add: LV_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
      have "flat v3 = flat v" using as1 Right(3)
        by (simp add: Posix1(2)) 
      ultimately have "Right v :\<sqsubseteq>val Right v3" 
         by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   next
      case (Left v3)
      have "v3 \<in> LV r1 s" using Left(2,3) as2  
        by (auto simp add: LV_def prefix_list_def)
      then have "flat v3 = flat v \<and> \<turnstile> v3 : r1" using as1 Left(3)
        by (simp add: Posix1(2) LV_def) 
      then have "False" using as1 as2 Left
        using Prf_flat_lang by blast
      then show "Right v :\<sqsubseteq>val v2" by simp
   qed
 next 
   case (Posix_Times s1 r1 v1 s2 r2 v2 v3)
   have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
   then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
   have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
   have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<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> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by fact
   have "v3 \<in> LV (Times r1 r2) (s1 @ s2)" by fact
   then obtain v3a v3b where eqs:
     "v3 = Seq v3a v3b" "\<turnstile> v3a : r1" "\<turnstile> v3b : r2"
     "flat v3a @ flat v3b = s1 @ s2" 
     by (force simp add: prefix_list_def LV_def elim: Prf.cases)
   with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
     by (smt Prf_flat_lang append_eq_append_conv2 append_self_conv)
   then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
     by (simp add: sprefix_list_def append_eq_conv_conj)
   then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
     using PosOrd_spreI as1(1) eqs by blast
   then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3)
     by (auto simp add: LV_def)
   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) 
   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next 
   case (Posix_Star1 s1 r v s2 vs v3) 
   have "s1 \<in> r \<rightarrow> v" "s2 \<in> Star r \<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 (Star r) 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> lang r \<and> s\<^sub>4 \<in> lang (Star r))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v3 \<in> LV (Star r) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
     "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : Star r"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v3 = Stars []"
   unfolding LV_def  
   apply(auto)
   apply(erule Prf_elims)
   by (metis NonEmpty Prf.intros(6) list.set_intros(1) list.set_intros(2) neq_Nil_conv)
   then show "Stars (v # vs) :\<sqsubseteq>val v3" 
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flat (Stars (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 Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7)) 
       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 (Star r) 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 (metis flat.simps(7) flat_Stars val.inject(5)) 
       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_Star2 r v2)
   have "v2 \<in> LV (Star r) []" by fact
   then have "v2 = Stars []" 
     unfolding LV_def by (auto elim: Prf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_NTimes2 vs r n v2)
   have IH: "\<forall>v\<in>set vs. [] \<in> r \<rightarrow> v \<and> (\<forall>x. x \<in> LV r [] \<longrightarrow> v :\<sqsubseteq>val x)" by fact
   then have "flats vs = []"
     by (metis Posix.Posix_NTimes2 Posix1(2) flat_Stars) 
   have "v2 \<in> LV (NTimes r n) []" by fact
     then obtain vs' where eq: "v2 = Stars vs'" and "length vs' = n" and as: "\<forall>v \<in> set vs'. v \<in> LV r [] \<and> flat v = []" 
       unfolding LV_def by (auto elim!: Prf_elims)
   then have "Stars vs :\<sqsubseteq>val Stars vs'"
     apply(rule_tac PosOrd_Stars_equalsI)
     apply (simp add: \<open>flats vs = []\<close>)
     using Posix_NTimes2.hyps(2) apply blast
     using IH apply(simp add: list_all2_iff)
     apply(auto)
     using Posix_NTimes2.hyps(2) apply blast
     by (meson in_set_zipE)
   then show "Stars vs :\<sqsubseteq>val v2" using eq by simp 
 next
   case (Posix_NTimes1 s1 r v s2 n vs)
   have "s1 \<in> r \<rightarrow> v" "s2 \<in> NTimes r (n - 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 (NTimes r (n - 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> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v2 \<in> LV (NTimes r n) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v2 = Stars (v3a # vs3)" 
     "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : NTimes r (n - 1)"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v2 = Stars []"
   unfolding LV_def  
   apply(auto)
   apply(erule Prf_elims)
   apply(case_tac vs1)
    apply(simp)
    defer
    apply(simp)
   using Prf.simps apply fastforce
   by (simp add: Aux as1(1) cond2)  
   then show "Stars (v # vs) :\<sqsubseteq>val v2" 
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flat (Stars (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 Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7)) 
       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 (NTimes r (n - 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 (metis flat.simps(7) flat_Stars val.inject(5)) 
       then show "Stars (v # vs) :\<sqsubseteq>val v2" unfolding NonEmpty by blast
     next 
       case Empty
       have "v2 = Stars []" by fact
       then show "Stars (v # vs) :\<sqsubseteq>val v2"
       unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
+  qed  
+next
+  case (Posix_Upto1 s1 r v s2 n vs v3)
+    have "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto r (n - 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 (Upto r (n - 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" by fact
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (Upto r n) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : Upto r (n - 1)"
+    "flat (Stars (v3a # vs3)) = s1 @ s2"
+  | (Empty) "v3 = Stars []"
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf_elims)
+  apply(case_tac vs)
+   apply(auto)
+  by (simp add: Prf.intros(8))
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flat (Stars (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 Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7)) 
+      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 (Upto r (n - 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 (metis flat.simps(7) flat_Stars val.inject(5)) 
+      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_Upto2 r n v2) 
+    have "v2 \<in> LV (Upto r n) []" by fact
+  then have "v2 = Stars []" 
+    unfolding LV_def by (auto elim: Prf.cases) 
+  then show "Stars [] :\<sqsubseteq>val v2"
+    by (simp add: PosOrd_ex_eq_def)
 qed
 
 
 lemma Posix_PosOrd_reverse:
   assumes "s \<in> r \<rightarrow> v1" 
   shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)"
 using assms
 by (metis Posix_PosOrd less_irrefl PosOrd_def 
     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
 
 lemma PosOrd_Posix:
   assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   shows "s \<in> r \<rightarrow> v1" 
 proof -
   have "s \<in> lang r" using assms(1) unfolding LV_def
     using Prf_flat_lang by blast
   then obtain vposix where vp: "s \<in> r \<rightarrow> vposix"
     using lexer_correct_Some by blast 
   with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd) 
   then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto
   moreover
     { assume "vposix :\<sqsubset>val v1"
       moreover
       have "vposix \<in> LV r s" using vp 
          using Posix_LV by blast 
       ultimately have "False" using assms(2) by blast
     }
   ultimately show "s \<in> r \<rightarrow> v1" using vp by blast
 qed
 
 lemma Least_existence:
   assumes "LV r s \<noteq> {}"
   shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
 proof -
   from assms
   obtain vposix where "s \<in> r \<rightarrow> vposix"
   unfolding LV_def 
   using Prf_flat_lang lexer_correct_Some by blast
   then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v"
     by (simp add: Posix_PosOrd)
   then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
     using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast
 qed 
 
 lemma Least_existence1:
   assumes "LV r s \<noteq> {}"
   shows " \<exists>! v\<^sub>m\<^sub>i\<^sub>n \<in> LV r s. \<forall>v \<in> LV r s. v\<^sub>m\<^sub>i\<^sub>n :\<sqsubseteq>val v"
 using Least_existence[OF assms] assms
 using PosOrdeq_antisym by blast
 
 lemma Least_existence2:
   assumes "LV r s \<noteq> {}"
   shows " \<exists>!vmin \<in> LV r s. lexer r s = Some vmin \<and> (\<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v)"
 using Least_existence[OF assms] assms
 using PosOrdeq_antisym 
 using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1)
   by (metis (mono_tags, lifting)) 
 
 
 lemma Least_existence1_pre:
   assumes "LV r s \<noteq> {}"
   shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
 using Least_existence[OF assms] assms
 apply -
 apply(erule bexE)
 apply(rule_tac a="vmin" in ex1I)
 apply(auto)[1]
 apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
 apply(auto)[1]
 apply(simp add: PosOrdeq_antisym)
 done
 
 lemma PosOrd_partial:
   shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
 apply(simp add: partial_order_on_def)
 apply(simp add: preorder_on_def refl_on_def)
 apply(simp add: PosOrdeq_refl)
 apply(auto)
 apply(rule transI)
 apply(auto intro: PosOrdeq_trans)[1]
 apply(rule antisymI)
 apply(simp add: PosOrdeq_antisym)
 done
   
 lemma PosOrd_wf:
   shows "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
 proof -
   have "finite {(v1, v2). v1 \<in> LV r s \<and> v2 \<in> LV r s}"
     by (simp add: LV_finite)
   moreover
   have "{(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s} \<subseteq> {(v1, v2). v1 \<in> LV r s \<and> v2 \<in> LV r s}"
     by auto
   ultimately have "finite {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}" 
     using finite_subset by blast 
   moreover
   have "acyclicP (\<lambda>v1 v2. v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s)" 
     unfolding acyclic_def
     by (smt (verit, ccfv_threshold) PosOrd_irrefl PosOrd_trans tranclp_trans_induct tranclp_unfold)    
   ultimately show "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
     using finite_acyclic_wf by blast
 qed  
 
 unused_thms
 
 end
\ No newline at end of file
diff --git a/thys/Posix-Lexing/Extensions/Regular_Exps3.thy b/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
--- a/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
+++ b/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
@@ -1,54 +1,57 @@
 (* Adapted from Tobias Nipkow in order to accommodate 
    bounded regular expressions *)
 
 section "Extended Regular Expressions 3"
 
 theory Regular_Exps3
 imports "Regular-Sets.Regular_Set"
 begin
 
 datatype (atoms: 'a) rexp =
   is_Zero: Zero |
   is_One: One |
   Atom 'a |
   Plus "('a rexp)" "('a rexp)" |
   Times "('a rexp)" "('a rexp)" |
   Star "('a rexp)" |
-  NTimes  "('a rexp)" "nat"
+  NTimes "('a rexp)" "nat" | (* r{n}    - exactly n-times *)
+  Upto "('a rexp)" "nat"     (* r{..n}  - up to n-times *)  
 
-
-primrec lang :: "'a rexp => 'a lang" where
+fun lang :: "'a rexp => 'a lang" where
 "lang Zero = {}" |
 "lang One = {[]}" |
 "lang (Atom a) = {[a]}" |
 "lang (Plus r s) = (lang r) Un (lang s)" |
 "lang (Times r s) = conc (lang r) (lang s)" |
 "lang (Star r) = star(lang r)" |
-"lang (NTimes r n) = ((lang r) ^^ n)" 
+"lang (NTimes r n) = ((lang r) ^^ n)" | 
+"lang (Upto r n) = (\<Union>i \<in> {..n}. (lang r) ^^ i)"
 
 
 lemma lang_subset_lists: 
   "atoms r \<subseteq> A \<Longrightarrow> lang r \<subseteq> lists A"
-  by (induction r)
-     (auto simp: conc_subset_lists star_subset_lists lang_pow_subset_lists)
+  apply (induction r)
+  apply(auto simp: conc_subset_lists star_subset_lists lang_pow_subset_lists)
+  by (meson in_listsD lang_pow_subset_lists subsetD)
   
 
 primrec nullable :: "'a rexp \<Rightarrow> bool" where
 "nullable Zero = False" |
 "nullable One = True" |
 "nullable (Atom c) = False" |
 "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
 "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
 "nullable (Star r) = True" |
-"nullable (NTimes r n) = (if n = 0 then True else nullable r)"
+"nullable (NTimes r n) = (if n = 0 then True else nullable r)" |
+"nullable (Upto r n) = True"
 
 
 lemma pow_empty_iff:
   shows "[] \<in> (lang r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (lang r))"
   by (induct n)(auto)
 
 lemma nullable_iff: 
   shows "nullable r \<longleftrightarrow> [] \<in> lang r"
   by (induct r) (auto simp add: conc_def pow_empty_iff split: if_splits)
 
 end