IsarMathLib

In this theory we discuss sequences defined by conditions of the form \(a_0 = x,\ a_{n+1} = f(a_n)\) and similar.

One way of defining a sequence (that is a function \(a:\mathbb{N}\rightarrow X\)) is to provide the first element of the sequence and a function to find the next value when we have the current one. This is usually called "defining a sequence by induction". In this section we set up the notion of a sequence defined by induction and prove the theorems needed to use it.

First we define a helper notion of the sequence defined inductively up to a given natural number \(n\).

From that we define the inductive sequence on the whole set of natural numbers. Recall that in Isabelle/ZF the set of natural numbers is denoted nat.

First we will consider the question of existence and uniqueness of finite inductive sequences. The proof is by induction and the next lemma is the \(P(0)\) step. To understand the notation recall that for natural numbers in set theory we have \(n = \{0,1,..,n-1\}\) and \( succ(n) \)\( = \{0,1,..,n\}\).

A lemma about restricting finite sequences needed for the proof of the inductive step of the existence and uniqueness of finite inductive seqences.

Existence and uniqueness of finite inductive sequences. The proof is by induction and the next lemma is the inductive step.

The next lemma combines indseq_exun0 and indseq_exun_ind to show the existence and uniqueness of finite sequences defined by induction.

We are now ready to prove the main theorem about finite inductive sequences.

Since we have uniqueness we can show the inverse of fin_indseq_props: a sequence that satisfies the inductive sequence properties listed there is the inductively defined sequence.

A corollary about the domain of a finite inductive sequence.

The collection of finite sequences defined by induction is consistent in the sense that the restriction of the sequence defined on a larger set to the smaller set is the same as the sequence defined on the smaller set.

For any two natural numbers one of the corresponding inductive sequences is contained in the other.

The inductive sequence generated by applying a function 0 times is just the singleton list containing the starting point.

The tail of an inductive sequence generated by \(f\) and started from \(x\) is the same as the inductive sequence started from \(f(x)\).

The first theorem about properties of infinite inductive sequences: inductive sequence is a indeed a sequence (i.e. a function on the set of natural numbers.

Restriction of an inductive sequence to a finite domain is the corresponding finite inductive sequence.

The first element of the inductive sequence starting at \(x\) and generated by \(f\) is indeed \(x\).

An infinite inductive sequence satisfies the inductive relation that defines it.

In this section we consider the properties of sets that are images of inductive sequences, that is are of the form \(\{f^{(n)} (x) : n \in N\}\) for some \(x\) in the domain of \(f\), where \(f^{(n)}\) denotes the \(n\)'th iteration of the function \(f\). For a function \(f:X\rightarrow X\) and a point \(x\in X\) such set is set is sometimes called the orbit of \(x\) generated by \(f\).

The basic properties of orbits.

In algebra we often talk about sets "generated" by an element, that is sets of the form (in multiplicative notation) \(\{a^n | n\in Z\}\). This is a related to a general notion of "power" (as in \(a^n = a\cdot a \cdot .. \cdot a\) ) or multiplicity \(n\cdot a = a+a+..+a\). The intuitive meaning of such notions is obvious, but we need to do some work to be able to use it in the formalized setting. This sections is devoted to sequences that are created by repeatedly applying a binary operation with the second argument fixed to some constant.

Basic propertes of sets generated by binary operations.

A simple corollary to the theorem binop_gen_set: a set that contains all iterations of the application of a binary operation exists.

A more general version of binop_gen_set where the generating binary operation acts on a larger set.

A generalization of binop_gen_set_ex that applies when the binary operation acts on a larger set. This is used in our Metamath translation to prove the existence of the set of real natural numbers. Metamath defines the real natural numbers as the smallest set that cantains \(1\) and is closed with respect to operation of adding \(1\).

A seemingly more general form of a sequence defined by induction is a sequence generated by the difference equation \(x_{n+1} = f_{n} (x_n)\) where \(n\mapsto f_n\) is a given sequence of functions such that each maps \(X\) into inself. For example when \(f_n (x) := x + x_n\) then the equation \(S_{n+1} = f_{n} (S_n)\) describes the sequence \(n \mapsto S_n = s_0 +\sum_{i=0}^n x_n\), i.e. the sequence of partial sums of the sequence \(\{s_0, x_0, x_1, x_3,..\}\).

The situation where the function that we iterate changes with \(n\) can be derived from the simpler case if we define the generating function appropriately. Namely, we replace the generating function in the definitions of InductiveSequenceN by the function \(f: X\times n \rightarrow X\times n\), \(f\langle x,k\rangle = \langle f_k(x), k+1 \rangle\) if \(k < n\), \(\langle f_k(x), k \rangle\) otherwise. The first notion defines the expression we will use to define the generating function. To understand the notation recall that in standard Isabelle/ZF for a pair \(s=\langle x,n \rangle\) we have fst\((s)=x\) and snd\((s)=n\).

Then we define the actual generating function on sets of pairs from \(X\times \{0,1, .. ,n\}\).

Having the generating function we can define the expression that we cen use to define the inductive sequence generates.

Finally we can define the sequence given by a initial point \(x\), and a sequence \(F\) of \(n\) functions.

The state transformation function (StateTransfFunN is a function that transforms \(X\times n\) into itself.

We can apply fin_indseq_props to the sequence used in the definition of InductiveSeqVarFN to get the properties of the sequence of states generated by the StateTransfFunN.

Basic properties of sequences defined by equation \(x_{n+1}=f_n (x_n)\).

Uniqueness lemma for sequences generated by equation \(x_{n+1}=f_n (x_n)\):

A sequence that has the properties of sequences generated by equation \(x_{n+1}=f_n (x_n)\) must be the one generated by this equation.

A consistency condition: if we make the sequence of generating functions shorter, then we get a shorter inductive sequence with the same values as in the original sequence.

One possible application of the inductive sequences is to define the Pascal's triangle. The Pascal's triangle can be defined directly as \(P_{n,k} = {n\choose k}= \frac{n!}{k!(n-k)!}\) for \(n\geq k \geq 0\). Formalizing this definition (or explaining to a 10-years old) is quite difficult as it depends on the definition of factorial and some facts about factorizing natural numbers needed to show that the quotient in \(\frac{n!}{k!(n-k)!}\) is always a natural number. Another approach uses induction and the property that each number in the array is the sum of the two numbers directly above it.

To shorten the definition of the function generating the Pascal's trangle we first define expression for the k'th element in the row following given row \(r\). The rows are represented as lists, i.e. functions \(r:n\rightarrow \mathbb{N}\) (recall that for natural numbers we have \(n=\{ 0,1,2,...,n-1\})\). The value of the next row is 1 at the beginning and equals \(r(k-1)+r(k)\) otherwise. A careful reader might wonder why we do not require the values to be 1 on the right boundary of the Pascal's triangle. We are able to show this as a theorem (see binom_right_boundary below) using the fact that in Isabelle/ZF the value of a function on an argument that is outside of the domain is the empty set, which is the same as zero of natural numbers.

Next we define a function that takes a row in a Pascal's triangle and returns the next row.

The function generating rows of the Pascal's triangle is indeed a function that maps nonempty lists of natural numbers into nonempty lists of natural numbers.

The value of the function GenBinom at a nonempty list \(r\) is a list of length one greater than the length of \(r\).

Now we are ready to define the Pascal's triangle as the inductive sequence that starts from a singleton list \(0\mapsto 1\) and is generated by iterations of the GenBinom function.

The singleton list containing 1 (i.e. the starting point of the inductive sequence that defines the PascalTriangle) is a finite list and the PascalTriangle is a sequence (an infinite list) of nonempty lists of natural numbers.

The GenBinom function creates the next row of the Pascal's triangle from the previous one.

The \(n\)'th row of the Pascal's triangle is a list of \(n+1\) natural numbers.

In our approach the Pascal's triangle is a list of lists. The value at index \(n\in \mathbb{N}\) is a list of length \(n+1\) (see pascal_row_list above). Hence, the largest index in the domain of this list is \(n\). However, we can still show that the value of that list at index \(n+1\) is 0, because in Isabelle/ZF (as well as in Metamath) the value of a function at a point outside of the domain is the empty set, which happens to be the same as the natural number 0.

For \(n>0\) the Pascal's triangle values at \((n,k)\) are given by the BinomElem expression.

The notion that will actually be used is the binomial coefficient \({n\choose k}\) which we define as the value at the right place of the Pascal's triangle.

Entries in the Pascal's triangle are natural numbers. Since in Isabelle/ZF the value of a function at a point that is outside of the domain is the empty set (which is the same as zero of natural numbers) we do not need any assumption on \(k\).

The top of the Pascal's triangle is equal to 1 (i.e. \({0\choose 0}=1\)). This is an easy fact that it is useful to have handy as it is at the start of a couple of inductive arguments.

The binomial coefficients are 1 on the left boundary of the Pascal's triangle.

The main recursive property of binomial coefficients: each number in the \({n\choose k}\), \(n>0, 0\neq k\leq n\) array (i.e. the Pascal's triangle except the top) is the sum of the two numbers directly above it. The statement looks like it has an off-by-one error in the assumptions, but it's ok and needed later.

A version binom_prop where we write \(k+1\) instead of \(k\).

A special case of binom_prop when \(n=k+1\) that helps with the induction step in the proof that the binomial coefficient are 1 on the right boundary of the Pascal's triangle.

The binomial coefficients are 1 on the right boundary of the Pascal's triangle.