# HG changeset patch
# User haftmann
# Date 1349385542 -7200
# Node ID 16d8c6d288bcf85bf3e28d28f4c995641b9fdac6
# Parent  2c7c32f342207f0a208c2caa922aa8bd8e8315c7
more facts on setsum and setprod

diff -r 2c7c32f34220 -r 16d8c6d288bc src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Oct 04 17:26:04 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Thu Oct 04 23:19:02 2012 +0200
@@ -447,6 +447,15 @@
    setsum f A + setsum f B - setsum f (A Int B)"
 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
 
+lemma setsum_Un2:
+  assumes "finite (A \<union> B)"
+  shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
+proof -
+  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
+    by auto
+  with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
+qed
+
 lemma (in comm_monoid_add) setsum_eq_general_reverses:
   assumes fS: "finite S" and fT: "finite T"
   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
@@ -1087,6 +1096,15 @@
    = setprod f A * setprod f B / setprod f (A Int B)"
 by (subst setprod_Un_Int [symmetric], auto)
 
+lemma setprod_Un2:
+  assumes "finite (A \<union> B)"
+  shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
+proof -
+  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
+    by auto
+  with assms show ?thesis by simp (subst setprod_Un_disjoint, auto)+
+qed
+
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =
   (if a:A then setprod f A / f a else setprod f A)"