diff -r 32b222d77fa0 -r 6746f5e1f1f8 thys/Positions.thy
--- a/thys/Positions.thy	Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Positions.thy	Fri Aug 18 14:51:29 2017 +0100
@@ -1,6 +1,6 @@
    
 theory Positions
-  imports "Spec" 
+  imports "Spec" "Lexer" 
 begin
 
 section {* Positions in Values *}
@@ -38,30 +38,9 @@
   shows "[] \<in> Pos v"
 by (induct v rule: Pos.induct)(auto)
 
-fun intlen :: "'a list \<Rightarrow> int"
-where
-  "intlen [] = 0"
-| "intlen (x # xs) = 1 + intlen xs"
-
-lemma intlen_int:
-  shows "intlen xs = int (length xs)"
-by (induct xs)(simp_all)
+abbreviation
+  "intlen vs \<equiv> int (length vs)"
 
-lemma intlen_bigger:
-  shows "0 \<le> intlen xs"
-by (induct xs)(auto)
-
-lemma intlen_append:
-  shows "intlen (xs @ ys) = intlen xs + intlen ys"
-by (simp add: intlen_int)
-
-lemma intlen_length:
-  shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
-by (simp add: intlen_int)
-
-lemma intlen_length_eq:
-  shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
-by (simp add: intlen_int)
 
 definition pflat_len :: "val \<Rightarrow> nat list => int"
 where
@@ -165,27 +144,118 @@
   "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 
+
+text {*
+  :\<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_irrefl apply blast
+using PosOrd_assym apply blast
+using PosOrd_trans 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)
+unfolding ordering_def
+by blast
+
+
+lemma PosOrd_ex_eq2:
+  shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
+using PosOrd_ordering 
+unfolding ordering_def
+by auto
+
+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 blast
+
+lemma PosOrdeq_antisym:
+  assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
+  shows "v1 = v2"
+using assms PosOrd_ordering 
+unfolding ordering_def
+by blast
+
+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 simp add: pflat_len_def intlen_int split: if_splits)
+apply(auto simp add: pflat_len_def split: if_splits)
 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
 
 lemma PosOrd_shorterI:
   assumes "length (flat v2) < length (flat v1)"
-  shows "v1 :\<sqsubset>val v2" 
-using assms
-unfolding PosOrd_ex_def
-by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
+  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)
-by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
+unfolding prefix_list_def sprefix_list_def
+by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
 
 
 lemma PosOrd_Left_Right:
@@ -194,7 +264,7 @@
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
 using assms 
-apply(auto simp add: PosOrd_def pflat_len_simps intlen_int)
+apply(auto simp add: PosOrd_def pflat_len_simps)
 done
 
 lemma PosOrd_Left_eq:
@@ -219,7 +289,7 @@
 
 lemma PosOrd_RightI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
-  shows "(Right v) :\<sqsubset>val (Right v')" 
+  shows "Right v :\<sqsubset>val Right v'" 
 using assms(1)
 unfolding PosOrd_ex_def
 apply(auto)
@@ -229,7 +299,7 @@
 done
 
 lemma PosOrd_RightE:
-  assumes "(Right v1) :\<sqsubset>val (Right v2)"
+  assumes "Right v1 :\<sqsubset>val Right v2"
   shows "v1 :\<sqsubset>val v2"
 using assms
 apply(simp add: PosOrd_ex_def)
@@ -258,7 +328,7 @@
 
 lemma PosOrd_SeqI1:
   assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
-  shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
+  shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
@@ -275,12 +345,12 @@
 apply(simp add: pflat_len_simps)
 using assms(2)
 apply(simp)
-apply(auto simp add: pflat_len_simps)[2]
-done
+apply(auto simp add: pflat_len_simps)
+by (metis length_append of_nat_add)
 
 lemma PosOrd_SeqI2:
   assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
-  shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" 
+  shows "Seq v v2 :\<sqsubset>val Seq v v2'" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
@@ -301,21 +371,21 @@
 done
 
 lemma PosOrd_SeqE:
-  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
+  assumes "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" 
   shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
 using assms
 apply(simp add: PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac p)
 apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps intlen_append)[1]
+apply(auto simp add: pflat_len_simps)[1]
 apply(rule_tac x="[]" in exI)
 apply(drule_tac x="[]" in spec)
 apply(simp add: Pos_empty pflat_len_simps)
 apply(case_tac a)
 apply(rule disjI1)
 apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps intlen_append)[1]
+apply(auto simp add: pflat_len_simps)[1]
 apply(rule_tac x="list" in exI)
 apply(simp)
 apply(rule ballI)
@@ -326,7 +396,7 @@
 apply(case_tac nat)
 apply(rule disjI2)
 apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps intlen_append)
+apply(auto simp add: pflat_len_simps)
 apply(rule_tac x="list" in exI)
 apply(simp add: Pos_empty)
 apply(rule ballI)
@@ -342,8 +412,8 @@
 done
 
 lemma PosOrd_StarsI:
-  assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
-  shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" 
+  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)
@@ -353,13 +423,13 @@
 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 intlen_append)
+apply(simp add: pflat_len_simps)
 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
-done
+by (metis length_append of_nat_add)
 
 lemma PosOrd_StarsI2:
-  assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
-  shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" 
+  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)
@@ -368,13 +438,8 @@
 apply(subst PosOrd_def)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
-apply(rule_tac x="[]" in exI)
-apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
 apply(rule_tac x="Suc a#list" in exI)
-apply(simp add: pflat_len_Stars_simps pflat_len_simps)
-using assms(2)
-apply(simp add: pflat_len_simps intlen_append)
-apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
 done
 
 lemma PosOrd_Stars_appendI:
@@ -394,7 +459,7 @@
 apply(erule exE)
 apply(case_tac p)
 apply(simp)
-apply(simp add: PosOrd_def pflat_len_simps intlen_append)
+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)
@@ -405,19 +470,19 @@
 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 intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 apply(case_tac q)
-apply(simp add: PosOrd_def pflat_len_simps intlen_append)
+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 intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 apply(case_tac q)
-apply(simp add: PosOrd_def pflat_len_simps intlen_append)
+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 intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 done
 
 lemma PosOrd_Stars_appendE:
@@ -439,42 +504,6 @@
 apply(auto)
 done
 
-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
-  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 fastforce
-      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 intlen_bigger 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_almost_trichotomous:
   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
 apply(auto simp add: PosOrd_ex_def)
@@ -485,12 +514,6 @@
 apply(auto simp add: Pos_empty pflat_len_simps)
 done
 
-lemma WW1:
-  assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
-  shows "False"
-using assms
-apply(auto simp add: PosOrd_ex_def PosOrd_def)
-using assms PosOrd_irrefl PosOrd_trans by blast
 
 lemma PosOrd_SeqE2:
   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
@@ -512,8 +535,8 @@
 apply(auto simp add: PosOrd_def pflat_len_simps)
 apply(case_tac a)
 apply(auto simp add: PosOrd_def pflat_len_simps)
-apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
-by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
+apply (metis PosOrd_SeqI1 PosOrd_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear)
+by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff)
 
 lemma PosOrd_SeqE4:
   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
@@ -531,7 +554,7 @@
 apply(auto)
 apply(case_tac "length (flat v1') < length (flat v1)")
 using PosOrd_shorterI apply blast
-by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
+by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2))
 
 
 
@@ -539,39 +562,39 @@
 
 
 lemma Posix_PosOrd:
-  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s" 
+  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> CV ONE []" by fact
+  have "v \<in> LV ONE []" by fact
   then have "v = Void"
-    by (simp add: CV_simps)
+    by (simp add: LV_simps)
   then show "Void :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_CHAR c v)
-  have "v \<in> CV (CHAR c) [c]" by fact
+  have "v \<in> LV (CHAR c) [c]" by fact
   then have "v = Char c"
-    by (simp add: CV_simps)
+    by (simp add: LV_simps)
   then show "Char c :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_ALT1 s r1 v r2 v2)
   have as1: "s \<in> r1 \<rightarrow> v" by fact
-  have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CV (ALT r1 r2) s" by fact
+  have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> LV (ALT r1 r2) s" by fact
   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-    by(auto simp add: CV_def prefix_list_def)
+    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: CPrf.cases)
+  by (auto elim: Prf.cases)
   then show "Left v :\<sqsubseteq>val v2"
   proof(cases)
      case (Left v3)
-     have "v3 \<in> CV r1 s" using Left(2,3) 
-       by (auto simp add: CV_def prefix_list_def)
+     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)
@@ -583,27 +606,28 @@
      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" using Right(3) as1 
-       by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
+     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_ALT2 s r2 v r1 v2)
   have as1: "s \<in> r2 \<rightarrow> v" by fact
   have as2: "s \<notin> L r1" by fact
-  have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CV (ALT r1 r2) s" by fact
+  have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> LV (ALT r1 r2) s" by fact
   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-    by(auto simp add: CV_def prefix_list_def)
+    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: CPrf.cases)
+  by (auto elim: Prf.cases)
   then show "Right v :\<sqsubseteq>val v2"
   proof (cases)
     case (Right v3)
-     have "v3 \<in> CV r2 s" using Right(2,3) 
-       by (auto simp add: CV_def prefix_list_def)
+     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)
@@ -613,34 +637,34 @@
      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   next
      case (Left v3)
-     have "v3 \<in> CV r1 s" using Left(2,3) as2  
-       by (auto simp add: CV_def prefix_list_def)
+     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) CV_def) 
+       by (simp add: Posix1(2) LV_def) 
      then have "False" using as1 as2 Left
-       by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
+       by (auto simp add: Posix1(2) L_flat_Prf1)
      then show "Right v :\<sqsubseteq>val v2" by simp
   qed
 next 
   case (Posix_SEQ 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> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
+  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> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
-  have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact
+  have "v3 \<in> LV (SEQ 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 CV_def elim: CPrf.cases)
+    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 L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
+    by (smt L_flat_Prf1 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> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3)
-    by (auto simp add: CV_def)
+  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_SeqI2) 
@@ -649,43 +673,43 @@
   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> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  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> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   have cond2: "flat v \<noteq> []" by fact
-  have "v3 \<in> CV (STAR r) (s1 @ s2)" 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 CV_def
+  unfolding LV_def  
   apply(auto)
-  apply(erule CPrf.cases)
+  apply(erule Prf.cases)
   apply(simp_all)
   apply(auto)[1]
   apply(case_tac vs)
   apply(auto)
-  using CPrf.intros(6) by blast
-  then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
+  using Prf.intros(6) by blast
+  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 L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) 
+        by (smt L_flat_Prf1 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> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)" 
-        using NonEmpty(2,3) by (auto simp add: CV_def)
+      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) val.inject(5))
+        using PosOrd_StarsI PosOrd_StarsI2 by auto 
       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
     next 
       case Empty
@@ -696,9 +720,9 @@
     qed      
 next 
   case (Posix_STAR2 r v2)
-  have "v2 \<in> CV (STAR r) []" by fact
+  have "v2 \<in> LV (STAR r) []" by fact
   then have "v2 = Stars []" 
-    unfolding CV_def by (auto elim: CPrf.cases) 
+    unfolding LV_def by (auto elim: Prf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
   by (simp add: PosOrd_ex_eq_def)
 qed
@@ -706,7 +730,7 @@
 
 lemma Posix_PosOrd_reverse:
   assumes "s \<in> r \<rightarrow> v1" 
-  shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val 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)
@@ -729,7 +753,7 @@
              \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
   have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
   have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
-  have "flat v \<in> r \<rightarrow> v" using as2 by simp
+  have "flat v \<in> r \<rightarrow> v" "flat v \<noteq> []" using as2 by auto
   moreover
   have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
     proof (rule IH)
@@ -742,11 +766,14 @@
         apply(erule Prf.cases)
         apply(simp_all)
         apply(drule_tac x="Stars (v # vs)" in bspec)
-        apply(simp add: LV_def CV_def)
-        using Posix_Prf Prf.intros(6) calculation
+        apply(simp add: LV_def)
+        using Posix_LV Prf.intros(6) calculation
         apply(rule_tac Prf.intros)
         apply(simp add:)
+        prefer 2
         apply (simp add: PosOrd_StarsI2)
+        apply(drule Posix_LV) 
+        apply(simp add: LV_def)
         done
     qed
   moreover
@@ -778,48 +805,44 @@
 
 section {* The Smallest Value is indeed the Posix Value *}
 
-text {*
-  The next lemma seems to require LV instead of CV in the Star-case.
-*}
-
 lemma PosOrd_Posix:
-  assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
+  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" 
 using assms
 proof(induct r arbitrary: s v1)
   case (ZERO s v1)
-  have "v1 \<in> CV ZERO s" by fact
-  then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def
-    by (auto elim: CPrf.cases)
+  have "v1 \<in> LV ZERO s" by fact
+  then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def
+    by (auto elim: Prf.cases)
 next 
   case (ONE s v1)
-  have "v1 \<in> CV ONE s" by fact
-  then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def
-    by(auto elim!: CPrf.cases intro: Posix.intros)
+  have "v1 \<in> LV ONE s" by fact
+  then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def
+    by(auto elim!: Prf.cases intro: Posix.intros)
 next 
   case (CHAR c s v1)
-  have "v1 \<in> CV (CHAR c) s" by fact
-  then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def
-    by (auto elim!: CPrf.cases intro: Posix.intros)
+  have "v1 \<in> LV (CHAR c) s" by fact
+  then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def
+    by (auto elim!: Prf.cases intro: Posix.intros)
 next
   case (ALT r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> CV (ALT r1 r2) s" by fact
+  have as2: "v1 \<in> LV (ALT r1 r2) s" by fact
   then consider 
      (Left) v1' where
         "v1 = Left v1'" "s = flat v1'"
-        "v1' \<in> CV r1 s"
+        "v1' \<in> LV r1 s"
   |  (Right) v1' where
         "v1 = Right v1'" "s = flat v1'"
-        "v1' \<in> CV r2 s"
-  unfolding CV_def by (auto elim: CPrf.cases)
+        "v1' \<in> LV r2 s"
+  unfolding LV_def by (auto elim: Prf.cases)
   then show "s \<in> ALT r1 r2 \<rightarrow> v1"
    proof (cases)
      case (Left v1')
-     have "v1' \<in> CV r1 s" using as2
-       unfolding CV_def Left by (auto elim: CPrf.cases)
+     have "v1' \<in> LV r1 s" using as2
+       unfolding LV_def Left by (auto elim: Prf.cases)
      moreover
      have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
        unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force  
@@ -828,8 +851,8 @@
      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
    next
      case (Right v1')
-     have "v1' \<in> CV r2 s" using as2
-       unfolding CV_def Right by (auto elim: CPrf.cases)
+     have "v1' \<in> LV r2 s" using as2
+       unfolding LV_def Right by (auto elim: Prf.cases)
      moreover
      have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
        unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force   
@@ -841,7 +864,8 @@
          then have "Left v' \<in>  LV (ALT r1 r2) s" 
             unfolding LV_def by (auto intro: Prf.intros)
          with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
-            unfolding LV_def Right by (auto)
+            unfolding LV_def Right 
+            by (auto)
          then have False using PosOrd_Left_Right Right by blast  
        }
      then have "s \<notin> L r1" by rule 
@@ -850,21 +874,21 @@
   qed
 next 
   case (SEQ r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact
+  have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact
   then obtain 
     v1a v1b where eqs:
         "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
-        "v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)" 
-  unfolding CV_def by(auto elim: CPrf.cases)
+        "v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" 
+  unfolding LV_def by(auto elim: Prf.cases)
   have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
     proof
       fix v2
       assume "v2 \<in> LV r1 (flat v1a)"
       with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
-         by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf)
+         by (simp add: LV_def Prf.intros(1))
       with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
          using eqs by (simp add: LV_def) 
       then show "\<not> v2 :\<sqsubset>val v1a"
@@ -877,7 +901,7 @@
       fix v2
       assume "v2 \<in> LV r2 (flat v1b)"
       with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
-         by (simp add: CV_def LV_def Prf.intros Prf_CPrf)
+         by (simp add: LV_def Prf.intros)
       with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
          using eqs by (simp add: LV_def) 
       then show "\<not> v2 :\<sqsubset>val v1b"
@@ -889,10 +913,10 @@
   proof
      assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
      then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
-     then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
+     then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2"
         using L_flat_Prf2 by blast
      then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
-       by (auto simp add: LV_def intro: Prf.intros)
+       by (auto simp add: LV_def intro!: Prf.intros)
      with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
      then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
      then show "False"
@@ -903,14 +927,14 @@
     by (rule Posix.intros)
 next
    case (STAR r s v1)
-   have IH: "\<And>s v1. \<lbrakk>v1 \<in> CV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
+   have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
    have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
-   have as2: "v1 \<in> CV (STAR r) s" by fact
+   have as2: "v1 \<in> LV (STAR r) s" by fact
    then obtain 
     vs where eqs:
         "v1 = Stars vs" "s = flat (Stars vs)"
-        "\<forall>v \<in> set vs. v \<in> CV r (flat v)"
-        unfolding CV_def by (auto elim: CPrf.cases)
+        "\<forall>v \<in> set vs. v \<in> LV r (flat v)"
+        unfolding LV_def by (auto elim: Prf.cases)
    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
      proof 
         fix v
@@ -926,9 +950,9 @@
              assume "v2 \<in> LV r (flat v)"
              then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" 
                  using as2 unfolding e eqs
-                 apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1]
-                 using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast
-                 by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5))
+                 apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE)
+                 apply(auto dest!: Prf_Stars_appendE elim: Prf.cases)
+                 done
              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
                 using q by simp     
              with w show "False"
@@ -936,25 +960,18 @@
                 PosOrd_StarsI PosOrd_Stars_appendI by auto
           qed     
         with IH
-        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def
-        by (auto elim: CPrf.cases)
+        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def
+        by (auto elim: Prf.cases)
      qed
    moreover
    have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
      proof 
        assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
-       then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
+       then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
                              "Stars vs2 :\<sqsubset>val Stars vs" 
-         unfolding LV_def
-         apply(auto)
-         apply(erule Prf.cases)
-         apply(auto intro: Prf.intros)
-         done
+         unfolding LV_def by (force elim: Prf_elims intro: Prf.intros)
        then show "False" using as1 unfolding eqs
-         apply -
-         apply(drule_tac x="Stars vs2" in bspec)
-         apply(auto simp add: LV_def)
-         done
+         by (auto simp add: LV_def)
      qed
    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
      thm PosOrd_Posix_Stars
@@ -962,6 +979,55 @@
    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
 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 L_flat_Prf1 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>!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
+  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
+ "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
+apply(rule finite_acyclic_wf)
+prefer 2
+apply(simp add: acyclic_def)
+apply(induct_tac rule: trancl.induct)
+apply(auto)[1]
+oops
+
+
 unused_thms
 
 end
\ No newline at end of file