# Theory Fold_ZF

(*
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Folding in ZF›

theory Fold_ZF imports InductiveSeq_ZF

begin

text‹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$.›

subsection‹Folding in ZF›

text‹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 ‹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.›

text‹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
"Seq2TrSeq(f,a) ≡ {⟨k,Fix2ndVar(f,a(k))⟩. k ∈ domain(a)}"

text‹Definition of a sequence of partial folds.›

definition
"FoldSeq(f,x,a) ≡
InductiveSeqVarFN(x,fstdom(f),Seq2TrSeq(f,a),domain(a))"

text‹Definition of a fold.›

definition
"Fold(f,x,a) ≡ Last(FoldSeq(f,x,a))"

text‹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 ∈ nat" and A2: "f : X×Y → X" and A3: "a:n→Y" and
A4: "T = Seq2TrSeq(f,a)"
shows
"T : n → (X→X)" and
"∀k∈n. ∀x∈X. (T(k))(x) = f⟨x,a(k)⟩"
proof -
from ‹a:n→Y› have D: "domain(a) = n" using func1_1_L1 by simp
with A2 A3 A4 show "T : n → (X→X)"
using apply_funtype fix_2nd_var_fun ZF_fun_from_total Seq2TrSeq_def
by simp
with A4 D have I: "∀k ∈ n. T(k) = Fix2ndVar(f,a(k))"
using Seq2TrSeq_def ZF_fun_from_tot_val0 by simp
{ fix k fix x assume A5: "k∈n"  "x∈X"
with A1 A3 have "a(k) ∈ Y" using apply_funtype
by auto
with A2 A5 I have "(T(k))(x) = f⟨x,a(k)⟩"
using fix_var_val by simp
} thus "∀k∈n. ∀x∈X. (T(k))(x) = f⟨x,a(k)⟩"
by simp
qed

text‹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 ∈ nat" and A2: "f : X×Y → X" and
A3: "y:n→Y" and A4: "x∈X" and A5: "Y≠0" and
A6: "F = FoldSeq(f,x,y)"
shows
"F: succ(n) → X"
"F(0) = x" and
"∀k∈n. F(succ(k)) = f⟨F(k), y(k)⟩"
proof -
let ?T = "Seq2TrSeq(f,y)"
from A1 A3 have D: "domain(y) = n"
using func1_1_L1 by simp
from ‹f : X×Y → X›  ‹Y≠0› have I: "fstdom(f) = X"
using fstdomdef by simp
with A1 A2 A3 A4 A6 D show
II: "F: succ(n) → X"  and "F(0) = x"
using seq2trans_seq_props FoldSeq_def fin_indseq_var_f_props
by auto
from A1 A2 A3 A4 A6 I D have "∀k∈n. F(succ(k)) = ?T(k)(F(k))"
using seq2trans_seq_props FoldSeq_def fin_indseq_var_f_props
by simp
moreover
{ fix k assume A5: "k∈n" hence "k ∈ succ(n)" by auto
with A1 A2 A3 II A5 have "(?T(k))(F(k)) = f⟨F(k),y(k)⟩"
using apply_funtype seq2trans_seq_props by simp }
ultimately show "∀k∈n. F(succ(k)) = f⟨F(k), y(k)⟩"
by simp
qed

text‹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 ∈ nat"   "k ∈ succ(n)" and
"i ∈ nat"  "f : X×Y → X"  "a : n → Y"  "b : i → Y" and
"n ⊆ i"   "∀j ∈ n. b(j) = a(j)"   "x ∈ X"   "Y ≠ 0"
shows "FoldSeq(f,x,b)(k) = FoldSeq(f,x,a)(k)"
proof -
let ?P = "FoldSeq(f,x,a)"
let ?Q = "FoldSeq(f,x,b)"
from assms have
"n ∈ nat"   "k ∈ succ(n)"
"?Q(0) = ?P(0)" and
"∀j ∈ n. ?Q(j) = ?P(j) ⟶ ?Q(succ(j)) = ?P(succ(j))"
using fold_seq_props by auto
then show  "?Q(k) = ?P(k)" by (rule fin_nat_ind)
qed

text‹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 ∈ nat"   "f : X×Y → X"   "a:n → Y" and
"x∈X"   "k ∈ succ(n)"   "y∈Y"
shows "FoldSeq(f,x,Append(a,y))(k) = FoldSeq(f,x,a)(k)"
proof -
let ?b = "Append(a,y)"
from assms have "?b : succ(n) → Y"  "∀j ∈ n. ?b(j) = a(j)"
using append_props by auto
with assms show ?thesis using foldseq_restrict by blast
qed

text‹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 ∈ nat" and
A2: "f : X×Y → X"  "a:n → Y"  "x∈X"  "Y≠0"
shows
"Fold(f,x,a) =  FoldSeq(f,x,a)(n)" and
"Fold(f,x,a) ∈ X"
proof -
from assms have " FoldSeq(f,x,a) : succ(n) → X"
using  fold_seq_props by simp
with A1 show
"Fold(f,x,a) =  FoldSeq(f,x,a)(n)" and "Fold(f,x,a) ∈ X"
using last_seq_elem apply_funtype Fold_def by auto
qed

text‹A corner case: what happens when we fold an empty list?›

theorem fold_empty: assumes A1: "f : X×Y → X" and
A2: "a:0→Y"  "x∈X"  "Y≠0"
shows "Fold(f,x,a) = x"
proof -
let ?F = "FoldSeq(f,x,a)"
from assms have I:
"0 ∈ nat"  "f : X×Y → X"  "a:0→Y"  "x∈X"  "Y≠0"
by auto
then have "Fold(f,x,a) = ?F(0)" by (rule fold_props)
moreover
from I have
"0 ∈ nat"  "f : X×Y → X"  "a:0→Y"  "x∈X"  "Y≠0" and
"?F = FoldSeq(f,x,a)" by auto
then have "?F(0) = x" by (rule fold_seq_props)
ultimately show "Fold(f,x,a) = x" by simp
qed

text‹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 ∈ nat" and  A2: "f : X×Y → X" and
A3: "a:n→Y" and A4: "x∈X" and A5: "y∈Y"
shows
"FoldSeq(f,x,Append(a,y))(n) = Fold(f,x,a)" and
"Fold(f,x,Append(a,y)) = f⟨Fold(f,x,a), y⟩"
proof -
let ?b = "Append(a,y)"
let ?P = "FoldSeq(f,x,?b)"
from A5 have I: "Y ≠ 0" by auto
with assms show thesis1: "?P(n) = Fold(f,x,a)"
using fold_seq_append fold_props by simp
from assms I have II:
"succ(n) ∈ nat"   "f : X×Y → X"
"?b : succ(n) → Y"   "x∈X"  "Y ≠ 0"
"?P = FoldSeq(f,x,?b)"
using append_props by auto
then have
"∀k ∈ succ(n). ?P(succ(k)) =  f⟨?P(k), ?b(k)⟩"
by (rule fold_seq_props)
with A3 A5 thesis1 have "?P(succ(n)) =  f⟨ Fold(f,x,a), y⟩"
using append_props by auto
moreover
from II have "?P : succ(succ(n)) → X"
by (rule fold_seq_props)
then have "Fold(f,x,?b) = ?P(succ(n))"
using last_seq_elem Fold_def by simp
ultimately show "Fold(f,x,Append(a,y)) = f⟨Fold(f,x,a), y⟩"
by simp
qed

text‹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 ∈ nat" "f : X×Y → X" "x∈X" "∀k∈n #+ 1. q(k) ∈ Y"
shows "Fold(f,x,{⟨k,q(k)⟩. k∈n #+ 1}) = f⟨Fold(f,x,{⟨k,q(k)⟩. k∈n}), q(n)⟩"
proof -
let ?a = "{⟨k,q(k)⟩. k∈n #+ 1}"
let ?b = "{⟨k,q(k)⟩. k∈n}"
from assms have
"Fold(f,x,Append(?b,q(n))) = f⟨Fold(f,x,?b), q(n)⟩"
using ZF_fun_from_total fold_append(2) by simp_all
moreover from assms(1,4) have "?a = Append(?b,q(n))"
using set_list_append1(4) by simp
ultimately show "Fold(f,x,?a) = f⟨Fold(f,x,?b), q(n)⟩"
by simp
qed

text‹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 ∈ nat" "f : X×Y → X" "y:succ(n)→Y" "x∈X"
shows "FoldSeq(f,f⟨x,y(0)⟩,Tail(y)) = Tail(FoldSeq(f,x,y))"
proof -
let ?F = "FoldSeq(f,x,y)"
let ?T = "Tail(?F)"
let ?S = "Seq2TrSeq(f,Tail(y))"
from assms(1,3) have "succ(n) ∈ nat" "0 ∈ succ(n)" "y(0)∈Y"
using empty_in_every_succ apply_funtype by simp_all
have "n ∈ nat" "f⟨x,y(0)⟩ ∈ X" "?S:n→(X→X)"
and "?T:succ(n) → X" "?T(0) = f⟨x,y(0)⟩"
and "∀k∈n. ?T(succ(k)) = (?S(k))(?T(k))"
proof -
from assms(1) show "n ∈ nat" by simp
from assms ‹succ(n) ∈ nat› show "?T:succ(n) → X"
using fold_seq_props(1) tail_props(1) nelist_vals_nonempty by simp
from assms(2,4) ‹y(0)∈Y› show "f⟨x,y(0)⟩ ∈ X"
using apply_funtype by simp
from assms(1,2,3) show "?S:n→(X→X)"
using tail_props(1) seq2trans_seq_props by simp
from assms  have I: "?F:succ(succ(n)) → X"
using fold_seq_props(1) nelist_vals_nonempty by simp
show "?T(0) = f⟨x,y(0)⟩"
proof -
from ‹succ(n) ∈ nat› ‹0 ∈ succ(n)› I
have "?T(0) = ?F(succ(0))"
using tail_props(2) by blast
moreover from assms  ‹0 ∈ succ(n)›
have "?F(succ(0)) = f⟨?F(0), y(0)⟩"
using fold_seq_props(3) nelist_vals_nonempty by blast
moreover from assms  have "?F(0) = x"
using fold_seq_props(2) nelist_vals_nonempty by blast
ultimately show "?T(0) = f⟨x,y(0)⟩" by simp
qed
show "∀k∈n. ?T(succ(k)) = (?S(k))(?T(k))"
proof -
{ fix k assume "k∈n"
with assms(1) have
"succ(k) ∈ succ(n)" "k∈succ(n)" "succ(k) ∈ succ(succ(n))"
using succ_ineq by auto
with ‹succ(n) ∈ nat› I have "?T(succ(k)) = ?F(succ(succ(k)))"
using tail_props(2) by blast
moreover from assms ‹succ(k) ∈ succ(n)›
have "?F(succ(succ(k))) = f⟨?F(succ(k)), y(succ(k))⟩"
using fold_seq_props(3) nelist_vals_nonempty by blast
moreover from assms(1,3) ‹k∈n› have "y(succ(k)) = (Tail(y))(k)"
using tail_props(2) by simp
moreover from assms ‹k∈n› I ‹succ(k) ∈ succ(succ(n))›
have "f⟨?F(succ(k)),(Tail(y))(k)⟩ = (?S(k))(?F(succ(k)))"
using tail_props(1) seq2trans_seq_props(2) apply_funtype
by simp
moreover from ‹succ(n) ∈ nat› I ‹k∈succ(n)›
have "?T(k) = ?F(succ(k))"
using tail_props(2) by blast
ultimately have "?T(succ(k)) = (?S(k))(?T(k))" by simp
} thus ?thesis by simp
qed
qed
then have "?T = InductiveSeqVarFN(f⟨x,y(0)⟩,X,?S,n)"
by (rule is_fin_indseq_var_f)
moreover have "fstdom(f) = X" and "domain(Tail(y)) = n"
proof -
from assms(2,3) show "fstdom(f) = X"
using fstdomdef nelist_vals_nonempty by simp
from assms(1,3) show "domain(Tail(y)) = n"
using tail_props(1) func1_1_L1 by blast
qed
ultimately show ?thesis unfolding FoldSeq_def by simp
qed

text‹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 ∈ nat" "f : X×Y → X" "y:succ(n)→Y" "x∈X"
shows "Fold(f,x,y) = Fold(f,f⟨x,y(0)⟩,Tail(y))"
proof -
from assms have "FoldSeq(f,x,y):succ(succ(n))→X"
using fold_seq_props(1) nelist_vals_nonempty by simp
with assms show ?thesis
using last_tail_last fold_seq_detach_first unfolding Fold_def
by simp
qed

end