--- a/NEWS Wed Jul 20 22:36:10 2016 +0200
+++ b/NEWS Thu Jul 21 10:52:27 2016 +0200
@@ -410,10 +410,19 @@
less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
INCOMPATIBILITY.
+* The lemma mset_map has now the attribute [simp].
+INCOMPATIBILITY.
+
+* Some theorems about multisets have been removed:
+ le_multiset_plus_plus_left_iff ~> add_less_cancel_right
+ le_multiset_plus_plus_right_iff ~> add_less_cancel_left
+ add_eq_self_empty_iff ~> add_cancel_left_right
+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,
-and linordered_cancel_ab_semigroup_add.
+linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.
INCOMPATIBILITY.
* There are some new simplification rules about multisets and the multiset
--- a/src/HOL/Algebra/Divisibility.thy Wed Jul 20 22:36:10 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Thu Jul 21 10:52:27 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"
--- a/src/HOL/Library/Multiset.thy Wed Jul 20 22:36:10 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jul 21 10:52:27 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" "{#}"
--- a/src/HOL/Library/Multiset_Order.thy Wed Jul 20 22:36:10 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Thu Jul 21 10:52:27 2016 +0200
@@ -187,9 +187,6 @@
shows "{#} \<le> M"
by (simp add: subset_eq_imp_le_multiset)
-lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
- by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
-
lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
unfolding less_multiset\<^sub>H\<^sub>O
by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
@@ -207,7 +204,7 @@
lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
-instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
+instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
begin
lemma less_eq_multiset\<^sub>H\<^sub>O:
@@ -219,24 +216,16 @@
lemma
fixes M N :: "'a multiset"
shows
- less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
- less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
- using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
-
-lemma
- fixes M N :: "'a multiset"
- shows
- le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
- le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
+ less_eq_multiset_plus_left: "N \<le> (M + N)" and
+ less_eq_multiset_plus_right: "M \<le> (M + N)"
by simp_all
lemma
fixes M N :: "'a multiset"
shows
- le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
- le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
- using [[metis_verbose = false]]
- by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
+ le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
+ le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
+ by simp_all
end