binomial: THEORY
%------------------------------------------------------------------------------
%
% Binomial coefficient
%
% Author: David Lester              Manchester University
%
%------------------------------------------------------------------------------

  BEGIN

  IMPORTING factorial, sigma_upto, product[posnat]

  n:    VAR nat
  pn:   VAR posnat
  nge2: VAR {k:posnat| k>=2}

  C(n:nat,k:{i:nat| i<=n}):posnat = factorial(n)/(factorial(k)*factorial(n-k))

  C_0:     LEMMA C(n,0)     = 1
  C_n:     LEMMA C(n,n)     = 1
  C_1:     LEMMA C(pn,1)    = pn
  C_n_1:   LEMMA C(pn,pn-1) = pn

  C_symmetry:  LEMMA FORALL (k:{i:nat| i<=n}): C(n,k) = C(n,n-k)

  C_n_plus_1:  LEMMA FORALL (k:{i:posnat| i<=n}): C(n+1,k) = C(n,k)+C(n,k-1)
  C_k_plus_1:  LEMMA FORALL (k:{i:nat| i<n}): C(n,k)*(n-k) = C(n,k+1)*(k+1)
  C_k_minus_1: LEMMA FORALL (k:{i:nat| i<n}): C(n,k+1) = C(n,k)*((n-k)/(k+1))

  C_2:         LEMMA C(nge2,2)      = (nge2*(nge2-1))/2
  C_n_2:       LEMMA C(nge2,nge2-2) = (nge2*(nge2-1))/2

  sigma_C:     LEMMA sigma(0,n,LAMBDA (i:{i:nat| i<=n}): C(n,i)) = 2^n

  % An iterative version of C(n,k) =  product(1,k,(n-(k-i))/i) 

  C_it(n:nat,k:{i:nat| i<=n}):rat =
    product_it(1,k,LAMBDA(i:posnat):(n-(k-i))/i)

  C_it_C : LEMMA
      C_it = C

  C_it_posnat : JUDGEMENT
    C_it(n:nat,k:{i:nat| i<=n}) HAS_TYPE posnat

  END binomial