# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1499182969 -3600
# Node ID 45ad887fa6aa73106af3e7a4a12b11db2fbdcb51
# Parent  247fc5dd49435cb98f7f17f3b8008783c1a457f6
isar proofs

diff -r 247fc5dd4943 -r 45ad887fa6aa thys/Positions.thy
--- a/thys/Positions.thy	Tue Jul 04 15:59:31 2017 +0100
+++ b/thys/Positions.thy	Tue Jul 04 16:42:49 2017 +0100
@@ -868,165 +868,146 @@
 
 section {* The Posix Value is smaller than any other Value *}
 
+
 lemma Posix_PosOrd:
-  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
+  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
   shows "v1 :\<sqsubseteq>val v2"
 using assms
 proof (induct arbitrary: v2 rule: Posix.induct)
   case (Posix_ONE v)
-  have "v \<in> CPTpre ONE []" by fact
+  have "v \<in> CPT ONE []" by fact
+  then have "v = Void"
+    by (simp add: CPT_simps)
   then show "Void :\<sqsubseteq>val v"
-    by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases)
+    by (simp add: PosOrd_ex1_def)
 next
   case (Posix_CHAR c v)
-  have "v \<in> CPTpre (CHAR c) [c]" by fact
+  have "v \<in> CPT (CHAR c) [c]" by fact
+  then have "v = Char c"
+    by (simp add: CPT_simps)
   then show "Char c :\<sqsubseteq>val v"
-    by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases)
+    by (simp add: PosOrd_ex1_def)
 next
   case (Posix_ALT1 s r1 v r2 v2)
   have as1: "s \<in> r1 \<rightarrow> v" by fact
-  have IH: "\<And>v2. v2 \<in> CPTpre r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CPTpre (ALT r1 r2) s" by fact
-  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s"
-    by(auto simp add: CPTpre_def prefix_list_def)
+  have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> CPT (ALT r1 r2) s" by fact
+  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
+    by(auto simp add: CPT_def prefix_list_def)
   then consider
-    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" 
-  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s"
+    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
+  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   by (auto elim: CPrf.cases)
   then show "Left v :\<sqsubseteq>val v2"
   proof(cases)
      case (Left v3)
-     have "v3 \<in> CPTpre r1 s" using Left(2,3) 
-       by (auto simp add: CPTpre_def prefix_list_def)
+     have "v3 \<in> CPT r1 s" using Left(2,3) 
+       by (auto simp add: CPT_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
-     have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3)
-       by (simp add: Posix1(2) sprefix_list_def) 
+     have "flat v3 = flat v" using as1 Left(3)
+       by (simp add: Posix1(2)) 
      ultimately have "Left v :\<sqsubseteq>val Left v3"
-       by (auto simp add: PosOrd_ex1_def PosOrd_LeftI PosOrd_spreI)
+       by (auto simp add: PosOrd_ex1_def PosOrd_LeftI)
      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
   next
      case (Right v3)
-     have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3)
-       by (simp add: Posix1(2) sprefix_list_def) 
+     have "flat v3 = flat v" using as1 Right(3)
+       by (simp add: Posix1(2)) 
      then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
-       by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right PosOrd_spreI)
+       by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right)
      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
   qed
 next
   case (Posix_ALT2 s r2 v r1 v2)
   have as1: "s \<in> r2 \<rightarrow> v" by fact
   have as2: "s \<notin> L r1" by fact
-  have IH: "\<And>v2. v2 \<in> CPTpre r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CPTpre (ALT r1 r2) s" by fact
-  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 \<sqsubseteq>pre s"
-    by(auto simp add: CPTpre_def prefix_list_def)
+  have IH: "\<And>v2. v2 \<in> CPT r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> CPT (ALT r1 r2) s" by fact
+  then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
+    by(auto simp add: CPT_def prefix_list_def)
   then consider
-    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 \<sqsubseteq>pre s" 
-  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 \<sqsubseteq>pre s"
+    (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
+  | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   by (auto elim: CPrf.cases)
   then show "Right v :\<sqsubseteq>val v2"
   proof (cases)
     case (Right v3)
-     have "v3 \<in> CPTpre r2 s" using Right(2,3) 
-       by (auto simp add: CPTpre_def prefix_list_def)
+     have "v3 \<in> CPT r2 s" using Right(2,3) 
+       by (auto simp add: CPT_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
-     have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Right(3)
-       by (simp add: Posix1(2) sprefix_list_def) 
+     have "flat v3 = flat v" using as1 Right(3)
+       by (simp add: Posix1(2)) 
      ultimately have "Right v :\<sqsubseteq>val Right v3" 
-        by (auto simp add: PosOrd_ex1_def PosOrd_RightI PosOrd_spreI)
+        by (auto simp add: PosOrd_ex1_def PosOrd_RightI)
      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   next
      case (Left v3)
-     have w: "v3 \<in> CPTpre r1 s" using Left(2,3) as2  
-       by (auto simp add: CPTpre_def prefix_list_def)
-     have "flat v3 \<sqsubset>spre flat v \<or> flat v3 = flat v" using as1 Left(3)
-       by (simp add: Posix1(2) sprefix_list_def) 
-     then have "flat v3 \<sqsubset>spre flat v \<or> \<Turnstile> v3 : r1" using w 
-       by(auto simp add: CPTpre_def)
-     then have "flat v3 \<sqsubset>spre flat v" using as1 as2 Left
-       by (auto simp add: prefix_list_def sprefix_list_def Posix1(2) L_flat_Prf1 Prf_CPrf)
-     then have "Right v :\<sqsubseteq>val Left v3"
-       by (simp add: PosOrd_ex1_def PosOrd_spreI)
-     then show "Right v :\<sqsubseteq>val v2" unfolding Left .
+     have "v3 \<in> CPT r1 s" using Left(2,3) as2  
+       by (auto simp add: CPT_def prefix_list_def)
+     then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
+       by (simp add: Posix1(2) CPT_def) 
+     then have "False" using as1 as2 Left
+       by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
+     then show "Right v :\<sqsubseteq>val v2" by simp
   qed
 next 
   case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
   have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
-  have IH1: "\<And>v3. v3 \<in> CPTpre r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CPTpre r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
+  have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
-  have "v3 \<in> CPTpre (SEQ r1 r2) (s1 @ s2)" by fact
+  have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact
   then obtain v3a v3b where eqs:
     "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
-    "flat v3a @ flat v3b \<sqsubseteq>pre s1 @ s2" 
-    by (force simp add: prefix_list_def CPTpre_def elim: CPrf.cases)
-  then have "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2 \<or> flat v3a @ flat v3b = s1 @ s2"
-    by (simp add: sprefix_list_def)
-  moreover
-    { assume "flat v3a @ flat v3b \<sqsubset>spre s1 @ s2"
-      then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using as1 
-        by (auto simp add: PosOrd_ex1_def PosOrd_spreI Posix1(2))
-    }
-  moreover
-    { assume q1: "flat v3a @ flat v3b = s1 @ s2"
-      then have "flat v3a \<sqsubseteq>pre s1" using eqs(2,3) cond 
-        unfolding prefix_list_def
-        by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
-      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using q1
-        by (simp add: sprefix_list_def append_eq_conv_conj)
-      then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
-        using PosOrd_spreI Posix1(2) as1(1) q1 by blast
-      then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r1 s1 \<and> v3b \<in> CPTpre r2 s2)" using eqs(2,3)
-        by (auto simp add: CPTpre_def)
-      then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
-      then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using q1 q2 as1
-        unfolding  PosOrd_ex1_def
-        by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) 
-    }
-  ultimately show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
+    "flat v3a @ flat v3b = s1 @ s2" 
+    by (force simp add: prefix_list_def CPT_def elim: CPrf.cases)
+  with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
+    by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
+  then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
+    by (simp add: sprefix_list_def append_eq_conv_conj)
+  then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
+    using PosOrd_spreI Posix1(2) as1(1) eqs by blast
+  then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3)
+    by (auto simp add: CPT_def)
+  then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
+  then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
+    unfolding  PosOrd_ex1_def
+    by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5)) 
+  then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next 
   case (Posix_STAR1 s1 r v s2 vs v3) 
   have as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
-  have IH1: "\<And>v3. v3 \<in> CPTpre r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CPTpre (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   have cond2: "flat v \<noteq> []" by fact
-  have "v3 \<in> CPTpre (STAR r) (s1 @ s2)" by fact
+  have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
   then consider
     (NonEmpty) v3a vs3 where
     "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
-    "flat v3a @ flat (Stars vs3) \<sqsubseteq>pre s1 @ s2"
+    "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v3 = Stars []"
-    by (force simp add: CPTpre_def prefix_list_def elim: CPrf.cases)
+  by (force simp add: CPT_def elim: CPrf.cases)
   then show "Stars (v # vs) :\<sqsubseteq>val v3"
     proof (cases)
       case (NonEmpty v3a vs3)
-      then have "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2 \<or> flat (Stars (v3a # vs3)) = s1 @ s2"
-      by (simp add: sprefix_list_def)
-        moreover
-          { assume "flat (Stars (v3a # vs3)) \<sqsubset>spre s1 @ s2"
-            then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using as1
-            by (metis PosOrd_ex1_def PosOrd_spreI Posix1(2) flat.simps(7))
-          }
-        moreover
-          { assume q1: "flat (Stars (v3a # vs3)) = s1 @ s2"
-            then have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) cond 
-            unfolding prefix_list_def
-              by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7))
-            then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using q1
-              by (simp add: sprefix_list_def append_eq_conv_conj)
-            then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
-              using PosOrd_spreI Posix1(2) as1(1) q1 by blast
-            then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPTpre r s1 \<and> Stars vs3 \<in> CPTpre (STAR r) s2)" 
-              using NonEmpty(2,3) by (auto simp add: CPTpre_def)
-            then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast         
-            then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using q1 q2 as1
-              unfolding  PosOrd_ex1_def
-              by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5))
-           }
-        ultimately show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+      have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) 
+      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+        by (simp add: sprefix_list_def append_eq_conv_conj)
+      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
+        using PosOrd_spreI Posix1(2) as1(1) NonEmpty(4) by blast
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" 
+        using NonEmpty(2,3) by (auto simp add: CPT_def)
+      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast         
+      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+        unfolding  PosOrd_ex1_def
+        by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5))
+      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
     next 
       case Empty
       have "v3 = Stars []" by fact
@@ -1036,25 +1017,18 @@
     qed      
 next 
   case (Posix_STAR2 r v2)
-  have "v2 \<in> CPTpre (STAR r) []" by fact
-  then have "v2 = Stars []" using CPTpre_subsets by auto
+  have "v2 \<in> CPT (STAR r) []" by fact
+  then have "v2 = Stars []" 
+    unfolding CPT_def by (auto elim: CPrf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
   by (simp add: PosOrd_ex1_def)
 qed
 
-
-lemma Posix_PosOrd_stronger:
-  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
-  shows "v1 :\<sqsubseteq>val v2"
-using assms Posix_PosOrd
-using CPT_CPTpre_subset by blast
-
-
 lemma Posix_PosOrd_reverse:
   assumes "s \<in> r \<rightarrow> v1" 
   shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
 using assms
-by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
+by (metis Posix_PosOrd less_irrefl PosOrd_def 
     PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)