src/HOL/Power.thy
 changeset 57418 6ab1c7cb0b8d parent 56544 b60d5d119489 child 57512 cc97b347b301
```     1.1 --- a/src/HOL/Power.thy	Fri Jun 27 22:08:55 2014 +0200
1.2 +++ b/src/HOL/Power.thy	Sat Jun 28 09:16:42 2014 +0200
1.3 @@ -761,6 +761,22 @@
1.4      done
1.5  qed
1.6
1.7 +
1.8 +subsubsection {* Generalized sum over a set *}
1.9 +
1.10 +lemma setsum_zero_power [simp]:
1.11 +  fixes c :: "nat \<Rightarrow> 'a::division_ring"
1.12 +  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
1.13 +apply (cases "finite A")
1.14 +  by (induction A rule: finite_induct) auto
1.15 +
1.16 +lemma setsum_zero_power' [simp]:
1.17 +  fixes c :: "nat \<Rightarrow> 'a::field"
1.18 +  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
1.19 +  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
1.20 +  by auto
1.21 +
1.22 +
1.23  subsubsection {* Generalized product over a set *}
1.24
1.25  lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
1.26 @@ -768,6 +784,17 @@
1.27  apply auto
1.28  done
1.29
1.30 +lemma setprod_power_distrib:
1.31 +  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
1.32 +  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
1.33 +proof (cases "finite A")
1.34 +  case True then show ?thesis
1.35 +    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
1.36 +next
1.37 +  case False then show ?thesis
1.38 +    by simp
1.39 +qed
1.40 +
1.41  lemma setprod_gen_delta:
1.42    assumes fS: "finite S"
1.43    shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
1.44 @@ -784,14 +811,14 @@
1.45      have dj: "?A \<inter> ?B = {}" by simp
1.46      from fS have fAB: "finite ?A" "finite ?B" by auto
1.47      have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
1.48 -      apply (rule setprod_cong) by auto
1.49 +      apply (rule setprod.cong) by auto
1.50      have cA: "card ?A = card S - 1" using fS a by auto
1.51      have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
1.52      have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1.53 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.54 +      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.55        by simp
1.56      then have ?thesis using a cA
1.57 -      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
1.58 +      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
1.59    ultimately show ?thesis by blast
1.60  qed
1.61
```