new theorems (some from Multiset)
authorpaulson
Wed May 31 11:55:21 2000 +0200 (2000-05-31)
changeset 9002a752f2499dae
parent 9001 93af64f54bf2
child 9003 3747ec2aeb86
new theorems (some from Multiset)
src/HOL/Finite.ML
     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.5  Addsimps [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.16 +Addsimps [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);