src/HOL/Factorial.thy
changeset 67969 83c8cafdebe8
parent 67411 3f4b0c84630f
child 68224 1f7308050349
     1.1 --- a/src/HOL/Factorial.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Factorial.thy	Mon Apr 09 15:20:11 2018 +0100
     1.3 @@ -290,17 +290,13 @@
     1.4      using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
     1.5      by auto
     1.6    with Suc show ?thesis
     1.7 -    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
     1.8 -    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
     1.9 +    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"] 
    1.10 +    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff simp del: prod_constant)
    1.11  qed
    1.12  
    1.13  lemma pochhammer_minus':
    1.14    "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
    1.15 -  apply (simp only: pochhammer_minus [where b = b])
    1.16 -  apply (simp only: mult.assoc [symmetric])
    1.17 -  apply (simp only: power_add [symmetric])
    1.18 -  apply simp
    1.19 -  done
    1.20 +  by (simp add: pochhammer_minus)
    1.21  
    1.22  lemma pochhammer_same: "pochhammer (- of_nat n) n =
    1.23      ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"