# HG changeset patch
# User chaieb
# Date 1248376377 -7200
# Node ID 4082bd9824c90b42d5eef4f857c6e0018b629c46
# Parent  4dc119d4fc8bff1166f0ac1d95bafa27c5bede44
More theorems about pochhammer

diff -r 4dc119d4fc8b -r 4082bd9824c9 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Wed Jul 15 16:31:44 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Thu Jul 23 21:12:57 2009 +0200
@@ -288,6 +288,56 @@
     pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
   by (auto simp add: not_le[symmetric])
 
+
+lemma pochhammer_eq_0_iff: 
+  "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (EX k < n . a = - of_nat k) "
+  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
+  apply (cases n, auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
+  apply (rule_tac x=x in exI)
+  apply auto
+  done
+
+
+lemma pochhammer_eq_0_mono: 
+  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
+  unfolding pochhammer_eq_0_iff by auto 
+
+lemma pochhammer_neq_0_mono: 
+  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
+  unfolding pochhammer_eq_0_iff by auto 
+
+lemma pochhammer_minus:
+  assumes kn: "k \<le> n" 
+  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
+proof-
+  {assume k0: "k = 0" then have ?thesis by simp}
+  moreover 
+  {fix h assume h: "k = Suc h"
+    have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}"
+      using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
+      by auto
+    have ?thesis
+      unfolding h h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
+      apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
+      apply (auto simp add: inj_on_def image_def h )
+      apply (rule_tac x="h - x" in bexI)
+      by (auto simp add: expand_fun_eq h of_nat_diff)}
+  ultimately show ?thesis by (cases k, auto)
+qed
+
+lemma pochhammer_minus':
+  assumes kn: "k \<le> n" 
+  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
+  unfolding pochhammer_minus[OF kn, where b=b]
+  unfolding mult_assoc[symmetric]
+  unfolding power_add[symmetric]
+  apply simp
+  done
+
+lemma pochhammer_same: "pochhammer (- of_nat n) n = ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
+  unfolding pochhammer_minus[OF le_refl[of n]]
+  by (simp add: of_nat_diff pochhammer_fact)
+
 subsection{* Generalized binomial coefficients *}
 
 definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)