(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2007 Slawomir Kolodynski

This program is free software Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED

WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF

MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,

PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS

OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,

WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR

OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,

EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

header{*\isaheader{FiniteSeq\_ZF.thy}*}

theory FiniteSeq_ZF imports Nat_ZF_IML func1

begin

text{* 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.*}

section{*Lists as finite sequences*}

text{*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$.

*}

text{*We define the set of lists with values in set $X$ as @{text "Lists(X)"}.*}

definition

"Lists(X) ≡ \<Union>n∈nat.(n->X)"

text{*The set of nonempty $X$-value listst will be called @{text "NELists(X)"}.*}

definition

"NELists(X) ≡ \<Union>n∈nat.(succ(n)->X)"

text{*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

@{text "pred(n)"} is the previous natural number and

denotes the difference between natural numbers $n$ and $k$.*}

definition

"ShiftedSeq(b,n) ≡ {⟨j, b`(j #- n)⟩. j ∈ NatInterval(n,domain(b))}"

text{*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

"Concat(a,b) ≡ a ∪ ShiftedSeq(b,domain(a))"

text{* 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 @{text "Tail"} here as well.*}

definition

"Tail(a) ≡ {⟨k, a`(succ(k))⟩. k ∈ pred(domain(a))}"

text{*A dual notion to @{text "Tail"} is the list

of all elements of a list except the last one. Borrowing

the terminology from Haskell again, we will call this @{text "Init"}.*}

definition

"Init(a) ≡ restrict(a,pred(domain(a)))"

text{* Another obvious operation we can talk about is appending an element

at the end of a sequence. This is called @{text "Append"}.*}

definition

"Append(a,x) ≡ a ∪ {⟨domain(a),x⟩}"

text{*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 @{text "Last"}

element of a list. *}

definition

"Last(a) ≡ a`(pred(domain(a)))"

text{*Shifted sequence is a function on a the interval of natural numbers.*}

lemma shifted_seq_props:

assumes A1: "n ∈ nat" "k ∈ nat" and A2: "b:k->X"

shows

"ShiftedSeq(b,n): NatInterval(n,k) -> X"

"∀i ∈ NatInterval(n,k). ShiftedSeq(b,n)`(i) = b`(i #- n)"

"∀j∈k. ShiftedSeq(b,n)`(n #+ j) = b`(j)"

proof -

let ?I = "NatInterval(n,domain(b))"

from A2 have Fact: "?I = NatInterval(n,k)" using func1_1_L1 by simp

with A1 A2 have "∀j∈ ?I. b`(j #- n) ∈ X"

using inter_diff_in_len apply_funtype by simp

then have

"{⟨j, b`(j #- n)⟩. j ∈ ?I} : ?I -> X" by (rule ZF_fun_from_total)

with Fact show thesis_1: "ShiftedSeq(b,n): NatInterval(n,k) -> X"

using ShiftedSeq_def by simp

{ fix i

from Fact thesis_1 have "ShiftedSeq(b,n): ?I -> X" by simp

moreover

assume "i ∈ NatInterval(n,k)"

with Fact have "i ∈ ?I" by simp

moreover from Fact have

"ShiftedSeq(b,n) = {⟨i, b`(i #- n)⟩. i ∈ ?I}"

using ShiftedSeq_def by simp

ultimately have "ShiftedSeq(b,n)`(i) = b`(i #- n)"

by (rule ZF_fun_from_tot_val)

} then show thesis1:

"∀i ∈ NatInterval(n,k). ShiftedSeq(b,n)`(i) = b`(i #- n)"

by simp

{ fix j

let ?i = "n #+ j"

assume A3: "j∈k"

with A1 have "j ∈ nat" using elem_nat_is_nat by blast

then have "?i #- n = j" using diff_add_inverse by simp

with A3 thesis1 have "ShiftedSeq(b,n)`(?i) = b`(j)"

using NatInterval_def by auto

} then show "∀j∈k. ShiftedSeq(b,n)`(n #+ j) = b`(j)"

by simp

qed

text{*Basis properties of the contatenation of two finite sequences.*}

theorem concat_props:

assumes A1: "n ∈ nat" "k ∈ nat" and A2: "a:n->X" "b:k->X"

shows

"Concat(a,b): n #+ k -> X"

"∀i∈n. Concat(a,b)`(i) = a`(i)"

"∀i ∈ NatInterval(n,k). Concat(a,b)`(i) = b`(i #- n)"

"∀j ∈ k. Concat(a,b)`(n #+ j) = b`(j)"

proof -

from A1 A2 have

"a:n->X" and I: "ShiftedSeq(b,n): NatInterval(n,k) -> X"

and "n ∩ NatInterval(n,k) = 0"

using shifted_seq_props length_start_decomp by auto

then have

"a ∪ ShiftedSeq(b,n): n ∪ NatInterval(n,k) -> X ∪ X"

by (rule fun_disjoint_Un)

with A1 A2 show "Concat(a,b): n #+ k -> X"

using func1_1_L1 Concat_def length_start_decomp by auto

{ fix i assume "i ∈ n"

with A1 I have "i ∉ domain(ShiftedSeq(b,n))"

using length_start_decomp func1_1_L1 by auto

with A2 have "Concat(a,b)`(i) = a`(i)"

using func1_1_L1 fun_disjoint_apply1 Concat_def by simp

} thus "∀i∈n. Concat(a,b)`(i) = a`(i)" by simp

{ fix i assume A3: "i ∈ NatInterval(n,k)"

with A1 A2 have "i ∉ domain(a)"

using length_start_decomp func1_1_L1 by auto

with A1 A2 A3 have "Concat(a,b)`(i) = b`(i #- n)"

using func1_1_L1 fun_disjoint_apply2 Concat_def shifted_seq_props

by simp

} thus II: "∀i ∈ NatInterval(n,k). Concat(a,b)`(i) = b`(i #- n)"

by simp

{ fix j

let ?i = "n #+ j"

assume A3: "j∈k"

with A1 have "j ∈ nat" using elem_nat_is_nat by blast

then have "?i #- n = j" using diff_add_inverse by simp

with A3 II have "Concat(a,b)`(?i) = b`(j)"

using NatInterval_def by auto

} thus "∀j ∈ k. Concat(a,b)`(n #+ j) = b`(j)"

by simp

qed

text{*Properties of concatenating three lists.*}

lemma concat_concat_list:

assumes A1: "n ∈ nat" "k ∈ nat" "m ∈ nat" and

A2: "a:n->X" "b:k->X" "c:m->X" and

A3: "d = Concat(Concat(a,b),c)"

shows

"d : n #+k #+ m -> X"

"∀j ∈ n. d`(j) = a`(j)"

"∀j ∈ k. d`(n #+ j) = b`(j)"

"∀j ∈ m. d`(n #+ k #+ j) = c`(j)"

proof -

from A1 A2 have I:

"n #+ k ∈ nat" "m ∈ nat"

"Concat(a,b): n #+ k -> X" "c:m->X"

using concat_props by auto

with A3 show "d: n #+k #+ m -> X"

using concat_props by simp

from I have II: "∀i ∈ n #+ k.

Concat(Concat(a,b),c)`(i) = Concat(a,b)`(i)"

by (rule concat_props)

{ fix j assume A4: "j ∈ n"

moreover from A1 have "n ⊆ n #+ k" using add_nat_le by simp

ultimately have "j ∈ n #+ k" by auto

with A3 II have "d`(j) = Concat(a,b)`(j)" by simp

with A1 A2 A4 have "d`(j) = a`(j)"

using concat_props by simp

} thus "∀j ∈ n. d`(j) = a`(j)" by simp

{ fix j assume A5: "j ∈ k"

with A1 A3 II have "d`(n #+ j) = Concat(a,b)`(n #+ j)"

using add_lt_mono by simp

also from A1 A2 A5 have "… = b`(j)"

using concat_props by simp

finally have "d`(n #+ j) = b`(j)" by simp

} thus "∀j ∈ k. d`(n #+ j) = b`(j)" by simp

from I have "∀j ∈ m. Concat(Concat(a,b),c)`(n #+ k #+ j) = c`(j)"

by (rule concat_props)

with A3 show "∀j ∈ m. d`(n #+ k #+ j) = c`(j)"

by simp

qed

text{*Properties of concatenating a list with a concatenation

of two other lists.*}

lemma concat_list_concat:

assumes A1: "n ∈ nat" "k ∈ nat" "m ∈ nat" and

A2: "a:n->X" "b:k->X" "c:m->X" and

A3: "e = Concat(a, Concat(b,c))"

shows

"e : n #+k #+ m -> X"

"∀j ∈ n. e`(j) = a`(j)"

"∀j ∈ k. e`(n #+ j) = b`(j)"

"∀j ∈ m. e`(n #+ k #+ j) = c`(j)"

proof -

from A1 A2 have I:

"n ∈ nat" "k #+ m ∈ nat"

"a:n->X" "Concat(b,c): k #+ m -> X"

using concat_props by auto

with A3 show "e : n #+k #+ m -> X"

using concat_props add_assoc by simp

from I have "∀j ∈ n. Concat(a, Concat(b,c))`(j) = a`(j)"

by (rule concat_props)

with A3 show "∀j ∈ n. e`(j) = a`(j)" by simp

from I have II:

"∀j ∈ k #+ m. Concat(a, Concat(b,c))`(n #+ j) = Concat(b,c)`(j)"

by (rule concat_props)

{ fix j assume A4: "j ∈ k"

moreover from A1 have "k ⊆ k #+ m" using add_nat_le by simp

ultimately have "j ∈ k #+ m" by auto

with A3 II have "e`(n #+ j) = Concat(b,c)`(j)" by simp

also from A1 A2 A4 have "… = b`(j)"

using concat_props by simp

finally have "e`(n #+ j) = b`(j)" by simp

} thus "∀j ∈ k. e`(n #+ j) = b`(j)" by simp

{ fix j assume A5: "j ∈ m"

with A1 II A3 have "e`(n #+ k #+ j) = Concat(b,c)`(k #+ j)"

using add_lt_mono add_assoc by simp

also from A1 A2 A5 have "… = c`(j)"

using concat_props by simp

finally have "e`(n #+ k #+ j) = c`(j)" by simp

} then show "∀j ∈ m. e`(n #+ k #+ j) = c`(j)"

by simp

qed

text{*Concatenation is associative.*}

theorem concat_assoc:

assumes A1: "n ∈ nat" "k ∈ nat" "m ∈ nat" and

A2: "a:n->X" "b:k->X" "c:m->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

"?d : n #+k #+ m -> X" and "?e : n #+k #+ m -> X"

using concat_concat_list concat_list_concat by auto

moreover have "∀i ∈ n #+k #+ m. ?d`(i) = ?e`(i)"

proof -

{ fix i assume "i ∈ n #+k #+ m"

moreover from A1 have

"n #+k #+ m = n ∪ NatInterval(n,k) ∪ NatInterval(n #+ k,m)"

using adjacent_intervals3 by simp

ultimately have

"i ∈ n ∨ i ∈ NatInterval(n,k) ∨ i ∈ NatInterval(n #+ k,m)"

by simp

moreover

{ assume "i ∈ n"

with A1 A2 have "?d`(i) = ?e`(i)"

using concat_concat_list concat_list_concat by simp }

moreover

{ assume "i ∈ NatInterval(n,k)"

then obtain j where "j∈k" and "i = n #+ j"

using NatInterval_def by auto

with A1 A2 have "?d`(i) = ?e`(i)"

using concat_concat_list concat_list_concat by simp }

moreover

{ assume "i ∈ NatInterval(n #+ k,m)"

then obtain j where "j ∈ m" and "i = n #+ k #+ j"

using NatInterval_def by auto

with A1 A2 have "?d`(i) = ?e`(i)"

using concat_concat_list concat_list_concat by simp }

ultimately have "?d`(i) = ?e`(i)" by auto

} thus ?thesis by simp

qed

ultimately show "?d = ?e" by (rule func_eq)

qed

text{*Properties of @{text "Tail"}.*}

theorem tail_props:

assumes A1: "n ∈ nat" and A2: "a: succ(n) -> X"

shows

"Tail(a) : n -> X"

"∀k ∈ n. Tail(a)`(k) = a`(succ(k))"

proof -

from A1 A2 have "∀k ∈ n. a`(succ(k)) ∈ X"

using succ_ineq apply_funtype by simp

then have "{⟨k, a`(succ(k))⟩. k ∈ n} : n -> X"

by (rule ZF_fun_from_total)

with A2 show I: "Tail(a) : n -> X"

using func1_1_L1 pred_succ_eq Tail_def by simp

moreover from A2 have "Tail(a) = {⟨k, a`(succ(k))⟩. k ∈ n}"

using func1_1_L1 pred_succ_eq Tail_def by simp

ultimately show "∀k ∈ n. Tail(a)`(k) = a`(succ(k))"

by (rule ZF_fun_from_tot_val0)

qed

text{*Properties of @{text "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 -> X" and A2: "x∈X" and A3: "b = Append(a,x)"

shows

"b : succ(n) -> X"

"∀k∈n. b`(k) = a`(k)"

"b`(n) = x"

proof -

note A1

moreover have I: "n ∉ n" using mem_not_refl by simp

moreover from A1 A3 have II: "b = a ∪ {⟨n,x⟩}"

using func1_1_L1 Append_def by simp

ultimately have "b : n ∪ {n} -> X ∪ {x}"

by (rule func1_1_L11D)

with A2 show "b : succ(n) -> X"

using succ_explained set_elem_add by simp

from A1 I II show "∀k∈n. b`(k) = a`(k)" and "b`(n) = x"

using func1_1_L11D by auto

qed

text{*A special case of @{text "append_props"}: appending to a nonempty

list does not change the head (first element) of the list.*}

corollary head_of_append:

assumes "n∈ nat" and "a: succ(n) -> X" and "x∈X"

shows "Append(a,x)`(0) = a`(0)"

using assms append_props empty_in_every_succ by auto

(*text{*A bit technical special case of @{text "append_props"} that tells us

what is the value of the appended list at the sucessor of some argument.*}

corollary append_val_succ:

assumes "n ∈ nat" and "a: succ(n) -> X" and "x∈X" and "k ∈ n"

shows "Append(a,x)`(succ(k)) = a`(succ(k))"

using assms succ_ineq append_props by simp*)

text{* @{text "Tail"} commutes with @{text "Append"}.*}

theorem tail_append_commute:

assumes A1: "n ∈ nat" and A2: "a: succ(n) -> X" and A3: "x∈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 -> X" using tail_props

by simp

from A1 A2 A3 have

"succ(n) ∈ nat" and "Append(a,x) : succ(succ(n)) -> X"

using append_props by auto

then have II: "∀k ∈ succ(n). ?c`(k) = Append(a,x)`(succ(k))"

by (rule tail_props)

from assms have

"?b : succ(n) -> X" and "?c : succ(n) -> X"

using tail_props append_props by auto

moreover have "∀k ∈ succ(n). ?b`(k) = ?c`(k)"

proof -

{ fix k assume "k ∈ succ(n)"

hence "k ∈ n ∨ k = n" by auto

moreover

{ assume A4: "k ∈ n"

with assms II have "?c`(k) = a`(succ(k))"

using succ_ineq append_props by simp

moreover

from A3 I have "∀k∈n. ?b`(k) = Tail(a)`(k)"

using append_props by simp

with A1 A2 A4 have "?b`(k) = a`(succ(k))"

using tail_props by simp

ultimately have "?b`(k) = ?c`(k)" by simp }

moreover

{ assume A5: "k = n"

with A2 A3 I II have "?b`(k) = ?c`(k)"

using append_props by auto }

ultimately have "?b`(k) = ?c`(k)" by auto

} thus ?thesis by simp

qed

ultimately show "?b = ?c" by (rule func_eq)

qed

text{*Properties of @{text "Init"}.*}

theorem init_props:

assumes A1: "n ∈ nat" and A2: "a: succ(n) -> X"

shows

"Init(a) : n -> X"

"∀k∈n. Init(a)`(k) = a`(k)"

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

proof -

have "n ⊆ succ(n)" by auto

with A2 have "restrict(a,n): n -> X"

using restrict_type2 by simp

moreover from A1 A2 have I: "restrict(a,n) = Init(a)"

using func1_1_L1 pred_succ_eq Init_def by simp

ultimately show thesis1: "Init(a) : n -> X" by simp

{ fix k assume "k∈n"

then have "restrict(a,n)`(k) = a`(k)"

using restrict by simp

with I have "Init(a)`(k) = a`(k)" by simp

} then show thesis2: "∀k∈n. Init(a)`(k) = a`(k)" by simp

let ?b = "Append(Init(a), a`(n))"

from A2 thesis1 have II:

"Init(a) : n -> X" "a`(n) ∈ X"

"?b = Append(Init(a), a`(n))"

using apply_funtype by auto

note A2

moreover from II have "?b : succ(n) -> X"

by (rule append_props)

moreover have "∀k ∈ succ(n). a`(k) = ?b`(k)"

proof -

{ fix k assume A3: "k ∈ n"

from II have "∀j∈n. ?b`(j) = Init(a)`(j)"

by (rule append_props)

with thesis2 A3 have "a`(k) = ?b`(k)" by simp }

moreover

from II have "?b`(n) = a`(n)"

by (rule append_props)

hence " a`(n) = ?b`(n)" by simp

ultimately show "∀k ∈ succ(n). a`(k) = ?b`(k)"

by simp

qed

ultimately show "a = ?b" by (rule func_eq)

qed

text{*If we take init of the result of append, we get back the same list.*}

lemma init_append: assumes A1: "n ∈ nat" and A2: "a:n->X" and A3: "x ∈ X"

shows "Init(Append(a,x)) = a"

proof -

from A2 A3 have "Append(a,x): succ(n)->X" using append_props by simp

with A1 have "Init(Append(a,x)):n->X" and "∀k∈n. Init(Append(a,x))`(k) = Append(a,x)`(k)"

using init_props by auto

with A2 A3 have "∀k∈n. Init(Append(a,x))`(k) = a`(k)" using append_props by simp

with `Init(Append(a,x)):n->X` A2 show ?thesis by (rule func_eq)

qed

text{*A reformulation of definition of @{text "Init"}.*}

lemma init_def: assumes "n ∈ nat" and "x:succ(n)->X"

shows "Init(x) = restrict(x,n)"

using assms func1_1_L1 Init_def by simp

text{*A lemma about extending a finite sequence by one more value. This is

just a more explicit version of @{text "append_props"}.*}

lemma finseq_extend:

assumes "a:n->X" "y∈X" "b = a ∪ {⟨n,y⟩}"

shows

"b: succ(n) -> X"

"∀k∈n. b`(k) = a`(k)"

"b`(n) = y"

using assms Append_def func1_1_L1 append_props by auto

text{*The next lemma is a bit displaced as it is mainly

about finite sets. It is proven here because it uses

the notion of @{text "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 @{text "bij_extend_point"}

from @{text "func1.thy"}.

*}

lemma bij_append_point:

assumes A1: "n ∈ nat" and A2: "b ∈ bij(n,X)" and A3: "x ∉ X"

shows "Append(b,x) ∈ bij(succ(n), X ∪ {x})"

proof -

from A2 A3 have "b ∪ {⟨n,x⟩} ∈ bij(n ∪ {n},X ∪ {x})"

using mem_not_refl bij_extend_point by simp

moreover have "Append(b,x) = b ∪ {⟨n,x⟩}"

proof -

from A2 have "b:n->X"

using bij_def surj_def by simp

then have "b : n -> X ∪ {x}" using func1_1_L1B

by blast

then show "Append(b,x) = b ∪ {⟨n,x⟩}"

using Append_def func1_1_L1 by simp

qed

ultimately show ?thesis using succ_explained by auto

qed

text{*The next lemma rephrases the definition of @{text "Last"}.

Recall that in ZF we have $\{0,1,2,..,n\} = n+1=$@{text "succ"}$(n)$.*}

lemma last_seq_elem: assumes "a: succ(n) -> X" shows "Last(a) = a`(n)"

using assms func1_1_L1 pred_succ_eq Last_def by simp

text{*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 ∈ nat" and

A2: "a: succ(n) -> X" "b: succ(n) -> X" and

A3: "restrict(a,n) = restrict(b,n)" and

A4: "a`(n) = b`(n)"

shows "a = b"

proof -

{ fix k assume "k ∈ succ(n)"

then have "k ∈ n ∨ k = n" by auto

moreover

{ assume "k ∈ n"

then have

"restrict(a,n)`(k) = a`(k)" and "restrict(b,n)`(k) = b`(k)"

using restrict by auto

with A3 have "a`(k) = b`(k)" by simp }

moreover

{ assume "k = n"

with A4 have "a`(k) = b`(k)" by simp }

ultimately have "a`(k) = b`(k)" by auto

} then have "∀ k ∈ succ(n). a`(k) = b`(k)" by simp

with A2 show "a = b" by (rule func_eq)

qed

text{*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 ∈ nat" and

A2: "a: n -> X" and A3: "b : 1 -> 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 ∈ nat" "1 ∈ nat"

"a:n->X" "b:1->X" by auto

have "?C : succ(n) -> X"

proof -

from I have "?C : n #+ 1 -> X"

by (rule concat_props)

with A1 show "?C : succ(n) -> X" by simp

qed

moreover from A2 A3 have "?A : succ(n) -> X"

using apply_funtype append_props by simp

moreover have "∀k ∈ succ(n). ?C`(k) = ?A`(k)"

proof

fix k assume "k ∈ succ(n)"

moreover

{ assume "k ∈ n"

moreover from I have "∀i ∈ n. ?C`(i) = a`(i)"

by (rule concat_props)

moreover from A2 A3 have "∀i∈n. ?A`(i) = a`(i)"

using apply_funtype append_props by simp

ultimately have "?C`(k) = ?A`(k)" by simp }

moreover have "?C`(n) = ?A`(n)"

proof -

from I have "∀j ∈ 1. ?C`(n #+ j) = b`(j)"

by (rule concat_props)

with A1 A2 A3 show "?C`(n) = ?A`(n)"

using apply_funtype append_props by simp

qed

ultimately show "?C`(k) = ?A`(k)" by auto

qed

ultimately show "?C = ?A" by (rule func_eq)

qed

text{*A simple lemma about lists of length $1$.*}

lemma list_len1_singleton: assumes A1: "x∈X"

shows "{⟨0,x⟩} : 1 -> X"

proof -

from A1 have "{⟨0,x⟩} : {0} -> X" using pair_func_singleton

by simp

moreover have "{0} = 1" by auto

ultimately show ?thesis by simp

qed

text{*A singleton list is in fact a singleton set with a pair as the only element.*}

lemma list_singleton_pair: assumes A1: "x:1->X" shows "x = {⟨0,x`(0)⟩}"

proof -

from A1 have "x = {⟨t,x`(t)⟩. t∈1}" by (rule fun_is_set_of_pairs)

hence "x = {⟨t,x`(t)⟩. t∈{0} }" by simp

thus ?thesis by simp

qed

text{*When we append an element to the empty list we get

a list with length $1$.*}

lemma empty_append1: assumes A1: "x∈X"

shows "Append(0,x): 1 -> X" and "Append(0,x)`(0) = x"

proof -

let ?a = "Append(0,x)"

have "?a = {⟨0,x⟩}" using Append_def by auto

with A1 show "?a : 1 -> X" and "?a`(0) = x"

using list_len1_singleton pair_func_singleton

by auto

qed

(*text{*Tail of a list of length 1 is a list of length 0.*}

lemma list_len1_tail: assumes "a:1->X"

shows "Tail(a) : 0 -> X"

using assms tail_props by blast *)

text{*Appending an element is the same as concatenating

with certain pair.*}

lemma append_concat_pair:

assumes "n ∈ nat" and "a: n -> X" and "x∈X"

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

using assms list_len1_singleton append_1elem pair_val

by simp

text{*An associativity property involving concatenation

and appending. For proof we just convert appending to

concatenation and use @{text "concat_assoc"}.*}

lemma concat_append_assoc: assumes A1: "n ∈ nat" "k ∈ nat" and

A2: "a:n->X" "b:k->X" and A3: "x ∈ X"

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

proof -

from A1 A2 A3 have

"n #+ k ∈ nat" "Concat(a,b) : n #+ k -> X" "x ∈ X"

using concat_props by auto

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 ∈ nat" "k ∈ nat" "1 ∈ nat"

"a:n->X" "b:k->X" "{⟨0,x⟩} : 1 -> X"

using list_len1_singleton by auto

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 by simp

ultimately show "Append(Concat(a,b),x) = Concat(a, Append(b,x))"

by simp

qed

text{*An identity involving concatenating with init

and appending the last element.*}

lemma concat_init_last_elem:

assumes "n ∈ nat" "k ∈ nat" and

"a: n -> X" and "b : succ(k) -> X"

shows "Append(Concat(a,Init(b)),b`(k)) = Concat(a,b)"

using assms init_props apply_funtype concat_append_assoc

by simp

text{*A lemma about creating lists by composition and how

@{text "Append"} behaves in such case.*}

lemma list_compose_append:

assumes A1: "n ∈ nat" and A2: "a : n -> X" and

A3: "x ∈ X" and A4: "c : X -> Y"

shows

"c O Append(a,x) : succ(n) -> Y"

"c O Append(a,x) = Append(c O a, c`(x))"

proof -

let ?b = "Append(a,x)"

let ?d = "Append(c O a, c`(x))"

from A2 A4 have "c O a : n -> Y"

using comp_fun by simp

from A2 A3 have "?b : succ(n) -> X"

using append_props by simp

with A4 show "c O ?b : succ(n) -> Y"

using comp_fun by simp

moreover from A3 A4 `c O a : n -> Y` have

"?d: succ(n) -> Y"

using apply_funtype append_props by simp

moreover have "∀k ∈ succ(n). (c O ?b) `(k) = ?d`(k)"

proof -

{ fix k assume "k ∈ succ(n)"

with `?b : succ(n) -> X` have

"(c O ?b) `(k) = c`(?b`(k))"

using comp_fun_apply by simp

with A2 A3 A4 `c O a : n -> Y` `c O a : n -> Y` `k ∈ succ(n)`

have "(c O ?b) `(k) = ?d`(k)"

using append_props comp_fun_apply apply_funtype

by auto

} thus ?thesis by simp

qed

ultimately show "c O ?b = ?d" by (rule func_eq)

qed

text{*A lemma about appending an element to a list defined by set

comprehension.*}

lemma set_list_append: assumes

A1: "∀i ∈ succ(k). b(i) ∈ X" and

A2: "a = {⟨i,b(i)⟩. i ∈ succ(k)}"

shows

"a: succ(k) -> X"

"{⟨i,b(i)⟩. i ∈ k}: k -> X"

"a = Append({⟨i,b(i)⟩. i ∈ k},b(k))"

proof -

from A1 have "{⟨i,b(i)⟩. i ∈ succ(k)} : succ(k) -> X"

by (rule ZF_fun_from_total)

with A2 show "a: succ(k) -> X" by simp

from A1 have "∀i ∈ k. b(i) ∈ X"

by simp

then show "{⟨i,b(i)⟩. i ∈ k}: k -> X"

by (rule ZF_fun_from_total)

with A2 show "a = Append({⟨i,b(i)⟩. i ∈ k},b(k))"

using func1_1_L1 Append_def by auto

qed

text{* An induction theorem for lists.*}

lemma list_induct: assumes A1: "∀b∈1->X. P(b)" and

A2: "∀b∈NELists(X). P(b) --> (∀x∈X. P(Append(b,x)))" and

A3: "d ∈ NELists(X)"

shows "P(d)"

proof -

{ fix n

assume "n∈nat"

moreover from A1 have "∀b∈succ(0)->X. P(b)" by simp

moreover have "∀k∈nat. ((∀b∈succ(k)->X. P(b)) --> (∀c∈succ(succ(k))->X. P(c)))"

proof -

{ fix k assume "k ∈ nat" assume "∀b∈succ(k)->X. P(b)"

have "∀c∈succ(succ(k))->X. P(c)"

proof

fix c assume "c: succ(succ(k))->X"

let ?b = "Init(c)"

let ?x = "c`(succ(k))"

from `k ∈ nat` `c: succ(succ(k))->X` have "?b:succ(k)->X"

using init_props by simp

with A2 `k ∈ nat` `∀b∈succ(k)->X. P(b)` have "∀x∈X. P(Append(?b,x))"

using NELists_def by auto

with `c: succ(succ(k))->X` have "P(Append(?b,?x))" using apply_funtype by simp

with `k ∈ nat` `c: succ(succ(k))->X` show "P(c)"

using init_props by simp

qed

} thus ?thesis by simp

qed

ultimately have "∀b∈succ(n)->X. P(b)" by (rule ind_on_nat)

} with A3 show ?thesis using NELists_def by auto

qed

section{*Lists and cartesian products*}

text{*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.*}

text{*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 ∈ nat"

shows "{⟨x,⟨Init(x),x`(n)⟩⟩. x ∈ succ(n)->X} ∈ bij(succ(n)->X,(n->X)×X)"

proof -

let ?f = "{⟨x,⟨Init(x),x`(n)⟩⟩. x ∈ succ(n)->X}"

from assms have "∀x ∈ succ(n)->X. ⟨Init(x),x`(n)⟩ ∈ (n->X)×X"

using init_props succ_iff apply_funtype by simp

then have I: "?f: (succ(n)->X)->((n->X)×X)" by (rule ZF_fun_from_total)

moreover from assms I have "∀x∈succ(n)->X.∀y∈succ(n)->X. ?f`(x)=?f`(y) --> x=y"

using ZF_fun_from_tot_val init_def finseq_restr_eq by auto

moreover have "∀p∈(n->X)×X.∃x∈succ(n)->X. ?f`(x) = p"

proof

fix p assume "p ∈ (n->X)×X"

let ?x = "Append(fst(p),snd(p))"

from assms `p ∈ (n->X)×X` have "?x:succ(n)->X" using append_props by simp

with I have "?f`(?x) = ⟨Init(?x),?x`(n)⟩" using succ_iff ZF_fun_from_tot_val by simp

moreover from assms `p ∈ (n->X)×X` have "Init(?x) = fst(p)" and "?x`(n) = snd(p)"

using init_append append_props by auto

ultimately have "?f`(?x) = ⟨fst(p),snd(p)⟩" by auto

with `p ∈ (n->X)×X` `?x:succ(n)->X` show "∃x∈succ(n)->X. ?f`(x) = p" by auto

qed

ultimately show ?thesis using inj_def surj_def bij_def by auto

qed

text{*We can identify a set $X$ with lists of length one of elements of $X$.*}

lemma singleton_list_bij: shows "{⟨x,x`(0)⟩. x∈1->X} ∈ bij(1->X,X)"

proof -

let ?f = "{⟨x,x`(0)⟩. x∈1->X}"

have "∀x∈1->X. x`(0) ∈ X" using apply_funtype by simp

then have I: "?f:(1->X)->X" by (rule ZF_fun_from_total)

moreover have "∀x∈1->X.∀y∈1->X. ?f`(x) = ?f`(y) --> x=y"

proof -

{ fix x y

assume "x:1->X" "y:1->X" and "?f`(x) = ?f`(y)"

with I have "x`(0) = y`(0)" using ZF_fun_from_tot_val by auto

moreover from `x:1->X` `y:1->X` have "x = {⟨0,x`(0)⟩}" and "y = {⟨0,y`(0)⟩}"

using list_singleton_pair by auto

ultimately have "x=y" by simp

} thus ?thesis by auto

qed

moreover have "∀y∈X. ∃x∈1->X. ?f`(x)=y"

proof

fix y assume "y∈X"

let ?x = "{⟨0,y⟩}"

from I `y∈X` have "?x:1->X" and "?f`(?x) = y"

using list_len1_singleton ZF_fun_from_tot_val pair_val by auto

thus "∃x∈1->X. ?f`(x)=y" by auto

qed

ultimately show ?thesis using inj_def surj_def bij_def by simp

qed

text{*We can identify a set of $X$-valued lists of length with $X$.*}

lemma list_singleton_bij: shows

"{⟨x,{⟨0,x⟩}⟩.x∈X} ∈ bij(X,1->X)" and

"{⟨y,y`(0)⟩. y∈1->X} = converse({⟨x,{⟨0,x⟩}⟩.x∈X})" and

"{⟨x,{⟨0,x⟩}⟩.x∈X} = converse({⟨y,y`(0)⟩. y∈1->X})"

proof -

let ?f = "{⟨y,y`(0)⟩. y∈1->X}"

let ?g = "{⟨x,{⟨0,x⟩}⟩.x∈X}"

have "1 = {0}" by auto

then have "?f ∈ bij(1->X,X)" and "?g:X->(1->X)"

using singleton_list_bij pair_func_singleton ZF_fun_from_total

by auto

moreover have "∀y∈1->X.?g`(?f`(y)) = y"

proof

fix y assume "y:1->X"

have "?f:(1->X)->X" using singleton_list_bij bij_def inj_def by simp

with `1 = {0}` `y:1->X` `?g:X->(1->X)` show "?g`(?f`(y)) = y"

using ZF_fun_from_tot_val apply_funtype func_singleton_pair

by simp

qed

ultimately show "?g ∈ bij(X,1->X)" and "?f = converse(?g)" and "?g = converse(?f)"

using comp_conv_id by auto

qed

text{*What is the inverse image of a set by the natural bijection between $X$-valued

singleton lists and $X$? *}

lemma singleton_vimage: assumes "U⊆X" shows "{x∈1->X. x`(0) ∈ U} = { {⟨0,y⟩}. y∈U}"

proof

have "1 = {0}" by auto

{ fix x assume "x ∈ {x∈1->X. x`(0) ∈ U}"

with `1 = {0}` have "x = {⟨0, x`(0)⟩}" using func_singleton_pair by auto

} thus "{x∈1->X. x`(0) ∈ U} ⊆ { {⟨0,y⟩}. y∈U}" by auto

{ fix x assume "x ∈ { {⟨0,y⟩}. y∈U}"

then obtain y where "x = {⟨0,y⟩}" and "y∈U" by auto

with `1 = {0}` assms have "x:1->X" using pair_func_singleton by auto

} thus "{ {⟨0,y⟩}. y∈U} ⊆ {x∈1->X. x`(0) ∈ U}" by auto

qed

text{*A technical lemma about extending a list by values from a set.*}

lemma list_append_from: assumes A1: "n ∈ nat" and A2: "U ⊆ n->X" and A3: "V ⊆ X"

shows

"{x ∈ succ(n)->X. Init(x) ∈ U ∧ x`(n) ∈ V} = (\<Union>y∈V.{Append(x,y).x∈U})"

proof -

{ fix x assume "x ∈ {x ∈ succ(n)->X. Init(x) ∈ U ∧ x`(n) ∈ V}"

then have "x ∈ succ(n)->X" and "Init(x) ∈ U" and I: "x`(n) ∈ V"

by auto

let ?y = "x`(n)"

from A1 and `x ∈ succ(n)->X` have "x = Append(Init(x),?y)"

using init_props by simp

with I and `Init(x) ∈ U` have "x ∈ (\<Union>y∈V.{Append(a,y).a∈U})" by auto

}

moreover

{ fix x assume "x ∈ (\<Union>y∈V.{Append(a,y).a∈U})"

then obtain a y where "y∈V" and "a∈U" and "x = Append(a,y)" by auto

with A2 A3 have "x: succ(n)->X" using append_props by blast

from A2 A3 `y∈V` `a∈U` have "a:n->X" and "y∈X" by auto

with A1 `a∈U` `y∈V` `x = Append(a,y)` have "Init(x) ∈ U" and "x`(n) ∈ V"

using append_props init_append by auto

with `x: succ(n)->X` have "x ∈ {x ∈ succ(n)->X. Init(x) ∈ U ∧ x`(n) ∈ V}"

by auto

}

ultimately show ?thesis by blast

qed

end