--- a/thys/Positions.thy	Tue Jun 27 08:59:11 2017 +0100
+++ b/thys/Positions.thy	Tue Jun 27 13:15:55 2017 +0100
@@ -3,6 +3,9 @@
   imports "Lexer" 
 begin
 
+
+section {* Position in values *}
+
 fun 
   at :: "val \<Rightarrow> nat list \<Rightarrow> val"
 where
@@ -34,8 +37,6 @@
 apply(auto)[1]
 using less_Suc_eq_0_disj by auto
 
-
-
 lemma Pos_empty:
   shows "[] \<in> Pos v"
 by (induct v rule: Pos.induct)(auto)
@@ -89,199 +90,10 @@
 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
 
-lemma Two_to_Three_aux:
-  assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"
-  shows "p \<in> Pos v1 \<inter> Pos v2"
-using assms
-apply(simp add: pflat_len_def)
-apply(auto split: if_splits)
-apply (smt inlen_bigger)+
-done
-
-lemma Two_to_Three_orig:
-  assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"
-  shows "Pos v1 = Pos v2"
-using assms
-by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym)
-
-lemma inj_image_eq_if:
-  assumes "f ` A = f ` B" "inj f"
-  shows "A = B"
-using assms
-by (simp add: inj_image_eq_iff)
-
-lemma Three_to_One:
-  assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" 
-  and "Pos v1 = Pos v2" 
-  shows "v1 = v2"
-using assms
-apply(induct v1 arbitrary: r v2 rule: Pos.induct)
-(* ZERO *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* ONE *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* CHAR *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* ALT Left *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(simp add: insert_ident)
-apply(drule_tac x="r1a" in meta_spec)
-apply(drule_tac x="v1a" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule subset_antisym)
-apply(auto)[3]
-(* ALT Right *)
-apply(clarify)
-apply(simp add: insert_ident)
-using Pos_empty apply blast
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(simp add: insert_ident)
-using Pos_empty apply blast
-apply(simp add: insert_ident)
-apply(drule_tac x="r2a" in meta_spec)
-apply(drule_tac x="v2b" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule subset_antisym)
-apply(auto)[3]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* SEQ *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp add: insert_ident)
-apply(clarify)
-apply(drule_tac x="r1a" in meta_spec)
-apply(drule_tac x="r2a" in meta_spec)
-apply(drule_tac x="v1b" in meta_spec)
-apply(drule_tac x="v2c" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule_tac f="op # 0" in inj_image_eq_if)
-apply(simp add: Setcompr_eq_image)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
-apply(rule subsetI)
-apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
-apply(simp)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule_tac f="op # (Suc 0)" in inj_image_eq_if)
-apply(simp add: Setcompr_eq_image)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
-apply(rule subsetI)
-apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
-apply(simp)
-apply(simp)
-(* STAR empty *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-using Pos_empty apply fastforce
-(* STAR non-empty *)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all del: Pos.simps)
-apply(erule Prf.cases)
-apply(simp_all del: Pos.simps)
-apply(simp)
-apply(auto)[1]
-using Pos_empty apply fastforce
-apply(clarify)
-apply(simp)
-apply(simp add: insert_ident)
-apply(drule_tac x="rb" in meta_spec)
-apply(drule_tac x="STAR rb" in meta_spec)
-apply(drule_tac x="vb" in meta_spec)
-apply(drule_tac x="Stars vsb" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule_tac f="op # 0" in inj_image_eq_if)
-apply(simp add: Setcompr_eq_image)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply (smt Un_iff image_iff list.inject mem_Collect_eq nat.discI)
-apply(rule subsetI)
-using list.inject apply blast
-apply(simp)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply(case_tac vsa)
-apply(simp)
-apply (simp add: Pos_empty)
-apply(simp)
-apply(clarify)
-apply(erule disjE)
-apply (simp add: Pos_empty)
-apply(erule disjE)
-apply(clarify)
-apply(subgoal_tac 
-  "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
-prefer 2
-apply blast
-apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union>  {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp)
-apply(clarify)
-apply(subgoal_tac 
-  "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
-prefer 2
-apply blast
-apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp)
-apply(rule subsetI)
-apply(case_tac vsb)
-apply(simp)
-apply (simp add: Pos_empty)
-apply(simp)
-apply(clarify)
-apply(erule disjE)
-apply (simp add: Pos_empty)
-apply(erule disjE)
-apply(clarify)
-apply(subgoal_tac 
-  "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
-prefer 2
-apply(simp)
-apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")
-apply blast
-using list.inject apply blast
-apply(clarify)
-apply(subgoal_tac 
-  "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
-prefer 2
-apply(simp)
-apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp (no_asm_use))
-apply(simp)
-done
-
+lemma outside_lemma:
+  assumes "p \<notin> Pos v1 \<union> Pos v2"
+  shows "pflat_len v1 p = pflat_len v2 p"
+using assms by (auto simp add: pflat_len_def)
 
 
 section {* Orderings *}
@@ -346,16 +158,16 @@
 apply(auto)
 done
 
-lemma outside_lemma:
-  assumes "p \<notin> Pos v1 \<union> Pos v2"
-  shows "pflat_len v1 p = pflat_len v2 p"
-using assms
-apply(auto simp add: pflat_len_def)
-done
+
+
+
+section {* Ordering of values according to Okui & Suzuki *}
+
 
 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
 where
-  "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and>
+  "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))"
 
 
@@ -381,6 +193,7 @@
 apply(rule_tac val_ord_shorterI)
 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
+
 lemma val_ord_LeftI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Left v) :\<sqsubset>val (Left v')" 
@@ -447,41 +260,6 @@
 apply(simp add: pflat_len_simps)
 done
 
-lemma val_ord_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(clarify)
-apply(subst val_ord_ex_def)
-apply(subst val_ord_def)
-apply(rule_tac x="0#p" in exI)
-apply(simp add: pflat_len_Stars_simps pflat_len_simps)
-using assms(2)
-apply(simp add: pflat_len_simps intlen_append)
-apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
-done
-
-lemma val_ord_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(clarify)
-apply(subst val_ord_ex_def)
-apply(subst val_ord_def)
-apply(case_tac p)
-apply(simp add: pflat_len_simps)
-apply(rule_tac x="[]" in exI)
-apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
-apply(rule_tac x="Suc a#list" in exI)
-apply(simp add: pflat_len_Stars_simps pflat_len_simps)
-using assms(2)
-apply(simp add: pflat_len_simps intlen_append)
-apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
-done
 
 lemma val_ord_SeqI1:
   assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
@@ -531,126 +309,143 @@
 apply(auto simp add: pflat_len_simps)
 done
 
-
-lemma val_ord_SEQE_0:
-  assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" 
-  shows "v1 \<sqsubset>val p v1'"
-using assms(1)
-apply(simp add: val_ord_def val_ord_ex_def)
-apply(auto)[1]
-apply(simp add: pflat_len_simps)
-apply(simp add: val_ord_def pflat_len_def)
-apply(auto)[1]
+lemma val_ord_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(erule exE)
+apply(case_tac p)
+apply(simp add: val_ord_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(auto simp add: pflat_len_simps intlen_append)[1]
+apply(rule_tac x="list" in exI)
+apply(simp)
+apply(rule ballI)
+apply(rule impI)
 apply(drule_tac x="0#q" in bspec)
 apply(simp)
-apply(simp)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
+apply(simp add: pflat_len_simps)
+apply(case_tac nat)
+apply(rule disjI2)
+apply(simp add: val_ord_def)
+apply(auto simp add: pflat_len_simps intlen_append)
+apply(rule_tac x="list" in exI)
+apply(simp add: Pos_empty)
+apply(rule ballI)
+apply(rule impI)
+apply(drule_tac x="Suc 0#q" in bspec)
 apply(simp)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
-apply(simp)
-apply(simp add: val_ord_def pflat_len_def)
-apply(auto)[1]
+apply(simp add: pflat_len_simps)
+apply(simp add: val_ord_def)
 done
 
-lemma val_ord_SEQE_1:
-  assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 
-  shows "v2 \<sqsubset>val p v2'"
+lemma val_ord_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(simp add: val_ord_def pflat_len_def)
-apply(auto)[1]
-apply(drule_tac x="1#q" in bspec)
-apply(simp)
-apply(simp)
-apply(drule_tac x="1#q" in bspec)
-apply(simp)
-apply(simp)
-apply(drule_tac x="1#q" in bspec)
-apply(simp)
-apply(auto)[1]
-apply(drule_tac x="1#q" in bspec)
-apply(simp)
-apply(auto)
-apply(simp add: intlen_append)
-apply force
-apply(simp add: intlen_append)
-apply force
-apply(simp add: intlen_append)
-apply force
-apply(simp add: intlen_append)
-apply force
+apply(subst (asm) val_ord_ex_def)
+apply(subst (asm) val_ord_def)
+apply(clarify)
+apply(subst val_ord_ex_def)
+apply(subst val_ord_def)
+apply(rule_tac x="0#p" in exI)
+apply(simp add: pflat_len_Stars_simps pflat_len_simps)
+using assms(2)
+apply(simp add: pflat_len_simps intlen_append)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 done
 
-lemma val_ord_SEQE_2:
-  assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 
-  and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 
-  shows "v1 = v1'"
-proof -
-  have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0#q \<sqsubset>lex Suc 0#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q"
-  using assms(1) 
-  apply(simp add: val_ord_def)
-  apply(rule ballI)
-  apply(clarify)
-  apply(drule_tac x="0#q" in bspec)
-  apply(auto)[1]
-  apply(simp add: pflat_len_simps)
-  done
-  then have "Pos v1 = Pos v1'"
-  apply(rule_tac Two_to_Three_orig)
-  apply(rule ballI)
-  apply(drule_tac x="pa" in bspec)
-  apply(simp)
-  apply(simp)
-  done
-  then show "v1 = v1'" 
-  apply(rule_tac Three_to_One)
-  apply(rule assms(2))
-  apply(rule assms(3))
-  apply(simp)
-  done
-qed
-
-lemma val_ord_SEQ:
-  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
-  and "flat (Seq v1 v2) = flat (Seq v1' v2')"
-  and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 
-  shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))"
+lemma val_ord_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(erule exE)
-apply(simp only: val_ord_def)
+apply(subst (asm) val_ord_def)
+apply(clarify)
+apply(subst val_ord_ex_def)
+apply(subst val_ord_def)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(rule_tac x="[]" in exI)
+apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
+apply(rule_tac x="Suc a#list" in exI)
+apply(simp add: pflat_len_Stars_simps pflat_len_simps)
+using assms(2)
+apply(simp add: pflat_len_simps intlen_append)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
+done
+
+lemma val_ord_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(erule conjE)+
-apply(erule disjE)
-prefer 2
-apply(erule disjE)
-apply(erule exE)
-apply(rule disjI1)
-apply(simp)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="ps" in exI)
-apply(rule val_ord_SEQE_0)
-apply(simp add: val_ord_def)
+apply(simp add: val_ord_StarsI2)
+done
+
+lemma val_ord_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(erule exE)
-apply(rule disjI2)
-apply(rule conjI)
-thm val_ord_SEQE_1
-apply(rule_tac val_ord_SEQE_2)
-apply(auto simp add: val_ord_def)[3]
-apply(rule assms(3))
-apply(rule assms(4))
+apply(case_tac p)
+apply(simp)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(subst val_ord_ex_def)
-apply(rule_tac x="ps" in exI)
-apply(rule_tac val_ord_SEQE_1)
-apply(auto simp add: val_ord_def)[1]
+apply(rule_tac x="[]" in exI)
+apply(simp add: val_ord_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(clarify)
+apply(simp add: val_ord_ex_def)
+apply(rule_tac x="nat#list" in exI)
+apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
+apply(case_tac q)
+apply(simp add: val_ord_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(case_tac q)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
+apply(clarify)
+apply(drule_tac x="Suc a # lista" in bspec)
 apply(simp)
-using assms(2)
-apply(simp add: pflat_len_simps)
+apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
+done
+
+lemma val_ord_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)
+done
+
+lemma val_ord_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(auto)
 done
 
 
-lemma val_ord_ex_trans:
+lemma val_ord_trans:
   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
   shows "v1 :\<sqsubset>val v3"
 using assms
@@ -679,7 +474,10 @@
 apply (metis (no_types, hide_lams) lex_trans outside_lemma)
 apply(simp add: val_ord_def)
 apply(auto)[1]
-by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
+by (smt inlen_bigger lex_trans outside_lemma pflat_len_def)
+
+
+section {* CPT and CPTpre *}
 
 
 inductive 
@@ -697,10 +495,38 @@
   assumes "\<Turnstile> v : r"
   shows "\<turnstile> v : r"
 using assms
-apply(induct)
-apply(auto intro: Prf.intros)
+by (induct) (auto intro: Prf.intros)
+
+lemma CPrf_stars:
+  assumes "\<Turnstile> Stars vs : STAR r"
+  shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
+using assms
+apply(induct vs)
+apply(auto)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
 done
 
+lemma CPrf_Stars_appendE:
+  assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
+  shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
+using assms
+apply(induct vs1 arbitrary: vs2)
+apply(auto intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(auto intro: CPrf.intros)
+done
+
+definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
+
 definition
   "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
 
@@ -709,9 +535,7 @@
 
 lemma CPT_CPTpre_subset:
   shows "CPT r s \<subseteq> CPTpre r s"
-apply(auto simp add: CPT_def CPTpre_def)
-done
-
+by(auto simp add: CPT_def CPTpre_def)
 
 lemma CPTpre_subsets:
   "CPTpre ZERO s = {}"
@@ -1096,41 +920,7 @@
 using assms
 apply(rule_tac Posix_val_ord)
 apply(assumption)
-apply(simp add: CPTpre_def CPT_def)
-done
-
-
-lemma STAR_val_ord:
-  assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2"
-  shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)"
-using assms(1,2)
-apply -
-apply(simp(no_asm)  add: val_ord_def)
-apply(rule conjI)
-apply(simp add: val_ord_def)
-apply(rule conjI)
-apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps)[1]
-apply(rule ballI)
-apply(rule impI)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
-apply(clarify)
-apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
-apply(clarify)
-apply(erule disjE)
-prefer 2
-apply(drule_tac x="Suc a # list" in bspec)
-apply(simp)
-apply(drule mp)
-apply(simp)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
-apply(drule_tac x="Suc a # list" in bspec)
-apply(simp)
-apply(drule mp)
-apply(simp)
-apply(simp add: val_ord_def pflat_len_simps intlen_append)
-done
+using CPT_CPTpre_subset by auto
 
 
 lemma Posix_val_ord_reverse:
@@ -1138,89 +928,7 @@
   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_ex_trans)
-
-
-lemma STAR_val_ord_ex:
-  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(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(rule_tac x="[]" in exI)
-apply(simp add: val_ord_def pflat_len_simps Pos_empty)
-apply(simp)
-apply(case_tac a)
-apply(clarify)
-prefer 2
-using STAR_val_ord val_ord_ex_def apply blast
-apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
-done
-
-lemma STAR_val_ord_exI:
-  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)
-apply(rule val_ord_StarsI2)
-apply(simp)
-apply(simp)
-done
-
-lemma STAR_val_ord_ex_append:
-  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)
-apply(drule STAR_val_ord_ex)
-apply(simp)
-done
-
-lemma STAR_val_ord_ex_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 STAR_val_ord_ex_append)
-apply(rule STAR_val_ord_exI)
-apply(auto)
-done
-
-
-lemma CPrf_stars:
-  assumes "\<Turnstile> Stars vs : STAR r"
-  shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
-using assms
-apply(induct vs)
-apply(auto)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-done
-
-definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
-
-lemma exists:
-  assumes "s \<in> (L r)\<star>"
-  shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
-using assms
-apply(drule_tac Star_string)
-apply(auto)
-by (metis L_flat_Prf2 Prf_Stars Star_val)
+    val_ord_ex1_def val_ord_ex_def val_ord_trans)
 
 
 lemma val_ord_Posix_Stars:
@@ -1271,7 +979,7 @@
 apply(simp)
 prefer 2
 apply(simp)
-using exists apply blast
+using Star_values_exists apply blast
 prefer 2
 apply(drule meta_mp)
 apply(erule CPrf.cases)
@@ -1310,27 +1018,9 @@
     using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI)
 qed
 
-lemma Prf_Stars_append:
-  assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
-  shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
-using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto intro: Prf.intros)
-done
+
 
-lemma CPrf_Stars_appendE:
-  assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
-  shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
-using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(auto intro: CPrf.intros)
-done
+
 
 lemma val_ord_Posix:
   assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)"
@@ -1497,9 +1187,9 @@
 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) STAR_val_ord_ex_append_eq)
+apply(subst (asm) val_ord_Stars_append_eq)
 apply(simp)
-apply(subst (asm) STAR_val_ord_ex_append_eq)
+apply(subst (asm) val_ord_Stars_append_eq)
 apply(simp)
 prefer 2
 apply(simp)