theory Positions
  imports "Spec" "Lexer" 
begin

section {* Positions in Values *}

fun 
  at :: "val \<Rightarrow> nat list \<Rightarrow> 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 :: "val \<Rightarrow> (nat list) set"
where
  "Pos (Void) = {[]}"
| "Pos (Char 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 :: "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 {* Orderings *}


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 {* POSIX Ordering of Values According to Okui & Suzuki *}


definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> 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)"



definition PosOrd_ex:: "val \<Rightarrow> 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:: "val \<Rightarrow> 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 

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 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"
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 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)
using assms 
apply(auto simp add: PosOrd_def pflat_len_simps)
done

lemma PosOrd_Left_eq:
  assumes "flat v = flat v'"
  shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
using assms
unfolding 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(rule_tac x="list" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
apply(auto simp add: PosOrd_def pflat_len_outside)[1]
apply(rule_tac x="0#p" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps)
done


lemma PosOrd_RightI:
  assumes "v :\<sqsubset>val v'" "flat v = flat v'"
  shows "Right v :\<sqsubset>val Right v'" 
using assms(1)
unfolding PosOrd_ex_def
apply(auto)
apply(rule_tac x="Suc 0#p" in exI)
using assms(2)
apply(auto simp add: PosOrd_def pflat_len_simps)
done

lemma PosOrd_RightE:
  assumes "Right v1 :\<sqsubset>val Right v2"
  shows "v1 :\<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)
apply(rule_tac x="[]" in exI)
apply(simp add: Pos_empty pflat_len_simps)
apply(case_tac a)
apply(simp add: pflat_len_def PosOrd_def)
apply(case_tac nat)
prefer 2
apply(simp add: pflat_len_def PosOrd_def)
apply(auto simp add: pflat_len_simps PosOrd_def)
apply(rule_tac x="list" in exI)
apply(auto)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
done


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'" 
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)
using assms(2)
apply(simp)
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'" 
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_SeqE:
  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)[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)[1]
apply(rule_tac x="list" in exI)
apply(simp)
apply(rule ballI)
apply(rule impI)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(case_tac nat)
apply(rule disjI2)
apply(simp add: PosOrd_def)
apply(auto simp add: pflat_len_simps)
apply(rule_tac x="list" in exI)
apply(simp add: Pos_empty)
apply(rule ballI)
apply(rule impI)
apply(auto)[1]
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(simp add: PosOrd_def pflat_len_def)
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 "flat (Stars vs1) = flat (Stars 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_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)
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


lemma PosOrd_SeqE2:
  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
  shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
using assms 
apply(frule_tac PosOrd_SeqE)
apply(erule disjE)
apply(simp)
apply(case_tac "v1 :\<sqsubset>val v1'")
apply(simp)
apply(rule disjI2)
apply(rule conjI)
prefer 2
apply(simp)
apply(auto)
apply(auto simp add: PosOrd_ex_def)
apply(auto simp add: PosOrd_def pflat_len_simps)
apply(case_tac p)
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_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')"
  shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
using assms 
apply(frule_tac PosOrd_SeqE)
apply(erule disjE)
apply(simp)
apply(case_tac "v1 :\<sqsubset>val v1'")
apply(simp)
apply(rule disjI2)
apply(rule conjI)
prefer 2
apply(simp)
apply(auto)
apply(case_tac "length (flat v1') < length (flat v1)")
using PosOrd_shorterI apply blast
by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2))



section {* The Posix Value is smaller than any other Value *}


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_CHAR c v)
  have "v \<in> LV (CHAR c) [c]" by fact
  then have "v = Char c"
    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> 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: 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_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> 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: 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
       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> 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> 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 LV_def elim: Prf.cases)
  with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
    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> 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) 
  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> L r \<and> s\<^sub>4 \<in> L (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.cases)
  apply(simp_all)
  apply(auto)[1]
  apply(case_tac vs)
  apply(auto)
  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 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 auto 
      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)
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_Stars:
  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
  and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
  shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
using assms
proof(induct vs)
  case Nil
  show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
    by(simp add: Posix.intros)
next
  case (Cons v vs)
  have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
             \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
             \<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" "flat v \<noteq> []" using as2 by auto
  moreover
  have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
    proof (rule IH)
      show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
    next 
      show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
        apply(auto)
        apply(subst (asm) (2) LV_def)
        apply(auto)
        apply(erule Prf.cases)
        apply(simp_all)
        apply(drule_tac x="Stars (v # vs)" in bspec)
        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
  have "flat v \<noteq> []" using as2 by simp
  moreover
  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
   using as3
   apply(auto)
   apply(drule L_flat_Prf2)
   apply(erule exE)
   apply(simp only: L.simps[symmetric])
   apply(drule L_flat_Prf2)
   apply(erule exE)
   apply(clarify)
   apply(rotate_tac 5)
   apply(erule Prf.cases)
   apply(simp_all)
   apply(clarify)
   apply(drule_tac x="Stars (va#vs)" in bspec)
   apply(auto simp add: LV_def)[1]   
   apply(rule Prf.intros)
   apply(simp)
   by (simp add: PosOrd_StarsI PosOrd_shorterI)
  ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
  by (simp add: Posix.intros)
qed



section {* The Smallest Value is indeed the Posix Value *}

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" 
using assms
proof(induct r arbitrary: s v1)
  case (ZERO s v1)
  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> 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> 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> 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> LV (ALT r1 r2) s" by fact
  then consider 
     (Left) v1' where
        "v1 = Left v1'" "s = flat v1'"
        "v1' \<in> LV r1 s"
  |  (Right) v1' where
        "v1 = Right v1'" "s = flat v1'"
        "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> 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  
     ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
     then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
   next
     case (Right v1')
     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   
     ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
     moreover 
       { assume "s \<in> L r1"
         then obtain v' where "v' \<in>  LV r1 s"
            unfolding LV_def using L_flat_Prf2 by blast
         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)
         then have False using PosOrd_Left_Right Right by blast  
       }
     then have "s \<notin> L r1" by rule 
     ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
  qed
next 
  case (SEQ r1 r2 s v1)
  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> LV (SEQ r1 r2) s" by fact
  then obtain 
    v1a v1b where eqs:
        "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
        "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: 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"
         using PosOrd_SeqI1 by blast
    qed     
  then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
  moreover
  have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
    proof 
      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: 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"
         using PosOrd_SeqI2 by auto
    qed     
  then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp    
  moreover
  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
  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"
        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)
     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"
       using PosOrd_shorterI by blast  
  qed
  ultimately
  show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
    by (rule Posix.intros)
next
   case (STAR r s v1)
   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> 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> 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
        assume a: "v \<in> set vs"
        then obtain pre post where e: "vs = pre @ [v] @ post"
          by (metis append_Cons append_Nil in_set_conv_decomp_first)
        then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" 
          using as1 unfolding eqs by simp
        have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs 
          proof (rule ballI, rule notI) 
             fix v2
             assume w: "v2 :\<sqsubset>val v"
             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: 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"
                using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
                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 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)"
                             "Stars vs2 :\<sqsubset>val Stars vs" 
         unfolding LV_def by (force elim: Prf_elims intro: Prf.intros)
       then show "False" using as1 unfolding eqs
         by (auto simp add: LV_def)
     qed
   ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
     thm PosOrd_Posix_Stars
     by (rule PosOrd_Posix_Stars)
   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