author nipkow Mon, 20 Aug 2012 08:40:18 +0200 changeset 48861 461be56c312f parent 48860 56ec76f769c0 child 48862 8967b42db2d5
abstracted lemma
 src/HOL/Big_Operators.thy file | annotate | diff | comparison | revisions
```--- 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)"