# HG changeset patch
# User nipkow
# Date 1238743651 -7200
# Node ID 29eb80cef6b74f0f683c1876361312a554f30ec7
# Parent  2048e99f4e3eec7210d9ac5d59b7f61386d77ab3
added setsum_eq_1_iff

diff -r 2048e99f4e3e -r 29eb80cef6b7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Apr 02 22:03:04 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Apr 03 09:27:31 2009 +0200
@@ -1216,6 +1216,14 @@
     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
 by (induct set: finite) auto
 
+lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
+  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
+apply(erule finite_induct)
+apply (auto simp add:add_is_1)
+done
+
+lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
+
 lemma setsum_Un_nat: "finite A ==> finite B ==>
   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   -- {* For the natural numbers, we have subtraction. *}