# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory InductiveSeq_ZF imports Nat_ZF_IML FiniteSeq_ZF FinOrd_ZF
begin

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

### Sequences defined by induction

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$$.

Definition

$$\text{InductiveSequenceN}(x,f,n) \equiv$$ $$\text{The } a.\ a: succ(n) \rightarrow domain(f) \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$

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.

Definition

$$\text{InductiveSequence}(x,f) \equiv \bigcup n\in nat.\ \text{InductiveSequenceN}(x,f,n)$$

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\}$$.

lemma indseq_exun0:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$

shows $$\exists ! a.\ a: succ(0) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in 0.\ a(succ(k)) = f(a(k)) )$$proof
fix $$a$$ $$b$$
assume A3: $$a: succ(0) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in 0.\ a(succ(k)) = f(a(k)) )$$, $$b: succ(0) \rightarrow X \wedge b(0) = x \wedge ( \forall k\in 0.\ b(succ(k)) = f(b(k)) )$$
moreover
have $$succ(0) = \{0\}$$
ultimately have $$a: \{0\} \rightarrow X$$, $$b: \{0\} \rightarrow X$$
then have $$a = \{\langle 0, a(0)\rangle \}$$, $$b = \{\langle 0, b(0)\rangle \}$$ using func_singleton_pair
with A3 show $$a=b$$
next
let $$a = \{\langle 0,x\rangle \}$$
have $$a : \{0\} \rightarrow \{x\}$$ using singleton_fun
moreover
from A1, A2 have $$\{x\} \subseteq X$$
ultimately have $$a : \{0\} \rightarrow X$$ using func1_1_L1B
moreover
have $$\{0\} = succ(0)$$
ultimately have $$a : succ(0) \rightarrow X$$
with A1 show $$\exists a.\ a: succ(0) \rightarrow X \wedge a(0) = x \wedge (\forall k\in 0.\ a(succ(k)) = f(a(k)))$$ using singleton_apply
qed

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

lemma indseq_restrict:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$ and A4: $$a: succ(succ(n))\rightarrow X \wedge a(0) = x \wedge (\forall k\in succ(n).\ a(succ(k)) = f(a(k)))$$ and A5: $$a_r = \text{restrict}(a,succ(n))$$

shows $$a_r: succ(n) \rightarrow X \wedge a_r(0) = x \wedge ( \forall k\in n.\ a_r(succ(k)) = f(a_r(k)) )$$proof
from A3 have $$succ(n) \subseteq succ(succ(n))$$
with A4, A5 have $$a_r: succ(n) \rightarrow X$$ using restrict_type2
moreover
from A3 have $$0 \in succ(n)$$ using empty_in_every_succ
with A4, A5 have $$a_r(0) = x$$ using restrict_if
moreover
from A3, A4, A5 have $$\forall k\in n.\ a_r(succ(k)) = f(a_r(k))$$ using succ_ineq, restrict_if
ultimately show $$thesis$$
qed

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

lemma indseq_exun_ind:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$ and A4: $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$

shows $$\exists ! a.\ a: succ(succ(n)) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall k\in succ(n).\ a(succ(k)) = f(a(k)) )$$proof
fix $$a$$ $$b$$
assume A5: $$a: succ(succ(n)) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall k\in succ(n).\ a(succ(k)) = f(a(k)) )$$ and A6: $$b: succ(succ(n)) \rightarrow X \wedge b(0) = x \wedge$$ $$( \forall k\in succ(n).\ b(succ(k)) = f(b(k)) )$$
show $$a = b$$proof
let $$a_r = \text{restrict}(a,succ(n))$$
let $$b_r = \text{restrict}(b,succ(n))$$
note A1, A2, A3, A5
moreover
have $$a_r = \text{restrict}(a,succ(n))$$
ultimately have I: $$a_r: succ(n) \rightarrow X \wedge a_r(0) = x \wedge ( \forall k\in n.\ a_r(succ(k)) = f(a_r(k)) )$$ by (rule indseq_restrict )
note A1, A2, A3, A6
moreover
have $$b_r = \text{restrict}(b,succ(n))$$
ultimately have $$b_r: succ(n) \rightarrow X \wedge b_r(0) = x \wedge ( \forall k\in n.\ b_r(succ(k)) = f(b_r(k)) )$$ by (rule indseq_restrict )
with A4, I have II: $$a_r = b_r$$
from A3 have $$succ(n) \in nat$$
moreover
from A5, A6 have $$a: succ(succ(n)) \rightarrow X$$ and $$b: succ(succ(n)) \rightarrow X$$
moreover
note II
moreover
have T: $$n \in succ(n)$$
then have $$a_r(n) = a(n)$$ and $$b_r(n) = b(n)$$ using restrict
with A5, A6, II, T have $$a(succ(n)) = b(succ(n))$$
ultimately show $$a = b$$ by (rule finseq_restr_eq )
qed
next
show $$\exists a.\ a: succ(succ(n)) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall k\in succ(n).\ a(succ(k)) = f(a(k)) )$$proof
from A4 obtain $$a$$ where III: $$a: succ(n) \rightarrow X$$ and IV: $$a(0) = x$$ and V: $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
let $$b = a \cup \{\langle succ(n), f(a(n))\rangle \}$$
from A1, III have VI: $$b : succ(succ(n)) \rightarrow X$$ and VII: $$\forall k \in succ(n).\ b(k) = a(k)$$ and VIII: $$b(succ(n)) = f(a(n))$$ using apply_funtype, finseq_extend
from A3 have $$0 \in succ(n)$$ using empty_in_every_succ
with IV, VII have IX: $$b(0) = x$$
{
fix $$k$$
assume $$k \in succ(n)$$
then have $$k\in n \vee k = n$$
moreover {
assume A7: $$k \in n$$
with A3, VII have $$b(succ(k)) = a(succ(k))$$ using succ_ineq
also
from A7, V, VII have $$a(succ(k)) = f(b(k))$$
finally have $$b(succ(k)) = f(b(k))$$
} moreover {
assume A8: $$k = n$$
with VIII have $$b(succ(k)) = f(a(k))$$
with A8, VII, VIII have $$b(succ(k)) = f(b(k))$$
} ultimately have $$b(succ(k)) = f(b(k))$$
}
then have $$\forall k \in succ(n).\ b(succ(k)) = f(b(k))$$
with VI, IX show $$thesis$$
qed
qed

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

lemma indseq_exun:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$

shows $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$proof
note A3
moreover
from A1, A2 have $$\exists ! a.\ a: succ(0) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in 0.\ a(succ(k)) = f(a(k)) )$$ using indseq_exun0
moreover
from A1, A2 have $$\forall k \in nat.\$$ $$( \exists ! a.\ a: succ(k) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall i\in k.\ a(succ(i)) = f(a(i)) )) \longrightarrow$$ $$( \exists ! a.\ a: succ(succ(k)) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall i\in succ(k).\ a(succ(i)) = f(a(i)) ) )$$ using indseq_exun_ind
ultimately show $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in n.\ a(succ(k)) = f(a(k)) )$$ by (rule ind_on_nat )
qed

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

theorem fin_indseq_props:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$ and A4: $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$proof
let $$i = \text{The } a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall k\in n.\ a(succ(k)) = f(a(k)) )$$
from A1, A2, A3 have $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in n.\ a(succ(k)) = f(a(k)) )$$ using indseq_exun
then have $$i: succ(n) \rightarrow X \wedge i(0) = x \wedge ( \forall k\in n.\ i(succ(k)) = f(i(k)) )$$ by (rule theI )
moreover
from A1, A4 have $$a = i$$ using InductiveSequenceN_def, func1_1_L1
ultimately show $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
qed

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.

lemma is_fin_indseq:

assumes $$n \in nat$$, $$f: X\rightarrow X$$, $$x\in X$$ and $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$

shows $$a = \text{InductiveSequenceN}(x,f,n)$$proof
let $$b = \text{InductiveSequenceN}(x,f,n)$$
from assms(1,2,3) have $$b: succ(n) \rightarrow X$$, $$b(0) = x$$, $$\forall k\in n.\ b(succ(k)) = f(b(k))$$ using fin_indseq_props
with assms show $$thesis$$ using indseq_exun
qed

A corollary about the domain of a finite inductive sequence.

corollary fin_indseq_domain:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$

shows $$domain( \text{InductiveSequenceN}(x,f,n)) = succ(n)$$proof
from assms have $$\text{InductiveSequenceN}(x,f,n) : succ(n) \rightarrow X$$ using fin_indseq_props
then show $$thesis$$ using func1_1_L1
qed

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.

lemma indseq_consistent:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$i \in nat$$, $$j \in nat$$ and A4: $$i \subseteq j$$

shows $$\text{restrict}( \text{InductiveSequenceN}(x,f,j),succ(i)) = \text{InductiveSequenceN}(x,f,i)$$proof
let $$a = \text{InductiveSequenceN}(x,f,j)$$
let $$b = \text{restrict}( \text{InductiveSequenceN}(x,f,j),succ(i))$$
let $$c = \text{InductiveSequenceN}(x,f,i)$$
from A1, A2, A3 have $$a: succ(j) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in j.\ a(succ(k)) = f(a(k))$$ using fin_indseq_props
with A3, A4 have $$b: succ(i) \rightarrow X \wedge b(0) = x \wedge ( \forall k\in i.\ b(succ(k)) = f(b(k)))$$ using succ_subset, restrict_type2, empty_in_every_succ, restrict, succ_ineq
moreover
from A1, A2, A3 have $$c: succ(i) \rightarrow X \wedge c(0) = x \wedge ( \forall k\in i.\ c(succ(k)) = f(c(k)))$$ using fin_indseq_props
moreover
from A1, A2, A3 have $$\exists ! a.\ a: succ(i) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in i.\ a(succ(k)) = f(a(k)) )$$ using indseq_exun
ultimately show $$b = c$$
qed

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

lemma indseq_subsets:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$i \in nat$$, $$j \in nat$$ and A4: $$a = \text{InductiveSequenceN}(x,f,i)$$, $$b = \text{InductiveSequenceN}(x,f,j)$$

shows $$a \subseteq b \vee b \subseteq a$$proof
from A3 have $$i\subseteq j \vee j\subseteq i$$ using nat_incl_total
moreover {
assume $$i\subseteq j$$
with A1, A2, A3, A4 have $$\text{restrict}(b,succ(i)) = a$$ using indseq_consistent
moreover
have $$\text{restrict}(b,succ(i)) \subseteq b$$ using restrict_subset
ultimately have $$a \subseteq b \vee b \subseteq a$$
} moreover {
assume $$j\subseteq i$$
with A1, A2, A3, A4 have $$\text{restrict}(a,succ(j)) = b$$ using indseq_consistent
moreover
have $$\text{restrict}(a,succ(j)) \subseteq a$$ using restrict_subset
ultimately have $$a \subseteq b \vee b \subseteq a$$
} ultimately show $$a \subseteq b \vee b \subseteq a$$
qed

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

lemma indseq_empty:

assumes $$f: X\rightarrow X$$, $$x\in X$$

shows $$\text{InductiveSequenceN}(x,f,0):\{0\}\rightarrow X$$, $$\text{InductiveSequenceN}(x,f,0) = \{\langle 0,x\rangle \}$$proof
let $$a = \text{InductiveSequenceN}(x,f,0)$$
from assms have $$a:succ(0)\rightarrow X$$ and $$a(0) = x$$ using fin_indseq_props(1,2)
moreover
have $$succ(0) = \{0\}$$
ultimately show $$a:\{0\}\rightarrow X$$
then have $$a = \{\langle 0,a(0)\rangle \}$$ using func_singleton_pair
with $$a(0) = x$$ show $$a = \{\langle 0,x\rangle \}$$
qed

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

lemma indseq_tail:

assumes $$n \in nat$$, $$f: X\rightarrow X$$, $$x\in X$$

shows $$\text{Tail}( \text{InductiveSequenceN}(x,f,succ(n))) = \text{InductiveSequenceN}(f(x),f,n)$$proof
let $$a = \text{Tail}( \text{InductiveSequenceN}(x,f,succ(n)))$$
from assms(2,3) have $$f(x)\in X$$ using apply_funtype
have $$a: succ(n) \rightarrow X$$, $$a(0) = f(x)$$ and $$\forall k\in n.\ a(succ(k)) = f(a(k))$$proof
let $$b = \text{InductiveSequenceN}(x,f,succ(n))$$
from assms have I: $$succ(n)\in nat$$, $$b: succ(succ(n)) \rightarrow X$$ using fin_indseq_props(1)
then show $$\text{Tail}(b):succ(n)\rightarrow X$$ using tail_props
from assms(1), I have II: $$\text{Tail}(b)(0) = b(succ(0))$$ using tail_props, empty_in_every_succ
from assms, $$succ(n)\in nat$$ have $$b(succ(0)) = f(b(0))$$ using fin_indseq_props(3), empty_in_every_succ
moreover
from assms(2,3), $$succ(n)\in nat$$ have $$b(0) = x$$ using fin_indseq_props(2)
ultimately have $$b(succ(0)) = f(x)$$
with II show $$a(0) = f(x)$$
{
fix $$k$$
assume $$k\in n$$
from I have III: $$\forall k\in succ(n).\ a(k) = b(succ(k))$$ using tail_props
with assms(1), $$k\in n$$ have $$a(succ(k)) = b(succ(succ(k)))$$ using succ_ineq
with assms, $$k\in n$$, III have $$a(succ(k)) = f(a(k))$$ using succ_ineq, fin_indseq_props(3)
}
then show $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
qed
with assms(1,2), $$f(x)\in X$$ show $$thesis$$ by (rule is_fin_indseq )
qed

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.

theorem indseq_seq:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$

shows $$\text{InductiveSequence}(x,f) : nat \rightarrow X$$proof
let $$S = \{ \text{InductiveSequenceN}(x,f,n).\ n \in nat\}$$
{
fix $$a$$
assume $$a\in S$$
then obtain $$n$$ where $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$
with A1, A2 have $$a : succ(n)\rightarrow X$$ using fin_indseq_props
then have $$\exists A B.\ a:A\rightarrow B$$
}
then have $$\forall a \in S.\ \exists A B.\ a:A\rightarrow B$$
moreover {
fix $$a$$ $$b$$
assume $$a\in S$$, $$b\in S$$
then obtain $$i$$ $$j$$ where $$i\in nat$$, $$j\in nat$$ and $$a = \text{InductiveSequenceN}(x,f,i)$$, $$b = \text{InductiveSequenceN}(x,f,j)$$
with A1, A2 have $$a\subseteq b \vee b\subseteq a$$ using indseq_subsets
}
then have $$\forall a\in S.\ \forall b\in S.\ a\subseteq b \vee b\subseteq a$$
ultimately have $$\bigcup S : domain(\bigcup S) \rightarrow \text{range}(\bigcup S)$$ using fun_Union
with A1, A2 have I: $$\bigcup S : nat \rightarrow \text{range}(\bigcup S)$$ using domain_UN, fin_indseq_domain, nat_union_succ
moreover {
fix $$k$$
assume A3: $$k \in nat$$
let $$y = (\bigcup S)(k)$$
note I, A3
moreover
have $$y = (\bigcup S)(k)$$
ultimately have $$\langle k,y\rangle \in (\bigcup S)$$ by (rule func1_1_L5A )
then obtain $$n$$ where $$n \in nat$$ and II: $$\langle k,y\rangle \in \text{InductiveSequenceN}(x,f,n)$$
with A1, A2 have $$\text{InductiveSequenceN}(x,f,n): succ(n) \rightarrow X$$ using fin_indseq_props
with II have $$y \in X$$ using func1_1_L5
}
then have $$\forall k \in nat.\ (\bigcup S)(k) \in X$$
ultimately have $$\bigcup S : nat \rightarrow X$$ using func1_1_L1A
then show $$\text{InductiveSequence}(x,f) : nat \rightarrow X$$ using InductiveSequence_def
qed

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

lemma indseq_restr_eq:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$

shows $$\text{restrict}( \text{InductiveSequence}(x,f),succ(n)) = \text{InductiveSequenceN}(x,f,n)$$proof
let $$a = \text{InductiveSequence}(x,f)$$
let $$b = \text{InductiveSequenceN}(x,f,n)$$
let $$S = \{ \text{InductiveSequenceN}(x,f,n).\ n \in nat\}$$
from A1, A2, A3 have I: $$a : nat \rightarrow X$$ and $$succ(n) \subseteq nat$$ using indseq_seq, succnat_subset_nat
then have $$\text{restrict}(a,succ(n)) : succ(n) \rightarrow X$$ using restrict_type2
moreover
from A1, A2, A3 have $$b : succ(n) \rightarrow X$$ using fin_indseq_props
moreover {
fix $$k$$
assume A4: $$k \in succ(n)$$
from A1, A2, A3, I have $$\bigcup S : nat \rightarrow X$$, $$b \in S$$, $$b : succ(n) \rightarrow X$$ using InductiveSequence_def, fin_indseq_props
with A4 have $$\text{restrict}(a,succ(n))(k) = b(k)$$ using fun_Union_apply, InductiveSequence_def, restrict_if
}
then have $$\forall k \in succ(n).\ \text{restrict}(a,succ(n))(k) = b(k)$$
ultimately show $$thesis$$ by (rule func_eq )
qed

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

theorem indseq_valat0:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$

shows $$\text{InductiveSequence}(x,f)(0) = x$$proof
let $$a = \text{InductiveSequence}(x,f)$$
let $$b = \text{InductiveSequenceN}(x,f,0)$$
have T: $$0\in nat$$, $$0 \in succ(0)$$
with A1, A2 have $$b(0) = x$$ using fin_indseq_props
moreover
from T have $$\text{restrict}(a,succ(0))(0) = a(0)$$ using restrict_if
moreover
from A1, A2, T have $$\text{restrict}(a,succ(0)) = b$$ using indseq_restr_eq
ultimately show $$a(0) = x$$
qed

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

theorem indseq_vals:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$n \in nat$$

shows $$\text{InductiveSequence}(x,f)(succ(n)) = f( \text{InductiveSequence}(x,f)(n))$$proof
let $$a = \text{InductiveSequence}(x,f)$$
let $$b = \text{InductiveSequenceN}(x,f,succ(n))$$
from A3 have T: $$succ(n) \in succ(succ(n))$$, $$succ(succ(n)) \in nat$$, $$n \in succ(succ(n))$$
then have $$a(succ(n)) = \text{restrict}(a,succ(succ(n)))(succ(n))$$ using restrict_if
also
from A1, A2, T have $$\ldots = f(\text{restrict}(a,succ(succ(n)))(n))$$ using indseq_restr_eq, fin_indseq_props
also
from T have $$\ldots = f(a(n))$$ using restrict_if
finally show $$a(succ(n)) = f(a(n))$$
qed

### Images of inductive sequences

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.

theorem ind_seq_image:

assumes A1: $$f: X\rightarrow X$$ and A2: $$x\in X$$ and A3: $$A = \text{InductiveSequence}(x,f)(nat)$$

shows $$x\in A$$ and $$\forall y\in A.\ f(y) \in A$$proof
let $$a = \text{InductiveSequence}(x,f)$$
from A1, A2 have $$a : nat \rightarrow X$$ using indseq_seq
with A3 have I: $$A = \{a(n).\ n \in nat\}$$ using func_imagedef
hence $$a(0) \in A$$
with A1, A2 show $$x\in A$$ using indseq_valat0
{
fix $$y$$
assume $$y\in A$$
with I obtain $$n$$ where II: $$n \in nat$$ and III: $$y = a(n)$$
with A1, A2 have $$a(succ(n)) = f(y)$$ using indseq_vals
moreover
from I, II have $$a(succ(n)) \in A$$
ultimately have $$f(y) \in A$$
}
then show $$\forall y\in A.\ f(y) \in A$$
qed

### Subsets generated by a binary operation

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.

theorem binop_gen_set:

assumes A1: $$f: X\times Y \rightarrow X$$ and A2: $$x\in X$$, $$y\in Y$$ and A3: $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(f,y))$$

shows $$a : nat \rightarrow X$$, $$a(nat) \in Pow(X)$$, $$x \in a(nat)$$, $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$proof
let $$g = \text{Fix2ndVar}(f,y)$$
from A1, A2 have I: $$g : X\rightarrow X$$ using fix_2nd_var_fun
with A2, A3 show $$a : nat \rightarrow X$$ using indseq_seq
then show $$a(nat) \in Pow(X)$$ using func1_1_L6
from A2, A3, I show $$x \in a(nat)$$ using ind_seq_image
from A2, A3, I have $$g : X\rightarrow X$$, $$x\in X$$, $$a(nat) = \text{InductiveSequence}(x,g)(nat)$$
then show $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$ by (rule ind_seq_image )
qed

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

lemma binop_gen_set_ex:

assumes A1: $$f: X\times Y \rightarrow X$$ and A2: $$x\in X$$, $$y\in Y$$

shows $$\{A \in Pow(X).\ x\in A \wedge (\forall z \in A.\ f\langle z,y\rangle \in A) \} \neq 0$$proof
let $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(f,y))$$
let $$A = a(nat)$$
from A1, A2 have I: $$A \in Pow(X)$$ and $$x \in A$$ using binop_gen_set
moreover {
fix $$z$$
assume T: $$z\in A$$
with A1, A2 have $$\text{Fix2ndVar}(f,y)(z) \in A$$ using binop_gen_set
moreover
from I, T have $$z \in X$$
with A1, A2 have $$\text{Fix2ndVar}(f,y)(z) = f\langle z,y\rangle$$ using fix_var_val
ultimately have $$f\langle z,y\rangle \in A$$
}
then have $$\forall z \in A.\ f\langle z,y\rangle \in A$$
ultimately show $$thesis$$
qed

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

theorem binop_gen_set1:

assumes A1: $$f: X\times Y \rightarrow X$$ and A2: $$X_1 \subseteq X$$ and A3: $$x\in X_1$$, $$y\in Y$$ and A4: $$\forall t\in X_1.\ f\langle t,y\rangle \in X_1$$ and A5: $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y))$$

shows $$a : nat \rightarrow X_1$$, $$a(nat) \in Pow(X_1)$$, $$x \in a(nat)$$, $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$, $$\forall z \in a(nat).\ f\langle z,y\rangle \in a(nat)$$proof
let $$h = \text{restrict}(f,X_1\times Y)$$
let $$g = \text{Fix2ndVar}(h,y)$$
from A2 have $$X_1\times Y \subseteq X\times Y$$
with A1 have I: $$h : X_1\times Y \rightarrow X$$ using restrict_type2
with A3 have II: $$g: X_1 \rightarrow X$$ using fix_2nd_var_fun
from A3, A4, I have $$\forall t\in X_1.\ g(t) \in X_1$$ using restrict, fix_var_val
with II have III: $$g : X_1 \rightarrow X_1$$ using func1_1_L1A
with A3, A5 show $$a : nat \rightarrow X_1$$ using indseq_seq
then show IV: $$a(nat) \in Pow(X_1)$$ using func1_1_L6
from A3, A5, III show $$x \in a(nat)$$ using ind_seq_image
from A3, A5, III have $$g : X_1 \rightarrow X_1$$, $$x\in X_1$$, $$a(nat) = \text{InductiveSequence}(x,g)(nat)$$
then have $$\forall z \in a(nat).\ \text{Fix2ndVar}(h,y)(z) \in a(nat)$$ by (rule ind_seq_image )
moreover {
fix $$z$$
assume $$z \in a(nat)$$
with IV have $$z \in X_1$$
with A1, A2, A3 have $$g(z) = \text{Fix2ndVar}(f,y)(z)$$ using fix_2nd_var_restr_comm, restrict
}
then have $$\forall z \in a(nat).\ g(z) = \text{Fix2ndVar}(f,y)(z)$$
ultimately show $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$
moreover {
fix $$z$$
assume $$z \in a(nat)$$
with A2, IV have $$z\in X$$
with A1, A3 have $$\text{Fix2ndVar}(f,y)(z) = f\langle z,y\rangle$$ using fix_var_val
}
then have $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) = f\langle z,y\rangle$$
ultimately show $$\forall z \in a(nat).\ f\langle z,y\rangle \in a(nat)$$
qed

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$$.

lemma binop_gen_set_ex1:

assumes A1: $$f: X\times Y \rightarrow X$$ and A2: $$X_1 \subseteq X$$ and A3: $$x\in X_1$$, $$y\in Y$$ and A4: $$\forall t\in X_1.\ f\langle t,y\rangle \in X_1$$

shows $$\{A \in Pow(X_1).\ x\in A \wedge (\forall z \in A.\ f\langle z,y\rangle \in A) \} \neq 0$$proof
let $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y))$$
let $$A = a(nat)$$
from A1, A2, A3, A4 have $$A \in Pow(X_1)$$, $$x \in A$$, $$\forall z \in A.\ f\langle z,y\rangle \in A$$ using binop_gen_set1
thus $$thesis$$
qed

### Inductive sequences with changing generating function

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$$.

Definition

$$\text{StateTransfFunNMeta}(F,n,s) \equiv$$ $$\text{if }(\text{snd}(s) \in n)\text{ then }\langle F(\text{snd}(s))(\text{fst}(s)), succ(\text{snd}(s))\rangle \text{ else }s$$

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

Definition

$$\text{StateTransfFunN}(X,F,n) \equiv \{\langle s, \text{StateTransfFunNMeta}(F,n,s)\rangle .\ s \in X\times succ(n)\}$$

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

Definition

$$\text{StatesSeq}(x,X,F,n) \equiv$$ $$\text{InductiveSequenceN}(\langle x,0\rangle , \text{StateTransfFunN}(X,F,n),n)$$

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

Definition

$$\text{InductiveSeqVarFN}(x,X,F,n) \equiv \{\langle k,\text{fst}( \text{StatesSeq}(x,X,F,n)(k))\rangle .\ k \in succ(n)\}$$

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

lemma state_trans_fun:

assumes A1: $$n \in nat$$ and A2: $$F: n \rightarrow (X\rightarrow X)$$

shows $$\text{StateTransfFunN}(X,F,n): X\times succ(n) \rightarrow X\times succ(n)$$proof
{
fix $$s$$
assume A3: $$s \in X\times succ(n)$$
let $$x = \text{fst}(s)$$
let $$k = \text{snd}(s)$$
let $$S = \text{StateTransfFunNMeta}(F,n,s)$$
from A3 have T: $$x \in X$$, $$k \in succ(n)$$ and $$\langle x,k\rangle = s$$
{
assume A4: $$k \in n$$
with A1 have $$succ(k) \in succ(n)$$ using succ_ineq
with A2, T, A4 have $$S \in X\times succ(n)$$ using apply_funtype, StateTransfFunNMeta_def
}
with A2, A3, T have $$S \in X\times succ(n)$$ using apply_funtype, StateTransfFunNMeta_def
}
then have $$\forall s \in X\times succ(n).\ \text{StateTransfFunNMeta}(F,n,s) \in X\times succ(n)$$
then have $$\{\langle s, \text{StateTransfFunNMeta}(F,n,s)\rangle .\ s \in X\times succ(n)\} : X\times succ(n) \rightarrow X\times succ(n)$$ by (rule ZF_fun_from_total )
then show $$\text{StateTransfFunN}(X,F,n): X\times succ(n) \rightarrow X\times succ(n)$$ using StateTransfFunN_def
qed

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.

lemma states_seq_props:

assumes A1: $$n \in nat$$ and A2: $$F: n \rightarrow (X\rightarrow X)$$ and A3: $$x\in X$$ and A4: $$b = \text{StatesSeq}(x,X,F,n)$$

shows $$b : succ(n) \rightarrow X\times succ(n)$$, $$b(0) = \langle x,0\rangle$$, $$\forall k \in succ(n).\ \text{snd}(b(k)) = k$$, $$\forall k\in n.\ b(succ(k)) = \langle F(k)(\text{fst}(b(k))), succ(k)\rangle$$proof
let $$f = \text{StateTransfFunN}(X,F,n)$$
from A1, A2 have I: $$f : X\times succ(n) \rightarrow X\times succ(n)$$ using state_trans_fun
moreover
from A1, A3 have II: $$\langle x,0\rangle \in X\times succ(n)$$ using empty_in_every_succ
moreover
note A1
moreover
from A4 have III: $$b = \text{InductiveSequenceN}(\langle x,0\rangle ,f,n)$$ using StatesSeq_def
ultimately show IV: $$b : succ(n) \rightarrow X\times succ(n)$$ by (rule fin_indseq_props )
from I, II, A1, III show V: $$b(0) = \langle x,0\rangle$$ by (rule fin_indseq_props )
from I, II, A1, III have VI: $$\forall k\in n.\ b(succ(k)) = f(b(k))$$ by (rule fin_indseq_props )
{
fix $$k$$
note I
moreover
assume A5: $$k \in n$$
hence $$k \in succ(n)$$
with IV have $$b(k) \in X\times succ(n)$$ using apply_funtype
moreover
have $$f = \{\langle s, \text{StateTransfFunNMeta}(F,n,s)\rangle .\ s \in X\times succ(n)\}$$ using StateTransfFunN_def
ultimately have $$f(b(k)) = \text{StateTransfFunNMeta}(F,n,b(k))$$ by (rule ZF_fun_from_tot_val )
}
then have VII: $$\forall k \in n.\ f(b(k)) = \text{StateTransfFunNMeta}(F,n,b(k))$$
{
fix $$k$$
assume A5: $$k \in succ(n)$$
note A1, A5
moreover
from V have $$\text{snd}(b(0)) = 0$$
moreover
from VI, VII have $$\forall j\in n.\ \text{snd}(b(j)) = j \longrightarrow \text{snd}(b(succ(j))) = succ(j)$$ using StateTransfFunNMeta_def
ultimately have $$\text{snd}(b(k)) = k$$ by (rule fin_nat_ind )
}
then show $$\forall k \in succ(n).\ \text{snd}(b(k)) = k$$
with VI, VII show $$\forall k\in n.\ b(succ(k)) = \langle F(k)(\text{fst}(b(k))), succ(k)\rangle$$ using StateTransfFunNMeta_def
qed

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

theorem fin_indseq_var_f_props:

assumes A1: $$n \in nat$$ and A2: $$x\in X$$ and A3: $$F: n \rightarrow (X\rightarrow X)$$ and A4: $$a = \text{InductiveSeqVarFN}(x,X,F,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = F(k)(a(k))$$proof
let $$f = \text{StateTransfFunN}(X,F,n)$$
let $$b = \text{StatesSeq}(x,X,F,n)$$
from A1, A2, A3 have $$b : succ(n) \rightarrow X\times succ(n)$$ using states_seq_props
then have $$\forall k \in succ(n).\ b(k) \in X\times succ(n)$$ using apply_funtype
hence $$\forall k \in succ(n).\ \text{fst}(b(k)) \in X$$
then have I: $$\{\langle k,\text{fst}(b(k))\rangle .\ k \in succ(n)\} : succ(n) \rightarrow X$$ by (rule ZF_fun_from_total )
with A4 show II: $$a: succ(n) \rightarrow X$$ using InductiveSeqVarFN_def
moreover
from A1 have $$0 \in succ(n)$$ using empty_in_every_succ
moreover
from A4 have III: $$a = \{\langle k,\text{fst}( \text{StatesSeq}(x,X,F,n)(k))\rangle .\ k \in succ(n)\}$$ using InductiveSeqVarFN_def
ultimately have $$a(0) = \text{fst}(b(0))$$ by (rule ZF_fun_from_tot_val )
with A1, A2, A3 show $$a(0) = x$$ using states_seq_props
{
fix $$k$$
assume A5: $$k \in n$$
with A1 have T1: $$succ(k) \in succ(n)$$ and T2: $$k \in succ(n)$$ using succ_ineq
from II, T1, III have $$a(succ(k)) = \text{fst}(b(succ(k)))$$ by (rule ZF_fun_from_tot_val )
with A1, A2, A3, A5 have $$a(succ(k)) = F(k)(\text{fst}(b(k)))$$ using states_seq_props
moreover
from II, T2, III have $$a(k) = \text{fst}(b(k))$$ by (rule ZF_fun_from_tot_val )
ultimately have $$a(succ(k)) = F(k)(a(k))$$
}
then show $$\forall k\in n.\ a(succ(k)) = F(k)(a(k))$$
qed

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

lemma fin_indseq_var_f_uniq:

assumes $$n\in nat$$, $$x\in X$$, $$F: n \rightarrow (X\rightarrow X)$$ and $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = (F(k))(a(k))$$ and $$b: succ(n) \rightarrow X$$, $$b(0) = x$$, $$\forall k\in n.\ b(succ(k)) = (F(k))(b(k))$$

shows $$a=b$$proof
have $$\forall k\in succ(n).\ a(k) = b(k)$$proof
let $$A = \{i\in succ(succ(n)).\ \forall k\in i.\ a(k) = b(k)\}$$
let $$m = \text{Maximum}(Le,A)$$
from assms(1) have I: $$succ(succ(n)) \in nat$$, $$A\subseteq succ(succ(n))$$
moreover
from assms(1,5,8) have $$succ(0) \in A$$ using empty_in_every_succ, succ_ineq
hence II: $$A\neq 0$$
ultimately have $$m\in A$$ by (rule nat_max_props )
moreover
have $$m = succ(n)$$proof
{
assume $$m \neq succ(n)$$
from I, II have III: $$\forall k\in A.\ k \leq m$$ by (rule nat_max_props )
have $$succ(m) \in A$$proof
from $$m \neq succ(n)$$, $$m\in A$$ have $$m\in succ(n)$$ using mem_succ_not_eq
from I, II have $$m \in nat$$ by (rule nat_max_props )
from $$succ(0) \in A$$, III have $$succ(0) \leq m$$
hence $$m \neq 0$$
with $$m \in nat$$ obtain $$k$$ where $$k\in nat$$, $$m = succ(k)$$ using Nat_ZF_1_L3
with assms(1), $$m\in succ(n)$$ have $$k\in n$$ using succ_mem
with assms(6,9), $$m = succ(k)$$, $$m\in A$$ have $$a(m) = b(m)$$ using succ_explained
with assms(1), $$m\in A$$, $$m\in succ(n)$$ show $$succ(m) \in A$$ using succ_explained, succ_ineq
qed
with III have $$succ(m) \leq m$$ by (rule property_holds )
hence $$False$$
}
thus $$thesis$$
qed
ultimately show $$thesis$$
qed
with assms(4,7) show $$a=b$$ by (rule func_eq )
qed

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.

theorem is_fin_indseq_var_f:

assumes $$n\in nat$$, $$x\in X$$, $$F: n \rightarrow (X\rightarrow X)$$ and $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = (F(k))(a(k))$$

shows $$a = \text{InductiveSeqVarFN}(x,X,F,n)$$proof
let $$b = \text{InductiveSeqVarFN}(x,X,F,n)$$
from assms(1,2,3) have $$b: succ(n) \rightarrow X$$, $$b(0) = x$$ and $$\forall k\in n.\ b(succ(k)) = F(k)(b(k))$$ using fin_indseq_var_f_props
with assms show $$thesis$$ by (rule fin_indseq_var_f_uniq )
qed

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.

lemma fin_indseq_var_f_restrict:

assumes A1: $$n \in nat$$, $$i \in nat$$, $$x\in X$$, $$F: n \rightarrow (X\rightarrow X)$$, $$G: i \rightarrow (X\rightarrow X)$$ and A2: $$i \subseteq n$$ and A3: $$\forall j\in i.\ G(j) = F(j)$$ and A4: $$k \in succ(i)$$

shows $$\text{InductiveSeqVarFN}(x,X,G,i)(k) = \text{InductiveSeqVarFN}(x,X,F,n)(k)$$proof
let $$a = \text{InductiveSeqVarFN}(x,X,F,n)$$
let $$b = \text{InductiveSeqVarFN}(x,X,G,i)$$
from A1, A4 have $$i \in nat$$, $$k \in succ(i)$$
moreover
from A1 have $$b(0) = a(0)$$ using fin_indseq_var_f_props
moreover
from A1, A2, A3 have $$\forall j\in i.\ b(j) = a(j) \longrightarrow b(succ(j)) = a(succ(j))$$ using fin_indseq_var_f_props
ultimately show $$b(k) = a(k)$$ by (rule fin_nat_ind )
qed

### The Pascal's triangle

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.

Definition

$$\text{BinomElem}(r,k) \equiv \text{if }k=0\text{ then }1\text{ else }r(pred(k)) +_\mathbb{N} r(k)$$

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

Definition

$$GenBinom \equiv \{\langle r,\{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}\rangle .\ r\in \text{NELists}(nat)\}$$

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.

lemma gen_binom_fun:

shows $$GenBinom: \text{NELists}(nat) \rightarrow \text{NELists}(nat)$$proof
{
fix $$r$$
assume $$r \in \text{NELists}(nat)$$
then obtain $$n$$ where $$n\in nat$$ and $$r:succ(n)\rightarrow nat$$ unfolding NELists_def
then have $$domain(r) = succ(n)$$ using func1_1_L1
let $$r_1 = \{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}$$
have $$\forall k\in succ(domain(r)).\ \text{BinomElem}(r,k) \in nat$$ unfolding BinomElem_def
then have $$r_1: succ(domain(r))\rightarrow nat$$ by (rule ZF_fun_from_total )
with $$n\in nat$$, $$domain(r) = succ(n)$$ have $$r_1\in \text{NELists}(nat)$$ unfolding NELists_def
}
then show $$thesis$$ using ZF_fun_from_total unfolding GenBinom_def
qed

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

lemma gen_binom_fun_val:

assumes $$n\in nat$$, $$r:succ(n)\rightarrow nat$$

shows $$GenBinom(r):succ(succ(n)) \rightarrow nat$$proof
let $$B = \{\langle r,\{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}\rangle .\ r\in \text{NELists}(nat)\}$$
let $$r_1 = \{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}$$
from assms have $$r\in \text{NELists}(nat)$$ unfolding NELists_def
then have $$B(r) = r_1$$ using ZF_fun_from_tot_val1
have $$\forall k\in succ(domain(r)).\ \text{BinomElem}(r,k) \in nat$$ unfolding BinomElem_def
then have $$r_1: succ(domain(r))\rightarrow nat$$ by (rule ZF_fun_from_total )
with assms(2), $$B(r) = r_1$$ show $$thesis$$ using func1_1_L1 unfolding GenBinom_def
qed

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.

Definition

$$PascalTriangle \equiv \text{InductiveSequence}(\{\langle 0,1\rangle \},GenBinom)$$

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.

lemma pascal_sequence:

shows $$\{\langle 0,1\rangle \} \in \text{NELists}(nat)$$ and $$PascalTriangle: nat \rightarrow \text{NELists}(nat)$$ using list_len1_singleton(2), gen_binom_fun, indseq_seq unfolding PascalTriangle_def

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

lemma binom_gen:

assumes $$n\in nat$$

shows $$PascalTriangle(succ(n)) = GenBinom(PascalTriangle(n))$$ using assms, pascal_sequence, gen_binom_fun, indseq_vals unfolding PascalTriangle_def

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

lemma pascal_row_list:

assumes $$n\in nat$$

shows $$PascalTriangle(n):succ(n)\rightarrow nat$$proof
from assms(1) have $$n\in nat$$ and $$PascalTriangle(0):succ(0)\rightarrow nat$$ using gen_binom_fun, pascal_sequence(1), indseq_valat0, list_len1_singleton(1) unfolding PascalTriangle_def
moreover
have $$\forall k\in nat.\ PascalTriangle(k):succ(k)\rightarrow nat \longrightarrow$$ $$PascalTriangle(succ(k)):succ(succ(k))\rightarrow nat$$proof
{
fix $$k$$
assume $$k\in nat$$ and $$PascalTriangle(k):succ(k)\rightarrow nat$$
then have $$PascalTriangle(succ(k)):succ(succ(k))\rightarrow nat$$ using gen_binom_fun_val, gen_binom_fun, pascal_sequence(1), indseq_vals unfolding NELists_def, PascalTriangle_def
}
thus $$thesis$$
qed
ultimately show $$thesis$$ by (rule ind_on_nat )
qed

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.

lemma pascal_val_beyond:

assumes $$n\in nat$$

shows $$(PascalTriangle(n))(succ(n)) = 0$$proof
from assms have $$domain(PascalTriangle(n)) = succ(n)$$ using pascal_row_list, func1_1_L1
then show $$thesis$$ using mem_self, apply_0
qed

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

lemma pascal_row_val:

assumes $$n\in nat$$, $$k\in succ(succ(n))$$

shows $$(PascalTriangle(succ(n)))(k) = \text{BinomElem}(PascalTriangle(n),k)$$proof
let $$B = \{\langle r,\{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}\rangle .\ r\in \text{NELists}(nat)\}$$
let $$r = PascalTriangle(n)$$
let $$B_r = \{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(succ(n))\}$$
from assms(1) have $$r \in \text{NELists}(nat)$$ and $$r : succ(n)\rightarrow nat$$ using pascal_sequence(2), apply_funtype, pascal_row_list
then have $$B(r) = B_r$$ using func1_1_L1, ZF_fun_from_tot_val1
moreover
from assms(1) have $$B(r) = PascalTriangle(succ(n))$$ using binom_gen unfolding GenBinom_def
moreover
from assms(2) have $$B_r(k) = \text{BinomElem}(r,k)$$ by (rule ZF_fun_from_tot_val1 )
ultimately show $$thesis$$
qed

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.

Definition

$${{n}\choose {k}} \equiv (PascalTriangle(n))(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.

lemma binom_zero_zero:

shows $${{0}\choose {0}} = 1$$ using gen_binom_fun, pascal_sequence(1), indseq_valat0, pair_val unfolding Binom_def, PascalTriangle_def

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

theorem binom_left_boundary:

assumes $$n\in nat$$

shows $${{n}\choose {0}} = 1$$proof
{
assume $$n\neq 0$$
with assms obtain $$k$$ where $$k\in nat$$ and $$n = succ(k)$$ using Nat_ZF_1_L3
then have $${{n}\choose {0}} = 1$$ using empty_in_every_succ, pascal_row_val unfolding BinomElem_def, Binom_def
}
then show $$thesis$$ using binom_zero_zero
qed

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.

theorem binom_prop:

assumes $$n\in nat$$, $$k \leq n +_\mathbb{N} 1$$, $$k\neq 0$$

shows $${{n +_\mathbb{N} 1}\choose {k}} = {{n}\choose {k -_\mathbb{N} 1}} +_\mathbb{N} {{n}\choose {k}}$$proof
let $$P = PascalTriangle$$
from assms(1,2) have $$k\in nat$$ and $$k \in succ(succ(n))$$ using le_in_nat, nat_mem_lt(2)
with assms(1) have $${{n +_\mathbb{N} 1}\choose {k}} = \text{BinomElem}(P(n),k)$$ unfolding Binom_def using pascal_row_val
also
from assms(3), $$k\in nat$$ have $$\text{BinomElem}(P(n),k) = (P(n))(k -_\mathbb{N} 1) +_\mathbb{N} (P(n))(k)$$ unfolding BinomElem_def using pred_minus_one
also
have $$(P(n))(k -_\mathbb{N} 1) +_\mathbb{N} (P(n))(k) = {{n}\choose {k -_\mathbb{N} 1}} +_\mathbb{N} {{n}\choose {k}}$$ unfolding Binom_def
finally show $$thesis$$
qed

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.

lemma binom_prop1:

assumes $$n\in nat$$

shows $${{n +_\mathbb{N} 1}\choose {n +_\mathbb{N} 1}} = {{n}\choose {n}}$$proof
let $$B = Binom$$
from assms have $$B(n,n) \in nat$$ using pascal_row_list, apply_funtype unfolding Binom_def
from assms have $$(PascalTriangle(n))(succ(n)) = 0$$ using pascal_val_beyond
moreover
from assms have $$succ(n) = n +_\mathbb{N} 1$$ using succ_add_one(1)
ultimately have $$B(n,n +_\mathbb{N} 1) = 0$$ unfolding Binom_def
with assms, $$B(n,n) \in nat$$ show $$thesis$$ using succ_add_one(2), binom_prop, add_subctract, add_0, add_commute
qed

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

theorem binom_right_boundary:

assumes $$n\in nat$$

shows $${{n}\choose {n}} = 1$$proof
from assms have $$n\in nat$$ and $${{0}\choose {0}} = 1$$ using binom_zero_zero
moreover
have $$\forall k\in nat.\ {{k}\choose {k}} = 1 \longrightarrow {{succ(k)}\choose {succ(k)}} = 1$$ using binom_prop1
ultimately show $$thesis$$ by (rule ind_on_nat )
qed
end
lemma func_singleton_pair:

assumes $$f : \{a\}\rightarrow X$$

shows $$f = \{\langle a, f(a)\rangle \}$$
lemma func1_1_L1B:

assumes $$f:X\rightarrow Y$$ and $$Y\subseteq Z$$

shows $$f:X\rightarrow Z$$
lemma empty_in_every_succ:

assumes $$n \in nat$$

shows $$0 \in succ(n)$$
lemma succ_ineq:

assumes $$n \in nat$$

shows $$\forall i \in n.\ succ(i) \in succ(n)$$
lemma indseq_restrict:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a: succ(succ(n))\rightarrow X \wedge a(0) = x \wedge (\forall k\in succ(n).\ a(succ(k)) = f(a(k)))$$ and $$a_r = \text{restrict}(a,succ(n))$$

shows $$a_r: succ(n) \rightarrow X \wedge a_r(0) = x \wedge ( \forall k\in n.\ a_r(succ(k)) = f(a_r(k)) )$$
lemma finseq_restr_eq:

assumes $$n \in nat$$ and $$a: succ(n) \rightarrow X$$, $$b: succ(n) \rightarrow X$$ and $$\text{restrict}(a,n) = \text{restrict}(b,n)$$ and $$a(n) = b(n)$$

shows $$a = b$$
lemma finseq_extend:

assumes $$a:n\rightarrow X$$, $$y\in X$$, $$b = a \cup \{\langle n,y\rangle \}$$

shows $$b: succ(n) \rightarrow X$$, $$\forall k\in n.\ b(k) = a(k)$$, $$b(n) = y$$
lemma indseq_exun0:

assumes $$f: X\rightarrow X$$ and $$x\in X$$

shows $$\exists ! a.\ a: succ(0) \rightarrow X \wedge a(0) = x \wedge ( \forall k\in 0.\ a(succ(k)) = f(a(k)) )$$
lemma indseq_exun_ind:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$

shows $$\exists ! a.\ a: succ(succ(n)) \rightarrow X \wedge a(0) = x \wedge$$ $$( \forall k\in succ(n).\ a(succ(k)) = f(a(k)) )$$
theorem ind_on_nat:

assumes $$n\in nat$$ and $$P(0)$$ and $$\forall k\in nat.\ P(k)\longrightarrow P(succ(k))$$

shows $$P(n)$$
lemma indseq_exun:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$

shows $$\exists ! a.\ a: succ(n) \rightarrow X \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$
Definition of InductiveSequenceN: $$\text{InductiveSequenceN}(x,f,n) \equiv$$ $$\text{The } a.\ a: succ(n) \rightarrow domain(f) \wedge a(0) = x \wedge (\forall k\in n.\ a(succ(k)) = f(a(k)))$$
lemma func1_1_L1:

assumes $$f:A\rightarrow C$$

shows $$domain(f) = A$$
theorem fin_indseq_props:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
lemma succ_subset:

assumes $$k \in nat$$, $$n \in nat$$ and $$k\subseteq n$$

shows $$succ(k) \subseteq succ(n)$$
lemma nat_incl_total:

assumes $$i \in nat$$, $$j \in nat$$

shows $$i \subseteq j \vee j \subseteq i$$
lemma indseq_consistent:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$i \in nat$$, $$j \in nat$$ and $$i \subseteq j$$

shows $$\text{restrict}( \text{InductiveSequenceN}(x,f,j),succ(i)) = \text{InductiveSequenceN}(x,f,i)$$
theorem fin_indseq_props:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
theorem fin_indseq_props:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
theorem tail_props:

assumes $$n \in nat$$ and $$a: succ(n) \rightarrow X$$

shows $$\text{Tail}(a) : n \rightarrow X$$, $$\forall k \in n.\ \text{Tail}(a)(k) = a(succ(k))$$
theorem fin_indseq_props:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
theorem fin_indseq_props:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$
lemma is_fin_indseq:

assumes $$n \in nat$$, $$f: X\rightarrow X$$, $$x\in X$$ and $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = f(a(k))$$

shows $$a = \text{InductiveSequenceN}(x,f,n)$$
lemma indseq_subsets:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$i \in nat$$, $$j \in nat$$ and $$a = \text{InductiveSequenceN}(x,f,i)$$, $$b = \text{InductiveSequenceN}(x,f,j)$$

shows $$a \subseteq b \vee b \subseteq a$$
corollary fin_indseq_domain:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$

shows $$domain( \text{InductiveSequenceN}(x,f,n)) = succ(n)$$
lemma nat_union_succ: shows $$nat = (\bigcup n \in nat.\ succ(n))$$
lemma func1_1_L5A:

assumes $$f:X\rightarrow Y$$, $$x\in X$$, $$y = f(x)$$

shows $$\langle x,y\rangle \in f$$, $$y \in \text{range}(f)$$
lemma func1_1_L5:

assumes $$\langle x,y\rangle \in f$$ and $$f:X\rightarrow Y$$

shows $$x\in X \wedge y\in Y$$
lemma func1_1_L1A:

assumes $$f:X\rightarrow Y$$ and $$\forall x\in X.\ f(x) \in Z$$

shows $$f:X\rightarrow Z$$
Definition of InductiveSequence: $$\text{InductiveSequence}(x,f) \equiv \bigcup n\in nat.\ \text{InductiveSequenceN}(x,f,n)$$
theorem indseq_seq:

assumes $$f: X\rightarrow X$$ and $$x\in X$$

shows $$\text{InductiveSequence}(x,f) : nat \rightarrow X$$
lemma succnat_subset_nat:

assumes $$n \in nat$$

shows $$succ(n) \subseteq nat$$
lemma fun_Union_apply:

assumes $$\bigcup F : X\rightarrow Y$$ and $$f\in F$$ and $$f:A\rightarrow B$$ and $$x\in A$$

shows $$(\bigcup F)(x) = f(x)$$
lemma func_eq:

assumes $$f: X\rightarrow Y$$, $$g: X\rightarrow Z$$ and $$\forall x\in X.\ f(x) = g(x)$$

shows $$f = g$$
lemma indseq_restr_eq:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$

shows $$\text{restrict}( \text{InductiveSequence}(x,f),succ(n)) = \text{InductiveSequenceN}(x,f,n)$$
lemma func_imagedef:

assumes $$f:X\rightarrow Y$$ and $$A\subseteq X$$

shows $$f(A) = \{f(x).\ x \in A\}$$
theorem indseq_valat0:

assumes $$f: X\rightarrow X$$ and $$x\in X$$

shows $$\text{InductiveSequence}(x,f)(0) = x$$
theorem indseq_vals:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$n \in nat$$

shows $$\text{InductiveSequence}(x,f)(succ(n)) = f( \text{InductiveSequence}(x,f)(n))$$
lemma fix_2nd_var_fun:

assumes $$f : X\times Y \rightarrow Z$$ and $$y\in Y$$

shows $$\text{Fix2ndVar}(f,y) : X \rightarrow Z$$
lemma func1_1_L6:

assumes $$f:X\rightarrow Y$$

shows $$f(B) \subseteq \text{range}(f)$$ and $$f(B) \subseteq Y$$
theorem ind_seq_image:

assumes $$f: X\rightarrow X$$ and $$x\in X$$ and $$A = \text{InductiveSequence}(x,f)(nat)$$

shows $$x\in A$$ and $$\forall y\in A.\ f(y) \in A$$
theorem binop_gen_set:

assumes $$f: X\times Y \rightarrow X$$ and $$x\in X$$, $$y\in Y$$ and $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(f,y))$$

shows $$a : nat \rightarrow X$$, $$a(nat) \in Pow(X)$$, $$x \in a(nat)$$, $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$
lemma fix_var_val:

assumes $$f : X\times Y \rightarrow Z$$ and $$x\in X$$, $$y\in Y$$

shows $$\text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle$$, $$\text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle$$
lemma fix_2nd_var_restr_comm:

assumes $$f : X\times Y \rightarrow Z$$ and $$y\in Y$$ and $$X_1 \subseteq X$$

shows $$\text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y) = \text{restrict}( \text{Fix2ndVar}(f,y),X_1)$$
theorem binop_gen_set1:

assumes $$f: X\times Y \rightarrow X$$ and $$X_1 \subseteq X$$ and $$x\in X_1$$, $$y\in Y$$ and $$\forall t\in X_1.\ f\langle t,y\rangle \in X_1$$ and $$a = \text{InductiveSequence}(x, \text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y))$$

shows $$a : nat \rightarrow X_1$$, $$a(nat) \in Pow(X_1)$$, $$x \in a(nat)$$, $$\forall z \in a(nat).\ \text{Fix2ndVar}(f,y)(z) \in a(nat)$$, $$\forall z \in a(nat).\ f\langle z,y\rangle \in a(nat)$$
Definition of StateTransfFunNMeta: $$\text{StateTransfFunNMeta}(F,n,s) \equiv$$ $$\text{if }(\text{snd}(s) \in n)\text{ then }\langle F(\text{snd}(s))(\text{fst}(s)), succ(\text{snd}(s))\rangle \text{ else }s$$
lemma ZF_fun_from_total:

assumes $$\forall x\in X.\ b(x) \in Y$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
Definition of StateTransfFunN: $$\text{StateTransfFunN}(X,F,n) \equiv \{\langle s, \text{StateTransfFunNMeta}(F,n,s)\rangle .\ s \in X\times succ(n)\}$$
lemma state_trans_fun:

assumes $$n \in nat$$ and $$F: n \rightarrow (X\rightarrow X)$$

shows $$\text{StateTransfFunN}(X,F,n): X\times succ(n) \rightarrow X\times succ(n)$$
Definition of StatesSeq: $$\text{StatesSeq}(x,X,F,n) \equiv$$ $$\text{InductiveSequenceN}(\langle x,0\rangle , \text{StateTransfFunN}(X,F,n),n)$$
lemma ZF_fun_from_tot_val:

assumes $$f:X\rightarrow Y$$, $$x\in X$$ and $$f = \{\langle x,b(x)\rangle .\ x\in X\}$$

shows $$f(x) = b(x)$$ and $$b(x)\in Y$$
lemma fin_nat_ind:

assumes $$n \in nat$$ and $$k \in succ(n)$$ and $$P(0)$$ and $$\forall j\in n.\ P(j) \longrightarrow P(succ(j))$$

shows $$P(k)$$
lemma states_seq_props:

assumes $$n \in nat$$ and $$F: n \rightarrow (X\rightarrow X)$$ and $$x\in X$$ and $$b = \text{StatesSeq}(x,X,F,n)$$

shows $$b : succ(n) \rightarrow X\times succ(n)$$, $$b(0) = \langle x,0\rangle$$, $$\forall k \in succ(n).\ \text{snd}(b(k)) = k$$, $$\forall k\in n.\ b(succ(k)) = \langle F(k)(\text{fst}(b(k))), succ(k)\rangle$$
Definition of InductiveSeqVarFN: $$\text{InductiveSeqVarFN}(x,X,F,n) \equiv \{\langle k,\text{fst}( \text{StatesSeq}(x,X,F,n)(k))\rangle .\ k \in succ(n)\}$$
lemma nat_max_props:

assumes $$n\in nat$$, $$A\subseteq n$$, $$A\neq 0$$

shows $$\text{Maximum}(Le,A) \in A$$, $$\text{Maximum}(Le,A) \in nat$$, $$\forall k\in A.\ k \leq \text{Maximum}(Le,A)$$
lemma mem_succ_not_eq:

assumes $$k\in succ(n)$$, $$k\neq n$$

shows $$k\in n$$
lemma Nat_ZF_1_L3:

assumes $$n \in nat$$ and $$n\neq 0$$

shows $$\exists k\in nat.\ n = succ(k)$$
lemma succ_mem:

assumes $$n \in nat$$, $$succ(k) \in succ(n)$$

shows $$k\in n$$
lemma succ_explained: shows $$succ(n) = n \cup \{n\}$$
lemma property_holds:

assumes $$\forall t\in X.\ \phi (t)$$ and $$x\in X$$

shows $$\phi (x)$$
theorem fin_indseq_var_f_props:

assumes $$n \in nat$$ and $$x\in X$$ and $$F: n \rightarrow (X\rightarrow X)$$ and $$a = \text{InductiveSeqVarFN}(x,X,F,n)$$

shows $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = F(k)(a(k))$$
lemma fin_indseq_var_f_uniq:

assumes $$n\in nat$$, $$x\in X$$, $$F: n \rightarrow (X\rightarrow X)$$ and $$a: succ(n) \rightarrow X$$, $$a(0) = x$$, $$\forall k\in n.\ a(succ(k)) = (F(k))(a(k))$$ and $$b: succ(n) \rightarrow X$$, $$b(0) = x$$, $$\forall k\in n.\ b(succ(k)) = (F(k))(b(k))$$

shows $$a=b$$
Definition of NELists: $$\text{NELists}(X) \equiv \bigcup n\in nat.\ (succ(n)\rightarrow X)$$
Definition of BinomElem: $$\text{BinomElem}(r,k) \equiv \text{if }k=0\text{ then }1\text{ else }r(pred(k)) +_\mathbb{N} r(k)$$
Definition of GenBinom: $$GenBinom \equiv \{\langle r,\{\langle k, \text{BinomElem}(r,k)\rangle .\ k\in succ(domain(r))\}\rangle .\ r\in \text{NELists}(nat)\}$$
lemma ZF_fun_from_tot_val1:

assumes $$x\in X$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x)$$
lemma list_len1_singleton:

assumes $$x\in X$$

shows $$\{\langle 0,x\rangle \} : 1 \rightarrow X$$ and $$\{\langle 0,x\rangle \} \in \text{NELists}(X)$$
lemma gen_binom_fun: shows $$GenBinom: \text{NELists}(nat) \rightarrow \text{NELists}(nat)$$
Definition of PascalTriangle: $$PascalTriangle \equiv \text{InductiveSequence}(\{\langle 0,1\rangle \},GenBinom)$$
lemma pascal_sequence: shows $$\{\langle 0,1\rangle \} \in \text{NELists}(nat)$$ and $$PascalTriangle: nat \rightarrow \text{NELists}(nat)$$
lemma pascal_sequence: shows $$\{\langle 0,1\rangle \} \in \text{NELists}(nat)$$ and $$PascalTriangle: nat \rightarrow \text{NELists}(nat)$$
lemma list_len1_singleton:

assumes $$x\in X$$

shows $$\{\langle 0,x\rangle \} : 1 \rightarrow X$$ and $$\{\langle 0,x\rangle \} \in \text{NELists}(X)$$
lemma gen_binom_fun_val:

assumes $$n\in nat$$, $$r:succ(n)\rightarrow nat$$

shows $$GenBinom(r):succ(succ(n)) \rightarrow nat$$
lemma pascal_row_list:

assumes $$n\in nat$$

shows $$PascalTriangle(n):succ(n)\rightarrow nat$$
lemma mem_self: shows $$x\notin x$$
lemma pascal_sequence: shows $$\{\langle 0,1\rangle \} \in \text{NELists}(nat)$$ and $$PascalTriangle: nat \rightarrow \text{NELists}(nat)$$
lemma binom_gen:

assumes $$n\in nat$$

shows $$PascalTriangle(succ(n)) = GenBinom(PascalTriangle(n))$$
lemma pair_val: shows $$\{\langle x,y\rangle \}(x) = y$$
Definition of Binom: $${{n}\choose {k}} \equiv (PascalTriangle(n))(k)$$
lemma pascal_row_val:

assumes $$n\in nat$$, $$k\in succ(succ(n))$$

shows $$(PascalTriangle(succ(n)))(k) = \text{BinomElem}(PascalTriangle(n),k)$$
lemma binom_zero_zero: shows $${{0}\choose {0}} = 1$$
lemma nat_mem_lt:

assumes $$n\in nat$$

shows $$k \lt n \longleftrightarrow k\in n$$ and $$k\leq n \longleftrightarrow k \in succ(n)$$
lemma pred_minus_one:

assumes $$n\in nat$$, $$n\neq 0$$

shows $$n -_\mathbb{N} 1 = pred(n)$$
lemma pascal_val_beyond:

assumes $$n\in nat$$

shows $$(PascalTriangle(n))(succ(n)) = 0$$

assumes $$n\in nat$$

shows $$n +_\mathbb{N} 1 = succ(n)$$ and $$n +_\mathbb{N} 1 \in nat$$

assumes $$n\in nat$$

shows $$n +_\mathbb{N} 1 = succ(n)$$ and $$n +_\mathbb{N} 1 \in nat$$
theorem binom_prop:

assumes $$n\in nat$$, $$k \leq n +_\mathbb{N} 1$$, $$k\neq 0$$

shows $${{n +_\mathbb{N} 1}\choose {k}} = {{n}\choose {k -_\mathbb{N} 1}} +_\mathbb{N} {{n}\choose {k}}$$
assumes $$m\in nat$$
shows $$(m +_\mathbb{N} n) -_\mathbb{N} n = m$$
assumes $$n\in nat$$
shows $${{n +_\mathbb{N} 1}\choose {n +_\mathbb{N} 1}} = {{n}\choose {n}}$$