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