tuned
authornipkow
Fri Sep 14 07:31:55 2018 +0200 (4 days ago)
changeset 689928f7d3241ed68
parent 68991 6c1beb52d766
child 68993 e66783811518
tuned
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Sep 13 16:30:07 2018 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Sep 14 07:31:55 2018 +0200
     1.3 @@ -1520,8 +1520,12 @@
     1.4  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
     1.5  by (cases "B = {#}") (auto dest: multi_member_split)
     1.6  
     1.7 +lemma union_filter_mset_complement[simp]:
     1.8 +  "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
     1.9 +by (subst multiset_eq_iff) auto
    1.10 +
    1.11  lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
    1.12 -  by (subst multiset_eq_iff) auto
    1.13 +by simp
    1.14  
    1.15  lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
    1.16  proof (induct A arbitrary: B)
    1.17 @@ -1887,9 +1891,6 @@
    1.18  apply simp
    1.19  done
    1.20  
    1.21 -lemma union_mset_compl[simp]: "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
    1.22 -by (induction M) simp_all
    1.23 -
    1.24  lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
    1.25  proof (induct ls arbitrary: i)
    1.26    case Nil
    1.27 @@ -2924,7 +2925,7 @@
    1.28    next
    1.29      case [simp]: False
    1.30      have K: "K = {#x \<in># K. (x, a) \<in> r#} + {#x \<in># K. (x, a) \<notin> r#}"
    1.31 -      by (rule multiset_partition)
    1.32 +      by simp
    1.33      have "(I + K, (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r"
    1.34        using IH[of J' "{# x \<in># K. (x, a) \<notin> r#}" "I + {# x \<in># K. (x, a) \<in> r#}"]
    1.35          J Suc.prems K size_J by (auto simp: ac_simps)