# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1475691176 -7200
# Node ID 6e7bf76785185d123187d7b928f6852963a0c9a3
# Parent  5c2c559f01ebb78ccace859fb07551a925421743
more multiset simp rules

diff -r 5c2c559f01eb -r 6e7bf7678518 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Oct 05 14:28:22 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Oct 05 20:12:56 2016 +0200
@@ -545,6 +545,8 @@
 interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_subset_eq_exists_conv)
 
+declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp]
+
 lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    by (fact subset_mset.add_le_cancel_right)
 
@@ -2649,7 +2651,7 @@
       using K N trans True by (meson that transE)
     ultimately show ?thesis
       by (rule_tac x = I in exI, rule_tac x = J in exI, rule_tac x = "(K - {#a#}) + K'" in exI)
-        (use z y N in \<open>auto simp: subset_mset.add_diff_assoc dest: in_diffD\<close>)
+        (use z y N in \<open>auto simp del: subset_mset.add_diff_assoc2 dest: in_diffD\<close>)
   next
     case False
     then have "a \<in># I" by (metis N(2) union_iff union_single_eq_member z)
@@ -2658,7 +2660,7 @@
     ultimately show ?thesis
       by (rule_tac x = "I - {#a#}" in exI, rule_tac x = "add_mset a J" in exI,
           rule_tac x = "K + K'" in exI)
-        (use z y N False K in \<open>auto simp: subset_mset.diff_add_assoc2\<close>)
+        (use z y N False K in \<open>auto simp: add.assoc\<close>)
   qed
 qed