# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1498642625 -3600
# Node ID 222ed43892ea1e71f6e511ae70d188c871c0c0ba
# Parent  7c89d3f6923e83ee1ceeac02fdfacb2d5e61b080
updated

diff -r 7c89d3f6923e -r 222ed43892ea thys/Positions.thy
--- 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]
diff -r 7c89d3f6923e -r 222ed43892ea thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Tue Jun 27 13:15:55 2017 +0100
+++ b/thys/Sulzmann.thy	Wed Jun 28 10:37:05 2017 +0100
@@ -6,6 +6,20 @@
 
 section {* Sulzmann's "Ordering" of Values *}
 
+inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100)
+where
+  MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" 
+| C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" 
+| C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" 
+| A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)"
+| A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')"
+| A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')"
+| K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))"
+| K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))"
+| K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk>  \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))"
+
+
+(*
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
 where
   C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" 
@@ -18,6 +32,7 @@
 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
 | K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
 | K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
+*)
 (*| MY1: "Void \<preceq>ONE Void" 
 | MY2: "(Char c) \<preceq>(CHAR c) (Char c)" 
 | MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" 
@@ -44,7 +59,7 @@
 *)
 
 lemma ValOrd_irrefl: 
-  assumes "\<turnstile> v : r"  "v \<preceq>r v" 
+  assumes "\<turnstile> v : r"  "v \<prec> v" 
   shows "False"
 using assms
 apply(induct v r rule: Prf.induct)
@@ -72,25 +87,105 @@
 
 
 lemma Posix_CPT2:
-  assumes "v1 \<preceq>r v2" "flat v2 \<sqsubseteq>pre s" "flat v1 \<sqsubseteq>pre s"
+  assumes "v1 \<prec> v2" 
   shows "v1 :\<sqsubset>val v2" 
 using assms
-apply(induct v1 r v2 arbitrary: s rule: ValOrd.induct)
-prefer 3
-apply(simp)
+apply(induct v1 v2 arbitrary: rule: ValOrd.induct)
 apply(rule val_ord_shorterI)
 apply(simp)
-apply(subst (asm) (3) prefix_list_def)
-apply(subst (asm) (3) prefix_list_def)
-apply(clarify)
-apply(simp)
-apply(simp add: append_eq_append_conv2)
-apply(auto)[1]
-apply(drule_tac x="flat v1' @ flat v2' @ usa" in meta_spec)
-apply(simp add: prefix_list_def)
 apply(rule val_ord_SeqI1)
 apply(simp)
 apply(simp)
+apply(rule val_ord_SeqI2)
+apply(simp)
+apply(simp)
+apply(simp add: val_ord_ex_def)
+apply(rule_tac x="[0]" in exI)
+apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1]
+apply(smt inlen_bigger)
+apply(rule val_ord_RightI)
+apply(simp)
+apply(simp)
+apply(rule val_ord_LeftI)
+apply(simp)
+apply(simp)
+defer
+apply(rule val_ord_StarsI)
+apply(simp)
+apply(simp)
+apply(rule val_ord_StarsI2)
+apply(simp)
+apply(simp)
+oops
+
+lemma Posix_CPT2:
+  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
+  shows "v1 \<prec> v2"
+using assms
+apply(induct r arbitrary: v1 v2 s)  
+apply(auto simp add: CPTpre_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(auto simp add: CPTpre_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(auto simp add: CPTpre_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(simp add: val_ord_ex_def)
+apply(auto simp add: val_ord_def)[1]
+apply(auto simp add: CPTpre_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(auto simp add: val_ord_ex_def val_ord_def)[1]
+(* SEQ case *)
+apply(subst (asm) (5) CPTpre_def)
+apply(subst (asm) (5) CPTpre_def)
+apply(auto)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule val_ord_SeqE)
+apply(erule disjE)
+apply(drule_tac x="v1a" in meta_spec)
+apply(rotate_tac 7)
+apply(drule_tac x="v1b" in meta_spec)
+apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
+apply(auto simp add: CPTpre_def)[1]
+apply(drule meta_mp)
+apply(auto simp add: CPTpre_def)[1]
+apply(rule ValOrd.intros)
+apply(subst (asm) (3) CPTpre_def)
+apply(subst (asm) (3) CPTpre_def)
+apply(auto)[1]
+apply(drule_tac meta_mp)
+apply(auto simp add: CPTpre_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule val_ord_SeqE)
+apply(erule disjE)
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+prefer 2
+apply(rule  ValOrd.intros(2))
+prefer 2
+apply(simp)
+thm ValOrd.intros
+apply(case_tac "flat v1b = flat v1a")
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp)
+
+
 
 
 lemma Posix_CPT: