msetprod_empty, msetprod_singleton

--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
@@ -72,6 +72,14 @@
 translations
   "PROD i :# A. b" == "CONST msetprod (%i. b) A"
 
+lemma msetprod_empty:
+  "msetprod f {#} = 1"
+  by (simp add: msetprod_def)
+
+lemma msetprod_singleton:
+  "msetprod f {#x#} = f x"
+  by (simp add: msetprod_def)
+
 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
   apply (simp add: msetprod_def power_add)
   apply (subst setprod_Un2)