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

diff -r 160d0b08471c -r 247fc5dd4943 thys/Lexer.thy
--- a/thys/Lexer.thy	Sat Jul 01 13:08:48 2017 +0100
+++ b/thys/Lexer.thy	Tue Jul 04 15:59:31 2017 +0100
@@ -171,6 +171,9 @@
 apply(simp_all add: Ders_def der_correctness Der_def)
 done
 
+
+section {* Lemmas about ders *}
+
 lemma ders_ZERO:
   shows "ders s (ZERO) = ZERO"
 apply(induct s)
@@ -184,8 +187,9 @@
 done
 
 lemma ders_CHAR:
-  shows "ders s (CHAR c) = (if s = [c] then ONE else 
-                           (if s = [] then (CHAR c) else ZERO))"
+  shows "ders s (CHAR c) = 
+           (if s = [c] then ONE else 
+           (if s = [] then (CHAR c) else ZERO))"
 apply(induct s)
 apply(simp_all add: ders_ZERO ders_ONE)
 done
diff -r 160d0b08471c -r 247fc5dd4943 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Jul 01 13:08:48 2017 +0100
+++ b/thys/LexerExt.thy	Tue Jul 04 15:59:31 2017 +0100
@@ -362,6 +362,7 @@
 apply(auto)
 using Der_UNION Der_star Star_def by fastforce
 
+
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
 apply(induct s arbitrary: r)
diff -r 160d0b08471c -r 247fc5dd4943 thys/Positions.thy
--- a/thys/Positions.thy	Sat Jul 01 13:08:48 2017 +0100
+++ b/thys/Positions.thy	Tue Jul 04 15:59:31 2017 +0100
@@ -162,26 +162,57 @@
 section {* Ordering of values according to Okui & Suzuki *}
 
 
-definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
+definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
+where
+  "v1 \<sqsubset>val p v2 \<equiv> p \<in> Pos v1 \<and> 
+                   pflat_len v1 p > pflat_len v2 p \<and>
+                   (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
+
+definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _")
 where
-  "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> 
-                    pflat_len v1 p > pflat_len v2 p \<and>
-                   (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))"
+  "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and> 
+                    (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and>
+                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> (pflat_len v1 q = pflat_len v2 q))"
+
+lemma 
+  assumes "v1 \<sqsubset>fval p v2" 
+  shows "v1 \<sqsubset>val p v2"
+using assms
+unfolding ValFlat_ord_def PosOrd_def
+apply(clarify)
+apply(simp add: pflat_len_def)
+apply(auto)[1]
+apply(smt intlen_bigger)
+apply(simp add: sprefix_list_def prefix_list_def)
+apply(auto)[1]
+apply(drule sym)
+apply(simp add: intlen_append)
+apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3))
+apply(smt intlen_bigger)
+done
+
+lemma 
+  assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)"
+  shows "v1 \<sqsubset>fval p v2"
+using assms
+unfolding ValFlat_ord_def PosOrd_def
+apply(clarify)
+done
 
 
-definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")
+definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
 where
   "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
 
-definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
+definition PosOrd_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
-lemma val_ord_shorterE:
+lemma PosOrd_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(auto simp add: PosOrd_ex_def PosOrd_def)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
 apply(simp add: intlen_length)
@@ -192,56 +223,64 @@
 by (metis intlen_length le_less less_irrefl linear)
 
 
-lemma val_ord_shorterI:
+lemma PosOrd_shorterI:
   assumes "length (flat v') < length (flat v)"
   shows "v :\<sqsubset>val v'" 
 using assms
-unfolding val_ord_ex_def
-by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def)
+unfolding PosOrd_ex_def
+by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
 
-lemma val_ord_spreI:
+lemma PosOrd_spreI:
   assumes "(flat v') \<sqsubset>spre (flat v)"
   shows "v :\<sqsubset>val v'" 
 using assms
-apply(rule_tac val_ord_shorterI)
+apply(rule_tac PosOrd_shorterI)
 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
-
+lemma PosOrd_Left_Right:
+  assumes "flat v1 = flat v2"
+  shows "Left v1 :\<sqsubset>val Right v2" 
+unfolding PosOrd_ex_def
+apply(rule_tac x="[0]" in exI)
+using assms
+apply(auto simp add: PosOrd_def pflat_len_simps Pos_empty)
+apply(smt intlen_bigger)
+done
 
-lemma val_ord_LeftI:
+lemma PosOrd_LeftI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Left v) :\<sqsubset>val (Left v')" 
 using assms(1)
-unfolding val_ord_ex_def
+unfolding PosOrd_ex_def
 apply(auto)
 apply(rule_tac x="0#p" in exI)
 using assms(2)
-apply(auto simp add: val_ord_def pflat_len_simps)
+apply(auto simp add: PosOrd_def pflat_len_simps)
 done
 
-lemma val_ord_RightI:
+lemma PosOrd_RightI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Right v) :\<sqsubset>val (Right v')" 
 using assms(1)
-unfolding val_ord_ex_def
+unfolding PosOrd_ex_def
 apply(auto)
 apply(rule_tac x="Suc 0#p" in exI)
 using assms(2)
-apply(auto simp add: val_ord_def pflat_len_simps)
+apply(auto simp add: PosOrd_def pflat_len_simps)
 done
 
-lemma val_ord_LeftE:
+lemma PosOrd_LeftE:
   assumes "(Left v1) :\<sqsubset>val (Left v2)"
   shows "v1 :\<sqsubset>val v2"
 using assms
-apply(simp add: val_ord_ex_def)
+apply(simp add: PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac "p = []")
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto simp add: pflat_len_simps)
 apply(rule_tac x="[]" in exI)
 apply(simp add: Pos_empty pflat_len_simps)
-apply(auto simp add: pflat_len_simps val_ord_def)
+apply(auto simp add: pflat_len_simps PosOrd_def)
 apply(rule_tac x="ps" in exI)
 apply(auto)
 apply(drule_tac x="0#q" in bspec)
@@ -252,18 +291,18 @@
 apply(simp add: pflat_len_simps)
 done
 
-lemma val_ord_RightE:
+lemma PosOrd_RightE:
   assumes "(Right v1) :\<sqsubset>val (Right v2)"
   shows "v1 :\<sqsubset>val v2"
 using assms
-apply(simp add: val_ord_ex_def)
+apply(simp add: PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac "p = []")
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto simp add: pflat_len_simps)
 apply(rule_tac x="[]" in exI)
 apply(simp add: Pos_empty pflat_len_simps)
-apply(auto simp add: pflat_len_simps val_ord_def)
+apply(auto simp add: pflat_len_simps PosOrd_def)
 apply(rule_tac x="ps" in exI)
 apply(auto)
 apply(drule_tac x="Suc 0#q" in bspec)
@@ -275,16 +314,16 @@
 done
 
 
-lemma val_ord_SeqI1:
+lemma PosOrd_SeqI1:
   assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
 using assms(1)
-apply(subst (asm) val_ord_ex_def)
-apply(subst (asm) val_ord_def)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
 apply(clarify)
-apply(subst val_ord_ex_def)
+apply(subst PosOrd_ex_def)
 apply(rule_tac x="0#p" in exI)
-apply(subst val_ord_def)
+apply(subst PosOrd_def)
 apply(rule conjI)
 apply(simp)
 apply(rule conjI)
@@ -299,16 +338,16 @@
 apply(auto simp add: pflat_len_simps)[2]
 done
 
-lemma val_ord_SeqI2:
+lemma PosOrd_SeqI2:
   assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
   shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" 
 using assms(1)
-apply(subst (asm) val_ord_ex_def)
-apply(subst (asm) val_ord_def)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
 apply(clarify)
-apply(subst val_ord_ex_def)
+apply(subst PosOrd_ex_def)
 apply(rule_tac x="Suc 0#p" in exI)
-apply(subst val_ord_def)
+apply(subst PosOrd_def)
 apply(rule conjI)
 apply(simp)
 apply(rule conjI)
@@ -323,21 +362,21 @@
 apply(auto simp add: pflat_len_simps)
 done
 
-lemma val_ord_SeqE:
+lemma PosOrd_SeqE:
   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
   shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
 using assms
-apply(simp add: val_ord_ex_def)
+apply(simp add: PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac p)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto simp add: pflat_len_simps intlen_append)[1]
 apply(rule_tac x="[]" in exI)
 apply(drule_tac x="[]" in spec)
 apply(simp add: Pos_empty pflat_len_simps)
 apply(case_tac a)
 apply(rule disjI1)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto simp add: pflat_len_simps intlen_append)[1]
 apply(rule_tac x="list" in exI)
 apply(simp)
@@ -348,7 +387,7 @@
 apply(simp add: pflat_len_simps)
 apply(case_tac nat)
 apply(rule disjI2)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto simp add: pflat_len_simps intlen_append)
 apply(rule_tac x="list" in exI)
 apply(simp add: Pos_empty)
@@ -357,18 +396,18 @@
 apply(drule_tac x="Suc 0#q" in bspec)
 apply(simp)
 apply(simp add: pflat_len_simps)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 done
 
-lemma val_ord_StarsI:
+lemma PosOrd_StarsI:
   assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
   shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" 
 using assms(1)
-apply(subst (asm) val_ord_ex_def)
-apply(subst (asm) val_ord_def)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
 apply(clarify)
-apply(subst val_ord_ex_def)
-apply(subst val_ord_def)
+apply(subst PosOrd_ex_def)
+apply(subst PosOrd_def)
 apply(rule_tac x="0#p" in exI)
 apply(simp add: pflat_len_Stars_simps pflat_len_simps)
 using assms(2)
@@ -376,15 +415,15 @@
 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 done
 
-lemma val_ord_StarsI2:
+lemma PosOrd_StarsI2:
   assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
   shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" 
 using assms(1)
-apply(subst (asm) val_ord_ex_def)
-apply(subst (asm) val_ord_def)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
 apply(clarify)
-apply(subst val_ord_ex_def)
-apply(subst val_ord_def)
+apply(subst PosOrd_ex_def)
+apply(subst PosOrd_def)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
 apply(rule_tac x="[]" in exI)
@@ -396,74 +435,74 @@
 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 done
 
-lemma val_ord_Stars_appendI:
+lemma PosOrd_Stars_appendI:
   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
 using assms
 apply(induct vs)
 apply(simp)
-apply(simp add: val_ord_StarsI2)
+apply(simp add: PosOrd_StarsI2)
 done
 
-lemma val_ord_StarsE2:
+lemma PosOrd_StarsE2:
   assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
   shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
-apply(subst (asm) val_ord_ex_def)
+apply(subst (asm) PosOrd_ex_def)
 apply(erule exE)
 apply(case_tac p)
 apply(simp)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
-apply(subst val_ord_ex_def)
+apply(simp add: PosOrd_def pflat_len_simps intlen_append)
+apply(subst PosOrd_ex_def)
 apply(rule_tac x="[]" in exI)
-apply(simp add: val_ord_def pflat_len_simps Pos_empty)
+apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
 apply(simp)
 apply(case_tac a)
 apply(clarify)
-apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
+apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def)[1]
 apply(clarify)
-apply(simp add: val_ord_ex_def)
+apply(simp add: PosOrd_ex_def)
 apply(rule_tac x="nat#list" in exI)
-apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
 apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
+apply(simp add: PosOrd_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(drule_tac x="Suc a # lista" in bspec)
 apply(simp)
-apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
 apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
+apply(simp add: PosOrd_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(drule_tac x="Suc a # lista" in bspec)
 apply(simp)
-apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
+apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
 done
 
-lemma val_ord_Stars_appendE:
+lemma PosOrd_Stars_appendE:
   assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(induct vs)
 apply(simp)
-apply(simp add: val_ord_StarsE2)
+apply(simp add: PosOrd_StarsE2)
 done
 
-lemma val_ord_Stars_append_eq:
+lemma PosOrd_Stars_append_eq:
   assumes "flat (Stars vs1) = flat (Stars vs2)"
   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(rule_tac iffI)
-apply(erule val_ord_Stars_appendE)
-apply(rule val_ord_Stars_appendI)
+apply(erule PosOrd_Stars_appendE)
+apply(rule PosOrd_Stars_appendI)
 apply(auto)
 done
 
 
-lemma val_ord_trans:
+lemma PosOrd_trans:
   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
   shows "v1 :\<sqsubset>val v3"
 using assms
-unfolding val_ord_ex_def
+unfolding PosOrd_ex_def
 apply(clarify)
 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")
 prefer 2
@@ -471,35 +510,35 @@
 apply(erule disjE)
 apply(simp)
 apply(rule_tac x="pa" in exI)
-apply(subst val_ord_def)
+apply(subst PosOrd_def)
 apply(rule conjI)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto)[1]
-apply(simp add: val_ord_def)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
+apply(simp add: PosOrd_def)
 apply(auto)[1]
 using outside_lemma apply blast
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto)[1]
 using outside_lemma apply force
 apply auto[1]
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto)[1]
 apply (metis (no_types, hide_lams) lex_trans outside_lemma)
-apply(simp add: val_ord_def)
+apply(simp add: PosOrd_def)
 apply(auto)[1]
 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def)
 
-lemma val_ord_irrefl:
+lemma PosOrd_irrefl:
   assumes "v :\<sqsubset>val v"
   shows "False"
 using assms
-by(auto simp add: val_ord_ex_def val_ord_def)
+by(auto simp add: PosOrd_ex_def PosOrd_def)
 
-lemma val_ord_almost_trichotomous:
+lemma PosOrd_almost_trichotomous:
   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
-apply(auto simp add: val_ord_ex_def)
-apply(auto simp add: val_ord_def)
+apply(auto simp add: PosOrd_ex_def)
+apply(auto simp add: PosOrd_def)
 apply(rule_tac x="[]" in exI)
 apply(auto simp add: Pos_empty pflat_len_simps)
 apply(drule_tac x="[]" in spec)
@@ -510,8 +549,8 @@
   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
   shows "False"
 using assms
-apply(auto simp add: val_ord_ex_def val_ord_def)
-using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast
+apply(auto simp add: PosOrd_ex_def PosOrd_def)
+using assms(1) assms(2) PosOrd_irrefl PosOrd_trans by blast
 
 lemma WW2:
   assumes "\<not>(v1 :\<sqsubset>val v2)" 
@@ -519,17 +558,17 @@
 using assms
 oops
 
-lemma val_ord_SeqE2:
+lemma PosOrd_SeqE2:
   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
   shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
 using assms 
-apply(frule_tac val_ord_SeqE)
+apply(frule_tac PosOrd_SeqE)
 apply(erule disjE)
 apply(simp)
 apply(auto)
 apply(case_tac "v1 :\<sqsubset>val v1'")
 apply(simp)
-apply(auto simp add: val_ord_ex_def)
+apply(auto simp add: PosOrd_ex_def)
 apply(case_tac "v1 = v1'")
 apply(simp)
 oops
@@ -605,7 +644,7 @@
 apply(simp)
 done
 
-lemma val_ord_trichotomous_stronger:
+lemma PosOrd_trichotomous_stronger:
   assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
 oops
@@ -827,224 +866,199 @@
 apply(rule CPrf.intros)
 done
 
-lemma Posix_val_ord:
+section {* The Posix Value is smaller than any other Value *}
+
+lemma Posix_PosOrd:
   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
   shows "v1 :\<sqsubseteq>val v2"
 using assms
-apply(induct arbitrary: v2 rule: Posix.induct)
-apply(simp add: CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: val_ord_ex1_def)
-apply(simp add: CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: val_ord_ex1_def)
-(* ALT1 *)
-prefer 3
-(* SEQ case *)
-apply(subst (asm) (3) CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(case_tac "s' = []")
-apply(simp)
-prefer 2
-apply(simp add: val_ord_ex1_def)
-apply(clarify)
-apply(simp)
-apply(simp add: val_ord_ex_def)
-apply(simp (no_asm) add: val_ord_def)
-apply(rule_tac x="[]" in exI)
-apply(simp add: pflat_len_simps)
-apply(simp only: intlen_length)
-apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le)
-apply(subgoal_tac "length (flat v1a) \<le> length s1")
-prefer 2
-apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil)
-apply(subst (asm) append_eq_append_conv_if)
-apply(simp)
-apply(clarify)
-apply(drule_tac x="v1a" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-using append_eq_conv_conj apply blast
-apply(subst (asm) (2)val_ord_ex1_def)
-apply(erule disjE)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_SeqI1)
-apply(simp)
-apply(simp)
-apply (metis Posix1(2) append_assoc append_take_drop_id)
-apply(simp)
-apply(drule_tac x="v2b" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply (simp add: Posix1(2))
-apply(subst (asm) val_ord_ex1_def)
-apply(erule disjE)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_SeqI2)
-apply(simp)
-apply (simp add: Posix1(2))
-apply(subst val_ord_ex1_def)
-apply(simp)
-(* ALT *)
-apply(subst (asm) (2) CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply(case_tac "s' = []")
-apply(simp)
-apply(drule_tac x="v1" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(subst (asm) val_ord_ex1_def)
-apply(erule disjE)
-apply(subst (asm) val_ord_ex_def)
-apply(erule exE)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_LeftI)
-apply(subst val_ord_ex_def)
-apply(auto)[1]
-using Posix1(2) apply blast
-using val_ord_ex1_def apply blast
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply (simp add: Posix1(2) val_ord_shorterI)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(case_tac "s' = []")
-apply(simp)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="[0]" in exI)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp add: Pos_empty)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply (smt intlen_bigger)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-using Posix1(2) apply auto[1]
-apply(rule ballI)
-apply(rule impI)
-apply(case_tac "q = []")
-using Posix1(2) apply auto[1]
-apply(auto)[1]
-apply(rule val_ord_shorterI)
-apply(simp)
-apply (simp add: Posix1(2))
-(* ALT RIGHT *)
-apply(subst (asm) (2) CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply(case_tac "s' = []")
-apply(simp)
-apply (simp add: L_flat_Prf1 Prf_CPrf)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply (simp add: Posix1(2))
-apply(case_tac "s' = []")
-apply(simp)
-apply(drule_tac x="v2a" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(subst (asm) val_ord_ex1_def)
-apply(erule disjE)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_RightI)
-apply(simp)
-using Posix1(2) apply blast
-apply (simp add: val_ord_ex1_def)
-apply(subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply (simp add: Posix1(2))
-(* STAR empty case *)
-prefer 2
-apply(subst (asm) CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply (simp add: val_ord_ex1_def)
-(* STAR non-empty case *)
-apply(subst (asm) (3) CPTpre_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply (simp add: val_ord_ex1_def)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply(case_tac "s' = []")
-apply(simp)
-prefer 2
-apply (simp add: val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less)
-apply(drule_tac x="va" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv)
-apply (subst (asm) (2) val_ord_ex1_def)
-apply(erule disjE)
-prefer 2
-apply(simp)
-apply(drule_tac x="Stars vsa" in meta_spec)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply (simp add: Posix1(2))
-apply (subst (asm) val_ord_ex1_def)
-apply(erule disjE)
-apply (subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_StarsI2)
-apply(simp)
-using Posix1(2) apply force
-apply(simp add: val_ord_ex1_def)
-apply (subst val_ord_ex1_def)
-apply(rule disjI1)
-apply(rule val_ord_StarsI)
-apply(simp)
-apply(simp add: Posix1)
-using Posix1(2) by force
+proof (induct arbitrary: v2 rule: Posix.induct)
+  case (Posix_ONE v)
+  have "v \<in> CPTpre ONE []" by fact
+  then show "Void :\<sqsubseteq>val v"
+    by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases)
+next
+  case (Posix_CHAR c v)
+  have "v \<in> CPTpre (CHAR c) [c]" by fact
+  then show "Char c :\<sqsubseteq>val v"
+    by (auto simp add: CPTpre_def PosOrd_ex1_def elim: CPrf.cases)
+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)
+  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"
+  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)
+     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) 
+     ultimately have "Left v :\<sqsubseteq>val Left v3"
+       by (auto simp add: PosOrd_ex1_def PosOrd_LeftI PosOrd_spreI)
+     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) 
+     then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
+       by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right PosOrd_spreI)
+     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)
+  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"
+  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)
+     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) 
+     ultimately have "Right v :\<sqsubseteq>val Right v3" 
+        by (auto simp add: PosOrd_ex1_def PosOrd_RightI PosOrd_spreI)
+     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 .
+  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 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
+  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
+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 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
+  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"
+  | (Empty) "v3 = Stars []"
+    by (force simp add: CPTpre_def prefix_list_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
+    next 
+      case Empty
+      have "v3 = Stars []" by fact
+      then show "Stars (v # vs) :\<sqsubseteq>val v3"
+      unfolding PosOrd_ex1_def using cond2
+      by (simp add: PosOrd_shorterI)
+    qed      
+next 
+  case (Posix_STAR2 r v2)
+  have "v2 \<in> CPTpre (STAR r) []" by fact
+  then have "v2 = Stars []" using CPTpre_subsets by auto
+  then show "Stars [] :\<sqsubseteq>val v2"
+  by (simp add: PosOrd_ex1_def)
+qed
 
 
-lemma Posix_val_ord_stronger:
+lemma Posix_PosOrd_stronger:
   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
   shows "v1 :\<sqsubseteq>val v2"
-using assms
-apply(rule_tac Posix_val_ord)
-apply(assumption)
-using CPT_CPTpre_subset by auto
+using assms Posix_PosOrd
+using CPT_CPTpre_subset by blast
 
 
-lemma Posix_val_ord_reverse:
+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_val_ord_stronger less_irrefl val_ord_def 
-    val_ord_ex1_def val_ord_ex_def val_ord_trans)
+by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
+    PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)
 
 
-lemma val_ord_Posix_Stars:
+lemma PosOrd_Posix_Stars:
   assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
   and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
   shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
@@ -1066,15 +1080,15 @@
 apply(auto simp add: CPT_def PT_def)[1]
 apply(erule Prf.cases)
 apply(simp_all)
-apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
+apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_PosOrd_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
 apply(clarify)
 apply(drule_tac x="Stars (a#v#vsa)" in spec)
 apply(simp)
 apply(drule mp)
 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
-apply(subst (asm) (2) val_ord_ex_def)
+apply(subst (asm) (2) PosOrd_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
 apply(auto simp add: CPT_def PT_def)[1]
 using CPrf_stars apply auto[1]
 apply(auto)[1]
@@ -1088,7 +1102,7 @@
 apply(simp)
 apply(drule mp)
 using Prf.intros(7) apply blast
-apply(subst (asm) (2) val_ord_ex_def)
+apply(subst (asm) (2) PosOrd_ex_def)
 apply(simp)
 prefer 2
 apply(simp)
@@ -1107,20 +1121,20 @@
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)
-apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def)
+apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def PosOrd_ex_def)
 apply(drule_tac x="Stars (v#va#vsb)" in spec)
 apply(drule mp)
 apply (simp add: Posix1a Prf.intros(7))
 apply(simp)
-apply(subst (asm) (2) val_ord_ex_def)
+apply(subst (asm) (2) PosOrd_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
 proof -
   fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
   assume a1: "s\<^sub>3 \<noteq> []"
   assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
   assume a3: "flat vA = flat a @ s\<^sub>3"
-  assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)"
+  assume a4: "\<forall>p. \<not> (Stars (vA # vB) \<sqsubset>val p (Stars (a # vsa)))"
   have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs"
     by (meson drop_eq_Nil not_less)
   have f6: "\<not> length (flat vA) \<le> length (flat a)"
@@ -1128,189 +1142,201 @@
   have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))"
     using a3 a2 by simp
   then show False
-    using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI)
+    using f6 f5 a4 by (metis (full_types) drop_eq_Nil PosOrd_StarsI PosOrd_ex_def PosOrd_shorterI)
 qed
 
 
 
 
+section {* The Smallest Value is indeed the Posix Value *}
 
-lemma val_ord_Posix:
-  assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)"
+lemma PosOrd_Posix:
+  assumes "v1 \<in> CPT r s" "\<forall>v2 \<in> PT r s. \<not> v2 :\<sqsubset>val v1"
   shows "s \<in> r \<rightarrow> v1" 
 using assms
-apply(induct r arbitrary: s v1)
-apply(auto simp add: CPT_def PT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-(* ONE *)
-apply(auto simp add: CPT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule Posix.intros)
-(* CHAR *)
-apply(auto simp add: CPT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule Posix.intros)
-prefer 2
-(* ALT *)
-apply(auto simp add: CPT_def PT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule Posix.intros)
-apply(drule_tac x="flat v1a" in meta_spec)
-apply(drule_tac x="v1a" in meta_spec)
-apply(drule meta_mp)
-apply(simp)
-apply(drule meta_mp)
-apply(auto)[1]
-apply(drule_tac x="Left v2" in spec)
-apply(simp)
-apply(drule mp)
-apply(rule Prf.intros)
-apply(simp)
-apply (meson val_ord_LeftI)
-apply(assumption)
-(* ALT Right *)
-apply(auto simp add: CPT_def)[1]
-apply(rule Posix.intros)
-apply(rotate_tac 1)
-apply(drule_tac x="flat v2" in meta_spec)
-apply(drule_tac x="v2" in meta_spec)
-apply(drule meta_mp)
-apply(simp)
-apply(drule meta_mp)
-apply(auto)[1]
-apply(drule_tac x="Right v2a" in spec)
-apply(simp)
-apply(drule mp)
-apply(rule Prf.intros)
-apply(simp)
-apply(drule val_ord_RightI)
-apply(assumption)
-apply(auto simp add: val_ord_ex_def)[1]
-apply(assumption)
-apply(auto)[1]
-apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a")
-apply(clarify)
-apply(drule_tac x="Left v2'" in spec)
-apply(simp)
-apply(drule mp)
-apply(rule Prf.intros)
-apply(assumption)
-apply(simp add: val_ord_ex_def)
-apply(subst (asm) (3) val_ord_def)
-apply(simp)
-apply(simp add: pflat_len_simps)
-apply(drule_tac x="[0]" in spec)
-apply(simp add: pflat_len_simps Pos_empty)
-apply(drule mp)
-apply (smt intlen_bigger)
-apply(erule disjE)
-apply blast
-apply auto[1]
-apply (meson L_flat_Prf2)
-(* SEQ *)
-apply(auto simp add: CPT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule Posix.intros)
-apply(drule_tac x="flat v1a" in meta_spec)
-apply(drule_tac x="v1a" in meta_spec)
-apply(drule meta_mp)
-apply(simp)
-apply(drule meta_mp)
-apply(auto)[1]
-apply(auto simp add: PT_def)[1]
-apply(drule_tac x="Seq v2a v2" in spec)
-apply(simp)
-apply(drule mp)
-apply (simp add: Prf.intros(1) Prf_CPrf)
-using val_ord_SeqI1 apply fastforce
-apply(assumption)
-apply(rotate_tac 1)
-apply(drule_tac x="flat v2" in meta_spec)
-apply(drule_tac x="v2" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(drule meta_mp)
-apply(auto)[1]
-apply(auto simp add: PT_def)[1]
-apply(drule_tac x="Seq v1a v2a" in spec)
-apply(simp)
-apply(drule mp)
-apply (simp add: Prf.intros(1) Prf_CPrf)
-apply (meson val_ord_SeqI2)
-apply(assumption)
-(* SEQ side condition *)
-apply(auto simp add: PT_def)
-apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a")
-prefer 2
-apply (meson L_flat_Prf2)
-apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a")
-prefer 2
-apply (meson L_flat_Prf2)
-apply(clarify)
-apply(drule_tac x="Seq vA vB" in spec)
-apply(simp)
-apply(drule mp)
-apply (simp add: Prf.intros(1))
-apply(subst (asm) (3) val_ord_ex_def)
-apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SeqI1 val_ord_ex_def val_ord_shorterI)
-(* STAR *)
-apply(auto simp add: CPT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-using Posix_STAR2 apply blast
-apply(clarify)
-apply(rule val_ord_Posix_Stars)
-apply(auto simp add: CPT_def)[1]
-apply (simp add: CPrf.intros(7))
-apply(auto)[1]
-apply(drule_tac x="flat v" in meta_spec)
-apply(drule_tac x="v" in meta_spec)
-apply(simp)
-apply(drule meta_mp)
-apply(auto)[1]
-apply(drule_tac x="Stars (v2#vs)" in spec)
-apply(simp)
-apply(drule mp)
-using Prf.intros(7) Prf_CPrf apply blast
-apply(simp add: val_ord_StarsI)
-apply(assumption)
-apply(drule_tac x="flat va" in meta_spec)
-apply(drule_tac x="va" in meta_spec)
-apply(simp)
-apply(drule meta_mp)
-using CPrf_stars apply blast
-apply(drule meta_mp)
-apply(auto)[1]
-apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post")
-prefer 2
-apply (metis append_Cons append_Nil in_set_conv_decomp_first)
-apply(clarify)
-apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec)
-apply(simp)
-apply(drule mp)
-apply(rule Prf.intros)
-apply (simp add: Prf_CPrf)
-apply(rule Prf_Stars_append)
-apply(drule CPrf_Stars_appendE)
-apply(auto simp add: Prf_CPrf)[1]
-apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD)
-apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)")
-apply(subst (asm) val_ord_Stars_append_eq)
-apply(simp)
-apply(subst (asm) val_ord_Stars_append_eq)
-apply(simp)
-prefer 2
-apply(simp)
-prefer 2
-apply(simp)
-apply (simp add: val_ord_StarsI)
-apply(auto simp add: PT_def)
-done
+proof(induct r arbitrary: s v1)
+  case (ZERO s v1)
+  have "v1 \<in> CPT ZERO s" by fact
+  then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def
+    by (auto elim: CPrf.cases)
+next 
+  case (ONE s v1)
+  have "v1 \<in> CPT ONE s" by fact
+  then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def
+    by(auto elim!: CPrf.cases intro: Posix.intros)
+next 
+  case (CHAR c s v1)
+  have "v1 \<in> CPT (CHAR c) s" by fact
+  then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_def
+    by (auto elim!: CPrf.cases intro: Posix.intros)
+next
+  case (ALT r1 r2 s v1)
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have as1: "\<forall>v2\<in>PT (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+  have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact
+  then consider 
+     (Left) v1' where
+        "v1 = Left v1'" "s = flat v1'"
+        "v1' \<in> CPT r1 s"
+  |  (Right) v1' where
+        "v1 = Right v1'" "s = flat v1'"
+        "v1' \<in> CPT r2 s"
+  unfolding CPT_def by (auto elim: CPrf.cases)
+  then show "s \<in> ALT r1 r2 \<rightarrow> v1"
+   proof (cases)
+     case (Left v1')
+     have "v1' \<in> CPT r1 s" using as2
+       unfolding CPT_def Left by (auto elim: CPrf.cases)
+     moreover
+     have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
+       unfolding PT_def Left using Prf.intros(2) PosOrd_LeftI by force  
+     ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
+     then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
+     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
+   next
+     case (Right v1')
+     have "v1' \<in> CPT r2 s" using as2
+       unfolding CPT_def Right by (auto elim: CPrf.cases)
+     moreover
+     have "\<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
+       unfolding PT_def Right using Prf.intros(3) PosOrd_RightI by force   
+     ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
+     moreover 
+       { assume "s \<in> L r1"
+         then obtain v' where "v' \<in>  PT r1 s"
+            unfolding PT_def using L_flat_Prf2 by blast
+         then have "Left v' \<in>  PT (ALT r1 r2) s" 
+            unfolding PT_def by (auto intro: Prf.intros)
+         with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
+            unfolding PT_def Right by (auto)
+         then have False using PosOrd_Left_Right Right by blast  
+       }
+     then have "s \<notin> L r1" by rule 
+     ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
+     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
+  qed
+next 
+  case (SEQ r1 r2 s v1)
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have as1: "\<forall>v2\<in>PT (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+  have as2: "v1 \<in> CPT (SEQ r1 r2) s" by fact
+  then obtain 
+    v1a v1b where eqs:
+        "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
+        "v1a \<in> CPT r1 (flat v1a)" "v1b \<in> CPT r2 (flat v1b)" 
+  unfolding CPT_def by(auto elim: CPrf.cases)
+  have "\<forall>v2 \<in> PT r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
+    proof
+      fix v2
+      assume "v2 \<in> PT r1 (flat v1a)"
+      with eqs(2,4) have "Seq v2 v1b \<in> PT (SEQ r1 r2) s"
+         by (simp add: CPT_def PT_def Prf.intros(1) Prf_CPrf)
+      with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
+         using eqs by (simp add: PT_def) 
+      then show "\<not> v2 :\<sqsubset>val v1a"
+         using PosOrd_SeqI1 by blast
+    qed     
+  then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
+  moreover
+  have "\<forall>v2 \<in> PT r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
+    proof 
+      fix v2
+      assume "v2 \<in> PT r2 (flat v1b)"
+      with eqs(2,3,4) have "Seq v1a v2 \<in> PT (SEQ r1 r2) s"
+         by (simp add: CPT_def PT_def Prf.intros Prf_CPrf)
+      with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
+         using eqs by (simp add: PT_def) 
+      then show "\<not> v2 :\<sqsubset>val v1b"
+         using PosOrd_SeqI2 by auto
+    qed     
+  then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp    
+  moreover
+  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
+  proof
+     assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
+     then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
+     then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
+        using L_flat_Prf2 by blast
+     then have "Seq vA vB \<in> PT (SEQ r1 r2) s" unfolding eqs using q1
+       by (auto simp add: PT_def intro: Prf.intros)
+     with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
+     then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
+     then show "False"
+       using PosOrd_shorterI by blast  
+  qed
+  ultimately
+  show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
+    by (rule Posix.intros)
+next
+   case (STAR r s v1)
+   have IH: "\<And>s v1. \<lbrakk>v1 \<in> CPT r s; \<forall>v2\<in>PT r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
+   have as1: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
+   have as2: "v1 \<in> CPT (STAR r) s" by fact
+   then obtain 
+    vs where eqs:
+        "v1 = Stars vs" "s = flat (Stars vs)"
+        "\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
+        unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
+   have "Stars vs \<in> CPT (STAR r) (flat (Stars vs))" 
+     using as2 unfolding eqs .
+   moreover
+   have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v" 
+     proof 
+        fix v
+        assume a: "v \<in> set vs"
+        then obtain pre post where e: "vs = pre @ [v] @ post"
+          by (metis append_Cons append_Nil in_set_conv_decomp_first)
+        then have q: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" 
+          using as1 unfolding eqs by simp
+        have "\<forall>v2\<in>PT r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs 
+          proof (rule ballI, rule notI) 
+             fix v2
+             assume w: "v2 :\<sqsubset>val v"
+             assume "v2 \<in> PT r (flat v)"
+             then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" 
+                 using as2 unfolding e eqs
+                 apply(auto simp add: CPT_def PT_def intro!: Prf_Stars)[1]
+                 using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
+                 by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
+             then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
+                using q by simp     
+             with w show "False"
+                using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
+                PosOrd_StarsI PosOrd_Stars_appendI by auto
+          qed     
+        with IH
+        show "flat v \<in> r \<rightarrow> v" using a as2 unfolding eqs
+          using eqs(3) by blast
+     qed
+   moreover
+   have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
+     proof 
+       assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
+       then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
+                             "Stars vs2 :\<sqsubset>val Stars vs" 
+         unfolding PT_def
+         apply(auto elim: Prf.cases)
+         apply(erule Prf.cases)
+         apply(auto intro: Prf.intros)
+         apply(drule_tac x="[]" in meta_spec) 
+         apply(simp)
+         apply(drule meta_mp)
+         apply(auto intro: Prf.intros)
+         apply(drule_tac x="(v#vsa)" in meta_spec)
+         apply(auto intro: Prf.intros)
+         done
+       then show "False" using as1 unfolding eqs
+         apply -
+         apply(drule_tac x="Stars vs2" in bspec)
+         apply(auto simp add: PT_def)
+         done
+     qed
+   ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
+     by (rule PosOrd_Posix_Stars)
+   then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
+qed
 
 unused_thms