src/HOL/Library/Binomial.thy
changeset 47108 2a1953f0d20d
parent 46757 ad878aff9c15
child 48830 72efe3e0a46b
     1.1 --- a/src/HOL/Library/Binomial.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4      have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
     1.5        by auto
     1.6      from n0 have ?thesis 
     1.7 -      by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric])}
     1.8 +      by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *)}
     1.9    ultimately show ?thesis by blast
    1.10  qed
    1.11  
    1.12 @@ -417,8 +417,8 @@
    1.13      from eq[symmetric]
    1.14      have ?thesis using kn
    1.15        apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
    1.16 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
    1.17 -      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
    1.18 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one)
    1.19 +      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one)
    1.20        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
    1.21        unfolding mult_assoc[symmetric] 
    1.22        unfolding setprod_timesf[symmetric]