diff --git a/thys/Posix-Lexing/Extensions/Derivatives3.thy b/thys/Posix-Lexing/Extensions/Derivatives3.thy
--- a/thys/Posix-Lexing/Extensions/Derivatives3.thy
+++ b/thys/Posix-Lexing/Extensions/Derivatives3.thy
@@ -1,67 +1,71 @@
 section "Derivatives of Extended Regular Expressions"
 
 (* Author: Christian Urban *)
 
 theory Derivatives3
 imports Regular_Exps3
 begin
 
 text\<open>This theory is based on work by Brozowski \cite{Brzozowski64}.\<close>
 
 subsection \<open>Brzozowski's derivatives of regular expressions\<close>
 
 fun
   deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
   "deriv c (Zero) = Zero"
 | "deriv c (One) = Zero"
 | "deriv c (Atom c') = (if c = c' then One else Zero)"
 | "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
 | "deriv c (Times r1 r2) = 
     (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
 | "deriv c (Star r) = Times (deriv c r) (Star r)"
 | "deriv c (NTimes r n) = (if n = 0 then Zero else Times (deriv c r) (NTimes r (n - 1)))"
 | "deriv c (Upto r n) = (if n = 0 then Zero else Times (deriv c r) (Upto r (n - 1)))"
+| "deriv c (From r n) = (if n = 0 then Times (deriv c r) (Star r) else Times (deriv c r) (From r (n - 1)))"
 
 fun 
   derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 where
   "derivs [] r = r"
 | "derivs (c # s) r = derivs s (deriv c r)"
 
 
 lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
 by (induction r) (auto)
 
 lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> atoms r"
 by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD])
 
 
 
 lemma deriv_pow [simp]:
   shows "Deriv c (A ^^ n) = (if n = 0 then {} else (Deriv c A) @@ (A ^^ (n - 1)))"
   apply(induct n arbitrary: A)
   apply(auto)
   by (metis Suc_pred concI_if_Nil2 conc_assoc conc_pow_comm lang_pow.simps(2))
 
 lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
   apply (induct r rule: lang.induct) 
   apply(auto simp add: nullable_iff conc_UNION_distrib)
   apply (metis IntI Suc_pred atMost_iff diff_Suc_1 mem_Collect_eq not_less_eq_eq zero_less_Suc)
   apply(auto)
+  apply(simp add: conc_def)
+  apply(metis diff_Suc_Suc minus_nat.diff_0 star_pow zero_less_Suc)
+  apply(metis IntI Suc_le_mono Suc_pred atLeast_iff diff_Suc_1 mem_Collect_eq zero_less_Suc)
   done    
   
 
 lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)"
 by (induct s arbitrary: r) (simp_all add: lang_deriv)
 
 text \<open>A regular expression matcher:\<close>
 
 definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
 "matcher r s = nullable (derivs s r)"
 
 lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
 by (induct s arbitrary: r)
    (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
 
 end
diff --git a/thys/Posix-Lexing/Extensions/Lexer3.thy b/thys/Posix-Lexing/Extensions/Lexer3.thy
--- a/thys/Posix-Lexing/Extensions/Lexer3.thy
+++ b/thys/Posix-Lexing/Extensions/Lexer3.thy
@@ -1,794 +1,987 @@
 (*  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)
+  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 Seq_decomp:
+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 NTimes_string:
+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!: Seq_decomp)
+  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:
+lemma pow_cstring:
   assumes "s \<in> A ^^ n"
   shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> 
          (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])"
 using assms
 apply(induct n arbitrary: s)
   apply(auto)[1]
-  apply(auto dest!: Seq_decomp simp add: Seq_def)
+  apply(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(induct v r rule: Prf.induct) 
+  apply(auto simp add: concat_in_star subset_eq lang_pow_add)
   apply(meson concI pow_Prf)
-  by (meson atMost_iff 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
+  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)    
+    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) 
+    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)
-  done
+  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 split: if_splits)
-(* Star *)
-apply (simp add: Prf_injval_flat)
+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)
-  done
+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_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_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)
-  by (metis Suc_pred atMost_iff concI lang_pow.simps(2) not_less_eq_eq)
+  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))
-  done
+  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)
-done
+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')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
     using Posix1(1) apply fastforce
     apply (metis One_nat_def Posix1(1) Posix_NTimes1.hyps(7) append.right_neutral append_self_conv2)
   using Posix1(2) by blast
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NTimes r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 next
   case (Posix_Upto1 s1 r v s2 n vs)
   have "(s1 @ s2) \<in> Upto r n \<rightarrow> v2" 
        "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (Upto r (n - 1)) \<rightarrow> (Stars vs')"
     apply(cases) apply (auto simp add: append_eq_append_conv2)
     using Posix1(1) apply fastforce
     apply (metis One_nat_def Posix1(1) Posix_Upto1.hyps(7) append_Nil2 self_append_conv2)
   using Posix1(2) by blast
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> Upto r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
 next
   case (Posix_Upto2 r n)
   have "[] \<in> Upto r n \<rightarrow> v2" by fact
   then show "Stars [] = v2" by cases (auto simp add: Posix1)
+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)" 
-           apply (rule_tac Posix.intros)
-               apply(simp_all)
-              apply(case_tac n)
-            apply(simp)
-           using Posix_elims(1) NTimes.prems apply auto[1]
-             apply(simp)
-             done
+        have "((c # s1) @ s2) \<in> NTimes r n \<rightarrow> Stars (injval r c v1 # vs)"
+          by (meson Posix_NTimes1 cons(5)) 
         then show "(c # s) \<in> NTimes r n \<rightarrow> injval (NTimes r n) c v" using cons by(simp)
       qed  
 next
   case (Upto r n)
   have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
   have "s \<in> deriv c (Upto r n) \<rightarrow> v" by fact
   then consider
       (cons) v1 vs s1 s2 where 
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" "0 < n"
         "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (Upto r (n - 1)) \<rightarrow> (Stars vs)"
         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" 
-    apply(auto elim!: Posix_elims simp add: lang_deriv Deriv_def intro: Posix.intros)
+    apply(auto elim!: Posix_elims simp add: lang_deriv Deriv_def intro: Posix.intros)    
     apply(case_tac n)
      apply(auto)
     using Posix_elims(1) apply blast
     apply(erule_tac Posix_elims)
     apply(auto)
     by (metis Posix1a Prf_elims(8) UN_E cons diff_Suc_1 lang.simps(8) zero_less_Suc)
     then show "(c # s) \<in> Upto r n \<rightarrow> injval (Upto r n) c v" 
     proof (cases)
       case cons
           have "s1 \<in> deriv c r \<rightarrow> v1" by fact
           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
         moreover
           have "s2 \<in> Upto r (n - 1) \<rightarrow> Stars vs" by fact
         moreover 
           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
           then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
           then have "flat (injval r c v1) \<noteq> []" by simp
         moreover 
           have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" by fact
           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" 
             by (simp add: lang_deriv Deriv_def)
         ultimately 
         have "((c # s1) @ s2) \<in> Upto r n \<rightarrow> Stars (injval r c v1 # vs)"
           by (meson Posix_Upto1 cons(3)) 
         then show "(c # s) \<in> Upto r n \<rightarrow> injval (Upto r n) c v" using cons by(simp)
       qed
+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/LexicalVals3.thy b/thys/Posix-Lexing/Extensions/LexicalVals3.thy
--- a/thys/Posix-Lexing/Extensions/LexicalVals3.thy
+++ b/thys/Posix-Lexing/Extensions/LexicalVals3.thy
@@ -1,263 +1,381 @@
 theory LexicalVals3
   imports Lexer3 "HOL-Library.Sublist"
 begin
 
 section \<open> Sets of Lexical Values \<close>
 
 text \<open>
   Shows that lexical values are finite for a given regex and string.
 \<close>
 
 definition
   LV :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) set"
 where  "LV r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
 
 lemma LV_simps:
   shows "LV Zero s = {}"
   and   "LV One s = (if s = [] then {Void} else {})"
   and   "LV (Atom c) s = (if s = [c] then {Atm c} else {})"
   and   "LV (Plus r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
   and   "LV (NTimes r 0) s = (if s = [] then {Stars []} else {})"
 unfolding LV_def
   apply(auto intro: Prf.intros elim: Prf.cases)
-  by (simp add: Prf_NTimes_empty)
-  
+  apply(simp add: Prf_NTimes_empty)
+  done  
 
 abbreviation
   "Prefixes s \<equiv> {s'. prefix s' s}"
 
 abbreviation
   "Suffixes s \<equiv> {s'. suffix s' s}"
 
 abbreviation
   "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
 
 lemma Suffixes_cons [simp]:
   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
 by (auto simp add: suffix_def Cons_eq_append_conv)
 
 
 lemma finite_Suffixes: 
   shows "finite (Suffixes s)"
 by (induct s) (simp_all)
 
 lemma finite_SSuffixes: 
   shows "finite (SSuffixes s)"
 proof -
   have "SSuffixes s \<subseteq> Suffixes s"
    unfolding strict_suffix_def suffix_def by auto
   then show "finite (SSuffixes s)"
    using finite_Suffixes finite_subset by blast
 qed
 
 lemma finite_Prefixes: 
   shows "finite (Prefixes s)"
 proof -
   have "finite (Suffixes (rev s))" 
     by (rule finite_Suffixes)
   then have "finite (rev ` Suffixes (rev s))" by simp
   moreover
   have "rev ` (Suffixes (rev s)) = Prefixes s"
   unfolding suffix_def prefix_def image_def
    by (auto)(metis rev_append rev_rev_ident)+
   ultimately show "finite (Prefixes s)" by simp
 qed
 
 lemma LV_STAR_finite:
   assumes "\<forall>s. finite (LV r s)"
   shows "finite (LV (Star r) s)"
 proof(induct s rule: length_induct)
   fix s::"'a list"
   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (Star r) s')"
   then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (Star r) s')"
     by (force simp add: strict_suffix_def suffix_def) 
   define f where "f \<equiv> \<lambda>(v::'a val, vs). Stars (v # vs)"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
   define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (Star r) s2)"
   have "finite S1" using assms
     unfolding S1_def by (simp_all add: finite_Prefixes)
   moreover 
   with IH have "finite S2" unfolding S2_def
     by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
   ultimately 
   have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
   moreover 
   have "LV (Star r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
   unfolding S1_def S2_def f_def
   unfolding LV_def image_def prefix_def strict_suffix_def 
   apply(auto)
   apply(case_tac x)
   apply(auto elim: Prf_elims)
   apply(erule Prf_elims)
   apply(auto)
   apply(case_tac vs)
   apply(auto intro: Prf.intros)  
   apply(rule exI)
   apply(rule conjI)
   apply(rule_tac x="flat a" in exI)
   apply(rule conjI)
   apply(rule_tac x="flats list" in exI)
   apply(simp)
   apply(blast)
   apply(simp add: suffix_def)
   using Prf.intros(6) by blast  
   ultimately
   show "finite (LV (Star r) s)" by (simp add: finite_subset)
 qed  
 
 definition
+  "Stars_Cons V Vs \<equiv> {Stars (v # vs) | v vs. v \<in> V \<and> Stars vs \<in> Vs}"
+
+definition
   "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
 
+fun Stars_Pow :: "('a val) set \<Rightarrow> nat \<Rightarrow> ('a val) set"
+where  
+  "Stars_Pow Vs 0 = {Stars []}"
+| "Stars_Pow Vs (Suc n) = Stars_Cons Vs (Stars_Pow Vs n)"
+  
+lemma finite_Stars_Cons:
+  assumes "finite V" "finite Vs"
+  shows "finite (Stars_Cons V Vs)"
+  using assms  
+proof -
+  from assms(2) have "finite (Stars -` Vs)"
+    by(simp add: finite_vimageI inj_on_def) 
+  with assms(1) have "finite (V \<times> (Stars -` Vs))"
+    by(simp)
+  then have "finite ((\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs)))"
+    by simp
+  moreover have "Stars_Cons V Vs = (\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs))"
+    unfolding Stars_Cons_def by auto    
+  ultimately show "finite (Stars_Cons V Vs)"   
+    by simp
+qed
+
 lemma finite_Stars_Append:
   assumes "finite Vs1" "finite Vs2"
   shows "finite (Stars_Append Vs1 Vs2)"
   using assms  
 proof -
   define UVs1 where "UVs1 \<equiv> Stars -` Vs1"
   define UVs2 where "UVs2 \<equiv> Stars -` Vs2"  
   from assms have "finite UVs1" "finite UVs2"
     unfolding UVs1_def UVs2_def
     by(simp_all add: finite_vimageI inj_on_def) 
   then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"
     by simp
   moreover 
     have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"
     unfolding Stars_Append_def UVs1_def UVs2_def by auto    
   ultimately show "finite (Stars_Append Vs1 Vs2)"   
     by simp
 qed 
+ 
+lemma finite_Stars_Pow:
+  assumes "finite Vs"
+  shows "finite (Stars_Pow Vs n)"    
+by (induct n) (simp_all add: finite_Stars_Cons assms)
 
 lemma LV_NTimes_5:
   "LV (NTimes r n) s \<subseteq> Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (NTimes r i) [])"
 apply(auto simp add: LV_def)
 apply(auto elim!: Prf_elims)
   apply(auto simp add: Stars_Append_def)
   apply(rule_tac x="vs1" in exI)
   apply(rule_tac x="vs2" in exI)  
   apply(auto)
     using Prf.intros(6) apply(auto)
       apply(rule_tac x="length vs2" in bexI)
     thm Prf.intros
       apply(subst append.simps(1)[symmetric])
     apply(rule Prf.intros)
       apply(auto)[1]
       apply(auto)[1]
      apply(simp)
     apply(simp)
       done
 
 lemma LV_NTIMES_3:
   shows "LV (NTimes r (Suc n)) [] = 
      (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTimes r n) [])))"
 unfolding LV_def
 apply(auto elim!: Prf_elims simp add: image_def)
 apply(case_tac vs1)
 apply(auto)
 apply(case_tac vs2)
 apply(auto)
 apply(subst append.simps(1)[symmetric])
 apply(rule Prf.intros)
 apply(auto)
 apply(subst append.simps(1)[symmetric])
 apply(rule Prf.intros)
 apply(auto)
   done 
 
 lemma finite_NTimes_empty:
   assumes "\<And>s. finite (LV r s)" 
   shows "finite (LV (NTimes r n) [])"
   using assms
   apply(induct n)
    apply(auto simp add: LV_simps)
   apply(subst LV_NTIMES_3)
   apply(rule finite_imageI)
   apply(rule finite_cartesian_product)
   using assms apply simp 
   apply(rule finite_vimageI)
   apply(simp)
   apply(simp add: inj_on_def)
   done
 
+lemma LV_From_5:
+  shows "LV (From r n) s \<subseteq> Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (From r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+apply(auto simp add: Stars_Append_def)
+apply(rule_tac x="vs1" in exI)
+apply(rule_tac x="vs2" in exI)  
+apply(auto)
+    using Prf.intros(6) apply(auto)
+      apply(rule_tac x="length vs2" in bexI)
+    thm Prf.intros
+      apply(subst append.simps(1)[symmetric])
+    apply(rule Prf.intros)
+      apply(auto)[1]
+      apply(auto)[1]
+     apply(simp)
+     apply(simp)
+      apply(rule_tac x="vs" in exI)
+    apply(rule_tac x="[]" in exI) 
+    apply(auto)
+    by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le)
+
+lemma LV_FROMNTIMES_3:
+  shows "LV (From r (Suc n)) [] = 
+    (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (From r n) [])))"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+     apply(auto)
+  apply (metis le_imp_less_Suc length_greater_0_conv less_antisym list.exhaust list.set_intros(1) not_less_eq zero_le)
+  prefer 2
+  using nth_mem apply blast
+  apply(case_tac vs1)
+  apply (smt Groups.add_ac(2) Prf.intros(9) add.right_neutral add_Suc_right append.simps(1) insert_iff length_append list.set(2) list.size(3) list.size(4))
+    apply(auto)
+done   
+
+lemma LV_From_empty:
+ "LV (From r n) [] = Stars_Pow (LV r []) n" 
+  apply(induct n)
+   apply(simp add: LV_def)    
+   apply(auto elim: Prf_elims simp add: image_def)[1]
+   prefer 2
+    apply(subst append.simps[symmetric])
+    apply(rule Prf.intros)
+      apply(simp_all)
+   apply(erule Prf_elims) 
+    apply(case_tac vs1)
+     apply(simp)
+    apply(simp)
+   apply(case_tac x)
+    apply(simp_all)
+    apply(simp add: LV_FROMNTIMES_3 image_def Stars_Cons_def)
+  apply blast
+ done   
+
+lemma finite_From_empty:
+  assumes "\<forall>s. finite (LV r s)"
+  shows "finite (LV (From r n) s)"
+  apply(rule finite_subset)
+   apply(rule LV_From_5)
+  apply(rule finite_Stars_Append)
+    apply(rule LV_STAR_finite)
+   apply(rule assms)
+  apply(rule finite_UN_I)
+   apply(auto)
+  by (simp add: assms finite_Stars_Pow LV_From_empty)
+    
+
 lemma subseteq_Upto_Star:
   shows "LV (Upto r n) s \<subseteq> LV (Star r) s"
   apply(auto simp add: LV_def)
   by (metis Prf.intros(6) Prf_elims(8))
 
+
 lemma LV_finite:
   shows "finite (LV r s)"
 proof(induct r arbitrary: s)
   case (Zero s) 
   show "finite (LV Zero s)" by (simp add: LV_simps)
 next
   case (One s)
   show "finite (LV One s)" by (simp add: LV_simps)
 next
   case (Atom c s)
   show "finite (LV (Atom c) s)" by (simp add: LV_simps)
 next 
   case (Plus r1 r2 s)
   then show "finite (LV (Plus r1 r2) s)" by (simp add: LV_simps)
 next 
   case (Times r1 r2 s)
   define f where "f \<equiv> \<lambda>(v1::'a val, v2). Seq v1 v2"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'"
   define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'"
   have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+
   then have "finite S1" "finite S2" unfolding S1_def S2_def
     by (simp_all add: finite_Prefixes finite_Suffixes)
   moreover
   have "LV (Times r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
     unfolding f_def S1_def S2_def 
     unfolding LV_def image_def prefix_def suffix_def
     apply (auto elim!: Prf_elims)
     by (metis (mono_tags, lifting) mem_Collect_eq)  
   ultimately 
   show "finite (LV (Times r1 r2) s)"
     by (simp add: finite_subset)
 next
   case (Star r s)
   then show "finite (LV (Star r) s)" by (simp add: LV_STAR_finite)
 next
   case (NTimes r n s)
   have "\<And>s. finite (LV r s)" by fact
   then have "finite (Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (NTimes r i) []))" 
     apply(rule_tac finite_Stars_Append)
      apply (simp add: LV_STAR_finite)
     using finite_NTimes_empty by blast
   then show "finite (LV (NTimes r n) s)"
     by (metis LV_NTimes_5 finite_subset)
 next
   case (Upto r n s)
   then have "finite (LV (Star r) s)" by (simp add: LV_STAR_finite)
   moreover
   have "LV (Upto r n) s \<subseteq> LV (Star r) s"
     by (meson subseteq_Upto_Star) 
   ultimately show "finite (LV (Upto r n) s)"
-    using rev_finite_subset by blast    
+    using rev_finite_subset by blast 
+next 
+  case (From r n)
+  then show "finite (LV (From r n) s)"
+    by (simp add: finite_From_empty)
 qed
 
 
 
 text \<open>
   Our POSIX values are lexical values.
 \<close>
 
 
 lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"
   shows "v \<in> LV r s"
   using assms unfolding LV_def
   apply(induct rule: Posix.induct)
-          apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a)
-  apply (smt (verit, best) One_nat_def Posix1a Posix_NTimes1 lang.simps(7))
-  using Prf_NTimes_empty by blast
+  using Prf.intros(4) flat.simps(1) apply blast
+  apply (simp add: Prf.intros(5))
+  apply (simp add: Prf.intros(2))
+  apply (simp add: Prf.intros(3))
+  apply (simp add: Prf.intros(1))
+  apply (smt (verit, best) CollectI Posix1(2) Posix1a Posix_Star1)
+  apply (simp add: Prf.intros(6))
+  apply (smt (verit, best) Posix1(2) Posix1a Posix_NTimes1 mem_Collect_eq)
+  using Posix1a Posix_NTimes2 apply fastforce
+  apply (smt (verit, ccfv_threshold) Posix1(2) Posix1a Posix_Upto1 mem_Collect_eq)
+  using Posix1a Posix_Upto2 apply fastforce
+  using Posix1a Posix_From2 apply fastforce
+  apply (smt (verit, best) Posix1(2) Posix1a Posix_From1 mem_Collect_eq)
+  by (smt (verit, best) Posix1a Posix_From3 flat.simps(7) mem_Collect_eq)
 
 lemma Posix_Prf:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
   using assms Posix_LV LV_def
   by blast
 
-thm Posix1a
-
 end
\ No newline at end of file
diff --git a/thys/Posix-Lexing/Extensions/Positions3.thy b/thys/Posix-Lexing/Extensions/Positions3.thy
--- a/thys/Posix-Lexing/Extensions/Positions3.thy
+++ b/thys/Posix-Lexing/Extensions/Positions3.thy
@@ -1,916 +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+
   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
   have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
   have IH2: "\<And>v3. v3 \<in> LV (NTimes r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v2 \<in> LV (NTimes r n) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v2 = Stars (v3a # vs3)" 
     "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : NTimes r (n - 1)"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v2 = Stars []"
   unfolding LV_def  
   apply(auto)
   apply(erule Prf_elims)
   apply(case_tac vs1)
    apply(simp)
    defer
    apply(simp)
   using Prf.simps apply fastforce
   by (simp add: Aux as1(1) cond2)  
   then show "Stars (v # vs) :\<sqsubseteq>val v2" 
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
         unfolding prefix_list_def
         by (smt Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7)) 
       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
         by (simp add: sprefix_list_def append_eq_conv_conj)
       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
         using PosOrd_spreI as1(1) NonEmpty(4) by blast
       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NTimes r (n - 1)) s2)" 
         using NonEmpty(2,3) by (auto simp add: LV_def)
       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
          unfolding PosOrd_ex_eq_def by auto     
       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
         unfolding  PosOrd_ex_eq_def
         using PosOrd_StarsI PosOrd_StarsI2
         by (metis flat.simps(7) flat_Stars val.inject(5)) 
       then show "Stars (v # vs) :\<sqsubseteq>val v2" unfolding NonEmpty by blast
     next 
       case Empty
       have "v2 = Stars []" by fact
       then show "Stars (v # vs) :\<sqsubseteq>val v2"
       unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
   qed  
 next
   case (Posix_Upto1 s1 r v s2 n vs v3)
     have "s1 \<in> r \<rightarrow> v" "s2 \<in> Upto r (n - 1) \<rightarrow> Stars vs" by fact+
   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
   have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
   have IH2: "\<And>v3. v3 \<in> LV (Upto r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Upto r (n - 1)))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v3 \<in> LV (Upto r n) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
     "\<turnstile> v3a : r" "\<turnstile> Stars vs3 : Upto r (n - 1)"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v3 = Stars []"
   unfolding LV_def  
   apply(auto)
   apply(erule Prf_elims)
   apply(case_tac vs)
    apply(auto)
   by (simp add: Prf.intros(8))
   then show "Stars (v # vs) :\<sqsubseteq>val v3" 
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
         unfolding prefix_list_def
         by (smt Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7)) 
       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
         by (simp add: sprefix_list_def append_eq_conv_conj)
       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
         using PosOrd_spreI as1(1) NonEmpty(4) by blast
       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (Upto r (n - 1)) s2)" 
         using NonEmpty(2,3) by (auto simp add: LV_def)
       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
          unfolding PosOrd_ex_eq_def by auto     
       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
         unfolding  PosOrd_ex_eq_def
         using PosOrd_StarsI PosOrd_StarsI2
         by (metis flat.simps(7) flat_Stars val.inject(5)) 
       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
     next 
       case Empty
       have "v3 = Stars []" by fact
       then show "Stars (v # vs) :\<sqsubseteq>val v3"
       unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
     qed    
 next
   case (Posix_Upto2 r n v2) 
     have "v2 \<in> LV (Upto r n) []" by fact
   then have "v2 = Stars []" 
     unfolding LV_def by (auto elim: Prf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
     by (simp add: PosOrd_ex_eq_def)
+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
diff --git a/thys/Posix-Lexing/Extensions/Regular_Exps3.thy b/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
--- a/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
+++ b/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
@@ -1,57 +1,59 @@
 (* Adapted from Tobias Nipkow in order to accommodate 
    bounded regular expressions *)
 
 section "Extended Regular Expressions 3"
 
 theory Regular_Exps3
 imports "Regular-Sets.Regular_Set"
 begin
 
 datatype (atoms: 'a) rexp =
   is_Zero: Zero |
   is_One: One |
   Atom 'a |
   Plus "('a rexp)" "('a rexp)" |
   Times "('a rexp)" "('a rexp)" |
   Star "('a rexp)" |
   NTimes "('a rexp)" "nat" | (* r{n}    - exactly n-times *)
-  Upto "('a rexp)" "nat"     (* r{..n}  - up to n-times *)  
+  Upto "('a rexp)" "nat" |   (* r{..n}  - up to n-times *) 
+  From "('a rexp)" "nat"     (* r{n..}  - from n-times *) 
 
 fun lang :: "'a rexp => 'a lang" where
 "lang Zero = {}" |
 "lang One = {[]}" |
 "lang (Atom a) = {[a]}" |
 "lang (Plus r s) = (lang r) Un (lang s)" |
 "lang (Times r s) = conc (lang r) (lang s)" |
 "lang (Star r) = star(lang r)" |
 "lang (NTimes r n) = ((lang r) ^^ n)" | 
-"lang (Upto r n) = (\<Union>i \<in> {..n}. (lang r) ^^ i)"
-
+"lang (Upto r n) = (\<Union>i \<in> {..n}. (lang r) ^^ i)" |
+"lang (From r n) = (\<Union>i \<in> {n..}. (lang r) ^^ i)"
 
 lemma lang_subset_lists: 
   "atoms r \<subseteq> A \<Longrightarrow> lang r \<subseteq> lists A"
-  apply (induction r)
+  apply(induction r)
   apply(auto simp: conc_subset_lists star_subset_lists lang_pow_subset_lists)
+  apply(meson in_listsD lang_pow_subset_lists subsetD)
   by (meson in_listsD lang_pow_subset_lists subsetD)
   
 
 primrec nullable :: "'a rexp \<Rightarrow> bool" where
 "nullable Zero = False" |
 "nullable One = True" |
 "nullable (Atom c) = False" |
 "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
 "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
 "nullable (Star r) = True" |
 "nullable (NTimes r n) = (if n = 0 then True else nullable r)" |
-"nullable (Upto r n) = True"
-
+"nullable (Upto r n) = True" |
+"nullable (From r n) = (if n = 0 then True else nullable r)" 
 
 lemma pow_empty_iff:
   shows "[] \<in> (lang r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (lang r))"
   by (induct n)(auto)
 
 lemma nullable_iff: 
   shows "nullable r \<longleftrightarrow> [] \<in> lang r"
   by (induct r) (auto simp add: conc_def pow_empty_iff split: if_splits)
 
 end
diff --git a/thys/Regular-Sets/Regular_Set.thy b/thys/Regular-Sets/Regular_Set.thy
--- a/thys/Regular-Sets/Regular_Set.thy
+++ b/thys/Regular-Sets/Regular_Set.thy
@@ -1,456 +1,475 @@
 (*  Author: Tobias Nipkow, Alex Krauss, Christian Urban  *)
 
 section "Regular sets"
 
 theory Regular_Set
 imports Main
 begin
 
 type_synonym 'a lang = "'a list set"
 
 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
 
 text \<open>checks the code preprocessor for set comprehensions\<close>
 export_code conc checking SML
 
 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 begin
   primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
   "lang_pow 0 A = {[]}" |
   "lang_pow (Suc n) A = A @@ (lang_pow n A)"
 end
 
 text \<open>for code generation\<close>
 
 definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
   lang_pow_code_def [code_abbrev]: "lang_pow = compow"
 
 lemma [code]:
   "lang_pow (Suc n) A = A @@ (lang_pow n A)"
   "lang_pow 0 A = {[]}"
   by (simp_all add: lang_pow_code_def)
 
 hide_const (open) lang_pow
 
 definition star :: "'a lang \<Rightarrow> 'a lang" where
 "star A = (\<Union>n. A ^^ n)"
 
 
 subsection\<open>@{term "(@@)"}\<close>
 
 lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"
 by (auto simp add: conc_def)
 
 lemma concE[elim]: 
 assumes "w \<in> A @@ B"
 obtains u v where "u \<in> A" "v \<in> B" "w = u@v"
 using assms by (auto simp: conc_def)
 
 lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> C @@ D"
 by (auto simp: conc_def) 
 
 lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"
 by auto
 
 lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"
 by (simp_all add:conc_def)
 
 lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"
 by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)
 
 lemma conc_Un_distrib:
 shows "A @@ (B \<union> C) = A @@ B \<union> A @@ C"
 and   "(A \<union> B) @@ C = A @@ C \<union> B @@ C"
 by auto
 
 lemma conc_UNION_distrib:
 shows "A @@ \<Union>(M ` I) = \<Union>((%i. A @@ M i) ` I)"
 and   "\<Union>(M ` I) @@ A = \<Union>((%i. M i @@ A) ` I)"
 by auto
 
 lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
 by(fastforce simp: conc_def in_lists_conv_set)
 
 lemma Nil_in_conc[simp]: "[] \<in> A @@ B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
 by (metis append_is_Nil_conv concE concI)
 
 lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A @@ B"
 by (metis append_Nil concI)
 
 lemma conc_Diff_if_Nil1: "[] \<in> A \<Longrightarrow> A @@ B = (A - {[]}) @@ B \<union> B"
 by (fastforce elim: concI_if_Nil1)
 
 lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A @@ B"
 by (metis append_Nil2 concI)
 
 lemma conc_Diff_if_Nil2: "[] \<in> B \<Longrightarrow> A @@ B = A @@ (B - {[]}) \<union> A"
 by (fastforce elim: concI_if_Nil2)
 
 lemma singleton_in_conc:
   "[x] : A @@ B \<longleftrightarrow> [x] : A \<and> [] : B \<or> [] : A \<and> [x] : B"
 by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv
        conc_Diff_if_Nil1 conc_Diff_if_Nil2)
 
 
 subsection\<open>@{term "A ^^ n"}\<close>
 
 lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"
 by (induct n) (auto simp: conc_assoc)
 
 lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"
 by (induct n) auto
 
 lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"
 by (simp add: lang_pow_empty)
 
 lemma conc_pow_comm:
   shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
 by (induct n) (simp_all add: conc_assoc[symmetric])
 
 lemma length_lang_pow_ub:
   "\<forall>w \<in> A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
 by(induct n arbitrary: w) (fastforce simp: conc_def)+
 
 lemma length_lang_pow_lb:
   "\<forall>w \<in> A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
 by(induct n arbitrary: w) (fastforce simp: conc_def)+
 
 lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
 by(induct n)(auto simp: conc_subset_lists)
 
+lemma empty_pow_add:
+  assumes "[] \<in> A" "s \<in> A ^^ n"
+  shows "s \<in> A ^^ (n + m)"
+  using assms
+  apply(induct m arbitrary: n)
+  apply(auto simp add: concI_if_Nil1)
+  done
+
 
 subsection\<open>@{const star}\<close>
 
 lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
 unfolding star_def by(blast dest: lang_pow_subset_lists)
 
 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"
 by (auto simp: star_def)
 
 lemma Nil_in_star[iff]: "[] : star A"
 proof (rule star_if_lang_pow)
   show "[] : A ^^ 0" by simp
 qed
 
 lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"
 proof (rule star_if_lang_pow)
   show "w : A ^^ 1" using \<open>w : A\<close> by simp
 qed
 
 lemma append_in_starI[simp]:
 assumes "u : star A" and "v : star A" shows "u@v : star A"
 proof -
   from \<open>u : star A\<close> obtain m where "u : A ^^ m" by (auto simp: star_def)
   moreover
   from \<open>v : star A\<close> obtain n where "v : A ^^ n" by (auto simp: star_def)
   ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)
   thus ?thesis by simp
 qed
 
 lemma conc_star_star: "star A @@ star A = star A"
 by (auto simp: conc_def)
 
 lemma conc_star_comm:
   shows "A @@ star A = star A @@ A"
 unfolding star_def conc_pow_comm conc_UNION_distrib
 by simp
 
 lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
 assumes "w : star A"
   and "P []"
   and step: "!!u v. u : A \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)"
 shows "P w"
 proof -
   { fix n have "w : A ^^ n \<Longrightarrow> P w"
     by (induct n arbitrary: w) (auto intro: \<open>P []\<close> step star_if_lang_pow) }
   with \<open>w : star A\<close> show "P w" by (auto simp: star_def)
 qed
 
 lemma star_empty[simp]: "star {} = {[]}"
 by (auto elim: star_induct)
 
 lemma star_epsilon[simp]: "star {[]} = {[]}"
 by (auto elim: star_induct)
 
 lemma star_idemp[simp]: "star (star A) = star A"
 by (auto elim: star_induct)
 
 lemma star_unfold_left: "star A = A @@ star A \<union> {[]}" (is "?L = ?R")
 proof
   show "?L \<subseteq> ?R" by (rule, erule star_induct) auto
 qed auto
 
 lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A"
 by (induct ws) simp_all
 
 lemma in_star_iff_concat:
   "w \<in> star A = (\<exists>ws. set ws \<subseteq> A \<and> w = concat ws)"
   (is "_ = (\<exists>ws. ?R w ws)")
 proof
   assume "w : star A" thus "\<exists>ws. ?R w ws"
   proof induct
     case Nil have "?R [] []" by simp
     thus ?case ..
   next
     case (append u v)
     then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast
     with append have "?R (u@v) (u#ws)" by auto
     thus ?case ..
   qed
 next
   assume "\<exists>us. ?R w us" thus "w : star A"
   by (auto simp: concat_in_star)
 qed
 
 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"
 by (fastforce simp: in_star_iff_concat)
 
 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
 proof-
   { fix us
     have "set us \<subseteq> insert [] A \<Longrightarrow> \<exists>vs. concat us = concat vs \<and> set vs \<subseteq> A"
       (is "?P \<Longrightarrow> \<exists>vs. ?Q vs")
     proof
       let ?vs = "filter (%u. u \<noteq> []) us"
       show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto
     qed
   } thus ?thesis by (auto simp: star_conv_concat)
 qed
 
 lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) \<union> {[]}"
 by (metis insert_Diff_single star_insert_eps star_unfold_left)
 
 lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}"
 proof -
   have "[] \<notin> (A - {[]}) @@ star A" by simp
   thus ?thesis using star_unfold_left_Nil by blast
 qed
 
 lemma star_decom: 
   assumes a: "x \<in> star A" "x \<noteq> []"
   shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
 using a by (induct rule: star_induct) (blast)+
 
+lemma star_pow:
+  assumes "s \<in> star A"
+  shows "\<exists>n. s \<in> A ^^ n"
+using assms
+apply(induct)
+apply(rule_tac x="0" in exI)
+apply(auto)
+apply(rule_tac x="Suc n" in exI)
+apply(auto)
+done
+
 
 subsection \<open>Left-Quotients of languages\<close>
 
 definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
   where "Deriv x A = { xs. x#xs \<in> A }"
     
 definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 where "Derivs xs A = { ys. xs @ ys \<in> A }"
 
 abbreviation 
   Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
 where
   "Derivss s As \<equiv> \<Union> (Derivs s ` As)"
 
 
 lemma Deriv_empty[simp]:   "Deriv a {} = {}"
   and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
   and Deriv_char[simp]:    "Deriv a {[b]} = (if a = b then {[]} else {})"
   and Deriv_union[simp]:   "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
   and Deriv_inter[simp]:   "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B"
   and Deriv_compl[simp]:   "Deriv a (-A) = - Deriv a A"
   and Deriv_Union[simp]:   "Deriv a (Union M) = Union(Deriv a ` M)"
   and Deriv_UN[simp]:      "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
 by (auto simp: Deriv_def)
 
 lemma Der_conc [simp]: 
   shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
 unfolding Deriv_def conc_def
 by (auto simp add: Cons_eq_append_conv)
 
 lemma Deriv_star [simp]: 
   shows "Deriv c (star A) = (Deriv c A) @@ star A"
 proof -
   have "Deriv c (star A) = Deriv c ({[]} \<union> A @@ star A)"
     by (metis star_unfold_left sup.commute)
   also have "... = Deriv c (A @@ star A)"
     unfolding Deriv_union by (simp)
   also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
     by simp
   also have "... =  (Deriv c A) @@ star A"
     unfolding conc_def Deriv_def
     using star_decom by (force simp add: Cons_eq_append_conv)
   finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
 qed
 
 lemma Deriv_diff[simp]:   
   shows "Deriv c (A - B) = Deriv c A - Deriv c B"
 by(auto simp add: Deriv_def)
 
 lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S"
 by(auto simp add: Deriv_def)
 
 lemma Derivs_simps [simp]:
   shows "Derivs [] A = A"
   and   "Derivs (c # s) A = Derivs s (Deriv c A)"
   and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
 unfolding Derivs_def Deriv_def by auto
 
 lemma in_fold_Deriv: "v \<in> fold Deriv w L \<longleftrightarrow> w @ v \<in> L"
   by (induct w arbitrary: L) (simp_all add: Deriv_def)
 
 lemma Derivs_alt_def [code]: "Derivs w L = fold Deriv w L"
   by (induct w arbitrary: L) simp_all
 
 lemma Deriv_code [code]: 
   "Deriv x A = tl ` Set.filter (\<lambda>xs. case xs of x' # _ \<Rightarrow> x = x' | _ \<Rightarrow> False) A"
   by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits)
 
 subsection \<open>Shuffle product\<close>
 
 definition Shuffle (infixr "\<parallel>" 80) where
   "Shuffle A B = \<Union>{shuffles xs ys | xs ys. xs \<in> A \<and> ys \<in> B}"
 
 lemma Deriv_Shuffle[simp]:
   "Deriv a (A \<parallel> B) = Deriv a A \<parallel> B \<union> A \<parallel> Deriv a B"
   unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffles_iff neq_Nil_conv)
 
 lemma shuffle_subset_lists:
   assumes "A \<subseteq> lists S" "B \<subseteq> lists S"
   shows "A \<parallel> B \<subseteq> lists S"
 unfolding Shuffle_def proof safe
   fix x and zs xs ys :: "'a list"
   assume zs: "zs \<in> shuffles xs ys" "x \<in> set zs" and "xs \<in> A" "ys \<in> B"
   with assms have "xs \<in> lists S" "ys \<in> lists S" by auto
   with zs show "x \<in> S" by (induct xs ys arbitrary: zs rule: shuffles.induct) auto
 qed
 
 lemma Nil_in_Shuffle[simp]: "[] \<in> A \<parallel> B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
   unfolding Shuffle_def by force
 
 lemma shuffle_Un_distrib:
 shows "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
 and   "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
 unfolding Shuffle_def by fast+
 
 lemma shuffle_UNION_distrib:
 shows "A \<parallel> \<Union>(M ` I) = \<Union>((%i. A \<parallel> M i) ` I)"
 and   "\<Union>(M ` I) \<parallel> A = \<Union>((%i. M i \<parallel> A) ` I)"
 unfolding Shuffle_def by fast+
 
 lemma Shuffle_empty[simp]:
   "A \<parallel> {} = {}"
   "{} \<parallel> B = {}"
   unfolding Shuffle_def by auto
 
 lemma Shuffle_eps[simp]:
   "A \<parallel> {[]} = A"
   "{[]} \<parallel> B = B"
   unfolding Shuffle_def by auto
 
 
 subsection \<open>Arden's Lemma\<close>
 
 lemma arden_helper:
   assumes eq: "X = A @@ X \<union> B"
   shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
 proof (induct n)
   case 0 
   show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)"
     using eq by simp
 next
   case (Suc n)
   have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact
   also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp
   also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
     by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
   also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)"
     by (auto simp add: atMost_Suc)
   finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" .
 qed
 
 lemma Arden:
   assumes "[] \<notin> A" 
   shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B"
 proof
   assume eq: "X = A @@ X \<union> B"
   { fix w assume "w : X"
     let ?n = "size w"
     from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
       by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
     hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
       by (metis length_lang_pow_lb nat_mult_1)
     hence "\<forall>u \<in> A^^(?n+1)@@X. length u \<ge> ?n+1"
       by(auto simp only: conc_def length_append)
     hence "w \<notin> A^^(?n+1)@@X" by auto
     hence "w : star A @@ B" using \<open>w : X\<close> using arden_helper[OF eq, where n="?n"]
       by (auto simp add: star_def conc_UNION_distrib)
   } moreover
   { fix w assume "w : star A @@ B"
     hence "\<exists>n. w \<in> A^^n @@ B" by(auto simp: conc_def star_def)
     hence "w : X" using arden_helper[OF eq] by blast
   } ultimately show "X = star A @@ B" by blast 
 next
   assume eq: "X = star A @@ B"
   have "star A = A @@ star A \<union> {[]}"
     by (rule star_unfold_left)
   then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B"
     by metis
   also have "\<dots> = (A @@ star A) @@ B \<union> B"
     unfolding conc_Un_distrib by simp
   also have "\<dots> = A @@ (star A @@ B) \<union> B" 
     by (simp only: conc_assoc)
   finally show "X = A @@ X \<union> B" 
     using eq by blast 
 qed
 
 
 lemma reversed_arden_helper:
   assumes eq: "X = X @@ A \<union> B"
   shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
 proof (induct n)
   case 0 
   show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))"
     using eq by simp
 next
   case (Suc n)
   have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact
   also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp
   also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
     by (simp add: conc_Un_distrib conc_assoc)
   also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))"
     by (auto simp add: atMost_Suc)
   finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" .
 qed
 
 theorem reversed_Arden:
   assumes nemp: "[] \<notin> A"
   shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A"
 proof
  assume eq: "X = X @@ A \<union> B"
   { fix w assume "w : X"
     let ?n = "size w"
     from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
       by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
     hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
       by (metis length_lang_pow_lb nat_mult_1)
     hence "\<forall>u \<in> X @@ A^^(?n+1). length u \<ge> ?n+1"
       by(auto simp only: conc_def length_append)
     hence "w \<notin> X @@ A^^(?n+1)" by auto
     hence "w : B @@ star A" using \<open>w : X\<close> using reversed_arden_helper[OF eq, where n="?n"]
       by (auto simp add: star_def conc_UNION_distrib)
   } moreover
   { fix w assume "w : B @@ star A"
     hence "\<exists>n. w \<in> B @@ A^^n" by (auto simp: conc_def star_def)
     hence "w : X" using reversed_arden_helper[OF eq] by blast
   } ultimately show "X = B @@ star A" by blast 
 next 
   assume eq: "X = B @@ star A"
   have "star A = {[]} \<union> star A @@ A" 
     unfolding conc_star_comm[symmetric]
     by(metis Un_commute star_unfold_left)
   then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)"
     by metis
   also have "\<dots> = B \<union> B @@ (star A @@ A)"
     unfolding conc_Un_distrib by simp
   also have "\<dots> = B \<union> (B @@ star A) @@ A" 
     by (simp only: conc_assoc)
   finally show "X = X @@ A \<union> B" 
     using eq by blast 
 qed
 
 end