288 case (Suc h) |
288 case (Suc h) |
289 have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)" |
289 have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)" |
290 using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"] |
290 using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"] |
291 by auto |
291 by auto |
292 with Suc show ?thesis |
292 with Suc show ?thesis |
293 using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"] |
293 using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"] |
294 by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff) |
294 by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff simp del: prod_constant) |
295 qed |
295 qed |
296 |
296 |
297 lemma pochhammer_minus': |
297 lemma pochhammer_minus': |
298 "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" |
298 "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" |
299 apply (simp only: pochhammer_minus [where b = b]) |
299 by (simp add: pochhammer_minus) |
300 apply (simp only: mult.assoc [symmetric]) |
|
301 apply (simp only: power_add [symmetric]) |
|
302 apply simp |
|
303 done |
|
304 |
300 |
305 lemma pochhammer_same: "pochhammer (- of_nat n) n = |
301 lemma pochhammer_same: "pochhammer (- of_nat n) n = |
306 ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n" |
302 ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n" |
307 unfolding pochhammer_minus |
303 unfolding pochhammer_minus |
308 by (simp add: of_nat_diff pochhammer_fact) |
304 by (simp add: of_nat_diff pochhammer_fact) |