# HG changeset patch # User nipkow # Date 1345028214 -7200 # Node ID bfd136281c136b1dd3568f4e1147888a0d958081 # Parent 6cf7a9d8bbaf5488cf82c558bf3c2690cbc9cb77 Backed out changeset 6cf7a9d8bbaf diff -r 6cf7a9d8bbaf -r bfd136281c13 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Wed Aug 15 12:18:30 2012 +0200 +++ b/src/HOL/Big_Operators.thy Wed Aug 15 12:56:54 2012 +0200 @@ -39,12 +39,6 @@ then show ?thesis unfolding `A = B` by simp qed -lemma F_unit[simp]: "F (%i. 1) A = 1" -by (cases "finite A") (erule finite_induct, auto) - -lemma F_unit': "ALL a:A. g a = 1 ==> F g A = 1" -by (simp add:F_cong) - lemma If_cases: fixes P :: "'b \ bool" and g h :: "'b \ 'a" assumes fA: "finite A" @@ -208,8 +202,11 @@ ==> setsum h B = setsum g A" by (simp add: setsum_reindex) -lemmas setsum_0 = setsum.F_unit -lemmas setsum_0' = setsum.F_unit' +lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0" + by (cases "finite A") (erule finite_induct, auto) + +lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0" + by (simp add:setsum_cong) lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" @@ -945,9 +942,16 @@ using I0 by auto -lemmas setprod_1 = setprod.F_unit -lemmas setprod_1' = setprod.F_unit' +lemma setprod_1: "setprod (%i. 1) A = 1" +apply (case_tac "finite A") +apply (erule finite_induct, auto simp add: mult_ac) +done +lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" +apply (subgoal_tac "setprod f F = setprod (%x. 1) F") +apply (erule ssubst, rule setprod_1) +apply (rule setprod_cong, auto) +done lemma setprod_Un_Int: "finite A ==> finite B ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"