diff -r 925232418a15 -r 022b80503766 thys/Positions.thy
--- a/thys/Positions.thy	Tue Jun 27 01:02:17 2017 +0100
+++ b/thys/Positions.thy	Tue Jun 27 04:40:43 2017 +0100
@@ -91,6 +91,11 @@
 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" 
@@ -98,14 +103,18 @@
   shows "v1 = v2"
 using assms
 apply(induct v1 arbitrary: r v2 rule: Pos.induct)
+(* ZERO *)
+apply(erule Prf.cases)
+apply(simp_all)
+(* ONE *)
+apply(erule Prf.cases)
+apply(simp_all)
+(* CHAR *)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(erule Prf.cases)
 apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
+(* ALT Left *)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(erule Prf.cases)
@@ -116,9 +125,9 @@
 apply(drule_tac x="v1a" in meta_spec)
 apply(simp)
 apply(drule_tac meta_mp)
-thm subset_antisym
 apply(rule subset_antisym)
 apply(auto)[3]
+(* ALT Right *)
 apply(clarify)
 apply(simp add: insert_ident)
 using Pos_empty apply blast
@@ -138,6 +147,7 @@
 apply(auto)[3]
 apply(erule Prf.cases)
 apply(simp_all)
+(* SEQ *)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(simp add: insert_ident)
@@ -148,49 +158,33 @@
 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(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp)
+apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
 apply(rule subsetI)
-apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp (no_asm_use))
+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(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp)
+apply (metis (mono_tags, hide_lams) Un_iff image_iff n_not_Suc_n nth_Cons_0)
 apply(rule subsetI)
-apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
-prefer 2
-apply (metis (no_types, lifting) Un_iff)
-apply(simp (no_asm_use))
+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)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(auto)[1]
 using Pos_empty apply fastforce
+(* STAR non-empty *)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(erule Prf.cases)
@@ -205,23 +199,14 @@
 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(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "0 # x \<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 (smt Un_iff image_iff list.inject mem_Collect_eq nat.discI)
 apply(rule subsetI)
-apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<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))
+using list.inject apply blast
+apply(simp)
 apply(simp)
 apply(drule_tac meta_mp)
 apply(rule subset_antisym)
@@ -281,17 +266,22 @@
 apply(simp)
 done
 
+
+
+section {* Orderings *}
+
+
 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")
 where
-  "ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)"
+  "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
 
 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
 where
-  "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"
+  "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
 
 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
 where
-  "[] \<sqsubset>lex p#ps"
+  "[] \<sqsubset>lex (p#ps)"
 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
 
@@ -397,24 +387,50 @@
 apply(auto simp add: val_ord_def pflat_len_simps)
 done
 
-
-lemma val_ord_ALTE:
-  assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
-  shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
-using assms(1)
+lemma val_ord_LeftE:
+  assumes "(Left v1) :\<sqsubset>val (Left v2)"
+  shows "v1 :\<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)
-apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+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(rule_tac x="ps" in exI)
+apply(auto)
+apply(drule_tac x="0#q" in bspec)
+apply(simp)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="0#q" in bspec)
+apply(simp)
+apply(simp add: pflat_len_simps)
+done
 
-lemma val_ord_ALTE2:
-  assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
-  shows "p = 1 \<and> v1 \<sqsubset>val ps v2"
-using assms(1)
+lemma val_ord_RightE:
+  assumes "(Right v1) :\<sqsubset>val (Right v2)"
+  shows "v1 :\<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)
-apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+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(rule_tac x="ps" in exI)
+apply(auto)
+apply(drule_tac x="Suc 0#q" in bspec)
+apply(simp)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="Suc 0#q" in bspec)
+apply(simp)
+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))"
@@ -435,9 +451,11 @@
 apply(rule impI)
 apply(simp)
 apply(auto)
+apply(drule_tac x="[]" in bspec)
+apply(simp add: Pos_empty)
 using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_Stars_simps)
+apply(simp add: pflat_len_simps intlen_append)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
 done
 
 lemma val_ord_STARI2:
@@ -484,13 +502,15 @@
 apply force
 done
 
-
-lemma val_ord_SEQI:
-  assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
-  shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')" 
+lemma val_ord_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(erule conjE)
+apply(clarify)
+apply(subst val_ord_ex_def)
+apply(rule_tac x="0#p" in exI)
 apply(subst val_ord_def)
 apply(rule conjI)
 apply(simp)
@@ -506,13 +526,15 @@
 apply(auto simp add: pflat_len_simps)[2]
 done
 
-
-lemma val_ord_SEQI2:
-  assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'"
-  shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')" 
+lemma val_ord_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(erule conjE)+
+apply(clarify)
+apply(subst val_ord_ex_def)
+apply(rule_tac x="Suc 0#p" in exI)
 apply(subst val_ord_def)
 apply(rule conjI)
 apply(simp)
@@ -521,11 +543,14 @@
 apply(rule ballI)
 apply(rule impI)
 apply(simp only: Pos.simps)
-apply(auto)
-apply(auto simp add: pflat_len_def intlen_append)
-apply(auto simp add: assms(2))
+apply(auto)[1]
+apply(simp add: pflat_len_simps)
+using assms(2)
+apply(simp)
+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'"
@@ -581,7 +606,7 @@
   and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 
   shows "v1 = v1'"
 proof -
-  have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q"
+  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)
@@ -599,8 +624,8 @@
   done
   then show "v1 = v1'" 
   apply(rule_tac Three_to_One)
-  apply(rule assms)
-  apply(rule assms)
+  apply(rule assms(2))
+  apply(rule assms(3))
   apply(simp)
   done
 qed
@@ -930,13 +955,9 @@
 using append_eq_conv_conj apply blast
 apply(subst (asm) (2)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(rule_tac x="0#p" in exI)
-apply(rule val_ord_SEQI)
+apply(rule val_ord_SeqI1)
 apply(simp)
 apply(simp)
 apply (metis Posix1(2) append_assoc append_take_drop_id)
@@ -947,13 +968,9 @@
 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(rule_tac x="1#p" in exI)
-apply(rule val_ord_SEQI2)
+apply(rule val_ord_SeqI2)
 apply(simp)
 apply (simp add: Posix1(2))
 apply(subst val_ord_ex1_def)
@@ -1441,7 +1458,7 @@
 apply(simp)
 apply(drule mp)
 apply (simp add: Prf.intros(1) Prf_CPrf)
-using val_ord_SEQI val_ord_ex_def apply fastforce
+using val_ord_SeqI1 apply fastforce
 apply(assumption)
 apply(rotate_tac 1)
 apply(drule_tac x="flat v2" in meta_spec)
@@ -1455,7 +1472,7 @@
 apply(simp)
 apply(drule mp)
 apply (simp add: Prf.intros(1) Prf_CPrf)
-apply (meson val_ord_SEQI2 val_ord_ex_def)
+apply (meson val_ord_SeqI2)
 apply(assumption)
 (* SEQ side condition *)
 apply(auto simp add: PT_def)
@@ -1471,7 +1488,7 @@
 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_SEQI val_ord_ex_def val_ord_shorterI)
+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)