1.1 --- a/src/HOL/Library/Binomial.thy	Thu Dec 05 20:22:53 2013 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Thu Dec 05 23:13:54 2013 +0000
     1.3 @@ -12,6 +12,8 @@
     1.4  text {* This development is based on the work of Andy Gordon and
     1.5    Florian Kammueller. *}
     1.6  
     1.7 +subsection {* Basic definitions and lemmas *}
     1.8 +
     1.9  primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
    1.10  where
    1.11    "0 choose k = (if k = 0 then 1 else 0)"
    1.12 @@ -48,11 +50,11 @@
    1.13  lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"
    1.14    by (induct n k rule: diff_induct) simp_all
    1.15  
    1.16 -lemma binomial_eq_0_iff: "n choose k = 0 \<longleftrightarrow> n < k"
    1.17 +lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k"
    1.18    by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)
    1.19  
    1.20 -lemma zero_less_binomial_iff: "n choose k > 0 \<longleftrightarrow> k \<le> n"
    1.21 -  by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv)
    1.22 +lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n"
    1.23 +  by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)
    1.24  
    1.25  (*Might be more useful if re-oriented*)
    1.26  lemma Suc_times_binomial_eq:
    1.27 @@ -76,12 +78,9 @@
    1.28    by (auto split add: nat_diff_split)
    1.29  
    1.30  
    1.31 -subsection {* Theorems about @{text "choose"} *}
    1.32 +subsection {* Combinatorial theorems involving @{text "choose"} *}
    1.33  
    1.34 -text {*
    1.35 -  \medskip Basic theorem about @{text "choose"}.  By Florian
    1.36 -  Kamm\"uller, tidied by LCP.
    1.37 -*}
    1.38 +text {*By Florian Kamm\"uller, tidied by LCP.*}
    1.39  
    1.40  lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1"
    1.41    by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
    1.42 @@ -139,10 +138,10 @@
    1.43  qed
    1.44  
    1.45  
    1.46 -text{* The binomial theorem (courtesy of Tobias Nipkow): *}
    1.47 +subsection {* The binomial theorem (courtesy of Tobias Nipkow): *}
    1.48  
    1.49 -(* Avigad's version, generalized to any commutative semiring *)
    1.50 -theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = 
    1.51 +text{* Avigad's version, generalized to any commutative ring *}
    1.52 +theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n = 
    1.53    (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
    1.54  proof (induct n)
    1.55    case 0 then show "?P 0" by simp
    1.56 @@ -178,7 +177,15 @@
    1.57    finally show "?P (Suc n)" by simp
    1.58  qed
    1.59  
    1.60 -subsection{* Pochhammer's symbol : generalized raising factorial*}
    1.61 +text{* Original version for the naturals *}
    1.62 +corollary binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
    1.63 +    using binomial_ring [of "int a" "int b" n]
    1.64 +  by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]
    1.65 +           of_nat_setsum [symmetric]
    1.66 +           of_nat_eq_iff of_nat_id)
    1.67 +
    1.68 +subsection{* Pochhammer's symbol : generalized rising factorial 
    1.69 +          See http://en.wikipedia.org/wiki/Pochhammer_symbol *}
    1.70  
    1.71  definition "pochhammer (a::'a::comm_semiring_1) n =
    1.72    (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
    1.73 @@ -313,9 +320,8 @@
    1.74      unfolding Suc pochhammer_Suc_setprod eq setprod_timesf[symmetric]
    1.75      apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
    1.76      using Suc
    1.77 -    apply (auto simp add: inj_on_def image_def)
    1.78 -    apply (rule_tac x="h - x" in bexI)
    1.79 -    apply (auto simp add: fun_eq_iff of_nat_diff)
    1.80 +    apply (auto simp add: inj_on_def image_def of_nat_diff)
    1.81 +    apply (metis atLeast0AtMost atMost_iff diff_diff_cancel diff_le_self)
    1.82      done
    1.83  qed
    1.84  
    1.85 @@ -402,8 +408,9 @@
    1.86  lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
    1.87  proof -
    1.88    { assume kn: "k > n"
    1.89 -    from kn binomial_eq_0[OF kn] have ?thesis
    1.90 -      by (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
    1.91 +    then have ?thesis
    1.92 +      by (subst binomial_eq_0[OF kn]) 
    1.93 +         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
    1.94    moreover
    1.95    { assume "k=0" then have ?thesis by simp }
    1.96    moreover