# HG changeset patch
# User haftmann
# Date 1455814389 -3600
# Node ID 95c6cf433c9188e55f279d71bcb16b3b6f5bf325
# Parent  8a105c235b1fa0bac9630f311a60039a357f11c4
more theorems

diff -r 8a105c235b1f -r 95c6cf433c91 src/HOL/Library/Multiset.thy
--- 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>
 
diff -r 8a105c235b1f -r 95c6cf433c91 src/HOL/Number_Theory/Factorial_Ring.thy
--- 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"
diff -r 8a105c235b1f -r 95c6cf433c91 src/HOL/Power.thy
--- 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
diff -r 8a105c235b1f -r 95c6cf433c91 src/HOL/Rings.thy
--- 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)