theory Positions

  imports "Spec" "Lexer"

begin

chapter \<open>An alternative definition for POSIX values\<close>

section \<open>Positions in Values\<close>

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 \<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:: "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)"

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:: "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 

(*

  :\<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 (metis (full_types) 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 

  unfolding ordering_def

  by (simp add: ordering_axioms_def)

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_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 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_CH c v)