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)"
*)

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

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

lemma val_ord_ALTE:
  assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
  shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
using assms(1)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps)
apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)

lemma val_ord_ALTE2:
  assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
  shows "p = 1 \<and> v1 \<sqsubset>val ps v2"
using assms(1)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps)
apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)

lemma val_ord_STARI:
  assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
  shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" 
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(subst pflat_len_Stars_simps)
apply(simp)
apply(subst pflat_len_Stars_simps)
apply(simp)
apply(simp)
apply(rule ballI)
apply(rule impI)
apply(simp)
apply(auto)
using assms(2)
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_Stars_simps)
done

lemma val_ord_STARI2:
  assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
  shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" 
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(case_tac vs1)
apply(simp)
apply(simp)
apply(auto)[1]
apply(case_tac vs2)
apply(simp)
apply (simp add: pflat_len_def)
apply(simp)
apply(auto)[1]
apply (simp add: pflat_len_Stars_simps)
using pflat_len_def apply auto[1]
apply(rule ballI)
apply(rule impI)
apply(simp)
using assms(2)
apply(auto)
apply (simp add: pflat_len_simps(7))
apply (simp add: pflat_len_Stars_simps)
using assms(2)
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
done


lemma val_ord_SEQI:
  assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
  shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')" 
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]
apply(simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(auto simp add: pflat_len_simps)[2]
done


lemma val_ord_SEQI2:
  assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'"
  shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')" 
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)
apply(auto simp add: pflat_len_def intlen_append)
apply(auto simp add: assms(2))
done

lemma val_ord_SEQE_0:
  assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" 
  shows "v1 \<sqsubset>val p v1'"
using assms(1)
apply(simp add: val_ord_def val_ord_ex_def)
apply(auto)[1]
apply(simp add: pflat_len_simps)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
done

lemma val_ord_SEQE_1:
  assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 
  shows "v2 \<sqsubset>val p v2'"
using assms(1)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(auto)[1]
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(auto)
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
done

lemma val_ord_SEQE_2:
  assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 
  and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 
  shows "v1 = v1'"
proof -
  have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q"
  using assms(1) 
  apply(simp add: val_ord_def)
  apply(rule ballI)
  apply(clarify)
  apply(drule_tac x="0#q" in bspec)
  apply(auto)[1]
  apply(simp add: pflat_len_simps)
  done
  then have "Pos v1 = Pos v1'"
  apply(rule_tac Two_to_Three_orig)
  apply(rule ballI)
  apply(drule_tac x="pa" in bspec)
  apply(simp)
  apply(simp)
  done
  then show "v1 = v1'" 
  apply(rule_tac Three_to_One)
  apply(rule assms)
  apply(rule assms)
  apply(simp)
  done
qed

lemma val_ord_SEQ:
  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
  and "flat (Seq v1 v2) = flat (Seq v1' v2')"
  and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 
  shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))"
using assms(1)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(simp only: val_ord_def)
apply(simp)
apply(erule conjE)+
apply(erule disjE)
prefer 2
apply(erule disjE)
apply(erule exE)
apply(rule disjI1)
apply(simp)
apply(subst val_ord_ex_def)
apply(rule_tac x="ps" in exI)
apply(rule val_ord_SEQE_0)
apply(simp add: val_ord_def)
apply(erule exE)
apply(rule disjI2)
apply(rule conjI)
thm val_ord_SEQE_1
apply(rule_tac val_ord_SEQE_2)
apply(auto simp add: val_ord_def)[3]
apply(rule assms(3))
apply(rule assms(4))
apply(subst val_ord_ex_def)
apply(rule_tac x="ps" in exI)
apply(rule_tac val_ord_SEQE_1)
apply(auto simp add: val_ord_def)[1]
apply(simp)
using assms(2)
apply(simp add: pflat_len_simps)
done


lemma val_ord_ex_trans:
  assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
  shows "v1 :\<sqsubset>val v3"
using assms
unfolding val_ord_ex_def
apply(clarify)
apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")
prefer 2
apply(rule trichotomous)
apply(erule disjE)
apply(simp)
apply(rule_tac x="pa" in exI)
apply(subst val_ord_def)
apply(rule conjI)
apply(simp add: val_ord_def)
apply(auto)[1]
apply(simp add: val_ord_def)
apply(simp add: val_ord_def)
apply(auto)[1]
using outside_lemma apply blast
apply(simp add: val_ord_def)
apply(auto)[1]
using outside_lemma apply force
apply auto[1]
apply(simp add: val_ord_def)
apply(auto)[1]
apply (metis (no_types, hide_lams) lex_trans outside_lemma)
apply(simp add: val_ord_def)
apply(auto)[1]
by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)


lemma Pos_pre:
  assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"
  shows "q \<in> Pos v"
using assms
apply(induct v arbitrary: p q rule: Pos.induct)
apply(simp_all add: prefix_list_def)
apply (meson append_eq_Cons_conv append_is_Nil_conv)
apply (meson append_eq_Cons_conv append_is_Nil_conv)
apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv)
apply(auto)
apply (meson append_eq_Cons_conv)
apply(simp add: append_eq_Cons_conv)
apply(auto)
done

lemma lex_lists_order:
  assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)"
  shows "\<not>(q \<sqsubset>lex q')"
using assms
apply(induct rule: lex_lists.induct)
apply(simp add: prefix_list_def)
apply(auto)
using trichotomous_aux2 by auto

lemma lex_appendL:
  assumes "q \<sqsubset>lex p" 
  shows "q \<sqsubset>lex p @ q'"
using assms
apply(induct arbitrary: q' rule: lex_lists.induct)
apply(auto)
done


inductive 
  CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
where
 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
| "\<Turnstile> Void : ONE"
| "\<Turnstile> Char c : CHAR c"
| "\<Turnstile> Stars [] : STAR r"
| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"

lemma Prf_CPrf:
  assumes "\<Turnstile> v : r"
  shows "\<turnstile> v : r"
using assms
apply(induct)
apply(auto intro: Prf.intros)
done

definition
  "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"

definition
  "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"

lemma CPT_CPTpre_subset:
  shows "CPT r s \<subseteq> CPTpre r s"
apply(auto simp add: CPT_def CPTpre_def)
done


lemma CPTpre_subsets:
  "CPTpre ZERO s = {}"
  "CPTpre ONE s \<subseteq> {Void}"
  "CPTpre (CHAR c) s \<subseteq> {Char c}"
  "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
  "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
  "CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
    {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"
  "CPTpre (STAR r) [] = {Stars []}"
apply(auto simp add: CPTpre_def)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule CPrf.intros)
done


lemma CPTpre_simps:
  shows "CPTpre ONE s = {Void}"
  and   "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
  and   "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
  and   "CPTpre (SEQ r1 r2) s = 
          {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
apply -
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]
apply(case_tac "c = d")
apply(simp)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(simp)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
done

lemma CPT_simps:
  shows "CPT ONE s = (if s = [] then {Void} else {})"
  and   "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
  and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
  and   "CPT (SEQ r1 r2) s = 
          {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
apply -
apply(rule subset_antisym)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(clarify)
apply blast
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
done

lemma CPTpre_SEQ:
  assumes "v \<in> CPTpre (SEQ r1 r2) s"
  shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)"
using assms
apply(simp add: CPTpre_simps)
apply(auto simp add: CPTpre_def)
apply (simp add: prefix_list_def)
by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))

term "{vs. Stars vs \<in> A}"

lemma test: 
  assumes "finite A"
  shows "finite {vs. Stars vs \<in> A}"
using assms
apply(induct A)
apply(simp)
apply(auto)
apply(case_tac x)
apply(simp_all)
done

lemma CPTpre_STAR_finite:
  assumes "\<And>s. finite (CPTpre r s)"
  shows "finite (CPTpre (STAR r) s)"
apply(induct s rule: length_induct)
apply(case_tac xs)
apply(simp)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_SigmaI)
apply(rule assms)
apply(case_tac "flat v = []")
apply(simp)
apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
apply(simp)
apply(auto)[1]
apply(rule test)
apply(simp)
done

lemma CPTpre_finite:
  shows "finite (CPTpre r s)"
apply(induct r arbitrary: s)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2).  v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
by (simp add: CPTpre_STAR_finite)


lemma CPT_finite:
  shows "finite (CPT r s)"
apply(rule finite_subset)
apply(rule CPT_CPTpre_subset)
apply(rule CPTpre_finite)
done

lemma Posix_CPT:
  assumes "s \<in> r \<rightarrow> v"
  shows "v \<in> CPT r s"
using assms
apply(induct rule: Posix.induct)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
done

lemma Posix_val_ord:
  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
  shows "v1 :\<sqsubseteq>val v2"
using assms
apply(induct arbitrary: v2 rule: Posix.induct)
apply(simp add: CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: val_ord_ex1_def)
apply(simp add: CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: val_ord_ex1_def)
(* ALT1 *)
prefer 3
(* SEQ case *)
apply(subst (asm) (3) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(case_tac "s' = []")
apply(simp)
prefer 2
apply(simp add: val_ord_ex1_def)
apply(clarify)
apply(simp)
apply(simp add: val_ord_ex_def)
apply(simp (no_asm) add: val_ord_def)
apply(rule_tac x="[]" in exI)
apply(simp add: pflat_len_simps)
apply(rule intlen_length)
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le)
apply(subgoal_tac "length (flat v1a) \<le> length s1")
prefer 2
apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil)
apply(subst (asm) append_eq_append_conv_if)
apply(simp)
apply(clarify)
apply(drule_tac x="v1a" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
using append_eq_conv_conj apply blast
apply(subst (asm) (2)val_ord_ex1_def)
apply(erule disjE)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(subst val_ord_ex_def)
apply(rule_tac x="0#p" in exI)
apply(rule val_ord_SEQI)
apply(simp)
apply(simp)
apply (metis Posix1(2) append_assoc append_take_drop_id)
apply(simp)
apply(drule_tac x="v2b" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (simp add: Posix1(2))
apply(subst (asm) val_ord_ex1_def)
apply(erule disjE)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(subst val_ord_ex_def)
apply(rule_tac x="1#p" in exI)
apply(rule val_ord_SEQI2)
apply(simp)
apply (simp add: Posix1(2))
apply(subst val_ord_ex1_def)
apply(simp)
(* ALT *)
apply(subst (asm) (2) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(case_tac "s' = []")
apply(simp)
apply(drule_tac x="v1" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply(subst (asm) val_ord_ex1_def)
apply(erule disjE)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(subst val_ord_ex_def)
apply(rule_tac x="0#p" in exI)
apply(rule val_ord_ALTI)
apply(simp)
using Posix1(2) apply blast
using val_ord_ex1_def apply blast
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply (simp add: Posix1(2) val_ord_shorterI)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(case_tac "s' = []")
apply(simp)
apply(subst val_ord_ex_def)
apply(rule_tac x="[0]" 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 (smt inlen_bigger)
apply(simp)
apply(rule conjI)
apply(simp add: pflat_len_simps)
using Posix1(2) apply auto[1]
apply(rule ballI)
apply(rule impI)
apply(case_tac "q = []")
using Posix1(2) apply auto[1]
apply(auto)[1]
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
(* ALT RIGHT *)
apply(subst (asm) (2) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(case_tac "s' = []")
apply(simp)
apply (simp add: L_flat_Prf1 Prf_CPrf)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
apply(case_tac "s' = []")
apply(simp)
apply(drule_tac x="v2a" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply(subst (asm) val_ord_ex1_def)
apply(erule disjE)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(subst val_ord_ex_def)
apply(rule_tac x="1#p" in exI)
apply(rule val_ord_ALTI2)
apply(simp)
using Posix1(2) apply blast
apply (simp add: val_ord_ex1_def)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
(* STAR empty case *)
prefer 2
apply(subst (asm) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply (simp add: val_ord_ex1_def)
(* STAR non-empty case *)
apply(subst (asm) (3) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply (simp add: val_ord_ex1_def)
apply(rule val_ord_shorterI)
apply(simp)
apply(case_tac "s' = []")
apply(simp)
prefer 2
apply (simp add: val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less)
apply(drule_tac x="va" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv)
apply (subst (asm) (2) val_ord_ex1_def)
apply(erule disjE)
prefer 2
apply(simp)
apply(drule_tac x="Stars vsa" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (simp add: Posix1(2))
apply (subst (asm) val_ord_ex1_def)
apply(erule disjE)
apply (subst (asm) val_ord_ex_def)
apply(erule exE)
apply (subst val_ord_ex1_def)
apply(rule disjI1)
apply (subst val_ord_ex_def)
apply(case_tac p)
apply(simp)
apply (metis Posix1(2) flat_Stars not_less_iff_gr_or_eq pflat_len_simps(7) same_append_eq val_ord_def)
using Posix1(2) val_ord_STARI2 apply fastforce
apply(simp add: val_ord_ex1_def)
apply (subst (asm) val_ord_ex_def)
apply(erule exE)
apply (subst val_ord_ex1_def)
apply(rule disjI1)
apply (subst val_ord_ex_def)
by (metis Posix1(2) flat.simps(7) flat_Stars val_ord_STARI)

lemma Posix_val_ord_stronger:
  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
  shows "v1 :\<sqsubseteq>val v2"
using assms
apply(rule_tac Posix_val_ord)
apply(assumption)
apply(simp add: CPTpre_def CPT_def)
done


lemma STAR_val_ord:
  assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2"
  shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)"
using assms(1,2)
apply -
apply(simp(no_asm)  add: val_ord_def)
apply(rule conjI)
apply(simp add: val_ord_def)
apply(rule conjI)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1]
apply(rule ballI)
apply(rule impI)
apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
apply(clarify)
apply(case_tac q)
apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
apply(clarify)
apply(erule disjE)
prefer 2
apply(drule_tac x="Suc a # list" in bspec)
apply(simp)
apply(drule mp)
apply(simp)
apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
apply(drule_tac x="Suc a # list" in bspec)
apply(simp)
apply(drule mp)
apply(simp)
apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
done


lemma Posix_val_ord_reverse:
  assumes "s \<in> r \<rightarrow> v1" 
  shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
using assms
by (metis Posix_val_ord_stronger less_irrefl val_ord_def 
    val_ord_ex1_def val_ord_ex_def val_ord_ex_trans)

thm Posix.intros(6)

inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool"
where
  "Prop r []"
| "\<lbrakk>Prop r vs; 
    \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> 
   \<Longrightarrow> Prop r (v # vs)"

lemma STAR_val_ord_ex:
  assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
  shows "Stars vs1 :\<sqsubset>val Stars vs2"
using assms
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp)
apply(simp add: val_ord_def pflat_len_simps intlen_append)
apply(subst val_ord_ex_def)
apply(rule_tac x="[]" in exI)
apply(simp add: val_ord_def pflat_len_simps Pos_empty)
apply(simp)
apply(case_tac a)
apply(clarify)
prefer 2
using STAR_val_ord val_ord_ex_def apply blast
apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1]
done

lemma STAR_val_ord_exI:
  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)
apply(simp add: val_ord_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp)
apply(rule_tac x="[]" in exI)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps intlen_append)[1]
apply(simp)
apply(rule_tac x="Suc aa#list" in exI)
apply(rule val_ord_STARI2)
apply(simp)
apply(simp)
done

lemma STAR_val_ord_ex_append:
  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)
apply(drule STAR_val_ord_ex)
apply(simp)
done

lemma STAR_val_ord_ex_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 STAR_val_ord_ex_append)
apply(rule STAR_val_ord_exI)
apply(auto)
done

lemma Posix_STARI:
  assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs"
  shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
using assms
apply(induct vs arbitrary: r)
apply(simp)
apply(rule Posix.intros)
apply(simp)
apply(rule Posix.intros)
apply(simp)
apply(auto)[1]
apply(erule Prop.cases)
apply(simp)
apply(simp)
apply(simp)
apply(erule Prop.cases)
apply(simp)
apply(auto)[1]
done

lemma CPrf_stars:
  assumes "\<Turnstile> Stars vs : STAR r"
  shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
using assms
apply(induct vs)
apply(auto)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
done

definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"

lemma exists:
  assumes "s \<in> (L r)\<star>"
  shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
using assms
apply(drule_tac Star_string)
apply(auto)
by (metis L_flat_Prf2 Prf_Stars Star_val)


lemma val_ord_Posix_Stars:
  assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
  and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
  shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
using assms
apply(induct vs)
apply(simp)
apply(rule Posix.intros)
apply(simp (no_asm))
apply(rule Posix.intros)
apply(auto)[1]
apply(auto simp add: CPT_def PT_def)[1]
defer
apply(simp)
apply(drule meta_mp)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(drule meta_mp)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule Prf.cases)
apply(simp_all)
apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
apply(clarify)
apply(drule_tac x="Stars (a#v#vsa)" in spec)
apply(simp)
apply(drule mp)
apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
apply(auto simp add: CPT_def PT_def)[1]
using CPrf_stars apply auto[1]
apply(auto)[1]
apply(auto simp add: CPT_def PT_def)[1]
apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r")
prefer 2
apply (meson L_flat_Prf2)
apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)")
apply(clarify)
apply(drule_tac x="Stars (vA # vB)" in spec)
apply(simp)
apply(drule mp)
using Prf.intros(7) apply blast
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
prefer 2
apply(simp)
using exists apply blast
prefer 2
apply(drule meta_mp)
apply(erule CPrf.cases)
apply(simp_all)
apply(drule meta_mp)
apply(auto)[1]
prefer 2
apply(simp)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)
apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def)
apply(drule_tac x="Stars (v#va#vsb)" in spec)
apply(drule mp)
apply (simp add: Posix1a Prf.intros(7))
apply(simp)
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
proof -
  fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
  assume a1: "s\<^sub>3 \<noteq> []"
  assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
  assume a3: "flat vA = flat a @ s\<^sub>3"
  assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)"
  have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs"
    by (meson drop_eq_Nil not_less)
  have f6: "\<not> length (flat vA) \<le> length (flat a)"
    using a3 a1 by simp
  have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))"
    using a3 a2 by simp
  then show False
    using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_STARI val_ord_ex_def val_ord_shorterI)
qed

lemma Prf_Stars_append:
  assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
  shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
using assms
apply(induct vs1 arbitrary: vs2)
apply(auto intro: Prf.intros)
apply(erule Prf.cases)
apply(simp_all)
apply(auto intro: Prf.intros)
done

lemma CPrf_Stars_appendE:
  assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
  shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
using assms
apply(induct vs1 arbitrary: vs2)
apply(auto intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(auto intro: CPrf.intros)
done

lemma val_ord_Posix:
  assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)"
  shows "s \<in> r \<rightarrow> v1" 
using assms
apply(induct r arbitrary: s v1)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
(* ONE *)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule Posix.intros)
(* CHAR *)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule Posix.intros)
prefer 2
(* ALT *)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule Posix.intros)
apply(drule_tac x="flat v1a" in meta_spec)
apply(drule_tac x="v1a" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac x="Left v2" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply(simp)
apply (meson val_ord_ALTI val_ord_ex_def)
apply(assumption)
(* ALT Right *)
apply(auto simp add: CPT_def)[1]
apply(rule Posix.intros)
apply(rotate_tac 1)
apply(drule_tac x="flat v2" in meta_spec)
apply(drule_tac x="v2" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac x="Right v2a" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply(simp)
apply(subst (asm) (2) val_ord_ex_def)
apply(erule exE)
apply(drule val_ord_ALTI2)
apply(assumption)
apply(auto simp add: val_ord_ex_def)[1]
apply(assumption)
apply(auto)[1]
apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a")
apply(clarify)
apply(drule_tac x="Left v2'" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply(assumption)
apply(simp add: val_ord_ex_def)
apply(subst (asm) (3) val_ord_def)
apply(simp)
apply(simp add: pflat_len_simps)
apply(drule_tac x="[0]" in spec)
apply(simp add: pflat_len_simps Pos_empty)
apply(drule mp)
apply (smt inlen_bigger)
apply(erule disjE)
apply blast
apply auto[1]
apply (meson L_flat_Prf2)
(* SEQ *)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule Posix.intros)
apply(drule_tac x="flat v1a" in meta_spec)
apply(drule_tac x="v1a" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(auto)[1]
apply(auto simp add: PT_def)[1]
apply(drule_tac x="Seq v2a v2" in spec)
apply(simp)
apply(drule mp)
apply (simp add: Prf.intros(1) Prf_CPrf)
using val_ord_SEQI val_ord_ex_def apply fastforce
apply(assumption)
apply(rotate_tac 1)
apply(drule_tac x="flat v2" in meta_spec)
apply(drule_tac x="v2" in meta_spec)
apply(simp)
apply(auto)[1]
apply(drule meta_mp)
apply(auto)[1]
apply(auto simp add: PT_def)[1]
apply(drule_tac x="Seq v1a v2a" in spec)
apply(simp)
apply(drule mp)
apply (simp add: Prf.intros(1) Prf_CPrf)
apply (meson val_ord_SEQI2 val_ord_ex_def)
apply(assumption)
(* SEQ side condition *)
apply(auto simp add: PT_def)
apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a")
prefer 2
apply (meson L_flat_Prf2)
apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a")
prefer 2
apply (meson L_flat_Prf2)
apply(clarify)
apply(drule_tac x="Seq vA vB" in spec)
apply(simp)
apply(drule mp)
apply (simp add: Prf.intros(1))
apply(subst (asm) (3) val_ord_ex_def)
apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SEQI val_ord_ex_def val_ord_shorterI)
(* STAR *)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
using Posix_STAR2 apply blast
apply(clarify)
apply(rule val_ord_Posix_Stars)
apply(auto simp add: CPT_def)[1]
apply (simp add: CPrf.intros(7))
apply(auto)[1]
apply(drule_tac x="flat v" in meta_spec)
apply(drule_tac x="v" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac x="Stars (v2#vs)" in spec)
apply(simp)
apply(drule mp)
using Prf.intros(7) Prf_CPrf apply blast
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
using val_ord_STARI val_ord_ex_def apply fastforce
apply(assumption)
apply(drule_tac x="flat va" in meta_spec)
apply(drule_tac x="va" in meta_spec)
apply(simp)
apply(drule meta_mp)
using CPrf_stars apply blast
apply(drule meta_mp)
apply(auto)[1]
apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post")
prefer 2
apply (metis append_Cons append_Nil in_set_conv_decomp_first)
apply(clarify)
apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply (simp add: Prf_CPrf)
apply(rule Prf_Stars_append)
apply(drule CPrf_Stars_appendE)
apply(auto simp add: Prf_CPrf)[1]
apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD)
apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)")
apply(subst (asm) STAR_val_ord_ex_append_eq)
apply(simp)
apply(subst (asm) STAR_val_ord_ex_append_eq)
apply(simp)
prefer 2
apply(simp)
prefer 2
apply(simp)
apply(simp add: val_ord_ex_def)
apply(erule exE)
apply(rotate_tac 6)
apply(drule_tac x="0#p" in spec)
apply (simp add: val_ord_STARI)
apply(auto simp add: PT_def)
done

unused_thms

end