theory Positions

  imports "Lexer" 

begin

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

  shows "[] \<in> Pos v"

apply(induct v rule: Pos.induct)

apply(auto)

done

fun intlen :: "'a list \<Rightarrow> int"

where

  "intlen [] = 0"

| "intlen (x#xs) = 1 + intlen xs"

lemma inlen_bigger:

  shows "0 \<le> intlen xs"

apply(induct xs)

apply(auto)

done 

lemma intlen_append:

  shows "intlen (xs @ ys) = intlen xs + intlen ys"

apply(induct xs arbitrary: ys)

apply(auto)

done 

lemma intlen_length:

  assumes "length xs < length ys"

  shows "intlen xs < intlen ys"

using assms

apply(induct xs arbitrary: ys)

apply(auto)

apply(case_tac ys)

apply(simp_all)

apply (smt inlen_bigger)

by (smt Suc_lessE intlen.simps(2) length_Suc_conv)

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 v [] = intlen (flat v)"

apply(auto simp add: pflat_len_def Pos_empty)

done

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(simp)

apply(simp)

apply(simp add: pflat_len_def)

apply(auto)[1]

apply (metis at.simps(6))

apply (metis Suc_less_eq Suc_pred)

by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')

lemma pflat_len_Stars_simps2:

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

using assms 

apply(simp_all add: pflat_len_def)

done

lemma Two_to_Three_aux:

  assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"

  shows "p \<in> Pos v1 \<inter> Pos v2"

using assms

apply(simp add: pflat_len_def)

apply(auto split: if_splits)

apply (smt inlen_bigger)+

done

lemma Two_to_Three_orig:

  assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"

  shows "Pos v1 = Pos v2"

using assms

by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym)

lemma Three_to_One:

  assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" 

  and "Pos v1 = Pos v2" 

  shows "v1 = v2"

using assms

apply(induct v1 arbitrary: r v2 rule: Pos.induct)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(clarify)

apply(simp add: insert_ident)

apply(drule_tac x="r1a" in meta_spec)

apply(drule_tac x="v1a" in meta_spec)

apply(simp)

apply(drule_tac meta_mp)

thm subset_antisym

apply(rule subset_antisym)

apply(auto)[3]

apply(clarify)

apply(simp add: insert_ident)

using Pos_empty apply blast

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(clarify)

apply(simp add: insert_ident)

using Pos_empty apply blast

apply(simp add: insert_ident)

apply(drule_tac x="r2a" in meta_spec)

apply(drule_tac x="v2b" in meta_spec)

apply(simp)

apply(drule_tac meta_mp)

apply(rule subset_antisym)

apply(auto)[3]

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(simp add: insert_ident)

apply(clarify)

apply(drule_tac x="r1a" in meta_spec)

apply(drule_tac x="r2a" in meta_spec)

apply(drule_tac x="v1b" in meta_spec)

apply(drule_tac x="v2c" in meta_spec)

apply(simp)

apply(drule_tac meta_mp)

apply(rule subset_antisym)

apply(rule subsetI)

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp)

apply(rule subsetI)

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp (no_asm_use))

apply(simp)

apply(drule_tac meta_mp)

apply(rule subset_antisym)

apply(rule subsetI)

apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp)

apply(rule subsetI)

apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp (no_asm_use))

apply(simp)

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(auto)[1]

using Pos_empty apply fastforce

apply(erule Prf.cases)

apply(simp_all)

apply(erule Prf.cases)

apply(simp_all)

apply(auto)[1]

using Pos_empty apply fastforce

apply(clarify)

apply(simp add: insert_ident)

apply(drule_tac x="rb" in meta_spec)

apply(drule_tac x="STAR rb" in meta_spec)

apply(drule_tac x="vb" in meta_spec)

apply(drule_tac x="Stars vsb" in meta_spec)

apply(simp)

apply(drule_tac meta_mp)

apply(rule subset_antisym)

apply(rule subsetI)

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp)

apply(rule subsetI)

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}")

prefer 2

apply(auto)[1]

apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp (no_asm_use))

apply(simp)

apply(drule_tac meta_mp)

apply(rule subset_antisym)

apply(rule subsetI)

apply(case_tac vsa)

apply(simp)

apply (simp add: Pos_empty)

apply(simp)

apply(clarify)

apply(erule disjE)

apply (simp add: Pos_empty)

apply(erule disjE)

apply(clarify)

apply(subgoal_tac 

  "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

prefer 2

apply blast

apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union>  {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp)

apply(clarify)

apply(subgoal_tac 

  "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

prefer 2

apply blast

apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp)

apply(rule subsetI)

apply(case_tac vsb)

apply(simp)

apply (simp add: Pos_empty)

apply(simp)

apply(clarify)

apply(erule disjE)

apply (simp add: Pos_empty)

apply(erule disjE)

apply(clarify)

apply(subgoal_tac 

  "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

prefer 2

apply(simp)

apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

apply blast

using list.inject apply blast

apply(clarify)

apply(subgoal_tac 

  "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

prefer 2

apply(simp)

apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

prefer 2

apply (metis (no_types, lifting) Un_iff)

apply(simp (no_asm_use))

apply(simp)

done

definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")

where

  "ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)"

definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")

where

  "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"

inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")

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

apply(induct rule: lex_lists.induct)

apply(auto)

done

lemma lex_append:

  assumes "ps2 \<noteq> []"  

  shows "ps \<sqsubset>lex ps @ ps2"

using assms

apply(induct ps)

apply(auto intro: lex_lists.intros)

apply(case_tac ps2)

apply(simp)

apply(simp)

apply(auto intro: lex_lists.intros)

done

lemma lexordp_simps [simp]:

  fixes xs ys :: "nat list"

  shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"

  and   "xs \<sqsubset>lex [] = False"

  and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"

apply -

apply (metis lex_append lex_lists.simps list.simps(3))

using lex_lists.cases apply blast

using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce

lemma lex_append_cancel [simp]:

  fixes ps ps1 ps2 :: "nat list"

  shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2"

apply(induct ps)

apply(auto)

done

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

apply(induct arbitrary: ps3 rule: lex_lists.induct)

apply(erule lex_lists.cases)

apply(simp_all)

apply(rotate_tac 2)

apply(erule lex_lists.cases)

apply(simp_all)

apply(erule lex_lists.cases)

apply(simp_all)

done

lemma trichotomous_aux:

  fixes p q :: "nat list"

  assumes "p \<sqsubset>lex q" "p \<noteq> q"

  shows "\<not>(q \<sqsubset>lex p)"

using assms

apply(induct rule: lex_lists.induct)

apply(auto)

done

lemma trichotomous_aux2:

  fixes p q :: "nat list"

  assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p"

  shows "False"

using assms

apply(induct rule: lex_lists.induct)

apply(auto)

done

lemma 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)

apply(case_tac q)

apply(auto)

done

definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 

  where

  "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"

definition

  "DPos v1 v2 \<equiv> {p. dpos v1 v2 p}"

lemma outside_lemma:

  assumes "p \<notin> Pos v1 \<union> Pos v2"

  shows "pflat_len v1 p = pflat_len v2 p"

using assms

apply(auto simp add: pflat_len_def)

done

lemma dpos_lemma_aux:

  assumes "p \<in> Pos v1 \<union> Pos v2"

  and "pflat_len v1 p = pflat_len v2 p"

  shows "p \<in> Pos v1 \<inter> Pos v2"

using assms

apply(auto simp add: pflat_len_def)

apply (smt inlen_bigger)

apply (smt inlen_bigger)

done

lemma dpos_lemma:

  assumes "p \<in> Pos v1 \<union> Pos v2"

  and "pflat_len v1 p = pflat_len v2 p"

  shows "\<not>dpos v1 v2 p"

using assms

apply(auto simp add: dpos_def dpos_lemma_aux)

using dpos_lemma_aux apply auto[1]

using dpos_lemma_aux apply auto[1]

done

lemma dpos_lemma2:

  assumes "p \<in> Pos v1 \<union> Pos v2"

  and "dpos v1 v2 p"

  shows "pflat_len v1 p \<noteq> pflat_len v2 p"

using assms

using dpos_lemma by blast

lemma DPos_lemma:

  assumes "p \<in> DPos v1 v2"

  shows "pflat_len v1 p \<noteq> pflat_len v2 p"

using assms

unfolding DPos_def 

apply(auto simp add: pflat_len_def dpos_def)

apply (smt inlen_bigger)

by (smt inlen_bigger)

definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")

where

  "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> 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 val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")

where

  "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"

definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")

where

  "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"

lemma val_ord_shorterI:

  assumes "length (flat v') < length (flat v)"

  shows "v :\<sqsubset>val v'" 

using assms(1)

apply(subst val_ord_ex_def)

apply(rule_tac x="[]" in exI)

apply(subst val_ord_def)

apply(rule conjI)

apply (simp add: Pos_empty)

apply(rule conjI)

apply(simp add: pflat_len_simps)

apply (simp add: intlen_length)

apply(simp)

done

lemma val_ord_spre:

  assumes "(flat v') \<sqsubset>spre (flat v)"

  shows "v :\<sqsubset>val v'" 

using assms(1)

apply(rule_tac val_ord_shorterI)

apply(simp add: sprefix_list_def prefix_list_def)

apply(auto)

apply(case_tac ps')

apply(auto)

by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)

lemma val_ord_ALTI:

  assumes "v \<sqsubset>val p v'" "flat v = flat v'"

  shows "(Left v) \<sqsubset>val (0#p) (Left v')" 

using assms(1)

apply(subst (asm) val_ord_def)

apply(erule conjE)

apply(subst val_ord_def)

apply(rule conjI)

apply(simp)

apply(rule conjI)

apply(simp add: pflat_len_simps)

apply(rule ballI)

apply(rule impI)

apply(simp only: Pos.simps)

apply(auto)[1]

using assms(2)

apply(simp add: pflat_len_simps)

apply(auto simp add: pflat_len_simps)[2]

done

lemma val_ord_ALTI2:

  assumes "v \<sqsubset>val p v'" "flat v = flat v'"

  shows "(Right v) \<sqsubset>val (1#p) (Right v')" 

using assms(1)

apply(subst (asm) val_ord_def)

apply(erule conjE)

apply(subst val_ord_def)

apply(rule conjI)

apply(simp)

apply(rule conjI)

apply(simp add: pflat_len_simps)

apply(rule ballI)

apply(rule impI)

apply(simp only: Pos.simps)

apply(auto)[1]

using assms(2)

apply(simp add: pflat_len_simps)

apply(auto simp add: pflat_len_simps)[2]

done