theory FiniteSeq_ZF imports Nat_ZF_IML func1
begin
This theory treats finite sequences (i.e. maps \(n\rightarrow X\), where \(n=\{0,1,..,n-1\}\) is a natural number) as lists. It defines and proves the properties of basic operations on lists: concatenation, appending and element etc.
Lists as finite sequences
A natural way of representing (finite) lists in set theory is through (finite) sequences. In such view a list of elements of a set \(X\) is a function that maps the set \(\{0,1,..n-1\}\) into \(X\). Since natural numbers in set theory are defined so that \(n =\{0,1,..n-1\}\), a list of length \(n\) can be understood as an element of the function space \(n\rightarrow X\).
We define the set of lists with values in set \(X\) as \( \text{Lists}(X) \).
definition
\( \text{Lists}(X) \equiv \bigcup n\in nat.\ (n\rightarrow X) \)
The set of nonempty \(X\)-value listst will be called \( \text{NELists}(X) \).
definition
\( \text{NELists}(X) \equiv \bigcup n\in nat.\ (succ(n)\rightarrow X) \)
We first define the shift that moves the second sequence to the domain \(\{n,..,n+k-1\}\), where \(n,k\) are the lengths of the first and the second sequence, resp. To understand the notation in the definitions below recall that in Isabelle/ZF \( pred(n) \) (predecessor of \(n\) is the previous natural number.
definition
\( \text{ShiftedSeq}(b,n) \equiv \{\langle j, b(j - n)\rangle .\ j \in \text{NatInterval}(n,domain(b))\} \)
We define concatenation of two sequences as the union of the first sequence with the shifted second sequence. The result of concatenating lists \(a\) and \(b\) is called \( \text{Concat}(a,b) \).
definition
\( \text{Concat}(a,b) \equiv a \cup \text{ShiftedSeq}(b,domain(a)) \)
For a finite sequence we define the sequence of all elements except the first one. This corresponds to the "tail" function in Haskell. We call it Tail here as well.
definition
\( \text{Tail}(a) \equiv \{\langle k, a(succ(k))\rangle .\ k \in pred(domain(a))\} \)
A dual notion to Tail is the list of all elements of a list except the last one. Borrowing the terminology from Haskell again, we will call this Init.
definition
\( \text{Init}(a) \equiv \text{restrict}(a,pred(domain(a))) \)
Another obvious operation we can talk about is appending an element at the end of a sequence. This is called Append.
definition
\( \text{Append}(a,x) \equiv a \cup \{\langle domain(a),x\rangle \} \)
If lists are modeled as finite sequences (i.e. functions on natural intervals \(\{0,1,..,n-1\} = n\)) it is easy to get the first element of a list as the value of the sequence at \(0\). The last element is the value at \(n-1\). To hide this behind a familiar name we define the Last element of a list.
definition
\( \text{Last}(a) \equiv a(pred(domain(a))) \)
A formula for tail of a finite list.
lemma tail_as_set:
assumes \( n \in nat \) and \( a: n + 1 \rightarrow X \)
shows \( \text{Tail}(a) = \{\langle k,a(k + 1)\rangle .\ k\in n\} \) using assms, func1_1_L1, elem_nat_is_nat(2), succ_add_one(1) unfolding Tail_defFormula for the tail of a list defined by an expression:
lemma tail_formula:
assumes \( n \in nat \) and \( \forall k \in n + 1.\ q(k) \in X \)
shows \( \text{Tail}(\{\langle k,q(k)\rangle .\ k \in n + 1\}) = \{\langle k,q(k + 1)\rangle .\ k \in n\} \)proof let \( a = \{\langle k,q(k)\rangle .\ k \in n + 1\} \)
from assms(2) have \( a : n + 1 \rightarrow X \) by (rule ZF_fun_from_total )
with assms(1) have \( \text{Tail}(a) = \{\langle k,a(k + 1)\rangle .\ k\in n\} \) using tail_as_set
moreover
qed
have \( \forall k\in n.\ a(k + 1) = q(k + 1) \)proof
ultimately show \( thesis \)
{
}
fix \( k \)
assume \( k\in n \)
with assms(1) have \( k + 1 \in n + 1 \) using succ_ineq1, elem_nat_is_nat(2), succ_add_one(1)
then have \( a(k + 1) = q(k + 1) \) by (rule ZF_fun_from_tot_val1 )
thus \( thesis \)
qed
Codomain of a nonempty list is nonempty.
lemma nelist_vals_nonempty:
assumes \( a:succ(n)\rightarrow Y \)
shows \( Y\neq 0 \) using assms, codomain_nonemptyShifted sequence is a function on a the interval of natural numbers.
lemma shifted_seq_props:
assumes A1: \( n \in nat \), \( k \in nat \) and A2: \( b:k\rightarrow X \)
shows \( \text{ShiftedSeq}(b,n): \text{NatInterval}(n,k) \rightarrow X \), \( \forall i \in \text{NatInterval}(n,k).\ \text{ShiftedSeq}(b,n)(i) = b(i - n) \), \( \forall j\in k.\ \text{ShiftedSeq}(b,n)(n + j) = b(j) \)proof let \( I = \text{NatInterval}(n,domain(b)) \)
from A2 have Fact: \( I = \text{NatInterval}(n,k) \) using func1_1_L1
with A1, A2 have \( \forall j\in I.\ b(j - n) \in X \) using inter_diff_in_len, apply_funtype
then have \( \{\langle j, b(j - n)\rangle .\ j \in I\} : I \rightarrow X \) by (rule ZF_fun_from_total )
with Fact show thesis_1: \( \text{ShiftedSeq}(b,n): \text{NatInterval}(n,k) \rightarrow X \) using ShiftedSeq_def
{
fix \( i \)
from Fact, thesis_1 have \( \text{ShiftedSeq}(b,n): I \rightarrow X \)
moreover
assume \( i \in \text{NatInterval}(n,k) \)
with Fact have \( i \in I \)
moreover from Fact have \( \text{ShiftedSeq}(b,n) = \{\langle i, b(i - n)\rangle .\ i \in I\} \) using ShiftedSeq_def
ultimately have \( \text{ShiftedSeq}(b,n)(i) = b(i - n) \) by (rule ZF_fun_from_tot_val )
then show thesis1: \( \forall i \in \text{NatInterval}(n,k).\ \text{ShiftedSeq}(b,n)(i) = b(i - n) \)
{
fix \( j \)
let \( i = n + j \)
assume A3: \( j\in k \)
with A1 have \( j \in nat \) using elem_nat_is_nat
then have \( i - n = j \) using diff_add_inverse
with A3, thesis1 have \( \text{ShiftedSeq}(b,n)(i) = b(j) \) using NatInterval_def
then show \( \forall j\in k.\ \text{ShiftedSeq}(b,n)(n + j) = b(j) \)
qed
A list shifted by a \(0\) is the same list.
lemma seq_shifted_by_zero:
assumes \( n\in nat \), \( b:n\rightarrow X \)
shows \( \text{ShiftedSeq}(b,0) = b \) using assms, func1_1_L1, nat_interval_zero_beg, elem_nat_is_nat(2), fun_is_set_of_pairs unfolding ShiftedSeq_defA shifted empty list is still empty.
lemma empty_shifted_empty:
shows \( \text{ShiftedSeq}(\emptyset ,n) = \emptyset \) using nat_interval_zero_len unfolding ShiftedSeq_defBasis properties of the concatenation of two finite sequences.
theorem concat_props:
assumes A1: \( n \in nat \), \( k \in nat \) and A2: \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \)proof from A1, A2 have \( a:n\rightarrow X \) and I: \( \text{ShiftedSeq}(b,n): \text{NatInterval}(n,k) \rightarrow X \) and \( n \cap \text{NatInterval}(n,k) = 0 \) using shifted_seq_props, length_start_decomp
then have \( a \cup \text{ShiftedSeq}(b,n): n \cup \text{NatInterval}(n,k) \rightarrow X \cup X \) by (rule fun_disjoint_Un )
with A1, A2 show \( \text{Concat}(a,b): n + k \rightarrow X \) using func1_1_L1, Concat_def, length_start_decomp
{
fix \( i \)
assume \( i \in n \)
with A1, I have \( i \notin domain( \text{ShiftedSeq}(b,n)) \) using length_start_decomp, func1_1_L1
with A2 have \( \text{Concat}(a,b)(i) = a(i) \) using func1_1_L1, fun_disjoint_apply1, Concat_def
thus \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \)
{
fix \( i \)
assume A3: \( i \in \text{NatInterval}(n,k) \)
with A1, A2 have \( i \notin domain(a) \) using length_start_decomp, func1_1_L1
with A1, A2, A3 have \( \text{Concat}(a,b)(i) = b(i - n) \) using func1_1_L1, fun_disjoint_apply2, Concat_def, shifted_seq_props
thus II: \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \)
{
fix \( j \)
let \( i = n + j \)
assume A3: \( j\in k \)
with A1 have \( j \in nat \) using elem_nat_is_nat
then have \( i - n = j \) using diff_add_inverse
with A3, II have \( \text{Concat}(a,b)(i) = b(j) \) using NatInterval_def
thus \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \)
qed
Properties of concatenating three lists.
lemma concat_concat_list:
assumes A1: \( n \in nat \), \( k \in nat \), \( m \in nat \) and A2: \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \) and A3: \( d = \text{Concat}( \text{Concat}(a,b),c) \)
shows \( d : n + k + m \rightarrow X \), \( \forall j \in n.\ d(j) = a(j) \), \( \forall j \in k.\ d(n + j) = b(j) \), \( \forall j \in m.\ d(n + k + j) = c(j) \)proof from A1, A2 have I: \( n + k \in nat \), \( m \in nat \), \( \text{Concat}(a,b): n + k \rightarrow X \), \( c:m\rightarrow X \) using concat_props
with A3 show \( d: n #+k + m \rightarrow X \) using concat_props
from I have II: \( \forall i \in n + k.\ \)
\( \text{Concat}( \text{Concat}(a,b),c)(i) = \text{Concat}(a,b)(i) \) by (rule concat_props )
{
fix \( j \)
assume A4: \( j \in n \)
moreover
from A1 have \( n \subseteq n + k \) using add_nat_le
ultimately have \( j \in n + k \)
with A3, II have \( d(j) = \text{Concat}(a,b)(j) \)
with A1, A2, A4 have \( d(j) = a(j) \) using concat_props
thus \( \forall j \in n.\ d(j) = a(j) \)
{
fix \( j \)
assume A5: \( j \in k \)
with A1, A3, II have \( d(n + j) = \text{Concat}(a,b)(n + j) \) using add_lt_mono
also
from A1, A2, A5 have \( \ldots = b(j) \) using concat_props
finally have \( d(n + j) = b(j) \)
thus \( \forall j \in k.\ d(n + j) = b(j) \)
from I have \( \forall j \in m.\ \text{Concat}( \text{Concat}(a,b),c)(n + k + j) = c(j) \) by (rule concat_props )
with A3 show \( \forall j \in m.\ d(n + k + j) = c(j) \)
qed
Properties of concatenating a list with a concatenation of two other lists.
lemma concat_list_concat:
assumes A1: \( n \in nat \), \( k \in nat \), \( m \in nat \) and A2: \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \) and A3: \( e = \text{Concat}(a, \text{Concat}(b,c)) \)
shows \( e : n + k + m \rightarrow X \), \( \forall j \in n.\ e(j) = a(j) \), \( \forall j \in k.\ e(n + j) = b(j) \), \( \forall j \in m.\ e(n + k + j) = c(j) \)proof from A1, A2 have I: \( n \in nat \), \( k + m \in nat \), \( a:n\rightarrow X \), \( \text{Concat}(b,c): k + m \rightarrow X \) using concat_props
with A3 show \( e : n #+k + m \rightarrow X \) using concat_props, add_assoc
from I have \( \forall j \in n.\ \text{Concat}(a, \text{Concat}(b,c))(j) = a(j) \) by (rule concat_props )
with A3 show \( \forall j \in n.\ e(j) = a(j) \)
from I have II: \( \forall j \in k + m.\ \text{Concat}(a, \text{Concat}(b,c))(n + j) = \text{Concat}(b,c)(j) \) by (rule concat_props )
{
fix \( j \)
assume A4: \( j \in k \)
moreover
from A1 have \( k \subseteq k + m \) using add_nat_le
ultimately have \( j \in k + m \)
with A3, II have \( e(n + j) = \text{Concat}(b,c)(j) \)
also
from A1, A2, A4 have \( \ldots = b(j) \) using concat_props
finally have \( e(n + j) = b(j) \)
thus \( \forall j \in k.\ e(n + j) = b(j) \)
{
fix \( j \)
assume A5: \( j \in m \)
with A1, II, A3 have \( e(n + k + j) = \text{Concat}(b,c)(k + j) \) using add_lt_mono, add_assoc
also
from A1, A2, A5 have \( \ldots = c(j) \) using concat_props
finally have \( e(n + k + j) = c(j) \)
then show \( \forall j \in m.\ e(n + k + j) = c(j) \)
qed
Concatenation is associative.
theorem concat_assoc:
assumes A1: \( n \in nat \), \( k \in nat \), \( m \in nat \) and A2: \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \)
shows \( \text{Concat}( \text{Concat}(a,b),c) = \text{Concat}(a, \text{Concat}(b,c)) \)proof let \( d = \text{Concat}( \text{Concat}(a,b),c) \)
let \( e = \text{Concat}(a, \text{Concat}(b,c)) \)
from A1, A2 have \( d : n #+k + m \rightarrow X \) and \( e : n #+k + m \rightarrow X \) using concat_concat_list, concat_list_concat
moreover
qed
have \( \forall i \in n #+k + m.\ d(i) = e(i) \)proof
ultimately show \( d = e \) by (rule func_eq )
{
}
fix \( i \)
assume \( i \in n #+k + m \)
moreover
from A1 have \( n #+k + m = n \cup \text{NatInterval}(n,k) \cup \text{NatInterval}(n + k,m) \) using adjacent_intervals3
ultimately have \( i \in n \vee i \in \text{NatInterval}(n,k) \vee i \in \text{NatInterval}(n + k,m) \)
moreover {
}
moreover {
}
moreover {
}
ultimately have \( d(i) = e(i) \)
assume \( i \in n \)
with A1, A2 have \( d(i) = e(i) \) using concat_concat_list, concat_list_concat
assume \( i \in \text{NatInterval}(n,k) \)
then obtain \( j \) where \( j\in k \) and \( i = n + j \) using NatInterval_def
with A1, A2 have \( d(i) = e(i) \) using concat_concat_list, concat_list_concat
assume \( i \in \text{NatInterval}(n + k,m) \)
then obtain \( j \) where \( j \in m \) and \( i = n + k + j \) using NatInterval_def
with A1, A2 have \( d(i) = e(i) \) using concat_concat_list, concat_list_concat
thus \( thesis \)
qed
Properties of Tail.
theorem tail_props:
assumes A1: \( n \in nat \) and A2: \( a: succ(n) \rightarrow X \)
shows \( \text{Tail}(a) : n \rightarrow X \), \( \forall k \in n.\ \text{Tail}(a)(k) = a(succ(k)) \)proof from A1, A2 have \( \forall k \in n.\ a(succ(k)) \in X \) using succ_ineq, apply_funtype
then have \( \{\langle k, a(succ(k))\rangle .\ k \in n\} : n \rightarrow X \) by (rule ZF_fun_from_total )
with A2 show I: \( \text{Tail}(a) : n \rightarrow X \) using func1_1_L1, pred_succ_eq, Tail_def
moreover
qed
from A2 have \( \text{Tail}(a) = \{\langle k, a(succ(k))\rangle .\ k \in n\} \) using func1_1_L1, pred_succ_eq, Tail_def
ultimately show \( \forall k \in n.\ \text{Tail}(a)(k) = a(succ(k)) \) by (rule ZF_fun_from_tot_val0 )
Essentially the second assertion of tail_props but formulated using notation \(n+1\) instead of \( succ(n) \):
lemma tail_props2:
assumes \( n \in nat \), \( a: n + 1 \rightarrow X \), \( k\in n \)
shows \( \text{Tail}(a)(k) = a(k + 1) \) using assms, succ_add_one(1), tail_props(2), elem_nat_is_nat(2)A nonempty list can be decomposed into concatenation of its first element and the tail.
lemma first_concat_tail:
assumes \( n\in nat \), \( a:succ(n)\rightarrow X \)
shows \( a = \text{Concat}(\{\langle 0,a(0)\rangle \}, \text{Tail}(a)) \)proof let \( b = \text{Concat}(\{\langle 0,a(0)\rangle \}, \text{Tail}(a)) \)
have \( b:succ(n)\rightarrow X \) and \( \forall k\in succ(n).\ a(k) = b(k) \)proof
}
}
from assms(1) have \( 0\in succ(n) \) using empty_in_every_succ
with assms(2) have \( a(0) \in X \) using apply_funtype
then have I: \( \{\langle 0,a(0)\rangle \}:\{0\}\rightarrow X \) using pair_func_singleton
have \( \{0\}\in nat \) using one_is_nat
from assms have \( \text{Tail}(a): n \rightarrow X \) using tail_props(1)
with assms(1), \( \{0\}\in nat \), I have \( b:\{0\} + n \rightarrow X \) using concat_props(1)
with assms(1) show \( b:succ(n) \rightarrow X \) using succ_add_one(3)
{
fix \( k \)
assume \( k\in succ(n) \)
{
assume \( k=0 \)
with assms(1), \( \{0\}\in nat \), I, \( \text{Tail}(a): n \rightarrow X \) have \( a(k) = b(k) \) using concat_props(2), pair_val
moreover {
}
ultimately have \( a(k) = b(k) \)
assume \( k\neq 0 \)
from assms(1), \( k\in succ(n) \) have \( k\in nat \) using elem_nat_is_nat(2)
with \( k\neq 0 \) obtain \( m \) where \( m\in nat \) and \( k=succ(m) \) using Nat_ZF_1_L3
with assms(1), \( k\in succ(n) \) have \( m\in n \) using succ_mem
with \( \{0\}\in nat \), assms(1), I, \( \text{Tail}(a): n \rightarrow X \) have \( b(\{0\} + m) = \text{Tail}(a)(m) \) using concat_props(4)
with assms, \( m\in nat \), \( k\in succ(n) \), \( k=succ(m) \), \( m\in n \) have \( a(k) = b(k) \) using succ_add_one(3), tail_props(2)
thus \( \forall k\in succ(n).\ a(k) = b(k) \)
qed
with assms(2) show \( thesis \) by (rule func_eq )
qed
Properties of Append. It is a bit surprising that the we don't need to assume that \(n\) is a natural number.
theorem append_props:
assumes A1: \( a: n \rightarrow X \) and A2: \( x\in X \) and A3: \( b = \text{Append}(a,x) \)
shows \( b : succ(n) \rightarrow X \), \( \forall k\in n.\ b(k) = a(k) \), \( b(n) = x \)proof note A1
moreover
have I: \( n \notin n \) using mem_not_refl
moreover from A1, A3 have II: \( b = a \cup \{\langle n,x\rangle \} \) using func1_1_L1, Append_def
ultimately have \( b : n \cup \{n\} \rightarrow X \cup \{x\} \) by (rule func1_1_L11D )
with A2 show \( b : succ(n) \rightarrow X \) using succ_explained, set_elem_add
from A1, I, II show \( \forall k\in n.\ b(k) = a(k) \) and \( b(n) = x \) using func1_1_L11D
qed
A special case of append_props: appending to a nonempty list does not change the head (first element) of the list.
corollary head_of_append:
assumes \( n\in nat \) and \( a: succ(n) \rightarrow X \) and \( x\in X \)
shows \( \text{Append}(a,x)(0) = a(0) \) using assms, append_props, empty_in_every_succTail commutes with Append.
theorem tail_append_commute:
assumes A1: \( n \in nat \) and A2: \( a: succ(n) \rightarrow X \) and A3: \( x\in X \)
shows \( \text{Append}( \text{Tail}(a),x) = \text{Tail}( \text{Append}(a,x)) \)proof let \( b = \text{Append}( \text{Tail}(a),x) \)
let \( c = \text{Tail}( \text{Append}(a,x)) \)
from A1, A2 have I: \( \text{Tail}(a) : n \rightarrow X \) using tail_props
from A1, A2, A3 have \( succ(n) \in nat \) and \( \text{Append}(a,x) : succ(succ(n)) \rightarrow X \) using append_props
then have II: \( \forall k \in succ(n).\ c(k) = \text{Append}(a,x)(succ(k)) \) by (rule tail_props )
from assms have \( b : succ(n) \rightarrow X \) and \( c : succ(n) \rightarrow X \) using tail_props, append_props
moreover
qed
have \( \forall k \in succ(n).\ b(k) = c(k) \)proof
ultimately show \( b = c \) by (rule func_eq )
{
}
fix \( k \)
assume \( k \in succ(n) \)
hence \( k \in n \vee k = n \)
moreover {
}
moreover {
}
ultimately have \( b(k) = c(k) \)
assume A4: \( k \in n \)
with assms, II have \( c(k) = a(succ(k)) \) using succ_ineq, append_props
moreover
from A3, I have \( \forall k\in n.\ b(k) = \text{Tail}(a)(k) \) using append_props
with A1, A2, A4 have \( b(k) = a(succ(k)) \) using tail_props
ultimately have \( b(k) = c(k) \)
assume A5: \( k = n \)
with A2, A3, I, II have \( b(k) = c(k) \) using append_props
thus \( thesis \)
qed
NELists are nonempty lists
lemma non_zero_List_func_is_NEList:
shows \( \text{NELists}(X) = \{a\in \text{Lists}(X).\ a\neq 0\} \)proof{
}
}
fix \( a \)
assume as: \( a\in \{a\in \text{Lists}(X).\ a\neq 0\} \)
from as obtain \( n \) where a: \( n\in nat \), \( a:n\rightarrow X \) unfolding Lists_def
{
assume \( n=0 \)
with a(2) have \( a=0 \) unfolding Pi_def
with as have \( False \)
hence \( n\neq 0 \)
with a(1) obtain \( k \) where \( k\in nat \), \( n=succ(k) \) using Nat_ZF_1_L3
with a(2) have \( a \in \text{NELists}(X) \) unfolding NELists_def
moreover {
}
}
ultimately show \( thesis \)
qed
fix \( a \)
assume as: \( a\in \text{NELists}(X) \)
then obtain \( k \) where k: \( a:succ(k)\rightarrow X \), \( k\in nat \) unfolding NELists_def
{
assume \( a=0 \)
hence \( domain(a) = 0 \)
with k(1) have \( succ(k) = 0 \) using domain_of_fun
hence \( False \)
moreover {
}
ultimately have \( a\in \{a\in \text{Lists}(X).\ a\neq 0\} \)
from k(2) have \( succ(k)\in nat \) using nat_succI
with k(1) have \( a\in \text{Lists}(X) \) unfolding Lists_def
Properties of Init.
theorem init_props:
assumes A1: \( n \in nat \) and A2: \( a: succ(n) \rightarrow X \)
shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \)proof have \( n \subseteq succ(n) \)
with A2 have \( \text{restrict}(a,n): n \rightarrow X \) using restrict_type2
moreover
{
from A1, A2 have I: \( \text{restrict}(a,n) = \text{Init}(a) \) using func1_1_L1, pred_succ_eq, Init_def
ultimately show thesis1: \( \text{Init}(a) : n \rightarrow X \)
fix \( k \)
assume \( k\in n \)
then have \( \text{restrict}(a,n)(k) = a(k) \) using restrict
with I have \( \text{Init}(a)(k) = a(k) \)
then show thesis2: \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \)
let \( b = \text{Append}( \text{Init}(a), a(n)) \)
from A2, thesis1 have II: \( \text{Init}(a) : n \rightarrow X \), \( a(n) \in X \), \( b = \text{Append}( \text{Init}(a), a(n)) \) using apply_funtype
note A2
moreover
qed
from II have \( b : succ(n) \rightarrow X \) by (rule append_props )
moreover have \( \forall k \in succ(n).\ a(k) = b(k) \)proof
ultimately show \( a = b \) by (rule func_eq )
{
}
fix \( k \)
assume A3: \( k \in n \)
from II have \( \forall j\in n.\ b(j) = \text{Init}(a)(j) \) by (rule append_props )
with thesis2, A3 have \( a(k) = b(k) \)
moreover
qed
from II have \( b(n) = a(n) \) by (rule append_props )
hence \( a(n) = b(n) \)
ultimately show \( \forall k \in succ(n).\ a(k) = b(k) \)
The initial part of a nonempty list is a list, and the domain of the original list is the successor of its initial part.
theorem init_NElist:
assumes \( a \in \text{NELists}(X) \)
shows \( \text{Init}(a) \in \text{Lists}(X) \) and \( succ(domain( \text{Init}(a))) = domain(a) \)proof from assms obtain \( n \) where n: \( n\in nat \), \( a:succ(n) \rightarrow X \) unfolding NELists_def
then have tailF: \( \text{Init}(a):n \rightarrow X \) using init_props(1)
with n(1) show \( \text{Init}(a) \in \text{Lists}(X) \) unfolding Lists_def
from tailF have \( domain( \text{Init}(a)) = n \) using domain_of_fun
moreover
qed
from n(2) have \( domain(a) = succ(n) \) using domain_of_fun
ultimately show \( succ(domain( \text{Init}(a))) = domain(a) \)
If we take init of the result of append, we get back the same list.
lemma init_append:
assumes A1: \( n \in nat \) and A2: \( a:n\rightarrow X \) and A3: \( x \in X \)
shows \( \text{Init}( \text{Append}(a,x)) = a \)proof from A2, A3 have \( \text{Append}(a,x): succ(n)\rightarrow X \) using append_props
with A1 have \( \text{Init}( \text{Append}(a,x)):n\rightarrow X \) and \( \forall k\in n.\ \text{Init}( \text{Append}(a,x))(k) = \text{Append}(a,x)(k) \) using init_props
with A2, A3 have \( \forall k\in n.\ \text{Init}( \text{Append}(a,x))(k) = a(k) \) using append_props
with \( \text{Init}( \text{Append}(a,x)):n\rightarrow X \), A2 show \( thesis \) by (rule func_eq )
qed
A reformulation of definition of Init.
lemma init_def:
assumes \( n \in nat \) and \( a:succ(n)\rightarrow X \)
shows \( \text{Init}(a) = \text{restrict}(a,n) \) using assms, func1_1_L1, Init_defAnother reformulation of the definition of Init, starting with the expression defining the list.
lemma init_def_alt:
assumes \( n\in nat \) and \( \forall k\in n + 1.\ q(k) \in X \)
shows \( \text{Init}(\{\langle k,q(k)\rangle .\ k\in n + 1\}) = \{\langle k,q(k)\rangle .\ k\in n\} \)proof let \( a = \{\langle k,q(k)\rangle .\ k\in n + 1\} \)
from assms(2) have \( a:n + 1\rightarrow X \) by (rule ZF_fun_from_total )
moreover
from assms(1) have \( n + 1 = succ(n) \) using succ_add_one(1)
ultimately have \( a:succ(n)\rightarrow X \)
with assms(1) have \( \text{Init}(a) = \text{restrict}(a,n) \) using init_def
moreover
qed
from assms(1) have \( n \subseteq n + 1 \)
then have \( \text{restrict}(a,n) = \{\langle k,q(k)\rangle .\ k\in n\} \) by (rule restrict_def_alt )
ultimately show \( thesis \)
A lemma about extending a finite sequence by one more value. This is just a more explicit version of append_props.
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 \) using assms, Append_def, func1_1_L1, append_propsThe next lemma is a bit displaced as it is mainly about finite sets. It is proven here because it uses the notion of Append. Suppose we have a list of element of \(A\) is a bijection. Then for every element that does not belong to \(A\) we can we can construct a bijection for the set \(A \cup \{ x\}\) by appending \(x\). This is just a specialised version of lemma bij_extend_point from func1.thy.
lemma bij_append_point:
assumes A1: \( n \in nat \) and A2: \( b \in \text{bij}(n,X) \) and A3: \( x \notin X \)
shows \( \text{Append}(b,x) \in \text{bij}(succ(n), X \cup \{x\}) \)proof from A2, A3 have \( b \cup \{\langle n,x\rangle \} \in \text{bij}(n \cup \{n\},X \cup \{x\}) \) using mem_not_refl, bij_extend_point
moreover
qed
have \( \text{Append}(b,x) = b \cup \{\langle n,x\rangle \} \)proof
ultimately show \( thesis \) using succ_explained
from A2 have \( b:n\rightarrow X \) using bij_def, surj_def
then have \( b : n \rightarrow X \cup \{x\} \) using func1_1_L1B
then show \( \text{Append}(b,x) = b \cup \{\langle n,x\rangle \} \) using Append_def, func1_1_L1
qed
The next lemma rephrases the definition of Last. Recall that in ZF we have \(\{0,1,2,..,n\} = n+1=\)succ\((n)\).
lemma last_seq_elem:
assumes \( a: succ(n) \rightarrow X \)
shows \( \text{Last}(a) = a(n) \) using assms, func1_1_L1, pred_succ_eq, Last_defThe last element of a nonempty list valued in \(X\) is in \(X\).
lemma last_type:
assumes \( a \in \text{NELists}(X) \)
shows \( \text{Last}(a) \in X \) using assms, last_seq_elem, apply_funtype unfolding NELists_defThe last element of a list of length at least 2 is the same as the last element of the tail of that list.
lemma last_tail_last:
assumes \( n\in nat \), \( a: succ(succ(n)) \rightarrow X \)
shows \( \text{Last}( \text{Tail}(a)) = \text{Last}(a) \)proof from assms have \( \text{Last}( \text{Tail}(a)) = \text{Tail}(a)(n) \) using tail_props(1), last_seq_elem
also
qed
from assms have \( \text{Tail}(a)(n) = a(succ(n)) \) using tail_props(2)
also from assms(2) have \( a(succ(n)) = \text{Last}(a) \) using last_seq_elem
finally show \( thesis \)
If two finite sequences are the same when restricted to domain one shorter than the original and have the same value on the last element, then they are equal.
lemma finseq_restr_eq:
assumes A1: \( n \in nat \) and A2: \( a: succ(n) \rightarrow X \), \( b: succ(n) \rightarrow X \) and A3: \( \text{restrict}(a,n) = \text{restrict}(b,n) \) and A4: \( a(n) = b(n) \)
shows \( a = b \)proof{
}
fix \( k \)
assume \( k \in succ(n) \)
then have \( k \in n \vee k = n \)
moreover {
}
moreover {
}
ultimately have \( a(k) = b(k) \)
assume \( k \in n \)
then have \( \text{restrict}(a,n)(k) = a(k) \) and \( \text{restrict}(b,n)(k) = b(k) \) using restrict
with A3 have \( a(k) = b(k) \)
assume \( k = n \)
with A4 have \( a(k) = b(k) \)
then have \( \forall k \in succ(n).\ a(k) = b(k) \)
with A2 show \( a = b \) by (rule func_eq )
qed
Concatenating a list of length \(1\) is the same as appending its first (and only) element. Recall that in ZF set theory \(1 = \{ 0 \} \).
lemma append_1elem:
assumes A1: \( n \in nat \) and A2: \( a: n \rightarrow X \) and A3: \( b : 1 \rightarrow X \)
shows \( \text{Concat}(a,b) = \text{Append}(a,b(0)) \)proof let \( C = \text{Concat}(a,b) \)
let \( A = \text{Append}(a,b(0)) \)
from A1, A2, A3 have I: \( n \in nat \), \( 1 \in nat \), \( a:n\rightarrow X \), \( b:1\rightarrow X \)
have \( C : succ(n) \rightarrow X \)proof
from I have \( C : n + 1 \rightarrow X \) by (rule concat_props )
with A1 show \( C : succ(n) \rightarrow X \)
qed
moreover
qed
from A2, A3 have \( A : succ(n) \rightarrow X \) using apply_funtype, append_props
moreover have \( \forall k \in succ(n).\ C(k) = A(k) \)proof
ultimately show \( C = A \) by (rule func_eq )
fix \( k \)
assume \( k \in succ(n) \)
moreover {
}
moreover
qed
assume \( k \in n \)
moreover
from I have \( \forall i \in n.\ C(i) = a(i) \) by (rule concat_props )
moreover from A2, A3 have \( \forall i\in n.\ A(i) = a(i) \) using apply_funtype, append_props
ultimately have \( C(k) = A(k) \)
have \( C(n) = A(n) \)proof
ultimately show \( C(k) = A(k) \)
from I have \( \forall j \in 1.\ C(n + j) = b(j) \) by (rule concat_props )
with A1, A2, A3 show \( C(n) = A(n) \) using apply_funtype, append_props
qed
If \(x\in X\) then the singleton set with the pair \(\langle 0,x\rangle\) as the only element is a list of length 1 and hence a nonempty list.
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) \)proof from assms have \( \{\langle 0,x\rangle \} : \{0\} \rightarrow X \) using pair_func_singleton
moreover
qed
have \( \{0\} = 1 \)
ultimately show \( \{\langle 0,x\rangle \} : 1 \rightarrow X \) and \( \{\langle 0,x\rangle \} \in \text{NELists}(X) \) unfolding NELists_def
A singleton list is in fact a singleton set with a pair as the only element.
lemma list_singleton_pair:
assumes A1: \( x:1\rightarrow X \)
shows \( x = \{\langle 0,x(0)\rangle \} \)proof from A1 have \( x = \{\langle t,x(t)\rangle .\ t\in 1\} \) by (rule fun_is_set_of_pairs )
hence \( x = \{\langle t,x(t)\rangle .\ t\in \{0\} \} \)
thus \( thesis \)
qed
When we append an element to the empty list we get a list with length \(1\).
lemma empty_append1:
assumes A1: \( x\in X \)
shows \( \text{Append}(0,x): 1 \rightarrow X \) and \( \text{Append}(0,x)(0) = x \)proof let \( a = \text{Append}(0,x) \)
have \( a = \{\langle 0,x\rangle \} \) using Append_def
with A1 show \( a : 1 \rightarrow X \) and \( a(0) = x \) using list_len1_singleton, pair_func_singleton
qed
Concatenating with an empty list gives the same list. Recall that an empty list is in fact an empty set (see fun_empty_empty in func1 theory.
lemma concat_empty:
assumes \( n\in nat \), \( x:n\rightarrow X \)
shows \( \text{Concat}(x,\emptyset ) = x \) and \( \text{Concat}(\emptyset ,x) = x \) using assms, empty_shifted_empty, seq_shifted_by_zero unfolding Concat_defAppending an element is the same as concatenating with certain pair.
lemma append_concat_pair:
assumes \( n \in nat \) and \( a: n \rightarrow X \) and \( x\in X \)
shows \( \text{Append}(a,x) = \text{Concat}(a,\{\langle 0,x\rangle \}) \) using assms, list_len1_singleton, append_1elem, pair_valAn associativity property involving concatenation and appending. For proof we just convert appending to concatenation and use concat_assoc.
lemma concat_append_assoc:
assumes A1: \( n \in nat \), \( k \in nat \) and A2: \( a:n\rightarrow X \), \( b:k\rightarrow X \) and A3: \( x \in X \)
shows \( \text{Append}( \text{Concat}(a,b),x) = \text{Concat}(a, \text{Append}(b,x)) \)proof from A1, A2, A3 have \( n + k \in nat \), \( \text{Concat}(a,b) : n + k \rightarrow X \), \( x \in X \) using concat_props
then have \( \text{Append}( \text{Concat}(a,b),x) = \text{Concat}( \text{Concat}(a,b),\{\langle 0,x\rangle \}) \) by (rule append_concat_pair )
moreover
qed
from A1, A2, A3 have \( n \in nat \), \( k \in nat \), \( 1 \in nat \), \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( \{\langle 0,x\rangle \} : 1 \rightarrow X \) using list_len1_singleton
then have \( \text{Concat}( \text{Concat}(a,b),\{\langle 0,x\rangle \}) = \text{Concat}(a, \text{Concat}(b,\{\langle 0,x\rangle \})) \) by (rule concat_assoc )
moreover from A1, A2, A3 have \( \text{Concat}(b,\{\langle 0,x\rangle \}) = \text{Append}(b,x) \) using list_len1_singleton, append_1elem, pair_val
ultimately show \( \text{Append}( \text{Concat}(a,b),x) = \text{Concat}(a, \text{Append}(b,x)) \)
An identity involving concatenating with init and appending the last element.
lemma concat_init_last_elem:
assumes \( n \in nat \), \( k \in nat \) and \( a: n \rightarrow X \) and \( b : succ(k) \rightarrow X \)
shows \( \text{Append}( \text{Concat}(a, \text{Init}(b)),b(k)) = \text{Concat}(a,b) \) using assms, init_props, apply_funtype, concat_append_assocA lemma about creating lists by composition and how Append behaves in such case.
lemma list_compose_append:
assumes A1: \( n \in nat \) and A2: \( a : n \rightarrow X \) and A3: \( x \in X \) and A4: \( c : X \rightarrow Y \)
shows \( c\circ \text{Append}(a,x) : succ(n) \rightarrow Y \), \( c\circ \text{Append}(a,x) = \text{Append}(c\circ a, c(x)) \)proof let \( b = \text{Append}(a,x) \)
let \( d = \text{Append}(c\circ a, c(x)) \)
from A2, A4 have \( c\circ a : n \rightarrow Y \) using comp_fun
from A2, A3 have \( b : succ(n) \rightarrow X \) using append_props
with A4 show \( c\circ b : succ(n) \rightarrow Y \) using comp_fun
moreover
qed
from A3, A4, \( c\circ a : n \rightarrow Y \) have \( d: succ(n) \rightarrow Y \) using apply_funtype, append_props
moreover have \( \forall k \in succ(n).\ (c\circ b) (k) = d(k) \)proof
ultimately show \( c\circ b = d \) by (rule func_eq )
{
}
fix \( k \)
assume \( k \in succ(n) \)
with \( b : succ(n) \rightarrow X \) have \( (c\circ b) (k) = c(b(k)) \) using comp_fun_apply
with A2, A3, A4, \( c\circ a : n \rightarrow Y \), \( c\circ a : n \rightarrow Y \), \( k \in succ(n) \) have \( (c\circ b) (k) = d(k) \) using append_props, comp_fun_apply, apply_funtype
thus \( thesis \)
qed
Composition commutes with concatenation i.e. composition with a concatenation is concatenation of compositions.
lemma list_compose_concat:
assumes \( n \in nat \), \( m\in nat \), \( a:n\rightarrow X \), \( b:m\rightarrow X \), \( c:X\rightarrow Y \)
shows \( c\circ \text{Concat}(a,b) = \text{Concat}(c\circ a, c\circ b) \)proof let \( L = c\circ \text{Concat}(a,b) \)
let \( R = \text{Concat}(c\circ a, c\circ b) \)
from assms(1,2,3,4) have \( \text{Concat}(a,b):n + m \rightarrow X \) using concat_props(1)
with assms(5) have \( L : n + m \rightarrow Y \) using comp_fun
moreover
}
qed
from assms(3,4,5) have I: \( (c\circ a): n\rightarrow Y \), \( (c\circ b): m\rightarrow Y \) using comp_fun
with assms(1,2) have \( R : n + m \rightarrow Y \) using concat_props(1)
moreover {
fix \( i \)
assume \( i \in n + m \)
with assms(1,2), \( \text{Concat}(a,b):n + m \rightarrow X \) have II: \( L(i) = c( \text{Concat}(a,b)(i)) \), \( i \in n\cup \text{NatInterval}(n,m) \) using comp_fun_apply, length_start_decomp(2)
hence \( i \in n \vee i \in \text{NatInterval}(n,m) \)
moreover {
}
moreover {
}
ultimately have \( L(i) = R(i) \)
assume \( i\in n \)
with assms(1,2,3,4), I, II have \( L(i) = R(i) \) using concat_props(2), comp_fun_apply
assume \( i\in \text{NatInterval}(n,m) \)
with assms(1,2,3,4), I, II have \( L(i) = R(i) \) using inter_diff_in_len, concat_props(3), comp_fun_apply
hence \( \forall i \in n + m.\ L(i) = R(i) \)
ultimately show \( L = R \) by (rule func_eq )
A lemma about appending an element to a list defined by set comprehension.
lemma set_list_append:
assumes A1: \( \forall i \in succ(k).\ b(i) \in X \) and A2: \( a = \{\langle i,b(i)\rangle .\ i \in succ(k)\} \)
shows \( a: succ(k) \rightarrow X \), \( \{\langle i,b(i)\rangle .\ i \in k\}: k \rightarrow X \), \( a = \text{Append}(\{\langle i,b(i)\rangle .\ i \in k\},b(k)) \)proof from A1 have \( \{\langle i,b(i)\rangle .\ i \in succ(k)\} : succ(k) \rightarrow X \) by (rule ZF_fun_from_total )
with A2 show \( a: succ(k) \rightarrow X \)
from A1 have \( \forall i \in k.\ b(i) \in X \)
then show \( \{\langle i,b(i)\rangle .\ i \in k\}: k \rightarrow X \) by (rule ZF_fun_from_total )
with A2 show \( a = \text{Append}(\{\langle i,b(i)\rangle .\ i \in k\},b(k)) \) using func1_1_L1, Append_def
qed
A version of set_list_append using \(n+1\) instead of \( succ(n) \).
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)) \)proof from assms(1) have I: \( n + 1 = succ(n) \) using succ_add_one(1)
with assms show \( a: n + 1 \rightarrow X \) and \( \{\langle k,q(k)\rangle .\ k \in n\}: n \rightarrow X \) and II: \( \text{Init}(a) = \{\langle k,q(k)\rangle .\ k \in n\} \) using set_list_append(1,2), init_def_alt
from assms(2,3), I have \( \forall k\in succ(n).\ q(k) \in X \) and \( a = \{\langle k,q(k)\rangle .\ k \in succ(n)\} \)
then show \( a = \text{Append}(\{\langle k,q(k)\rangle .\ k \in n\},q(n)) \) using set_list_append(3)
with II show \( a = \text{Append}( \text{Init}(a), q(n)) \)
from I have \( n \in n + 1 \)
then have \( \{\langle k,q(k)\rangle .\ k\in n + 1\}(n) = q(n) \) by (rule ZF_fun_from_tot_val1 )
with assms(3), \( a = \text{Append}( \text{Init}(a), q(n)) \) show \( a = \text{Append}( \text{Init}(a), a(n)) \)
qed
An induction theorem for lists.
lemma list_induct:
assumes A1: \( \forall b\in 1\rightarrow X.\ P(b) \) and A2: \( \forall b\in \text{NELists}(X).\ P(b) \longrightarrow (\forall x\in X.\ P( \text{Append}(b,x))) \) and A3: \( d \in \text{NELists}(X) \)
shows \( P(d) \)proof{
}
fix \( n \)
assume \( n\in nat \)
moreover
from A1 have \( \forall b\in succ(0)\rightarrow X.\ P(b) \)
moreover have \( \forall k\in nat.\ ((\forall b\in succ(k)\rightarrow X.\ P(b)) \longrightarrow (\forall c\in succ(succ(k))\rightarrow X.\ P(c))) \)proof
ultimately have \( \forall b\in succ(n)\rightarrow X.\ P(b) \) by (rule ind_on_nat )
{
}
fix \( k \)
assume \( k \in nat \)
assume \( \forall b\in succ(k)\rightarrow X.\ P(b) \)
have \( \forall c\in succ(succ(k))\rightarrow X.\ P(c) \)proof
fix \( c \)
assume \( c: succ(succ(k))\rightarrow X \)
let \( b = \text{Init}(c) \)
let \( x = c(succ(k)) \)
from \( k \in nat \), \( c: succ(succ(k))\rightarrow X \) have \( b:succ(k)\rightarrow X \) using init_props
with A2, \( k \in nat \), \( \forall b\in succ(k)\rightarrow X.\ P(b) \) have \( \forall x\in X.\ P( \text{Append}(b,x)) \) using NELists_def
with \( c: succ(succ(k))\rightarrow X \) have \( P( \text{Append}(b,x)) \) using apply_funtype
with \( k \in nat \), \( c: succ(succ(k))\rightarrow X \) show \( P(c) \) using init_props
qed
thus \( thesis \)
qed
with A3 show \( thesis \) using NELists_def
qed
A dual notion to Append is Prepend where we add an element to the list at the beginning of the list. We define the value of the list \(a\) prepended by an element \(x\) as \(x\) if index is 0 and \(a(k-1)\) otherwise.
definition
\( \text{Prepend}(a,x) \equiv \{\langle k,\text{if }k = 0\text{ then }x\text{ else }a(k - 1)\rangle .\ k\in domain(a) + 1\} \)
If \(a:n\rightarrow X\) is a list, then \(a\) with prepended \(x\in X\) is a list as well and its first element is \(x\).
lemma prepend_props:
assumes \( n\in nat \), \( a:n\rightarrow X \), \( x\in X \)
shows \( \text{Prepend}(a,x):(n + 1)\rightarrow X \) and \( \text{Prepend}(a,x)(0) = x \)proof let \( b = \{\langle k,\text{if }k = 0\text{ then }x\text{ else }a(k - 1)\rangle .\ k\in n + 1\} \)
have \( \forall k\in n + 1.\ (\text{if }k = 0\text{ then }x\text{ else }a(k - 1)) \in X \)proof
{
}
}
fix \( k \)
assume \( k \in n + 1 \)
let \( v = \text{if }k = 0\text{ then }x\text{ else }a(k - 1) \)
{
assume \( k\neq 0 \)
with \( k \in n + 1 \) have \( n\neq 0 \)
from assms(1), \( k \in n + 1 \) have \( k \in nat \) using elem_nat_is_nat(2)
from assms(1) have \( succ(n) = n + 1 \) using succ_add_one(1)
with \( k \in n + 1 \) have \( k\in succ(n) \)
with assms(1), \( n\neq 0 \) have \( pred(k) \in n \) using pred_succ_mem
with assms(2), \( k \in nat \), \( k\neq 0 \) have \( v\in X \) using pred_minus_one, apply_funtype
with assms(3) have \( v \in X \)
thus \( thesis \)
qed
then have \( b: (n + 1)\rightarrow X \) by (rule ZF_fun_from_total )
with assms(2) show \( \text{Prepend}(a,x):(n + 1)\rightarrow X \) using func1_1_L1 unfolding Prepend_def
from assms(1) have \( 0 \in n + 1 \) using succ_add_one(1), empty_in_every_succ
then have \( b(0) = (\text{if }0 = 0\text{ then }x\text{ else }a(0 - 1)) \) by (rule ZF_fun_from_tot_val1 )
with assms(2) show \( \text{Prepend}(a,x)(0) = x \) using func1_1_L1 unfolding Prepend_def
qed
When prepending an element to a list the values at positive indices do not change.
lemma prepend_val:
assumes \( n\in nat \), \( a:n\rightarrow X \), \( x\in X \), \( k\in n \)
shows \( \text{Prepend}(a,x)(k + 1) = a(k) \)proof let \( b = \{\langle k,\text{if }k = 0\text{ then }x\text{ else }a(k - 1)\rangle .\ k\in n + 1\} \)
from assms(1,4) have \( k\in nat \) using elem_nat_is_nat(2)
with assms(1) have \( succ(n) = n + 1 \) and \( succ(k) = k + 1 \) using succ_add_one(1)
with assms(1,4) have \( k + 1 \in n + 1 \) using succ_ineq
from \( k + 1 \in n + 1 \) have \( b(k + 1) = (\text{if }k + 1 = 0\text{ then }x\text{ else }a((k + 1) - 1)) \) by (rule ZF_fun_from_tot_val1 )
with assms(2), \( k\in nat \) show \( thesis \) using func1_1_L1 unfolding Prepend_def
qed
The tail of a list prepended by an element is equal to the list.
lemma tail_prepend:
assumes \( n\in nat \), \( a:n\rightarrow X \), \( x\in X \)
shows \( \text{Tail}( \text{Prepend}(a,x)) = a \)proof let \( b = \text{Prepend}(a,x) \)
from assms have \( b:(n + 1)\rightarrow X \) using prepend_props(1)
with assms(1) have \( \text{Tail}(b):n\rightarrow X \) using tail_props(1)
from assms, \( b:(n + 1)\rightarrow X \) have \( \forall k\in n.\ \text{Tail}(b)(k) = a(k) \) using tail_props2, prepend_val
with assms(2), \( \text{Tail}(b):n\rightarrow X \) show \( thesis \) using func_eq
qed
Lists and cartesian products
Lists of length \(n\) of elements of some set \(X\) can be thought of as a model of the cartesian product \(X^n\) which is more convenient in many applications.
There is a natural bijection between the space \((n+1)\rightarrow X\) of lists of length \(n+1\) of elements of \(X\) and the cartesian product \((n\rightarrow X)\times X\).
lemma lists_cart_prod:
assumes \( n \in nat \)
shows \( \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in succ(n)\rightarrow X\} \in \text{bij}(succ(n)\rightarrow X,(n\rightarrow X)\times X) \)proof let \( f = \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in succ(n)\rightarrow X\} \)
from assms have \( \forall x \in succ(n)\rightarrow X.\ \langle \text{Init}(x),x(n)\rangle \in (n\rightarrow X)\times X \) using init_props, succ_iff, apply_funtype
then have I: \( f: (succ(n)\rightarrow X)\rightarrow ((n\rightarrow X)\times X) \) by (rule ZF_fun_from_total )
moreover
qed
from assms, I have \( \forall x\in succ(n)\rightarrow X.\ \forall y\in succ(n)\rightarrow X.\ f(x)=f(y) \longrightarrow x=y \) using ZF_fun_from_tot_val, init_def, finseq_restr_eq
moreover have \( \forall p\in (n\rightarrow X)\times X.\ \exists x\in succ(n)\rightarrow X.\ f(x) = p \)proof
ultimately show \( thesis \) using inj_def, surj_def, bij_def
fix \( p \)
assume \( p \in (n\rightarrow X)\times X \)
let \( x = \text{Append}(\text{fst}(p),\text{snd}(p)) \)
from assms, \( p \in (n\rightarrow X)\times X \) have \( x:succ(n)\rightarrow X \) using append_props
with I have \( f(x) = \langle \text{Init}(x),x(n)\rangle \) using succ_iff, ZF_fun_from_tot_val
moreover
qed
from assms, \( p \in (n\rightarrow X)\times X \) have \( \text{Init}(x) = \text{fst}(p) \) and \( x(n) = \text{snd}(p) \) using init_append, append_props
ultimately have \( f(x) = \langle \text{fst}(p),\text{snd}(p)\rangle \)
with \( p \in (n\rightarrow X)\times X \), \( x:succ(n)\rightarrow X \) show \( \exists x\in succ(n)\rightarrow X.\ f(x) = p \)
We can identify a set \(X\) with lists of length one of elements of \(X\).
lemma singleton_list_bij:
shows \( \{\langle x,x(0)\rangle .\ x\in 1\rightarrow X\} \in \text{bij}(1\rightarrow X,X) \)proof let \( f = \{\langle x,x(0)\rangle .\ x\in 1\rightarrow X\} \)
have \( \forall x\in 1\rightarrow X.\ x(0) \in X \) using apply_funtype
then have I: \( f:(1\rightarrow X)\rightarrow X \) by (rule ZF_fun_from_total )
moreover
qed
have \( \forall x\in 1\rightarrow X.\ \forall y\in 1\rightarrow X.\ f(x) = f(y) \longrightarrow x=y \)proof
moreover {
}
fix \( x \) \( y \)
assume \( x:1\rightarrow X \), \( y:1\rightarrow X \) and \( f(x) = f(y) \)
with I have \( x(0) = y(0) \) using ZF_fun_from_tot_val
moreover
from \( x:1\rightarrow X \), \( y:1\rightarrow X \) have \( x = \{\langle 0,x(0)\rangle \} \) and \( y = \{\langle 0,y(0)\rangle \} \) using list_singleton_pair
ultimately have \( x=y \)
thus \( thesis \)
qed
have \( \forall y\in X.\ \exists x\in 1\rightarrow X.\ f(x)=y \)proof
ultimately show \( thesis \) using inj_def, surj_def, bij_def
fix \( y \)
assume \( y\in X \)
let \( x = \{\langle 0,y\rangle \} \)
from I, \( y\in X \) have \( x:1\rightarrow X \) and \( f(x) = y \) using list_len1_singleton, ZF_fun_from_tot_val, pair_val
thus \( \exists x\in 1\rightarrow X.\ f(x)=y \)
qed
We can identify a set of \(X\)-valued lists of length with \(X\).
lemma list_singleton_bij:
shows \( \{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\} \in \text{bij}(X,1\rightarrow X) \) and \( \{\langle y,y(0)\rangle .\ y\in 1\rightarrow X\} = converse(\{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\}) \) and \( \{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\} = converse(\{\langle y,y(0)\rangle .\ y\in 1\rightarrow X\}) \)proof let \( f = \{\langle y,y(0)\rangle .\ y\in 1\rightarrow X\} \)
let \( g = \{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\} \)
have \( 1 = \{0\} \)
then have \( f \in \text{bij}(1\rightarrow X,X) \) and \( g:X\rightarrow (1\rightarrow X) \) using singleton_list_bij, pair_func_singleton, ZF_fun_from_total
moreover
qed
have \( \forall y\in 1\rightarrow X.\ g(f(y)) = y \)proof
ultimately show \( g \in \text{bij}(X,1\rightarrow X) \) and \( f = converse(g) \) and \( g = converse(f) \) using comp_conv_id
fix \( y \)
assume \( y:1\rightarrow X \)
have \( f:(1\rightarrow X)\rightarrow X \) using singleton_list_bij, bij_def, inj_def
with \( 1 = \{0\} \), \( y:1\rightarrow X \), \( g:X\rightarrow (1\rightarrow X) \) show \( g(f(y)) = y \) using ZF_fun_from_tot_val, apply_funtype, func_singleton_pair
qed
What is the inverse image of a set by the natural bijection between \(X\)-valued singleton lists and \(X\)?
lemma singleton_vimage:
assumes \( U\subseteq X \)
shows \( \{x\in 1\rightarrow X.\ x(0) \in U\} = \{ \{\langle 0,y\rangle \}.\ y\in U\} \)proof have \( 1 = \{0\} \)
{
fix \( x \)
assume \( x \in \{x\in 1\rightarrow X.\ x(0) \in U\} \)
with \( 1 = \{0\} \) have \( x = \{\langle 0, x(0)\rangle \} \) using func_singleton_pair
thus \( \{x\in 1\rightarrow X.\ x(0) \in U\} \subseteq \{ \{\langle 0,y\rangle \}.\ y\in U\} \)
{
fix \( x \)
assume \( x \in \{ \{\langle 0,y\rangle \}.\ y\in U\} \)
then obtain \( y \) where \( x = \{\langle 0,y\rangle \} \) and \( y\in U \)
with \( 1 = \{0\} \), assms have \( x:1\rightarrow X \) using pair_func_singleton
thus \( \{ \{\langle 0,y\rangle \}.\ y\in U\} \subseteq \{x\in 1\rightarrow X.\ x(0) \in U\} \)
qed
A technical lemma about extending a list by values from a set.
lemma list_append_from:
assumes A1: \( n \in nat \) and A2: \( U \subseteq n\rightarrow X \) and A3: \( V \subseteq X \)
shows \( \{x \in succ(n)\rightarrow X.\ \text{Init}(x) \in U \wedge x(n) \in V\} = (\bigcup y\in V.\ \{ \text{Append}(x,y).\ x\in U\}) \)proof{
}
fix \( x \)
assume \( x \in \{x \in succ(n)\rightarrow X.\ \text{Init}(x) \in U \wedge x(n) \in V\} \)
then have \( x \in succ(n)\rightarrow X \) and \( \text{Init}(x) \in U \) and I: \( x(n) \in V \)
let \( y = x(n) \)
from A1, and, \( x \in succ(n)\rightarrow X \) have \( x = \text{Append}( \text{Init}(x),y) \) using init_props
with I, and, \( \text{Init}(x) \in U \) have \( x \in (\bigcup y\in V.\ \{ \text{Append}(a,y).\ a\in U\}) \)
moreover {
}
ultimately show \( thesis \)
qed
fix \( x \)
assume \( x \in (\bigcup y\in V.\ \{ \text{Append}(a,y).\ a\in U\}) \)
then obtain \( a \) \( y \) where \( y\in V \) and \( a\in U \) and \( x = \text{Append}(a,y) \)
with A2, A3 have \( x: succ(n)\rightarrow X \) using append_props
from A2, A3, \( y\in V \), \( a\in U \) have \( a:n\rightarrow X \) and \( y\in X \)
with A1, \( a\in U \), \( y\in V \), \( x = \text{Append}(a,y) \) have \( \text{Init}(x) \in U \) and \( x(n) \in V \) using append_props, init_append
with \( x: succ(n)\rightarrow X \) have \( x \in \{x \in succ(n)\rightarrow X.\ \text{Init}(x) \in U \wedge x(n) \in V\} \)
Chains
In this section we define chains and operations on them. Chains are essentially lists that are parametrized by the first and last element.
Chains of elements of \(X\) connecting \(x\) and \(y\) are lists (i.e. functions) \(c:\{0,1,...,n\}\rightarrow X\) for some \(n\in \mathbb{N}\) such that the first element (i.e. \(c(0)\)) is \(x\) and the last (i.e. \(c(n)\)) element is \(y\). In informal comments we will say that the chain has length \(n\) when it consists of \(n+1\) elements of \(X\), i.e. it has \(n\) links, see the definition below.
definition
\( \text{Chains}(X,n,x,y) \equiv \{c \in (n + 1)\rightarrow X.\ c(0) = x \wedge c(n) = y\} \)
If \(c\) is a chain in \(X\) of length \(n\) connecting \(x\) and \(y\) then it maps \(n+1\) (i.e. the set \(\{0,1,..., n\}\)) to \(X\), the first element is \(x\), the \(n\)'th (last) element is \(y\) and both \(x\) and \(y\) are elements of \(X\).
lemma chain_props:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( c \in (n + 1)\rightarrow X \), \( c(0) = x \), \( c(n) = y \), \( x\in X \), \( y\in X \) using assms, succ_add_one(6), nat_less_add_one(2), apply_funtype unfolding Chains_defOne operation that we can do on a chain \(x=c_0,c_1,...,c_n=y\) is converting it to a list of pairs \(\langle c_i, c_{i+1}\rangle, 0 \leq i < n\). I don't have a good name for this operation, let's call it ChainLinks for now.
definition
\( \text{ChainLinks}(c) \equiv \{\langle i,\langle c(i),c(i + 1)\rangle \rangle .\ i \in (domain(c) - 1)\} \)
If \(c\) is a chain in \(X\) of length \(n\) then chain links of \(c\) form a list of elements of \(X\times X\) of length \(n\).
lemma chain_links_fun:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( domain(c) - 1 = n \) and \( \text{ChainLinks}(c):n\rightarrow X\times X \) using assms, func1_1_L1, ZF_fun_from_total, succ_ineq1(2,3), apply_funtype unfolding Chains_def, ChainLinks_defIf \(c\) is a chain in \(X\) connecting \(x\) and \(y\) of length \(n\) and \(k < n\) (i.e. \(k\in n\)) then the value of the \(k\)'th element of the derived chain links is \(\langle c(k),c(k+1)\rangle\).
lemma chain_links_val:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( k\in n \)
shows \( \text{ChainLinks}(c)(k) = \langle c(k),c(k + 1)\rangle \) using assms, chain_links_fun(1), ZF_fun_from_tot_val1 unfolding ChainLinks_defIf \(c\) is a chain in \(X\) connecting \(x\) and \(y\) of a non-zero length \(n\) then the first component of the first element of the derived chain links is \(x\) and the second component of the last element of the derived chain links is equal to \(y\).
lemma chain_intervals_ends:
assumes \( n\in nat \), \( n\neq 0 \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( \text{fst}( \text{ChainLinks}(c)(0)) = x \) and \( \text{snd}( \text{ChainLinks}(c)(n - 1)) = y \) using assms, empty_in_non_empty, nat_subtr_add1, func1_1_L1, nat_subtr_add1, pred_minus_one(2), ZF_fun_from_tot_val1 unfolding ChainLinks_def, Chains_defIf \(c\) is a chain in \(X\) connecting \(x\) and \(y\) of length \(n\) and \(k\) is a natural number such that \(k+1\in n\) then the second component of the \(k\)'th element of the derived chain intervals is the same as the first component of the \(k+1\)'th element of the derived chain intervals.
lemma chain_links_connected:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( k\in nat \), \( k + 1 \in n \)
shows \( \text{snd}( \text{ChainLinks}(c)(k)) = \text{fst}( \text{ChainLinks}(c)(k + 1)) \) using assms, succ_mem_mem(2), chain_links_fun(1), ZF_fun_from_tot_val1 unfolding ChainLinks_defIf \(c_i\) are chains from \(x_i\) to \(y_i\) of natural length \(n_i\) for \(i=1,2\) then concatenation \(c_3\) of \(c_1\) and \(c_2\) is a chain from \(x_1\) to \(y_1\) of length \(n_1 + n_2 + 1\). The chain links of the concatenation is a list of elements of \(X\times X\) of length \(n_1 + n_2 + 1\), obtained by appending the pair \(\langle c_1(n_1), c_2(0)\rangle\) to the chain links of \(c_1\) and then concatenating that with the chain links of \(c_2\). The proof is surprisingly long and tedious for such a trivial fact.
lemma concat_chains:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x_1,y_1) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,x_2,y_2) \)
defines \( c_3 \equiv \text{Concat}(c_1,c_2) \)
shows \( c_3 \in \text{Chains}(X,n_1 + n_2 + 1,x_1,y_2) \), \( \text{ChainLinks}(c_3): (n_1 + n_2 + 1)\rightarrow X\times X \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle c_1(n_1),c_2(0)\rangle ), \text{ChainLinks}(c_2)) \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle y_1,x_2\rangle ), \text{ChainLinks}(c_2)) \)proof let \( L_1 = \text{ChainLinks}(c_1) \)
let \( L_2 = \text{ChainLinks}(c_2) \)
let \( L_3 = \text{ChainLinks}(c_3) \)
let \( R = \text{Concat}( \text{Append}(L_1,\langle c_1(n_1),c_2(0)\rangle ),L_2) \)
from assms(1,2,3,4) have \( L_1:n_1\rightarrow X\times X \) and \( L_2:n_2\rightarrow X\times X \) using chain_links_fun(2)
from assms(2,4) have I: \( c_1: n_1 + 1\rightarrow X \), \( c_2: n_2 + 1\rightarrow X \) unfolding Chains_def
with assms(1,3,5) have \( c_3 : ((n_1 + 1) + (n_2 + 1)) \rightarrow X \) using concat_props(1)
with assms(1,2) have \( c_3 : ((n_1 + n_2 + 1) + 1) \rightarrow X \)
moreover
from assms(1,2,3,5), I have \( c_3(0) = x_1 \) using concat_props(2), succ_add_one(6)succ_add_one(6) unfolding Chains_def
moreover from assms(1,3) have \( n_2 \in (n_2 + 1) \)
with assms(5), I have \( c_3(n_1 + 1 + n_2) = c_2(n_2) \) using concat_props(4)
with assms(4) have \( c_3(n_1 + n_2 + 1) = y_2 \) unfolding Chains_def
ultimately show \( c_3 \in \text{Chains}(X,n_1 + n_2 + 1,x_1,y_2) \) unfolding Chains_def
with assms(1,3) show \( L_3: (n_1 + n_2 + 1)\rightarrow X\times X \) using chain_links_fun(2)
moreover
qed
have \( R: (n_1 + n_2 + 1)\rightarrow X\times X \)proof
moreover from assms(1,3), I, \( L_1:n_1\rightarrow X\times X \) have \( \text{Append}(L_1,\langle c_1(n_1),c_2(0)\rangle ): (n_1 + 1)\rightarrow X\times X \) using succ_add_one(6), apply_funtype, append_props(1)
with assms(3), \( L_2:n_2\rightarrow X\times X \) have \( R: ((n_1 + 1) + n_2) \rightarrow X\times X \) using concat_props(1)
with assms(1) show \( thesis \)
qed
have \( \forall i\in (n_1 + n_2 + 1).\ L_3(i) = R(i) \)proof
}
ultimately show \( L_3 = R \) by (rule func_eq )
from assms(1,3), I have \( \langle c_1(n_1),c_2(0)\rangle \in X\times X \) using succ_add_one(6), apply_funtype
with assms(1), \( L_1:n_1\rightarrow X\times X \) have II: \( \text{Append}(L_1,\langle c_1(n_1),c_2(0)\rangle ): (n_1 + 1)\rightarrow X\times X \) using append_props(1)
{
fix \( i \)
assume \( i\in (n_1 + n_2 + 1) \)
with assms(1,3), \( c_3 \in \text{Chains}(X,n_1 + n_2 + 1,x_1,y_2) \) have III: \( L_3(i) = \langle c_3(i),c_3(i + 1)\rangle \) using chain_links_val
from assms(1,3), \( i\in (n_1 + n_2 + 1) \) have \( i \in (n_1 + 1) \cup \text{NatInterval}((n_1 + 1),n_2) \) using length_start_decomp(2)
hence \( i\in (n_1 + 1) \vee i\in \text{NatInterval}((n_1 + 1),n_2) \)
moreover {
}
moreover {
}
ultimately have \( L_3(i) = R(i) \)
assume \( i\in (n_1 + 1) \)
with assms(1,3,5), I have \( c_3(i)=c_1(i) \) using concat_props(2)
from assms(1,3), \( L_2:n_2\rightarrow X\times X \), II, \( i\in (n_1 + 1) \) have IV: \( R(i) = \text{Append}(L_1,\langle c_1(n_1),c_2(0)\rangle )(i) \) using concat_props(2)
from \( i\in (n_1 + 1) \), assms(1) have \( i\in n_1 \vee i=n_1 \) using succ_ineq2(3)
moreover {
}
moreover {
}
ultimately have \( L_3(i) = R(i) \)
assume \( i\in n_1 \)
with assms(1) have \( i + 1 \in (n_1 + 1) \) using succ_ineq1(2)
with assms(1,3,5), I have \( c_3(i + 1)=c_1(i + 1) \) using concat_props(2)
from \( L_1:n_1\rightarrow X\times X \), \( \langle c_1(n_1),c_2(0)\rangle \in X\times X \), \( i\in n_1 \), IV have \( R(i) = L_1(i) \) using append_props(2)
with assms(1,2), \( i\in n_1 \), \( c_3(i)=c_1(i) \), \( c_3(i + 1)=c_1(i + 1) \), III have \( L_3(i) = R(i) \) using chain_links_val
assume \( i=n_1 \)
from assms(1,3,5), I have \( c_3(n_1 + 1 + 0)=c_2(0) \) using concat_props(4), succ_add_one(6)
with assms(1), \( i=n_1 \) have \( c_3(i + 1)=c_2(0) \)
with III, IV, \( c_3(i)=c_1(i) \), \( L_1:n_1\rightarrow X\times X \), \( \langle c_1(n_1),c_2(0)\rangle \in X\times X \), \( i=n_1 \) have \( L_3(i) = R(i) \) using append_props(3)
assume \( i\in \text{NatInterval}(n_1 + 1,n_2) \)
with assms(1,3) have \( i\in \text{NatInterval}(n_1 + 1,n_2 + 1) \) and \( (i + 1) \in \text{NatInterval}(n_1 + 1,n_2 + 1) \) using interval_incr_len
from assms(3), \( i\in \text{NatInterval}(n_1 + 1,n_2) \) have \( i - (n_1 + 1) \in n_2 \) using inter_diff_in_len
from assms(1,3,5), I, \( i\in \text{NatInterval}(n_1 + 1,n_2 + 1) \) have VI: \( c_3(i)=c_2(i - (n_1 + 1)) \) using concat_props(3)
from assms(1,3,5), I, \( (i + 1) \in \text{NatInterval}(n_1 + 1,n_2 + 1) \) have VII: \( c_3(i + 1)=c_2((i + 1) - (n_1 + 1)) \) using concat_props(3)
from assms(1,3), \( L_2:n_2\rightarrow X\times X \), II, \( i\in \text{NatInterval}(n_1 + 1,n_2) \) have \( R(i) = L_2(i - (n_1 + 1)) \) using concat_props(3)
with assms(1,3,4), III, VI, VII, \( i\in \text{NatInterval}(n_1 + 1,n_2) \), \( i - (n_1 + 1) \in n_2 \) have \( L_3(i) = R(i) \) using chain_links_val, inter_diff_in_len(2)
thus \( thesis \)
qed
with assms(1,2,3,4) show \( L_3 = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle y_1,x_2\rangle ), \text{ChainLinks}(c_2)) \) using chain_props(2,3)
end
lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \) lemma elem_nat_is_nat:
assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \)Definition of Tail:
\( \text{Tail}(a) \equiv \{\langle k, a(succ(k))\rangle .\ k \in pred(domain(a))\} \)
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 \) lemma tail_as_set:
assumes \( n \in nat \) and \( a: n + 1 \rightarrow X \)
shows \( \text{Tail}(a) = \{\langle k,a(k + 1)\rangle .\ k\in n\} \) lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \) lemma codomain_nonempty:
assumes \( f:X\rightarrow Y \), \( X\neq \emptyset \)
shows \( Y\neq \emptyset \) lemma inter_diff_in_len:
assumes \( k \in nat \) and \( i \in \text{NatInterval}(n,k) \)
shows \( i - n \in k \) and \( i + 1 - n = i - n + 1 \)Definition of ShiftedSeq:
\( \text{ShiftedSeq}(b,n) \equiv \{\langle j, b(j - n)\rangle .\ j \in \text{NatInterval}(n,domain(b))\} \)
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 elem_nat_is_nat:
assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \)Definition of NatInterval:
\( \text{NatInterval}(n,k) \equiv \{n + j.\ j\in k\} \)
lemma nat_interval_zero_beg:
assumes \( n\in nat \)
shows \( \text{NatInterval}(0,n) = n \) theorem fun_is_set_of_pairs:
assumes \( f:X\rightarrow Y \)
shows \( f = \{\langle x,f(x)\rangle .\ x \in X\} \) lemma nat_interval_zero_len: shows \( \text{NatInterval}(n,0) = 0 \)
lemma shifted_seq_props:
assumes \( n \in nat \), \( k \in nat \) and \( b:k\rightarrow X \)
shows \( \text{ShiftedSeq}(b,n): \text{NatInterval}(n,k) \rightarrow X \), \( \forall i \in \text{NatInterval}(n,k).\ \text{ShiftedSeq}(b,n)(i) = b(i - n) \), \( \forall j\in k.\ \text{ShiftedSeq}(b,n)(n + j) = b(j) \) lemma length_start_decomp:
assumes \( n \in nat \), \( k \in nat \)
shows \( n \cap \text{NatInterval}(n,k) = 0 \), \( n \cup \text{NatInterval}(n,k) = n + k \)Definition of Concat:
\( \text{Concat}(a,b) \equiv a \cup \text{ShiftedSeq}(b,domain(a)) \)
theorem concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \) lemma add_nat_le:
assumes \( n \in nat \) and \( k \in nat \)
shows \( n \leq n + k \), \( n \subseteq n + k \), \( n \subseteq k + n \) lemma add_lt_mono:
assumes \( k \in nat \) and \( j\in k \)
shows \( (n + j) \lt (n + k) \), \( (n + j) \in (n + k) \) lemma concat_concat_list:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \) and \( d = \text{Concat}( \text{Concat}(a,b),c) \)
shows \( d : n + k + m \rightarrow X \), \( \forall j \in n.\ d(j) = a(j) \), \( \forall j \in k.\ d(n + j) = b(j) \), \( \forall j \in m.\ d(n + k + j) = c(j) \) lemma concat_list_concat:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \) and \( e = \text{Concat}(a, \text{Concat}(b,c)) \)
shows \( e : n + k + m \rightarrow X \), \( \forall j \in n.\ e(j) = a(j) \), \( \forall j \in k.\ e(n + j) = b(j) \), \( \forall j \in m.\ e(n + k + j) = c(j) \) lemma adjacent_intervals3:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \)
shows \( n + k + m = (n + k) \cup \text{NatInterval}(n + k,m) \), \( n + k + m = n \cup \text{NatInterval}(n,k + m) \), \( n + k + m = n \cup \text{NatInterval}(n,k) \cup \text{NatInterval}(n + k,m) \) 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 succ_ineq:
assumes \( n \in nat \)
shows \( \forall i \in n.\ succ(i) \in succ(n) \) 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) \) 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 empty_in_every_succ:
assumes \( n \in nat \)
shows \( 0 \in succ(n) \) lemma pair_func_singleton:
assumes \( y \in Y \)
shows \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \) lemma one_is_nat: shows \( \{0\} \in nat \), \( \{0\} = succ(0) \), \( \{0\} = 1 \)
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 concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) theorem concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \) lemma pair_val: shows \( \{\langle x,y\rangle \}(x) = y \)
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 \) theorem concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \)Definition of Append:
\( \text{Append}(a,x) \equiv a \cup \{\langle domain(a),x\rangle \} \)
lemma func1_1_L11D:
assumes \( f:X\rightarrow Y \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \)
shows \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \), \( \forall x\in X.\ g(x) = f(x) \), \( g(a) = b \) lemma succ_explained: shows \( succ(n) = n \cup \{n\} \)
lemma set_elem_add:
assumes \( x\in X \)
shows \( X \cup \{x\} = X \) 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 \) 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)) \)Definition of Lists:
\( \text{Lists}(X) \equiv \bigcup n\in nat.\ (n\rightarrow X) \)
Definition of NELists:
\( \text{NELists}(X) \equiv \bigcup n\in nat.\ (succ(n)\rightarrow X) \)
Definition of Init:
\( \text{Init}(a) \equiv \text{restrict}(a,pred(domain(a))) \)
theorem init_props:
assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)
shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \) theorem init_props:
assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)
shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \) lemma init_def:
assumes \( n \in nat \) and \( a:succ(n)\rightarrow X \)
shows \( \text{Init}(a) = \text{restrict}(a,n) \) lemma restrict_def_alt:
assumes \( A\subseteq X \)
shows \( \text{restrict}(\{\langle x,q(x)\rangle .\ x\in X\},A) = \{\langle x,q(x)\rangle .\ x\in A\} \) lemma bij_extend_point:
assumes \( f \in \text{bij}(X,Y) \), \( a\notin X \), \( b\notin Y \)
shows \( (f \cup \{\langle a,b\rangle \}) \in \text{bij}(X\cup \{a\},Y\cup \{b\}) \) lemma func1_1_L1B:
assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)
shows \( f:X\rightarrow Z \)Definition of Last:
\( \text{Last}(a) \equiv a(pred(domain(a))) \)
lemma last_seq_elem:
assumes \( a: succ(n) \rightarrow X \)
shows \( \text{Last}(a) = a(n) \) 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 empty_shifted_empty: shows \( \text{ShiftedSeq}(\emptyset ,n) = \emptyset \)
lemma seq_shifted_by_zero:
assumes \( n\in nat \), \( b:n\rightarrow X \)
shows \( \text{ShiftedSeq}(b,0) = b \) lemma append_1elem:
assumes \( n \in nat \) and \( a: n \rightarrow X \) and \( b : 1 \rightarrow X \)
shows \( \text{Concat}(a,b) = \text{Append}(a,b(0)) \) lemma append_concat_pair:
assumes \( n \in nat \) and \( a: n \rightarrow X \) and \( x\in X \)
shows \( \text{Append}(a,x) = \text{Concat}(a,\{\langle 0,x\rangle \}) \) theorem concat_assoc:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \), \( c:m\rightarrow X \)
shows \( \text{Concat}( \text{Concat}(a,b),c) = \text{Concat}(a, \text{Concat}(b,c)) \) lemma concat_append_assoc:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \) and \( x \in X \)
shows \( \text{Append}( \text{Concat}(a,b),x) = \text{Concat}(a, \text{Append}(b,x)) \) lemma length_start_decomp:
assumes \( n \in nat \), \( k \in nat \)
shows \( n \cap \text{NatInterval}(n,k) = 0 \), \( n \cup \text{NatInterval}(n,k) = n + k \) theorem concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \) lemma set_list_append:
assumes \( \forall i \in succ(k).\ b(i) \in X \) and \( a = \{\langle i,b(i)\rangle .\ i \in succ(k)\} \)
shows \( a: succ(k) \rightarrow X \), \( \{\langle i,b(i)\rangle .\ i \in k\}: k \rightarrow X \), \( a = \text{Append}(\{\langle i,b(i)\rangle .\ i \in k\},b(k)) \) lemma init_def_alt:
assumes \( n\in nat \) and \( \forall k\in n + 1.\ q(k) \in X \)
shows \( \text{Init}(\{\langle k,q(k)\rangle .\ k\in n + 1\}) = \{\langle k,q(k)\rangle .\ k\in n\} \) lemma set_list_append:
assumes \( \forall i \in succ(k).\ b(i) \in X \) and \( a = \{\langle i,b(i)\rangle .\ i \in succ(k)\} \)
shows \( a: succ(k) \rightarrow X \), \( \{\langle i,b(i)\rangle .\ i \in k\}: k \rightarrow X \), \( a = \text{Append}(\{\langle i,b(i)\rangle .\ i \in k\},b(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 pred_succ_mem:
assumes \( n\in nat \), \( n\neq 0 \), \( k\in succ(n) \)
shows \( pred(k)\in n \) lemma pred_minus_one:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( n - 1 = pred(n) \) and \( n - 1 \in n \)Definition of Prepend:
\( \text{Prepend}(a,x) \equiv \{\langle k,\text{if }k = 0\text{ then }x\text{ else }a(k - 1)\rangle .\ k\in domain(a) + 1\} \)
lemma prepend_props:
assumes \( n\in nat \), \( a:n\rightarrow X \), \( x\in X \)
shows \( \text{Prepend}(a,x):(n + 1)\rightarrow X \) and \( \text{Prepend}(a,x)(0) = x \) lemma tail_props2:
assumes \( n \in nat \), \( a: n + 1 \rightarrow X \), \( k\in n \)
shows \( \text{Tail}(a)(k) = a(k + 1) \) lemma prepend_val:
assumes \( n\in nat \), \( a:n\rightarrow X \), \( x\in X \), \( k\in n \)
shows \( \text{Prepend}(a,x)(k + 1) = a(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 init_append:
assumes \( n \in nat \) and \( a:n\rightarrow X \) and \( x \in X \)
shows \( \text{Init}( \text{Append}(a,x)) = a \) lemma list_singleton_pair:
assumes \( x:1\rightarrow X \)
shows \( x = \{\langle 0,x(0)\rangle \} \) lemma singleton_list_bij: shows \( \{\langle x,x(0)\rangle .\ x\in 1\rightarrow X\} \in \text{bij}(1\rightarrow X,X) \)
lemma func_singleton_pair:
assumes \( f : \{a\}\rightarrow X \)
shows \( f = \{\langle a, f(a)\rangle \} \) lemma comp_conv_id:
assumes \( a \in \text{bij}(A,B) \) and \( b:B\rightarrow A \) and \( \forall x\in A.\ b(a(x)) = x \)
shows \( b \in \text{bij}(B,A) \) and \( a = converse(b) \) and \( b = converse(a) \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma nat_less_add_one:
assumes \( n\in nat \)
shows \( n \lt n + 1 \) and \( n \in n + 1 \)Definition of Chains:
\( \text{Chains}(X,n,x,y) \equiv \{c \in (n + 1)\rightarrow X.\ c(0) = x \wedge c(n) = y\} \)
lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \)Definition of ChainLinks:
\( \text{ChainLinks}(c) \equiv \{\langle i,\langle c(i),c(i + 1)\rangle \rangle .\ i \in (domain(c) - 1)\} \)
lemma chain_links_fun:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( domain(c) - 1 = n \) and \( \text{ChainLinks}(c):n\rightarrow X\times X \) lemma empty_in_non_empty:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( 0\in n \) lemma nat_subtr_add1:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( (n - 1) + 1 = n \) lemma pred_minus_one:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( n - 1 = pred(n) \) and \( n - 1 \in n \) lemma succ_mem_mem:
assumes \( n\in nat \), \( k\in nat \), \( k + 1 \in n \)
shows \( k \lt n \) and \( k\in n \) lemma chain_links_fun:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( domain(c) - 1 = n \) and \( \text{ChainLinks}(c):n\rightarrow X\times X \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) 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 chain_links_val:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( k\in n \)
shows \( \text{ChainLinks}(c)(k) = \langle c(k),c(k + 1)\rangle \) lemma succ_ineq2:
assumes \( n \in nat \), \( k \in n + 1 \)
shows \( k + 1 \leq n + 1 \), \( k\leq n \), \( k\in n \vee k=n \) lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \) 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 \) 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 interval_incr_len:
assumes \( n \in nat \), \( k \in nat \), \( i \in \text{NatInterval}(n,k) \)
shows \( i \in \text{NatInterval}(n,k + 1) \) and \( (i + 1) \in \text{NatInterval}(n,k + 1) \) lemma inter_diff_in_len:
assumes \( k \in nat \) and \( i \in \text{NatInterval}(n,k) \)
shows \( i - n \in k \) and \( i + 1 - n = i - n + 1 \) lemma chain_props:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( c \in (n + 1)\rightarrow X \), \( c(0) = x \), \( c(n) = y \), \( x\in X \), \( y\in X \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
