merged
authorwenzelm
Thu, 21 Jul 2016 10:52:27 +0200
changeset 63533 42b6186fc0e4
parent 63525 f01d1e393f3f (diff)
parent 63532 b01154b74314 (current diff)
child 63536 8cecf0100996
child 63539 70d4d9e5707b
merged
NEWS
--- 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