theory Fold_ZF imports InductiveSeq_ZF
begin
Suppose we have a binary operation \(P: X\times X \rightarrow X\) written multiplicatively as \(P\langle x, y \rangle= x\cdot y\). In informal mathematics we can take a sequence \(\{ x_k \}_{k\in 0.. n}\) of elements of \(X\) and consider the product \(x_0\cdot x_1 \cdot .. \cdot x_n\). To do the same thing in formalized mathematics we have to define precisely what is meant by that "\(\cdot .. \cdot\)". The definitition we want to use is based on the notion of sequence defined by induction discussed in InductiveSeq_ZF. We don't really want to derive the terminology for this from the word "product" as that would tie it conceptually to the multiplicative notation. This would be awkward when we want to reuse the same notions to talk about sums like \(x_0 + x_1 + .. + x_n\). In functional programming there is something called "fold". Namely for a function \(f\), initial point \(a\) and list \(\left[ b, c, d\right]\) the expression \( fold(f, a, [b,c,d]) \) is defined to be \( f(f(f(a,b),c),d) \) (in Haskell something like this is called foldl). If we write \(f\) in multiplicative notation we get \(a\cdot b \cdot c\cdot d\), so this is exactly what we need. The notion of folds in functional programming is actually much more general that what we need here (not that I know anything about that). In this theory file we just make a slight generalization and talk about folding a list with a binary operation \(f:X\times Y \rightarrow X\) with \(X\) not necessarily the same as \(Y\).
Folding in ZF
Suppose we have a binary operation \(f : X\times Y \rightarrow X\). Then every \(y\in Y\) defines a transformation of \(X\) defined by \(T_y(x) = f\langle x,y\rangle\). In IsarMathLib such transformation is called as \( \text{Fix2ndVar}(f,y) \). Using this notion, given a function \(f: X\times Y\rightarrow X\) and a sequence \(y = \{y_k\}_{k\in N}\) of elements of \(X\) we can get a sequence of transformations of \(X\). This is defined in Seq2TransSeq below. Then we use that sequence of tranformations to define the sequence of partial folds (called FoldSeq) by means of InductiveSeqVarFN (defined in InductiveSeq_ZF theory) which implements the inductive sequence determined by a starting point and a sequence of transformations. Finally, we define the fold of a sequence as the last element of the sequence of the partial folds.
Definition that specifies how to convert a sequence \(a\) of elements of \(Y\) into a sequence of transformations of \(X\), given a binary operation \(f :X\times Y \rightarrow X\).
definition
\( \text{Seq2TrSeq}(f,a) \equiv \{\langle k, \text{Fix2ndVar}(f,a(k))\rangle .\ k \in domain(a)\} \)
Definition of a sequence of partial folds.
definition
\( \text{FoldSeq}(f,x,a) \equiv \) \( \text{InductiveSeqVarFN}(x, \text{fstdom}(f), \text{Seq2TrSeq}(f,a),domain(a)) \)
Definition of a fold.
definition
\( \text{Fold}(f,x,a) \equiv \text{Last}( \text{FoldSeq}(f,x,a)) \)
If \(X\) is a set with a binary operation \(f:X\times Y \rightarrow X\) then \( Seq2TransSeqN(f,a) \) converts a sequence \(a\) of elements of \(Y\) into the sequence of corresponding transformations of \(X\).
lemma seq2trans_seq_props:
assumes A1: \( n \in nat \) and A2: \( f : X\times Y \rightarrow X \) and A3: \( a:n\rightarrow Y \) and A4: \( T = \text{Seq2TrSeq}(f,a) \)
shows \( T : n \rightarrow (X\rightarrow X) \) and \( \forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle \)proof from \( a:n\rightarrow Y \) have D: \( domain(a) = n \) using func1_1_L1
with A2, A3, A4 show \( T : n \rightarrow (X\rightarrow X) \) using apply_funtype, fix_2nd_var_fun, ZF_fun_from_total, Seq2TrSeq_def
with A4, D have I: \( \forall k \in n.\ T(k) = \text{Fix2ndVar}(f,a(k)) \) using Seq2TrSeq_def, ZF_fun_from_tot_val0
{
fix \( k \) \( fix \) \( x \)
assume A5: \( k\in n \), \( x\in X \)
with A1, A3 have \( a(k) \in Y \) using apply_funtype
with A2, A5, I have \( (T(k))(x) = f\langle x,a(k)\rangle \) using fix_var_val
thus \( \forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle \)
qed
Basic properties of the sequence of partial folds of a sequence \(a = \{y_k\}_{k\in \{0,..,n\} }\).
theorem fold_seq_props:
assumes A1: \( n \in nat \) and A2: \( f : X\times Y \rightarrow X \) and A3: \( y:n\rightarrow Y \) and A4: \( x\in X \) and A5: \( Y\neq 0 \) and A6: \( F = \text{FoldSeq}(f,x,y) \)
shows \( F: succ(n) \rightarrow X \), \( F(0) = x \) and \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \)proof let \( T = \text{Seq2TrSeq}(f,y) \)
from A1, A3 have D: \( domain(y) = n \) using func1_1_L1
from \( f : X\times Y \rightarrow X \), \( Y\neq 0 \) have I: \( \text{fstdom}(f) = X \) using fstdomdef
with A1, A2, A3, A4, A6, D show II: \( F: succ(n) \rightarrow X \) and \( F(0) = x \) using seq2trans_seq_props, FoldSeq_def, fin_indseq_var_f_props
from A1, A2, A3, A4, A6, I, D have \( \forall k\in n.\ F(succ(k)) = T(k)(F(k)) \) using seq2trans_seq_props, FoldSeq_def, fin_indseq_var_f_props
moreover {
}
ultimately show \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \)
qed
fix \( k \)
assume A5: \( k\in n \)
hence \( k \in succ(n) \)
with A1, A2, A3, II, A5 have \( (T(k))(F(k)) = f\langle F(k),y(k)\rangle \) using apply_funtype, seq2trans_seq_props
A consistency condition: if we make the list shorter, then we get a shorter sequence of partial folds with the same values as in the original sequence. This can be proven as a special case of fin_indseq_var_f_restrict but a proof using fold_seq_props and induction turns out to be shorter.
lemma foldseq_restrict:
assumes \( n \in nat \), \( k \in succ(n) \) and \( i \in nat \), \( f : X\times Y \rightarrow X \), \( a : n \rightarrow Y \), \( b : i \rightarrow Y \) and \( n \subseteq i \), \( \forall j \in n.\ b(j) = a(j) \), \( x \in X \), \( Y \neq 0 \)
shows \( \text{FoldSeq}(f,x,b)(k) = \text{FoldSeq}(f,x,a)(k) \)proof let \( P = \text{FoldSeq}(f,x,a) \)
let \( Q = \text{FoldSeq}(f,x,b) \)
from assms have \( n \in nat \), \( k \in succ(n) \), \( Q(0) = P(0) \) and \( \forall j \in n.\ Q(j) = P(j) \longrightarrow Q(succ(j)) = P(succ(j)) \) using fold_seq_props
then show \( Q(k) = P(k) \) by (rule fin_nat_ind )
qed
A special case of foldseq_restrict when the longer sequence is created from the shorter one by appending one element.
corollary fold_seq_append:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \) and \( x\in X \), \( k \in succ(n) \), \( y\in Y \)
shows \( \text{FoldSeq}(f,x, \text{Append}(a,y))(k) = \text{FoldSeq}(f,x,a)(k) \)proof let \( b = \text{Append}(a,y) \)
from assms have \( b : succ(n) \rightarrow Y \), \( \forall j \in n.\ b(j) = a(j) \) using append_props
with assms show \( thesis \) using foldseq_restrict
qed
What we really will be using is the notion of the fold of a sequence, which we define as the last element of (inductively defined) sequence of partial folds. The next theorem lists some properties of the product of the fold operation.
theorem fold_props:
assumes A1: \( n \in nat \) and A2: \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
shows \( \text{Fold}(f,x,a) = \text{FoldSeq}(f,x,a)(n) \) and \( \text{Fold}(f,x,a) \in X \)proof from assms have \( \text{FoldSeq}(f,x,a) : succ(n) \rightarrow X \) using fold_seq_props
with A1 show \( \text{Fold}(f,x,a) = \text{FoldSeq}(f,x,a)(n) \) and \( \text{Fold}(f,x,a) \in X \) using last_seq_elem, apply_funtype, Fold_def
qed
A corner case: what happens when we fold an empty list?
theorem fold_empty:
assumes A1: \( f : X\times Y \rightarrow X \) and A2: \( a:0\rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
shows \( \text{Fold}(f,x,a) = x \)proof let \( F = \text{FoldSeq}(f,x,a) \)
from assms have I: \( 0 \in nat \), \( f : X\times Y \rightarrow X \), \( a:0\rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
then have \( \text{Fold}(f,x,a) = F(0) \) by (rule fold_props )
moreover
qed
from I have \( 0 \in nat \), \( f : X\times Y \rightarrow X \), \( a:0\rightarrow Y \), \( x\in X \), \( Y\neq 0 \) and \( F = \text{FoldSeq}(f,x,a) \)
then have \( F(0) = x \) by (rule fold_seq_props )
ultimately show \( \text{Fold}(f,x,a) = x \)
The next theorem tells us what happens to the fold of a sequence when we add one more element to it.
theorem fold_append:
assumes A1: \( n \in nat \) and A2: \( f : X\times Y \rightarrow X \) and A3: \( a:n\rightarrow Y \) and A4: \( x\in X \) and A5: \( y\in Y \)
shows \( \text{FoldSeq}(f,x, \text{Append}(a,y))(n) = \text{Fold}(f,x,a) \) and \( \text{Fold}(f,x, \text{Append}(a,y)) = f\langle \text{Fold}(f,x,a), y\rangle \)proof let \( b = \text{Append}(a,y) \)
let \( P = \text{FoldSeq}(f,x,b) \)
from A5 have I: \( Y \neq 0 \)
with assms show thesis1: \( P(n) = \text{Fold}(f,x,a) \) using fold_seq_append, fold_props
from assms, I have II: \( succ(n) \in nat \), \( f : X\times Y \rightarrow X \), \( b : succ(n) \rightarrow Y \), \( x\in X \), \( Y \neq 0 \), \( P = \text{FoldSeq}(f,x,b) \) using append_props
then have \( \forall k \in succ(n).\ P(succ(k)) = f\langle P(k), b(k)\rangle \) by (rule fold_seq_props )
with A3, A5, thesis1 have \( P(succ(n)) = f\langle \text{Fold}(f,x,a), y\rangle \) using append_props
moreover
qed
from II have \( P : succ(succ(n)) \rightarrow X \) by (rule fold_seq_props )
then have \( \text{Fold}(f,x,b) = P(succ(n)) \) using last_seq_elem, Fold_def
ultimately show \( \text{Fold}(f,x, \text{Append}(a,y)) = f\langle \text{Fold}(f,x,a), y\rangle \)
Another way of formulating information contained in fold_append is to start with a longer sequence \(a:n+1\rightarrow X\) and then detach the last element from it. This provides an identity between the fold of the longer sequence and the value of the folding function on the fold of the shorter sequence and the last element of the longer one.
lemma fold_detach_last:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( x\in X \), \( \forall k\in n + 1.\ q(k) \in Y \)
shows \( \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n + 1\}) = f\langle \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n\}), q(n)\rangle \)proof let \( a = \{\langle k,q(k)\rangle .\ k\in n + 1\} \)
let \( b = \{\langle k,q(k)\rangle .\ k\in n\} \)
from assms have \( \text{Fold}(f,x, \text{Append}(b,q(n))) = f\langle \text{Fold}(f,x,b), q(n)\rangle \) using ZF_fun_from_total, fold_append(2)
moreover
qed
from assms(1,4) have \( a = \text{Append}(b,q(n)) \) using set_list_append1(4)
ultimately show \( \text{Fold}(f,x,a) = f\langle \text{Fold}(f,x,b), q(n)\rangle \)
The tail of the sequence of partial folds defined by the folding function \(f\), starting point \(x\) and a sequence \(y\) is the same as the sequence of partial folds starting from \(f(x,y(0))\).
lemma fold_seq_detach_first:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( y:succ(n)\rightarrow Y \), \( x\in X \)
shows \( \text{FoldSeq}(f,f\langle x,y(0)\rangle , \text{Tail}(y)) = \text{Tail}( \text{FoldSeq}(f,x,y)) \)proof let \( F = \text{FoldSeq}(f,x,y) \)
let \( T = \text{Tail}(F) \)
let \( S = \text{Seq2TrSeq}(f, \text{Tail}(y)) \)
from assms(1,3) have \( succ(n) \in nat \), \( 0 \in succ(n) \), \( y(0)\in Y \) using empty_in_every_succ, apply_funtype
have \( n \in nat \), \( f\langle x,y(0)\rangle \in X \), \( S:n\rightarrow (X\rightarrow X) \) and \( T:succ(n) \rightarrow X \), \( T(0) = f\langle x,y(0)\rangle \) and \( \forall k\in n.\ T(succ(k)) = (S(k))(T(k)) \)proof
from assms(1) show \( n \in nat \)
from assms, \( succ(n) \in nat \) show \( T:succ(n) \rightarrow X \) using fold_seq_props(1), tail_props(1), nelist_vals_nonempty
from assms(2,4), \( y(0)\in Y \) show \( f\langle x,y(0)\rangle \in X \) using apply_funtype
from assms(1,2,3) show \( S:n\rightarrow (X\rightarrow X) \) using tail_props(1), seq2trans_seq_props
from assms have I: \( F:succ(succ(n)) \rightarrow X \) using fold_seq_props(1), nelist_vals_nonempty
show \( T(0) = f\langle x,y(0)\rangle \)proof
from \( succ(n) \in nat \), \( 0 \in succ(n) \), I have \( T(0) = F(succ(0)) \) using tail_props(2)
moreover
qed
from assms, \( 0 \in succ(n) \) have \( F(succ(0)) = f\langle F(0), y(0)\rangle \) using fold_seq_props(3), nelist_vals_nonempty
moreover from assms have \( F(0) = x \) using fold_seq_props(2), nelist_vals_nonempty
ultimately show \( T(0) = f\langle x,y(0)\rangle \)
show \( \forall k\in n.\ T(succ(k)) = (S(k))(T(k)) \)proof
qed
{
}
fix \( k \)
assume \( k\in n \)
with assms(1) have \( succ(k) \in succ(n) \), \( k\in succ(n) \), \( succ(k) \in succ(succ(n)) \) using succ_ineq
with \( succ(n) \in nat \), I have \( T(succ(k)) = F(succ(succ(k))) \) using tail_props(2)
moreover
from assms, \( succ(k) \in succ(n) \) have \( F(succ(succ(k))) = f\langle F(succ(k)), y(succ(k))\rangle \) using fold_seq_props(3), nelist_vals_nonempty
moreover from assms(1,3), \( k\in n \) have \( y(succ(k)) = ( \text{Tail}(y))(k) \) using tail_props(2)
moreover from assms, \( k\in n \), I, \( succ(k) \in succ(succ(n)) \) have \( f\langle F(succ(k)),( \text{Tail}(y))(k)\rangle = (S(k))(F(succ(k))) \) using tail_props(1), seq2trans_seq_props(2), apply_funtype
moreover from \( succ(n) \in nat \), I, \( k\in succ(n) \) have \( T(k) = F(succ(k)) \) using tail_props(2)
ultimately have \( T(succ(k)) = (S(k))(T(k)) \)
thus \( thesis \)
qed
then have \( T = \text{InductiveSeqVarFN}(f\langle x,y(0)\rangle ,X,S,n) \) by (rule is_fin_indseq_var_f )
moreover
qed
have \( \text{fstdom}(f) = X \) and \( domain( \text{Tail}(y)) = n \)proof
ultimately show \( thesis \) unfolding FoldSeq_def
from assms(2,3) show \( \text{fstdom}(f) = X \) using fstdomdef, nelist_vals_nonempty
from assms(1,3) show \( domain( \text{Tail}(y)) = n \) using tail_props(1), func1_1_L1
qed
Taking a fold of a sequence \(y\) with a function \(f\) with the starting point \(x\) is the same as the fold starting from \(f\langle x,y(0)\rangle\) of the tail of \(y\).
lemma fold_detach_first:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( y:succ(n)\rightarrow Y \), \( x\in X \)
shows \( \text{Fold}(f,x,y) = \text{Fold}(f,f\langle x,y(0)\rangle , \text{Tail}(y)) \)proof from assms have \( \text{FoldSeq}(f,x,y):succ(succ(n))\rightarrow X \) using fold_seq_props(1), nelist_vals_nonempty
with assms show \( thesis \) using last_tail_last, fold_seq_detach_first unfolding Fold_def
qed
end
lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \) 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 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 Seq2TrSeq:
\( \text{Seq2TrSeq}(f,a) \equiv \{\langle k, \text{Fix2ndVar}(f,a(k))\rangle .\ k \in domain(a)\} \)
lemma ZF_fun_from_tot_val0:
assumes \( f:X\rightarrow Y \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( \forall x\in X.\ f(x) = b(x) \) 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 fstdomdef:
assumes \( f: X\times Y \rightarrow Z \) and \( Y\neq \emptyset \)
shows \( \text{fstdom}(f) = X \) lemma seq2trans_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( a:n\rightarrow Y \) and \( T = \text{Seq2TrSeq}(f,a) \)
shows \( T : n \rightarrow (X\rightarrow X) \) and \( \forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle \)Definition of FoldSeq:
\( \text{FoldSeq}(f,x,a) \equiv \)
\( \text{InductiveSeqVarFN}(x, \text{fstdom}(f), \text{Seq2TrSeq}(f,a),domain(a)) \)
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)) \) theorem fold_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( y:n\rightarrow Y \) and \( x\in X \) and \( Y\neq 0 \) and \( F = \text{FoldSeq}(f,x,y) \)
shows \( F: succ(n) \rightarrow X \), \( F(0) = x \) and \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \) 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) \) theorem append_props:
assumes \( a: n \rightarrow X \) and \( x\in X \) and \( b = \text{Append}(a,x) \)
shows \( b : succ(n) \rightarrow X \), \( \forall k\in n.\ b(k) = a(k) \), \( b(n) = x \) lemma foldseq_restrict:
assumes \( n \in nat \), \( k \in succ(n) \) and \( i \in nat \), \( f : X\times Y \rightarrow X \), \( a : n \rightarrow Y \), \( b : i \rightarrow Y \) and \( n \subseteq i \), \( \forall j \in n.\ b(j) = a(j) \), \( x \in X \), \( Y \neq 0 \)
shows \( \text{FoldSeq}(f,x,b)(k) = \text{FoldSeq}(f,x,a)(k) \) lemma last_seq_elem:
assumes \( a: succ(n) \rightarrow X \)
shows \( \text{Last}(a) = a(n) \)Definition of Fold:
\( \text{Fold}(f,x,a) \equiv \text{Last}( \text{FoldSeq}(f,x,a)) \)
theorem fold_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
shows \( \text{Fold}(f,x,a) = \text{FoldSeq}(f,x,a)(n) \) and \( \text{Fold}(f,x,a) \in X \) corollary fold_seq_append:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \) and \( x\in X \), \( k \in succ(n) \), \( y\in Y \)
shows \( \text{FoldSeq}(f,x, \text{Append}(a,y))(k) = \text{FoldSeq}(f,x,a)(k) \) theorem fold_append:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( a:n\rightarrow Y \) and \( x\in X \) and \( y\in Y \)
shows \( \text{FoldSeq}(f,x, \text{Append}(a,y))(n) = \text{Fold}(f,x,a) \) and \( \text{Fold}(f,x, \text{Append}(a,y)) = f\langle \text{Fold}(f,x,a), y\rangle \) lemma set_list_append1:
assumes \( n\in nat \) and \( \forall k\in n + 1.\ q(k) \in X \)
defines \( a\equiv \{\langle k,q(k)\rangle .\ k\in n + 1\} \)
shows \( a: n + 1 \rightarrow X \), \( \{\langle k,q(k)\rangle .\ k \in n\}: n \rightarrow X \), \( \text{Init}(a) = \{\langle k,q(k)\rangle .\ k \in n\} \), \( a = \text{Append}(\{\langle k,q(k)\rangle .\ k \in n\},q(n)) \), \( a = \text{Append}( \text{Init}(a), q(n)) \), \( a = \text{Append}( \text{Init}(a), a(n)) \) lemma empty_in_every_succ:
assumes \( n \in nat \)
shows \( 0 \in succ(n) \) theorem fold_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( y:n\rightarrow Y \) and \( x\in X \) and \( Y\neq 0 \) and \( F = \text{FoldSeq}(f,x,y) \)
shows \( F: succ(n) \rightarrow X \), \( F(0) = x \) and \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \) 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)) \) lemma nelist_vals_nonempty:
assumes \( a:succ(n)\rightarrow Y \)
shows \( Y\neq 0 \) 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 fold_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( y:n\rightarrow Y \) and \( x\in X \) and \( Y\neq 0 \) and \( F = \text{FoldSeq}(f,x,y) \)
shows \( F: succ(n) \rightarrow X \), \( F(0) = x \) and \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \) theorem fold_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( y:n\rightarrow Y \) and \( x\in X \) and \( Y\neq 0 \) and \( F = \text{FoldSeq}(f,x,y) \)
shows \( F: succ(n) \rightarrow X \), \( F(0) = x \) and \( \forall k\in n.\ F(succ(k)) = f\langle F(k), y(k)\rangle \) lemma succ_ineq:
assumes \( n \in nat \)
shows \( \forall i \in n.\ succ(i) \in succ(n) \) lemma seq2trans_seq_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \) and \( a:n\rightarrow Y \) and \( T = \text{Seq2TrSeq}(f,a) \)
shows \( T : n \rightarrow (X\rightarrow X) \) and \( \forall k\in n.\ \forall x\in X.\ (T(k))(x) = f\langle x,a(k)\rangle \) 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) \) lemma last_tail_last:
assumes \( n\in nat \), \( a: succ(succ(n)) \rightarrow X \)
shows \( \text{Last}( \text{Tail}(a)) = \text{Last}(a) \) lemma fold_seq_detach_first:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( y:succ(n)\rightarrow Y \), \( x\in X \)
shows \( \text{FoldSeq}(f,f\langle x,y(0)\rangle , \text{Tail}(y)) = \text{Tail}( \text{FoldSeq}(f,x,y)) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8