src/HOL/Finite_Set.thy
changeset 15543 0024472afce7
parent 15542 ee6cd48cf840
child 15552 8ab8e425410b
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 21 19:23:46 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Feb 22 10:54:30 2005 +0100
     1.3 @@ -905,11 +905,8 @@
     1.4  apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
     1.5  done
     1.6  
     1.7 -lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
     1.8 -  apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
     1.9 -  apply (erule ssubst, rule setsum_0)
    1.10 -  apply (rule setsum_cong, auto)
    1.11 -  done
    1.12 +lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
    1.13 +by(simp add:setsum_cong)
    1.14  
    1.15  lemma setsum_Un_Int: "finite A ==> finite B ==>
    1.16    setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
    1.17 @@ -954,7 +951,7 @@
    1.18   apply (cases "finite B") 
    1.19    apply (simp add: setsum_Sigma)
    1.20   apply (cases "A={}", simp)
    1.21 - apply (simp add: setsum_0) 
    1.22 + apply (simp) 
    1.23  apply (auto simp add: setsum_def
    1.24              dest: finite_cartesian_productD1 finite_cartesian_productD2) 
    1.25  done