src/HOL/Groups_Big.thy
 changeset 55096 916b2ac758f4 parent 54745 46e441e61ff5 child 56166 9a241bc276cd
```     1.1 --- a/src/HOL/Groups_Big.thy	Tue Jan 21 13:05:22 2014 +0100
1.2 +++ b/src/HOL/Groups_Big.thy	Tue Jan 21 13:21:55 2014 +0100
1.3 @@ -1332,38 +1332,6 @@
1.4      by induct (auto simp add: field_simps abs_mult)
1.5  qed auto
1.6
1.7 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
1.8 -apply (erule finite_induct)
1.9 -apply auto
1.10 -done
1.11 -
1.12 -lemma setprod_gen_delta:
1.13 -  assumes fS: "finite S"
1.14 -  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.15 -proof-
1.16 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
1.17 -  {assume a: "a \<notin> S"
1.18 -    hence "\<forall> k\<in> S. ?f k = c" by simp
1.19 -    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
1.20 -  moreover
1.21 -  {assume a: "a \<in> S"
1.22 -    let ?A = "S - {a}"
1.23 -    let ?B = "{a}"
1.24 -    have eq: "S = ?A \<union> ?B" using a by blast
1.25 -    have dj: "?A \<inter> ?B = {}" by simp
1.26 -    from fS have fAB: "finite ?A" "finite ?B" by auto
1.27 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
1.28 -      apply (rule setprod_cong) by auto
1.29 -    have cA: "card ?A = card S - 1" using fS a by auto
1.30 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
1.31 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1.32 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.33 -      by simp
1.34 -    then have ?thesis using a cA
1.35 -      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
1.36 -  ultimately show ?thesis by blast
1.37 -qed
1.38 -
1.39  lemma setprod_eq_1_iff [simp]:
1.40    "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
1.41    by (induct set: finite) auto
```