# Theory CZH_Sets_FSequences

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Finite sequences›
theory CZH_Sets_FSequences
imports CZH_Sets_Cardinality
begin

subsection‹Background›

text‹
The section presents a theory of finite sequences internalized in the
type \<^typ>‹V›. The content of this subsection
was inspired by and draws on many ideas from the content
of the theory ‹List› in the main library of Isabelle/HOL.
›

subsection‹Definition and common properties›

text‹
A finite sequence is defined as a single-valued binary relation whose domain
is an initial segment of the set of natural numbers.
›

locale vfsequence = vsv xs for xs +
assumes vfsequence_vdomain_in_omega: "𝒟⇩∘ xs ∈⇩∘ ω"

locale vfsequence_pair = r⇩1: vfsequence xs⇩1 + r⇩2: vfsequence xs⇩2 for xs⇩1 xs⇩2

text‹Rules.›

lemmas [intro] = vfsequence.axioms(1)

lemma vfsequenceI[intro]:
assumes "vsv xs" and "𝒟⇩∘ xs ∈⇩∘ ω"
shows "vfsequence xs"
using assms by (simp add: vfsequence.intro vfsequence_axioms_def)

lemma vfsequenceD[dest]:
assumes "vfsequence xs"
shows "𝒟⇩∘ xs ∈⇩∘ ω"
using assms vfsequence.vfsequence_vdomain_in_omega by simp

lemma vfsequenceE[elim]:
assumes "vfsequence xs" and "𝒟⇩∘ xs ∈⇩∘ ω ⟹ P"
shows P
using assms by auto

lemma vfsequence_iff: "vfsequence xs ⟷ vsv xs ∧ 𝒟⇩∘ xs ∈⇩∘ ω"
using vfsequence_def by auto

text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vdomain: "𝒟⇩∘ xs = vcard xs"
unfolding vsv_vcard_vdomain[symmetric] using vfsequence_vdomain_in_omega by simp

lemma (in vfsequence) vfsequence_vcard_in_omega[simp]: "vcard xs ∈⇩∘ ω"
using vfsequence_vdomain_in_omega by (simp add: vfsequence_vdomain)

text‹Set operations.›

lemma vfsequence_vempty[intro, simp]: "vfsequence 0" by (simp add: vfsequenceI)

lemma vfsequence_vsingleton[intro, simp]: "vfsequence (set {⟨0, a⟩})"
using vone_in_omega
unfolding one_V_def
by (intro vfsequenceI) (auto simp: set_vzero_eq_ord_of_nat_vone)

lemma (in vfsequence) vfsequence_vinsert:
"vfsequence (vinsert ⟨vcard xs, a⟩ xs)"
using succ_def succ_in_omega by (auto simp: vfsequence_vdomain)

text‹Connections.›

lemma (in vfsequence) vfsequence_vfinite[simp]: "vfinite xs"

lemma (in vfsequence) vfsequence_vlrestriction[intro, simp]:
assumes "k ∈⇩∘ ω"
shows "vfsequence (xs ↾⇧l⇩∘ k)"
using assms by (force simp: vfsequence_vdomain vdomain_vlrestriction)

lemma vfsequence_vproduct:
assumes "n ∈⇩∘ ω" and "xs ∈⇩∘ (∏⇩∘i∈⇩∘n. A i)"
shows "vfsequence xs"
using assms by auto

lemma vfsequence_vcpower:
assumes "n ∈⇩∘ ω" and "xs ∈⇩∘ A ^⇩× n"
shows "vfsequence xs"
using assms vfsequence_vproduct by auto

lemma vfsequence_vcomp_vsv_vfsequence:
assumes "vsv f" and "vfsequence xs" and "ℛ⇩∘ xs ⊆⇩∘ 𝒟⇩∘ f"
shows "vfsequence (f ∘⇩∘ xs)"
proof(intro vfsequenceI vsv_vcomp)
interpret xs: vfsequence xs by (rule assms(2))
show "𝒟⇩∘ (f ∘⇩∘ xs) ∈⇩∘ ω"
unfolding vdomain_vcomp_vsubset[OF assms(3)]
by (force simp: xs.vfsequence_vdomain_in_omega)
qed (auto intro: assms)

text‹Special properties.›

lemma (in vfsequence) vfsequence_vdomain_vlrestriction[intro, simp]:
assumes "k ∈⇩∘ vcard xs"
shows "𝒟⇩∘ (xs ↾⇧l⇩∘ k) = k"
using assms
by
(
OrdmemD
inf_absorb2
order.strict_implies_order
vdomain_vlrestriction
vfsequence_vdomain
)

lemma (in vfsequence) vfsequence_vlrestriction_vcard[simp]:
"xs ↾⇧l⇩∘ (vcard xs) = xs"
by (rule vlrestriction_vdomain[unfolded vfsequence_vdomain])

lemma vfsequence_vfinite_vcardI:
assumes "vsv xs" and "vfinite xs" and "𝒟⇩∘ xs = vcard xs"
shows "vfsequence xs"
using assms by (intro vfsequenceI) (auto simp: vfinite_vcard_omega)

lemma (in vfsequence) vfsequence_vrangeE:
assumes "a ∈⇩∘ ℛ⇩∘ xs"
obtains n where "n ∈⇩∘ vcard xs" and "xs⦇n⦈ = a"
using assms vfsequence_vdomain by auto

lemma (in vfsequence) vfsequence_vrange_vproduct:
assumes "⋀i. i ∈⇩∘ vcard xs ⟹ xs⦇i⦈ ∈⇩∘ A i"
shows "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A i)"
using vfsequence_vdomain vsv_axioms assms
by
(
intro vproductI;
(intro vsv.vsv_vrange_vsubset_vifunion_app | tactic‹all_tac›)
) auto

lemma (in vfsequence) vfsequence_vrange_vcpower:
assumes "ℛ⇩∘ xs ⊆⇩∘ A"
shows "xs ∈⇩∘ A ^⇩× (vcard xs)"
using assms
proof(elim vsubsetE; intro vcpowerI)
assume hyp: "x ∈⇩∘ ℛ⇩∘ xs ⟹ x ∈⇩∘ A" for x
from vfsequence_vdomain show "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A)"
by (intro vproductI) (blast intro: hyp elim: vdomain_atE)+
qed

text‹Alternative forms of existing results.›

lemmas [intro, simp] = vfsequence.vfsequence_vcard_in_omega
and [intro, simp] = vfsequence.vfsequence_vfinite
and [intro, simp] = vfsequence.vfsequence_vlrestriction
and [intro, simp] = vfsequence.vfsequence_vdomain_vlrestriction
and [intro, simp] = vfsequence.vfsequence_vlrestriction_vcard

subsection‹Appending an element to a finite sequence: ‹vcons››

subsubsection‹Definition and common properties›

definition vcons :: "V ⇒ V ⇒ V"  (infixr ‹#⇩∘› 65)
where "xs #⇩∘ x = vinsert ⟨vcard xs, x⟩ xs"

text‹Syntax.›

abbreviation vempty_vfsequence (‹[]⇩∘›) where
"vempty_vfsequence ≡ 0::V"

notation vempty_vfsequence (‹[]⇩∘›)

nonterminal fsfields
nonterminal vlist

syntax
"" :: "V ⇒ fsfields" ("_")
"_fsfields" :: "fsfields ⇒ V ⇒ fsfields" ("_,/ _")
"_vlist" :: "fsfields ⇒ V" ("[(_)]⇩∘")
"_vapp" :: "V ⇒ fsfields ⇒ V" ("_ ⦇(_)⦈⇩∙" [100, 100] 100)

translations
"[xs, x]⇩∘" == "[xs]⇩∘ #⇩∘ x"
"[x]⇩∘" == "[]⇩∘ #⇩∘ x"

translations
"f⦇xs, x⦈⇩∙" == "f⦇[xs, x]⇩∘⦈"
"f⦇x⦈⇩∙" == "f⦇[x]⇩∘⦈"

text‹Rules.›

lemma vconsI[intro!]:
assumes "a ∈⇩∘ vinsert ⟨vcard xs, x⟩ xs"
shows "a ∈⇩∘ xs #⇩∘ x"
using assms unfolding vcons_def by clarsimp

lemma vconsD[dest!]:
assumes "a ∈⇩∘ xs #⇩∘ x"
shows "a ∈⇩∘ vinsert ⟨vcard xs, x⟩ xs"
using assms unfolding vcons_def by clarsimp

lemma vconsE[elim!]:
assumes "a ∈⇩∘ xs #⇩∘ x"
obtains a where "a ∈⇩∘ vinsert ⟨vcard xs, x⟩ xs"
using assms unfolding vcons_def by clarsimp

text‹Elementary properties.›

lemma vcons_neq_vempty[simp]: "ys #⇩∘ y ≠ []⇩∘" by auto

text‹Set operations.›

lemma vcons_vsingleton: "[a]⇩∘ = set {⟨0⇩ℕ, a⟩}" unfolding vcons_def by simp

lemma vcons_vdoubleton: "[a, b]⇩∘ = set {⟨0⇩ℕ, a⟩, ⟨1⇩ℕ, b⟩}"
unfolding vcons_def
using vinsert_vsingleton
by (force simp: vinsert_set_insert_eq)

lemma vcons_vsubset: "xs ⊆⇩∘ xs #⇩∘ x" by clarsimp

lemma vcons_vsubset':
assumes "vcons xs x ⊆⇩∘ ys"
shows "vcons xs x ⊆⇩∘ vcons ys y"
using assms unfolding vcons_def by auto

text‹Connections.›

lemma (in vfsequence) vfsequence_vcons[intro, simp]: "vfsequence (xs #⇩∘ x)"
proof(intro vfsequenceI)
from vfsequence_vdomain_in_omega vsv_vcard_vdomain have "vcard xs = 𝒟⇩∘ xs"
show "vsv (xs #⇩∘ x)"
proof(intro vsvI)
fix a b c assume ab: "⟨a, b⟩ ∈⇩∘ xs #⇩∘ x" and ac: "⟨a, c⟩ ∈⇩∘ xs #⇩∘ x"
then consider (dom) "a ∈⇩∘ 𝒟⇩∘ xs" | (ndom) "a = vcard xs"
unfolding vcons_def by auto
then show "b = c"
proof cases
case dom
with ab have "⟨a, b⟩ ∈⇩∘ xs"
unfolding vcons_def by (auto simp: ‹vcard xs = 𝒟⇩∘ xs›)
moreover from dom ac have "⟨a, c⟩ ∈⇩∘ xs"
unfolding vcons_def by (auto simp: ‹vcard xs = 𝒟⇩∘ xs›)
ultimately show ?thesis using vsv by simp
next
case ndom
from ab have "⟨a, b⟩ = ⟨vcard xs, x⟩"
unfolding ndom vcons_def using ‹vcard xs = 𝒟⇩∘ xs› mem_not_refl by blast
moreover from ac have "⟨a, c⟩ = ⟨vcard xs, x⟩"
unfolding ndom vcons_def using ‹vcard xs = 𝒟⇩∘ xs› mem_not_refl by blast
ultimately show ?thesis by simp
qed
next
show "vbrelation (xs #⇩∘ x)" unfolding vcons_def
using vbrelation_vinsertI by auto
qed
show "𝒟⇩∘ (xs #⇩∘ x) ∈⇩∘ ω"
unfolding vcons_def
using succ_in_omega
by (auto simp: vfsequence_vdomain_in_omega succ_def ‹vcard xs = 𝒟⇩∘ xs›)
qed

lemma (in vfsequence) vfsequence_vcons_vdomain[simp]:
"𝒟⇩∘ (xs #⇩∘ x) = succ (vcard xs)"
by (simp add: succ_def vcons_def vfsequence_vdomain)

lemma (in vfsequence) vfsequence_vcons_vrange[simp]:
"ℛ⇩∘ (xs #⇩∘ x) = vinsert x (ℛ⇩∘ xs)"

lemma (in vfsequence) vfsequence_vrange_vconsI:
assumes "ℛ⇩∘ xs ⊆⇩∘ X" and "x ∈⇩∘ X"
shows "ℛ⇩∘ (xs #⇩∘ x) ⊆⇩∘ X"
using assms unfolding vcons_def by auto

lemmas vfsequence_vrange_vconsI = vfsequence.vfsequence_vrange_vconsI[rotated 1]

text‹Special properties.›

lemma vcons_vrange_mono:
assumes "xs ⊆⇩∘ ys"
shows "ℛ⇩∘ (xs #⇩∘ x) ⊆⇩∘ ℛ⇩∘ (ys #⇩∘ x)"
using assms
unfolding vcons_def
by (simp add: vrange_mono vsubset_vinsert_leftI vsubset_vinsert_rightI)

lemma (in vfsequence) vfsequence_vlrestriction_succ:
assumes [simp]: "k ∈⇩∘ vcard xs"
shows "xs ↾⇧l⇩∘ succ k = xs ↾⇧l⇩∘ k #⇩∘ (xs⦇k⦈)"
proof-
interpret vlr: vfsequence ‹xs ↾⇧l⇩∘ k›
using assms by (blast intro: vfsequence_vcard_in_omega Ord_trans)
from vlr.vfsequence_vdomain[symmetric, simplified] show ?thesis
by
(
vcons_def succ_def vfsequence_vdomain vsv_vlrestriction_vinsert
)
qed

lemma (in vfsequence) vfsequence_vremove_vcons_vfsequence:
assumes "xs = xs' #⇩∘ x"
shows "vfsequence xs'"
proof(cases‹⟨vcard xs', x⟩ ∈⇩∘ xs'›)
case True
with assms[unfolded vcons_def] have "xs = xs'" by auto
then show ?thesis using vfsequence_axioms by simp
next
case False
note x_def[simp] = assms[unfolded vcons_def]
interpret xs': vsv xs' using vsv_axioms by (auto intro: vsv_vinsertD)
have fin: "vfinite xs'" using vfsequence_vfinite by auto
have vcard_xs: "vcard xs = succ (vcard xs')" by (simp add: fin False)
have [simp]: "vcard xs' ∉⇩∘ 𝒟⇩∘ xs'" using False vsv_axioms by auto
have "vcard xs' ∈⇩∘ ω" using fin vfinite_vcard_omega by auto
have xs'_def: "xs' = xs ↾⇧l⇩∘ (vcard xs')"
using vcard_xs fin vfsequence_vdomain
by (auto simp: vinsert_ident succ_def)
from vfsequence_vlrestriction[OF ‹vcard xs' ∈⇩∘ ω›] show ?thesis
unfolding xs'_def[symmetric] .
qed

lemma (in vfsequence) vfsequence_vcons_ex:
assumes "xs ≠ []⇩∘"
obtains xs' x where "xs = xs' #⇩∘ x" and "vfsequence xs'"
proof-
from vcard_vempty have "0 ∈⇩∘ vcard xs" by (simp add: assms mem_0_Ord)
then obtain k where succk: "succ k = vcard xs"
by (metis omega_prev vfsequence_vcard_in_omega)
then have "k ∈⇩∘ vcard xs" using elts_succ by blast
from vfsequence_vlrestriction_succ[OF this, unfolded succk] show ?thesis
qed

subsubsection‹Induction and case analysis›

lemma vfsequence_induct[consumes 1, case_names 0 vcons]:
assumes "vfsequence xs"
and "P []⇩∘"
and "⋀xs x. ⟦vfsequence xs; P xs⟧ ⟹ P (xs #⇩∘ x)"
shows "P xs"
proof-
interpret vfsequence xs by (rule assms(1))
from assms(1) obtain n where "n ∈⇩∘ ω" and "𝒟⇩∘ xs = n" by auto
then have "n ≤ 𝒟⇩∘ xs" by auto
define P' where "P' k = P (xs ↾⇧l⇩∘ k)" for k
from ‹n ∈⇩∘ ω› and ‹n ≤ 𝒟⇩∘ xs› have "P' n"
proof(induction rule: omega_induct)
case (succ n') then show ?case
proof-
interpret vlr: vfsequence ‹xs ↾⇧l⇩∘ n'› by (simp add: succ.hyps)
have "P' n'" using succ.prems by (force intro: succ.IH)
then have "P (xs ↾⇧l⇩∘ n')" unfolding P'_def by assumption
have "n' ∈⇩∘ vcard xs"
using succ.prems by (auto simp: vsubset_iff vfsequence_vdomain)
from vfsequence_vlrestriction_succ[OF ‹n' ∈⇩∘ vcard xs›]
show "P' (succ n')"
by (simp add: P'_def ‹P (xs ↾⇧l⇩∘ n')› assms(3) vlr.vfsequence_axioms)
qed
then show ?thesis unfolding P'_def ‹𝒟⇩∘ xs = n›[symmetric] by simp
qed

lemma vfsequence_cases[consumes 1, case_names 0 vcons]:
assumes "vfsequence xs"
and "xs = []⇩∘ ⟹ P"
and "⋀xs' x. ⟦xs = xs' #⇩∘ x; vfsequence xs'⟧ ⟹ P"
shows P
proof-
interpret vfsequence xs by (rule assms(1))
show ?thesis
proof(cases ‹xs = 0›)
case False
then obtain xs' x where "xs = xs' #⇩∘ x"
by (blast intro: vfsequence_vcons_ex)
then show ?thesis by (auto simp: assms(3) intro: vfsequence_vcons_ex)
qed (use assms(2) in auto)
qed

subsubsection‹Evaluation›

lemma (in vfsequence) vfsequence_vcard_vcons[simp]:
"vcard (xs #⇩∘ x) = succ (vcard xs)"
proof-
interpret xsx: vfsequence ‹xs #⇩∘ x› by simp
have "vcard (xs #⇩∘ x) = 𝒟⇩∘ (xs #⇩∘ x)"
by (rule xsx.vfsequence_vdomain[symmetric])
then show ?thesis
by (subst vcons_def) (simp add: succ_def vcons_def vfsequence_vdomain)
qed

lemma (in vfsequence) vfsequence_at_last[intro, simp]:
assumes "i = vcard xs"
shows "(xs #⇩∘ x)⦇i⦈ = x"
by (simp add: vfsequence_vdomain vcons_def assms)

lemma (in vfsequence) vfsequence_at_not_last[intro, simp]:
assumes "i ∈⇩∘ vcard xs"
shows "(xs #⇩∘ x)⦇i⦈ = xs⦇i⦈"
proof-
from assms have [simp]: "𝒟⇩∘ xs = vcard xs" by (auto simp: vfsequence_vdomain)
from assms have "i ∈⇩∘ 𝒟⇩∘ xs" by simp
moreover have "i ≠ vcard xs" using assms mem_not_refl by blast
ultimately show ?thesis
unfolding vcons_def using vsv.vsv_vinsert vsvE vsv_axioms by auto
qed

text‹Alternative forms of existing results.›

lemmas [intro, simp] = vfsequence.vfsequence_vcons
and [intro, simp] = vfsequence.vfsequence_vcard_vcons
and [intro, simp] = vfsequence.vfsequence_at_last
and [intro, simp] = vfsequence.vfsequence_at_not_last
and [intro, simp] = vfsequence.vfsequence_vcons_vdomain
and [intro, simp] = vfsequence.vfsequence_vcons_vrange

subsubsection‹Congruence-like properties›

context vfsequence_pair
begin

lemma vcons_eq_vcard_eq:
assumes "xs⇩1 #⇩∘ x⇩1 = xs⇩2 #⇩∘ x⇩2"
shows "vcard xs⇩1 = vcard xs⇩2"
by
(
metis
assms
succ_inject_iff
vfsequence.vfsequence_vcons_vdomain
r⇩1.vfsequence_axioms
r⇩2.vfsequence_axioms
)

lemma vcons_eqD[dest]:
assumes "xs⇩1 #⇩∘ x⇩1 = xs⇩2 #⇩∘ x⇩2"
shows "xs⇩1 = xs⇩2" and "x⇩1 = x⇩2"
proof-

have xsx1_last: "(xs⇩1 #⇩∘ x⇩1)⦇vcard xs⇩1⦈ = x⇩1" by simp
have xsx2_last: "(xs⇩2 #⇩∘ x⇩2)⦇vcard xs⇩2⦈ = x⇩2" by simp

from assms have vcard: "vcard xs⇩1 = vcard xs⇩2" by (rule vcons_eq_vcard_eq)
from trans[OF xsx1_last xsx1_last[unfolded vcard assms, symmetric]]

show "x⇩1 = x⇩2" unfolding xsx1_last xsx2_last .

have nxs1: "⟨vcard xs⇩1, x⇩1⟩ ∉⇩∘ xs⇩1"
using mem_not_refl r⇩1.vfsequence_vdomain by blast
have nxs2: "⟨vcard xs⇩2, x⇩2⟩ ∉⇩∘ xs⇩2"
using mem_not_refl r⇩2.vfsequence_vdomain by blast
have xsx1_xsx2: "⟨vcard xs⇩1, x⇩1⟩ = ⟨vcard xs⇩2, x⇩2⟩"
unfolding vcons_eq_vcard_eq[OF assms(1)] ‹x⇩1 = x⇩2› by simp

show "xs⇩1 = xs⇩2"
proof(rule vinsert_identD[OF _ nxs1])
from assms(1)[unfolded vcons_def] show
"vinsert ⟨vcard xs⇩1, x⇩1⟩ xs⇩1 = vinsert ⟨vcard xs⇩1, x⇩1⟩ xs⇩2"
by (auto simp: xsx1_xsx2)
show "⟨vcard xs⇩1, x⇩1⟩ ∉⇩∘ xs⇩2"
by (rule nxs2[folded ‹x⇩1 = x⇩2› vcons_eq_vcard_eq[OF assms(1)]])
qed

qed

lemma vcons_eqI:
assumes "xs⇩1 = xs⇩2" and "x⇩1 = x⇩2"
shows "xs⇩1 #⇩∘ x⇩1 = xs⇩2 #⇩∘ x⇩2"
using assms by (rule arg_cong2)

lemma vcons_eq_iff[simp]: "(xs⇩1 #⇩∘ x⇩1 = xs⇩2 #⇩∘ x⇩2) ⟷ (xs⇩1 = xs⇩2 ∧ x⇩1 = x⇩2)"
by auto

end

text‹Alternative forms of existing results.›

context
fixes xs⇩1 xs⇩2
assumes xs⇩1: "vfsequence xs⇩1"
and xs⇩2: "vfsequence xs⇩2"
begin

lemmas_with[OF vfsequence_pair.intro[OF xs⇩1 xs⇩2]]:
vcons_eqD' = vfsequence_pair.vcons_eqD
and vcons_eq_iff[intro, simp] = vfsequence_pair.vcons_eq_iff

end

lemmas vcons_eqD[dest] = vcons_eqD'[rotated -1]

subsection‹Transfer between the type \<^typ>‹V list› and finite sequences›

subsubsection‹Initialization›

primrec vfsequence_of_vlist :: "V list ⇒ V"
where
"vfsequence_of_vlist [] = 0"
| "vfsequence_of_vlist (x # xs) = vfsequence_of_vlist xs #⇩∘ x"

definition vlist_of_vfsequence :: "V ⇒ V list"
where "vlist_of_vfsequence = inv_into UNIV vfsequence_of_vlist"

lemma vfsequence_vfsequence_of_vlist: "vfsequence (vfsequence_of_vlist xs)"
by (induction xs) auto

lemma inj_vfsequence_of_vlist: "inj vfsequence_of_vlist"
proof
show "vfsequence_of_vlist x = vfsequence_of_vlist y ⟹ x = y"
for x y
proof(induction y arbitrary: x)
case Nil then show ?case by (cases x) auto
next
case (Cons a ys)
note Cons' = Cons
show ?case
proof(cases x)
case Nil with Cons show ?thesis by auto
next
case (Cons b zs)
from Cons'[unfolded Cons vfsequence_of_vlist.simps] have
"vfsequence_of_vlist zs #⇩∘ b = vfsequence_of_vlist ys #⇩∘ a"
by simp
then have "vfsequence_of_vlist zs = vfsequence_of_vlist ys" and "b = a"
by (auto simp: vfsequence_vfsequence_of_vlist)
from Cons'(1)[OF this(1)] this(2) show ?thesis unfolding Cons by auto
qed
qed
qed

lemma range_vfsequence_of_vlist:
"range vfsequence_of_vlist = {xs. vfsequence xs}"
proof(intro subset_antisym subsetI; unfold mem_Collect_eq)
show "xs ∈ range vfsequence_of_vlist ⟹ vfsequence xs" for xs
by (clarsimp simp: vfsequence_vfsequence_of_vlist)
fix xs assume "vfsequence xs"
then show "xs ∈ range vfsequence_of_vlist"
proof(induction rule: vfsequence_induct)
case 0 then show ?case
by (metis image_iff iso_tuple_UNIV_I vfsequence_of_vlist.simps(1))
next
case (vcons xs x) then show ?case
by (metis rangeE rangeI vfsequence_of_vlist.simps(2))
qed
qed

lemma vlist_of_vfsequence_vfsequence_of_vlist[simp]:
"vlist_of_vfsequence (vfsequence_of_vlist xs) = xs"

lemma (in vfsequence) vfsequence_of_vlist_vlist_of_vfsequence[simp]:
"vfsequence_of_vlist (vlist_of_vfsequence xs) = xs"
using vfsequence_axioms range_vfsequence_of_vlist inj_vfsequence_of_vlist

lemmas vfsequence_of_vlist_vlist_of_vfsequence[intro, simp] =
vfsequence.vfsequence_of_vlist_vlist_of_vfsequence

lemma vlist_of_vfsequence_vempty[simp]: "vlist_of_vfsequence []⇩∘ = []"
by
(
metis
vfsequence_of_vlist.simps(1)
vlist_of_vfsequence_vfsequence_of_vlist
)

text‹Transfer relation 1.›

definition cr_vfsequence :: "V ⇒ V list ⇒ bool"
where "cr_vfsequence a b ⟷ (a = vfsequence_of_vlist b)"

lemma cr_vfsequence_right_total[transfer_rule]: "right_total cr_vfsequence"
unfolding cr_vfsequence_def right_total_def by simp

lemma cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_vfsequence"
unfolding cr_vfsequence_def bi_unique_def

lemma cr_vfsequence_transfer_domain_rule[transfer_domain_rule]:
"Domainp cr_vfsequence = (λxs. vfsequence xs)"
unfolding cr_vfsequence_def
proof(intro HOL.ext, rule iffI)
fix xs assume prems: "vfsequence xs"
interpret vfsequence xs by (rule prems)
have "∃ys. xs = vfsequence_of_vlist ys"
using prems
proof(induction rule: vfsequence_induct)
show "⟦ vfsequence xs; ∃ys. xs = vfsequence_of_vlist ys ⟧ ⟹
∃ys. xs #⇩∘ x = vfsequence_of_vlist ys"
for xs x
unfolding vfsequence_of_vlist_def by (metis list.simps(7))
qed auto
then show "Domainp (λa b. a = vfsequence_of_vlist b) xs" by auto
qed (clarsimp simp: vfsequence_vfsequence_of_vlist)

lemma cr_vfsequence_vconsD:
assumes "cr_vfsequence (xs #⇩∘ x) (y # ys)"
shows "cr_vfsequence xs ys" and "x = y"
proof-
from assms[unfolded cr_vfsequence_def] have xs_x_def:
"xs #⇩∘ x = vfsequence_of_vlist (y # ys)" .
then have xs_x: "vfsequence (xs #⇩∘ x)"
interpret vfsequence xs
by (blast intro: vfsequence.vfsequence_vremove_vcons_vfsequence xs_x)
from
assms[unfolded cr_vfsequence_def vfsequence_of_vlist.simps(2)]
vfsequence_axioms
show "cr_vfsequence xs ys" and "x = y"
unfolding cr_vfsequence_def by (auto simp: vfsequence_vfsequence_of_vlist)
qed

text‹Transfer relation 2.›

definition cr_cr_vfsequence :: "V ⇒ V list list ⇒ bool"
where "cr_cr_vfsequence a b ⟷
(a = vfsequence_of_vlist (map vfsequence_of_vlist b))"

lemma cr_cr_vfsequence_right_total[transfer_rule]:
"right_total cr_cr_vfsequence"
unfolding cr_cr_vfsequence_def right_total_def by simp

lemma cr_cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_cr_vfsequence"
unfolding cr_cr_vfsequence_def bi_unique_def

text‹Transfer relation for scalars.›

definition cr_scalar :: "(V ⇒ 'a ⇒ bool) ⇒ V ⇒ 'a ⇒ bool"
where "cr_scalar R x y = (∃a. x = [a]⇩∘ ∧ R a y)"

lemma cr_scalar_bi_unique[transfer_rule]:
assumes "bi_unique R"
shows "bi_unique (cr_scalar R)"
using assms unfolding cr_scalar_def bi_unique_def by auto

lemma cr_scalar_right_total[transfer_rule]:
assumes "right_total R"
shows "right_total (cr_scalar R)"
using assms unfolding cr_scalar_def right_total_def by simp

lemma cr_scalar_transfer_domain_rule[transfer_domain_rule]:
"Domainp (cr_scalar R) = (λx. ∃a. x = [a]⇩∘ ∧ Domainp R a)"
unfolding cr_scalar_def by auto

subsubsection‹Transfer rules for previously defined entities›

context
includes lifting_syntax
begin

lemma vfsequence_vempty_transfer[transfer_rule]: "cr_vfsequence []⇩∘ []"
unfolding cr_vfsequence_def by simp

lemma vfsequence_vempty_ll_transfer[transfer_rule]:
"cr_cr_vfsequence [[]⇩∘]⇩∘ [[]]"
unfolding cr_cr_vfsequence_def by simp

lemma vcons_transfer[transfer_rule]:
"((=) ===> cr_vfsequence ===> cr_vfsequence) (λx xs. xs #⇩∘ x) (λx xs. x # xs)"
by (intro rel_funI) (simp add: cr_vfsequence_def)

lemma vcons_ll_transfer[transfer_rule]:
"(cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence)
(λx xs. xs #⇩∘ x) (λx xs. x # xs)"
by (intro rel_funI) (simp add: cr_vfsequence_def cr_cr_vfsequence_def)

lemma vfsequence_vrange_transfer[transfer_rule]:
"(cr_vfsequence ===> (=)) (λxs. elts (ℛ⇩∘ xs)) list.set"
proof(intro rel_funI)
fix xs ys assume prems: "cr_vfsequence xs ys"
then have "xs = vfsequence_of_vlist ys" unfolding cr_vfsequence_def by simp
then have "vfsequence xs" by (simp add: vfsequence_vfsequence_of_vlist)
from this prems show "elts (ℛ⇩∘ xs) = list.set ys"
proof(induction ys arbitrary: xs)
case (Cons a ys)
from Cons(2) show ?case
proof(cases xs rule: vfsequence_cases)
case 0 with Cons show ?thesis by (simp add: Cons.IH cr_vfsequence_def)
next
case (vcons xs' x)
interpret vfsequence xs' by (rule vcons(2))
note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
have a_ys: "list.set (a # ys) = insert a (list.set ys)" by simp
from vcons(2) have R_xs'x: "ℛ⇩∘ (xs' #⇩∘ x) = vinsert x (ℛ⇩∘ xs')" by simp
show "elts (ℛ⇩∘ xs) = (list.set (a # ys))"
unfolding vcons(1) R_xs'x a_ys
by
(
auto simp:
vcons_transfer(2) Cons(1)[OF vfsequence_axioms vcons_transfer(1)]
)
qed
qed (auto simp: cr_vfsequence_def)
qed

lemma vcard_transfer[transfer_rule]:
"(cr_vfsequence ===> cr_omega) vcard length"
proof(intro rel_funI)
fix xs ys assume prems: "cr_vfsequence xs ys"
then have "xs = vfsequence_of_vlist ys" unfolding cr_vfsequence_def by simp
then have "vfsequence xs" by (simp add: vfsequence_vfsequence_of_vlist)
from this prems show "cr_omega (vcard xs) (length ys)"
proof(induction ys arbitrary: xs)
case (Cons y ys)
from Cons(2) show ?case
proof(cases xs rule: vfsequence_cases)
case 0 with Cons show ?thesis by (simp add: Cons.IH cr_vfsequence_def)
next
case (vcons xs' x)
interpret vfsequence xs' by (rule vcons(2))
note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
have vcard_xs_x: "vcard (xs' #⇩∘ x) = succ (vcard xs')" by simp
have vcard_y_ys: "length (y # ys) = Suc (length ys)" by simp
from vfsequence_axioms have [transfer_rule]:
"cr_omega (vcard xs') (length ys)"
show ?thesis unfolding vcons(1) vcard_xs_x vcard_y_ys by transfer_prover
qed
qed (auto simp: cr_omega_def cr_vfsequence_def)
qed

lemma vcard_ll_transfer[transfer_rule]:
"(cr_cr_vfsequence ===> cr_omega) vcard length"
unfolding cr_cr_vfsequence_def
by (intro rel_funI)
(metis cr_vfsequence_def length_map rel_funD vcard_transfer)

end

text‹Corollaries.›

lemma vdomain_vfsequence_of_vlist: "𝒟⇩∘ (vfsequence_of_vlist xs) = length xs"
proof-
define ys where "ys = vfsequence_of_vlist xs"
interpret vfsequence ys
unfolding ys_def by (rule vfsequence_vfsequence_of_vlist)
have [transfer_rule]: "cr_vfsequence ys xs"
unfolding ys_def cr_vfsequence_def by simp_all
show ?thesis
by (fold ys_def, unfold vfsequence_vdomain, transfer) simp
qed

lemma vrange_vfsequence_of_vlist:
"ℛ⇩∘ (vfsequence_of_vlist xs) = set (list.set xs)"
proof(intro vsubset_antisym vsubsetI)
fix x assume prems: "x ∈⇩∘ ℛ⇩∘ (vfsequence_of_vlist xs)"
define ys where "ys = vfsequence_of_vlist xs"
have [transfer_rule]: "cr_vfsequence ys xs" "x = x"
unfolding ys_def cr_vfsequence_def by simp_all
show "x ∈⇩∘ set (list.set xs)" by transfer (simp add: prems[folded ys_def])
next
fix x assume prems: "x ∈⇩∘ set (list.set xs)"
define ys where "ys = vfsequence_of_vlist xs"
have [transfer_rule]: "cr_vfsequence ys xs" "x = x"
unfolding ys_def cr_vfsequence_def by simp_all
from prems[untransferred] show "x ∈⇩∘ ℛ⇩∘ (vfsequence_of_vlist xs)"
unfolding ys_def by simp
qed

lemma cr_cr_vfsequence_transfer_domain_rule[transfer_domain_rule]:
"Domainp cr_cr_vfsequence =
(λxss. vfsequence xss ∧ (∀xs∈⇩∘ℛ⇩∘ xss. vfsequence xs))"
proof(intro HOL.ext, rule iffI; (elim conjE | intro conjI ballI))
fix xss assume prems: "Domainp cr_cr_vfsequence xss"
with vfsequence_vfsequence_of_vlist show xss: "vfsequence xss"
unfolding cr_cr_vfsequence_def by clarsimp
interpret vfsequence xss by (rule xss)
fix xs assume prems': "xs ∈⇩∘ ℛ⇩∘ xss"
from prems obtain yss where xss_def:
"xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
unfolding cr_cr_vfsequence_def by clarsimp
from prems' have "xs ∈⇩∘ set (list.set (map vfsequence_of_vlist yss))"
unfolding xss_def vrange_vfsequence_of_vlist by simp
then obtain ys where xs_def: "xs = vfsequence_of_vlist ys" by clarsimp
show "vfsequence xs"
unfolding xs_def by (simp add: vfsequence_vfsequence_of_vlist)
next
fix xss assume prems: "vfsequence xss" "∀xs∈⇩∘ℛ⇩∘ xss. vfsequence xs"
have "∃yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
using prems
proof(induction rule: vfsequence_induct)
case (vcons xss x)
let ?y = ‹vlist_of_vfsequence x›
from vcons(2,3) obtain yss where xss_def:
"xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
by auto
from vcons(3) have "vfsequence x" by auto
then have x_def: "x = vfsequence_of_vlist (vlist_of_vfsequence x)" by simp
then have
"xss #⇩∘ x = vfsequence_of_vlist (map vfsequence_of_vlist (?y # yss))"
unfolding xss_def by simp
then show ?case by blast
qed (auto intro: exI[of _ ‹[]›])
then show "Domainp cr_cr_vfsequence xss"
unfolding cr_cr_vfsequence_def by blast
qed

subsubsection‹Appending elements›

definition vappend :: "V ⇒ V ⇒ V" (infixr "@⇩∘" 65)
where "xs @⇩∘ ys =
vfsequence_of_vlist (vlist_of_vfsequence ys @ vlist_of_vfsequence xs)"

text‹Transfer.›

lemma vappend_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence)
(λxs ys. vappend ys xs) append"
by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vappend_def)

lemma vappend_ll_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence)
(λxs ys. vappend ys xs) append"
by (intro rel_funI, unfold cr_cr_vfsequence_def) (simp add: vappend_def)

text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vappend_vempty_vfsequence[simp]:
"[]⇩∘ @⇩∘ xs = xs"
unfolding vappend_def by auto

lemmas vfsequence_vappend_vempty_vfsequence[simp] =
vfsequence.vfsequence_vappend_vempty_vfsequence

lemma (in vfsequence) vfsequence_vappend_vfsequence_vempty[simp]:
"xs @⇩∘ []⇩∘ = xs"
unfolding vappend_def by auto

lemmas vfsequence_vappend_vfsequence_vempty[simp] =
vfsequence.vfsequence_vappend_vfsequence_vempty

lemma vappend_vcons[simp]:
assumes "vfsequence xs" and "vfsequence ys"
shows "xs @⇩∘ (ys #⇩∘ y) = (xs @⇩∘ ys) #⇩∘ y"
using append_Cons[where 'a=V, untransferred, OF assms(2,1)] by simp

subsubsection‹Distinct elements›

definition vdistinct :: "V ⇒ bool"
where "vdistinct xs = distinct (vlist_of_vfsequence xs)"

text‹Transfer.›

lemma vdistinct_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_vfsequence ===> (=)) vdistinct distinct"
by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vdistinct_def)

lemma vdistinct_ll_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_cr_vfsequence ===> (=)) vdistinct distinct"
by (intro rel_funI, unfold cr_cr_vfsequence_def)
(
metis
vdistinct_def
distinct_map
inj_onI
vlist_of_vfsequence_vfsequence_of_vlist
)

text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vdistinct_if_vcard_vrange_eq_vcard:
assumes "vcard (ℛ⇩∘ xs) = vcard xs"
shows "vdistinct xs"
proof-
have "finite (elts (ℛ⇩∘ xs))" by (simp add: assms vcard_vfinite_omega)
from vcard_finite_set[OF this] assms have "card (elts (ℛ⇩∘ xs))⇩ℕ = vcard xs"
by simp
from card_distinct[where ?'a=V, untransferred, OF vfsequence_axioms this]
show ?thesis.
qed

lemma vdistinct_vempty[intro, simp]: "vdistinct []⇩∘"
proof-
have t: "distinct ([]::V list)" by simp
show ?thesis by (rule t[untransferred])
qed

lemma (in vfsequence) vfsequence_vcons_vdistinct:
assumes "vdistinct (xs #⇩∘ x)"
shows "vdistinct xs"
proof-
from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct2, untransferred]
show ?thesis
using vfsequence_axioms assms by simp
qed

lemma (in vfsequence) vfsequence_vcons_nin_vrange:
assumes "vdistinct (xs #⇩∘ x)"
shows "x ∉⇩∘ ℛ⇩∘ xs"
proof-
from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct1, untransferred]
show ?thesis
using vfsequence_axioms assms by simp
qed

lemma (in vfsequence) vfsequence_v11I[intro]:
assumes "vdistinct xs"
shows "v11 xs"
using vfsequence_axioms assms
proof(induction xs rule: vfsequence_induct)
case (vcons xs x)
interpret vfsequence xs by (rule vcons(1))
from vcons(3) have dxs: "vdistinct xs" by (rule vfsequence_vcons_vdistinct)
interpret v11 xs using dxs by (rule vcons(2))
from vfsequence_vcons_nin_vrange[OF vcons(3)] have "x ∉⇩∘ ℛ⇩∘ xs" .
show "v11 (xs #⇩∘ x)"
by
(
vcons_def vfsequence_vdomain vfsequence_vcons_nin_vrange[OF vcons(3)]
)
qed simp

lemma (in vfsequence) vfsequence_vcons_vdistinctI:
assumes "vdistinct xs" and "x ∉⇩∘ ℛ⇩∘ xs"
shows "vdistinct (xs #⇩∘ x)"
proof-
have t: "distinct xs ⟹ x ∉ list.set xs ⟹ distinct (x # xs)"
for x ::V and xs
by simp
from vfsequence_axioms assms show ?thesis by (rule t[untransferred])
qed

lemmas vfsequence_vcons_vdistinctI[intro] =
vfsequence.vfsequence_vcons_vdistinctI

lemma (in vfsequence) vfsequence_nin_vrange_vcons:
assumes "y ∉⇩∘ ℛ⇩∘ xs" and "y ≠ x"
shows "y ∉⇩∘ ℛ⇩∘ (xs #⇩∘ x)"
proof-
have t: "y ∉ list.set xs ⟹ y ≠ x ⟹ y ∉ list.set (x # xs)"
for x y :: V and xs
by simp
from vfsequence_axioms assms show ?thesis by (rule t[untransferred])
qed

lemmas vfsequence_nin_vrange_vcons[intro] =
vfsequence.vfsequence_nin_vrange_vcons

subsubsection‹Concatenation of sequences›

definition vconcat :: "V ⇒ V"
where "vconcat xss =
vfsequence_of_vlist(
concat (map vlist_of_vfsequence (vlist_of_vfsequence xss))
)"

text‹Transfer.›

lemma vconcat_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_cr_vfsequence ===> cr_vfsequence) vconcat concat"
proof(intro rel_funI)
fix xs ys assume "cr_cr_vfsequence xs ys"
then have xs_def: "xs = vfsequence_of_vlist (map vfsequence_of_vlist ys)"
unfolding cr_cr_vfsequence_def by simp
have main_eq: "map vlist_of_vfsequence (vlist_of_vfsequence xs) = ys"
unfolding xs_def by (simp add: map_idI)
show "cr_vfsequence (vconcat xs) (concat ys)"
unfolding cr_vfsequence_def vconcat_def main_eq ..
qed

text‹Elementary properties.›

lemma vconcat_vempty[simp]: "vconcat []⇩∘ = []⇩∘"
unfolding vconcat_def by simp

lemma vconcat_append[simp]:
assumes "vfsequence xss"
and "∀xs∈⇩∘ℛ⇩∘ xss. vfsequence xs"
and "vfsequence yss"
and "∀xs∈⇩∘ℛ⇩∘ yss. vfsequence xs"
shows "vconcat (xss @⇩∘ yss) = vconcat xss @⇩∘ vconcat yss"
using assms concat_append[where 'a=V, untransferred] by simp

lemma vconcat_vcons[simp]:
assumes "vfsequence xs" and "vfsequence xss" and "∀xs∈⇩∘ℛ⇩∘ xss. vfsequence xs"
shows "vconcat (xss #⇩∘ xs) = vconcat xss @⇩∘ xs"
using assms concat.simps(2)[where 'a=V, untransferred] by simp

lemma (in vfsequence) vfsequence_vconcat_fsingleton[simp]: "vconcat [xs]⇩∘ = xs"
using vfsequence_axioms
by
(
metis
vfsequence_vappend_vempty_vfsequence
vconcat_vcons
vconcat_vempty
vempty_nin
vfsequence_vempty
vrange_vempty
)

lemmas vfsequence_vconcat_fsingleton[simp] =
vfsequence.vfsequence_vconcat_fsingleton

subsection‹Finite sequences and the Cartesian product›

lemma vfsequence_vcons_vproductI[intro!]:
assumes "n ∈⇩∘ ω"
and "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A i)"
and "x ∈⇩∘ A (vcard xs)"
and "n = vcard (xs #⇩∘ x)"
shows "xs #⇩∘ x ∈⇩∘ (∏⇩∘i∈⇩∘n. A i)"
proof
interpret xs: vfsequence xs
using assms
apply(intro vfsequenceI)
subgoal by auto
subgoal
by
(
metis
vcard_vfinite_omega
vcons_vsubset
vfinite_vcard_omega
vfinite_vsubset vproductD(2)
)
done
interpret xsx: vfsequence ‹xs #⇩∘ x› by auto
show "vsv (xs #⇩∘ x)" by (simp add: xsx.vsv_axioms)
show D: "𝒟⇩∘ (xs #⇩∘ x) = n" unfolding assms(4) xsx.vfsequence_vdomain by auto
from vproductD[OF assms(2)] have elem: "i ∈⇩∘ vcard xs ⟹ xs⦇i⦈ ∈⇩∘ A i" for i
by auto
show "∀i∈⇩∘n. (xs #⇩∘ x)⦇i⦈ ∈⇩∘ A i" by (auto simp: elem assms(3,4))
qed

lemma vfsequence_vcons_vproductD[dest]:
assumes "xs #⇩∘ x ∈⇩∘ (∏⇩∘i∈⇩∘n. A i)" and "n ∈⇩∘ ω"
shows "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A i)"
and "x ∈⇩∘ A (vcard xs)"
and "n = vcard (xs #⇩∘ x)"
proof-

interpret xsx: vfsequence ‹xs #⇩∘ x›
by (meson assms succ_in_omega vfsequence_vproduct)
interpret xs: vfsequence xs
by (blast intro: xsx.vfsequence_vremove_vcons_vfsequence)

show n_def: "n = vcard (xs #⇩∘ x)"
using assms using xsx.vfsequence_vdomain by blast
from vproductD[OF assms(1), unfolded n_def]
have elem_xs_x: "i ∈⇩∘ vcard (xs #⇩∘ x) ⟹ (xs #⇩∘ x)⦇i⦈ ∈⇩∘ A i"
for i
by auto
then have elem_xs[simp]: "i ∈⇩∘ vcard xs ⟹ xs⦇i⦈ ∈⇩∘ A i" for i
by (metis rev_vsubsetD vcard_mono vcons_vsubset xs.vfsequence_at_not_last)
show "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A i)"
by (auto simp: xs.vsv_axioms xs.vfsequence_vdomain)
from elem_xs_x show "x ∈⇩∘ A (vcard xs)" by fastforce

qed

lemma vfsequence_vcons_vproductE[elim!]:
assumes "xs #⇩∘ x ∈⇩∘ (∏⇩∘i∈⇩∘n. A i)" and "n ∈⇩∘ ω"
obtains "xs ∈⇩∘ (∏⇩∘i∈⇩∘vcard xs. A i)"
and "x ∈⇩∘ A (vcard xs)"
and "n = vcard (xs #⇩∘ x)"
using assms by (auto simp: vfsequence_vcons_vproductD)

subsection‹Binary Cartesian product based on finite sequences: ‹ftimes››

definition ftimes :: "V ⇒ V ⇒ V" (infixr ‹×⇩∙› 80)
where "ftimes a b ≡ (∏⇩∘i∈⇩∘2⇩ℕ. if i = 0 then a else b)"

lemma small_fpairs[simp]: "small {[a, b]⇩∘ | a b. [a, b]⇩∘ ∈⇩∘ r}"
by (rule down[of _ r]) clarsimp

text‹Rules.›

lemma ftimesI1[intro]:
assumes "x = [a, b]⇩∘" and "a ∈⇩∘ A" and "b ∈⇩∘ B"
shows "x ∈⇩∘ A ×⇩∙ B"
unfolding ftimes_def
proof
show vsv: "vsv x" by (simp add: assms(1) vfsequence.axioms(1))
then interpret vsv x .
from assms show D: "𝒟⇩∘ x = 2⇩ℕ"
unfolding nat_omega_simps two One_nat_def by auto
from assms(2,3) have i: "i ∈⇩∘ 2⇩ℕ ⟹ x⦇i⦈ ∈⇩∘ (if i = 0⇩ℕ then A else B)"
for i
unfolding assms(1) two nat_omega_simps One_nat_def by auto
from i show "∀i∈⇩∘2⇩ℕ. x⦇i⦈ ∈⇩∘ (if i = 0 then A else B)" by auto
qed

lemma ftimesI2[intro!]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ B"
shows "[a, b]⇩∘ ∈⇩∘ A ×⇩∙ B"
using assms ftimesI1 by auto

lemma fproductE1[elim!]:
assumes "x ∈⇩∘ A ×⇩∙ B"
obtains a b where "x = [a, b]⇩∘" and "a ∈⇩∘ A" and "b ∈⇩∘ B"
proof-
from vproduct_vdoubletonD[OF assms[unfolded two ftimes_def]]
have x_def: "x = set {⟨0⇩ℕ, x⦇0⇩ℕ⦈⟩, ⟨1⇩ℕ, x⦇1⇩ℕ⦈⟩}"
and "x⦇0⇩ℕ⦈ ∈⇩∘ A"
and "x⦇1⇩ℕ⦈ ∈⇩∘ B"
by auto
then show ?thesis using that using vcons_vdoubleton by simp
qed

lemma fproductE2[elim!]:
assumes "[a, b]⇩∘ ∈⇩∘ A ×⇩∙ B" obtains "a ∈⇩∘ A" and "b ∈⇩∘ B"
using assms by blast

text‹Set operations.›

lemma vfinite_0_left[simp]: "0 ×⇩∙ b = 0"
by (meson eq0_iff fproductE1)

lemma vfinite_0_right[simp]: "a ×⇩∙ 0 = 0"
by (meson eq0_iff fproductE1)

lemma fproduct_vintersection: "(a ∩⇩∘ b) ×⇩∙ (c ∩⇩∘ d) = (a ×⇩∙ c) ∩⇩∘ (b ×⇩∙ d)"
by auto

lemma fproduct_vdiff: "a ×⇩∙ (b -⇩∘ c) = (a ×⇩∙ b) -⇩∘ (a ×⇩∙ c)" by auto

lemma vfinite_ftimesI[intro!]:
assumes "vfinite a" and "vfinite b"
shows "vfinite (a ×⇩∙ b)"
using assms(1,2)
proof(induction arbitrary: b rule: vfinite_induct)
case (vinsert x a')
from vinsert(4) have "vfinite (set {x} ×⇩∙ b)"
proof(induction rule: vfinite_induct)
case (vinsert y b')
have "set {x} ×⇩∙ vinsert y b' = vinsert [x, y]⇩∘ (set {x} ×⇩∙ b')" by auto
with vinsert(3) show ?case by simp
qed simp
moreover have "vinsert x a' ×⇩∙ b = (set {x} ×⇩∙ b) ∪⇩∘ (a' ×⇩∙ b)" by auto
ultimately show ?case using vinsert by (auto simp: vfinite_vunionI)
qed simp

text‹‹ftimes› and ‹vcpower››

lemma vproduct_vpair: "[a, b]⇩∘ ∈⇩∘ (∏⇩∘i∈⇩∘2⇩ℕ. f i) ⟷ ⟨a, b⟩ ∈⇩∘ f (0⇩ℕ) ×⇩∘ f (1⇩ℕ)"
proof
interpret vfsequence ‹[a, b]⇩∘› by simp
show "[a, b]⇩∘ ∈⇩∘ (∏⇩∘i∈⇩∘2⇩ℕ. f i) ⟹ ⟨a, b⟩ ∈⇩∘ f (0⇩ℕ) ×⇩∘ f (1⇩ℕ)"
unfolding vcons_vdoubleton two by (elim vproduct_vdoubletonE) auto
assume hyp: "⟨a, b⟩ ∈⇩∘ f (0⇩ℕ) ×⇩∘ f (1⇩ℕ)"
then have af: "a ∈⇩∘ f (0⇩ℕ)" and bf: "b ∈⇩∘ f (1⇩ℕ)" by auto
have dom: "𝒟⇩∘ [a, b]⇩∘ = set {0⇩ℕ, 1⇩ℕ}" by (auto intro!: vsubset_antisym)
have ran: "ℛ⇩∘ [a, b]⇩∘ ⊆⇩∘ (⋃⇩∘i∈⇩∘2⇩ℕ. f i)"
unfolding two using af bf vifunion_vdoubleton by auto
show "[a, b]⇩∘ ∈⇩∘ (∏⇩∘i∈⇩∘2⇩ℕ. f i)"
apply(intro vproductI)
subgoal using dom ran vsv_axioms unfolding two by auto
subgoal using af bf unfolding two by (auto intro!: vsubset_antisym)
subgoal
unfolding two
using hyp VSigmaE2 small_empty vcons_vdoubleton
by (auto simp: vinsert_set_insert_eq)
done
qed

text‹Connections.›

lemma vcpower_two_ftimes: "A ^⇩× 2⇩ℕ = A ×⇩∙ A"
unfolding vcpower_def ftimes_def two by simp

lemma vcpower_two_ftimesI[intro]:
assumes "x ∈⇩∘ A ×⇩∙ A"
shows "x ∈⇩∘ A ^⇩× 2⇩ℕ"
using assms unfolding ftimes_def two by auto

lemma vcpower_two_ftimesD[dest]:
assumes "x ∈⇩∘ A ^⇩× 2⇩ℕ"
shows "x ∈⇩∘ A ×⇩∙ A"
using assms unfolding vcpower_def ftimes_def two by simp

lemma vcpower_two_ftimesE[elim]:
assumes "x ∈⇩∘ A ^⇩× 2⇩ℕ" and "x ∈⇩∘ A ×⇩∙ A ⟹ P"
shows P
using assms unfolding vcpower_def ftimes_def two by simp

lemma vfsequence_vcpower_two_vpair: "[a, b]⇩∘ ∈⇩∘ A ^⇩× 2⇩ℕ ⟷ ⟨a, b⟩ ∈⇩∘ A ×⇩∘ A"
proof(rule iffI)
show "[a, b]⇩∘ ∈⇩∘ A ^⇩× 2⇩ℕ ⟹ ⟨a, b⟩ ∈⇩∘ A ×⇩∘ A"
by (elim vcpowerE, unfold vproduct_vpair)
qed (intro vcpowerI, unfold vproduct_vpair)

lemma vsv_vfsequence_two:
assumes "vsv gf" and "𝒟⇩∘ gf = 2⇩ℕ"
shows "[vpfst gf, vpsnd gf]⇩∘ = gf"
proof-
interpret gf: vsv gf by (auto intro: assms(1))
show ?thesis
by
(
rule sym,
rule vsv_eqI,
blast,
blast,
unfold assms(2),
elim_in_numeral,
)
qed

lemma vsv_vfsequence_three:
assumes "vsv hgf" and "𝒟⇩∘ hgf = 3⇩ℕ"
shows "[vpfst hgf, vpsnd hgf, vpthrd hgf]⇩∘ = hgf"
proof-
interpret hgf: vsv hgf by (auto intro: assms(1))
show ?thesis
by
(
rule sym,
rule vsv_eqI,
blast,
blast,
unfold assms(2),
elim_in_numeral,
)
qed

subsection‹Sequence as an element of a Cartesian power of a set›

lemma vcons_in_vcpowerI[intro!]:
assumes "n ∈⇩∘ ω"
and "xs ∈⇩∘ A ^⇩× vcard xs"
and "x ∈⇩∘ A"
and "n = vcard (xs #⇩∘ x)"
shows "xs #⇩∘ x ∈⇩∘ A ^⇩× n"
proof-
interpret vfsequence xs
using assms
by
(
meson
vcons_vsubset
vfinite_vcard_omega_iff
vfinite_vsubset
vfsequence_vcpower
)
show ?thesis
by
(
metis
assms(2,3,4)
vcpower_vrange
vfsequence_vcons
vfsequence_vcons_vrange
vfsequence.vfsequence_vrange_vcpower
vsubset_vinsert_leftI
)
qed

lemma vcons_in_vcpowerD[dest]:
assumes "xs #⇩∘ x ∈⇩∘ A ^⇩× n" and "n ∈⇩∘ ω"
shows "xs ∈⇩∘ A ^⇩× vcard xs"
and "x ∈⇩∘ A"
and "n = vcard (xs #⇩∘ x)"
proof-
interpret vfsequence xs
by
(
meson
assms
vfsequence.vfsequence_vremove_vcons_vfsequence
vfsequence_vcpower
)
from assms vfsequence_vcard_vcons show "n = vcard (xs #⇩∘ x)" by auto
then show "xs ∈⇩∘ A ^⇩× vcard xs"
by
(
metis
assms(1)
vcpower_vrange
vfsequence_vcons_vrange
vfsequence_vrange_vcpower
vsubset_vinsert_leftD
)
show "x ∈⇩∘ A"
by
(
metis
assms(1)
vcpower_vrange
vfsequence.vfsequence_vcons_vrange
vfsequence_axioms
vinsertI1
vsubsetE
)
qed

lemma vcons_in_vcpowerE1[elim!]:
assumes "xs #⇩∘ x ∈⇩∘ A ^⇩× n" and "n ∈⇩∘ ω"
obtains "xs ∈⇩∘ A ^⇩× vcard xs" and "x ∈⇩∘ A" and "n = vcard (xs #⇩∘ x)"
using assms by blast

lemma vcons_in_vcpowerE2:
assumes "xs ∈⇩∘ A ^⇩× n" and "n ∈⇩∘ ω" and "0 ∈⇩∘ n"
obtains x xs' where "xs = xs' #⇩∘ x"
and "xs' ∈⇩∘ A ^⇩× vcard xs'"
and "x ∈⇩∘ A"
and "n = vcard (xs' #⇩∘ x)"
proof-
interpret vfsequence xs using assms(1,2) by auto
from assms obtain x xs' where xs_def: "xs = xs' #⇩∘ x"
by
(
metis
eq0_iff vcard_0 vcpower_vdomain vfsequence_vcons_ex vfsequence_vdomain
)
from vcons_in_vcpowerE1[OF assms(1)[unfolded xs_def] assms(2)] have
"xs' ∈⇩∘ A ^⇩× vcard xs'" and "x ∈⇩∘ A" and "n = vcard (xs' #⇩∘ x)"
by blast+
from xs_def this show ?thesis by (clarsimp simp: that)
qed

lemma vcons_vcpower1E: (*TODO: generalize*)
assumes "xs ∈⇩∘ A ^⇩× 1⇩ℕ"
obtains x where "xs = [x]⇩∘" and "x ∈⇩∘ A"
proof-
have 01: "0 ∈⇩∘ 1⇩ℕ" by simp
from vcons_in_vcpowerE2[OF assms ord_of_nat_ω 01] obtain x xs'
where xs_def: "xs = xs' #⇩∘ x"
and xs': "xs' ∈⇩∘ A ^⇩× vcard xs'"
and x: "x ∈⇩∘ A"
and one: "1⇩ℕ = vcard (xs' #⇩∘ x)"
by metis
interpret xs: vfsequence xs using assms by (auto intro: vfsequence_vcpower)
interpret xs': vfsequence xs'
using xs' xs_def xs.vfsequence_vremove_vcons_vfsequence by blast
from one have "vcard xs' = 0"
by (metis ord_of_nat_succ_vempty succ_inject_iff xs'.vfsequence_vcard_vcons)
then have "xs = [x]⇩∘" unfolding xs_def by (simp add: vcard_vempty)
with x that show ?thesis by simp
qed

subsection‹The set of all finite sequences on a set›

subsubsection‹Definition and elementary properties›

definition vfsequences_on :: "V ⇒ V"
where "vfsequences_on X = set {x. vfsequence x ∧ (∀i∈⇩∘𝒟⇩∘ x. x⦇i⦈ ∈⇩∘ X)}"

lemma vfsequences_on_subset_ω_set:
"{x. vfsequence x ∧ (∀i∈elts (𝒟⇩∘ x). x⦇i⦈ ∈⇩∘ X)} ⊆ elts (VPow (ω ×⇩∘ X))"
proof
(
intro subsetI,
unfold mem_Collect_eq VPow_iff,
elim conjE,
intro vsubsetI
)
fix xs nx
assume prems[rule_format]:
"vfsequence xs"
"∀i∈⇩∘𝒟⇩∘ xs. xs⦇i⦈ ∈⇩∘ X"
"nx ∈⇩∘ xs"
interpret vfsequence xs by (rule prems(1))
from prems(3) vbrelation obtain n x where nx_def: "nx = ⟨n, x⟩" by auto
from vsv_appI[OF prems(3)[unfolded this]] have xsn: "xs⦇n⦈ = x" .
from prems(3) nx_def have "n ∈⇩∘ 𝒟⇩∘ xs" by auto
with prems(2) show "nx ∈⇩∘ ω ×⇩∘ X"
by (auto simp: nx_def xsn[symmetric] Ord_trans vfsequence_vdomain_in_omega)
qed

lemma small_vfsequences_on[simp]:
"small {x. vfsequence x ∧ (∀i∈⇩∘𝒟⇩∘ x. x⦇i⦈ ∈⇩∘ X)}"
by (rule down, rule vfsequences_on_subset_ω_set)

text‹Rules.›

lemma vfsequences_onI:
assumes "vfsequence xs" and "⋀i. i ∈⇩∘ 𝒟⇩∘ xs ⟹ xs⦇i⦈ ∈⇩∘ X"
shows "xs ∈⇩∘ vfsequences_on X"
using assms unfolding vfsequences_on_def by simp

lemma vfsequences_onD[dest]:
assumes "xs ∈⇩∘ vfsequences_on X"
shows "vfsequence xs" and "⋀i. i ∈⇩∘ 𝒟⇩∘ xs ⟹ xs⦇i⦈ ∈⇩∘ X"
using assms unfolding vfsequences_on_def by auto

lemma vfsequences_onE[elim]:
assumes "xs ∈⇩∘ vfsequences_on X"
obtains "vfsequence xs" and "⋀i. i ∈⇩∘ 𝒟⇩∘ xs ⟹ xs⦇i⦈ ∈⇩∘ X"
using assms unfolding vfsequences_on_def by auto

subsubsection‹Further properties›

lemma vfsequences_on_vsubset_mono:
assumes "A ⊆⇩∘ B "
shows "vfsequences_on A ⊆⇩∘ vfsequences_on B"
proof(intro vsubsetI vfsequences_onI; elim vfsequences_onE)
fix i xs assume prems: "i ∈⇩∘ 𝒟⇩∘ xs" "⋀i. i ∈⇩∘ 𝒟⇩∘ xs ⟹ xs⦇i⦈ ∈⇩∘ A"
from assms prems(2)[OF prems(1)] show "xs⦇i⦈ ∈⇩∘ B" by auto
qed

text‹\newpage›

end```