# HG changeset patch # User Christian Urban # Date 1498550351 -3600 # Node ID ca4e9eb8d57643c32cb94e28095b87de47236e08 # Parent 022b80503766df9c1899636bab5a180f3f151039 polished diff -r 022b80503766 -r ca4e9eb8d576 thys/Positions.thy --- 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)) = {[]} \ {0#ps | ps. ps \ Pos v} \ {Suc n#ps | n ps. n#ps \ Pos (Stars vs)}" +lemma Pos_stars: + "Pos (Stars vs) = {[]} \ (\n < length vs. {n#ps | ps. ps \ 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 "[] \ 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 \val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" - shows "(Stars (v1#vs1)) \val (0#p) (Stars (v2#vs2))" +lemma val_ord_StarsI: + assumes "v1 :\val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" + shows "(Stars (v1#vs1)) :\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) \val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" - shows "(Stars (v#vs1)) \val (Suc n#p) (Stars (v#vs2))" +lemma val_ord_StarsI2: + assumes "(Stars vs1) :\val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" + shows "(Stars (v#vs1)) :\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 \ r \ v1" "v2 \ 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 \ []" @@ -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