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