author paulson Wed May 31 11:55:21 2000 +0200 (2000-05-31) changeset 9002 a752f2499dae parent 9001 93af64f54bf2 child 9003 3747ec2aeb86
new theorems (some from Multiset)
 src/HOL/Finite.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite.ML	Tue May 30 18:02:49 2000 +0200
1.2 +++ b/src/HOL/Finite.ML	Wed May 31 11:55:21 2000 +0200
1.3 @@ -688,12 +688,30 @@
1.4  qed "setsum_insert";
1.6
1.7 +Goal "finite A ==> setsum (%i. 0) A = 0";
1.8 +by (etac finite_induct 1);
1.9 +by Auto_tac;
1.10 +qed "setsum_0";
1.11 +
1.12 +Goal "finite F ==> (setsum f F = 0) = (! a:F. f a = (0::nat))";
1.13 +by (etac finite_induct 1);
1.14 +by Auto_tac;
1.15 +qed "setsum_eq_0_iff";
1.17 +
1.18 +Goal "[| setsum f F = Suc n; finite F |] ==> EX a:F. 0 < f a";
1.19 +by (etac rev_mp 1);
1.20 +by (etac finite_induct 1);
1.21 +by Auto_tac;
1.22 +qed "setsum_SucD";
1.23 +
1.24  (*Could allow many "card" proofs to be simplified*)
1.25  Goal "finite A ==> card A = setsum (%x. 1) A";
1.26  by (etac finite_induct 1);
1.27  by Auto_tac;
1.28  qed "card_eq_setsum";
1.29
1.30 +(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
1.31  Goal "[| finite A; finite B |] \
1.32  \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
1.33  by (etac finite_induct 1);
```