Tutorial/binomial/binomial.tex

2 % The Binomial Theorem proven in HOL %
7 % The Binomial Theorem proven in HOL.
30 The earliest surviving description is from the tenth century,
32 The Binomial Theorem itself was first reported in 1676 by Isaac Newton.
44 The construction is as follows. The numbers at the edges
48 The numbers in Pascal's Triangle are called Binomial Coefficients.
49 The number in the $n$th row and $k$th column (where $0 \leq k \leq n$, and the
51 $n \choose k$ and pronounced ``$n$ choose $k$''.  The coefficients are
62 The rest of this \self{} describes how the Binomial Theorem can be proven
67 The motivation for the proof of the Binomial Theorem in \HOL{} is
71 The proof illustrates specific ways in \HOL{} to represent mathematical
73 monoids, groups and rings. The following files accompany this \self{} in
77     The \ML{} program containing the definitions, lemmas and theorems\\
81     The theory file which is generated by \verb@mk_BINOMIAL.ml@.
86     The Binomial Theorem is bound to the \ML{} identifier \verb@BINOMIAL@.
88 % The aim of this \self{} is to introduce the small amount of algebra and
92 The \self{} is meant to be intelligible
100 The way to work with this case study is first to study this \self{} to see
118 (This is the first display of an interaction with \HOL{}.  The difference
124 The first input line in the display above loads in all the definitions,
125 theorems, derived rules and the tactic defined for the proof.  The second
126 input line asks \HOL{} to print theorem \verb@BINOMIAL@.  The constants
127 used in \verb@BINOMIAL@ are explained later in the \self{}.  The \HOL{}
132 The remainder of the \self{} follows the plan:
151     The proof is by induction, and depends on three main lemmas.
162 \section{The Binomial Coefficients}
165 The definition of the binomial coefficients as the numbers in Pascal's Triangle
174 the triangle as filled with $0$'s.) The desire is to define a constant
191 The theory \verb@prim_rec@ contains a primitive recursion theorem which
269 How might these laws be represented in \HOL{}?  The simplest scheme is
277 The two laws can be defined as two constants in \HOL{}:
308 The first step is to strip off the quantifiers, and break up the implication:
318 The next step is to rewrite \verb@plus a b@ to \verb@plus b a@ on the
394 The point of this example was to illustrate how to prove theorems about
396 like \verb@ASSOCIATIVE@ and \verb@COMMUTATIVE@. The main difficulty is
397 in deriving equations for use with rewriting or substitution.  The solution
420 The final new derived rule used in the proof of the Binomial Theorem
474 is unique.  The first step is to prove that there exists a function \verb@Id@
485 The proof of \verb@ID_LEMMA@ uses Hilbert's $\epsilon$-operator to
500 The condition that \verb@Id plus@ is a left and right identity is expressed
523 The use of these last two theorems is to help identify the element
525 of \verb@arithmetic@.  The abbreviations \verb@LEFT_ID@ and \verb@RIGHT_ID@
547 An alternative characterisation of \verb@Group@\footnote{The mixed
555 element \verb@Inv plus a@ is an inverse of \verb@a@.  The function
577 The predicates which say that \verb@Inv@ produces left and right inverses
593 The theory of groups has been developed only as far as needed to prove
603 is commutative.  The word ring is used in the remainder of this \self{}
637 The definition is a tree of predicates with atomic ones like
680 The one lemma about rings needed here, \verb@RING_0@, is stated in
689 The aim of this section is to explain how the mathematical notation
700 are scalar powers and the $\Sigma$-notation.  The latter is tackled in
732 definition by primitive recursion and proof by induction. The theory of
763 The constant \verb@RANGE@, which is a curried function of two numbers,
802 The standard $\Sigma$-notation is defined informally by the equation,
822 The brackets around the $n$ above the $\Sigma$ distinguish this
826 The difference between the two is just that the standard notation is
827 definable via \verb@INTERVAL@, and the second via \verb@RANGE@. The second
830 has a more complex definition. The disadvantage of this choice is that
835 The non-standard $\Sigma$-notation is defined in \HOL{} as the following
851 The functions \verb@REDUCE@ and \verb@RANGE@ are needed here only to define
859 \section{The Binomial Theorem for a Commutative Ring}
866 The statement and proof of the Binomial Theorem use a new \HOL{} constant,
891 In outline, the proof proceeds as follows.  The following equation is
923 \verb@LEMMA_1@ is the key to the inductive step. The three stages of the
958 \section{The Binomial Theorem for Integers}
961 The previous sections have dealt with the material in theory \verb@BINOMIAL@,