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.31 +apply (simp_all add: gbinomial_def)
    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