author Manuel Eberl Mon, 04 Jan 2021 19:41:38 +0100 changeset 73047 ab9e27da0e85 parent 73046 32edc2b4e243 child 73048 7ad9f197ca7e
HOL-Library: Changed notation for sum_mset
 NEWS file | annotate | diff | comparison | revisions src/HOL/Computational_Algebra/Primes.thy file | annotate | diff | comparison | revisions src/HOL/Data_Structures/Sorting.thy file | annotate | diff | comparison | revisions src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions
```--- 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))"

"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

```