# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1469015498 -7200
# Node ID 4ec7554857326339b963edc4d7ad9c8e24d087f9
# Parent  54e932f0c30a298a1c2257cc37a1b24b430b65ad
adding mset_map to the simp rules

diff -r 54e932f0c30a -r 4ec755485732 NEWS
--- a/NEWS	Tue Jul 19 16:50:39 2016 +0200
+++ b/NEWS	Wed Jul 20 13:51:38 2016 +0200
@@ -402,6 +402,9 @@
     less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
 INCOMPATIBILITY.
 
+* The lemma mset_map has now the attribute [simp].
+INCOMPATIBILITY.
+
 * Some typeclass constraints about multisets have been reduced from ordered or
 linordered to preorder. Multisets have the additional typeclasses order_bot,
 no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
diff -r 54e932f0c30a -r 4ec755485732 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Tue Jul 19 16:50:39 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jul 20 13:51:38 2016 +0200
@@ -1839,8 +1839,7 @@
 lemma (in monoid) fmset_perm_cong:
   assumes prm: "as <~~> bs"
   shows "fmset G as = fmset G bs"
-using perm_map[OF prm]
-by (simp add: mset_eq_perm fmset_def)
+using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
 
 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
   assumes "as [\<sim>] bs"
@@ -1905,7 +1904,7 @@
   shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> 
                  cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
 apply (rule perm.induct[of cas cbs], rule prm)
-apply safe apply simp_all
+apply safe apply (simp_all del: mset_map)
   apply (simp add: map_eq_Cons_conv, blast)
  apply force
 proof -
@@ -1924,7 +1923,7 @@
 
   from p1
       have "mset (map (assocs G) as) = mset ys"
-      by (simp add: mset_eq_perm)
+      by (simp add: mset_eq_perm del: mset_map)
   hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD)
 
   have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
@@ -1980,7 +1979,7 @@
 proof -
   from mset
       have mpp: "map (assocs G) as <~~> map (assocs G) bs"
-      by (simp add: fmset_def mset_eq_perm)
+      by (simp add: fmset_def mset_eq_perm del: mset_map)
 
   have "\<exists>cas. cas = map (assocs G) as" by simp
   from this obtain cas where cas: "cas = map (assocs G) as" by simp
@@ -2038,7 +2037,7 @@
   using elems
   unfolding Cs
     apply (induct Cs', simp)
-  proof clarsimp
+  proof (clarsimp simp del: mset_map)
     fix a Cs' cs 
     assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
       and csP: "\<forall>x\<in>set cs. P x"
diff -r 54e932f0c30a -r 4ec755485732 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jul 19 16:50:39 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jul 20 13:51:38 2016 +0200
@@ -1612,7 +1612,7 @@
 lemma mset_insort [simp]: "mset (insort x xs) = mset xs + {#x#}"
   by (induct xs) (simp_all add: ac_simps)
 
-lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
+lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
 global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"