equal
deleted
inserted
replaced
396 |
396 |
397 lemma gbinomial_mult_1: "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") |
397 lemma gbinomial_mult_1: "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") |
398 proof- |
398 proof- |
399 have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" |
399 have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" |
400 unfolding gbinomial_pochhammer |
400 unfolding gbinomial_pochhammer |
401 pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc |
401 pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc |
402 by (simp add: field_simps del: of_nat_Suc) |
402 by (simp add: field_simps del: of_nat_Suc) |
403 also have "\<dots> = ?l" unfolding gbinomial_pochhammer |
403 also have "\<dots> = ?l" unfolding gbinomial_pochhammer |
404 by (simp add: ring_simps) |
404 by (simp add: ring_simps) |
405 finally show ?thesis .. |
405 finally show ?thesis .. |
406 qed |
406 qed |
412 by (simp add: gbinomial_def) |
412 by (simp add: gbinomial_def) |
413 |
413 |
414 lemma gbinomial_mult_fact: |
414 lemma gbinomial_mult_fact: |
415 "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
415 "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
416 unfolding gbinomial_Suc |
416 unfolding gbinomial_Suc |
417 by (simp_all add: field_simps del: fact_Suc_nat) |
417 by (simp_all add: field_simps del: fact_Suc) |
418 |
418 |
419 lemma gbinomial_mult_fact': |
419 lemma gbinomial_mult_fact': |
420 "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
420 "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
421 using gbinomial_mult_fact[of k a] |
421 using gbinomial_mult_fact[of k a] |
422 apply (subst mult_commute) . |
422 apply (subst mult_commute) . |
430 apply (rule strong_setprod_reindex_cong[where f = Suc]) |
430 apply (rule strong_setprod_reindex_cong[where f = Suc]) |
431 using h by auto |
431 using h by auto |
432 |
432 |
433 have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)" |
433 have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)" |
434 unfolding h |
434 unfolding h |
435 apply (simp add: ring_simps del: fact_Suc_nat) |
435 apply (simp add: ring_simps del: fact_Suc) |
436 unfolding gbinomial_mult_fact' |
436 unfolding gbinomial_mult_fact' |
437 apply (subst fact_Suc_nat) |
437 apply (subst fact_Suc) |
438 unfolding of_nat_mult |
438 unfolding of_nat_mult |
439 apply (subst mult_commute) |
439 apply (subst mult_commute) |
440 unfolding mult_assoc |
440 unfolding mult_assoc |
441 unfolding gbinomial_mult_fact |
441 unfolding gbinomial_mult_fact |
442 by (simp add: ring_simps) |
442 by (simp add: ring_simps) |
447 using eq0 |
447 using eq0 |
448 unfolding h setprod_nat_ivl_1_Suc |
448 unfolding h setprod_nat_ivl_1_Suc |
449 by simp |
449 by simp |
450 also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" |
450 also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" |
451 unfolding gbinomial_mult_fact .. |
451 unfolding gbinomial_mult_fact .. |
452 finally have ?thesis by (simp del: fact_Suc_nat) } |
452 finally have ?thesis by (simp del: fact_Suc) } |
453 ultimately show ?thesis by (cases k, auto) |
453 ultimately show ?thesis by (cases k, auto) |
454 qed |
454 qed |
455 |
455 |
456 end |
456 end |