Theory InductiveSeq_ZF
section ‹Inductive sequences›
theory InductiveSeq_ZF imports Nat_ZF_IML FiniteSeq_ZF FinOrd_ZF
begin
text‹In this theory we discuss sequences defined by conditions of the form
$a_0 = x,\ a_{n+1} = f(a_n)$ and similar.›
subsection‹Sequences defined by induction›
text‹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.›
text‹First we define a helper notion of the sequence defined inductively up to a
given natural number $n$.›
definition
"InductiveSequenceN(x,f,n) ≡
THE a. a: succ(n) → domain(f) ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"
text‹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
"InductiveSequence(x,f) ≡ ⋃n∈nat. InductiveSequenceN(x,f,n)"
text‹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→X" and A2: "x∈X"
shows
"∃! a. a: succ(0) → X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
proof
fix a b
assume A3:
"a: succ(0) → X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
"b: succ(0) → X ∧ b`(0) = x ∧ ( ∀k∈0. b`(succ(k)) = f`(b`(k)) )"
moreover have "succ(0) = {0}" by auto
ultimately have "a: {0} → X" "b: {0} → X" by auto
then have "a = {⟨0, a`(0)⟩}" "b = {⟨0, b`(0)⟩}" using func_singleton_pair
by auto
with A3 show "a=b" by simp
next
let ?a = "{⟨0,x⟩}"
have "?a : {0} → {x}" using singleton_fun by simp
moreover from A1 A2 have "{x} ⊆ X" by simp
ultimately have "?a : {0} → X"
using func1_1_L1B by blast
moreover have "{0} = succ(0)" by auto
ultimately have "?a : succ(0) → X" by simp
with A1 show
"∃ a. a: succ(0) → X ∧ a`(0) = x ∧ (∀k∈0. a`(succ(k)) = f`(a`(k)))"
using singleton_apply by auto
qed
text‹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→X" and A2: "x∈X" and A3: "n ∈ nat" and
A4: "a: succ(succ(n))→ X ∧ a`(0) = x ∧ (∀k∈succ(n). a`(succ(k)) = f`(a`(k)))"
and A5: "a⇩r = restrict(a,succ(n))"
shows
"a⇩r: succ(n) → X ∧ a⇩r`(0) = x ∧ ( ∀k∈n. a⇩r`(succ(k)) = f`(a⇩r`(k)) )"
proof -
from A3 have "succ(n) ⊆ succ(succ(n))" by auto
with A4 A5 have "a⇩r: succ(n) → X" using restrict_type2 by auto
moreover
from A3 have "0 ∈ succ(n)" using empty_in_every_succ by simp
with A4 A5 have "a⇩r`(0) = x" using restrict_if by simp
moreover from A3 A4 A5 have "∀k∈n. a⇩r`(succ(k)) = f`(a⇩r`(k))"
using succ_ineq restrict_if by auto
ultimately show ?thesis by simp
qed
text‹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→X" and A2: "x∈X" and A3: "n ∈ nat" and
A4: "∃! a. a: succ(n) → X ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"
shows
"∃! a. a: succ(succ(n)) → X ∧ a`(0) = x ∧
( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )"
proof
fix a b assume
A5: "a: succ(succ(n)) → X ∧ a`(0) = x ∧
( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )" and
A6: "b: succ(succ(n)) → X ∧ b`(0) = x ∧
( ∀k∈succ(n). b`(succ(k)) = f`(b`(k)) )"
show "a = b"
proof -
let ?a⇩r = "restrict(a,succ(n))"
let ?b⇩r = "restrict(b,succ(n))"
note A1 A2 A3 A5
moreover have "?a⇩r = restrict(a,succ(n))" by simp
ultimately have I:
"?a⇩r: succ(n) → X ∧ ?a⇩r`(0) = x ∧ ( ∀k∈n. ?a⇩r`(succ(k)) = f`(?a⇩r`(k)) )"
by (rule indseq_restrict)
note A1 A2 A3 A6
moreover have "?b⇩r = restrict(b,succ(n))" by simp
ultimately have
"?b⇩r: succ(n) → X ∧ ?b⇩r`(0) = x ∧ ( ∀k∈n. ?b⇩r`(succ(k)) = f`(?b⇩r`(k)) )"
by (rule indseq_restrict)
with A4 I have II: "?a⇩r = ?b⇩r" by blast
from A3 have "succ(n) ∈ nat" by simp
moreover from A5 A6 have
"a: succ(succ(n)) → X" and "b: succ(succ(n)) → X"
by auto
moreover note II
moreover
have T: "n ∈ succ(n)" by simp
then have "?a⇩r`(n) = a`(n)" and "?b⇩r`(n) = b`(n)" using restrict
by auto
with A5 A6 II T have "a`(succ(n)) = b`(succ(n))" by simp
ultimately show "a = b" by (rule finseq_restr_eq)
qed
next show
"∃ a. a: succ(succ(n)) → X ∧ a`(0) = x ∧
( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )"
proof -
from A4 obtain a where III: "a: succ(n) → X" and IV: "a`(0) = x"
and V: "∀k∈n. a`(succ(k)) = f`(a`(k))" by auto
let ?b = "a ∪ {⟨succ(n), f`(a`(n))⟩}"
from A1 III have
VI: "?b : succ(succ(n)) → X" and
VII: "∀k ∈ succ(n). ?b`(k) = a`(k)" and
VIII: "?b`(succ(n)) = f`(a`(n))"
using apply_funtype finseq_extend by auto
from A3 have "0 ∈ succ(n)" using empty_in_every_succ by simp
with IV VII have IX: "?b`(0) = x" by auto
{ fix k assume "k ∈ succ(n)"
then have "k∈n ∨ k = n" by auto
moreover
{ assume A7: "k ∈ n"
with A3 VII have "?b`(succ(k)) = a`(succ(k))"
using succ_ineq by auto
also from A7 V VII have "a`(succ(k)) = f`(?b`(k))" by simp
finally have "?b`(succ(k)) = f`(?b`(k))" by simp }
moreover
{ assume A8: "k = n"
with VIII have "?b`(succ(k)) = f`(a`(k))" by simp
with A8 VII VIII have "?b`(succ(k)) = f`(?b`(k))" by simp }
ultimately have "?b`(succ(k)) = f`(?b`(k))" by auto
} then have "∀k ∈ succ(n). ?b`(succ(k)) = f`(?b`(k))" by simp
with VI IX show ?thesis by auto
qed
qed
text‹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→X" and A2: "x∈X" and A3: "n ∈ nat"
shows
"∃! a. a: succ(n) → X ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"
proof -
note A3
moreover from A1 A2 have
"∃! a. a: succ(0) → X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
using indseq_exun0 by simp
moreover from A1 A2 have "∀k ∈ nat.
( ∃! a. a: succ(k) → X ∧ a`(0) = x ∧
( ∀i∈k. a`(succ(i)) = f`(a`(i)) )) ⟶
( ∃! a. a: succ(succ(k)) → X ∧ a`(0) = x ∧
( ∀i∈succ(k). a`(succ(i)) = f`(a`(i)) ) )"
using indseq_exun_ind by simp
ultimately show
"∃! a. a: succ(n) → X ∧ a`(0) = x ∧ ( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
by (rule ind_on_nat)
qed
text‹We are now ready to prove the main theorem about finite inductive sequences.›
theorem fin_indseq_props:
assumes A1: "f: X→X" and A2: "x∈X" and A3: "n ∈ nat" and
A4: "a = InductiveSequenceN(x,f,n)"
shows
"a: succ(n) → X"
"a`(0) = x"
"∀k∈n. a`(succ(k)) = f`(a`(k))"
proof -
let ?i = "THE a. a: succ(n) → X ∧ a`(0) = x ∧
( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
from A1 A2 A3 have
"∃! a. a: succ(n) → X ∧ a`(0) = x ∧ ( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
using indseq_exun by simp
then have
"?i: succ(n) → X ∧ ?i`(0) = x ∧ ( ∀k∈n. ?i`(succ(k)) = f`(?i`(k)) )"
by (rule theI)
moreover from A1 A4 have "a = ?i"
using InductiveSequenceN_def func1_1_L1 by simp
ultimately show
"a: succ(n) → X" "a`(0) = x" "∀k∈n. a`(succ(k)) = f`(a`(k))"
by auto
qed
text‹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 ∈ nat" "f: X→X" "x∈X" and
"a: succ(n) → X" "a`(0) = x" "∀k∈n. a`(succ(k)) = f`(a`(k))"
shows "a = InductiveSequenceN(x,f,n)"
proof -
let ?b = "InductiveSequenceN(x,f,n)"
from assms(1,2,3) have
"?b: succ(n) → X" "?b`(0) = x" "∀k∈n. ?b`(succ(k)) = f`(?b`(k))"
using fin_indseq_props by simp_all
with assms show ?thesis using indseq_exun by blast
qed
text‹A corollary about the domain of a finite inductive sequence.›
corollary fin_indseq_domain:
assumes A1: "f: X→X" and A2: "x∈X" and A3: "n ∈ nat"
shows "domain(InductiveSequenceN(x,f,n)) = succ(n)"
proof -
from assms have "InductiveSequenceN(x,f,n) : succ(n) → X"
using fin_indseq_props by simp
then show ?thesis using func1_1_L1 by simp
qed
text‹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→X" and A2: "x∈X" and
A3: "i ∈ nat" "j ∈ nat" and A4: "i ⊆ j"
shows
"restrict(InductiveSequenceN(x,f,j),succ(i)) = InductiveSequenceN(x,f,i)"
proof -
let ?a = "InductiveSequenceN(x,f,j)"
let ?b = "restrict(InductiveSequenceN(x,f,j),succ(i))"
let ?c = "InductiveSequenceN(x,f,i)"
from A1 A2 A3 have
"?a: succ(j) → X" "?a`(0) = x" "∀k∈j. ?a`(succ(k)) = f`(?a`(k))"
using fin_indseq_props by auto
with A3 A4 have
"?b: succ(i) → X ∧ ?b`(0) = x ∧ ( ∀k∈i. ?b`(succ(k)) = f`(?b`(k)))"
using succ_subset restrict_type2 empty_in_every_succ restrict succ_ineq
by auto
moreover from A1 A2 A3 have
"?c: succ(i) → X ∧ ?c`(0) = x ∧ ( ∀k∈i. ?c`(succ(k)) = f`(?c`(k)))"
using fin_indseq_props by simp
moreover from A1 A2 A3 have
"∃! a. a: succ(i) → X ∧ a`(0) = x ∧ ( ∀k∈i. a`(succ(k)) = f`(a`(k)) )"
using indseq_exun by simp
ultimately show "?b = ?c" by blast
qed
text‹For any two natural numbers one of the corresponding inductive sequences
is contained in the other.›
lemma indseq_subsets: assumes A1: "f: X→X" and A2: "x∈X" and
A3: "i ∈ nat" "j ∈ nat" and
A4: "a = InductiveSequenceN(x,f,i)" "b = InductiveSequenceN(x,f,j)"
shows "a ⊆ b ∨ b ⊆ a"
proof -
from A3 have "i⊆j ∨ j⊆i" using nat_incl_total by simp
moreover
{ assume "i⊆j"
with A1 A2 A3 A4 have "restrict(b,succ(i)) = a"
using indseq_consistent by simp
moreover have "restrict(b,succ(i)) ⊆ b"
using restrict_subset by simp
ultimately have "a ⊆ b ∨ b ⊆ a" by simp }
moreover
{ assume "j⊆i"
with A1 A2 A3 A4 have "restrict(a,succ(j)) = b"
using indseq_consistent by simp
moreover have "restrict(a,succ(j)) ⊆ a"
using restrict_subset by simp
ultimately have "a ⊆ b ∨ b ⊆ a" by simp }
ultimately show "a ⊆ b ∨ b ⊆ a" by auto
qed
text‹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→X" "x∈X"
shows
"InductiveSequenceN(x,f,0):{0}→X"
"InductiveSequenceN(x,f,0) = {⟨0,x⟩}"
proof -
let ?a = "InductiveSequenceN(x,f,0)"
from assms have "?a:succ(0)→X" and "?a`(0) = x"
using fin_indseq_props(1,2) by simp_all
moreover have "succ(0) = {0}" by auto
ultimately show "?a:{0}→X" by auto
then have "?a = {⟨0,?a`(0)⟩}" using func_singleton_pair
by simp
with‹?a`(0) = x› show "?a = {⟨0,x⟩}" by simp
qed
text‹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 ∈ nat" "f: X→X" "x∈X"
shows "Tail(InductiveSequenceN(x,f,succ(n))) = InductiveSequenceN(f`(x),f,n)"
proof -
let ?a = "Tail(InductiveSequenceN(x,f,succ(n)))"
from assms(2,3) have "f`(x)∈X" using apply_funtype by simp
have "?a: succ(n) → X" "?a`(0) = f`(x)" and
"∀k∈n. ?a`(succ(k)) = f`(?a`(k))"
proof -
let ?b = "InductiveSequenceN(x,f,succ(n))"
from assms have I: "succ(n)∈nat" "?b: succ(succ(n)) → X"
using fin_indseq_props(1) by simp_all
then show "Tail(?b):succ(n)→X" using tail_props by simp
from assms(1) I have II: "Tail(?b)`(0) = ?b`(succ(0))"
using tail_props empty_in_every_succ by blast
from assms ‹succ(n)∈nat› have "?b`(succ(0)) = f`(?b`(0))"
using fin_indseq_props(3) empty_in_every_succ by blast
moreover from assms(2,3) ‹succ(n)∈nat› have "?b`(0) = x"
using fin_indseq_props(2) by simp
ultimately have "?b`(succ(0)) = f`(x)" by simp
with II show "?a`(0) = f`(x)" by simp
{ fix k assume "k∈n"
from I have III: "∀k∈succ(n). ?a`(k) = ?b`(succ(k))"
using tail_props by blast
with assms(1) ‹k∈n› have "?a`(succ(k)) = ?b`(succ(succ(k)))"
using succ_ineq by blast
with assms ‹k∈n› III have "?a`(succ(k)) = f`(?a`(k))"
using succ_ineq fin_indseq_props(3) by simp
} then show "∀k∈n. ?a`(succ(k)) = f`(?a`(k))"
by simp
qed
with assms(1,2) ‹f`(x)∈X› show ?thesis by (rule is_fin_indseq)
qed
text‹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→X" and A2: "x∈X"
shows "InductiveSequence(x,f) : nat → X"
proof -
let ?S = "{InductiveSequenceN(x,f,n). n ∈ nat}"
{ fix a assume "a∈?S"
then obtain n where "n ∈ nat" and "a = InductiveSequenceN(x,f,n)"
by auto
with A1 A2 have "a : succ(n)→X" using fin_indseq_props
by simp
then have "∃A B. a:A→B" by auto
} then have "∀a ∈ ?S. ∃A B. a:A→B" by auto
moreover
{ fix a b assume "a∈?S" "b∈?S"
then obtain i j where "i∈nat" "j∈nat" and
"a = InductiveSequenceN(x,f,i)" "b = InductiveSequenceN(x,f,j)"
by auto
with A1 A2 have "a⊆b ∨ b⊆a" using indseq_subsets by simp
} then have "∀a∈?S. ∀b∈?S. a⊆b ∨ b⊆a" by auto
ultimately have "⋃?S : domain(⋃?S) → range(⋃?S)"
using fun_Union by simp
with A1 A2 have I: "⋃?S : nat → range(⋃?S)"
using domain_UN fin_indseq_domain nat_union_succ by simp
moreover
{ fix k assume A3: "k ∈ nat"
let ?y = "(⋃?S)`(k)"
note I A3
moreover have "?y = (⋃?S)`(k)" by simp
ultimately have "⟨k,?y⟩ ∈ (⋃?S)" by (rule func1_1_L5A)
then obtain n where "n ∈ nat" and II: "⟨k,?y⟩ ∈ InductiveSequenceN(x,f,n)"
by auto
with A1 A2 have "InductiveSequenceN(x,f,n): succ(n) → X"
using fin_indseq_props by simp
with II have "?y ∈ X" using func1_1_L5 by blast
} then have "∀k ∈ nat. (⋃?S)`(k) ∈ X" by simp
ultimately have "⋃?S : nat → X" using func1_1_L1A
by blast
then show "InductiveSequence(x,f) : nat → X"
using InductiveSequence_def by simp
qed
text‹Restriction of an inductive sequence to a finite domain
is the corresponding finite inductive sequence.›
lemma indseq_restr_eq:
assumes A1: "f: X→X" and A2: "x∈X" and A3: "n ∈ nat"
shows
"restrict(InductiveSequence(x,f),succ(n)) = InductiveSequenceN(x,f,n)"
proof -
let ?a = "InductiveSequence(x,f)"
let ?b = "InductiveSequenceN(x,f,n)"
let ?S = "{InductiveSequenceN(x,f,n). n ∈ nat}"
from A1 A2 A3 have
I: "?a : nat → X" and "succ(n) ⊆ nat"
using indseq_seq succnat_subset_nat by auto
then have "restrict(?a,succ(n)) : succ(n) → X"
using restrict_type2 by simp
moreover from A1 A2 A3 have "?b : succ(n) → X"
using fin_indseq_props by simp
moreover
{ fix k assume A4: "k ∈ succ(n)"
from A1 A2 A3 I have
"⋃?S : nat → X" "?b ∈ ?S" "?b : succ(n) → X"
using InductiveSequence_def fin_indseq_props by auto
with A4 have "restrict(?a,succ(n))`(k) = ?b`(k)"
using fun_Union_apply InductiveSequence_def restrict_if
by simp
} then have "∀k ∈ succ(n). restrict(?a,succ(n))`(k) = ?b`(k)"
by simp
ultimately show ?thesis by (rule func_eq)
qed
text‹The first element of the inductive sequence starting at $x$ and generated by $f$
is indeed $x$.›
theorem indseq_valat0: assumes A1: "f: X→X" and A2: "x∈X"
shows "InductiveSequence(x,f)`(0) = x"
proof -
let ?a = "InductiveSequence(x,f)"
let ?b = "InductiveSequenceN(x,f,0)"
have T: "0∈nat" "0 ∈ succ(0)" by auto
with A1 A2 have "?b`(0) = x"
using fin_indseq_props by simp
moreover from T have "restrict(?a,succ(0))`(0) = ?a`(0)"
using restrict_if by simp
moreover from A1 A2 T have
"restrict(?a,succ(0)) = ?b"
using indseq_restr_eq by simp
ultimately show "?a`(0) = x" by simp
qed
text‹An infinite inductive sequence satisfies the
inductive relation that defines it.›
theorem indseq_vals:
assumes A1: "f: X→X" and A2: "x∈X" and A3: "n ∈ nat"
shows
"InductiveSequence(x,f)`(succ(n)) = f`(InductiveSequence(x,f)`(n))"
proof -
let ?a = "InductiveSequence(x,f)"
let ?b = "InductiveSequenceN(x,f,succ(n))"
from A3 have T:
"succ(n) ∈ succ(succ(n))"
"succ(succ(n)) ∈ nat"
"n ∈ succ(succ(n))"
by auto
then have "?a`(succ(n)) = restrict(?a,succ(succ(n)))`(succ(n))"
using restrict_if by simp
also from A1 A2 T have "… = f`(restrict(?a,succ(succ(n)))`(n))"
using indseq_restr_eq fin_indseq_props by simp
also from T have "… = f`(?a`(n))" using restrict_if by simp
finally show "?a`(succ(n)) = f`(?a`(n))" by simp
qed
subsection‹Images of inductive sequences›
text‹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$.›
text‹The basic properties of orbits.›
theorem ind_seq_image: assumes A1: "f: X→X" and A2: "x∈X" and
A3: "A = InductiveSequence(x,f)``(nat)"
shows "x∈A" and "∀y∈A. f`(y) ∈ A"
proof -
let ?a = "InductiveSequence(x,f)"
from A1 A2 have "?a : nat → X" using indseq_seq
by simp
with A3 have I: "A = {?a`(n). n ∈ nat}" using func_imagedef
by auto hence "?a`(0) ∈ A" by auto
with A1 A2 show "x∈A" using indseq_valat0 by simp
{ fix y assume "y∈A"
with I obtain n where II: "n ∈ nat" and III: "y = ?a`(n)"
by auto
with A1 A2 have "?a`(succ(n)) = f`(y)"
using indseq_vals by simp
moreover from I II have "?a`(succ(n)) ∈ A" by auto
ultimately have "f`(y) ∈ A" by simp
} then show "∀y∈A. f`(y) ∈ A" by simp
qed
subsection‹Subsets generated by a binary operation›
text‹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.›
text‹Basic propertes of sets generated by binary operations.›
theorem binop_gen_set:
assumes A1: "f: X×Y → X" and A2: "x∈X" "y∈Y" and
A3: "a = InductiveSequence(x,Fix2ndVar(f,y))"
shows
"a : nat → X"
"a``(nat) ∈ Pow(X)"
"x ∈ a``(nat)"
"∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
proof -
let ?g = "Fix2ndVar(f,y)"
from A1 A2 have I: "?g : X→X"
using fix_2nd_var_fun by simp
with A2 A3 show "a : nat → X"
using indseq_seq by simp
then show "a``(nat) ∈ Pow(X)" using func1_1_L6 by simp
from A2 A3 I show "x ∈ a``(nat)" using ind_seq_image by blast
from A2 A3 I have
"?g : X→X" "x∈X" "a``(nat) = InductiveSequence(x,?g)``(nat)"
by auto
then show "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
by (rule ind_seq_image)
qed
text‹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×Y → X" and A2: "x∈X" "y∈Y"
shows "{A ∈ Pow(X). x∈A ∧ (∀z ∈ A. f`⟨z,y⟩ ∈ A) } ≠ 0"
proof -
let ?a = "InductiveSequence(x,Fix2ndVar(f,y))"
let ?A = "?a``(nat)"
from A1 A2 have I: "?A ∈ Pow(X)" and "x ∈ ?A" using binop_gen_set
by auto
moreover
{ fix z assume T: "z∈?A"
with A1 A2 have "Fix2ndVar(f,y)`(z) ∈ ?A"
using binop_gen_set by simp
moreover
from I T have "z ∈ X" by auto
with A1 A2 have "Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
using fix_var_val by simp
ultimately have "f`⟨z,y⟩ ∈ ?A" by simp
} then have "∀z ∈ ?A. f`⟨z,y⟩ ∈ ?A" by simp
ultimately show ?thesis by auto
qed
text‹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×Y → X" and
A2: "X⇩1 ⊆ X" and A3: "x∈X⇩1" "y∈Y" and
A4: "∀t∈X⇩1. f`⟨t,y⟩ ∈ X⇩1" and
A5: "a = InductiveSequence(x,Fix2ndVar(restrict(f,X⇩1×Y),y))"
shows
"a : nat → X⇩1"
"a``(nat) ∈ Pow(X⇩1)"
"x ∈ a``(nat)"
"∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
"∀z ∈ a``(nat). f`⟨z,y⟩ ∈ a``(nat)"
proof -
let ?h = "restrict(f,X⇩1×Y)"
let ?g = "Fix2ndVar(?h,y)"
from A2 have "X⇩1×Y ⊆ X×Y" by auto
with A1 have I: "?h : X⇩1×Y → X"
using restrict_type2 by simp
with A3 have II: "?g: X⇩1 → X" using fix_2nd_var_fun by simp
from A3 A4 I have "∀t∈X⇩1. ?g`(t) ∈ X⇩1"
using restrict fix_var_val by simp
with II have III: "?g : X⇩1 → X⇩1" using func1_1_L1A by blast
with A3 A5 show "a : nat → X⇩1" using indseq_seq by simp
then show IV: "a``(nat) ∈ Pow(X⇩1)" using func1_1_L6 by simp
from A3 A5 III show "x ∈ a``(nat)" using ind_seq_image by blast
from A3 A5 III have
"?g : X⇩1 → X⇩1" "x∈X⇩1" "a``(nat) = InductiveSequence(x,?g)``(nat)"
by auto
then have "∀z ∈ a``(nat). Fix2ndVar(?h,y)`(z) ∈ a``(nat)"
by (rule ind_seq_image)
moreover
{ fix z assume "z ∈ a``(nat)"
with IV have "z ∈ X⇩1" by auto
with A1 A2 A3 have "?g`(z) = Fix2ndVar(f,y)`(z)"
using fix_2nd_var_restr_comm restrict by simp
} then have "∀z ∈ a``(nat). ?g`(z) = Fix2ndVar(f,y)`(z)" by simp
ultimately show "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)" by simp
moreover
{ fix z assume "z ∈ a``(nat)"
with A2 IV have "z∈X" by auto
with A1 A3 have "Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
using fix_var_val by simp
} then have "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
by simp
ultimately show "∀z ∈ a``(nat). f`⟨z,y⟩ ∈ a``(nat)"
by simp
qed
text‹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×Y → X" and
A2: "X⇩1 ⊆ X" and A3: "x∈X⇩1" "y∈Y" and
A4: "∀t∈X⇩1. f`⟨t,y⟩ ∈ X⇩1"
shows "{A ∈ Pow(X⇩1). x∈A ∧ (∀z ∈ A. f`⟨z,y⟩ ∈ A) } ≠ 0"
proof -
let ?a = "InductiveSequence(x,Fix2ndVar(restrict(f,X⇩1×Y),y))"
let ?A = "?a``(nat)"
from A1 A2 A3 A4 have
"?A ∈ Pow(X⇩1)" "x ∈ ?A" "∀z ∈ ?A. f`⟨z,y⟩ ∈ ?A"
using binop_gen_set1 by auto
thus ?thesis by auto
qed
subsection‹Inductive sequences with changing generating function›
text‹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,..\}$.
›
text‹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
"StateTransfFunNMeta(F,n,s) ≡
if (snd(s) ∈ n) then ⟨F`(snd(s))`(fst(s)), succ(snd(s))⟩ else s"
text‹Then we define the actual generating function on sets of pairs
from $X\times \{0,1, .. ,n\}$.›
definition
"StateTransfFunN(X,F,n) ≡ {⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)}"
text‹Having the generating function we can define the expression
that we cen use to define the inductive sequence generates.›
definition
"StatesSeq(x,X,F,n) ≡
InductiveSequenceN(⟨x,0⟩, StateTransfFunN(X,F,n),n)"
text‹Finally we can define the sequence given by a initial point $x$,
and a sequence $F$ of $n$ functions.›
definition
"InductiveSeqVarFN(x,X,F,n) ≡ {⟨k,fst(StatesSeq(x,X,F,n)`(k))⟩. k ∈ succ(n)}"
text‹The state transformation function (‹StateTransfFunN› is
a function that transforms $X\times n$ into itself.›
lemma state_trans_fun: assumes A1: "n ∈ nat" and A2: "F: n → (X→X)"
shows "StateTransfFunN(X,F,n): X×succ(n) → X×succ(n)"
proof -
{ fix s assume A3: "s ∈ X×succ(n)"
let ?x = "fst(s)"
let ?k = "snd(s)"
let ?S = "StateTransfFunNMeta(F,n,s)"
from A3 have T: "?x ∈ X" "?k ∈ succ(n)" and "⟨?x,?k⟩ = s" by auto
{ assume A4: "?k ∈ n"
with A1 have "succ(?k) ∈ succ(n)" using succ_ineq by simp
with A2 T A4 have "?S ∈ X×succ(n)"
using apply_funtype StateTransfFunNMeta_def by simp }
with A2 A3 T have "?S ∈ X×succ(n)"
using apply_funtype StateTransfFunNMeta_def by auto
} then have "∀s ∈ X×succ(n). StateTransfFunNMeta(F,n,s) ∈ X×succ(n)"
by simp
then have
"{⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)} : X×succ(n) → X×succ(n)"
by (rule ZF_fun_from_total)
then show "StateTransfFunN(X,F,n): X×succ(n) → X×succ(n)"
using StateTransfFunN_def by simp
qed
text‹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 ∈ nat" and A2: "F: n → (X→X)" and A3: "x∈X" and
A4: "b = StatesSeq(x,X,F,n)"
shows
"b : succ(n) → X×succ(n)"
"b`(0) = ⟨x,0⟩"
"∀k ∈ succ(n). snd(b`(k)) = k"
"∀k∈n. b`(succ(k)) = ⟨F`(k)`(fst(b`(k))), succ(k)⟩"
proof -
let ?f = "StateTransfFunN(X,F,n)"
from A1 A2 have I: "?f : X×succ(n) → X×succ(n)"
using state_trans_fun by simp
moreover from A1 A3 have II: "⟨x,0⟩ ∈ X×succ(n)"
using empty_in_every_succ by simp
moreover note A1
moreover from A4 have III: "b = InductiveSequenceN(⟨x,0⟩,?f,n)"
using StatesSeq_def by simp
ultimately show IV: "b : succ(n) → X×succ(n)"
by (rule fin_indseq_props)
from I II A1 III show V: "b`(0) = ⟨x,0⟩"
by (rule fin_indseq_props)
from I II A1 III have VI: "∀k∈n. b`(succ(k)) = ?f`(b`(k))"
by (rule fin_indseq_props)
{ fix k
note I
moreover
assume A5: "k ∈ n" hence "k ∈ succ(n)" by auto
with IV have "b`(k) ∈ X×succ(n)" using apply_funtype by simp
moreover have "?f = {⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)}"
using StateTransfFunN_def by simp
ultimately have "?f`(b`(k)) = StateTransfFunNMeta(F,n,b`(k))"
by (rule ZF_fun_from_tot_val)
} then have VII: "∀k ∈ n. ?f`(b`(k)) = StateTransfFunNMeta(F,n,b`(k))"
by simp
{ fix k assume A5: "k ∈ succ(n)"
note A1 A5
moreover from V have " snd(b`(0)) = 0" by simp
moreover from VI VII have
"∀j∈n. snd(b`(j)) = j ⟶ snd(b`(succ(j))) = succ(j)"
using StateTransfFunNMeta_def by auto
ultimately have "snd(b`(k)) = k" by (rule fin_nat_ind)
} then show "∀k ∈ succ(n). snd(b`(k)) = k" by simp
with VI VII show "∀k∈n. b`(succ(k)) = ⟨F`(k)`(fst(b`(k))), succ(k)⟩"
using StateTransfFunNMeta_def by auto
qed
text‹Basic properties of sequences defined by equation $x_{n+1}=f_n (x_n)$.›
theorem fin_indseq_var_f_props:
assumes A1: "n ∈ nat" and A2: "x∈X" and A3: "F: n → (X→X)" and
A4: "a = InductiveSeqVarFN(x,X,F,n)"
shows
"a: succ(n) → X"
"a`(0) = x"
"∀k∈n. a`(succ(k)) = F`(k)`(a`(k))"
proof -
let ?f = "StateTransfFunN(X,F,n)"
let ?b = "StatesSeq(x,X,F,n)"
from A1 A2 A3 have "?b : succ(n) → X×succ(n)"
using states_seq_props by simp
then have "∀k ∈ succ(n). ?b`(k) ∈ X×succ(n)"
using apply_funtype by simp
hence "∀k ∈ succ(n). fst(?b`(k)) ∈ X" by auto
then have I: "{⟨k,fst(?b`(k))⟩. k ∈ succ(n)} : succ(n) → X"
by (rule ZF_fun_from_total)
with A4 show II: "a: succ(n) → X" using InductiveSeqVarFN_def
by simp
moreover from A1 have "0 ∈ succ(n)" using empty_in_every_succ
by simp
moreover from A4 have III:
"a = {⟨k,fst(StatesSeq(x,X,F,n)`(k))⟩. k ∈ succ(n)}"
using InductiveSeqVarFN_def by simp
ultimately have "a`(0) = fst(?b`(0))"
by (rule ZF_fun_from_tot_val)
with A1 A2 A3 show "a`(0) = x" using states_seq_props by auto
{ fix k
assume A5: "k ∈ n"
with A1 have T1: "succ(k) ∈ succ(n)" and T2: "k ∈ succ(n)"
using succ_ineq by auto
from II T1 III have "a`(succ(k)) = fst(?b`(succ(k)))"
by (rule ZF_fun_from_tot_val)
with A1 A2 A3 A5 have "a`(succ(k)) = F`(k)`(fst(?b`(k)))"
using states_seq_props by simp
moreover from II T2 III have "a`(k) = fst(?b`(k))"
by (rule ZF_fun_from_tot_val)
ultimately have "a`(succ(k)) = F`(k)`(a`(k))"
by simp
} then show "∀k∈n. a`(succ(k)) = F`(k)`(a`(k))"
by simp
qed
text‹Uniqueness lemma for sequences generated by equation $x_{n+1}=f_n (x_n)$:›
lemma fin_indseq_var_f_uniq: assumes "n∈nat" "x∈X" "F: n → (X→X)"
and "a: succ(n) → X" "a`(0) = x" "∀k∈n. a`(succ(k)) = (F`(k))`(a`(k))"
and "b: succ(n) → X" "b`(0) = x" "∀k∈n. b`(succ(k)) = (F`(k))`(b`(k))"
shows "a=b"
proof -
have "∀k∈succ(n). a`(k) = b`(k)"
proof -
let ?A = "{i∈succ(succ(n)). ∀k∈i. a`(k) = b`(k)}"
let ?m = "Maximum(Le,?A)"
from assms(1) have I: "succ(succ(n)) ∈ nat" "?A⊆succ(succ(n))" by auto
moreover
from assms(1,5,8) have "succ(0) ∈ ?A" using empty_in_every_succ succ_ineq
by simp
hence II: "?A≠0" by auto
ultimately have "?m∈?A" by (rule nat_max_props)
moreover have "?m = succ(n)"
proof -
{ assume "?m ≠ succ(n)"
from I II have III: "∀k∈?A. k ≤ ?m" by (rule nat_max_props)
have "succ(?m) ∈ ?A"
proof -
from ‹?m ≠ succ(n)› ‹?m∈?A› have "?m∈succ(n)"
using mem_succ_not_eq by blast
from I II have "?m ∈ nat" by (rule nat_max_props)
from ‹succ(0) ∈ ?A› III have "succ(0) ≤ ?m" by blast
hence "?m ≠ 0" by auto
with ‹?m ∈ nat› obtain k where "k∈nat" "?m = succ(k)"
using Nat_ZF_1_L3 by auto
with assms(1) ‹?m∈succ(n)› have "k∈n" using succ_mem by simp
with assms(6,9) ‹?m = succ(k)› ‹?m∈?A›
have "a`(?m) = b`(?m)" using succ_explained by simp
with assms(1) ‹?m∈?A› ‹?m∈succ(n)› show "succ(?m) ∈ ?A"
using succ_explained succ_ineq by blast
qed
with III have "succ(?m) ≤ ?m" by (rule property_holds)
hence False by auto
} thus ?thesis by auto
qed
ultimately show ?thesis by simp
qed
with assms(4,7) show "a=b" by (rule func_eq)
qed
text‹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∈nat" "x∈X" "F: n → (X→X)"
and "a: succ(n) → X" "a`(0) = x" "∀k∈n. a`(succ(k)) = (F`(k))`(a`(k))"
shows "a = InductiveSeqVarFN(x,X,F,n)"
proof -
let ?b = "InductiveSeqVarFN(x,X,F,n)"
from assms(1,2,3) have "?b: succ(n) → X" "?b`(0) = x"
and "∀k∈n. ?b`(succ(k)) = F`(k)`(?b`(k))"
using fin_indseq_var_f_props by simp_all
with assms show ?thesis by (rule fin_indseq_var_f_uniq)
qed
text‹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 ∈ nat" "i ∈ nat" "x∈X" "F: n → (X→X)" "G: i → (X→X)"
and A2: "i ⊆ n" and A3: "∀j∈i. G`(j) = F`(j)" and A4: "k ∈ succ(i)"
shows "InductiveSeqVarFN(x,X,G,i)`(k) = InductiveSeqVarFN(x,X,F,n)`(k)"
proof -
let ?a = "InductiveSeqVarFN(x,X,F,n)"
let ?b = "InductiveSeqVarFN(x,X,G,i)"
from A1 A4 have "i ∈ nat" "k ∈ succ(i)" by auto
moreover from A1 have "?b`(0) = ?a`(0)"
using fin_indseq_var_f_props by simp
moreover from A1 A2 A3 have
"∀j∈i. ?b`(j) = ?a`(j) ⟶ ?b`(succ(j)) = ?a`(succ(j))"
using fin_indseq_var_f_props by auto
ultimately show "?b`(k) = ?a`(k)"
by (rule fin_nat_ind)
qed
subsection‹The Pascal's triangle›
text‹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.›
text‹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
"BinomElem(r,k) ≡ if k=0 then 1 else r`(pred(k)) #+ r`(k)"
text‹Next we define a function that takes a row in a Pascal's triangle and returns the next row. ›
definition
"GenBinom ≡ {⟨r,{⟨k,BinomElem(r,k)⟩. k∈succ(domain(r))}⟩. r∈NELists(nat)}"
text‹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: NELists(nat) → NELists(nat)"
proof -
{ fix r assume "r ∈ NELists(nat)"
then obtain n where "n∈nat" and "r:succ(n)→nat"
unfolding NELists_def by auto
then have "domain(r) = succ(n)" using func1_1_L1 by simp
let ?r⇩1 = "{⟨k,BinomElem(r,k)⟩. k∈succ(domain(r))}"
have "∀k∈succ(domain(r)). BinomElem(r,k) ∈ nat"
unfolding BinomElem_def by simp
then have "?r⇩1: succ(domain(r))→nat"
by (rule ZF_fun_from_total)
with ‹n∈nat› ‹domain(r) = succ(n)› have "?r⇩1∈NELists(nat)"
unfolding NELists_def by auto
} then show ?thesis using ZF_fun_from_total unfolding GenBinom_def
by simp
qed
text‹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∈nat" "r:succ(n)→nat"
shows "GenBinom`(r):succ(succ(n)) → nat"
proof -
let ?B = "{⟨r,{⟨k,BinomElem(r,k)⟩. k∈succ(domain(r))}⟩. r∈NELists(nat)}"
let ?r⇩1 = "{⟨k,BinomElem(r,k)⟩. k∈succ(domain(r))}"
from assms have "r∈NELists(nat)" unfolding NELists_def by blast
then have "?B`(r) = ?r⇩1" using ZF_fun_from_tot_val1 by simp
have "∀k∈succ(domain(r)). BinomElem(r,k) ∈ nat"
unfolding BinomElem_def by simp
then have "?r⇩1: succ(domain(r))→nat"
by (rule ZF_fun_from_total)
with assms(2) ‹?B`(r) = ?r⇩1› show ?thesis
using func1_1_L1 unfolding GenBinom_def by simp
qed
text‹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 ≡ InductiveSequence({⟨0,1⟩},GenBinom)"
text‹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 "{⟨0,1⟩} ∈ NELists(nat)" and "PascalTriangle: nat → NELists(nat)"
using list_len1_singleton(2) gen_binom_fun indseq_seq
unfolding PascalTriangle_def
by auto
text‹The ‹GenBinom› function creates the next row of the Pascal's triangle
from the previous one. ›
lemma binom_gen: assumes "n∈nat"
shows "PascalTriangle`(succ(n)) = GenBinom`(PascalTriangle`(n))"
using assms pascal_sequence gen_binom_fun indseq_vals
unfolding PascalTriangle_def by simp
text‹The $n$'th row of the Pascal's triangle is a list of $n+1$ natural numbers. ›
lemma pascal_row_list:
assumes "n∈nat" shows "PascalTriangle`(n):succ(n)→nat"
proof -
from assms(1) have "n∈nat" and "PascalTriangle`(0):succ(0)→nat"
using gen_binom_fun pascal_sequence(1) indseq_valat0 list_len1_singleton(1)
unfolding PascalTriangle_def by auto
moreover have
"∀k∈nat. PascalTriangle`(k):succ(k)→nat ⟶
PascalTriangle`(succ(k)):succ(succ(k))→nat"
proof -
{ fix k assume "k∈nat" and "PascalTriangle`(k):succ(k)→nat"
then have "PascalTriangle`(succ(k)):succ(succ(k))→nat"
using gen_binom_fun_val gen_binom_fun pascal_sequence(1) indseq_vals
unfolding NELists_def PascalTriangle_def
by auto
} thus ?thesis by simp
qed
ultimately show ?thesis by (rule ind_on_nat)
qed
text‹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∈nat"
shows "(PascalTriangle`(n))`(succ(n)) = 0"
proof -
from assms have "domain(PascalTriangle`(n)) = succ(n)"
using pascal_row_list func1_1_L1 by blast
then show ?thesis using mem_self apply_0
by simp
qed
text‹For $n>0$ the Pascal's triangle values at $(n,k)$ are given by the ‹BinomElem› expression. ›
lemma pascal_row_val: assumes "n∈nat" "k∈succ(succ(n))"
shows "(PascalTriangle`(succ(n)))`(k) = BinomElem(PascalTriangle`(n),k)"
proof -
let ?B = "{⟨r,{⟨k,BinomElem(r,k)⟩. k∈succ(domain(r))}⟩. r∈NELists(nat)}"
let ?r = "PascalTriangle`(n)"
let ?B⇩r = "{⟨k,BinomElem(?r,k)⟩. k∈succ(succ(n))}"
from assms(1) have "?r ∈ NELists(nat)" and "?r : succ(n)→nat"
using pascal_sequence(2) apply_funtype pascal_row_list
by auto
then have "?B`(?r) = ?B⇩r" using func1_1_L1 ZF_fun_from_tot_val1
by simp
moreover from assms(1) have "?B`(?r) = PascalTriangle`(succ(n))"
using binom_gen unfolding GenBinom_def by simp
moreover from assms(2) have "?B⇩r`(k) = BinomElem(?r,k)"
by (rule ZF_fun_from_tot_val1)
ultimately show ?thesis by simp
qed
text‹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
"Binom(n,k) ≡ (PascalTriangle`(n))`(k)"
text‹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$.›
lemma binom_in_nat: assumes "n∈nat" shows "Binom(n,k) ∈ nat"
proof -
{ assume "k ∈ succ(n)"
with assms have "(PascalTriangle`(n))`(k) ∈ nat"
using pascal_row_list apply_funtype by blast
}
moreover
{ assume "k ∉ succ(n)"
from assms have "domain(PascalTriangle`(n)) = succ(n)"
using pascal_row_list func1_1_L1 by blast
with ‹k ∉ succ(n)› have "(PascalTriangle`(n))`(k) = 0"
using apply_0 by simp
hence "(PascalTriangle`(n))`(k) ∈ nat" by simp
}
ultimately show ?thesis unfolding Binom_def by blast
qed
text‹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 "Binom(0,0) = 1"
using gen_binom_fun pascal_sequence(1) indseq_valat0 pair_val
unfolding Binom_def PascalTriangle_def by auto
text‹The binomial coefficients are 1 on the left boundary of the Pascal's triangle.›
theorem binom_left_boundary: assumes "n∈nat" shows "Binom(n,0) = 1"
proof -
{ assume "n≠0"
with assms obtain k where "k∈nat" and "n = succ(k)"
using Nat_ZF_1_L3 by blast
then have "Binom(n,0) = 1" using empty_in_every_succ pascal_row_val
unfolding BinomElem_def Binom_def by simp
}
then show ?thesis using binom_zero_zero by blast
qed
text‹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∈nat" "k ≤ n #+ 1" "k≠0"
shows "Binom(n #+ 1,k) = Binom(n,k #- 1) #+ Binom(n,k)"
proof -
let ?P = "PascalTriangle"
from assms(1,2) have "k∈nat" and "k ∈ succ(succ(n))"
using le_in_nat nat_mem_lt(2) by auto
with assms(1) have "Binom(n #+ 1,k) = BinomElem(?P`(n),k)"
unfolding Binom_def using pascal_row_val by simp
also from assms(3) ‹k∈nat› have
"BinomElem(?P`(n),k) = (?P`(n))`(k #- 1) #+ (?P`(n))`(k)"
unfolding BinomElem_def using pred_minus_one by simp
also have "(?P`(n))`(k #- 1) #+ (?P`(n))`(k) = Binom(n,k #- 1) #+ Binom(n,k)"
unfolding Binom_def by simp
finally show ?thesis by simp
qed
text‹A version ‹binom_prop› where we write $k+1$ instead of $k$.›
lemma binom_prop2: assumes "n∈nat" "k ∈ n #+ 1"
shows "Binom(n #+ 1,k #+ 1) = Binom(n,k #+ 1) #+ Binom(n,k)"
proof -
from assms have "k∈nat" using elem_nat_is_nat(2) by blast
hence "k #+1 #- 1 = k" by simp
moreover from assms have
"Binom(n #+ 1,k #+ 1) = Binom(n,k #+1 #- 1) #+ Binom(n,k #+ 1)"
using succ_ineq2 binom_prop by simp
ultimately show ?thesis by simp
qed
text‹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∈nat"
shows "Binom(n #+ 1,n #+ 1) = Binom(n,n)"
proof -
let ?B = "Binom"
from assms have "?B(n,n) ∈ nat"
using pascal_row_list apply_funtype
unfolding Binom_def by blast
from assms have "(PascalTriangle`(n))`(succ(n)) = 0"
using pascal_val_beyond by simp
moreover from assms have "succ(n) = n #+ 1"
using succ_add_one(1) by simp
ultimately have "?B(n,n #+ 1) = 0"
unfolding Binom_def by simp
with assms ‹?B(n,n) ∈ nat› show ?thesis
using succ_add_one(2) binom_prop add_subctract add_0 add_commute
by simp
qed
text‹The binomial coefficients are 1 on the right boundary of the Pascal's triangle.›
theorem binom_right_boundary: assumes "n∈nat" shows "Binom(n,n) = 1"
proof -
from assms have "n∈nat" and "Binom(0,0) = 1"
using binom_zero_zero by auto
moreover have
"∀k∈nat. Binom(k,k) = 1 ⟶ Binom(succ(k),succ(k)) = 1"
using binom_prop1 by simp
ultimately show ?thesis by (rule ind_on_nat)
qed
end