--- a/thys/Positions.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Positions.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -55,6 +55,17 @@
 by (induct xs arbitrary: ys) (auto)
 
 lemma intlen_length:
+  shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
+apply(induct xs arbitrary: ys)
+apply(auto)
+apply(case_tac ys)
+apply(simp_all)
+apply (smt intlen_bigger)
+(* HERE *)
+oops
+
+
+lemma intlen_length:
   assumes "length xs < length ys"
   shows "intlen xs < intlen ys"
 using assms
@@ -185,6 +196,9 @@
 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"
@@ -219,6 +233,7 @@
 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
 
+
 lemma val_ord_LeftI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Left v) :\<sqsubset>val (Left v')" 
@@ -501,6 +516,49 @@
 apply(auto)[1]
 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def)
 
+lemma val_ord_irrefl:
+  assumes "v :\<sqsubset>val v"
+  shows "False"
+using assms
+by(auto simp add: val_ord_ex_def val_ord_def)
+
+lemma val_ord_almost_trichotomous:
+  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
+apply(auto simp add: val_ord_ex_def)
+apply(auto simp add: val_ord_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 WW1:
+  assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
+  shows "False"
+using assms
+apply(auto simp add: val_ord_ex_def val_ord_def)
+using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast
+
+lemma WW2:
+  assumes "\<not>(v1 :\<sqsubset>val v2)" 
+  shows "v1 = v2 \<or> v2 :\<sqsubset>val v1"
+using assms
+oops
+
+lemma val_ord_SeqE2:
+  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
+  shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
+using assms 
+apply(frule_tac val_ord_SeqE)
+apply(erule disjE)
+apply(simp)
+apply(auto)
+apply(case_tac "v1 :\<sqsubset>val v1'")
+apply(simp)
+apply(auto simp add: val_ord_ex_def)
+apply(case_tac "v1 = v1'")
+apply(simp)
+oops
 
 section {* CPT and CPTpre *}
 
@@ -522,6 +580,62 @@
 using assms
 by (induct) (auto intro: Prf.intros)
 
+lemma pflat_len_equal_iff:
+  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
+  and "\<forall>p. pflat_len v1 p = pflat_len v2 p"
+  shows "v1 = v2"
+using assms
+apply(induct v1 r arbitrary: v2 rule: CPrf.induct)
+apply(rotate_tac 4)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis pflat_len_simps(1) pflat_len_simps(2))
+apply(rotate_tac 2)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis pflat_len_simps(3))
+apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
+apply(rotate_tac 2)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
+apply (metis pflat_len_simps(5))
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9))
+apply(rotate_tac 5)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9))
+apply(auto)
+apply (metis pflat_len_simps(8))
+apply(subgoal_tac "v = va")
+prefer 2
+apply (metis pflat_len_simps(8))
+apply(simp)
+apply(rotate_tac 3)
+apply(drule_tac x="Stars vsa" in meta_spec)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(rule allI)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="[]" in spec)
+apply(simp add: pflat_len_simps intlen_append)
+apply(drule_tac x="Suc a#list" in spec)
+apply(simp add: pflat_len_simps intlen_append)
+apply(simp)
+done
+
+lemma val_ord_trichotomous_stronger:
+  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
+  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
+oops
+
 lemma CPrf_stars:
   assumes "\<Turnstile> Stars vs : STAR r"
   shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"