--- a/thys/Positions.thy	Tue Jun 27 04:40:43 2017 +0100
+++ b/thys/Positions.thy	Tue Jun 27 08:59:11 2017 +0100
@@ -23,6 +23,19 @@
 | "Pos (Stars []) = {[]}"
 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 
+lemma Pos_stars:
+  "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
+apply(induct vs)
+apply(simp) 
+apply(simp)
+apply(simp add: insert_ident)
+apply(rule subset_antisym)
+apply(auto)
+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)
@@ -105,20 +118,20 @@
 apply(induct v1 arbitrary: r v2 rule: Pos.induct)
 (* ZERO *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 (* ONE *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 (* CHAR *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 (* ALT Left *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(clarify)
 apply(simp add: insert_ident)
 apply(drule_tac x="r1a" in meta_spec)
@@ -132,9 +145,9 @@
 apply(simp add: insert_ident)
 using Pos_empty apply blast
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(clarify)
 apply(simp add: insert_ident)
 using Pos_empty apply blast
@@ -146,10 +159,10 @@
 apply(rule subset_antisym)
 apply(auto)[3]
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 (* SEQ *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(simp add: insert_ident)
 apply(clarify)
 apply(drule_tac x="r1a" in meta_spec)
@@ -179,19 +192,22 @@
 apply(simp)
 (* STAR empty *)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all)[7]
 apply(auto)[1]
 using Pos_empty apply fastforce
 (* STAR non-empty *)
+apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)
+apply(simp_all del: Pos.simps)
 apply(erule Prf.cases)
-apply(simp_all)
+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)
@@ -431,75 +447,40 @@
 apply(simp add: pflat_len_simps)
 done
 
-
-lemma val_ord_STARI:
-  assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
-  shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" 
+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(erule conjE)
+apply(clarify)
+apply(subst val_ord_ex_def)
 apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(subst pflat_len_Stars_simps)
-apply(simp)
-apply(subst pflat_len_Stars_simps)
-apply(simp)
-apply(simp)
-apply(rule ballI)
-apply(rule impI)
-apply(simp)
-apply(auto)
-apply(drule_tac x="[]" in bspec)
-apply(simp add: Pos_empty)
+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_STARI2:
-  assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
-  shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" 
+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(erule conjE)+
+apply(clarify)
+apply(subst val_ord_ex_def)
 apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(case_tac vs1)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(case_tac vs2)
-apply(simp)
-apply (simp add: pflat_len_def)
-apply(simp)
-apply(auto)[1]
-apply (simp add: pflat_len_Stars_simps)
-using pflat_len_def apply auto[1]
-apply(rule ballI)
-apply(rule impI)
-apply(simp)
+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(auto)
-apply (simp add: pflat_len_simps(9))
-apply (simp add: pflat_len_Stars_simps)
-using assms(2)
-apply(auto simp add: pflat_len_def)[1]
-apply force
-apply force
-apply(auto simp add: pflat_len_def)[1]
-apply force
-apply force
-apply(auto simp add: pflat_len_def)[1]
-apply(auto simp add: pflat_len_def)[1]
-apply force
-apply force
-apply(auto simp add: pflat_len_def)[1]
-apply force
-apply force
+apply(simp add: pflat_len_simps intlen_append)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 done
 
 lemma val_ord_SeqI1:
@@ -1095,25 +1076,19 @@
 apply (simp add: Posix1(2))
 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 (subst val_ord_ex_def)
-apply(case_tac p)
+apply(rule val_ord_StarsI2)
 apply(simp)
-apply (metis Posix1(2) append_eq_conv_conj flat_Stars not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_def)
-
-
-
-using Posix1(2) val_ord_STARI2 apply fastforce
+using Posix1(2) apply force
 apply(simp add: val_ord_ex1_def)
-apply (subst (asm) val_ord_ex_def)
-apply(erule exE)
 apply (subst val_ord_ex1_def)
 apply(rule disjI1)
-apply (subst val_ord_ex_def)
-by (metis Posix1(2) flat.simps(7) flat_Stars val_ord_STARI)
+apply(rule val_ord_StarsI)
+apply(simp)
+apply(simp add: Posix1)
+using Posix1(2) by force
+
 
 lemma Posix_val_ord_stronger:
   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
@@ -1193,16 +1168,7 @@
 apply(induct vs)
 apply(simp)
 apply(simp)
-apply(simp add: val_ord_ex_def)
-apply(erule exE)
-apply(case_tac p)
-apply(simp)
-apply(rule_tac x="[]" in exI)
-apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps intlen_append)[1]
-apply(simp)
-apply(rule_tac x="Suc aa#list" in exI)
-apply(rule val_ord_STARI2)
+apply(rule val_ord_StarsI2)
 apply(simp)
 apply(simp)
 done
@@ -1287,7 +1253,7 @@
 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_ex_def)
 apply(auto simp add: CPT_def PT_def)[1]
 using CPrf_stars apply auto[1]
 apply(auto)[1]
@@ -1327,7 +1293,7 @@
 apply(simp)
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_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> []"
@@ -1341,7 +1307,7 @@
   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_STARI val_ord_ex_def val_ord_shorterI)
+    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:
@@ -1508,9 +1474,7 @@
 apply(simp)
 apply(drule mp)
 using Prf.intros(7) Prf_CPrf apply blast
-apply(subst (asm) (2) val_ord_ex_def)
-apply(simp)
-using val_ord_STARI val_ord_ex_def apply fastforce
+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)
@@ -1541,11 +1505,7 @@
 apply(simp)
 prefer 2
 apply(simp)
-apply(simp add: val_ord_ex_def)
-apply(erule exE)
-apply(rotate_tac 6)
-apply(drule_tac x="0#p" in spec)
-apply (simp add: val_ord_STARI)
+apply (simp add: val_ord_StarsI)
 apply(auto simp add: PT_def)
 done