diff --git a/thys/Posix-Lexing/Extensions/Derivatives3.thy b/thys/Posix-Lexing/Extensions/Derivatives3.thy
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/Derivatives3.thy
@@ -0,0 +1,62 @@
+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)))"
+
+fun 
+  derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+where
+  "derivs [] r = r"
+| "derivs (c # s) r = derivs s (deriv c r)"
+
+
+lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
+by (induction r) (auto)
+
+lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> atoms r"
+by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD])
+
+
+
+lemma deriv_pow [simp]:
+  shows "Deriv c (A ^^ n) = (if n = 0 then {} else (Deriv c A) @@ (A ^^ (n - 1)))"
+  apply(induct n arbitrary: A)
+  apply(auto)
+  by (metis Suc_pred concI_if_Nil2 conc_assoc conc_pow_comm lang_pow.simps(2))
+
+lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
+  by (induct r) (simp_all add: nullable_iff)
+  
+
+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
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/Lexer3.thy
@@ -0,0 +1,701 @@
+(*  Title:       POSIX Lexing with Derivatives of Extended Regular Expressions
+    Author:      Christian Urban <christian.urban at kcl.ac.uk>, 2022
+    Maintainer:  Christian Urban <christian.urban at kcl.ac.uk>
+*) 
+
+theory Lexer3
+  imports "Derivatives3"
+begin
+
+section \<open>Values\<close>
+
+datatype 'a val = 
+  Void
+| Atm 'a
+| Seq "'a val" "'a val"
+| Right "'a val"
+| Left "'a val"
+| Stars "('a val) list"
+
+
+section \<open>The string behind a value\<close>
+
+fun 
+  flat :: "'a val \<Rightarrow> 'a list"
+where
+  "flat (Void) = []"
+| "flat (Atm c) = [c]"
+| "flat (Left v) = flat v"
+| "flat (Right v) = flat v"
+| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
+| "flat (Stars []) = []"
+| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
+
+abbreviation
+  "flats vs \<equiv> concat (map flat vs)"
+
+lemma flat_Stars [simp]:
+ "flat (Stars vs) = concat (map flat vs)"
+by (induct vs) (auto)
+
+section \<open>Relation between values and regular expressions\<close>
+
+inductive 
+  Prf :: "'a val \<Rightarrow> 'a rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : Times r1 r2"
+| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : Plus r1 r2"
+| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : Plus r1 r2"
+| "\<turnstile> Void : One"
+| "\<turnstile> Atm c : Atom c"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : Star r"
+| "\<lbrakk>\<forall>v \<in> set vs1. \<turnstile> v : r \<and> flat v \<noteq> []; 
+    \<forall>v \<in> set vs2. \<turnstile> v : r \<and> flat v = []; 
+    length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (vs1 @ vs2) : NTimes r n"
+
+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"
+
+lemma Prf_NTimes_empty:
+  assumes "\<forall>v \<in> set vs. \<turnstile> v : r \<and> flat v = []" 
+  and     "length vs = n"
+  shows "\<turnstile> Stars vs : NTimes r n"
+  using assms
+  by (metis Prf.intros(7) empty_iff eq_Nil_appendI list.set(1))
+  
+
+lemma Seq_decomp:
+  assumes "s \<in> A @@ B"
+  shows "\<exists>s1 s2. s = s1 @ s2 \<and> s1 \<in> A \<and> s2 \<in> B"
+  using assms
+  by blast
+
+lemma NTimes_string:
+  assumes "s \<in> A ^^ n"
+  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> length ss = n"
+using assms
+  apply(induct n arbitrary: s)
+  apply(auto dest!: Seq_decomp)
+  apply(drule_tac x="s2" in meta_spec)
+  apply(auto)
+  apply(rule_tac x="s1 # ss" in exI)
+  apply(simp)
+  done
+
+lemma pow_Prf:
+  assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> A"
+  shows "flats vs \<in> A ^^ (length vs)"
+  using assms
+  by (induct vs) (auto)
+
+lemma Star_string:
+  assumes "s \<in> star A"
+  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
+using assms
+by (metis in_star_iff_concat subsetD)
+
+lemma Star_val:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+  shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> [])"
+using assms
+apply(induct ss)
+apply(auto)
+apply (metis empty_iff list.set(1))
+by (metis append.simps(1) flat.simps(7) flat_Stars set_ConsD)
+
+lemma Aux:
+  assumes "\<forall>s\<in>set ss. s = []"
+  shows "concat ss = []"
+using assms
+by (induct ss) (auto)
+
+lemma Pow_cstring:
+  assumes "s \<in> A ^^ n"
+  shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> 
+         (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])"
+using assms
+apply(induct n arbitrary: s)
+  apply(auto)[1]
+  apply(auto dest!: Seq_decomp simp add: Seq_def)
+  apply(drule_tac x="s2" in meta_spec)
+  apply(simp)
+apply(erule exE)+
+  apply(clarify)
+apply(case_tac "s1 = []")
+apply(simp)
+apply(rule_tac x="ss1" in exI)
+apply(rule_tac x="s1 # ss2" in exI)
+apply(simp)
+apply(rule_tac x="s1 # ss1" in exI)
+apply(rule_tac x="ss2" in exI)
+  apply(simp)
+  done
+
+lemma flats_cval:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+  shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> 
+          (\<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(rule_tac x="v#vs2" in exI)
+apply(simp)
+apply(rule_tac x="vs1 @ [v]" in exI)
+apply(rule_tac x="vs2" in exI)
+apply(simp)
+by (simp add: Aux)
+
+lemma Prf_flat_lang:
+  assumes "\<turnstile> v : r" shows "flat v \<in> lang r"
+using assms
+  apply (induct v r rule: Prf.induct) 
+  apply (auto simp add: concat_in_star subset_eq lang_pow_add)
+  by (meson concI pow_Prf)
+    
+lemma L_flat_Prf2:
+  assumes "s \<in> lang r" 
+  shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
+using assms
+proof(induct r arbitrary: s)
+  case (Star r s)
+  have IH: "\<And>s. s \<in> lang r \<Longrightarrow> \<exists>v.\<turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> lang (Star r)" by fact
+  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> lang r \<and> s \<noteq> []"
+    by (smt (z3) IH Prf_flat_lang Star_val imageE in_star_iff_concat lang.simps(6) list.set_map subset_iff)  
+  then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<noteq> []"
+  using IH by (metis Star_val) 
+  then show "\<exists>v. \<turnstile> v : Star r \<and> flat v = s"
+  using Prf.intros(6) flat_Stars by blast
+next 
+  case (Times r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : Times r1 r2 \<and> flat v = s"
+  unfolding Seq_def lang.simps by (fastforce intro: Prf.intros)
+next
+  case (Plus r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : Plus r1 r2 \<and> flat v = s"
+  unfolding lang.simps by (fastforce intro: Prf.intros)
+next
+  case (NTimes r n)
+  have IH: "\<And>s. s \<in> lang r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> lang (NTimes r n)" by fact
+  then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" 
+    "\<forall>s \<in> set ss1. s \<in> lang r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> lang r \<and> s = []"
+  using Pow_cstring by force
+  then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" 
+      "\<forall>v\<in>set vs1. \<turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<turnstile> v : r \<and> flat v = []"
+    using IH flats_cval 
+  apply -
+  apply(drule_tac x="ss1 @ ss2" in meta_spec)
+  apply(drule_tac x="r" in meta_spec)
+  apply(drule meta_mp)
+  apply(simp)
+  apply (metis Un_iff)
+  apply(clarify)
+  apply(drule_tac x="vs1" in meta_spec)
+  apply(drule_tac x="vs2" in meta_spec)
+  apply(simp)
+  done
+  then show "\<exists>v. \<turnstile> v : NTimes r n \<and> flat v = s"
+  using Prf.intros(7) flat_Stars by blast
+qed (auto intro: Prf.intros)
+
+lemma L_flat_Prf:
+  "lang r = {flat v | v. \<turnstile> v : r}"
+  using L_flat_Prf2 Prf_flat_lang by blast
+
+
+section \<open>Sulzmann and Lu functions\<close>
+
+fun 
+  mkeps :: "'a rexp \<Rightarrow> 'a val"
+where
+  "mkeps(One) = Void"
+| "mkeps(Times r1 r2) = Seq (mkeps r1) (mkeps r2)"
+| "mkeps(Plus r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+| "mkeps(Star r) = Stars []"
+| "mkeps(NTimes r n) = Stars (replicate n (mkeps r))"  
+
+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)" 
+
+section \<open>Mkeps, injval\<close>
+
+lemma mkeps_flat:
+  assumes "nullable(r)" 
+  shows "flat (mkeps r) = []"
+using assms
+  by (induct rule: mkeps.induct) (auto)
+
+lemma mkeps_nullable:
+  assumes "nullable r" 
+  shows "\<turnstile> mkeps r : r"
+using assms
+  apply (induct r) 
+  apply (auto intro: Prf.intros split: if_splits)
+  apply (metis Prf.intros(7) append_Nil2 in_set_replicate list.size(3) replicate_0)
+  apply(rule Prf_NTimes_empty)
+  apply(auto simp add: mkeps_flat)
+  done
+
+lemma Prf_injval_flat:
+  assumes "\<turnstile> v : deriv c r" 
+  shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct c r arbitrary: v rule: deriv.induct)
+apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
+done
+
+lemma Prf_injval:
+  assumes "\<turnstile> v : deriv c r" 
+  shows "\<turnstile> (injval r c v) : r"
+using assms
+apply(induct r arbitrary: c v rule: rexp.induct)
+apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
+(* Star *)
+apply (simp add: Prf_injval_flat)
+(* NTimes *)
+  apply(case_tac x2)
+    apply(simp)
+  apply(simp)
+  apply(subst append.simps(2)[symmetric])
+  apply(rule Prf.intros)
+  apply(auto simp add: Prf_injval_flat)
+  done
+
+section \<open>Our Alternative Posix definition\<close>
+
+inductive 
+  Posix :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+where
+  Posix_One: "[] \<in> One \<rightarrow> Void"
+| Posix_Atom: "[c] \<in> (Atom c) \<rightarrow> (Atm c)"
+| Posix_Plus1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Left v)"
+| Posix_Plus2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> lang r1\<rbrakk> \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Right v)"
+| Posix_Times: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
+    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)\<rbrakk> \<Longrightarrow> 
+    (s1 @ s2) \<in> (Times r1 r2) \<rightarrow> (Seq v1 v2)"
+| Posix_Star1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> Star r \<rightarrow> Stars vs; flat v \<noteq> [];
+    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> lang r \<and> s\<^sub>4 \<in> lang (Star r))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> Star r \<rightarrow> Stars (v # vs)"
+| Posix_Star2: "[] \<in> Star r \<rightarrow> Stars []"
+| Posix_NTimes1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTimes r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n;
+    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NTimes r n \<rightarrow> Stars (v # vs)"
+| Posix_NTimes2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
+    \<Longrightarrow> [] \<in> NTimes r n \<rightarrow> Stars vs"  
+
+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"
+
+lemma Posix1:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "s \<in> lang r" "flat v = s"
+using assms
+  apply (induct s r v rule: Posix.induct) 
+  apply(auto simp add: pow_empty_iff)
+  apply (metis Suc_pred concI lang_pow.simps(2))
+  by (meson ex_in_conv set_empty)
+
+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)
+  done
+      
+
+lemma Posix_mkeps:
+  assumes "nullable r"
+  shows "[] \<in> r \<rightarrow> mkeps r"
+using assms
+apply(induct r)
+apply(auto intro: Posix.intros simp add: nullable_iff)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+  by (simp add: Posix_NTimes2 pow_empty_iff)
+
+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
+qed
+
+
+lemma Posix_injval:
+  assumes "s \<in> (deriv c r) \<rightarrow> v"
+  shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
+using assms
+proof(induct r arbitrary: s v rule: rexp.induct)
+  case Zero
+  have "s \<in> deriv c Zero \<rightarrow> v" by fact
+  then have "s \<in> Zero \<rightarrow> v" by simp
+  then have "False" by cases
+  then show "(c # s) \<in> Zero \<rightarrow> (injval Zero c v)" by simp
+next
+  case One
+  have "s \<in> deriv c One \<rightarrow> v" by fact
+  then have "s \<in> Zero \<rightarrow> v" by simp
+  then have "False" by cases
+  then show "(c # s) \<in> One \<rightarrow> (injval One c v)" by simp
+next 
+  case (Atom d)
+  consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
+  then show "(c # s) \<in> (Atom d) \<rightarrow> (injval (Atom d) c v)"
+  proof (cases)
+    case eq
+    have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact
+    then have "s \<in> One \<rightarrow> v" using eq by simp
+    then have eqs: "s = [] \<and> v = Void" by cases simp
+    show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" using eq eqs 
+    by (auto intro: Posix.intros)
+  next
+    case ineq
+    have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact
+    then have "s \<in> Zero \<rightarrow> v" using ineq by simp
+    then have "False" by cases
+    then show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" by simp
+  qed
+next
+  case (Plus r1 r2)
+  have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+  have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+  have "s \<in> deriv c (Plus r1 r2) \<rightarrow> v" by fact
+  then have "s \<in> Plus (deriv c r1) (deriv c r2) \<rightarrow> v" by simp
+  then consider (left) v' where "v = Left v'" "s \<in> deriv c r1 \<rightarrow> v'" 
+              | (right) v' where "v = Right v'" "s \<notin> lang (deriv c r1)" "s \<in> deriv c r2 \<rightarrow> v'" 
+              by cases auto
+  then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v"
+  proof (cases)
+    case left
+    have "s \<in> deriv c r1 \<rightarrow> v'" by fact
+    then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
+    then have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Left v')" by (auto intro: Posix.intros)
+    then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using left by simp
+  next 
+    case right
+    have "s \<notin> lang (deriv c r1)" by fact
+    then have "c # s \<notin> lang r1" by (simp add: lang_deriv Deriv_def)
+    moreover 
+    have "s \<in> deriv c r2 \<rightarrow> v'" by fact
+    then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
+    ultimately have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Right v')" 
+      by (auto intro: Posix.intros)
+    then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using right by simp
+  qed
+next
+  case (Times r1 r2)
+  have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+  have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+  have "s \<in> deriv c (Times r1 r2) \<rightarrow> v" by fact
+  then consider 
+        (left_nullable) v1 v2 s1 s2 where 
+        "v = Left (Seq v1 v2)"  "s = s1 @ s2" 
+        "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" 
+        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)"
+      | (right_nullable) v1 s1 s2 where 
+        "v = Right v1" "s = s1 @ s2"  
+        "s \<in> deriv c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)"
+      | (not_nullable) v1 v2 s1 s2 where
+        "v = Seq v1 v2" "s = s1 @ s2" 
+        "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" 
+        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)"
+        by (force split: if_splits elim!: Posix_elims simp add: lang_deriv Deriv_def)   
+  then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" 
+    proof (cases)
+      case left_nullable
+      have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact
+      then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+      moreover
+      have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" by fact
+      then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" 
+         by (simp add: lang_deriv Deriv_def)
+      ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
+      then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using left_nullable by simp
+    next
+      case right_nullable
+      have "nullable r1" by fact
+      then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
+      moreover
+      have "s \<in> deriv c r2 \<rightarrow> v1" by fact
+      then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
+      moreover
+      have "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)" by fact
+      then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" 
+        using right_nullable 
+        apply (auto simp add: lang_deriv Deriv_def append_eq_Cons_conv)
+        by (metis concI mem_Collect_eq)
+      ultimately have "([] @ (c # s)) \<in> Times r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
+      by(rule Posix.intros)
+      then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using right_nullable by simp
+    next
+      case not_nullable
+      have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact
+      then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+      moreover
+      have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" by fact
+      then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by (simp add: lang_deriv Deriv_def)
+      ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable 
+        by (rule_tac Posix.intros) (simp_all) 
+      then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using not_nullable by simp
+    qed
+next
+  case (Star r)
+  have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+  have "s \<in> deriv c (Star r) \<rightarrow> v" by fact
+  then consider
+      (cons) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (Star r) \<rightarrow> (Stars vs)"
+        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" 
+        apply(auto elim!: Posix_elims(1-5) simp add: lang_deriv Deriv_def intro: Posix.intros)
+        apply(rotate_tac 3)
+        apply(erule_tac Posix_elims(6))
+        apply (simp add: Posix.intros(6))
+        using Posix.intros(7) by blast
+    then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" 
+    proof (cases)
+      case cons
+          have "s1 \<in> deriv c r \<rightarrow> v1" by fact
+          then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+        moreover
+          have "s2 \<in> Star r \<rightarrow> Stars vs" by fact
+        moreover 
+          have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
+          then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+          then have "flat (injval r c v1) \<noteq> []" by simp
+        moreover 
+          have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" by fact
+          then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Star r))" 
+            by (simp add: lang_deriv Deriv_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> Star r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
+        then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" using cons by(simp)
+      qed
+next
+  case (NTimes r n)
+  have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+  have "s \<in> deriv c (NTimes r n) \<rightarrow> v" by fact
+  then consider
+      (cons) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (NTimes r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
+        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))" 
+    apply(auto elim: Posix_elims simp add: lang_derivs Deriv_def intro: Posix.intros split: if_splits)
+    apply(erule Posix_elims)
+    apply(simp)
+    apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+    apply(clarify)
+    apply(drule_tac x="vss" in meta_spec)
+    apply(drule_tac x="s1" in meta_spec)
+    apply(drule_tac x="s2" in meta_spec)
+     apply(simp add: lang_derivs Deriv_def)
+    apply(erule Posix_elims)
+     apply(auto)
+      done
+    then show "(c # s) \<in> (NTimes r n) \<rightarrow> injval (NTimes r n) c v" 
+    proof (cases)
+      case cons
+          have "s1 \<in> deriv c r \<rightarrow> v1" by fact
+          then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+        moreover
+          have "s2 \<in> (NTimes r (n - 1)) \<rightarrow> Stars vs" by fact
+        moreover 
+          have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
+          then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+          then have "flat (injval r c v1) \<noteq> []" by simp
+        moreover 
+          have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))" by fact
+          then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (NTimes r (n - 1)))"
+            by (simp add: lang_deriv Deriv_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> NTimes r n \<rightarrow> Stars (injval r c v1 # vs)" 
+           apply (rule_tac Posix.intros)
+               apply(simp_all)
+              apply(case_tac n)
+            apply(simp)
+           using Posix_elims(1) NTimes.prems apply auto[1]
+             apply(simp)
+             done
+        then show "(c # s) \<in> NTimes r n \<rightarrow> injval (NTimes r n) c v" using cons by(simp)
+      qed  
+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
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/LexicalVals3.thy
@@ -0,0 +1,248 @@
+theory LexicalVals3
+  imports Lexer3 "HOL-Library.Sublist"
+begin
+
+section \<open> Sets of Lexical Values \<close>
+
+text \<open>
+  Shows that lexical values are finite for a given regex and string.
+\<close>
+
+definition
+  LV :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) set"
+where  "LV r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
+
+lemma LV_simps:
+  shows "LV Zero s = {}"
+  and   "LV One s = (if s = [] then {Void} else {})"
+  and   "LV (Atom c) s = (if s = [c] then {Atm c} else {})"
+  and   "LV (Plus r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
+  and   "LV (NTimes r 0) s = (if s = [] then {Stars []} else {})"
+unfolding LV_def
+  apply(auto intro: Prf.intros elim: Prf.cases)
+  by (simp add: Prf_NTimes_empty)
+  
+
+abbreviation
+  "Prefixes s \<equiv> {s'. prefix s' s}"
+
+abbreviation
+  "Suffixes s \<equiv> {s'. suffix s' s}"
+
+abbreviation
+  "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
+
+lemma Suffixes_cons [simp]:
+  shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
+by (auto simp add: suffix_def Cons_eq_append_conv)
+
+
+lemma finite_Suffixes: 
+  shows "finite (Suffixes s)"
+by (induct s) (simp_all)
+
+lemma finite_SSuffixes: 
+  shows "finite (SSuffixes s)"
+proof -
+  have "SSuffixes s \<subseteq> Suffixes s"
+   unfolding strict_suffix_def suffix_def by auto
+  then show "finite (SSuffixes s)"
+   using finite_Suffixes finite_subset by blast
+qed
+
+lemma finite_Prefixes: 
+  shows "finite (Prefixes s)"
+proof -
+  have "finite (Suffixes (rev s))" 
+    by (rule finite_Suffixes)
+  then have "finite (rev ` Suffixes (rev s))" by simp
+  moreover
+  have "rev ` (Suffixes (rev s)) = Prefixes s"
+  unfolding suffix_def prefix_def image_def
+   by (auto)(metis rev_append rev_rev_ident)+
+  ultimately show "finite (Prefixes s)" by simp
+qed
+
+lemma LV_STAR_finite:
+  assumes "\<forall>s. finite (LV r s)"
+  shows "finite (LV (Star r) s)"
+proof(induct s rule: length_induct)
+  fix s::"'a list"
+  assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (Star r) s')"
+  then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (Star r) s')"
+    by (force simp add: strict_suffix_def suffix_def) 
+  define f where "f \<equiv> \<lambda>(v::'a val, vs). Stars (v # vs)"
+  define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
+  define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (Star r) s2)"
+  have "finite S1" using assms
+    unfolding S1_def by (simp_all add: finite_Prefixes)
+  moreover 
+  with IH have "finite S2" unfolding S2_def
+    by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
+  ultimately 
+  have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
+  moreover 
+  have "LV (Star r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
+  unfolding S1_def S2_def f_def
+  unfolding LV_def image_def prefix_def strict_suffix_def 
+  apply(auto)
+  apply(case_tac x)
+  apply(auto elim: Prf_elims)
+  apply(erule Prf_elims)
+  apply(auto)
+  apply(case_tac vs)
+  apply(auto intro: Prf.intros)  
+  apply(rule exI)
+  apply(rule conjI)
+  apply(rule_tac x="flat a" in exI)
+  apply(rule conjI)
+  apply(rule_tac x="flats list" in exI)
+  apply(simp)
+  apply(blast)
+  apply(simp add: suffix_def)
+  using Prf.intros(6) by blast  
+  ultimately
+  show "finite (LV (Star r) s)" by (simp add: finite_subset)
+qed  
+
+definition
+  "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
+
+lemma finite_Stars_Append:
+  assumes "finite Vs1" "finite Vs2"
+  shows "finite (Stars_Append Vs1 Vs2)"
+  using assms  
+proof -
+  define UVs1 where "UVs1 \<equiv> Stars -` Vs1"
+  define UVs2 where "UVs2 \<equiv> Stars -` Vs2"  
+  from assms have "finite UVs1" "finite UVs2"
+    unfolding UVs1_def UVs2_def
+    by(simp_all add: finite_vimageI inj_on_def) 
+  then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"
+    by simp
+  moreover 
+    have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"
+    unfolding Stars_Append_def UVs1_def UVs2_def by auto    
+  ultimately show "finite (Stars_Append Vs1 Vs2)"   
+    by simp
+qed 
+
+lemma LV_NTimes_5:
+  "LV (NTimes r n) s \<subseteq> Stars_Append (LV (Star r) s) (\<Union>i\<le>n. LV (NTimes r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+  apply(auto simp add: Stars_Append_def)
+  apply(rule_tac x="vs1" in exI)
+  apply(rule_tac x="vs2" in exI)  
+  apply(auto)
+    using Prf.intros(6) apply(auto)
+      apply(rule_tac x="length vs2" in bexI)
+    thm Prf.intros
+      apply(subst append.simps(1)[symmetric])
+    apply(rule Prf.intros)
+      apply(auto)[1]
+      apply(auto)[1]
+     apply(simp)
+    apply(simp)
+      done
+
+lemma LV_NTIMES_3:
+  shows "LV (NTimes r (Suc n)) [] = 
+     (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTimes r n) [])))"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+  done 
+
+lemma finite_NTimes_empty:
+  assumes "\<And>s. finite (LV r s)" 
+  shows "finite (LV (NTimes r n) [])"
+  using assms
+  apply(induct n)
+   apply(auto simp add: LV_simps)
+  apply(subst LV_NTIMES_3)
+  apply(rule finite_imageI)
+  apply(rule finite_cartesian_product)
+  using assms apply simp 
+  apply(rule finite_vimageI)
+  apply(simp)
+  apply(simp add: inj_on_def)
+  done
+
+lemma 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)
+qed
+
+
+
+text \<open>
+  Our POSIX values are lexical values.
+\<close>
+
+lemma Posix_LV:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "v \<in> LV r s"
+  using assms unfolding LV_def
+  apply(induct rule: Posix.induct)
+          apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a)
+  apply (smt (verit, best) One_nat_def Posix1a Posix_NTimes1 lang.simps(7))
+  using Prf_NTimes_empty by blast
+
+lemma Posix_Prf:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<turnstile> v : r"
+  using assms Posix_LV LV_def
+  by blast
+
+
+end
\ No newline at end of file
diff --git a/thys/Posix-Lexing/Extensions/Positions3.thy b/thys/Posix-Lexing/Extensions/Positions3.thy
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/Positions3.thy
@@ -0,0 +1,861 @@
+   
+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    
+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
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/Regular_Exps3.thy
@@ -0,0 +1,54 @@
+(* 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"
+
+
+primrec 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)" 
+
+
+lemma lang_subset_lists: 
+  "atoms r \<subseteq> A \<Longrightarrow> lang r \<subseteq> lists A"
+  by (induction r)
+     (auto simp: conc_subset_lists star_subset_lists lang_pow_subset_lists)
+  
+
+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)"
+
+
+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/Posix-Lexing/Extensions/Simplifying3.thy b/thys/Posix-Lexing/Extensions/Simplifying3.thy
new file mode 100644
--- /dev/null
+++ b/thys/Posix-Lexing/Extensions/Simplifying3.thy
@@ -0,0 +1,236 @@
+(*  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 Simplifying3
+  imports Lexer3 
+begin
+
+section \<open>Lexer including simplifications\<close>
+
+
+fun F_RIGHT where
+  "F_RIGHT f v = Right (f v)"
+
+fun F_LEFT where
+  "F_LEFT f v = Left (f v)"
+
+fun F_Plus where
+  "F_Plus f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"
+| "F_Plus f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  
+| "F_Plus f1 f2 v = v"
+
+
+fun F_Times1 where
+  "F_Times1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"
+
+fun F_Times2 where 
+  "F_Times2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"
+
+fun F_Times where 
+  "F_Times f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"
+| "F_Times f1 f2 v = v"
+
+fun simp_Plus where
+  "simp_Plus (Zero, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"
+| "simp_Plus (r\<^sub>1, f\<^sub>1) (Zero, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
+| "simp_Plus (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (Plus r\<^sub>1 r\<^sub>2, F_Plus f\<^sub>1 f\<^sub>2)"
+
+fun simp_Times where
+  "simp_Times (One, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_Times1 f\<^sub>1 f\<^sub>2)"
+| "simp_Times (r\<^sub>1, f\<^sub>1) (One, f\<^sub>2) = (r\<^sub>1, F_Times2 f\<^sub>1 f\<^sub>2)"
+| "simp_Times (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (Times r\<^sub>1 r\<^sub>2, F_Times f\<^sub>1 f\<^sub>2)"  
+ 
+lemma simp_Times_simps[simp]:
+  "simp_Times p1 p2 = (if (fst p1 = One) then (fst p2, F_Times1 (snd p1) (snd p2))
+                    else (if (fst p2 = One) then (fst p1, F_Times2 (snd p1) (snd p2))
+                    else (Times (fst p1) (fst p2), F_Times (snd p1) (snd p2))))"
+by (induct p1 p2 rule: simp_Times.induct) (auto)
+
+lemma simp_Plus_simps[simp]:
+  "simp_Plus p1 p2 = (if (fst p1 = Zero) then (fst p2, F_RIGHT (snd p2))
+                    else (if (fst p2 = Zero) then (fst p1, F_LEFT (snd p1))
+                    else (Plus (fst p1) (fst p2), F_Plus (snd p1) (snd p2))))"
+by (induct p1 p2 rule: simp_Plus.induct) (auto)
+
+fun 
+  simp :: "'a rexp \<Rightarrow> 'a rexp * ('a val \<Rightarrow> 'a val)"
+where
+  "simp (Plus r1 r2) = simp_Plus (simp r1) (simp r2)" 
+| "simp (Times r1 r2) = simp_Times (simp r1) (simp r2)" 
+| "simp r = (r, id)"
+
+fun 
+  slexer :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) option"
+where
+  "slexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "slexer r (c#s) = (let (rs, fr) = simp (deriv c r) in
+                         (case (slexer rs s) of  
+                            None \<Rightarrow> None
+                          | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
+
+lemma slexer_better_simp:
+  "slexer r (c#s) = (case (slexer (fst (simp (deriv c r))) s) of  
+                            None \<Rightarrow> None
+                          | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (deriv c r))) v)))"
+by (auto split: prod.split option.split)
+
+
+lemma L_fst_simp:
+  shows "lang r = lang (fst (simp r))"
+by (induct r) (auto)
+
+lemma Posix_simp:
+  assumes "s \<in> (fst (simp r)) \<rightarrow> v" 
+  shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
+using assms
+proof(induct r arbitrary: s v rule: rexp.induct)
+  case (Plus r1 r2 s v)
+  have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+  have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+  have as: "s \<in> fst (simp (Plus r1 r2)) \<rightarrow> v" by fact
+  consider (Zero_Zero) "fst (simp r1) = Zero" "fst (simp r2) = Zero"
+         | (Zero_NZero) "fst (simp r1) = Zero" "fst (simp r2) \<noteq> Zero"
+         | (NZero_Zero) "fst (simp r1) \<noteq> Zero" "fst (simp r2) = Zero"
+         | (NZero_NZero) "fst (simp r1) \<noteq> Zero" "fst (simp r2) \<noteq> Zero" by auto
+  then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" 
+    proof(cases)
+      case (Zero_Zero)
+      with as have "s \<in> Zero \<rightarrow> v" by simp 
+      then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" by (rule Posix_elims(1))
+    next
+      case (Zero_NZero)
+      with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp
+      with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp
+      moreover
+      from Zero_NZero have "fst (simp r1) = Zero" by simp
+      then have "lang (fst (simp r1)) = {}" by simp
+      then have "lang r1 = {}" using L_fst_simp by auto
+      then have "s \<notin> lang r1" by simp 
+      ultimately have "s \<in> Plus r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_Plus2)
+      then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v"
+      using Zero_NZero by simp
+    next
+      case (NZero_Zero)
+      with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+      with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+      then have "s \<in> Plus r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_Plus1) 
+      then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_Zero by simp
+    next
+      case (NZero_NZero)
+      with as have "s \<in> Plus (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+      then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1"
+                  | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> lang (fst (simp r1))"
+                  by (erule_tac Posix_elims(4)) 
+      then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v"
+      proof(cases)
+        case (Left)
+        then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all
+        then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_NZero
+          by (simp_all add: Posix_Plus1)
+      next 
+        case (Right)
+        then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> lang r1" using IH2 L_fst_simp by auto
+        then show "s \<in> Plus r1 r2 \<rightarrow> snd (simp (Plus r1 r2)) v" using NZero_NZero
+          by (simp_all add: Posix_Plus2)
+      qed
+    qed
+next
+  case (Times r1 r2 s v)
+  have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+  have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+  have as: "s \<in> fst (simp (Times r1 r2)) \<rightarrow> v" by fact
+  consider (One_One) "fst (simp r1) = One" "fst (simp r2) = One"
+         | (One_NOne) "fst (simp r1) = One" "fst (simp r2) \<noteq> One"
+         | (NOne_One) "fst (simp r1) \<noteq> One" "fst (simp r2) = One"
+         | (NOne_NOne) "fst (simp r1) \<noteq> One" "fst (simp r2) \<noteq> One" by auto
+  then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" 
+  proof(cases)
+      case (One_One)
+      with as have b: "s \<in> One \<rightarrow> v" by simp 
+      from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 One_One by simp
+      moreover
+      from b have c: "s = []" "v = Void" using Posix_elims(2) by auto
+      moreover
+      have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One)
+      then have "[] \<in> fst (simp r2) \<rightarrow> Void" using One_One by simp
+      then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+      ultimately have "([] @ []) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)"
+        using Posix_Times by blast 
+      then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using c One_One by simp
+    next
+      case (One_NOne)
+      with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp 
+      from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 One_NOne by simp
+      moreover
+      have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One)
+      then have "[] \<in> fst (simp r1) \<rightarrow> Void" using One_NOne by simp
+      then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp
+      moreover
+      from One_NOne(1) have "lang (fst (simp r1)) = {[]}" by simp
+      then have "lang r1 = {[]}" by (simp add: L_fst_simp[symmetric])
+      ultimately have "([] @ s) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)"
+        by(rule_tac Posix_Times) auto
+      then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using One_NOne by simp
+    next
+      case (NOne_One)
+        with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+        with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+      moreover
+        have "[] \<in> One \<rightarrow> Void" by (simp add: Posix_One)
+        then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NOne_One by simp
+        then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+      ultimately have "(s @ []) \<in> Times r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)"
+        by(rule_tac Posix_Times) auto
+      then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using NOne_One by simp
+    next
+      case (NOne_NOne)
+      with as have "s \<in> Times (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+      then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2"
+                     "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp 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 (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) 
+      then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)"
+        using IH1 IH2 by auto             
+      then show "s \<in> Times r1 r2 \<rightarrow> snd (simp (Times r1 r2)) v" using eqs NOne_NOne
+        by(auto intro: Posix_Times)
+    qed
+qed (simp_all)
+
+
+lemma slexer_correctness:
+  shows "slexer r s = lexer r s"
+proof(induct s arbitrary: r)
+  case Nil
+  show "slexer r [] = lexer r []" by simp
+next 
+  case (Cons c s r)
+  have IH: "\<And>r. slexer r s = lexer r s" by fact
+  show "slexer r (c # s) = lexer r (c # s)" 
+   proof (cases "s \<in> lang (deriv c r)")
+     case True
+       assume a1: "s \<in> lang (deriv c r)"
+       then obtain v1 where a2: "lexer (deriv c r) s = Some v1" "s \<in> deriv c r \<rightarrow> v1"
+         using lexer_correct_Some by auto
+       from a1 have "s \<in> lang (fst (simp (deriv c r)))" using L_fst_simp[symmetric] by auto
+       then obtain v2 where a3: "lexer (fst (simp (deriv c r))) s = Some v2" "s \<in> (fst (simp (deriv c r))) \<rightarrow> v2"
+          using lexer_correct_Some by auto
+       then have a4: "slexer (fst (simp (deriv c r))) s = Some v2" using IH by simp
+       from a3(2) have "s \<in> deriv c r \<rightarrow> (snd (simp (deriv c r))) v2" using Posix_simp by auto
+       with a2(2) have "v1 = (snd (simp (deriv c r))) v2" using Posix_determ by auto
+       with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split)
+     next 
+     case False
+       assume b1: "s \<notin> lang (deriv c r)"
+       then have "lexer (deriv c r) s = None" using lexer_correct_None by auto
+       moreover
+       from b1 have "s \<notin> lang (fst (simp (deriv c r)))" using L_fst_simp[symmetric] by auto
+       then have "lexer (fst (simp (deriv c r))) s = None" using lexer_correct_None by auto
+       then have "slexer (fst (simp (deriv c r))) s = None" using IH by simp
+       ultimately show "slexer r (c # s) = lexer r (c # s)" 
+         by (simp del: slexer.simps add: slexer_better_simp)
+   qed
+qed  
+
+end
diff --git a/thys/Posix-Lexing/ROOT b/thys/Posix-Lexing/ROOT
--- a/thys/Posix-Lexing/ROOT
+++ b/thys/Posix-Lexing/ROOT
@@ -1,16 +1,25 @@
 chapter AFP
 
 session "Posix-Lexing" (AFP) = "Regular-Sets" +
 
   options [timeout = 600]
 
+  directories
+    "Extensions"
+    
   theories
     Lexer
     LexicalVals
     Simplifying
     Positions
+    "Extensions/Regular_Exps3"
+    "Extensions/Derivatives3"
+    "Extensions/Lexer3"
+    "Extensions/LexicalVals3"
+    "Extensions/Simplifying3"
+    "Extensions/Positions3"
     
   document_files
     "root.bib"
     "root.tex"