--- a/thys/Positions.thy	Tue Jun 27 13:15:55 2017 +0100
+++ b/thys/Positions.thy	Wed Jun 28 10:37:05 2017 +0100
@@ -46,7 +46,7 @@
   "intlen [] = 0"
 | "intlen (x#xs) = 1 + intlen xs"
 
-lemma inlen_bigger:
+lemma intlen_bigger:
   shows "0 \<le> intlen xs"
 by (induct xs)(auto)
 
@@ -62,9 +62,19 @@
 apply(auto)
 apply(case_tac ys)
 apply(simp_all)
-apply (smt inlen_bigger)
+apply (smt intlen_bigger)
 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 
+lemma length_intlen:
+  assumes "intlen xs < intlen ys"
+  shows "length xs < length ys"
+using assms
+apply(induct xs arbitrary: ys)
+apply(auto)
+apply(case_tac ys)
+apply(simp_all)
+by (smt intlen_bigger)
+
 
 definition pflat_len :: "val \<Rightarrow> nat list => int"
 where
@@ -179,6 +189,21 @@
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
+lemma val_ord_shorterE:
+  assumes "v1 :\<sqsubset>val v2" 
+  shows "length (flat v2) \<le> length (flat v1)"
+using assms
+apply(auto simp add: val_ord_ex_def val_ord_def)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(drule length_intlen)
+apply(simp)
+apply(drule_tac x="[]" in bspec)
+apply(simp add: Pos_empty)
+apply(simp add: pflat_len_simps)
+by (metis intlen_length le_less less_irrefl linear)
+
+
 lemma val_ord_shorterI:
   assumes "length (flat v') < length (flat v)"
   shows "v :\<sqsubset>val v'" 
@@ -474,7 +499,7 @@
 apply (metis (no_types, hide_lams) lex_trans outside_lemma)
 apply(simp add: val_ord_def)
 apply(auto)[1]
-by (smt inlen_bigger lex_trans outside_lemma pflat_len_def)
+by (smt intlen_bigger lex_trans outside_lemma pflat_len_def)
 
 
 section {* CPT and CPTpre *}
@@ -816,7 +841,7 @@
 apply(simp add: Pos_empty)
 apply(rule conjI)
 apply(simp add: pflat_len_simps)
-apply (smt inlen_bigger)
+apply (smt intlen_bigger)
 apply(simp)
 apply(rule conjI)
 apply(simp add: pflat_len_simps)
@@ -1093,7 +1118,7 @@
 apply(drule_tac x="[0]" in spec)
 apply(simp add: pflat_len_simps Pos_empty)
 apply(drule mp)
-apply (smt inlen_bigger)
+apply (smt intlen_bigger)
 apply(erule disjE)
 apply blast
 apply auto[1]