--- a/src/HOL/Library/Multiset.thy Thu Feb 18 17:52:53 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Feb 18 17:53:09 2016 +0100
@@ -1164,6 +1164,15 @@
"replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
by (induct xs) auto
+lemma replicate_mset_eq_empty_iff [simp]:
+ "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
+ by (induct n) simp_all
+
+lemma replicate_mset_eq_iff:
+ "replicate_mset m a = replicate_mset n b \<longleftrightarrow>
+ m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
+ by (auto simp add: multiset_eq_iff)
+
subsection \<open>Big operators\<close>
@@ -1237,6 +1246,12 @@
(simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
qed
+syntax (ASCII)
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
+syntax
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+translations
+ "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#_" [900] 900)
where "\<Union># MM \<equiv> msetsum MM"
@@ -1247,12 +1262,14 @@
lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
by (induct MM) auto
-syntax (ASCII)
- "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
-syntax
- "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
-translations
- "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
+lemma count_setsum:
+ "count (setsum f A) x = setsum (\<lambda>a. count (f a) x) A"
+ by (induct A rule: infinite_finite_induct) simp_all
+
+lemma setsum_eq_empty_iff:
+ assumes "finite A"
+ shows "setsum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
+ using assms by induct simp_all
context comm_monoid_mult
begin
@@ -1302,6 +1319,10 @@
then show ?thesis by simp
qed
+lemma (in semidom) msetprod_zero_iff:
+ "msetprod A = 0 \<longleftrightarrow> (\<exists>a\<in>set_mset A. a = 0)"
+ by (induct A) auto
+
subsection \<open>Alternative representations\<close>
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Thu Feb 18 17:52:53 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Thu Feb 18 17:53:09 2016 +0100
@@ -8,27 +8,6 @@
imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
begin
-context algebraic_semidom
-begin
-
-lemma is_unit_mult_iff:
- "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
- by (auto dest: dvd_mult_left dvd_mult_right)
-
-lemma is_unit_power_iff:
- "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
- by (induct n) (auto simp add: is_unit_mult_iff)
-
-lemma subset_divisors_dvd:
- "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
- by (auto simp add: subset_iff intro: dvd_trans)
-
-lemma strict_subset_divisors_dvd:
- "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
- by (auto simp add: subset_iff intro: dvd_trans)
-
-end
-
class factorial_semiring = normalization_semidom +
assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
fixes is_prime :: "'a \<Rightarrow> bool"
--- a/src/HOL/Power.thy Thu Feb 18 17:52:53 2016 +0100
+++ b/src/HOL/Power.thy Thu Feb 18 17:53:09 2016 +0100
@@ -331,6 +331,10 @@
shows "(a div b) ^ n = a ^ n div b ^ n"
using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
+lemma is_unit_power_iff:
+ "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
+ by (induct n) (auto simp add: is_unit_mult_iff)
+
end
context normalization_semidom
--- a/src/HOL/Rings.thy Thu Feb 18 17:52:53 2016 +0100
+++ b/src/HOL/Rings.thy Thu Feb 18 17:53:09 2016 +0100
@@ -10,7 +10,7 @@
section \<open>Rings\<close>
theory Rings
-imports Groups
+imports Groups Set
begin
class semiring = ab_semigroup_add + semigroup_mult +
@@ -155,6 +155,14 @@
then show ?thesis ..
qed
+lemma subset_divisors_dvd:
+ "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
+ by (auto simp add: subset_iff intro: dvd_trans)
+
+lemma strict_subset_divisors_dvd:
+ "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
+ by (auto simp add: subset_iff intro: dvd_trans)
+
lemma one_dvd [simp]:
"1 dvd a"
by (auto intro!: dvdI)
@@ -847,6 +855,10 @@
"is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
+lemma is_unit_mult_iff:
+ "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
+ by (auto dest: dvd_mult_left dvd_mult_right)
+
lemma unit_div [intro]:
"is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)