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.

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 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)\).

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.