diff -r 222ed43892ea -r 146b4817aebd thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Sulzmann.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -118,6 +118,10 @@
 apply(simp)
 oops
 
+lemma QQ: 
+  shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y"
+  by auto
+
 lemma Posix_CPT2:
   assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
   shows "v1 \<prec> v2"
@@ -149,10 +153,13 @@
 apply(erule CPrf.cases)
 apply(simp_all)[7]
 apply(clarify)
+apply(frule val_ord_shorterE)
+apply(subst (asm) QQ)
+apply(erule disjE)
 apply(drule val_ord_SeqE)
 apply(erule disjE)
 apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 7)
+apply(rotate_tac 8)
 apply(drule_tac x="v1b" in meta_spec)
 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
 apply(simp)
@@ -160,7 +167,19 @@
 apply(auto simp add: CPTpre_def)[1]
 apply(drule meta_mp)
 apply(auto simp add: CPTpre_def)[1]
+apply(rule ValOrd.intros(2))
+apply(assumption)
+apply(frule val_ord_shorterE)
+apply(subst (asm) append_eq_append_conv_if)
+apply(simp)
+apply (metis append_assoc append_eq_append_conv_if length_append)
+
+
+thm le
+apply(clarify)
 apply(rule ValOrd.intros)
+apply(simp)
+
 apply(subst (asm) (3) CPTpre_def)
 apply(subst (asm) (3) CPTpre_def)
 apply(auto)[1]