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,987 +1,986 @@
 (*  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)
 
 lemma flats_empty:
   assumes "(\<forall>v\<in>set vs. flat v = [])"
   shows "flats vs = []"
 using assms
 by(induct vs) (simp_all)
 
 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"
 | "\<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) : From r n"
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r  \<and> flat v \<noteq> []; length vs > n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : From 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"
   "\<turnstile> vs : From 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 Times_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 pow_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!: Times_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!: Times_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 = 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(simp)
 apply(rule_tac x="v#vs2" in exI)
 apply(simp)
   apply(rule_tac x="vs1 @ [v]" in exI)
   apply(simp)
 apply(rule_tac x="vs2" in exI)
 apply(simp)
   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)
   apply(meson concI pow_Prf)
   apply(meson atMost_iff pow_Prf)
   apply(subgoal_tac "flats vs1 @ flats vs2 \<in> lang r ^^ length vs1")
   apply (metis add_diff_cancel_left' atLeast_iff diff_is_0_eq empty_pow_add last_in_set length_0_conv order_refl)
   apply (metis (no_types, opaque_lifting) Aux imageE list.set_map pow_Prf self_append_conv)
   apply (meson atLeast_iff less_imp_le_nat pow_Prf)
   done
 
 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  
   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
 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) 
 next
   case (From 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 (From r n)" by fact
   then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k"  "n \<le> k"
     "\<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) = k" "n \<le> k"
       "\<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  
   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 : From r n \<and> flat v = s"
     apply(case_tac "length vs1 \<le> n")
     apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)
      apply(simp)
      apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")
       apply(auto)
        apply(rule Prf.intros(9))
        apply(auto)
     apply (meson in_set_takeD)
     apply (simp add: Aux)
     apply (meson in_set_takeD)
     apply(rule_tac x="Stars vs1" in exI)
     by (simp add: Prf.intros(10))
 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(Upto r n) = Stars []"
 | "mkeps(NTimes r n) = Stars (replicate n (mkeps r))"
 | "mkeps(From 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)" 
 | "injval (From 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)
   apply (metis Prf.intros(9) append_Nil empty_iff list.set(1) list.size(3))
   by (metis Prf.intros(9) append_Nil empty_iff in_set_replicate length_replicate list.set(1) mkeps_flat)
 
 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 simp add: Prf_injval_flat split: if_splits)[7]
 (* 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)[4]
 (* Upto *)
 apply(case_tac x2)
 apply(simp)
 using Prf_elims(1) apply blast
 apply(simp)
 apply(erule Prf_elims)
 apply(erule Prf_elims(8))
 apply(simp)
 apply(rule Prf.intros(8))
 apply(auto simp add: Prf_injval_flat)[2]  
 (* From *)
 apply(simp)  
 apply(case_tac x2)
 apply(simp)
 apply(erule Prf_elims)
 apply(simp)
 apply(erule Prf_elims(6))
 apply(simp)
 apply (simp add: Prf.intros(10) Prf_injval_flat)
 apply(simp)
 apply(erule Prf_elims)
 apply(simp)
 apply(erule Prf_elims(9))
 apply(simp)
 apply (smt (verit, best) Cons_eq_appendI Prf.intros(9) Prf_injval_flat length_Cons length_append list.discI set_ConsD)
 by (simp add: Prf.intros(10) Prf_injval_flat)
 
 
 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_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> lang r \<and> s\<^sub>4 \<in> lang (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" 
-| 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_Upto1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> Upto 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r n))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> Upto r (n + 1) \<rightarrow> Stars (v # vs)"
 | Posix_Upto2: "[] \<in> Upto r n \<rightarrow> Stars []"
 | Posix_From2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
     \<Longrightarrow> [] \<in> From r n \<rightarrow> Stars vs"
 | Posix_From1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> From 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 (From r (n - 1)))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> From r n \<rightarrow> Stars (v # vs)"  
 | Posix_From3: "\<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> From r 0 \<rightarrow> Stars (v # vs)"  
 
 
 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"
   "s \<in> From 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))
-  apply(meson ex_in_conv set_empty)
+  apply (meson ex_in_conv set_empty)
   apply(metis Suc_pred atMost_iff concI lang_pow.simps(2) not_less_eq_eq)
   apply (meson atLeast_iff dual_order.refl in_set_conv_nth)
   apply (metis Suc_le_mono Suc_pred atLeast_iff concI lang_pow.simps(2))
   by (simp add: star_pow)
   
 
 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))
+  apply (metis (no_types, lifting) Prf.intros(8) Prf_elims(8) Suc_le_mono length_Cons set_ConsD val.inject(5))
   apply (metis Posix1(2) Prf.intros(9) append_Nil empty_iff list.set(1))
   apply(erule Prf_elims)
   apply(auto)
   apply (smt (verit, best) Cons_eq_appendI Prf.intros(9) Suc_pred length_Cons length_append set_ConsD)
   apply (simp add: Prf.intros(10))
   apply(erule Prf_elims)
   apply(auto)
   by (simp add: Prf.intros(10))
       
 
 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)
 apply(simp add: Posix_NTimes2 pow_empty_iff)
 by (simp add: Posix_From2 pow_empty_iff)
 
 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')"
+  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> lang r \<and> s\<^sub>4 \<in> lang (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 Posix1(1) Posix_NTimes1.hyps(6) append.right_neutral append_Nil)
   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
 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')"
+  have "(s1 @ s2) \<in> Upto r (n + 1) \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto 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> lang r \<and> s\<^sub>4 \<in> lang (Upto r n))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (Upto 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_Upto1.hyps(7) append_Nil2 self_append_conv2)
+    apply (metis Posix1(1) Posix_Upto1.hyps(6) append.right_neutral append_Nil)
   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+
+            "\<And>v2. s2 \<in> Upto r n \<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)
 next
   case (Posix_From2 vs r n v2)
   then show "Stars vs = v2"
     apply(erule_tac Posix_elims)
      apply(auto)
     apply(rule List_eq_zipI)
      apply(auto)
       apply(meson in_set_zipE)
      apply (simp add: Posix1(2))
     using Posix1(2) by blast
 next
   case (Posix_From1 s1 r v s2 n vs)
   have "(s1 @ s2) \<in> From r n \<rightarrow> v2" 
        "s1 \<in> r \<rightarrow> v" "s2 \<in> From 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 (From r (n - 1 )))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (From r (n - 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 (smt (verit, ccfv_threshold) Posix1(1) UN_E append_eq_append_conv2 lang.simps(9))
     by (metis One_nat_def Posix1(1) Posix_From1.hyps(7) append_Nil2 append_self_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> From r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 next
   case (Posix_From3 s1 r v s2 vs)
   have "(s1 @ s2) \<in> From r 0 \<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(2) apply fastforce
     using Posix1(1) apply fastforce
     by (metis Posix1(1) Posix_From3.hyps(6) append.right_neutral append_Nil)
   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  
 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)"
-          by (meson Posix_NTimes1 cons(5)) 
+          by (metis One_nat_def Posix_NTimes1 Suc_pred add.commute cons(5) plus_1_eq_Suc)
         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"
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "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)
+    by (metis Posix1a Prf_elims(8) UN_E cons diff_Suc_1 lang.simps(8))
     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)) 
+          by (metis One_nat_def Posix_Upto1 Posix_elims(1) Suc_pred Upto.prems add.commute bot_nat_0.not_eq_extremum deriv.simps(8) plus_1_eq_Suc)
         then show "(c # s) \<in> Upto r n \<rightarrow> injval (Upto r n) c v" using cons by(simp)
       qed
 next
   case (From 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 (From 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> (From 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 (From r (n - 1)))"
      | (null) v1 vs s1 s2 where 
         "v = Seq v1 (Stars vs)" "s = s1 @ s2"  "s2 \<in> (Star r) \<rightarrow> (Stars vs)" 
         "s1 \<in> deriv c r \<rightarrow> v1" "n = 0"
          "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))"  
     apply(auto elim: Posix_elims simp add: lang_deriv Deriv_def intro: Posix.intros split: if_splits)
     apply(erule Posix_elims)
     apply(auto)
     apply(auto elim: Posix_elims simp add: lang_deriv Deriv_def intro: Posix.intros split: if_splits)
     apply(metis Posix1a Prf_elims(6))     
     apply(erule Posix_elims)
     apply(auto)
     apply(erule Posix_elims(9))
     apply (metis (no_types, lifting) Nil_is_append_conv Posix_From2)
      apply (simp add: Posix_From1 that(1))
     by (simp add: Posix_From3 that(1))
     then show "(c # s) \<in> (From r n) \<rightarrow> injval (From 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> (From 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 (From 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 (From r (n - 1)))" 
             by (simp add: lang_deriv Deriv_def)
         ultimately 
         have "((c # s1) @ s2) \<in> From r n \<rightarrow> Stars (injval r c v1 # vs)"
           by (meson Posix_From1 cons(5))
         then show "(c # s) \<in> From r n \<rightarrow> injval (From r n) c v" using cons by(simp)
       next 
        case null
           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> From r 0 \<rightarrow> Stars (injval r c v1 # vs)"
           by (metis Posix_From3) 
         then show "(c # s) \<in> From r n \<rightarrow> injval (From r n) c v" using null 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/Positions3.thy b/thys/Posix-Lexing/Extensions/Positions3.thy
--- a/thys/Posix-Lexing/Extensions/Positions3.thy
+++ b/thys/Posix-Lexing/Extensions/Positions3.thy
@@ -1,1031 +1,1031 @@
    
 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+
+  have "s1 \<in> r \<rightarrow> v" "s2 \<in> NTimes r n \<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 IH2: "\<And>v3. v3 \<in> LV (NTimes r n) 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))" by fact
   have cond2: "flat v \<noteq> []" by fact
-  have "v2 \<in> LV (NTimes r n) (s1 @ s2)" by fact
+  have "v2 \<in> LV (NTimes r (n + 1)) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v2 = Stars (v3a # vs3)" 
-    "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : NTimes r (n - 1)"
+    "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : NTimes r n"
     "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 add: as1(1) cond2 flats_empty)
    apply(simp)
   using Prf.simps apply fastforce
-  by (simp add: Aux as1(1) cond2)  
+  done
   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)" 
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NTimes r n) 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+
+    have "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto r n \<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 IH2: "\<And>v3. v3 \<in> LV (Upto r n) 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))" by fact
   have cond2: "flat v \<noteq> []" by fact
-  have "v3 \<in> LV (Upto r n) (s1 @ s2)" by fact
+  have "v3 \<in> LV (Upto r (n + 1)) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
-    "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : Upto r (n - 1)"
+    "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : Upto r n"
     "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> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (Upto r n) 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)
 next
   case (Posix_From2 vs r n)
   then show "Stars vs :\<sqsubseteq>val v2"
     apply(simp add: LV_def)
       apply(auto)  
     apply(erule Prf_elims)
      apply(auto)
     apply(rule PosOrd_Stars_equalsI)
     apply (metis Posix1(2) flats_empty) 
       apply(simp)
     apply(auto simp add: list_all2_iff)
     apply (meson set_zip_leftD set_zip_rightD)
     done
 next
   case (Posix_From1 s1 r v s2 n vs v3)
   have "s1 \<in> r \<rightarrow> v" "s2 \<in> From r (n - 1) \<rightarrow> Stars vs" by fact+
   then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
   have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
   have IH2: "\<And>v3. v3 \<in> LV (From 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 (From r (n - 1)))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v3 \<in> LV (From r n) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
     "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : From r (n - 1)"
     "flats (v3a # vs3) = s1 @ s2"
   | (Empty) "v3 = Stars []" 
   unfolding LV_def  
   apply(auto)
   apply(erule Prf.cases)
              apply(auto)  
   apply(case_tac vs1)
    apply(auto intro: Prf.intros)
    apply(case_tac vs2)
     apply(auto intro: Prf.intros)
     apply (simp add: as1(1) cond2 flats_empty)
   apply (simp add: Prf.intros)
   apply(case_tac vs)
    apply(auto)
   by (metis Posix_From1.hyps(6) Prf.intros(10) Suc_le_eq Suc_pred less_Suc_eq_le)
   then show "Stars (v # vs) :\<sqsubseteq>val v3" 
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
         unfolding prefix_list_def
         by (smt (z3) Prf_flat_lang append.right_neutral append_eq_append_conv2 flat.simps(7) flat_Stars)
       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
         by (simp add: sprefix_list_def append_eq_conv_conj)
       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
         using PosOrd_spreI as1(1) NonEmpty(4) by blast
       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (From 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
         by (metis PosOrd_StarsI PosOrd_StarsI2 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_From3 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 (From r 0) (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.cases)
   apply(auto)
   apply(case_tac vs)
   apply(auto intro: Prf.intros)
   done
   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 (z3) Prf_flat_lang append.right_neutral 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
         by (metis PosOrd_StarsI PosOrd_StarsI2 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      
 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