# HG changeset patch
# User nipkow
# Date 1345444818 -7200
# Node ID 461be56c312f0c8392b86fca06f2a7516c5c4a94
# Parent  56ec76f769c0b45ec0dcdadae3d562f8c3718aac
abstracted lemma

diff -r 56ec76f769c0 -r 461be56c312f src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sun Aug 19 19:31:45 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Mon Aug 20 08:40:18 2012 +0200
@@ -105,6 +105,9 @@
   "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
 using F_delta[OF fS, of a b, symmetric] by (auto intro: F_cong)
 
+lemma F_fun_f: "F (%x. g x * h x) A = (F g A * F h A)"
+by (cases "finite A") (simp_all add: distrib)
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fA: "finite A"
@@ -367,8 +370,8 @@
             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
 done
 
-lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-  by (cases "finite A") (simp_all add: setsum.distrib)
+lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
+by (fact setsum.F_fun_f)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -1036,9 +1039,8 @@
             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
 done
 
-lemma setprod_timesf:
-     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
-by(simp add:setprod_def fold_image_distrib)
+lemma setprod_timesf: "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
+by (fact setprod.F_fun_f)
 
 
 subsubsection {* Properties in more restricted classes of structures *}