--- a/NEWS Mon Jan 04 19:56:33 2021 +0100
+++ b/NEWS Mon Jan 04 19:41:38 2021 +0100
@@ -162,6 +162,9 @@
* Library theory "Signed_Division" provides operations for signed
division, instantiated for type int.
+* Theory "Multiset": removed misleading notation \<Union># for sum_mset;
+replaced with \<Sum>\<^sub>#.
+
* Self-contained library theory "Word" taken over from former session
"HOL-Word".
--- a/src/HOL/Computational_Algebra/Primes.thy Mon Jan 04 19:56:33 2021 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Mon Jan 04 19:41:38 2021 +0100
@@ -751,7 +751,7 @@
lemma prime_factorization_prod_mset:
assumes "0 \<notin># A"
- shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
+ shows "prime_factorization (prod_mset A) = \<Sum>\<^sub>#(image_mset prime_factorization A)"
using assms by (induct A) (auto simp add: prime_factorization_mult)
lemma prime_factors_prod:
--- a/src/HOL/Data_Structures/Sorting.thy Mon Jan 04 19:56:33 2021 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy Mon Jan 04 19:41:38 2021 +0100
@@ -272,7 +272,7 @@
subsubsection "Functional Correctness"
abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where
-"mset_mset xss \<equiv> \<Union># (image_mset mset (mset xss))"
+"mset_mset xss \<equiv> \<Sum>\<^sub># (image_mset mset (mset xss))"
lemma mset_merge_adj:
"mset_mset (merge_adj xss) = mset_mset xss"
--- a/src/HOL/Library/Multiset.thy Mon Jan 04 19:56:33 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Jan 04 19:41:38 2021 +0100
@@ -2293,6 +2293,8 @@
end
+notation sum_mset ("\<Sum>\<^sub>#")
+
syntax (ASCII)
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
@@ -2389,14 +2391,10 @@
shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
by (induction A) (auto simp: algebra_simps)
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#")
- where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
- could likewise refer to \<open>\<Squnion>#\<close>\<close>
-
-lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
+lemma set_mset_Union_mset[simp]: "set_mset (\<Sum>\<^sub># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
by (induct MM) auto
-lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
+lemma in_Union_mset_iff[iff]: "x \<in># \<Sum>\<^sub># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
by (induct MM) auto
lemma count_sum:
@@ -2408,10 +2406,10 @@
shows "sum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
using assms by induct simp_all
-lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
+lemma Union_mset_empty_conv[simp]: "\<Sum>\<^sub># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
by (induction M) auto
-lemma Union_image_single_mset[simp]: "\<Union># (image_mset (\<lambda>x. {#x#}) m) = m"
+lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
by(induction m) auto