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: