Theory FiniteSeq_ZF
section ‹Finite sequences›
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.›
subsection‹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 ‹Lists(X)›.›
definition
"Lists(X) ≡ ⋃n∈nat.(n→X)"
text‹The set of nonempty $X$-value listst will be called ‹NELists(X)›.›
definition
"NELists(X) ≡ ⋃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
‹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 ‹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 ‹Tail› here as well.›
definition
"Tail(a) ≡ {⟨k, a`(succ(k))⟩. k ∈ pred(domain(a))}"
text‹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) ≡ 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 ‹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 ‹Last›
element of a list.›
definition
"Last(a) ≡ a`(pred(domain(a)))"
text‹A formula for tail of a finite list.›
lemma tail_as_set: assumes "n ∈ nat" and "a: n #+ 1 → X"
shows "Tail(a) = {⟨k,a`(k #+ 1)⟩. k∈n}"
using assms func1_1_L1 elem_nat_is_nat(2) succ_add_one(1)
unfolding Tail_def by simp
text‹Formula for the tail of a list defined by an expression:›
lemma tail_formula: assumes "n ∈ nat" and "∀k ∈ n #+ 1. q(k) ∈ X"
shows "Tail({⟨k,q(k)⟩. k ∈ n #+ 1}) = {⟨k,q(k #+ 1)⟩. k ∈ n}"
proof -
let ?a = "{⟨k,q(k)⟩. k ∈ n #+ 1}"
from assms(2) have "?a : n #+ 1 → X"
by (rule ZF_fun_from_total)
with assms(1) have "Tail(?a) = {⟨k,?a`(k #+ 1)⟩. k∈n}"
using tail_as_set by simp
moreover have "∀k∈n. ?a`(k #+ 1) = q(k #+ 1)"
proof -
{ fix k assume "k∈n"
with assms(1) have "k #+ 1 ∈ n #+ 1"
using succ_ineq1 elem_nat_is_nat(2) succ_add_one(1)
by simp
then have "?a`(k #+ 1) = q(k #+ 1)"
by (rule ZF_fun_from_tot_val1)
} thus ?thesis by simp
qed
ultimately show ?thesis by simp
qed
text‹Codomain of a nonempty list is nonempty.›
lemma nelist_vals_nonempty: assumes "a:succ(n)→Y"
shows "Y≠0" using assms codomain_nonempty by simp
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 ‹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‹Essentially the second assertion of ‹tail_props› but formulated using notation
$n+1$ instead of ‹succ(n)›:›
lemma tail_props2: assumes "n ∈ nat" "a: n #+ 1 → X" "k∈n"
shows "Tail(a)`(k) = a`(k #+ 1)"
using assms succ_add_one(1) tail_props(2) elem_nat_is_nat(2)
by simp
text‹A nonempty list can be decomposed into concatenation of its first element and
the tail.›
lemma first_concat_tail: assumes "n∈nat" "a:succ(n)→X"
shows "a = Concat({⟨0,a`(0)⟩},Tail(a))"
proof -
let ?b = "Concat({⟨0,a`(0)⟩},Tail(a))"
have "?b:succ(n)→X" and "∀k∈succ(n). a`(k) = ?b`(k)"
proof -
from assms(1) have "0∈succ(n)" using empty_in_every_succ by simp
with assms(2) have "a`(0) ∈ X" using apply_funtype by simp
then have I: "{⟨0,a`(0)⟩}:{0}→X" using pair_func_singleton by simp
have "{0}∈nat" using one_is_nat by simp
from assms have "Tail(a): n → X" using tail_props(1) by simp
with assms(1) ‹{0}∈nat› I have "?b:{0} #+ n → X"
using concat_props(1) by simp
with assms(1) show "?b:succ(n) → X" using succ_add_one(3) by simp
{ fix k assume "k∈succ(n)"
{ assume "k=0"
with assms(1) ‹{0}∈nat› I ‹Tail(a): n → X›
have "a`(k) = ?b`(k)" using concat_props(2) pair_val
by simp
}
moreover
{ assume "k≠0"
from assms(1) ‹k∈succ(n)› have "k∈nat"
using elem_nat_is_nat(2) by blast
with ‹k≠0› obtain m where "m∈nat" and "k=succ(m)"
using Nat_ZF_1_L3 by blast
with assms(1) ‹k∈succ(n)› have "m∈n" using succ_mem
by simp
with ‹{0}∈nat› assms(1) I ‹Tail(a): n → X›
have "?b`({0} #+ m) = Tail(a)`(m)"
using concat_props(4) by simp
with assms ‹m∈nat› ‹k∈succ(n)› ‹k=succ(m)› ‹m∈n›
have "a`(k) = ?b`(k)"
using succ_add_one(3) tail_props(2) by simp
}
ultimately have "a`(k) = ?b`(k)" by blast
} thus "∀k∈succ(n). a`(k) = ?b`(k)" by simp
qed
with assms(2) show ?thesis by (rule func_eq)
qed
text‹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 → 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 ‹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‹‹Tail› commutes with ‹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‹@{term NELists} are non-empty lists›
lemma non_zero_List_func_is_NEList:
shows "NELists(X) = {a∈Lists(X). a≠0}"
proof-
{ fix a assume as: "a∈{a∈Lists(X). a≠0}"
from as obtain n where a: "n∈nat" "a:n→ X" unfolding Lists_def
by auto
{ assume "n=0"
with a(2) have "a=0" unfolding Pi_def by auto
with as have False by auto
}
hence "n≠0" by auto
with a(1) obtain k where "k∈nat" "n=succ(k)" using Nat_ZF_1_L3
by auto
with a(2) have "a ∈ NELists(X)" unfolding NELists_def by auto
} moreover
{ fix a assume as: "a∈NELists(X)"
then obtain k where k: "a:succ(k)→X" "k∈nat"
unfolding NELists_def by auto
{ assume "a=0"
hence "domain(a) = 0" by auto
with k(1) have "succ(k) = 0" using domain_of_fun by auto
hence False by auto
} moreover
{ from k(2) have "succ(k)∈nat" using nat_succI by auto
with k(1) have "a∈Lists(X)" unfolding Lists_def by auto
} ultimately
have "a∈{a∈Lists(X). a≠0}" by auto
}
ultimately show ?thesis by auto
qed
text‹Properties of ‹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‹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 ∈ NELists(X)"
shows "Init(a) ∈ Lists(X)" and "succ(domain(Init(a))) = domain(a)"
proof -
from assms obtain n where n: "n∈nat" "a:succ(n) → X"
unfolding NELists_def by auto
then have tailF: "Init(a):n → X" using init_props(1) by auto
with n(1) show "Init(a) ∈ Lists(X)" unfolding Lists_def by auto
from tailF have "domain(Init(a)) = n" using domain_of_fun by auto
moreover from n(2) have "domain(a) = succ(n)" using domain_of_fun
by auto
ultimately show "succ(domain(Init(a))) = domain(a)" by auto
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 ‹Init›.›
lemma init_def: assumes "n ∈ nat" and "a:succ(n)→X"
shows "Init(a) = restrict(a,n)"
using assms func1_1_L1 Init_def by simp
text‹Another reformulation of the definition of ‹Init›, starting with the
expression defining the list.›
lemma init_def_alt: assumes "n∈nat" and "∀k∈n #+ 1. q(k) ∈ X"
shows "Init({⟨k,q(k)⟩. k∈n #+ 1}) = {⟨k,q(k)⟩. k∈n}"
proof -
let ?a = "{⟨k,q(k)⟩. k∈n #+ 1}"
from assms(2) have "?a:n #+ 1→X" by (rule ZF_fun_from_total)
moreover from assms(1) have "n #+ 1 = succ(n)" using succ_add_one(1)
by simp
ultimately have "?a:succ(n)→X" by simp
with assms(1) have "Init(?a) = restrict(?a,n)" using init_def by simp
moreover
from assms(1) have "n ⊆ n #+ 1" by auto
then have "restrict(?a,n) = {⟨k,q(k)⟩. k∈n}"
by (rule restrict_def_alt)
ultimately show ?thesis by simp
qed
text‹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→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 ‹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 ∈ 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 ‹Last›.
Recall that in ZF we have $\{0,1,2,..,n\} = n+1=$‹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‹The last element of a non-empty list valued in $X$ is in $X$.›
lemma last_type: assumes "a ∈ NELists(X)" shows "Last(a) ∈ X"
using assms last_seq_elem apply_funtype unfolding NELists_def
by auto
text‹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∈nat" "a: succ(succ(n)) → X"
shows "Last(Tail(a)) = Last(a)"
proof -
from assms have "Last(Tail(a)) = Tail(a)`(n)"
using tail_props(1) last_seq_elem by blast
also from assms have "Tail(a)`(n) = a`(succ(n))" using tail_props(2)
by blast
also from assms(2) have "a`(succ(n)) = Last(a)" using last_seq_elem
by simp
finally show ?thesis by simp
qed
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‹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∈X"
shows "{⟨0,x⟩} : 1 → X" and "{⟨0,x⟩} ∈ NELists(X)"
proof -
from assms have "{⟨0,x⟩} : {0} → X" using pair_func_singleton
by simp
moreover have "{0} = 1" by auto
ultimately show "{⟨0,x⟩} : 1 → X" and "{⟨0,x⟩} ∈ NELists(X)"
unfolding NELists_def by auto
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‹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 ‹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
‹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‹A version of ‹set_list_append› using $n+1$ instead of ‹succ(n)›. ›
lemma set_list_append1:
assumes "n∈nat" and "∀k∈n #+ 1. q(k) ∈ X"
defines "a≡{⟨k,q(k)⟩. k∈n #+ 1}"
shows
"a: n #+ 1 → X"
"{⟨k,q(k)⟩. k ∈ n}: n → X"
"Init(a) = {⟨k,q(k)⟩. k ∈ n}"
"a = Append({⟨k,q(k)⟩. k ∈ n},q(n))"
"a = Append(Init(a), q(n))"
"a = Append(Init(a), a`(n))"
proof -
from assms(1) have I: "n #+ 1 = succ(n)" using succ_add_one(1)
by simp
with assms show
"a: n #+ 1 → X" and "{⟨k,q(k)⟩. k ∈ n}: n → X"
and II: "Init(a) = {⟨k,q(k)⟩. k ∈ n}"
using set_list_append(1,2) init_def_alt by simp_all
from assms(2,3) I have
"∀k∈succ(n). q(k) ∈ X" and "a = {⟨k,q(k)⟩. k ∈ succ(n)}"
by simp_all
then show "a = Append({⟨k,q(k)⟩. k ∈ n},q(n))"
using set_list_append(3) by simp
with II show "a = Append(Init(a), q(n))" by simp
from I have "n ∈ n #+ 1" by simp
then have "{⟨k,q(k)⟩. k∈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))"
by simp
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
text‹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) ≡ {⟨k,if k = 0 then x else a`(k #- 1)⟩. k∈domain(a) #+ 1}"
text‹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∈nat" "a:n→X" "x∈X"
shows "Prepend(a,x):(n #+ 1)→X" and "Prepend(a,x)`(0) = x"
proof -
let ?b = "{⟨k,if k = 0 then x else a`(k #- 1)⟩. k∈n #+ 1}"
have "∀k∈n #+ 1. (if k = 0 then x else a`(k #- 1)) ∈ X"
proof -
{ fix k assume "k ∈ n #+ 1"
let ?v = "if k = 0 then x else a`(k #- 1)"
{ assume "k≠0"
with ‹k ∈ n #+ 1› have "n≠0" by auto
from assms(1) ‹k ∈ n #+ 1› have "k ∈ nat"
using elem_nat_is_nat(2) by blast
from assms(1) have "succ(n) = n #+ 1"
using succ_add_one(1) by simp
with ‹k ∈ n #+ 1› have "k∈succ(n)" by simp
with assms(1) ‹n≠0› have "pred(k) ∈ n"
using pred_succ_mem by simp
with assms(2) ‹k ∈ nat› ‹k≠0› have "?v∈X"
using pred_minus_one apply_funtype by simp
}
with assms(3) have "?v ∈ X" by simp
} thus ?thesis by simp
qed
then have "?b: (n #+ 1)→X" by (rule ZF_fun_from_total)
with assms(2) show "Prepend(a,x):(n #+ 1)→X"
using func1_1_L1 unfolding Prepend_def by simp
from assms(1) have "0 ∈ n #+ 1"
using succ_add_one(1) empty_in_every_succ by simp
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 by simp
qed
text‹When prepending an element to a list the values at positive indices do not change.›
lemma prepend_val: assumes "n∈nat" "a:n→X" "x∈X" "k∈n"
shows "Prepend(a,x)`(k #+ 1) = a`(k)"
proof -
let ?b = "{⟨k,if k = 0 then x else a`(k #- 1)⟩. k∈n #+ 1}"
from assms(1,4) have "k∈nat"
using elem_nat_is_nat(2) by simp
with assms(1) have "succ(n) = n #+ 1" and "succ(k) = k #+ 1"
using succ_add_one(1) by auto
with assms(1,4) have "k #+ 1 ∈ n #+ 1"
using succ_ineq by simp
from ‹k #+ 1 ∈ 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∈nat› show ?thesis
using func1_1_L1 unfolding Prepend_def by simp
qed
subsection‹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} = (⋃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 ∈ (⋃y∈V.{Append(a,y).a∈U})" by auto
}
moreover
{ fix x assume "x ∈ (⋃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