choose_reduce_nat: re-ordered operands
authorpaulson <lp15@cam.ac.uk>
Thu Oct 30 16:36:44 2014 +0000 (2014-10-30)
changeset 5883309974789e483
parent 58832 ec9550bd5fd7
child 58834 773b378d9313
choose_reduce_nat: re-ordered operands
src/HOL/Number_Theory/Binomial.thy
     1.1 --- a/src/HOL/Number_Theory/Binomial.thy	Thu Oct 30 11:24:53 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Thu Oct 30 16:36:44 2014 +0000
     1.3 @@ -32,8 +32,8 @@
     1.4  
     1.5  lemma choose_reduce_nat: 
     1.6    "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>
     1.7 -    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
     1.8 -  by (metis Suc_diff_1 binomial.simps(2) add.commute neq0_conv)
     1.9 +    (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
    1.10 +  by (metis Suc_diff_1 binomial.simps(2) neq0_conv)
    1.11  
    1.12  lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"
    1.13    by (induct n arbitrary: k) auto
    1.14 @@ -524,7 +524,6 @@
    1.15        using Suc
    1.16        apply auto
    1.17      done
    1.18 -
    1.19    have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
    1.20      ((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)"
    1.21      apply (simp add: Suc field_simps del: fact_Suc)
    1.22 @@ -547,6 +546,10 @@
    1.23    finally show ?thesis by (simp del: fact_Suc)
    1.24  qed
    1.25  
    1.26 +lemma gbinomial_reduce_nat:
    1.27 +  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
    1.28 +by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
    1.29 +
    1.30  
    1.31  lemma binomial_symmetric:
    1.32    assumes kn: "k \<le> n"