# HG changeset patch
# User paulson
# Date 959766921 -7200
# Node ID a752f2499dae3a99899f0d8a01988ac7301c8bce
# Parent  93af64f54bf2d6b1b469d6c8e3def8eaca776602
new theorems (some from Multiset)

diff -r 93af64f54bf2 -r a752f2499dae src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue May 30 18:02:49 2000 +0200
+++ b/src/HOL/Finite.ML	Wed May 31 11:55:21 2000 +0200
@@ -688,12 +688,30 @@
 qed "setsum_insert";
 Addsimps [setsum_insert];
 
+Goal "finite A ==> setsum (%i. 0) A = 0";
+by (etac finite_induct 1);
+by Auto_tac;
+qed "setsum_0";
+
+Goal "finite F ==> (setsum f F = 0) = (! a:F. f a = (0::nat))";
+by (etac finite_induct 1);
+by Auto_tac;
+qed "setsum_eq_0_iff";
+Addsimps [setsum_eq_0_iff];
+
+Goal "[| setsum f F = Suc n; finite F |] ==> EX a:F. 0 < f a";
+by (etac rev_mp 1);
+by (etac finite_induct 1);
+by Auto_tac;
+qed "setsum_SucD";
+
 (*Could allow many "card" proofs to be simplified*)
 Goal "finite A ==> card A = setsum (%x. 1) A";
 by (etac finite_induct 1);
 by Auto_tac;
 qed "card_eq_setsum";
 
+(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
 Goal "[| finite A; finite B |] \
 \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
 by (etac finite_induct 1);