IsarMathLib

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

theory FiniteSeq_ZF imports Nat_ZF_IML func1

begin

This theory treats finite sequences (i.e. maps $n \to 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 \to X$ .

We define the set of lists with values in set $X$ as $Lists (X)$ .

definition

$Lists (X) \equiv ⋃ n \in n a t . (n \to X)$

The set of nonempty $X$ -value listst will be called $NELists (X)$ .

definition

$NELists (X) \equiv ⋃ n \in n a t . (s u c c (n) \to 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 $p r e d (n)$ is the previous natural number and denotes the difference between natural numbers $n$ and $k$ .

definition

$ShiftedSeq (b, n) \equiv {⟨ j, b (j - n) ⟩ . j \in N a t Interval (n, d o m a i n (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 $Concat (a, b)$ .

definition

$Concat (a, b) \equiv a \cup ShiftedSeq (b, d o m a i n (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

$Tail (a) \equiv {⟨ k, a (s u c c (k)) ⟩ . k \in p r e d (d o m a i n (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

$Init (a) \equiv restrict (a, p r e d (d o m a i n (a)))$

Another obvious operation we can talk about is appending an element at the end of a sequence. This is called Append.

definition

$Append (a, x) \equiv a \cup {⟨ d o m a i n (a), x ⟩}$

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

$Last (a) \equiv a (p r e d (d o m a i n (a)))$

A formula for tail of a finite list.

lemma tail_as_set:

assumes $n \in n a t$ and $a : n + 1 \to X$

shows

Tail (a) = {⟨ k, a (k + 1) ⟩ . k \in n}

using assms, func1_1_L1, elem_nat_is_nat(2), succ_add_one(1) unfolding Tail_def

Formula for the tail of a list defined by an expression:

lemma tail_formula:

assumes $n \in n a t$ and $\forall k \in n + 1. q (k) \in X$

shows

Tail ({⟨ k, q (k) ⟩ . k \in n + 1}) = {⟨ k, q (k + 1) ⟩ . k \in n}

proof

let

a = {⟨ k, q (k) ⟩ . k \in n + 1}

from assms(2) have

a : n + 1 \to X

by (rule ZF_fun_from_total )

with assms(1) have

Tail (a) = {⟨ k, a (k + 1) ⟩ . k \in n}

using tail_as_set

moreover

have

\forall k \in n . a (k + 1) = q (k + 1)

proof

{

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

t h e s i s

qed

ultimately show

t h e s i s

qed

Codomain of a nonempty list is nonempty.

lemma nelist_vals_nonempty:

assumes $a : s u c c (n) \to Y$

shows

Y \neq 0

using assms, codomain_nonempty

Shifted sequence is a function on a the interval of natural numbers.

lemma shifted_seq_props:

assumes A1: $n \in n a t$ , $k \in n a t$ and A2: $b : k \to X$

shows

ShiftedSeq (b, n) : N a t Interval (n, k) \to X

\forall i \in N a t Interval (n, k) . ShiftedSeq (b, n) (i) = b (i - n)

\forall j \in k . ShiftedSeq (b, n) (n + j) = b (j)

proof

let

I = N a t Interval (n, d o m a i n (b))

from A2 have Fact:

I = N a t Interval (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

{⟨ j, b (j - n) ⟩ . j \in I} : I \to X

by (rule ZF_fun_from_total )

with Fact show thesis_1:

ShiftedSeq (b, n) : N a t Interval (n, k) \to X

using ShiftedSeq_def

{

fix

i

from Fact, thesis_1 have

ShiftedSeq (b, n) : I \to X

moreover

assume

i \in N a t Interval (n, k)

with Fact have

i \in I

moreover

from Fact have

ShiftedSeq (b, n) = {⟨ i, b (i - n) ⟩ . i \in I}

using ShiftedSeq_def

ultimately have

ShiftedSeq (b, n) (i) = b (i - n)

by (rule ZF_fun_from_tot_val )

}

then show thesis1:

\forall i \in N a t Interval (n, k) . ShiftedSeq (b, n) (i) = b (i - n)

{

fix

j

let

i = n + j

assume A3:

j \in k

with A1 have

j \in n a t

using elem_nat_is_nat

then have

i - n = j

using diff_add_inverse

with A3, thesis1 have

ShiftedSeq (b, n) (i) = b (j)

using NatInterval_def

}

then show

\forall j \in k . ShiftedSeq (b, n) (n + j) = b (j)

qed

Basis properties of the contatenation of two finite sequences.

theorem concat_props:

assumes A1: $n \in n a t$ , $k \in n a t$ and A2: $a : n \to X$ , $b : k \to X$

shows

Concat (a, b) : n + k \to X

\forall i \in n . Concat (a, b) (i) = a (i)

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

\forall j \in k . Concat (a, b) (n + j) = b (j)

proof

from A1, A2 have

a : n \to X

and I:

ShiftedSeq (b, n) : N a t Interval (n, k) \to X

and

n \cap N a t Interval (n, k) = 0

using shifted_seq_props, length_start_decomp

then have

a \cup ShiftedSeq (b, n) : n \cup N a t Interval (n, k) \to X \cup X

by (rule fun_disjoint_Un )

with A1, A2 show

Concat (a, b) : n + k \to X

using func1_1_L1, Concat_def, length_start_decomp

{

fix

i

assume

i \in n

with A1, I have

i \notin d o m a i n (ShiftedSeq (b, n))

using length_start_decomp, func1_1_L1

with A2 have

Concat (a, b) (i) = a (i)

using func1_1_L1, fun_disjoint_apply1, Concat_def

}

thus

\forall i \in n . Concat (a, b) (i) = a (i)

{

fix

i

assume A3:

i \in N a t Interval (n, k)

with A1, A2 have

i \notin d o m a i n (a)

using length_start_decomp, func1_1_L1

with A1, A2, A3 have

Concat (a, b) (i) = b (i - n)

using func1_1_L1, fun_disjoint_apply2, Concat_def, shifted_seq_props

}

thus II:

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

{

fix

j

let

i = n + j

assume A3:

j \in k

with A1 have

j \in n a t

using elem_nat_is_nat

then have

i - n = j

using diff_add_inverse

with A3, II have

Concat (a, b) (i) = b (j)

using NatInterval_def

}

thus

\forall j \in k . Concat (a, b) (n + j) = b (j)

qed

Properties of concatenating three lists.

lemma concat_concat_list:

assumes A1: $n \in n a t$ , $k \in n a t$ , $m \in n a t$ and A2: $a : n \to X$ , $b : k \to X$ , $c : m \to X$ and A3: $d = Concat (Concat (a, b), c)$

shows

d : n + k + m \to 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 n a t

m \in n a t

Concat (a, b) : n + k \to X

c : m \to X

using concat_props

with A3 show

You can't use 'macro parameter character #' in math mode

using concat_props

from I have II:

\forall i \in n + k .

Concat (Concat (a, b), c) (i) = 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) = 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) = Concat (a, b) (n + j)

using add_lt_mono

also

from A1, A2, A5 have

\dots = 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 . Concat (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 n a t$ , $k \in n a t$ , $m \in n a t$ and A2: $a : n \to X$ , $b : k \to X$ , $c : m \to X$ and A3: $e = Concat (a, Concat (b, c))$

shows

e : n + k + m \to 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 n a t

k + m \in n a t

a : n \to X

Concat (b, c) : k + m \to X

using concat_props

with A3 show

You can't use 'macro parameter character #' in math mode

using concat_props, add_assoc

from I have

\forall j \in n . Concat (a, 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 . Concat (a, Concat (b, c)) (n + j) = 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) = Concat (b, c) (j)

also

from A1, A2, A4 have

\dots = 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) = Concat (b, c) (k + j)

using add_lt_mono, add_assoc

also

from A1, A2, A5 have

\dots = 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 n a t$ , $k \in n a t$ , $m \in n a t$ and A2: $a : n \to X$ , $b : k \to X$ , $c : m \to X$

shows

Concat (Concat (a, b), c) = Concat (a, Concat (b, c))

proof

let

d = Concat (Concat (a, b), c)

let

e = Concat (a, Concat (b, c))

from A1, A2 have

You can't use 'macro parameter character #' in math mode

and

You can't use 'macro parameter character #' in math mode

using concat_concat_list, concat_list_concat

moreover

have

You can't use 'macro parameter character #' in math mode

proof

{

fix

i

assume

You can't use 'macro parameter character #' in math mode

moreover

from A1 have

You can't use 'macro parameter character #' in math mode

using adjacent_intervals3

ultimately have

i \in n \lor i \in N a t Interval (n, k) \lor i \in N a t Interval (n + k, m)

moreover {

assume

i \in n

with A1, A2 have

d (i) = e (i)

using concat_concat_list, concat_list_concat

} moreover {

assume

i \in N a t Interval (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

} moreover {

assume

i \in N a t Interval (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

} ultimately have

d (i) = e (i)

}

thus

t h e s i s

qed

ultimately show

d = e

by (rule func_eq )

qed

Properties of Tail.

theorem tail_props:

assumes A1: $n \in n a t$ and A2: $a : s u c c (n) \to X$

shows

Tail (a) : n \to X

\forall k \in n . Tail (a) (k) = a (s u c c (k))

proof

from A1, A2 have

\forall k \in n . a (s u c c (k)) \in X

using succ_ineq, apply_funtype

then have

{⟨ k, a (s u c c (k)) ⟩ . k \in n} : n \to X

by (rule ZF_fun_from_total )

with A2 show I:

Tail (a) : n \to X

using func1_1_L1, pred_succ_eq, Tail_def

moreover

from A2 have

Tail (a) = {⟨ k, a (s u c c (k)) ⟩ . k \in n}

using func1_1_L1, pred_succ_eq, Tail_def

ultimately show

\forall k \in n . Tail (a) (k) = a (s u c c (k))

by (rule ZF_fun_from_tot_val0 )

qed

Essentially the second assertion of tail_props but formulated using notation $n + 1$ instead of $s u c c (n)$ :

lemma tail_props2:

assumes $n \in n a t$ , $a : n + 1 \to X$ , $k \in n$

shows

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 n a t$ , $a : s u c c (n) \to X$

shows

a = Concat ({⟨ 0, a (0) ⟩}, Tail (a))

proof

let

b = Concat ({⟨ 0, a (0) ⟩}, Tail (a))

have

b : s u c c (n) \to X

and

\forall k \in s u c c (n) . a (k) = b (k)

proof

from assms(1) have

0 \in s u c c (n)

using empty_in_every_succ

with assms(2) have

a (0) \in X

using apply_funtype

then have I:

{⟨ 0, a (0) ⟩} : {0} \to X

using pair_func_singleton

have

{0} \in n a t

using one_is_nat

from assms have

Tail (a) : n \to X

using tail_props(1)

with assms(1),

{0} \in n a t

, I have

b : {0} + n \to X

using concat_props(1)

with assms(1) show

b : s u c c (n) \to X

using succ_add_one(3)

{

fix

k

assume

k \in s u c c (n)

{

assume

k = 0

with assms(1),

{0} \in n a t

, I,

Tail (a) : n \to X

have

a (k) = b (k)

using concat_props(2), pair_val

}

moreover {

assume

k \neq 0

from assms(1),

k \in s u c c (n)

have

k \in n a t

using elem_nat_is_nat(2)

with

k \neq 0

obtain

m

where

m \in n a t

and

k = s u c c (m)

using Nat_ZF_1_L3

with assms(1),

k \in s u c c (n)

have

m \in n

using succ_mem

with

{0} \in n a t

, assms(1), I,

Tail (a) : n \to X

have

b ({0} + m) = Tail (a) (m)

using concat_props(4)

with assms,

m \in n a t

k \in s u c c (n)

k = s u c c (m)

m \in n

have

a (k) = b (k)

using succ_add_one(3), tail_props(2)

} ultimately have

a (k) = b (k)

}

thus

\forall k \in s u c c (n) . a (k) = b (k)

qed

with assms(2) show

t h e s i s

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 \to X$ and A2: $x \in X$ and A3: $b = Append (a, x)$

shows

b : s u c c (n) \to 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 {⟨ n, x ⟩}

using func1_1_L1, Append_def

ultimately have

b : n \cup {n} \to X \cup {x}

by (rule func1_1_L11D )

with A2 show

b : s u c c (n) \to 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 n a t$ and $a : s u c c (n) \to X$ and $x \in X$

shows

Append (a, x) (0) = a (0)

using assms, append_props, empty_in_every_succ

Tail commutes with Append.

theorem tail_append_commute:

assumes A1: $n \in n a t$ and A2: $a : s u c c (n) \to X$ and A3: $x \in X$

shows

Append (Tail (a), x) = Tail (Append (a, x))

proof

let

b = Append (Tail (a), x)

let

c = Tail (Append (a, x))

from A1, A2 have I:

Tail (a) : n \to X

using tail_props

from A1, A2, A3 have

s u c c (n) \in n a t

and

Append (a, x) : s u c c (s u c c (n)) \to X

using append_props

then have II:

\forall k \in s u c c (n) . c (k) = Append (a, x) (s u c c (k))

by (rule tail_props )

from assms have

b : s u c c (n) \to X

and

c : s u c c (n) \to X

using tail_props, append_props

moreover

have

\forall k \in s u c c (n) . b (k) = c (k)

proof

{

fix

k

assume

k \in s u c c (n)

hence

k \in n \lor k = n

moreover {

assume A4:

k \in n

with assms, II have

c (k) = a (s u c c (k))

using succ_ineq, append_props

moreover

from A3, I have

\forall k \in n . b (k) = Tail (a) (k)

using append_props

with A1, A2, A4 have

b (k) = a (s u c c (k))

using tail_props

ultimately have

b (k) = c (k)

} moreover {

assume A5:

k = n

with A2, A3, I, II have

b (k) = c (k)

using append_props

} ultimately have

b (k) = c (k)

}

thus

t h e s i s

qed

ultimately show

b = c

by (rule func_eq )

qed

@{term NELists} are non-empty lists

lemma non_zero_List_func_is_NEList:

shows

NELists (X) = {a \in Lists (X) . a \neq 0}

proof

{

fix

a

assume as:

a \in {a \in Lists (X) . a \neq 0}

from as obtain

n

where a:

n \in n a t

a : n \to X

unfolding Lists_def

{

assume

n = 0

with a(2) have

a = 0

unfolding Pi_def

with as have

F a l s e

}

hence

n \neq 0

with a(1) obtain

k

where

k \in n a t

n = s u c c (k)

using Nat_ZF_1_L3

with a(2) have

a \in NELists (X)

unfolding NELists_def

}

moreover {

fix

a

assume as:

a \in NELists (X)

then obtain

k

where k:

a : s u c c (k) \to X

k \in n a t

unfolding NELists_def

{

assume

a = 0

hence

d o m a i n (a) = 0

with k(1) have

s u c c (k) = 0

using domain_of_fun

hence

F a l s e

}

moreover {

from k(2) have

s u c c (k) \in n a t

using nat_succI

with k(1) have

a \in Lists (X)

unfolding Lists_def

} ultimately have

a \in {a \in Lists (X) . a \neq 0}

} ultimately show

t h e s i s

qed

Properties of Init.

theorem init_props:

assumes A1: $n \in n a t$ and A2: $a : s u c c (n) \to X$

shows

Init (a) : n \to X

\forall k \in n . Init (a) (k) = a (k)

a = Append (Init (a), a (n))

proof

have

n \subseteq s u c c (n)

with A2 have

restrict (a, n) : n \to X

using restrict_type2

moreover

from A1, A2 have I:

restrict (a, n) = Init (a)

using func1_1_L1, pred_succ_eq, Init_def

ultimately show thesis1:

Init (a) : n \to X

{

fix

k

assume

k \in n

then have

restrict (a, n) (k) = a (k)

using restrict

with I have

Init (a) (k) = a (k)

}

then show thesis2:

\forall k \in n . Init (a) (k) = a (k)

let

b = Append (Init (a), a (n))

from A2, thesis1 have II:

Init (a) : n \to X

a (n) \in X

b = Append (Init (a), a (n))

using apply_funtype

note A2

moreover

from II have

b : s u c c (n) \to X

by (rule append_props )

moreover

have

\forall k \in s u c c (n) . a (k) = b (k)

proof

{

fix

k

assume A3:

k \in n

from II have

\forall j \in n . b (j) = Init (a) (j)

by (rule append_props )

with thesis2, A3 have

a (k) = b (k)

}

moreover

from II have

b (n) = a (n)

by (rule append_props )

hence

a (n) = b (n)

ultimately show

\forall k \in s u c c (n) . a (k) = b (k)

qed

ultimately show

a = b

by (rule func_eq )

qed

The initial part of a non-empty list is a list, and the domain of the original list is the successor of its initial part.

theorem init_NElist:

assumes $a \in NELists (X)$

shows

Init (a) \in Lists (X)

and

s u c c (d o m a i n (Init (a))) = d o m a i n (a)

proof

from assms obtain

n

where n:

n \in n a t

a : s u c c (n) \to X

unfolding NELists_def

then have tailF:

Init (a) : n \to X

using init_props(1)

with n(1) show

Init (a) \in Lists (X)

unfolding Lists_def

from tailF have

d o m a i n (Init (a)) = n

using domain_of_fun

moreover

from n(2) have

d o m a i n (a) = s u c c (n)

using domain_of_fun

ultimately show

s u c c (d o m a i n (Init (a))) = d o m a i n (a)

qed

If we take init of the result of append, we get back the same list.

lemma init_append:

assumes A1: $n \in n a t$ and A2: $a : n \to X$ and A3: $x \in X$

shows

Init (Append (a, x)) = a

proof

from A2, A3 have

Append (a, x) : s u c c (n) \to X

using append_props

with A1 have

Init (Append (a, x)) : n \to X

and

\forall k \in n . Init (Append (a, x)) (k) = Append (a, x) (k)

using init_props

with A2, A3 have

\forall k \in n . Init (Append (a, x)) (k) = a (k)

using append_props

with

Init (Append (a, x)) : n \to X

, A2 show

t h e s i s

by (rule func_eq )

qed

A reformulation of definition of Init.

lemma init_def:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Init (a) = restrict (a, n)

using assms, func1_1_L1, Init_def

Another reformulation of the definition of Init, starting with the expression defining the list.

lemma init_def_alt:

assumes $n \in n a t$ and $\forall k \in n + 1. q (k) \in X$

shows

Init ({⟨ k, q (k) ⟩ . k \in n + 1}) = {⟨ k, q (k) ⟩ . k \in n}

proof

let

a = {⟨ k, q (k) ⟩ . k \in n + 1}

from assms(2) have

a : n + 1 \to X

by (rule ZF_fun_from_total )

moreover

from assms(1) have

n + 1 = s u c c (n)

using succ_add_one(1)

ultimately have

a : s u c c (n) \to X

with assms(1) have

Init (a) = restrict (a, n)

using init_def

moreover

from assms(1) have

n \subseteq n + 1

then have

restrict (a, n) = {⟨ k, q (k) ⟩ . k \in n}

by (rule restrict_def_alt )

ultimately show

t h e s i s

qed

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 \to X$ , $y \in X$ , $b = a \cup {⟨ n, y ⟩}$

shows

b : s u c c (n) \to X

\forall k \in n . b (k) = a (k)

b (n) = y

using assms, Append_def, func1_1_L1, append_props

The 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 n a t$ and A2: $b \in bij (n, X)$ and A3: $x \notin X$

shows

Append (b, x) \in bij (s u c c (n), X \cup {x})

proof

from A2, A3 have

b \cup {⟨ n, x ⟩} \in bij (n \cup {n}, X \cup {x})

using mem_not_refl, bij_extend_point

moreover

have

Append (b, x) = b \cup {⟨ n, x ⟩}

proof

from A2 have

b : n \to X

using bij_def, surj_def

then have

b : n \to X \cup {x}

using func1_1_L1B

then show

Append (b, x) = b \cup {⟨ n, x ⟩}

using Append_def, func1_1_L1

qed

ultimately show

t h e s i s

using succ_explained

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 : s u c c (n) \to X$

shows

Last (a) = a (n)

using assms, func1_1_L1, pred_succ_eq, Last_def

The last element of a non-empty list valued in $X$ is in $X$ .

lemma last_type:

assumes $a \in NELists (X)$

shows

Last (a) \in X

using assms, last_seq_elem, apply_funtype unfolding NELists_def

The 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 n a t$ , $a : s u c c (s u c c (n)) \to X$

shows

Last (Tail (a)) = Last (a)

proof

from assms have

Last (Tail (a)) = Tail (a) (n)

using tail_props(1), last_seq_elem

also

from assms have

Tail (a) (n) = a (s u c c (n))

using tail_props(2)

also

from assms(2) have

a (s u c c (n)) = Last (a)

using last_seq_elem

finally show

t h e s i s

qed

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 n a t$ and A2: $a : s u c c (n) \to X$ , $b : s u c c (n) \to X$ and A3: $restrict (a, n) = restrict (b, n)$ and A4: $a (n) = b (n)$

shows

a = b

proof

{

fix

k

assume

k \in s u c c (n)

then have

k \in n \lor k = n

moreover {

assume

k \in n

then have

restrict (a, n) (k) = a (k)

and

restrict (b, n) (k) = b (k)

using restrict

with A3 have

a (k) = b (k)

} moreover {

assume

k = n

with A4 have

a (k) = b (k)

} ultimately have

a (k) = b (k)

}

then have

\forall k \in s u c c (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 n a t$ and A2: $a : n \to X$ and A3: $b : 1 \to X$

shows

Concat (a, b) = Append (a, b (0))

proof

let

C = Concat (a, b)

let

A = Append (a, b (0))

from A1, A2, A3 have I:

n \in n a t

1 \in n a t

a : n \to X

b : 1 \to X

have

C : s u c c (n) \to X

proof

from I have

C : n + 1 \to X

by (rule concat_props )

with A1 show

C : s u c c (n) \to X

qed

moreover

from A2, A3 have

A : s u c c (n) \to X

using apply_funtype, append_props

moreover

have

\forall k \in s u c c (n) . C (k) = A (k)

proof

fix

k

assume

k \in s u c c (n)

moreover {

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)

} moreover

have

C (n) = A (n)

proof

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

ultimately show

C (k) = A (k)

qed

ultimately show

C = A

by (rule func_eq )

qed

If $x \in X$ then the singleton set with the pair $⟨ 0, x ⟩$ as the only element is a list of length 1 and hence a nonempty list.

lemma list_len1_singleton:

assumes $x \in X$

shows

{⟨ 0, x ⟩} : 1 \to X

and

{⟨ 0, x ⟩} \in NELists (X)

proof

from assms have

{⟨ 0, x ⟩} : {0} \to X

using pair_func_singleton

moreover

have

{0} = 1

ultimately show

{⟨ 0, x ⟩} : 1 \to X

and

{⟨ 0, x ⟩} \in NELists (X)

unfolding NELists_def

qed

A singleton list is in fact a singleton set with a pair as the only element.

lemma list_singleton_pair:

assumes A1: $x : 1 \to X$

shows

x = {⟨ 0, x (0) ⟩}

proof

from A1 have

x = {⟨ t, x (t) ⟩ . t \in 1}

by (rule fun_is_set_of_pairs )

hence

x = {⟨ t, x (t) ⟩ . t \in {0}}

thus

t h e s i s

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

Append (0, x) : 1 \to X

and

Append (0, x) (0) = x

proof

let

a = Append (0, x)

have

a = {⟨ 0, x ⟩}

using Append_def

with A1 show

a : 1 \to X

and

a (0) = x

using list_len1_singleton, pair_func_singleton

qed

Appending an element is the same as concatenating with certain pair.

lemma append_concat_pair:

assumes $n \in n a t$ and $a : n \to X$ and $x \in X$

shows

Append (a, x) = Concat (a, {⟨ 0, x ⟩})

using assms, list_len1_singleton, append_1elem, pair_val

An 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 n a t$ , $k \in n a t$ and A2: $a : n \to X$ , $b : k \to X$ and A3: $x \in X$

shows

Append (Concat (a, b), x) = Concat (a, Append (b, x))

proof

from A1, A2, A3 have

n + k \in n a t

Concat (a, b) : n + k \to X

x \in X

using concat_props

then have

Append (Concat (a, b), x) = Concat (Concat (a, b), {⟨ 0, x ⟩})

by (rule append_concat_pair )

moreover

from A1, A2, A3 have

n \in n a t

k \in n a t

1 \in n a t

a : n \to X

b : k \to X

{⟨ 0, x ⟩} : 1 \to X

using list_len1_singleton

then have

Concat (Concat (a, b), {⟨ 0, x ⟩}) = Concat (a, Concat (b, {⟨ 0, x ⟩}))

by (rule concat_assoc )

moreover

from A1, A2, A3 have

Concat (b, {⟨ 0, x ⟩}) = Append (b, x)

using list_len1_singleton, append_1elem, pair_val

ultimately show

Append (Concat (a, b), x) = Concat (a, Append (b, x))

qed

An identity involving concatenating with init and appending the last element.

lemma concat_init_last_elem:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ and $b : s u c c (k) \to X$

shows

Append (Concat (a, Init (b)), b (k)) = Concat (a, b)

using assms, init_props, apply_funtype, concat_append_assoc

A lemma about creating lists by composition and how Append behaves in such case.

lemma list_compose_append:

assumes A1: $n \in n a t$ and A2: $a : n \to X$ and A3: $x \in X$ and A4: $c : X \to Y$

shows

c \circ Append (a, x) : s u c c (n) \to Y

c \circ Append (a, x) = Append (c \circ a, c (x))

proof

let

b = Append (a, x)

let

d = Append (c \circ a, c (x))

from A2, A4 have

c \circ a : n \to Y

using comp_fun

from A2, A3 have

b : s u c c (n) \to X

using append_props

with A4 show

c \circ b : s u c c (n) \to Y

using comp_fun

moreover

from A3, A4,

c \circ a : n \to Y

have

d : s u c c (n) \to Y

using apply_funtype, append_props

moreover

have

\forall k \in s u c c (n) . (c \circ b) (k) = d (k)

proof

{

fix

k

assume

k \in s u c c (n)

with

b : s u c c (n) \to X

have

(c \circ b) (k) = c (b (k))

using comp_fun_apply

with A2, A3, A4,

c \circ a : n \to Y

c \circ a : n \to Y

k \in s u c c (n)

have

(c \circ b) (k) = d (k)

using append_props, comp_fun_apply, apply_funtype

}

thus

t h e s i s

qed

ultimately show

c \circ b = d

by (rule func_eq )

qed

A lemma about appending an element to a list defined by set comprehension.

lemma set_list_append:

assumes A1: $\forall i \in s u c c (k) . b (i) \in X$ and A2: $a = {⟨ i, b (i) ⟩ . i \in s u c c (k)}$

shows

a : s u c c (k) \to X

{⟨ i, b (i) ⟩ . i \in k} : k \to X

a = Append ({⟨ i, b (i) ⟩ . i \in k}, b (k))

proof

from A1 have

{⟨ i, b (i) ⟩ . i \in s u c c (k)} : s u c c (k) \to X

by (rule ZF_fun_from_total )

with A2 show

a : s u c c (k) \to X

from A1 have

\forall i \in k . b (i) \in X

then show

{⟨ i, b (i) ⟩ . i \in k} : k \to X

by (rule ZF_fun_from_total )

with A2 show

a = Append ({⟨ i, b (i) ⟩ . i \in k}, b (k))

using func1_1_L1, Append_def

qed

A version of set_list_append using $n + 1$ instead of $s u c c (n)$ .

lemma set_list_append1:

assumes $n \in n a t$ and $\forall k \in n + 1. q (k) \in X$

defines $a \equiv {⟨ k, q (k) ⟩ . k \in n + 1}$

shows

a : n + 1 \to X

{⟨ k, q (k) ⟩ . k \in n} : n \to X

Init (a) = {⟨ k, q (k) ⟩ . k \in n}

a = Append ({⟨ k, q (k) ⟩ . k \in n}, q (n))

a = Append (Init (a), q (n))

a = Append (Init (a), a (n))

proof

from assms(1) have I:

n + 1 = s u c c (n)

using succ_add_one(1)

with assms show

a : n + 1 \to X

and

{⟨ k, q (k) ⟩ . k \in n} : n \to X

and II:

Init (a) = {⟨ k, q (k) ⟩ . k \in n}

using set_list_append(1,2), init_def_alt

from assms(2,3), I have

\forall k \in s u c c (n) . q (k) \in X

and

a = {⟨ k, q (k) ⟩ . k \in s u c c (n)}

then show

a = Append ({⟨ k, q (k) ⟩ . k \in n}, q (n))

using set_list_append(3)

with II show

a = Append (Init (a), q (n))

from I have

n \in n + 1

then have

{⟨ k, q (k) ⟩ . k \in n + 1} (n) = q (n)

by (rule ZF_fun_from_tot_val1 )

with assms(3),

a = Append (Init (a), q (n))

show

a = Append (Init (a), a (n))

qed

An induction theorem for lists.

lemma list_induct:

assumes A1: $\forall b \in 1 \to X . P (b)$ and A2: $\forall b \in NELists (X) . P (b) ⟶ (\forall x \in X . P (Append (b, x)))$ and A3: $d \in NELists (X)$

shows

P (d)

proof

{

fix

n

assume

n \in n a t

moreover

from A1 have

\forall b \in s u c c (0) \to X . P (b)

moreover

have

\forall k \in n a t . ((\forall b \in s u c c (k) \to X . P (b)) ⟶ (\forall c \in s u c c (s u c c (k)) \to X . P (c)))

proof

{

fix

k

assume

k \in n a t

assume

\forall b \in s u c c (k) \to X . P (b)

have

\forall c \in s u c c (s u c c (k)) \to X . P (c)

proof

fix

c

assume

c : s u c c (s u c c (k)) \to X

let

b = Init (c)

let

x = c (s u c c (k))

from

k \in n a t

c : s u c c (s u c c (k)) \to X

have

b : s u c c (k) \to X

using init_props

with A2,

k \in n a t

\forall b \in s u c c (k) \to X . P (b)

have

\forall x \in X . P (Append (b, x))

using NELists_def

with

c : s u c c (s u c c (k)) \to X

have

P (Append (b, x))

using apply_funtype

with

k \in n a t

c : s u c c (s u c c (k)) \to X

show

P (c)

using init_props

qed

}

thus

t h e s i s

qed

ultimately have

\forall b \in s u c c (n) \to X . P (b)

by (rule ind_on_nat )

}

with A3 show

t h e s i s

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

$Prepend (a, x) \equiv {⟨ k, if k = 0 then x else a (k - 1) ⟩ . k \in d o m a i n (a) + 1}$

If $a : n \to 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 n a t$ , $a : n \to X$ , $x \in X$

shows

Prepend (a, x) : (n + 1) \to X

and

Prepend (a, x) (0) = x

proof

let

b = {⟨ k, if k = 0 then x else a (k - 1) ⟩ . k \in n + 1}

have

\forall k \in n + 1. (if k = 0 then x else a (k - 1)) \in X

proof

{

fix

k

assume

k \in n + 1

let

v = if k = 0 then x 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 n a t

using elem_nat_is_nat(2)

from assms(1) have

s u c c (n) = n + 1

using succ_add_one(1)

with

k \in n + 1

have

k \in s u c c (n)

with assms(1),

n \neq 0

have

p r e d (k) \in n

using pred_succ_mem

with assms(2),

k \in n a t

k \neq 0

have

v \in X

using pred_minus_one, apply_funtype

}

with assms(3) have

v \in X

}

thus

t h e s i s

qed

then have

b : (n + 1) \to X

by (rule ZF_fun_from_total )

with assms(2) show

Prepend (a, x) : (n + 1) \to 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) = (if 0 = 0 then x else a (0 - 1))

by (rule ZF_fun_from_tot_val1 )

with assms(2) show

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 n a t$ , $a : n \to X$ , $x \in X$ , $k \in n$

shows

Prepend (a, x) (k + 1) = a (k)

proof

let

b = {⟨ k, if k = 0 then x else a (k - 1) ⟩ . k \in n + 1}

from assms(1,4) have

k \in n a t

using elem_nat_is_nat(2)

with assms(1) have

s u c c (n) = n + 1

and

s u c c (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) = (if k + 1 = 0 then x else a ((k + 1) - 1))

by (rule ZF_fun_from_tot_val1 )

with assms(2),

k \in n a t

show

t h e s i s

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 n a t$ , $a : n \to X$ , $x \in X$

shows

Tail (Prepend (a, x)) = a

proof

let

b = Prepend (a, x)

from assms have

b : (n + 1) \to X

using prepend_props(1)

with assms(1) have

Tail (b) : n \to X

using tail_props(1)

from assms,

b : (n + 1) \to X

have

\forall k \in n . Tail (b) (k) = a (k)

using tail_props2, prepend_val

with assms(2),

Tail (b) : n \to X

show

t h e s i s

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) \to X$ of lists of length $n + 1$ of elements of $X$ and the cartesian product $(n \to X) \times X$ .

lemma lists_cart_prod:

assumes $n \in n a t$

shows

{⟨ x, ⟨ Init (x), x (n) ⟩ ⟩ . x \in s u c c (n) \to X} \in bij (s u c c (n) \to X, (n \to X) \times X)

proof

let

f = {⟨ x, ⟨ Init (x), x (n) ⟩ ⟩ . x \in s u c c (n) \to X}

from assms have

\forall x \in s u c c (n) \to X . ⟨ Init (x), x (n) ⟩ \in (n \to X) \times X

using init_props, succ_iff, apply_funtype

then have I:

f : (s u c c (n) \to X) \to ((n \to X) \times X)

by (rule ZF_fun_from_total )

moreover

from assms, I have

\forall x \in s u c c (n) \to X . \forall y \in s u c c (n) \to X . f (x) = f (y) ⟶ x = y

using ZF_fun_from_tot_val, init_def, finseq_restr_eq

moreover

have

\forall p \in (n \to X) \times X . \exists x \in s u c c (n) \to X . f (x) = p

proof

fix

p

assume

p \in (n \to X) \times X

let

x = Append (fst (p), snd (p))

from assms,

p \in (n \to X) \times X

have

x : s u c c (n) \to X

using append_props

with I have

f (x) = ⟨ Init (x), x (n) ⟩

using succ_iff, ZF_fun_from_tot_val

moreover

from assms,

p \in (n \to X) \times X

have

Init (x) = fst (p)

and

x (n) = snd (p)

using init_append, append_props

ultimately have

f (x) = ⟨ fst (p), snd (p) ⟩

with

p \in (n \to X) \times X

x : s u c c (n) \to X

show

\exists x \in s u c c (n) \to X . f (x) = p

qed

ultimately show

t h e s i s

using inj_def, surj_def, bij_def

qed

We can identify a set $X$ with lists of length one of elements of $X$ .

lemma singleton_list_bij:

shows

{⟨ x, x (0) ⟩ . x \in 1 \to X} \in bij (1 \to X, X)

proof

let

f = {⟨ x, x (0) ⟩ . x \in 1 \to X}

have

\forall x \in 1 \to X . x (0) \in X

using apply_funtype

then have I:

f : (1 \to X) \to X

by (rule ZF_fun_from_total )

moreover

have

\forall x \in 1 \to X . \forall y \in 1 \to X . f (x) = f (y) ⟶ x = y

proof

{

fix

x

y

assume

x : 1 \to X

y : 1 \to X

and

f (x) = f (y)

with I have

x (0) = y (0)

using ZF_fun_from_tot_val

moreover

from

x : 1 \to X

y : 1 \to X

have

x = {⟨ 0, x (0) ⟩}

and

y = {⟨ 0, y (0) ⟩}

using list_singleton_pair

ultimately have

x = y

}

thus

t h e s i s

qed

moreover

have

\forall y \in X . \exists x \in 1 \to X . f (x) = y

proof

fix

y

assume

y \in X

let

x = {⟨ 0, y ⟩}

from I,

y \in X

have

x : 1 \to X

and

f (x) = y

using list_len1_singleton, ZF_fun_from_tot_val, pair_val

thus

\exists x \in 1 \to X . f (x) = y

qed

ultimately show

t h e s i s

using inj_def, surj_def, bij_def

qed

We can identify a set of $X$ -valued lists of length with $X$ .

lemma list_singleton_bij:

shows

{⟨ x, {⟨ 0, x ⟩} ⟩ . x \in X} \in bij (X, 1 \to X)

and

{⟨ y, y (0) ⟩ . y \in 1 \to X} = c o n v e r s e ({⟨ x, {⟨ 0, x ⟩} ⟩ . x \in X})

and

{⟨ x, {⟨ 0, x ⟩} ⟩ . x \in X} = c o n v e r s e ({⟨ y, y (0) ⟩ . y \in 1 \to X})

proof

let

f = {⟨ y, y (0) ⟩ . y \in 1 \to X}

let

g = {⟨ x, {⟨ 0, x ⟩} ⟩ . x \in X}

have

1 = {0}

then have

f \in bij (1 \to X, X)

and

g : X \to (1 \to X)

using singleton_list_bij, pair_func_singleton, ZF_fun_from_total

moreover

have

\forall y \in 1 \to X . g (f (y)) = y

proof

fix

y

assume

y : 1 \to X

have

f : (1 \to X) \to X

using singleton_list_bij, bij_def, inj_def

with

1 = {0}

y : 1 \to X

g : X \to (1 \to X)

show

g (f (y)) = y

using ZF_fun_from_tot_val, apply_funtype, func_singleton_pair

qed

ultimately show

g \in bij (X, 1 \to X)

and

f = c o n v e r s e (g)

and

g = c o n v e r s e (f)

using comp_conv_id

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 \to X . x (0) \in U} = {{⟨ 0, y ⟩} . y \in U}

proof

have

1 = {0}

{

fix

x

assume

x \in {x \in 1 \to X . x (0) \in U}

with

1 = {0}

have

x = {⟨ 0, x (0) ⟩}

using func_singleton_pair

}

thus

{x \in 1 \to X . x (0) \in U} \subseteq {{⟨ 0, y ⟩} . y \in U}

{

fix

x

assume

x \in {{⟨ 0, y ⟩} . y \in U}

then obtain

y

where

x = {⟨ 0, y ⟩}

and

y \in U

with

1 = {0}

, assms have

x : 1 \to X

using pair_func_singleton

}

thus

{{⟨ 0, y ⟩} . y \in U} \subseteq {x \in 1 \to 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 n a t$ and A2: $U \subseteq n \to X$ and A3: $V \subseteq X$

shows

{x \in s u c c (n) \to X . Init (x) \in U \land x (n) \in V} = (⋃ y \in V . {Append (x, y) . x \in U})

proof

{

fix

x

assume

x \in {x \in s u c c (n) \to X . Init (x) \in U \land x (n) \in V}

then have

x \in s u c c (n) \to X

and

Init (x) \in U

and I:

x (n) \in V

let

y = x (n)

from A1, and,

x \in s u c c (n) \to X

have

x = Append (Init (x), y)

using init_props

with I, and,

Init (x) \in U

have

x \in (⋃ y \in V . {Append (a, y) . a \in U})

}

moreover {

fix

x

assume

x \in (⋃ y \in V . {Append (a, y) . a \in U})

then obtain

a

y

where

y \in V

and

a \in U

and

x = Append (a, y)

with A2, A3 have

x : s u c c (n) \to X

using append_props

from A2, A3,

y \in V

a \in U

have

a : n \to X

and

y \in X

with A1,

a \in U

y \in V

x = Append (a, y)

have

Init (x) \in U

and

x (n) \in V

using append_props, init_append

with

x : s u c c (n) \to X

have

x \in {x \in s u c c (n) \to X . Init (x) \in U \land x (n) \in V}

} ultimately show

t h e s i s

qed

end

lemma func1_1_L1:

assumes $f : A \to C$

shows

d o m a i n (f) = A

lemma elem_nat_is_nat:

assumes $n \in n a t$ and $k \in n$

shows

k < n

k \in n a t

k \leq n

⟨ k, n ⟩ \in L e

lemma succ_add_one:

assumes $n \in n a t$

shows

n + 1 = s u c c (n)

n + 1 \in n a t

{0} + n = s u c c (n)

n + {0} = s u c c (n)

s u c c (n) \in n a t

0 \in n + 1

n \subseteq n + 1

Definition of Tail:

Tail (a) \equiv {⟨ k, a (s u c c (k)) ⟩ . k \in p r e d (d o m a i n (a))}

lemma ZF_fun_from_total:

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

shows

{⟨ x, b (x) ⟩ . x \in X} : X \to Y

lemma tail_as_set:

assumes $n \in n a t$ and $a : n + 1 \to X$

shows

Tail (a) = {⟨ k, a (k + 1) ⟩ . k \in n}

lemma succ_ineq1:

assumes $n \in n a t$ , $i \in n$

shows

s u c c (i) \in s u c c (n)

i + 1 \in n + 1

i \in n + 1

lemma ZF_fun_from_tot_val1:

assumes $x \in X$

shows

{⟨ x, b (x) ⟩ . x \in X} (x) = b (x)

lemma codomain_nonempty:

assumes $f : X \to Y$ , $X \neq \emptyset$

shows

Y \neq \emptyset

lemma inter_diff_in_len:

assumes $k \in n a t$ and $i \in N a t Interval (n, k)$

shows

i - n \in k

Definition of ShiftedSeq:

ShiftedSeq (b, n) \equiv {⟨ j, b (j - n) ⟩ . j \in N a t Interval (n, d o m a i n (b))}

lemma ZF_fun_from_tot_val:

assumes $f : X \to Y$ , $x \in X$ and $f = {⟨ x, b (x) ⟩ . x \in X}$

shows

f (x) = b (x)

and

b (x) \in Y

lemma elem_nat_is_nat:

assumes $n \in n a t$ and $k \in n$

shows

k < n

k \in n a t

k \leq n

⟨ k, n ⟩ \in L e

Definition of NatInterval:

N a t Interval (n, k) \equiv {n + j . j \in k}

lemma shifted_seq_props:

assumes $n \in n a t$ , $k \in n a t$ and $b : k \to X$

shows

ShiftedSeq (b, n) : N a t Interval (n, k) \to X

\forall i \in N a t Interval (n, k) . ShiftedSeq (b, n) (i) = b (i - n)

\forall j \in k . ShiftedSeq (b, n) (n + j) = b (j)

lemma length_start_decomp:

assumes $n \in n a t$ , $k \in n a t$

shows

n \cap N a t Interval (n, k) = 0

n \cup N a t Interval (n, k) = n + k

Definition of Concat:

Concat (a, b) \equiv a \cup ShiftedSeq (b, d o m a i n (a))

theorem concat_props:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ , $b : k \to X$

shows

Concat (a, b) : n + k \to X

\forall i \in n . Concat (a, b) (i) = a (i)

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

\forall j \in k . Concat (a, b) (n + j) = b (j)

lemma add_nat_le:

assumes $n \in n a t$ and $k \in n a t$

shows

n \leq n + k

n \subseteq n + k

n \subseteq k + n

lemma add_lt_mono:

assumes $k \in n a t$ and $j \in k$

shows

(n + j) < (n + k)

(n + j) \in (n + k)

lemma concat_concat_list:

assumes $n \in n a t$ , $k \in n a t$ , $m \in n a t$ and $a : n \to X$ , $b : k \to X$ , $c : m \to X$ and $d = Concat (Concat (a, b), c)$

shows

d : n + k + m \to 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 n a t$ , $k \in n a t$ , $m \in n a t$ and $a : n \to X$ , $b : k \to X$ , $c : m \to X$ and $e = Concat (a, Concat (b, c))$

shows

e : n + k + m \to 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 n a t$ , $k \in n a t$ , $m \in n a t$

shows

n + k + m = (n + k) \cup N a t Interval (n + k, m)

n + k + m = n \cup N a t Interval (n, k + m)

n + k + m = n \cup N a t Interval (n, k) \cup N a t Interval (n + k, m)

lemma func_eq:

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

shows

f = g

lemma succ_ineq:

assumes $n \in n a t$

shows

\forall i \in n . s u c c (i) \in s u c c (n)

lemma ZF_fun_from_tot_val0:

assumes $f : X \to Y$ and $f = {⟨ x, b (x) ⟩ . x \in X}$

shows

\forall x \in X . f (x) = b (x)

theorem tail_props:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Tail (a) : n \to X

\forall k \in n . Tail (a) (k) = a (s u c c (k))

lemma empty_in_every_succ:

assumes $n \in n a t$

shows

0 \in s u c c (n)

lemma pair_func_singleton:

assumes $y \in Y$

shows

{⟨ x, y ⟩} : {x} \to Y

lemma one_is_nat: shows

{0} \in n a t

{0} = s u c c (0)

{0} = 1

theorem tail_props:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Tail (a) : n \to X

\forall k \in n . Tail (a) (k) = a (s u c c (k))

theorem concat_props:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ , $b : k \to X$

shows

Concat (a, b) : n + k \to X

\forall i \in n . Concat (a, b) (i) = a (i)

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

\forall j \in k . Concat (a, b) (n + j) = b (j)

lemma succ_add_one:

assumes $n \in n a t$

shows

n + 1 = s u c c (n)

n + 1 \in n a t

{0} + n = s u c c (n)

n + {0} = s u c c (n)

s u c c (n) \in n a t

0 \in n + 1

n \subseteq n + 1

theorem concat_props:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ , $b : k \to X$

shows

Concat (a, b) : n + k \to X

\forall i \in n . Concat (a, b) (i) = a (i)

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

\forall j \in k . Concat (a, b) (n + j) = b (j)

lemma pair_val: shows

{⟨ x, y ⟩} (x) = y

lemma Nat_ZF_1_L3:

assumes $n \in n a t$ and $n \neq 0$

shows

\exists k \in n a t . n = s u c c (k)

lemma succ_mem:

assumes $n \in n a t$ , $s u c c (k) \in s u c c (n)$

shows

k \in n

theorem concat_props:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ , $b : k \to X$

shows

Concat (a, b) : n + k \to X

\forall i \in n . Concat (a, b) (i) = a (i)

\forall i \in N a t Interval (n, k) . Concat (a, b) (i) = b (i - n)

\forall j \in k . Concat (a, b) (n + j) = b (j)

Definition of Append:

Append (a, x) \equiv a \cup {⟨ d o m a i n (a), x ⟩}

lemma func1_1_L11D:

assumes $f : X \to Y$ and $a \notin X$ and $g = f \cup {⟨ a, b ⟩}$

shows

g : X \cup {a} \to Y \cup {b}

\forall x \in X . g (x) = f (x)

g (a) = b

lemma succ_explained: shows

s u c c (n) = n \cup {n}

lemma set_elem_add:

assumes $x \in X$

shows

X \cup {x} = X

theorem append_props:

assumes $a : n \to X$ and $x \in X$ and $b = Append (a, x)$

shows

b : s u c c (n) \to X

\forall k \in n . b (k) = a (k)

b (n) = x

theorem tail_props:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Tail (a) : n \to X

\forall k \in n . Tail (a) (k) = a (s u c c (k))

Definition of Lists:

Lists (X) \equiv ⋃ n \in n a t . (n \to X)

Definition of NELists:

NELists (X) \equiv ⋃ n \in n a t . (s u c c (n) \to X)

Definition of Init:

Init (a) \equiv restrict (a, p r e d (d o m a i n (a)))

theorem init_props:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Init (a) : n \to X

\forall k \in n . Init (a) (k) = a (k)

a = Append (Init (a), a (n))

theorem init_props:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Init (a) : n \to X

\forall k \in n . Init (a) (k) = a (k)

a = Append (Init (a), a (n))

lemma init_def:

assumes $n \in n a t$ and $a : s u c c (n) \to X$

shows

Init (a) = restrict (a, n)

lemma restrict_def_alt:

assumes $A \subseteq X$

shows

restrict ({⟨ x, q (x) ⟩ . x \in X}, A) = {⟨ x, q (x) ⟩ . x \in A}

lemma bij_extend_point:

assumes $f \in bij (X, Y)$ , $a \notin X$ , $b \notin Y$

shows

(f \cup {⟨ a, b ⟩}) \in bij (X \cup {a}, Y \cup {b})

lemma func1_1_L1B:

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

shows

f : X \to Z

Definition of Last:

Last (a) \equiv a (p r e d (d o m a i n (a)))

lemma last_seq_elem:

assumes $a : s u c c (n) \to X$

shows

Last (a) = a (n)

theorem fun_is_set_of_pairs:

assumes $f : X \to Y$

shows

f = {⟨ x, f (x) ⟩ . x \in X}

lemma list_len1_singleton:

assumes $x \in X$

shows

{⟨ 0, x ⟩} : 1 \to X

and

{⟨ 0, x ⟩} \in NELists (X)

lemma append_1elem:

assumes $n \in n a t$ and $a : n \to X$ and $b : 1 \to X$

shows

Concat (a, b) = Append (a, b (0))

lemma append_concat_pair:

assumes $n \in n a t$ and $a : n \to X$ and $x \in X$

shows

Append (a, x) = Concat (a, {⟨ 0, x ⟩})

theorem concat_assoc:

assumes $n \in n a t$ , $k \in n a t$ , $m \in n a t$ and $a : n \to X$ , $b : k \to X$ , $c : m \to X$

shows

Concat (Concat (a, b), c) = Concat (a, Concat (b, c))

lemma concat_append_assoc:

assumes $n \in n a t$ , $k \in n a t$ and $a : n \to X$ , $b : k \to X$ and $x \in X$

shows

Append (Concat (a, b), x) = Concat (a, Append (b, x))

lemma set_list_append:

assumes $\forall i \in s u c c (k) . b (i) \in X$ and $a = {⟨ i, b (i) ⟩ . i \in s u c c (k)}$

shows

a : s u c c (k) \to X

{⟨ i, b (i) ⟩ . i \in k} : k \to X

a = Append ({⟨ i, b (i) ⟩ . i \in k}, b (k))

lemma init_def_alt:

assumes $n \in n a t$ and $\forall k \in n + 1. q (k) \in X$

shows

Init ({⟨ k, q (k) ⟩ . k \in n + 1}) = {⟨ k, q (k) ⟩ . k \in n}

lemma set_list_append:

assumes $\forall i \in s u c c (k) . b (i) \in X$ and $a = {⟨ i, b (i) ⟩ . i \in s u c c (k)}$

shows

a : s u c c (k) \to X

{⟨ i, b (i) ⟩ . i \in k} : k \to X

a = Append ({⟨ i, b (i) ⟩ . i \in k}, b (k))

theorem ind_on_nat:

assumes $n \in n a t$ and $P (0)$ and $\forall k \in n a t . P (k) ⟶ P (s u c c (k))$

shows

P (n)

lemma pred_succ_mem:

assumes $n \in n a t$ , $n \neq 0$ , $k \in s u c c (n)$

shows

p r e d (k) \in n

lemma pred_minus_one:

assumes $n \in n a t$ , $n \neq 0$

shows

n - 1 = p r e d (n)

Definition of Prepend:

Prepend (a, x) \equiv {⟨ k, if k = 0 then x else a (k - 1) ⟩ . k \in d o m a i n (a) + 1}

lemma prepend_props:

assumes $n \in n a t$ , $a : n \to X$ , $x \in X$

shows

Prepend (a, x) : (n + 1) \to X

and

Prepend (a, x) (0) = x

lemma tail_props2:

assumes $n \in n a t$ , $a : n + 1 \to X$ , $k \in n$

shows

Tail (a) (k) = a (k + 1)

lemma prepend_val:

assumes $n \in n a t$ , $a : n \to X$ , $x \in X$ , $k \in n$

shows

Prepend (a, x) (k + 1) = a (k)

lemma finseq_restr_eq:

assumes $n \in n a t$ and $a : s u c c (n) \to X$ , $b : s u c c (n) \to X$ and $restrict (a, n) = restrict (b, n)$ and $a (n) = b (n)$