--- 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)