diff -r 45ad887fa6aa -r 00c9a95d492e thys/Positions.thy
--- a/thys/Positions.thy	Tue Jul 04 16:42:49 2017 +0100
+++ b/thys/Positions.thy	Tue Jul 04 18:09:29 2017 +0100
@@ -1024,11 +1024,31 @@
   by (simp add: PosOrd_ex1_def)
 qed
 
+lemma Posix_PosOrd_stronger:
+  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
+  shows "v1 :\<sqsubseteq>val v2"
+proof -
+  from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s"
+  unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto
+  moreover
+    { assume "v2 \<in> CPT r s" 
+      with assms(1) have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd)
+    }
+  moreover
+    { assume "flat v2 \<sqsubset>spre s"
+      then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
+        using Posix1(2) by blast
+      then have "v1 :\<sqsubseteq>val v2"
+        by (simp add: PosOrd_ex1_def PosOrd_spreI) 
+    }
+  ultimately show "v1 :\<sqsubseteq>val v2" by blast
+qed
+
 lemma Posix_PosOrd_reverse:
   assumes "s \<in> r \<rightarrow> v1" 
-  shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
+  shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
 using assms
-by (metis Posix_PosOrd less_irrefl PosOrd_def 
+by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
     PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)