src/HOL/Library/Binomial.thy
 changeset 30843 3419ca741dbf parent 30663 0b6aff7451b2 child 31021 53642251a04f
```     1.1 --- a/src/HOL/Library/Binomial.thy	Wed Apr 01 18:41:15 2009 +0200
1.2 +++ b/src/HOL/Library/Binomial.thy	Wed Apr 01 22:29:10 2009 +0200
1.3 @@ -267,8 +267,6 @@
1.4    moreover
1.5    {assume n0: "n \<noteq> 0"
1.6      then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
1.7 -  apply (rule iffD2[OF setprod_zero_eq])
1.8 -  apply auto
1.9    apply (rule_tac x="n" in bexI)
1.10    using h kn by auto}
1.11  ultimately show ?thesis by blast
1.12 @@ -281,8 +279,7 @@
1.13    moreover
1.14    {fix h assume h: "k = Suc h"
1.15      then have ?thesis apply (simp add: pochhammer_Suc_setprod)
1.16 -      apply (subst setprod_zero_eq_field)
1.17 -      using h kn by (auto simp add: ring_simps)}
1.18 +      using h kn by (auto simp add: algebra_simps)}
1.19    ultimately show ?thesis by (cases k, auto)
1.20  qed
1.21
1.22 @@ -299,15 +296,14 @@
1.23    where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
1.24
1.25  lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
1.26 -  apply (simp_all add: gbinomial_def)
1.27 -  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
1.28 -  apply simp
1.29 -  apply (rule iffD2[OF setprod_zero_eq])
1.30 -  by auto
1.32 +apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
1.33 + apply (simp del:setprod_zero_iff)
1.34 +apply simp
1.35 +done
1.36
1.37  lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
1.38  proof-
1.39 -
1.40    {assume "n=0" then have ?thesis by simp}
1.41    moreover
1.42    {assume n0: "n\<noteq>0"
1.43 @@ -388,7 +384,6 @@
1.44        unfolding mult_assoc[symmetric]
1.45        unfolding setprod_timesf[symmetric]
1.46        apply simp
1.47 -      apply (rule disjI2)
1.48        apply (rule strong_setprod_reindex_cong[where f= "op - n"])
1.49        apply (auto simp add: inj_on_def image_iff Bex_def)
1.50        apply presburger
```