# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1609785698 -3600
# Node ID ab9e27da0e85c365eefdeb45a1e711ddb923affd
# Parent  32edc2b4e24385e0a9ec063af0b16be7d757b0fd
HOL-Library: Changed notation for sum_mset

diff -r 32edc2b4e243 -r ab9e27da0e85 NEWS
--- 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".
 
diff -r 32edc2b4e243 -r ab9e27da0e85 src/HOL/Computational_Algebra/Primes.thy
--- 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:
diff -r 32edc2b4e243 -r ab9e27da0e85 src/HOL/Data_Structures/Sorting.thy
--- 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"
diff -r 32edc2b4e243 -r ab9e27da0e85 src/HOL/Library/Multiset.thy
--- 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