src/HOL/Binomial.thy
changeset 63306 ca187a9f66da
parent 63092 a949b2a5f51d
child 63363 bd483ddb17f2
equal deleted inserted replaced
63305:3b6975875633 63306:ca187a9f66da
   669                  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
   669                  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
   670              of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
   670              of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
   671     by (simp add: of_nat_mult field_simps pochhammer_rec')
   671     by (simp add: of_nat_mult field_simps pochhammer_rec')
   672   finally show ?case .
   672   finally show ?case .
   673 qed simp
   673 qed simp
       
   674 
       
   675 lemma fact_double:
       
   676   "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"
       
   677   using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
   674 
   678 
   675 lemma pochhammer_absorb_comp:
   679 lemma pochhammer_absorb_comp:
   676   "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
   680   "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
   677   (is "?lhs = ?rhs")
   681   (is "?lhs = ?rhs")
   678 proof -
   682 proof -