# Theory CZH_Sets_MIF

(* Copyright 2021 (C) Manuel Eberl *)

section‹Mutliway If›
theory CZH_Sets_MIF
imports Main
begin

text‹
The code that is presented in this section was originally written
by Manuel Eberl and appeared in a post on the mailing list of Isabelle:
\cite{eberl_syntax_2021}.
The code was ported with minor amendments by the author of this work.
›

abbreviation multi_If :: "bool ⇒ 'a ⇒ 'a ⇒ 'a"
where "multi_If ≡ If"

nonterminal if_clauses and if_clause

syntax
"_if_block" :: "if_clauses ⇒ 'a" ("(1if _)"  10)
"_if_clause"  :: "bool ⇒ 'a ⇒ if_clause" ("(2_ ⇒/ _)" 13)
"_if_final" :: "'a ⇒ if_clauses" ("otherwise ⇒ _")
"_if_cons" :: "[if_clause, if_clauses] ⇒ if_clauses" ("_ /| _" [13, 12] 12)

syntax (ASCII)
"_if_clause" :: "[pttrn, 'a] ⇒ if_clause" ("(2_ =>/ _)" 13)

translations
"_if_block (_if_cons (_if_clause b t) (_if_final e))"
⇌ "CONST multi_If b t e"
"_if_block (_if_cons b (_if_cons c cs))"
⇌ "_if_block (_if_cons b (_if_final (_if_block (_if_cons c cs))))"
"_if_block (_if_final e)" ⇀ "e"

text‹\newpage›

end

# Theory CZH_Utilities

(* Copyright 2021 (C) Mihails Milehins *)

section‹Utilities›
theory CZH_Utilities
imports Main
keywords "lemmas_with" :: thy_decl
begin

text‹
Then command \<^text>‹lemmas_with› is a copy (with minor amendments to formatting)
of the command with the identical name that was introduced by Ondřej Kunčar in
\<^text>‹HOL-Types_To_Sets.Prerequisites›. A copy of the function was produced,
primarily, to avoid the unnecessary dependency of this work on the
axioms associated with the framework ‹Types-To-Sets›.
›

ML‹
val _ =
Outer_Syntax.local_theory'
\<^command_keyword>‹lemmas_with›
"note theorems with (the same) attributes"
(
Parse.attribs --| \<^keyword>‹:› --
Parse_Spec.name_facts --
Parse.for_fixes >>
(
fn (((attrs),facts), fixes) =>
#2 oo Specification.theorems_cmd Thm.theoremK
(map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes
)
)
›

text‹\newpage›

end

# Theory CZH_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

chapter‹Introduction›
theory CZH_Introduction
imports ZFC_in_HOL.ZFC_Typeclasses
begin

section‹Background›

text‹
that will be used for the formalization of
elements of the theory of 1-categories in the object logic
‹ZFC in HOL› (\cite{paulson_zermelo_2019}, also see
\cite{barkaoui_partizan_2006}) of the formal proof assistant
‹Isabelle› \cite{paulson_natural_1986} in future articles.
It is important to note that this chapter serves as
an introduction to the entire development and not merely
its foundational part.

There already exist several formalizations of the foundations of category
theory in Isabelle. In the context of the work presented here, the most relevant
formalizations (listed in the chronological order) are
\cite{okeefe_category_2005}, \cite{katovsky_category_2010} and
\cite{stark_category_2016}.
Arguably, the most well developed and maintained entry is
\cite{stark_category_2016}: it subsumes the majority of the content of
\cite{okeefe_category_2005} and \cite{katovsky_category_2010}.

From the perspective of the methodology that was chosen for the formalization,
this work differs significantly from the aforementioned previous work.
In particular, the categories are modelled as terms of the type \<^typ>‹V›
and no attempt is made to generalize the concept of a category to arbitrary
types. The inspiration for the chosen approach is drawn from
\cite{feferman_set-theoretical_1969},
\cite{sica_doing_2006} and \cite{shulman_set_2008}.

The primary references for this work are
‹Categories for the Working Mathematician› \cite{mac_lane_categories_2010}
by Saunders Mac Lane, ‹Category Theory in Context›
by Emily Riehl \cite{riehl_category_2016} and
‹Categories and Functors› by Bodo Pareigis \cite{bodo_categories_1970}.
The secondary sources of information include the textbooks
as well as several online encyclopedias
(including \cite{noauthor_nlab_nodate},
\cite{noauthor_wikipedia_2001},
\cite{noauthor_proofwiki_nodate}
and \cite{noauthor_encyclopedia_nodate}).
Of course, inspiration was also drawn from the previous formalizations of
category theory in Isabelle.

It is likely that none of the content that is formalized in this work
is original in nature. However, explicit citations
are not provided for many results that were deemed to be trivial.
›

section‹Related and previous work›

text‹
To the best knowledge of the author, this work is the first attempt
to develop a formalization of elements of category theory in the
object logic ZFC in HOL by modelling categories as terms of the type \<^typ>‹V›.
However, it should be noted that the formalization of category theory in
\cite{katovsky_category_2010} largely rested
on the object logic HOL/ZF \cite{barkaoui_partizan_2006}, which is
equiconsistent with the ZFC in HOL \cite{paulson_zermelo_2019}.
Nonetheless, in \cite{katovsky_category_2010}, the objects and arrows
associated with categories were modelled as terms of arbitrary
types. The object logic HOL/ZF was used for the exposition of
the category ‹Set› of all sets and functions between them
and a variety of closely related concepts.
In this sense, the methodology employed in
\cite{katovsky_category_2010} could be seen as a combination of the
methodology employed in this work and the methodology followed in
\cite{okeefe_category_2005} and \cite{stark_category_2016}.
Furthermore, in \cite{chen_hotg_2021},
the authors have experimented with the formalization of category
theory in Higher-Order Tarski-Grothendieck (HOTG)
theory \cite{brown_higher-order_2019} using a methodology that
shares many similarities with the approach that was chosen in this study.

The formalizations of various elements of category theory
in other proof assistants are abundant.
While a survey of such formalizations is outside of the scope of
this work, it is important to note that there exist at least two examples
of the formalization of elements of category theory in a set-theoretic setting
similar to the one that is used in this work.
More specifically, elements of category theory were formalized in
the Tarski-Grothendieck Set Theory in the Mizar proof assistant
\cite{noauthor_association_nodate} (and
published in the associated electronic journal
\cite{grabowski_preface_2014})
and the proof assistant Metamath
\cite{megill_metamath_2019}.
The following references contain some of the
relevant articles in \cite{grabowski_preface_2014}, but the list may not be
exhaustive:
\cite{bylinski_introduction_1990, bylinski_subcategories_1990,
bylinski_opposite_1991, trybulec_natural_1991,
bylinski_category_1991, muzalewski_categories_1991,
trybulec_isomorphisms_1991, muzalewski_category_1991,
muzalewski_category_1991-1, bancerek_comma_1991,
bylinski_products_1991, trybulec_isomorphisms_1992,
bylinski_cartesian_1992, bancerek_categorial_1996,
trybulec_categories_1996, bancerek_indexed_1996,
trybulec_functors_1996, nieszczerzewski_category_1997,
kornilowicz_categories_1997,
kornilowicz_composition_1998,
bancerek_concrete_2001,
kornilowicz_products_2012,
riccardi_object-free_2013,
golinski_coproducts_2013,
riccardi_categorical_2015,
riccardi_exponential_2015}.
›

end

# Theory CZH_Sets_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

chapter‹Set Theory for Category Theory›

section‹Introduction›
theory CZH_Sets_Introduction
imports
CZH_Introduction
CZH_Sets_MIF
CZH_Utilities
Intro_Dest_Elim.IHOL_IDE
Conditional_Simplification.IHOL_CS
ZFC_in_HOL.Cantor_NF
"HOL-Eisbach.Eisbach"
begin

subsection‹Background›

text‹
This chapter presents a formalization of the elements of set theory in
the object logic ‹ZFC in HOL› (\cite{paulson_zermelo_2019}, also see
\cite{barkaoui_partizan_2006})
of the formal proof assistant Isabelle \cite{paulson_natural_1986}.
The emphasis of this work is on the improvement of the convenience of the
formalization of abstract mathematics internalized in the type \<^typ>‹V›.
›

subsection‹References, related and previous work›

text‹
The results that are presented in this chapter cannot be traced to a single
source of information. Nonetheless, the results are not original.
A significant number of these results was carried over (with amendments)
from the main library of Isabelle/HOL \cite{noauthor_isabellehol_2020}.
Other results were inspired by elements of the content of the books
‹Introduction to Axiomatic Set Theory› by G. Takeuti
and W. M. Zaring \cite{takeuti_introduction_1971}, ‹Theory of Sets›
by N. Bourbaki \cite{bourbaki_elements_nodate} and ‹Algebra› by
T. W. Hungerford \cite{hungerford_algebra_2003}.
Furthermore, several online encyclopedias and forums
(including Wikipedia \cite{noauthor_wikipedia_2001},
ProofWiki \cite{noauthor_proofwiki_nodate},
Encyclopedia of Mathematics \cite{noauthor_encyclopedia_nodate},
nLab \cite{noauthor_nlab_nodate} and Mathematics Stack Exchange)
were used consistently throughout the development of this chapter.
Inspiration for the work presented in this chapter has also been drawn
from a similar ongoing project
in the formalization of mathematics in the system
HOTG (Higher Order Tarski-Grothendieck)
\cite{brown_higher-order_2019, chen_hotg_2021}.

It should also be mentioned that the Isabelle/HOL and the Isabelle/ML code
from the main distribution of Isabelle2020 and certain posts on the
mailing list of Isabelle were frequently reused
(with amendments) during the development of this chapter. Some of the
specific examples of such reuse are
\begin{itemize}
\item The adoption of the implementation of
the command @{command lemmas_with} that is available as part of
the framework Types-To-Sets in the main distribution of Isabelle2020.
\item The notation for the multiway-if'' was written
by Manuel Eberl and appeared in a post on the mailing list of Isabelle:
\cite{eberl_syntax_2021}.
\end{itemize}
›

hide_const (open) list.set Sum subset

lemmas ord_of_nat_zero = ord_of_nat.simps(1)

subsection‹Notation›

abbreviation (input) qm (‹(_ ? _ : _)› [0, 0, 10] 10)
where "C ? A : B ≡ if C then A else B"
abbreviation (input) if2 where "if2 a b ≡ (λi. (i = 0 ? a : b))"

subsection‹Further foundational results›

lemma theD:
assumes "∃!x. P x" and "x = (THE x. P x)"
shows "P x" and "P y ⟹ x = y"
using assms by (metis theI)+

lemmas [intro] = bij_betw_imageI

lemma bij_betwE[elim]:
assumes "bij_betw f A B" and "⟦ inj_on f A; f  A = B ⟧ ⟹ P"
shows P
using assms unfolding bij_betw_def by auto

lemma bij_betwD[dest]:
assumes "bij_betw f A B"
shows "inj_on f A" and "f  A = B"
using assms by auto

text‹\newpage›

end

# Theory CZH_Sets_Sets

(* Copyright 2021 (C) Mihails Milehins *)

section‹Further set algebra and other miscellaneous results›
theory CZH_Sets_Sets
imports CZH_Sets_Introduction
begin

subsection‹Background›

text‹
This section presents further set algebra and various elementary properties
of sets.

Many of the results that are presented in this section
were carried over (with amendments) from the theories \<^text>‹Set›
and \<^text>‹Complete_Lattices› in the main library.
›

declare elts_sup_iff[simp del]

subsection‹Further notation›

subsubsection‹Set membership›

abbreviation vmember :: "V ⇒ V ⇒ bool" ("(_/ ∈⇩∘ _)" [51, 51] 50)
where "vmember x A ≡ (x ∈ elts A)"
notation vmember ("'(∈⇩∘')")
and vmember ("(_/ ∈⇩∘ _)" [51, 51] 50)

abbreviation not_vmember :: "V ⇒ V ⇒ bool" ("(_/ ∉⇩∘ _)" [51, 51] 50)
where "not_vmember x A ≡ (x ∉ elts A)"
notation
not_vmember ("'(∉⇩∘')") and
not_vmember ("(_/ ∉⇩∘ _)" [51, 51] 50)

subsubsection‹Subsets›

abbreviation vsubset :: "V ⇒ V ⇒ bool"
where "vsubset ≡ less"
abbreviation vsubset_eq :: "V ⇒ V ⇒ bool"
where "vsubset_eq ≡ less_eq"

notation vsubset ("'(⊂⇩∘')")
and vsubset ("(_/ ⊂⇩∘ _)" [51, 51] 50)
and vsubset_eq ("'(⊆⇩∘')")
and vsubset_eq ("(_/ ⊆⇩∘ _)" [51, 51] 50)

subsubsection‹Ball›

syntax
"_VBall" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∀(_/∈⇩∘_)./ _)" [0, 0, 10] 10)
"_VBex" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∃(_/∈⇩∘_)./ _)" [0, 0, 10] 10)
"_VBex1" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∃!(_/∈⇩∘_)./ _)" [0, 0, 10] 10)

translations
"∀x∈⇩∘A. P" ⇌ "CONST Ball (CONST elts A) (λx. P)"
"∃x∈⇩∘A. P" ⇌ "CONST Bex (CONST elts A) (λx. P)"
"∃!x∈⇩∘A. P" ⇀ "∃!x. x ∈⇩∘ A ∧ P"

subsubsection‹‹VLambda››

text‹The following notation was adapted from \cite{paulson_hereditarily_2013}.›

syntax "_vlam" :: "[pttrn, V, V] ⇒ V" (‹(3λ_∈⇩∘_./ _)› 10)
translations "λx∈⇩∘A. f" ⇌ "CONST VLambda A (λx. f)"

subsubsection‹Intersection and union›

abbreviation vintersection :: "V ⇒ V ⇒ V" (infixl "∩⇩∘" 70)
where "(∩⇩∘) ≡ (⊓)"
notation vintersection (infixl "∩⇩∘" 70)

abbreviation vunion :: "V ⇒ V ⇒ V"  (infixl "∪⇩∘" 65)
where "vunion ≡ sup"
notation vunion (infixl "∪⇩∘" 65)

abbreviation VInter :: "V ⇒ V" (‹⋂⇩∘›)
where "⋂⇩∘ A ≡ ⨅ (elts A)"
notation VInter (‹⋂⇩∘›)

abbreviation VUnion :: "V ⇒ V" (‹⋃⇩∘›)
where "⋃⇩∘A ≡ ⨆ (elts A)"
notation VUnion (‹⋃⇩∘›)

subsubsection‹Miscellaneous›

notation app (‹_⦇_⦈› [999, 50] 999)
notation vtimes (infixr "×⇩∘" 80)

subsection‹Elementary results.›

lemma vempty_nin[simp]: "a ∉⇩∘ 0" by simp

lemma vemptyE:
assumes "A ≠ 0"
obtains x where "x ∈⇩∘ A"

lemma in_set_CollectI:
assumes "P x" and "small {x. P x}"
shows "x ∈⇩∘ set {x. P x}"
using assms by simp

lemma small_setcompr2:
assumes "small {f x y | x y. P x y}" and "a ∈⇩∘ set {f x y | x y. P x y}"
obtains x' y' where "a = f x' y'" and "P x' y'"
using assms by auto

lemma in_small_setI:
assumes "small A" and "x ∈ A"
shows "x ∈⇩∘ set A"
using assms by simp

lemma in_small_setD:
assumes "x ∈⇩∘ set A" and "small A"
shows "x ∈ A"
using assms by simp

lemma in_small_setE:
assumes "a ∈⇩∘ set A" and "small A"
obtains "a ∈ A"
using assms by auto

lemma small_set_vsubset:
assumes "small A" and "A ⊆ elts B"
shows "set A ⊆⇩∘ B"
using assms by auto

lemma some_in_set_if_set_neq_vempty[simp]:
assumes "A ≠ 0"
shows "(SOME x. x ∈⇩∘ A) ∈⇩∘ A"
by (meson assms someI_ex vemptyE)

lemma small_vsubset_set[intro, simp]:
assumes "small B" and "A ⊆ B"
shows "set A ⊆⇩∘ set B"
using assms by (auto simp: subset_iff_less_eq_V)

lemma vset_neq_1:
assumes "b ∉⇩∘ A" and "a ∈⇩∘ A"
shows "b ≠ a"
using assms by auto

lemma vset_neq_2:
assumes "b ∈⇩∘ A" and "a ∉⇩∘ A"
shows "b ≠ a"
using assms by auto

lemma nin_vinsertI:
assumes "a ≠ b" and "a ∉⇩∘ A"
shows "a ∉⇩∘ vinsert b A"
using assms by clarsimp

lemma vsubset_if_subset:
assumes "elts A ⊆ elts B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma small_set_comprehension[simp]: "small {A i | i. i ∈⇩∘ I}"
proof(rule smaller_than_small)
show "small (A  elts I)" by auto
qed auto

subsection‹‹VBall››

lemma vball_cong:
assumes "A = B" and "⋀x. x ∈⇩∘ B ⟹ P x ⟷ Q x"
shows "(∀x∈⇩∘A. P x) ⟷ (∀x∈⇩∘B. Q x)"

lemma vball_cong_simp[cong]:
assumes "A = B" and "⋀x. x ∈⇩∘ B =simp=> P x ⟷ Q x "
shows "(∀x∈⇩∘A. P x) ⟷ (∀x∈⇩∘B. Q x)"
using assms by (simp add: simp_implies_def)

subsection‹‹VBex››

lemma vbex_cong:
assumes "A = B" and  "⋀x. x ∈⇩∘ B ⟹ P x ⟷ Q x"
shows "(∃x∈⇩∘A. P x) ⟷ (∃x∈⇩∘B. Q x)"
using assms by (simp cong: conj_cong)

lemma vbex_cong_simp[cong]:
assumes "A = B" and "⋀x. x ∈⇩∘ B =simp=> P x ⟷ Q x "
shows "(∃x∈⇩∘A. P x) ⟷ (∃x∈⇩∘B. Q x)"
using assms by (simp add:  simp_implies_def)

subsection‹Subset›

text‹Rules.›

lemma vsubset_antisym:
assumes "A ⊆⇩∘ B" and "B ⊆⇩∘ A"
shows "A = B"
using assms by simp

lemma vsubsetI:
assumes "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vpsubsetI:
assumes "A ⊆⇩∘ B" and "x ∉⇩∘ A" and "x ∈⇩∘ B"
shows "A ⊂⇩∘ B"
using assms unfolding less_V_def by auto

lemma vsubsetD:
assumes "A ⊆⇩∘ B"
shows "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B"
using assms by auto

lemma vsubsetE:
assumes "A ⊆⇩∘ B" and "(⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B) ⟹ P"
shows P
using assms by auto

lemma vpsubsetE:
assumes "A ⊂⇩∘ B"
obtains x where "A ⊆⇩∘ B" and "x ∉⇩∘ A" and "x ∈⇩∘ B"
using assms unfolding less_V_def by (meson V_equalityI vsubsetE)

lemma vsubset_iff: "A ⊆⇩∘ B ⟷ (∀t. t ∈⇩∘ A ⟶ t ∈⇩∘ B)" by blast

text‹Elementary properties.›

lemma vsubset_eq: "A ⊆⇩∘ B ⟷ (∀x∈⇩∘A. x ∈⇩∘ B)" by auto

lemma vsubset_transitive[intro]:
assumes "A ⊆⇩∘ B" and "B ⊆⇩∘ C"
shows "A ⊆⇩∘ C"
using assms by simp

lemma vsubset_reflexive: "A ⊆⇩∘ A" by simp

text‹Set operations.›

lemma vsubset_vempty: "0 ⊆⇩∘ A" by simp

lemma vsubset_vsingleton_left: "set {a} ⊆⇩∘ A ⟷ a ∈⇩∘ A" by auto

lemmas vsubset_vsingleton_leftD[dest] = vsubset_vsingleton_left[THEN iffD1]
and vsubset_vsingleton_leftI[intro] = vsubset_vsingleton_left[THEN iffD2]

lemma vsubset_vsingleton_right: "A ⊆⇩∘ set {a} ⟷ A = set {a} ∨ A = 0"
by (auto intro!: vsubset_antisym)

lemmas vsubset_vsingleton_rightD[dest] = vsubset_vsingleton_right[THEN iffD1]
and vsubset_vsingleton_rightI[intro] = vsubset_vsingleton_right[THEN iffD2]

lemma vsubset_vdoubleton_leftD[dest]:
assumes "set {a, b} ⊆⇩∘ A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A"
using assms by auto

lemma vsubset_vdoubleton_leftI[intro]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "set {a, b} ⊆⇩∘ A"
using assms by auto

lemma vsubset_vinsert_leftD[dest]:
assumes "vinsert a A ⊆⇩∘ B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vsubset_vinsert_leftI[intro]:
assumes "A ⊆⇩∘ B" and "a ∈⇩∘ B"
shows "vinsert a A ⊆⇩∘ B"
using assms by auto

lemma vsubset_vinsert_vinsertI[intro]:
assumes "A ⊆⇩∘ vinsert b B"
shows "vinsert b A ⊆⇩∘ vinsert b B"
using assms by auto

lemma vsubset_vinsert_rightI[intro]:
assumes "A ⊆⇩∘ B"
shows "A ⊆⇩∘ vinsert b B"
using assms by auto

lemmas vsubset_VPow = VPow_le_VPow_iff

lemmas vsubset_VPowD = vsubset_VPow[THEN iffD1]
and vsubset_VPowI = vsubset_VPow[THEN iffD2]

text‹Special properties.›

assumes "A ⊆⇩∘ B" and "c ∉⇩∘ B"
shows "c ∉⇩∘ A"
using assms by auto

subsection‹Equality›

text‹Rules.›

lemma vequalityD1:
assumes "A = B"
shows "A ⊆⇩∘ B"
using assms by simp

lemma vequalityD2:
assumes "A = B"
shows "B ⊆⇩∘ A"
using assms by simp

lemma vequalityE:
assumes "A = B" and "⟦ A ⊆⇩∘ B; B ⊆⇩∘ A ⟧ ⟹ P"
shows P
using assms by simp

lemma vequalityCE[elim]:
assumes "A = B" and "⟦ c ∈⇩∘ A; c ∈⇩∘ B ⟧ ⟹ P" and "⟦ c ∉⇩∘ A; c ∉⇩∘ B ⟧ ⟹ P"
shows P
using assms by auto

subsection‹Binary intersection›

lemma vintersection_def: "A ∩⇩∘ B = set {x. x ∈⇩∘ A ∧ x ∈⇩∘ B}"
by (metis Int_def inf_V_def)

lemma small_vintersection_set[simp]: "small {x. x ∈⇩∘ A ∧ x ∈⇩∘ B}"
by (rule down[of _ A]) auto

text‹Rules.›

lemma vintersection_iff[simp]: "x ∈⇩∘ A ∩⇩∘ B ⟷ x ∈⇩∘ A ∧ x ∈⇩∘ B"
unfolding vintersection_def by simp

lemma vintersectionI[intro!]:
assumes "x ∈⇩∘ A" and "x ∈⇩∘ B"
shows "x ∈⇩∘ A ∩⇩∘ B"
using assms by simp

lemma vintersectionD1[dest]:
assumes "x ∈⇩∘ A ∩⇩∘ B"
shows "x ∈⇩∘ A"
using assms by simp

lemma vintersectionD2[dest]:
assumes "x ∈⇩∘ A ∩⇩∘ B"
shows "x ∈⇩∘ B"
using assms by simp

lemma vintersectionE[elim!]:
assumes "x ∈⇩∘ A ∩⇩∘ B" and "x ∈⇩∘ A ⟹ x ∈⇩∘ B ⟹ P"
shows P
using assms by simp

text‹Elementary properties.›

lemma vintersection_intersection: "A ∩⇩∘ B = set (elts A ∩ elts B)"
unfolding inf_V_def by simp

lemma vintersection_assoc: "A ∩⇩∘ (B ∩⇩∘ C) = (A ∩⇩∘ B) ∩⇩∘ C" by auto

lemma vintersection_commutativity: "A ∩⇩∘ B = B ∩⇩∘ A" by auto

text‹Previous set operations.›

lemma vsubset_vintersection_right: "A ⊆⇩∘ (B ∩⇩∘ C) = (A ⊆⇩∘ B ∧ A ⊆⇩∘ C)"
by clarsimp

lemma vsubset_vintersection_rightD[dest]:
assumes "A ⊆⇩∘ (B ∩⇩∘ C)"
shows "A ⊆⇩∘ B" and "A ⊆⇩∘ C"
using assms by auto

lemma vsubset_vintersection_rightI[intro]:
assumes "A ⊆⇩∘ B" and "A ⊆⇩∘ C"
shows "A ⊆⇩∘ (B ∩⇩∘ C)"
using assms by auto

text‹Set operations.›

lemma vintersection_vempty: "0 ⊆⇩∘ A" by simp

lemma vintersection_vsingleton: "a ∈⇩∘ set {a}" by simp

lemma vintersection_vdoubleton: "a ∈⇩∘ set {a, b}" and "b ∈⇩∘ set {a, b}"
by simp_all

lemma vintersection_VPow[simp]: "VPow (A ∩⇩∘ B) = VPow A ∩⇩∘ VPow B" by auto

text‹Special properties.›

lemma vintersection_function_mono:
assumes "mono f"
shows "f (A ∩⇩∘ B) ⊆⇩∘ f A ∩⇩∘ f B"
using assms by (fact mono_inf)

subsection‹Binary union›

lemma small_vunion_set: "small {x. x ∈⇩∘ A ∨ x ∈⇩∘ B}"
by (rule down[of _ ‹A ∪⇩∘ B›]) (auto simp: elts_sup_iff)

text‹Rules.›

lemma vunion_def: "A ∪⇩∘ B = set {x. x ∈⇩∘ A ∨ x ∈⇩∘ B}"
unfolding Un_def sup_V_def by simp

lemma vunion_iff[simp]: "x ∈⇩∘ A ∪⇩∘ B ⟷ x ∈⇩∘ A ∨ x ∈⇩∘ B"

lemma vunionI1:
assumes "a ∈⇩∘ A"
shows "a ∈⇩∘ A ∪⇩∘ B"
using assms by simp

lemma vunionI2:
assumes "a ∈⇩∘ B"
shows "a ∈⇩∘ A ∪⇩∘ B"
using assms by simp

lemma vunionCI[intro!]:
assumes "x ∉⇩∘ B ⟹ x ∈⇩∘ A"
shows "x ∈⇩∘ A ∪⇩∘ B"
using assms by clarsimp

lemma vunionE[elim!]:
assumes "x ∈⇩∘ A ∪⇩∘ B" and "x ∈⇩∘ A ⟹ P" and "x ∈⇩∘ B ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma vunion_union: "A ∪⇩∘ B = set (elts A ∪ elts B)" by auto

lemma vunion_assoc: "A ∪⇩∘ (B ∪⇩∘ C) = (A ∪⇩∘ B) ∪⇩∘ C" by auto

lemma vunion_comm: "A ∪⇩∘ B = B ∪⇩∘ A" by auto

text‹Previous set operations.›

lemma vsubset_vunion_left: "(A ∪⇩∘ B) ⊆⇩∘ C ⟷ (A ⊆⇩∘ C ∧ B ⊆⇩∘ C)" by simp

lemma vsubset_vunion_leftD[dest]:
assumes "(A ∪⇩∘ B) ⊆⇩∘ C"
shows "A ⊆⇩∘ C" and "B ⊆⇩∘ C"
using assms by auto

lemma vsubset_vunion_leftI[intro]:
assumes "A ⊆⇩∘ C" and "B ⊆⇩∘ C"
shows "(A ∪⇩∘ B) ⊆⇩∘ C"
using assms by auto

lemma vintersection_vunion_left: "(A ∪⇩∘ B) ∩⇩∘ C = (A ∩⇩∘ C) ∪⇩∘ (B ∩⇩∘ C)"
by auto

lemma vintersection_vunion_right: "A ∩⇩∘ (B ∪⇩∘ C) = (A ∩⇩∘ B) ∪⇩∘ (A ∩⇩∘ C)"
by auto

text‹Set operations.›

lemmas vunion_vempty_left = sup_V_0_left
and vunion_vempty_right = sup_V_0_right

lemma vunion_vsingleton[simp]: "set {a} ∪⇩∘ A = vinsert a A" by auto

lemma vunion_vdoubleton[simp]: "set {a, b} ∪⇩∘ A = vinsert a (vinsert b A)"
by auto

lemma vunion_vinsert_commutativity_left:
"(vinsert a A) ∪⇩∘ B = A ∪⇩∘ (vinsert a B)"
by auto

lemma vunion_vinsert_commutativity_right:
"A ∪⇩∘ (vinsert a B) = (vinsert a A) ∪⇩∘ B"
by auto

lemma vinsert_def: "vinsert y B = set {x. x = y} ∪⇩∘ B" by auto

lemma vunion_vinsert_left: "(vinsert a A) ∪⇩∘ B = vinsert a (A ∪⇩∘ B)" by auto

lemma vunion_vinsert_right: "A ∪⇩∘ (vinsert a B) = vinsert a (A ∪⇩∘ B)" by auto

text‹Special properties.›

lemma vunion_fun_mono:
assumes "mono f"
shows "f A ∪⇩∘ f B ⊆⇩∘ f (A ∪⇩∘ B)"
using assms by (fact mono_sup)

subsection‹Set difference›

definition vdiff :: "V ⇒ V ⇒ V" (infixl ‹-⇩∘› 65)
where "A -⇩∘ B = set {x. x ∈⇩∘ A ∧ x ∉⇩∘ B}"
notation vdiff (infixl "-⇩∘" 65)

lemma small_set_vdiff[simp]: "small {x. x ∈⇩∘ A ∧ x ∉⇩∘ B}"
by (rule down[of _ A]) simp

text‹Rules.›

lemma vdiff_iff[simp]: "x ∈⇩∘ A -⇩∘ B ⟷ x ∈⇩∘ A ∧ x ∉⇩∘ B"
unfolding vdiff_def by simp

lemma vdiffI[intro!]:
assumes "x ∈⇩∘ A" and "x ∉⇩∘ B"
shows "x ∈⇩∘ A -⇩∘ B"
using assms by simp

lemma vdiffD1:
assumes "x ∈⇩∘ A -⇩∘ B"
shows "x ∈⇩∘ A"
using assms by simp

lemma vdiffD2:
assumes "x ∈⇩∘ A -⇩∘ B" and "x ∈⇩∘ B"
shows P
using assms by simp

lemma vdiffE[elim!]:
assumes "x ∈⇩∘ A -⇩∘ B" and "⟦ x ∈⇩∘ A; x ∉⇩∘ B ⟧ ⟹ P"
shows P
using assms by simp

text‹Previous set operations.›

lemma vsubset_vdiff:
assumes "A ⊆⇩∘ B -⇩∘ C"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vinsert_vdiff_nin[simp]:
assumes "a ∉⇩∘ B"
shows "vinsert a (A -⇩∘ B) = vinsert a A -⇩∘ B"
using assms by auto

text‹Set operations.›

lemma vdiff_vempty_left[simp]: "0 -⇩∘ A = 0" by auto

lemma vdiff_vempty_right[simp]: "A -⇩∘ 0 = A" by auto

lemma vdiff_vsingleton_vinsert[simp]: "set {a} -⇩∘ vinsert a A = 0" by auto

lemma vdiff_vsingleton_in[simp]:
assumes "a ∈⇩∘ A"
shows "set {a} -⇩∘ A = 0"
using assms by auto

lemma vdiff_vsingleton_nin[simp]:
assumes "a ∉⇩∘ A"
shows "set {a} -⇩∘ A = set {a}"
using assms by auto

lemma vdiff_vinsert_vsingleton[simp]: "vinsert a A -⇩∘ set {a} = A -⇩∘ set {a}"
by auto

lemma vdiff_vsingleton[simp]:
assumes "a ∉⇩∘ A"
shows "A -⇩∘ set {a} = A"
using assms by auto

lemma vdiff_vsubset:
assumes "A ⊆⇩∘ B" and "D ⊆⇩∘ C"
shows "A -⇩∘ C ⊆⇩∘ B -⇩∘ D"
using assms by auto

lemma vdiff_vinsert_left_in[simp]:
assumes "a ∈⇩∘ B"
shows "(vinsert a A) -⇩∘ B = A -⇩∘ B"
using assms by auto

lemma vdiff_vinsert_left_nin:
assumes "a ∉⇩∘ B"
shows "(vinsert a A) -⇩∘ B = vinsert a (A -⇩∘ B)"
using assms by auto

lemma vdiff_vinsert_right_in: "A -⇩∘ (vinsert a B) = A -⇩∘ B -⇩∘ set {a}" by auto

lemma vdiff_vinsert_right_nin[simp]:
assumes "a ∉⇩∘ A"
shows "A -⇩∘ (vinsert a B) = A -⇩∘ B"
using assms by auto

lemma vdiff_vintersection_left: "(A ∩⇩∘ B) -⇩∘ C = (A -⇩∘ C) ∩⇩∘ (B -⇩∘ C)" by auto

lemma vdiff_vunion_left: "(A ∪⇩∘ B) -⇩∘ C = (A -⇩∘ C) ∪⇩∘ (B -⇩∘ C)" by auto

text‹Special properties.›

lemma complement_vsubset: "I -⇩∘ J ⊆⇩∘ I" by auto

lemma vintersection_complement: "(I -⇩∘ J) ∩⇩∘ J = 0" by auto

lemma vunion_complement:
assumes "J ⊆⇩∘ I"
shows "I -⇩∘ J ∪⇩∘ J = I"
using assms by auto

subsection‹Augmenting a set with an element›

lemma vinsert_compr: "vinsert y A = set {x. x = y ∨ x ∈⇩∘ A}"
unfolding vunion_def vinsert_def by simp_all

text‹Rules.›

lemma vinsert_iff[simp]: "x ∈⇩∘ vinsert y A ⟷ x = y ∨ x ∈⇩∘ A" by simp

lemma vinsertI1: "x ∈⇩∘ vinsert x A" by simp

lemma vinsertI2:
assumes "x ∈⇩∘ A"
shows "x ∈⇩∘ vinsert y A"
using assms by simp

lemma vinsertE1[elim!]:
assumes "x ∈⇩∘ vinsert y A" and "x = y ⟹ P" and "x ∈⇩∘ A ⟹ P"
shows P
using assms unfolding vinsert_def by auto

lemma vinsertCI[intro!]:
assumes "x ∉⇩∘ A ⟹ x = y"
shows "x ∈⇩∘ vinsert y A"
using assms by clarsimp

text‹Elementary properties.›

lemma vinsert_insert: "vinsert a A = set (insert a (elts A))" by auto

lemma vinsert_commutativity: "vinsert a (vinsert b C) = vinsert b (vinsert a C)"
by auto

lemma vinsert_ident:
assumes "x ∉⇩∘ A" and "x ∉⇩∘ B"
shows "vinsert x A = vinsert x B ⟷ A = B"
using assms by force

lemmas vinsert_identD[dest] = vinsert_ident[THEN iffD1, rotated 2]
and vinsert_identI[intro] = vinsert_ident[THEN iffD2]

text‹Set operations.›

lemma vinsert_vempty: "vinsert a 0 = set {a}" by auto

lemma vinsert_vsingleton: "vinsert a (set {b}) = set {a, b}" by auto

lemma vinsert_vdoubleton: "vinsert a (set {b, c}) = set {a, b, c}" by auto

lemma vinsert_vinsert: "vinsert a (vinsert b C) = set {a, b} ∪⇩∘ C" by auto

lemma vinsert_vunion_left: "vinsert a (A ∪⇩∘ B) = vinsert a A ∪⇩∘ B" by auto

lemma vinsert_vunion_right: "vinsert a (A ∪⇩∘ B) = A ∪⇩∘ vinsert a B" by auto

lemma vinsert_vintersection: "vinsert a (A ∩⇩∘ B) = vinsert a A ∩⇩∘ vinsert a B"
by auto

text‹Special properties.›

lemma vinsert_set_insert_empty_anyI:
assumes "P (vinsert a 0)"
shows "P (set (insert a {}))"
using assms by (simp add: vinsert_def)

lemma vinsert_set_insert_anyI:
assumes "small B" and "P (vinsert a (set (insert b B)))"
shows "P (set (insert a (insert b B)))"
using assms by (simp add: ZFC_in_HOL.vinsert_def)

lemma vinsert_set_insert_eq:
assumes "small B"
shows "set (insert a (insert b B)) = vinsert a (set (insert b B))"
using assms by (simp add: ZFC_in_HOL.vinsert_def)

lemma vsubset_vinsert:
"A ⊆⇩∘ vinsert x B ⟷ (if x ∈⇩∘ A then A -⇩∘ set {x} ⊆⇩∘ B else A ⊆⇩∘ B)"
by auto

lemma vinsert_obtain_ne:
assumes "A ≠ 0"
obtains a A' where "A = vinsert a A'" and "a ∉⇩∘ A'"
proof-
from assms mem_not_refl obtain a where "a ∈⇩∘ A"
by (auto intro!: vsubset_antisym)
with ‹a ∈⇩∘ A› have "A = vinsert a (A -⇩∘ set {a})" by auto
then show ?thesis using that by auto
qed

subsection‹Power set›

text‹Rules.›

lemma VPowI:
assumes "A ⊆⇩∘ B"
shows "A ∈⇩∘ VPow B"
using assms by simp

lemma VPowD:
assumes "A ∈⇩∘ VPow B"
shows "A ⊆⇩∘ B"
using assms by (simp add: Pow_def)

lemma VPowE[elim]:
assumes "A ∈⇩∘ VPow B" and "A ⊆⇩∘ B ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma VPow_bottom: "0 ∈⇩∘ VPow B" by simp

lemma VPow_top: "A ∈⇩∘ VPow A" by simp

text‹Set operations.›

lemma VPow_vempty[simp]: "VPow 0 = set {0}" by auto

lemma VPow_vsingleton[simp]: "VPow (set {a}) = set {0, set {a}}"
by (rule vsubset_antisym; rule vsubsetI) auto

lemma VPow_not_vempty: "VPow A ≠ 0" by auto

lemma VPow_mono:
assumes "A ⊆⇩∘ B"
shows "VPow A ⊆⇩∘ VPow B"
using assms by simp

lemma VPow_vunion_subset: "VPow A ∪⇩∘ VPow B ⊆⇩∘ VPow (A ∪⇩∘ B)" by simp

subsection‹Singletons, using insert›

text‹Rules.›

lemma vsingletonI[intro!]: "x ∈⇩∘ set {x}" by auto

lemma vsingletonD[dest!]:
assumes "y ∈⇩∘ set {x}"
shows "y = x"
using assms by auto

lemma vsingleton_iff: "y ∈⇩∘ set {x} ⟷ y = x" by simp

text‹Previous set operations.›

lemma VPow_vdoubleton[simp]:
"VPow (set {a, b}) = set {0, set {a}, set {b}, set {a, b}}"
by (intro vsubset_antisym vsubsetI)
(auto intro!: vsubset_antisym simp: vinsert_set_insert_eq)

lemma vsubset_vinsertI:
assumes "A -⇩∘ set {x} ⊆⇩∘ B"
shows "A ⊆⇩∘ vinsert x B"
using assms by auto

text‹Special properties.›

lemma vsingleton_inject:
assumes "set {x} = set {y}"
shows "x = y"
using assms by simp

lemma vsingleton_insert_inj_eq[iff]:
"set {y} = vinsert x A ⟷ x = y ∧ A ⊆⇩∘ set {y}"
by auto

lemma vsingleton_insert_inj_eq'[iff]:
"vinsert x A = set {y} ⟷ x = y ∧ A ⊆⇩∘ set {y}"
by auto

lemma vsubset_vsingletonD:
assumes "A ⊆⇩∘ set {x}"
shows "A = 0 ∨ A = set {x}"
using assms by auto

lemma vsubset_vsingleton_iff: "a ⊆⇩∘ set {x} ⟷ a = 0 ∨ a = set {x}" by auto

lemma vsubset_vdiff_vinsert: "A ⊆⇩∘ B -⇩∘ vinsert x C ⟷ A ⊆⇩∘ B -⇩∘ C ∧ x ∉⇩∘ A"
by auto

lemma vunion_vsingleton_iff:
"A ∪⇩∘ B = set {x} ⟷
A = 0 ∧ B = set {x} ∨ A = set {x} ∧ B = 0 ∨ A = set {x} ∧ B = set {x}"
by
(
metis
vsubset_vsingletonD inf_sup_ord(4) sup.idem sup_V_0_right sup_commute
)

lemma vsingleton_Un_iff:
"set {x} = A ∪⇩∘ B ⟷
A = 0 ∧ B = set {x} ∨ A = set {x} ∧ B = 0 ∨ A = set {x} ∧ B = set {x}"
by (metis vunion_vsingleton_iff sup_V_0_left sup_V_0_right sup_idem)

lemma VPow_vsingleton_iff[simp]: "VPow X = set {Y} ⟷ X = 0 ∧ Y = 0"
by (auto intro!: vsubset_antisym)

subsection‹Intersection of elements›

lemma small_VInter[simp]:
assumes "A ≠ 0"
shows "small {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}"
by (metis (no_types, lifting) assms down eq0_iff mem_Collect_eq subsetI)

lemma VInter_def: "⋂⇩∘ A = (if A = 0 then 0 else set {a. ∀x ∈⇩∘ A. a ∈⇩∘ x})"
proof(cases ‹A = 0›)
case True show ?thesis unfolding True Inf_V_def by simp
next
case False
from False have "(⋂ (elts  elts A)) = {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}" by auto
with False show ?thesis unfolding Inf_V_def by auto
qed

text‹Rules.›

lemma VInter_iff[simp]:
assumes [simp]: "A ≠ 0"
shows "a ∈⇩∘ ⋂⇩∘ A ⟷ (∀x∈⇩∘A. a ∈⇩∘ x)"
unfolding VInter_def by auto

lemma VInterI[intro]:
assumes "A ≠ 0" and "⋀x. x ∈⇩∘ A ⟹ a ∈⇩∘ x"
shows "a ∈⇩∘ ⋂⇩∘ A"
using assms by auto

lemma VInter0I[intro]:
assumes "A = 0"
shows "⋂⇩∘ A = 0"
using assms unfolding VInter_def by simp

lemma VInterD[dest]:
assumes "a ∈⇩∘ ⋂⇩∘ A" and "x ∈⇩∘ A"
shows "a ∈⇩∘ x"
using assms by (cases ‹A = 0›) auto

lemma VInterE1[elim]:
assumes "a ∈⇩∘ ⋂⇩∘ A" and "x ∉⇩∘ A ⟹ R" and "a ∈⇩∘ x ⟹ R"
shows R
using assms elts_0 unfolding Inter_eq by blast

lemma VInterE2[elim]:
assumes "a ∈⇩∘ ⋂⇩∘ A"
obtains x where "a ∈⇩∘ x" and "x ∈⇩∘ A"
proof(cases ‹A = 0›)
show "(⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ thesis) ⟹ A = 0 ⟹ thesis"
using assms unfolding Inf_V_def by auto
show "(⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ thesis) ⟹ A ≠ 0 ⟹ thesis"
using assms by (meson assms VInterE1 that trad_foundation)
qed

lemma VInterE3: (*not elim*)
assumes "a ∈⇩∘ ⋂⇩∘ A" and "(⋀y. y ∈⇩∘ A ⟹ a ∈⇩∘ y) ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma VInter_Inter: "⋂⇩∘ A = set (⋂ (elts  (elts A)))"

lemma VInter_eq:
assumes [simp]: "A ≠ 0"
shows "⋂⇩∘ A = set {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}"
unfolding VInter_def by auto

text‹Set operations.›

lemma VInter_vempty[simp]: "⋂⇩∘ 0 = 0" using VInter0I by auto

lemma VInf_vempty[simp]: "⨅{} = (0::V)" by (simp add: Inf_V_def)

lemma VInter_vdoubleton: "⋂⇩∘ (set {a, b}) = a ∩⇩∘ b"
proof(intro vsubset_antisym vsubsetI)
show "x ∈⇩∘ ⋂⇩∘ (set {a, b}) ⟹ x ∈⇩∘ a ∩⇩∘ b" for x by (elim VInterE3) auto
show "x ∈⇩∘ a ∩⇩∘ b ⟹ x ∈⇩∘ ⋂⇩∘ (set {a, b})" for x by (intro VInterI) force+
qed

lemma VInter_antimono:
assumes "B ≠ 0" and "B ⊆⇩∘ A"
shows "⋂⇩∘ A ⊆⇩∘ ⋂⇩∘ B"
using assms by blast

lemma VInter_vsubset:
assumes "⋀x. x ∈⇩∘ A ⟹ x ⊆⇩∘ B" and "A ≠ 0"
shows "⋂⇩∘ A ⊆⇩∘ B"
using assms by auto

lemma VInter_vinsert:
assumes "A ≠ 0"
shows "⋂⇩∘ (vinsert a A) = a ∩⇩∘ ⋂⇩∘ A"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vunion:
assumes "A ≠ 0" and "B ≠ 0"
shows "⋂⇩∘(A ∪⇩∘ B) = ⋂⇩∘A ∩⇩∘ ⋂⇩∘B"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vintersection:
assumes "A ∩⇩∘ B ≠ 0"
shows "⋂⇩∘ A ∪⇩∘ ⋂⇩∘ B ⊆⇩∘ ⋂⇩∘ (A ∩⇩∘ B)"
using assms by auto

lemma VInter_VPow: "⋂⇩∘ (VPow A) ⊆⇩∘ VPow (⋂⇩∘ A)" by auto

text‹Elementary properties.›

lemma VInter_lower:
assumes "x ∈⇩∘ A"
shows "⋂⇩∘ A ⊆⇩∘ x"
using assms by auto

lemma VInter_greatest:
assumes "A ≠ 0" and "⋀x. x ∈⇩∘ A ⟹ B ⊆⇩∘ x"
shows "B ⊆⇩∘ ⋂⇩∘ A"
using assms by auto

subsection‹Union of elements›

lemma Union_eq_VUnion: "⋃(elts  elts A) = {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}" by auto

lemma small_VUnion[simp]: "small {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}"
by (fold Union_eq_VUnion) simp

lemma VUnion_def: "⋃⇩∘A = set {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}"
unfolding Sup_V_def by auto

text‹Rules.›

lemma VUnion_iff[simp]: "A ∈⇩∘ ⋃⇩∘C ⟷ (∃x∈⇩∘C. A ∈⇩∘ x)" by auto

lemma VUnionI[intro]:
assumes "x ∈⇩∘ A" and "a ∈⇩∘ x"
shows "a ∈⇩∘ ⋃⇩∘A"
using assms by auto

lemma VUnionE[elim!]:
assumes "a ∈⇩∘ ⋃⇩∘A" and "⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ R"
shows R
using assms by clarsimp

text‹Elementary properties.›

lemma VUnion_Union: "⋃⇩∘A = set (⋃ (elts  (elts A)))"

text‹Set operations.›

lemma VUnion_vempty[simp]: "⋃⇩∘0 = 0" by simp

lemma VUnion_vsingleton[simp]: "⋃⇩∘(set {a}) = a" by simp

lemma VUnion_vdoubleton[simp]: "⋃⇩∘(set {a, b}) = a ∪⇩∘ b" by auto

lemma VUnion_mono:
assumes "A ⊆⇩∘ B"
shows "⋃⇩∘A ⊆⇩∘ ⋃⇩∘B"
using assms by auto

lemma VUnion_vinsert: "⋃⇩∘(vinsert x A) = x ∪⇩∘ ⋃⇩∘A" by auto

lemma VUnion_vintersection: "⋃⇩∘(A ∩⇩∘ B) ⊆⇩∘ ⋃⇩∘A ∩⇩∘ ⋃⇩∘B" by auto

lemma VUnion_vunion[simp]: "⋃⇩∘(A ∪⇩∘ B) = ⋃⇩∘A ∪⇩∘ ⋃⇩∘B" by auto

lemma VUnion_VPow[simp]: "⋃⇩∘(VPow A) = A" by auto

text‹Special properties.›

lemma VUnion_vempty_conv_left: "0 = ⋃⇩∘A ⟷ (∀x∈⇩∘A. x = 0)" by auto

lemma VUnion_vempty_conv_right: "⋃⇩∘A = 0 ⟷ (∀x∈⇩∘A. x = 0)" by auto

lemma vsubset_VPow_VUnion: "A ⊆⇩∘ VPow (⋃⇩∘A)" by auto

lemma VUnion_vsubsetI:
assumes "⋀x. x ∈⇩∘ A ⟹ ∃y. y ∈⇩∘ B ∧ x ⊆⇩∘ y"
shows "⋃⇩∘A ⊆⇩∘ ⋃⇩∘B"
using assms by auto

lemma VUnion_upper:
assumes "x ∈⇩∘ A"
shows "x ⊆⇩∘ ⋃⇩∘A"
using assms by auto

lemma VUnion_least:
assumes "⋀x. x ∈⇩∘ A ⟹ x ⊆⇩∘ B"
shows "⋃⇩∘A ⊆⇩∘ B"
using assms by (fact Sup_least)

subsection‹Pairs›

subsubsection‹Further results›

lemma small_elts_of_set[simp, intro]:
assumes "small x"
shows "elts (set x) = x"

lemma small_vpair[intro, simp]:
assumes "small {a. P a}"
shows "small {⟨a, b⟩ | a. P a}"
by (subgoal_tac ‹{⟨a, b⟩ | a. P a} = (λa. ⟨a, b⟩)  {a. P a}›)
(auto simp: assms)

subsubsection‹‹vpairs››

definition vpairs :: "V ⇒ V" where
"vpairs r = set {x. x ∈⇩∘ r ∧ (∃a b. x = ⟨a, b⟩)}"

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

text‹Rules.›

lemma vpairsI[intro]:
assumes "x ∈⇩∘ r" and "x = ⟨a, b⟩"
shows "x ∈⇩∘ vpairs r"
using assms unfolding vpairs_def by auto

lemma vpairsD[dest]:
assumes "x ∈⇩∘ vpairs r"
shows "x ∈⇩∘ r" and "∃a b. x = ⟨a, b⟩"
using assms unfolding vpairs_def by auto

lemma vpairsE[elim]:
assumes "x ∈⇩∘ vpairs r"
obtains a b where "x = ⟨a, b⟩" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vpairs_def by auto

lemma vpairs_iff: "x ∈⇩∘ vpairs r ⟷ x ∈⇩∘ r ∧ (∃a b. x = ⟨a, b⟩)" by auto

text‹Elementary properties.›

lemma vpairs_iff_elts: "⟨a, b⟩ ∈⇩∘ vpairs r ⟷ ⟨a, b⟩ ∈⇩∘ r" by auto

lemma vpairs_iff_pairs: "⟨a, b⟩ ∈⇩∘ vpairs r ⟷ (a, b) ∈ pairs r"

text‹Set operations.›

lemma vpairs_vempty[simp]: "vpairs 0 = 0" by auto

lemma vpairs_vsingleton[simp]: "vpairs (set {⟨a, b⟩}) = set {⟨a, b⟩}" by auto

lemma vpairs_vinsert: "vpairs (vinsert ⟨a, b⟩ A) = set {⟨a, b⟩} ∪⇩∘ vpairs A"
by auto

lemma vpairs_mono:
assumes "r ⊆⇩∘ s"
shows "vpairs r ⊆⇩∘ vpairs s"
using assms by blast

lemma vpairs_vunion: "vpairs (A ∪⇩∘ B) = vpairs A ∪⇩∘ vpairs B" by auto

lemma vpairs_vintersection: "vpairs (A ∩⇩∘ B) = vpairs A ∩⇩∘ vpairs B" by auto

lemma vpairs_vdiff: "vpairs (A -⇩∘ B) = vpairs A -⇩∘ vpairs B" by auto

text‹Special properties.›

lemma vpairs_ex_vfst:
assumes "x ∈⇩∘ vpairs r"
shows "∃b. ⟨vfst x, b⟩ ∈⇩∘ r"
using assms by force

lemma vpairs_ex_vsnd:
assumes "y ∈⇩∘ vpairs r"
shows "∃a. ⟨a, vsnd y⟩ ∈⇩∘ r"
using assms by force

subsection‹Cartesian products›

text‹
The following lemma is based on Theorem 6.2 from
\cite{takeuti_introduction_1971}.
›

lemma vtimes_vsubset_VPowVPow: "A ×⇩∘ B ⊆⇩∘ VPow (VPow (A ∪⇩∘ B))"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ A ×⇩∘ B"
then obtain a b where x_def: "x = ⟨a, b⟩" and "a ∈⇩∘ A" and "b ∈⇩∘ B" by clarsimp
then show "x ∈⇩∘ VPow (VPow (A ∪⇩∘ B))"
unfolding x_def vpair_def by auto
qed

subsection‹Pairwise›

definition vpairwise :: "(V ⇒ V ⇒ bool) ⇒ V ⇒ bool"
where "vpairwise R S ⟷ (∀x∈⇩∘S. ∀y∈⇩∘S. x ≠ y ⟶ R x y)"

text‹Rules.›

lemma vpairwiseI[intro?]:
assumes "⋀x y. x ∈⇩∘ S ⟹ y ∈⇩∘ S ⟹ x ≠ y ⟹ R x y"
shows "vpairwise R S"
using assms by (simp add: vpairwise_def)

lemma vpairwiseD[dest]:
assumes "vpairwise R S" and "x ∈⇩∘ S" and "y ∈⇩∘ S" and "x ≠ y"
shows "R x y" and "R y x"
using assms unfolding vpairwise_def by auto

text‹Elementary properties.›

lemma vpairwise_trivial[simp]: "vpairwise (λi j. j ≠ i) I"
by (auto simp: vpairwise_def)

text‹Set operations.›

lemma vpairwise_vempty[simp]: "vpairwise P 0" by (force intro: vpairwiseI)

lemma vpairwise_vsingleton[simp]: "vpairwise P (set {A})"

lemma vpairwise_vinsert:
"vpairwise r (vinsert x s) ⟷
(∀y. y ∈⇩∘ s ∧ y ≠ x ⟶ r x y ∧ r y x) ∧ vpairwise r s"
by (intro iffI conjI allI impI; (elim conjE | tactic‹all_tac›))
(auto simp: vpairwise_def)

lemma vpairwise_vsubset:
assumes "vpairwise P S" and "T ⊆⇩∘ S"
shows "vpairwise P T"
using assms by (metis less_eq_V_def subset_eq vpairwiseD(2) vpairwiseI)

lemma vpairwise_mono:
assumes "vpairwise P A" and "⋀x y. P x y ⟹ Q x y" and "B ⊆⇩∘ A"
shows "vpairwise Q B"
using assms by (simp add: less_eq_V_def subset_eq vpairwiseD(2) vpairwiseI)

subsection‹Disjoint sets›

abbreviation vdisjnt :: "V ⇒ V ⇒ bool"
where "vdisjnt A B ≡ A ∩⇩∘ B = 0"

text‹Elementary properties.›

lemma vdisjnt_sym:
assumes "vdisjnt A B"
shows "vdisjnt B A"
using assms by blast

lemma vdisjnt_iff: "vdisjnt A B ⟷ (∀x. ~ (x ∈⇩∘ A ∧ x ∈⇩∘ B))" by auto

text‹Set operations.›

lemma vdisjnt_vempty1[simp]: "vdisjnt 0 A"
and vdisjnt_vempty2[simp]: "vdisjnt A 0"
by auto

lemma vdisjnt_singleton0[simp]: "vdisjnt (set {a}) (set {b}) ⟷ a ≠ b"
and vdisjnt_singleton1[simp]: "vdisjnt (set {a}) A ⟷ a ∉⇩∘ A"
and vdisjnt_singleton2[simp]: "vdisjnt A (set {a}) ⟷ a ∉⇩∘ A"
by force+

lemma vdisjnt_vinsert_left: "vdisjnt (vinsert a X) Y ⟷ a ∉⇩∘ Y ∧ vdisjnt X Y"
by (metis vdisjnt_iff vdisjnt_sym vinsertE1 vinsertI2 vinsert_iff)

lemma vdisjnt_vinsert_right: "vdisjnt Y (vinsert a X) ⟷ a ∉⇩∘ Y ∧ vdisjnt Y X"
using vdisjnt_sym vdisjnt_vinsert_left by meson

lemma vdisjnt_vsubset_left:
assumes "vdisjnt X Y" and "Z ⊆⇩∘ X"
shows "vdisjnt Z Y"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_vsubset_right:
assumes "vdisjnt X Y" and "Z ⊆⇩∘ Y"
shows "vdisjnt X Z"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_vunion_left: "vdisjnt (A ∪⇩∘ B) C ⟷ vdisjnt A C ∧ vdisjnt B C"
by auto

lemma vdisjnt_vunion_right: "vdisjnt C (A ∪⇩∘ B) ⟷ vdisjnt C A ∧ vdisjnt C B"
by auto

text‹Special properties.›

lemma vdisjnt_vemptyI[intro]:
assumes "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B ⟹ False"
shows "vdisjnt A B"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_self_iff_vempty[simp]: "vdisjnt S S ⟷ S = 0" by auto

lemma vdisjntI:
assumes "⋀x y. x ∈⇩∘ A ⟹ y ∈⇩∘ B ⟹ x ≠ y"
shows "vdisjnt A B"
using assms by auto

lemma vdisjnt_nin_right:
assumes "vdisjnt A B" and "a ∈⇩∘ A"
shows "a ∉⇩∘ B"
using assms by auto

lemma vdisjnt_nin_left:
assumes "vdisjnt B A" and "a ∈⇩∘ A"
shows "a ∉⇩∘ B"
using assms by auto

text‹\newpage›

end

# Theory CZH_Sets_Nat

(* Copyright 2021 (C) Mihails Milehins *)

section‹Further properties of natural numbers›
theory CZH_Sets_Nat
imports CZH_Sets_Sets
begin

subsection‹Background›

text‹
The section exposes certain fundamental properties of natural numbers and
provides convenience utilities for doing arithmetic within the type \<^typ>‹V›.

Many of the results that are presented in this sections were carried over
(with amendments) from the theory ‹Nat› that can be found in the main
library of Isabelle/HOL.
›

notation ord_of_nat (‹_⇩ℕ›  999)

named_theorems nat_omega_simps

declare One_nat_def[simp del]

abbreviation (input) vpfst where "vpfst a ≡ a⦇0⦈"
abbreviation (input) vpsnd where "vpsnd a ≡ a⦇1⇩ℕ⦈"
abbreviation (input) vpthrd where "vpthrd a ≡ a⦇2⇩ℕ⦈"

subsection‹Conversion between \<^typ>‹V› and ‹nat››

subsubsection‹Primitive arithmetic›

lemma ord_of_nat_plus[nat_omega_simps]: "a⇩ℕ + b⇩ℕ = (a + b)⇩ℕ"
by (induct b) (simp_all add: plus_V_succ_right)

lemma ord_of_nat_times[nat_omega_simps]: "a⇩ℕ * b⇩ℕ = (a * b)⇩ℕ"
by (induct b) (simp_all add: mult_succ nat_omega_simps)

lemma ord_of_nat_succ[nat_omega_simps]: "succ (a⇩ℕ) = (Suc a)⇩ℕ" by auto

lemma ord_of_nat_csucc[nat_omega_simps]: "csucc (a⇩ℕ) = succ (a⇩ℕ)"
using finite_csucc by blast

lemma ord_of_nat_succ_vempty[nat_omega_simps]: "succ 0 = 1⇩ℕ" by auto

lemma ord_of_nat_vone[nat_omega_simps]: "1 = 1⇩ℕ" by auto

subsubsection‹Transfer›

definition cr_omega :: "V ⇒ nat ⇒ bool"
where "cr_omega a b ⟷ (a = ord_of_nat b)"

text‹Transfer setup.›

lemma cr_omega_right_total[transfer_rule]: "right_total cr_omega"
unfolding cr_omega_def right_total_def by simp

lemma cr_omega_bi_unqie[transfer_rule]: "bi_unique cr_omega"
unfolding cr_omega_def bi_unique_def

lemma omega_transfer_domain_rule[transfer_domain_rule]:
"Domainp cr_omega = (λx. x ∈⇩∘ ω)"
unfolding cr_omega_def by (auto simp: elts_ω)

lemma omega_transfer[transfer_rule]:
"(rel_set cr_omega) (elts ω) (UNIV::nat set)"
unfolding cr_omega_def rel_set_def by (simp add: elts_ω)

lemma omega_of_real_transfer[transfer_rule]: "cr_omega (ord_of_nat a) a"
unfolding cr_omega_def by auto

text‹Operations.›

lemma omega_succ_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega) succ Suc"
proof(intro rel_funI, unfold cr_omega_def)
fix x y assume prems: "x = y⇩ℕ"
show "succ x = Suc y⇩ℕ" unfolding prems ord_of_nat_succ[symmetric] ..
qed

lemma omega_plus_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega ===> cr_omega) (+) (+)"
by (intro rel_funI, unfold cr_omega_def) (simp add: nat_omega_simps)

lemma omega_mult_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega ===> cr_omega) (*) (*)"
by (intro rel_funI, unfold cr_omega_def) (simp add: nat_omega_simps)

lemma ord_of_nat_card_transfer[transfer_rule]:
includes lifting_syntax
shows "(rel_set (=) ===> cr_omega) (λx. ord_of_nat (card x)) card"
by (intro rel_funI) (simp add: cr_omega_def rel_set_eq)

subsection‹Elementary results›

lemma ord_of_nat_vempty: "0 = 0⇩ℕ" by auto

lemma set_vzero_eq_ord_of_nat_vone: "set {0} = 1⇩ℕ"
by (metis elts_1 set_of_elts ord_of_nat_vone)

lemma vone_in_omega[simp]: "1 ∈⇩∘ ω" unfolding ω_def by force

lemma nat_of_omega:
assumes "n ∈⇩∘ ω"
obtains m where "n = m⇩ℕ"
using assms unfolding ω_def by clarsimp

lemma omega_prev:
assumes "n ∈⇩∘ ω" and "0 ∈⇩∘ n"
obtains k where "n = succ k"
proof-
from assms nat_of_omega obtain m where "n = m⇩ℕ" by auto
with assms(2) obtain m' where "m = Suc m'"
unfolding less_V_def by (auto dest: gr0_implies_Suc)
with that show ?thesis unfolding ‹n = m⇩ℕ› using ord_of_nat.simps(2) by blast
qed

lemma omega_vplus_commutative:
assumes "a ∈⇩∘ ω" and "b ∈⇩∘ ω"
shows "a + b = b + a"
using assms by (metis Groups.add_ac(2) nat_of_omega ord_of_nat_plus)

lemma omega_vinetrsection[intro]:
assumes "m ∈⇩∘ ω" and "n ∈⇩∘ ω"
shows "m ∩⇩∘ n ∈⇩∘ ω"
proof-
from nat_into_Ord[OF assms(1)] nat_into_Ord[OF assms(2)] Ord_linear_le
consider "m ⊆⇩∘ n" | "n ⊆⇩∘ m"
by auto
then show ?thesis by cases (simp_all add: assms inf.absorb1 inf.absorb2)
qed

subsection‹Induction›

lemma omega_induct_all[consumes 1, case_names step]:
assumes "n ∈⇩∘ ω" and "⋀x. ⟦x ∈⇩∘ ω; ⋀y. y ∈⇩∘ x ⟹ P y⟧ ⟹ P x"
shows "P n"
using assms by (metis Ord_ω Ord_induct Ord_linear Ord_trans nat_into_Ord)

lemma omega_induct[consumes 1, case_names 0 succ]:
assumes "n ∈⇩∘ ω" and "P 0" and "⋀n. ⟦ n ∈⇩∘ ω; P n ⟧ ⟹ P (succ n)"
shows "P n"
using assms(1,3)
proof(induct rule: omega_induct_all)
case (step x) show ?case
proof(cases ‹x = 0›)
case True with assms(2) show ?thesis by simp
next
case False
with step(1) have "0 ∈⇩∘ x" by (simp add: mem_0_Ord)
with ‹x ∈⇩∘ ω› obtain y where x_def: "x = succ y" by (elim omega_prev)
with elts_succ step.hyps(1) have "y ∈⇩∘ ω" by (blast intro: Ord_trans)
have "y ∈⇩∘ x" by (simp add: ‹x = succ y›)
have "P y" by (auto intro: step.prems step.hyps(2)[OF ‹y ∈⇩∘ x›])
from step.prems[OF ‹y ∈⇩∘ ω› ‹P y›, folded x_def] show "P x" .
qed
qed

subsection‹Methods›

text‹
The following methods provide an infrastructure for working with goals of the
form ‹a ∈⇩∘ n⇩ℕ ⟹ P a›.
›

lemma in_succE:
assumes "a ∈⇩∘ succ n" and "⋀a. a ∈⇩∘ n ⟹ P a" and "P n"
shows "P a"
using assms by auto

method Suc_of_numeral =
(
use nothing in ‹unfold Suc_eq_plus1_left[symmetric], unfold One_nat_def›
)

method succ_of_numeral =
(
Suc_of_numeral,
use nothing in ‹unfold ord_of_nat_succ[symmetric] ord_of_nat_zero›
)

method numeral_of_succ =
(
unfold nat_omega_simps,
use nothing in
‹
(unfold numerals(1))?
›
)

method elim_in_succ =
(
(
elim in_succE;
use nothing in ‹(unfold triv_forall_equality)?; (numeral_of_succ)?›
),
simp
)

method elim_in_numeral = (succ_of_numeral, use nothing in ‹elim_in_succ›)

subsection‹Auxiliary›

lemma two: "2⇩ℕ = set {0, 1⇩ℕ}" by force

lemma three: "3⇩ℕ = set {0, 1⇩ℕ, 2⇩ℕ}" by force

lemma four: "4⇩ℕ = set {0, 1⇩ℕ, 2⇩ℕ, 3⇩ℕ}" by force

lemma two_vdiff_zero[simp]: "set {0, 1⇩ℕ} -⇩∘ set {0} = set {1⇩ℕ}" by auto
lemma two_vdiff_one[simp]: "set {0, 1⇩ℕ} -⇩∘ set {1⇩ℕ} = set {0}" by auto

text‹\newpage›

end

# Theory CZH_Sets_BRelations

(* Copyright 2021 (C) Mihails Milehins *)

section‹Elementary binary relations›
theory CZH_Sets_BRelations
imports CZH_Sets_Sets
keywords "mk_VLambda" :: thy_defn
and "|app" "|vsv" "|vdomain"
begin

subsection‹Background›

text‹
This section presents a theory of binary relations internalized in the
type \<^typ>‹V› and exposes elementary properties of two special types of
binary relations: single-valued binary relations and injective single-valued
binary relations.

Many of the results that are presented in this section were carried over
(with amendments) from the theories \<^text>‹Set› and \<^text>‹Relation› in the main
library.
›

subsection‹Constructors›

subsubsection‹Identity relation›

definition vid_on :: "V ⇒ V"
where "vid_on A = set {⟨a, a⟩ | a. a ∈⇩∘ A}"

lemma vid_on_small[simp]: "small {⟨a, a⟩ | a. a ∈⇩∘ A}"
by (rule down[of _ ‹A ×⇩∘ A›]) blast

text‹Rules.›

lemma vid_on_eqI:
assumes "a = b" and "a ∈⇩∘ A"
shows "⟨a, b⟩ ∈⇩∘ vid_on A"
using assms by (simp add: vid_on_def)

lemma vid_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, a⟩ ∈⇩∘ vid_on A"
by (rule vid_on_eqI) (simp_all add: assms)

lemma vid_onD[dest!]:
assumes "⟨a, a⟩ ∈⇩∘ vid_on A"
shows "a ∈⇩∘ A"
using assms unfolding vid_on_def by auto

lemma vid_onE[elim!]:
assumes "x ∈⇩∘ vid_on A" and "∃a∈⇩∘A. x = ⟨a, a⟩ ⟹ P"
shows P
using assms unfolding vid_on_def by auto

lemma vid_on_iff: "⟨a, b⟩ ∈⇩∘ vid_on A ⟷ a = b ∧ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma vid_on_vempty[simp]: "vid_on 0 = 0" by auto

lemma vid_on_vsingleton[simp]: "vid_on (set {a}) = set {⟨a, a⟩}" by auto

lemma vid_on_vdoubleton[simp]: "vid_on (set {a, b}) = set {⟨a, a⟩, ⟨b, b⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vid_on_mono:
assumes "A ⊆⇩∘ B"
shows "vid_on A ⊆⇩∘ vid_on B"
using assms by auto

lemma vid_on_vinsert: "(vinsert ⟨a, a⟩ (vid_on A)) = (vid_on (vinsert a A))"
by auto

lemma vid_on_vintersection: "vid_on (A ∩⇩∘ B) = vid_on A ∩⇩∘ vid_on B" by auto

lemma vid_on_vunion: "vid_on (A ∪⇩∘ B) = vid_on A ∪⇩∘ vid_on B" by auto

lemma vid_on_vdiff: "vid_on (A -⇩∘ B) = vid_on A -⇩∘ vid_on B" by auto

text‹Special properties.›

lemma vid_on_vsubset_vtimes: "vid_on A ⊆⇩∘ A ×⇩∘ A" by clarsimp

subsubsection‹Constant function›

definition vconst_on :: "V ⇒ V ⇒ V"
where "vconst_on A c = set {⟨a, c⟩ | a. a ∈⇩∘ A}"

lemma small_vconst_on[simp]: "small {⟨a, c⟩ | a. a ∈⇩∘ A}"
by (rule down[of _ ‹A ×⇩∘ set {c}›]) auto

text‹Rules.›

lemma vconst_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, c⟩ ∈⇩∘ vconst_on A c"
using assms unfolding vconst_on_def by simp

lemma vconst_onD[dest!]:
assumes "⟨a, c⟩ ∈⇩∘ vconst_on A c"
shows "a ∈⇩∘ A"
using assms unfolding vconst_on_def by simp

lemma vconst_onE[elim!]:
assumes "x ∈⇩∘ vconst_on A c"
obtains a where "a ∈⇩∘ A" and "x = ⟨a, c⟩"
using assms unfolding vconst_on_def by auto

lemma vconst_on_iff: "⟨a, c⟩ ∈⇩∘ vconst_on A c ⟷ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma vconst_on_vempty[simp]: "vconst_on 0 c = 0"
unfolding vconst_on_def by auto

lemma vconst_on_vsingleton[simp]: "vconst_on (set {a}) c = set {⟨a, c⟩}" by auto

lemma vconst_on_vdoubleton[simp]: "vconst_on (set {a, b}) c = set {⟨a, c⟩, ⟨b, c⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vconst_on_mono:
assumes "A ⊆⇩∘ B"
shows "vconst_on A c ⊆⇩∘ vconst_on B c"
using assms by auto

lemma vconst_on_vinsert:
"(vinsert ⟨a, c⟩ (vconst_on A c)) = (vconst_on (vinsert a A) c)"
by auto

lemma vconst_on_vintersection:
"vconst_on (A ∩⇩∘ B) c = vconst_on A c ∩⇩∘ vconst_on B c"
by auto

lemma vconst_on_vunion: "vconst_on (A ∪⇩∘ B) c = vconst_on A c ∪⇩∘ vconst_on B c"
by auto

lemma vconst_on_vdiff: "vconst_on (A -⇩∘ B) c = vconst_on A c -⇩∘ vconst_on B c"
by auto

text‹Special properties.›

lemma vconst_on_eq_vtimes: "vconst_on A c = A ×⇩∘ set {c}"
by standard (auto intro!: vsubset_antisym)

subsubsection‹‹VLambda››

text‹Rules.›

lemma VLambdaI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, f a⟩ ∈⇩∘ (λa∈⇩∘A. f a)"
using assms unfolding VLambda_def by auto

assumes "⟨a, f a⟩ ∈⇩∘ (λa∈⇩∘A. f a)"
shows "a ∈⇩∘ A"
using assms unfolding VLambda_def by auto

lemma VLambdaE[elim!]:
assumes "x ∈⇩∘ (λa∈⇩∘A. f a)"
obtains a where "a ∈⇩∘ A" and "x = ⟨a, f a⟩"
using assms unfolding VLambda_def by auto

lemma VLambda_iff1: "x ∈⇩∘ (λa∈⇩∘A. f a) ⟷ (∃a∈⇩∘A. x = ⟨a, f a⟩)" by auto

lemma VLambda_iff2: "⟨a, b⟩ ∈⇩∘ (λa∈⇩∘A. f a) ⟷ b = f a ∧ a ∈⇩∘ A" by auto

lemma small_VLambda[simp]: "small {⟨a, f a⟩ | a. a ∈⇩∘ A}" by auto

lemma VLambda_set_def: "(λa∈⇩∘A. f a) = set {⟨a, f a⟩ | a. a ∈⇩∘ A}" by auto

text‹Set operations.›

lemma VLambda_vempty[simp]: "(λa∈⇩∘0. f a) = 0" by auto

lemma VLambda_vsingleton(*not simp*): "(λa∈⇩∘set {a}. f a) = set {⟨a, f a⟩}"
by auto

lemma VLambda_vdoubleton(*not simp*):
"(λa∈⇩∘set {a, b}. f a) = set {⟨a, f a⟩, ⟨b, f b⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma VLambda_mono:
assumes "A ⊆⇩∘ B"
shows "(λa∈⇩∘A. f a) ⊆⇩∘ (λa∈⇩∘B. f a)"
using assms by auto

lemma VLambda_vinsert:
"(λa∈⇩∘vinsert a A. f a) = (λa∈⇩∘set {a}. f a) ∪⇩∘ (λa∈⇩∘A. f a)"
by auto

lemma VLambda_vintersection: "(λa∈⇩∘A ∩⇩∘ B. f a) = (λa∈⇩∘A. f a) ∩⇩∘ (λa∈⇩∘B. f a)"
by auto

lemma VLambda_vunion: "(λa∈⇩∘A ∪⇩∘ B. f a) = (λa∈⇩∘A. f a) ∪⇩∘ (λa∈⇩∘B. f a)" by auto

lemma VLambda_vdiff: "(λa∈⇩∘A -⇩∘ B. f a) = (λa∈⇩∘A. f a) -⇩∘ (λa∈⇩∘B. f a)" by auto

text‹Connections.›

lemma VLambda_vid_on: "(λa∈⇩∘A. a) = vid_on A" by auto

lemma VLambda_vconst_on: "(λa∈⇩∘A. c) = vconst_on A c" by auto

subsubsection‹Composition›

definition vcomp :: "V ⇒ V ⇒ V" (infixr "∘⇩∘" 75)
where "r ∘⇩∘ s = set {⟨a, c⟩ | a c. ∃b. ⟨a, b⟩ ∈⇩∘ s ∧ ⟨b, c⟩ ∈⇩∘ r}"
notation vcomp (infixr ‹∘⇩∘› 75)

lemma vcomp_small[simp]: "small {⟨a, c⟩ | a c. ∃b. ⟨a, b⟩ ∈⇩∘ s ∧ ⟨b, c⟩ ∈⇩∘ r}"
(is ‹small ?s›)
proof-
define comp' where "comp' = (λ⟨⟨a, b⟩, ⟨c, d⟩⟩. ⟨a, d⟩)"
have "small (elts (vpairs (s ×⇩∘ r)))" by simp
then have small_comp: "small (comp'  elts (vpairs (s ×⇩∘ r)))" by simp
have ss: "?s ⊆ (comp'  elts (vpairs (s ×⇩∘ r)))"
proof
fix x assume "x ∈ ?s"
then obtain a b c where x_def: "x = ⟨a, c⟩"
and "⟨a, b⟩ ∈⇩∘ s"
and "⟨b, c⟩ ∈⇩∘ r"
by auto
then have abbc: "⟨⟨a, b⟩, ⟨b, c⟩⟩ ∈⇩∘ vpairs (s ×⇩∘ r)"
have x_def': "x = comp' ⟨⟨a, b⟩, ⟨b, c⟩⟩" unfolding comp'_def x_def by auto
then show "x ∈ comp'  elts (vpairs (s ×⇩∘ r))"
unfolding x_def' using abbc by auto
qed
with small_comp show ?thesis by (metis (lifting) smaller_than_small)
qed

text‹Rules.›

lemma vcompI[intro!]:
assumes "⟨b, c⟩ ∈⇩∘ r" and "⟨a, b⟩ ∈⇩∘ s"
shows "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
using assms unfolding vcomp_def by auto

lemma vcompD[dest!]:
assumes "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
shows "∃b. ⟨b, c⟩ ∈⇩∘ r ∧ ⟨a, b⟩ ∈⇩∘ s"
using assms unfolding vcomp_def by auto

lemma vcompE[elim!]:
assumes "ac ∈⇩∘ r ∘⇩∘ s"
obtains a b c where "ac = ⟨a, c⟩" and "⟨a, b⟩ ∈⇩∘ s" and "⟨b, c⟩ ∈⇩∘ r"
using assms unfolding vcomp_def by clarsimp

text‹Elementary properties.›

lemma vcomp_assoc: "(r ∘⇩∘ s) ∘⇩∘ t = r ∘⇩∘ (s ∘⇩∘ t)" by auto

text‹Set operations.›

lemma vcomp_vempty_left[simp]: "0 ∘⇩∘ r = 0" by auto

lemma vcomp_vempty_right[simp]: "r ∘⇩∘ 0 = 0" by auto

lemma vcomp_mono:
assumes "r' ⊆⇩∘ r" and "s' ⊆⇩∘ s"
shows "r' ∘⇩∘ s' ⊆⇩∘ r ∘⇩∘ s"
using assms by auto

lemma vcomp_vinsert_left[simp]:
"(vinsert ⟨a, b⟩ s) ∘⇩∘ r = (set {⟨a, b⟩} ∘⇩∘ r) ∪⇩∘ (s ∘⇩∘ r)"
by auto

lemma vcomp_vinsert_right[simp]:
"r ∘⇩∘ (vinsert ⟨a, b⟩ s) = (r ∘⇩∘ set {⟨a, b⟩}) ∪⇩∘ (r ∘⇩∘ s)"
by auto

lemma vcomp_vunion_left[simp]: "(s ∪⇩∘ t) ∘⇩∘ r = (s ∘⇩∘ r) ∪⇩∘ (t ∘⇩∘ r)" by auto

lemma vcomp_vunion_right[simp]: "r ∘⇩∘ (s ∪⇩∘ t) = (r ∘⇩∘ s) ∪⇩∘ (r ∘⇩∘ t)" by auto

text‹Connections.›

lemma vcomp_vid_on_idem[simp]: "vid_on A ∘⇩∘ vid_on A = vid_on A" by auto

lemma vcomp_vid_on[simp]: "vid_on A ∘⇩∘ vid_on B = vid_on (A ∩⇩∘ B)" by auto

lemma vcomp_vconst_on_vid_on[simp]: "vconst_on A c ∘⇩∘ vid_on A = vconst_on A c"
by auto

lemma vcomp_VLambda_vid_on[simp]: "(λa∈⇩∘A. f a) ∘⇩∘ vid_on A = (λa∈⇩∘A. f a)"
by auto

text‹Special properties.›

lemma vcomp_vsubset_vtimes:
assumes "r ⊆⇩∘ B ×⇩∘ C" and "s ⊆⇩∘ A ×⇩∘ B"
shows "r ∘⇩∘ s ⊆⇩∘ A ×⇩∘ C"
using assms by auto

lemma vcomp_obtain_middle[elim]:
assumes "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
obtains b where "⟨a, b⟩ ∈⇩∘ s" and "⟨b, c⟩ ∈⇩∘ r"
using assms by auto

subsubsection‹Converse relation›

definition vconverse :: "V ⇒ V"
where "vconverse A = (λr∈⇩∘A. set {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vconverse (‹(_¯⇩∘)›  999)
where "r¯⇩∘ ≡ vconverse (set {r}) ⦇r⦈"

lemma app_vconverse_def: "r¯⇩∘ = set {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vconverse_def by simp

lemma vconverse_small[simp]: "small {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have eq: "{⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r} = (λ⟨a, b⟩. ⟨b, a⟩)  elts (vpairs r)"
proof(rule subset_antisym; rule subsetI, unfold mem_Collect_eq)
fix x assume "x ∈ (λ⟨a, b⟩. ⟨b, a⟩)  elts (vpairs r)"
then obtain a b where "⟨a, b⟩ ∈⇩∘ vpairs r" and "x = (λ⟨a, b⟩. ⟨b, a⟩) ⟨a, b⟩"
by blast
then show "∃a b. x = ⟨b, a⟩ ∧ ⟨a, b⟩ ∈⇩∘ r" by auto
qed (use image_iff vpairs_iff_elts in fastforce)
show ?thesis unfolding eq by (rule replacement) auto
qed

text‹Rules.›

lemma vconverseI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, r¯⇩∘⟩ ∈⇩∘ vconverse A"
using assms unfolding vconverse_def by auto

lemma vconverseD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vconverse A"
shows "r ∈⇩∘ A" and "s = r¯⇩∘"
using assms unfolding vconverse_def by auto

lemma vconverseE[elim]:
assumes "x ∈⇩∘ vconverse A"
obtains r where "x = ⟨r, r¯⇩∘⟩" and "r ∈⇩∘ A"
using assms unfolding vconverse_def by auto

lemma app_vconverseI[sym, intro!]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "⟨b, a⟩ ∈⇩∘ r¯⇩∘"
using assms unfolding vconverse_def by auto

lemma app_vconverseD[sym, dest]:
assumes "⟨a, b⟩ ∈⇩∘ r¯⇩∘"
shows "⟨b, a⟩ ∈⇩∘ r"
using assms unfolding vconverse_def by simp

lemma app_vconverseE[elim!]:
assumes "x ∈⇩∘ r¯⇩∘"
obtains a b where "x = ⟨b, a⟩" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vconverse_def by auto

lemma vconverse_iff: "⟨b, a⟩ ∈⇩∘ r¯⇩∘ ⟷ ⟨a, b⟩ ∈⇩∘ r" by auto

text‹Set operations.›

lemma vconverse_vempty[simp]: "0¯⇩∘ = 0" by auto

lemma vconverse_vsingleton: "(set {⟨a, b⟩})¯⇩∘ = set {⟨b, a⟩}" by auto

lemma vconverse_vdoubleton[simp]: "(set {⟨a, b⟩, ⟨c, d⟩})¯⇩∘ = set {⟨b, a⟩, ⟨d, c⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vconverse_vinsert: "(vinsert ⟨a, b⟩ r)¯⇩∘ = vinsert ⟨b, a⟩ (r¯⇩∘)" by auto

lemma vconverse_vintersection: "(r ∩⇩∘ s)¯⇩∘ = r¯⇩∘ ∩⇩∘ s¯⇩∘" by auto

lemma vconverse_vunion: "(r ∪⇩∘ s)¯⇩∘ = r¯⇩∘ ∪⇩∘ s¯⇩∘" by auto

text‹Connections.›

lemma vconverse_vid_on[simp]: "(vid_on A)¯⇩∘ = vid_on A" by auto

lemma vconverse_vconst_on[simp]: "(vconst_on A c)¯⇩∘ = set {c} ×⇩∘ A" by auto

lemma vconverse_vcomp: "(r ∘⇩∘ s)¯⇩∘ = s¯⇩∘ ∘⇩∘ r¯⇩∘" by auto

lemma vconverse_vtimes: "(A ×⇩∘ B)¯⇩∘ = (B ×⇩∘ A)" by auto

subsubsection‹Left restriction›

definition vlrestriction :: "V ⇒ V"
where "vlrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vlrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧l⇩∘› 80)
where "r ↾⇧l⇩∘ A ≡ vlrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vlrestriction_def: "r ↾⇧l⇩∘ A = set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vlrestriction_def by simp

lemma vlrestriction_small[simp]: "small {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma vlrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇧l⇩∘ A⟩ ∈⇩∘ vlrestriction D"
using assms unfolding vlrestriction_def by (simp add: VLambda_iff2)

lemma vlrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vlrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇧l⇩∘ A"
using assms unfolding vlrestriction_def by auto

lemma vlrestrictionE[elim]:
assumes "x ∈⇩∘ vlrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇧l⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇧l⇩∘ A"
using assms unfolding vlrestriction_def by simp

lemma app_vlrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇧l⇩∘ A"
shows "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionE[elim]:
assumes "x ∈⇩∘ r ↾⇧l⇩∘ A"
obtains a b where "x = ⟨a, b⟩" and "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vlrestriction_def by auto

text‹Set operations.›

lemma vlrestriction_on_vempty[simp]: "r ↾⇧l⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vlrestriction_vempty[simp]: "0 ↾⇧l⇩∘ A = 0" by auto

lemma vlrestriction_vsingleton_in[simp]:
assumes "a ∈⇩∘ A"
shows "set {⟨a, b⟩} ↾⇧l⇩∘ A = set {⟨a, b⟩}"
using assms by auto

lemma vlrestriction_vsingleton_nin[simp]:
assumes "a ∉⇩∘ A"
shows "set {⟨a, b⟩} ↾⇧l⇩∘ A = 0"
using assms by auto

lemma vlrestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇧l⇩∘ A ⊆⇩∘ r ↾⇧l⇩∘ B"
using assms by auto

lemma vlrestriction_vinsert_nin[simp]:
assumes "a ∉⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧l⇩∘ A = r ↾⇧l⇩∘ A"
using assms by auto

lemma vlrestriction_vinsert_in:
assumes "a ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧l⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇧l⇩∘ A)"
using assms by auto

lemma vlrestriction_vintersection: "(r ∩⇩∘ s) ↾⇧l⇩∘ A = r ↾⇧l⇩∘ A ∩⇩∘ s ↾⇧l⇩∘ A" by auto

lemma vlrestriction_vunion: "(r ∪⇩∘ s) ↾⇧l⇩∘ A = r ↾⇧l⇩∘ A ∪⇩∘ s ↾⇧l⇩∘ A" by auto

lemma vlrestriction_vdiff: "(r -⇩∘ s) ↾⇧l⇩∘ A = r ↾⇧l⇩∘ A -⇩∘ s ↾⇧l⇩∘ A" by auto

text‹Connections.›

lemma vlrestriction_vid_on[simp]: "(vid_on A) ↾⇧l⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

lemma vlrestriction_vconst_on: "(vconst_on A c) ↾⇧l⇩∘ B = (vconst_on B c) ↾⇧l⇩∘ A"
by auto

lemma vlrestriction_vconst_on_commute:
assumes "x ∈⇩∘ vconst_on A c ↾⇧l⇩∘ B"
shows "x ∈⇩∘ vconst_on B c ↾⇧l⇩∘ A"
using assms by auto

lemma vlrestriction_vcomp[simp]: "(r ∘⇩∘ s) ↾⇧l⇩∘ A = r ∘⇩∘ (s ↾⇧l⇩∘ A)" by auto

text‹Previous connections.›

lemma vcomp_rel_vid_on[simp]: "r ∘⇩∘ vid_on A = r ↾⇧l⇩∘ A" by auto

lemma vcomp_vconst_on:
"r ∘⇩∘ (vconst_on A c) = (r ↾⇧l⇩∘ set {c}) ∘⇩∘ (vconst_on A c)"
by auto

text‹Special properties.›

lemma vlrestriction_vsubset_vpairs: "r ↾⇧l⇩∘ A ⊆⇩∘ vpairs r"
by (rule vsubsetI) blast

lemma vlrestriction_vsubset_rel: "r ↾⇧l⇩∘ A ⊆⇩∘ r" by auto

lemma vlrestriction_VLambda: "(λa∈⇩∘A. f a) ↾⇧l⇩∘ B = (λa∈⇩∘A ∩⇩∘ B. f a)" by auto

subsubsection‹Right restriction›

definition vrrestriction :: "V ⇒ V"
where "vrrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧r⇩∘› 80)
where "r ↾⇧r⇩∘ A ≡ vrrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vrrestriction_def: "r ↾⇧r⇩∘ A = set {⟨a, b⟩ | a b. b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrrestriction_def by simp

lemma vrrestriction_small[simp]: "small {⟨a, b⟩ | a b. b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma vrrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇧r⇩∘ A⟩ ∈⇩∘ vrrestriction D"
using assms unfolding vrrestriction_def by (simp add: VLambda_iff2)

lemma vrrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vrrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇧r⇩∘ A"
using assms unfolding vrrestriction_def by auto

lemma vrrestrictionE[elim]:
assumes "x ∈⇩∘ vrrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇧r⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionI[intro!]:
assumes "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇧r⇩∘ A"
using assms unfolding vrrestriction_def by simp

lemma app_vrrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇧r⇩∘ A"
shows "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionE[elim]:
assumes "x ∈⇩∘ r ↾⇧r⇩∘ A"
obtains a b where "x = ⟨a, b⟩" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrrestriction_def by auto

text‹Set operations.›

lemma vrrestriction_on_vempty[simp]: "r ↾⇧r⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vrrestriction_vempty[simp]: "0 ↾⇧r⇩∘ A = 0" by auto

lemma vrrestriction_vsingleton_in[simp]:
assumes "b ∈⇩∘ A"
shows "set {⟨a, b⟩} ↾⇧r⇩∘ A = set {⟨a, b⟩}"
using assms by auto

lemma vrrestriction_vsingleton_nin[simp]:
assumes "b ∉⇩∘ A"
shows "set {⟨a, b⟩} ↾⇧r⇩∘ A = 0"
using assms by auto

lemma vrrestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇧r⇩∘ A ⊆⇩∘ r ↾⇧r⇩∘ B"
using assms by auto

lemma vrrestriction_vinsert_nin[simp]:
assumes "b ∉⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧r⇩∘ A = r ↾⇧r⇩∘ A"
using assms by auto

lemma vrrestriction_vinsert_in:
assumes "b ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧r⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇧r⇩∘ A)"
using assms by auto

lemma vrrestriction_vintersection: "(r ∩⇩∘ s) ↾⇧r⇩∘ A = r ↾⇧r⇩∘ A ∩⇩∘ s ↾⇧r⇩∘ A" by auto

lemma vrrestriction_vunion: "(r ∪⇩∘ s) ↾⇧r⇩∘ A = r ↾⇧r⇩∘ A ∪⇩∘ s ↾⇧r⇩∘ A" by auto

lemma vrrestriction_vdiff: "(r -⇩∘ s) ↾⇧r⇩∘ A = r ↾⇧r⇩∘ A -⇩∘ s ↾⇧r⇩∘ A" by auto

text‹Connections.›

lemma vrrestriction_vid_on[simp]: "(vid_on A) ↾⇧r⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

lemma vrrestriction_vconst_on:
assumes "c ∈⇩∘ B"
shows "(vconst_on A c) ↾⇧r⇩∘ B = vconst_on A c"
using assms by auto

lemma vrrestriction_vcomp[simp]: "(r ∘⇩∘ s) ↾⇧r⇩∘ A = (r ↾⇧r⇩∘ A) ∘⇩∘ s" by auto

text‹Previous connections.›

lemma vcomp_vid_on_rel[simp]: "vid_on A ∘⇩∘ r = r ↾⇧r⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vcomp_vconst_on_rel: "(vconst_on A c) ∘⇩∘ r = (vconst_on A c) ∘⇩∘ (r ↾⇧r⇩∘ A)"
by auto

lemma vlrestriction_vconverse: "r¯⇩∘ ↾⇧l⇩∘ A = (r ↾⇧r⇩∘ A)¯⇩∘" by auto

lemma vrrestriction_vconverse: "r¯⇩∘ ↾⇧r⇩∘ A = (r ↾⇧l⇩∘ A)¯⇩∘" by auto

text‹Special properties.›

lemma vrrestriction_vsubset_rel: "r ↾⇧r⇩∘ A ⊆⇩∘ r" by auto

lemma vrrestriction_vsubset_vpairs: "r ↾⇧r⇩∘ A ⊆⇩∘ vpairs r" by auto

subsubsection‹Restriction›

definition vrestriction :: "V ⇒ V"
where "vrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇩∘› 80)
where "r ↾⇩∘ A ≡ vrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vrestriction_def:
"r ↾⇩∘ A = set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrestriction_def by simp

lemma vrestriction_small[simp]:
"small {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma vrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇩∘ A⟩ ∈⇩∘ vrestriction D"
using assms unfolding vrestriction_def by (simp add: VLambda_iff2)

lemma vrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇩∘ A"
using assms unfolding vrestriction_def by auto

lemma vrestrictionE[elim]:
assumes "x ∈⇩∘ vrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇩∘ A"
using assms unfolding vrestriction_def by simp

lemma app_vrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇩∘ A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionE[elim]:
assumes "x ∈⇩∘ r ↾⇩∘ A"
obtains a b where "x = ⟨a, b⟩" and "a ∈⇩∘ A" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrestriction_def by clarsimp

text‹Set operations.›

lemma vrestriction_on_vempty[simp]: "r ↾⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vrestriction_vempty[simp]: "0 ↾⇩∘ A = 0" by auto

lemma vrestriction_vsingleton_in[simp]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "set {⟨a, b⟩} ↾⇩∘ A = set {⟨a, b⟩}"
using assms by auto

lemma vrestriction_vsingleton_nin_left[simp]:
assumes "a ∉⇩∘ A"
shows "set {⟨a, b⟩} ↾⇩∘ A = 0"
using assms by auto

lemma vrestriction_vsingleton_nin_right[simp]:
assumes "b ∉⇩∘ A"
shows "set {⟨a, b⟩} ↾⇩∘ A = 0"
using assms by auto

lemma vrestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇩∘ A ⊆⇩∘ r ↾⇩∘ B"
using assms by auto

lemma vrestriction_vinsert_nin[simp]:
assumes "a ∉⇩∘ A" and "b ∉⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇩∘ A = r ↾⇩∘ A"
using assms by auto

lemma vrestriction_vinsert_in:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇩∘ A)"
using assms by auto

lemma vrestriction_vintersection: "(r ∩⇩∘ s) ↾⇩∘ A = r ↾⇩∘ A ∩⇩∘ s ↾⇩∘ A" by auto

lemma vrestriction_vunion: "(r ∪⇩∘ s) ↾⇩∘ A = r ↾⇩∘ A ∪⇩∘ s ↾⇩∘ A" by auto

lemma vrestriction_vdiff: "(r -⇩∘ s) ↾⇩∘ A = r ↾⇩∘ A -⇩∘ s ↾⇩∘ A" by auto

text‹Connections.›

lemma vrestriction_vid_on[simp]: "(vid_on A) ↾⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

lemma vrestriction_vconst_on_ex:
assumes "c ∈⇩∘ B"
shows "(vconst_on A c) ↾⇩∘ B = vconst_on (A ∩⇩∘ B) c"
using assms by auto

lemma vrestriction_vconst_on_nex:
assumes "c ∉⇩∘ B"
shows "(vconst_on A c) ↾⇩∘ B = 0"
using assms by auto

lemma vrestriction_vcomp[simp]: "(r ∘⇩∘ s) ↾⇩∘ A = (r ↾⇧r⇩∘ A) ∘⇩∘ (s ↾⇧l⇩∘ A)" by auto

lemma vrestriction_vconverse: "r¯⇩∘ ↾⇩∘ A = (r ↾⇩∘ A)¯⇩∘" by auto

text‹Previous connections.›

lemma vrrestriction_vlrestriction[simp]: "(r ↾⇧r⇩∘ A) ↾⇧l⇩∘ A = r ↾⇩∘ A" by auto

lemma vlrestriction_vrrestriction[simp]: "(r ↾⇧l⇩∘ A) ↾⇧r⇩∘ A = r ↾⇩∘ A" by auto

lemma vrestriction_vlrestriction[simp]: "(r ↾⇩∘ A) ↾⇧l⇩∘ A = r ↾⇩∘ A" by auto

lemma vrestriction_vrrestriction[simp]: "(r ↾⇩∘ A) ↾⇧r⇩∘ A = r ↾⇩∘ A" by auto

text‹Special properties.›

lemma vrestriction_vsubset_vpairs: "r ↾⇩∘ A ⊆⇩∘ vpairs r" by auto

lemma vrestriction_vsubset_vtimes: "r ↾⇩∘ A ⊆⇩∘ A ×⇩∘ A" by auto

lemma vrestriction_vsubset_rel: "r ↾⇩∘ A ⊆⇩∘ r" by auto

subsection‹Properties›

subsubsection‹Domain›

definition vdomain :: "V ⇒ V"
where "vdomain D = (λr∈⇩∘D. set {a. ∃b. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vdomain :: "V ⇒ V" (‹𝒟⇩∘›)
where "𝒟⇩∘ r ≡ vdomain (set {r}) ⦇r⦈"

lemma app_vdomain_def: "𝒟⇩∘ r = set {a. ∃b. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vdomain_def by simp

lemma vdomain_small[simp]: "small {a. ∃b. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b. ⟨a, b⟩ ∈⇩∘ r} ⊆ vfst  elts r" using image_iff by fastforce
have small: "small (vfst  elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma vdomainI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, 𝒟⇩∘ r⟩ ∈⇩∘ vdomain A"
using assms unfolding vdomain_def by auto

lemma vdomainD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vdomain A"
shows "r ∈⇩∘ A" and "s = 𝒟⇩∘ r"
using assms unfolding vdomain_def by auto

lemma vdomainE[elim]:
assumes "x ∈⇩∘ vdomain A"
obtains r where "x = ⟨r, 𝒟⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vdomain_def by auto

lemma app_vdomainI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "a ∈⇩∘ 𝒟⇩∘ r"
using assms unfolding vdomain_def by auto

lemma app_vdomainD[dest]:
assumes "a ∈⇩∘ 𝒟⇩∘ r"
shows "∃b. ⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vdomain_def by auto

lemma app_vdomainE[elim]:
assumes "a ∈⇩∘ 𝒟⇩∘ r"
obtains b where "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vdomain_def by clarsimp

lemma vdomain_iff: "a ∈⇩∘ 𝒟⇩∘ r ⟷ (∃y. ⟨a, y⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vdomain_vempty[simp]: "𝒟⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vdomain_vsingleton[simp]: "𝒟⇩∘ (set {⟨a, b⟩}) = set {a}" by auto

lemma vdomain_vdoubleton[simp]: "𝒟⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {a, c}"
by (auto simp: vinsert_set_insert_eq)

lemma vdomain_mono:
assumes "r ⊆⇩∘ s"
shows "𝒟⇩∘ r ⊆⇩∘ 𝒟⇩∘ s"
using assms by blast

lemma vdomain_vinsert[simp]: "𝒟⇩∘ (vinsert ⟨a, b⟩ r) = vinsert a (𝒟⇩∘ r)"
by (auto intro!: vsubset_antisym)

lemma vdomain_vunion: "𝒟⇩∘ (A ∪⇩∘ B) = 𝒟⇩∘ A ∪⇩∘ 𝒟⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma vdomain_vintersection_vsubset: "𝒟⇩∘ (A ∩⇩∘ B) ⊆⇩∘ 𝒟⇩∘ A ∩⇩∘ 𝒟⇩∘ B" by auto

lemma vdomain_vdiff_vsubset: "𝒟⇩∘ A -⇩∘ 𝒟⇩∘ B ⊆⇩∘ 𝒟⇩∘ (A -⇩∘ B)" by auto

text‹Connections.›

lemma vdomain_vid_on[simp]: "𝒟⇩∘ (vid_on A) = A"
by (auto intro!: vsubset_antisym)

lemma vdomain_vconst_on[simp]: "𝒟⇩∘ (vconst_on A c) = A"
by (auto intro!: vsubset_antisym)

lemma vdomain_VLambda[simp]: "𝒟⇩∘ (λa∈⇩∘A. f a) = A"
by (auto intro!: vsubset_antisym)

lemma vdomain_vlrestriction: "𝒟⇩∘ (r ↾⇧l⇩∘ A) = 𝒟⇩∘ r ∩⇩∘ A" by auto

text‹Special properties.›

lemma vdomain_vsubset_vtimes:
assumes "vpairs r ⊆⇩∘ x ×⇩∘ y"
shows "𝒟⇩∘ r ⊆⇩∘ x"
using assms by auto

subsubsection‹Range›

definition vrange :: "V ⇒ V"
where "vrange D = (λr∈⇩∘D. set {b. ∃a. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrange :: "V ⇒ V" (‹ℛ⇩∘›)
where "ℛ⇩∘ r ≡ vrange (set {r}) ⦇r⦈"

lemma app_vrange_def: "ℛ⇩∘ r = set {b. ∃a. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrange_def by simp

lemma vrange_small[simp]: "small {b. ∃a. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{b. ∃a. ⟨a, b⟩ ∈⇩∘ r} ⊆ vsnd  elts r" using image_iff by fastforce
have small: "small (vsnd  elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma vrangeI[intro]:
assumes "r ∈⇩∘ A"
shows "⟨r, ℛ⇩∘ r⟩ ∈⇩∘ vrange A"
using assms unfolding vrange_def by auto

lemma vrangeD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vrange A"
shows "r ∈⇩∘ A" and "s = ℛ⇩∘ r"
using assms unfolding vrange_def by auto

lemma vrangeE[elim]:
assumes "x ∈⇩∘ vrange A"
obtains r where "x = ⟨r, ℛ⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vrange_def by auto

lemma app_vrangeI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "b ∈⇩∘ ℛ⇩∘ r"
using assms unfolding vrange_def by auto

lemma app_vrangeD[dest]:
assumes "b ∈⇩∘ ℛ⇩∘ r"
shows "∃a. ⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrange_def by simp

lemma app_vrangeE[elim]:
assumes "b ∈⇩∘ ℛ⇩∘ r"
obtains a where "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrange_def by clarsimp

lemma vrange_iff: "b ∈⇩∘ ℛ⇩∘ r ⟷ (∃a. ⟨a, b⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vrange_vempty[simp]: "ℛ⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vrange_vsingleton[simp]: "ℛ⇩∘ (set {⟨a, b⟩}) = set {b}" by auto

lemma vrange_vdoubleton[simp]: "ℛ⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {b, d}"
by (auto simp: vinsert_set_insert_eq)

lemma vrange_mono:
assumes "r ⊆⇩∘ s"
shows "ℛ⇩∘ r ⊆⇩∘ ℛ⇩∘ s"
using assms by force

lemma vrange_vinsert[simp]: "ℛ⇩∘ (vinsert ⟨a, b⟩ r) = vinsert b (ℛ⇩∘ r)"
by (auto intro!: vsubset_antisym)

lemma vrange_vunion: "ℛ⇩∘ (r ∪⇩∘ s) = ℛ⇩∘ r ∪⇩∘ ℛ⇩∘ s"
by (auto intro!: vsubset_antisym)

lemma vrange_vintersection_vsubset: "ℛ⇩∘ (r ∩⇩∘ s) ⊆⇩∘ ℛ⇩∘ r ∩⇩∘ ℛ⇩∘ s" by auto

lemma vrange_vdiff_vsubset: "ℛ⇩∘ r -⇩∘ ℛ⇩∘ s ⊆⇩∘ ℛ⇩∘ (r -⇩∘ s)" by auto

text‹Connections.›

lemma vrange_vid_on[simp]: "ℛ⇩∘ (vid_on A) = A" by (auto intro!: vsubset_antisym)

lemma vrange_vconst_on_vempty[simp]: "ℛ⇩∘ (vconst_on 0 c) = 0" by auto

lemma vrange_vconst_on_ne[simp]:
assumes "A ≠ 0"
shows "ℛ⇩∘ (vconst_on A c) = set {c}"
using assms by (auto intro!: vsubset_antisym)

lemma vrange_VLambda: "ℛ⇩∘ (λa∈⇩∘A. f a) = set (f  elts A)"
by (intro vsubset_antisym vsubsetI) auto

lemma vrange_vrrestriction: "ℛ⇩∘ (r ↾⇧r⇩∘ A) = ℛ⇩∘ r ∩⇩∘ A" by auto

text‹Previous connections›

lemma vdomain_vconverse[simp]: "𝒟⇩∘ (r¯⇩∘) = ℛ⇩∘ r"
by (auto intro!: vsubset_antisym)

lemma vrange_vconverse[simp]: "ℛ⇩∘ (r¯⇩∘) = 𝒟⇩∘ r"
by (auto intro!: vsubset_antisym)

text‹Special properties.›

lemma vrange_iff_vdomain: "b ∈⇩∘ ℛ⇩∘ r ⟷ (∃a∈⇩∘𝒟⇩∘ r. ⟨a, b⟩ ∈⇩∘ r)" by auto

lemma vrange_vsubset_vtimes:
assumes "vpairs r ⊆⇩∘ x ×⇩∘ y"
shows "ℛ⇩∘ r ⊆⇩∘ y"
using assms by auto

lemma vrange_VLambda_vsubset:
assumes "⋀x. x ∈⇩∘ A ⟹ f x ∈⇩∘ B"
shows "ℛ⇩∘ (VLambda A f) ⊆⇩∘ B"
using assms by auto

lemma vpairs_vsubset_vdomain_vrange[simp]: "vpairs r ⊆⇩∘ 𝒟⇩∘ r ×⇩∘ ℛ⇩∘ r"
by (rule vsubsetI) auto

lemma vrange_vsubset:
assumes "⋀x y. ⟨x, y⟩ ∈⇩∘ r ⟹ y ∈⇩∘ A"
shows "ℛ⇩∘ r ⊆⇩∘ A"
using assms by auto

subsubsection‹Field›

definition vfield :: "V ⇒ V"
where "vfield D = (λr∈⇩∘D. 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r)"

abbreviation app_vfield :: "V ⇒ V" (‹ℱ⇩∘›)
where "ℱ⇩∘ r ≡ vfield (set {r}) ⦇r⦈"

lemma app_vfield_def: "ℱ⇩∘ r = 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r" unfolding vfield_def by simp

text‹Rules.›

lemma vfieldI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, ℱ⇩∘ r⟩ ∈⇩∘ vfield A"
using assms unfolding vfield_def by auto

lemma vfieldD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vfield A"
shows "r ∈⇩∘ A" and "s = ℱ⇩∘ r"
using assms unfolding vfield_def by auto

lemma vfieldE[elim]:
assumes "x ∈⇩∘ vfield A"
obtains r where "x = ⟨r, ℱ⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vfield_def by auto

lemma app_vfieldI1[intro]:
assumes "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r"
shows "a ∈⇩∘ ℱ⇩∘ r"
using assms unfolding vfield_def by simp

lemma app_vfieldI2[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "a ∈⇩∘ ℱ⇩∘ r"
using assms by auto

lemma app_vfieldI3[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "b ∈⇩∘ ℱ⇩∘ r"
using assms by auto

lemma app_vfieldD[dest]:
assumes "a ∈⇩∘ ℱ⇩∘ r"
shows "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r"
using assms unfolding vfield_def by simp

lemma app_vfieldE[elim]:
assumes "a ∈⇩∘ ℱ⇩∘ r" and "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r ⟹ P"
shows P
using assms by auto

lemma app_vfield_vpairE[elim]:
assumes "a ∈⇩∘ ℱ⇩∘ r"
obtains b where "⟨a, b⟩ ∈⇩∘ r ∨ ⟨b, a⟩ ∈⇩∘ r "
using assms unfolding app_vfield_def by blast

lemma vfield_iff: "a ∈⇩∘ ℱ⇩∘ r ⟷ (∃b. ⟨a, b⟩ ∈⇩∘ r ∨ ⟨b, a⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vfield_vempty[simp]: "ℱ⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vfield_vsingleton[simp]: "ℱ⇩∘ (set {⟨a, b⟩}) = set {a, b}"

lemma vfield_vdoubleton[simp]: "ℱ⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {a, b, c, d}"
by (auto simp: vinsert_set_insert_eq)

lemma vfield_mono:
assumes "r ⊆⇩∘ s"
shows "ℱ⇩∘ r ⊆⇩∘ ℱ⇩∘ s"
using assms by fastforce

lemma vfield_vinsert[simp]: "ℱ⇩∘ (vinsert ⟨a, b⟩ r) = set {a, b} ∪⇩∘ ℱ⇩∘ r"
by (auto intro!: vsubset_antisym)

lemma vfield_vunion[simp]: "ℱ⇩∘ (r ∪⇩∘ s) = ℱ⇩∘ r ∪⇩∘ ℱ⇩∘ s"
by (auto intro!: vsubset_antisym)

text‹Connections.›

lemma vid_on_vfield[simp]: "ℱ⇩∘ (vid_on A) = A" by (auto intro!: vsubset_antisym)

lemma vconst_on_vfield_ne[intro, simp]:
assumes "A ≠ 0"
shows "ℱ⇩∘ (vconst_on A c) = vinsert c A"
using assms by (auto intro!: vsubset_antisym)

lemma vconst_on_vfield_vempty[simp]: "ℱ⇩∘ (vconst_on 0 c) = 0" by auto

lemma vfield_vconverse[simp]: "ℱ⇩∘ (r¯⇩∘) = ℱ⇩∘ r"
by (auto intro!: vsubset_antisym)

subsubsection‹Image›

definition vimage :: "V ⇒ V"
where "vimage D = VLambda D (λ⟨r, A⟩. ℛ⇩∘ (r ↾⇧l⇩∘ A))"

abbreviation app_vimage :: "V ⇒ V ⇒ V" (infixr ‹⇩∘› 90)
where "r ⇩∘ A ≡ vimage (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vimage_def: "r ⇩∘ A = ℛ⇩∘ (r ↾⇧l⇩∘ A)" unfolding vimage_def by simp

lemma vimage_small[simp]: "small {b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r} ⊆ vsnd  elts r"
using image_iff by fastforce
have small: "small (vsnd  elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

lemma app_vimage_set_def: "r ⇩∘ A = set {b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vimage_def vrange_def by auto

text‹Rules.›

lemma vimageI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ⇩∘ A⟩ ∈⇩∘ vimage D"
using assms unfolding vimage_def by (simp add: VLambda_iff2)

lemma vimageD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vimage D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ⇩∘ A"
using assms unfolding vimage_def by auto

lemma vimageE[elim]:
assumes "x ∈⇩∘ vimage (R ×⇩∘ X)"
obtains r A where "x = ⟨⟨r, A⟩, r ⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vimage_def by auto

lemma app_vimageI1:
assumes "x ∈⇩∘ ℛ⇩∘ (r ↾⇧l⇩∘ A)"
shows "x ∈⇩∘ r ⇩∘ A"
using assms unfolding vimage_def by simp

lemma app_vimageI2[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r" and "a ∈⇩∘ A"
shows "b ∈⇩∘ r ⇩∘ A"
using assms app_vimageI1 by auto

lemma app_vimageD[dest]:
assumes "x ∈⇩∘ r ⇩∘ A"
shows "x ∈⇩∘ ℛ⇩∘ (r ↾⇧l⇩∘ A)"
using assms unfolding vimage_def by simp

lemma app_vimageE[elim]:
assumes "b ∈⇩∘ r ⇩∘ A"
obtains a where "⟨a, b⟩ ∈⇩∘ r" and "a ∈⇩∘ A"
using assms unfolding vimage_def by auto

lemma app_vimage_iff: "b ∈⇩∘ r ⇩∘ A ⟷ (∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vimage_vempty[simp]: "0 ⇩∘ A = 0" by (auto intro!: vsubset_antisym)

lemma vimage_of_vempty[simp]: "r ⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vimage_vsingleton: "r ⇩∘ set {a} = set {b. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have "{b. ⟨a, b⟩ ∈⇩∘ r} ⊆ {b. ∃a. ⟨a, b⟩ ∈⇩∘ r}" by auto
then have [simp]: "small {b. ⟨a, b⟩ ∈⇩∘ r}"
by (rule smaller_than_small[OF vrange_small[of r]])
show ?thesis using app_vimage_set_def by auto
qed

lemma vimage_vsingleton_in[intro, simp]:
assumes "a ∈⇩∘ A"
shows "set {⟨a, b⟩} ⇩∘ A = set {b}"
using assms by auto

lemma vimage_vsingleton_nin[intro, simp]:
assumes "a ∉⇩∘ A"
shows "set {⟨a, b⟩} ⇩∘ A = 0"
using assms by auto

lemma vimage_vsingleton_vinsert[simp]: "set {⟨a, b⟩} ⇩∘ vinsert a A = set {b}"
by auto

lemma vimage_mono:
assumes "r' ⊆⇩∘ r" and "A' ⊆⇩∘ A"
shows "(r' ⇩∘ A') ⊆⇩∘ (r ⇩∘ A)"
using assms by fastforce

lemma vimage_vinsert: "r ⇩∘ (vinsert a A) = r ⇩∘ set {a} ∪⇩∘ r ⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vimage_vunion_left: "(r ∪⇩∘ s) ⇩∘ A = r ⇩∘ A ∪⇩∘ s ⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vimage_vunion_right: "r ⇩∘ (A ∪⇩∘ B) = r ⇩∘ A ∪⇩∘ r ⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma vimage_vintersection: "r ⇩∘ (A ∩⇩∘ B) ⊆⇩∘ r ⇩∘ A ∩⇩∘ r ⇩∘ B" by auto

lemma vimage_vdiff: "r ⇩∘ A -⇩∘ r ⇩∘ B ⊆⇩∘ r ⇩∘ (A -⇩∘ B)" by auto

text‹Previous set operations.›

lemma VPow_vinsert:
"VPow (vinsert a A) = VPow A ∪⇩∘ ((λx∈⇩∘VPow A. vinsert a x) ⇩∘ VPow A)"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ VPow (vinsert a A)"
then have "x ⊆⇩∘ vinsert a A" by simp
then consider "x ⊆⇩∘ A" | "a ∈⇩∘ x" by auto
then show "x ∈⇩∘ VPow A ∪⇩∘ (λx∈⇩∘VPow A. vinsert a x) ⇩∘ VPow A"
proof cases
case 1 then show ?thesis by simp
next
case 2
define x' where "x' = x -⇩∘ set {a}"
with 2 have "x = vinsert a x'" and "a ∉⇩∘ x'" by auto
with ‹x ⊆⇩∘ vinsert a A› show ?thesis
unfolding vimage_def
by (fastforce simp: vsubset_vinsert vlrestriction_VLambda)
qed
qed (elim vunionE, auto)

text‹Special properties.›

lemma vimage_vsingleton_iff[iff]: "b ∈⇩∘ r ⇩∘ set {a} ⟷ ⟨a, b⟩ ∈⇩∘ r" by auto

lemma vimage_is_vempty[iff]: "r ⇩∘ A = 0 ⟷ vdisjnt (𝒟⇩∘ r) A" by fastforce

lemma vcomp_vimage_vtimes_right:
assumes "r ⇩∘ Y = Z"
shows "r ∘⇩∘ (X ×⇩∘ Y) = X ×⇩∘ Z"
proof(intro vsubset_antisym vsubsetI)
fix x assume x: "x ∈⇩∘ r ∘⇩∘ (X ×⇩∘ Y)"
then obtain a c where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ X" and "c ∈⇩∘ ℛ⇩∘ r" by auto
with x obtain b where "⟨a, b⟩ ∈⇩∘ X ×⇩∘ Y" and "⟨b, c⟩ ∈⇩∘ r" by clarsimp
then show "x ∈⇩∘ X ×⇩∘ Z" unfolding x_def using assms by auto
next
fix x assume "x ∈⇩∘ X ×⇩∘ Z"
then obtain a c where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ X" and "c ∈⇩∘ Z" by auto
then show "x ∈⇩∘ r ∘⇩∘ X ×⇩∘ Y"
using assms unfolding x_def by (meson VSigmaI app_vimageE vcompI)
qed

text‹Connections.›

lemma vid_on_vimage[simp]: "vid_on A ⇩∘ B = A ∩⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma vimage_vconst_on_ne[simp]:
assumes "B ∩⇩∘ A ≠ 0"
shows "vconst_on A c ⇩∘ B = set {c}"
using assms by auto

lemma vimage_vconst_on_vempty[simp]:
assumes "vdisjnt A B"
shows "vconst_on A c ⇩∘ B = 0"
using assms by auto

lemma vimage_vconst_on_vsubset_vconst: "vconst_on A c ⇩∘ B ⊆⇩∘ set {c}" by auto

lemma vimage_VLambda_vrange: "(λa∈⇩∘A. f a) ⇩∘ B = ℛ⇩∘ (λa∈⇩∘A ∩⇩∘ B. f a)"
unfolding vimage_def by (simp add: vlrestriction_VLambda)

lemma vimage_VLambda_vrange_rep: "(λa∈⇩∘A. f a) ⇩∘ A = ℛ⇩∘ (λa∈⇩∘A. f a)"

lemma vcomp_vimage: "(r ∘⇩∘ s) ⇩∘ A = r ⇩∘ (s ⇩∘ A)"
by (auto intro!: vsubset_antisym)

lemma vimage_vlrestriction[simp]: "(r ↾⇧l⇩∘ A) ⇩∘ B = r ⇩∘ (A ∩⇩∘ B)"
by (auto intro!: vsubset_antisym)

lemma vimage_vrrestriction[simp]: "(r ↾⇧r⇩∘ A) ⇩∘ B = A ∩⇩∘ r ⇩∘ B" by auto

lemma vimage_vrestriction[simp]: "(r ↾⇩∘ A) ⇩∘ B = A ∩⇩∘ (r ⇩∘ (A ∩⇩∘ B))" by auto

lemma vimage_vdomain: "r ⇩∘ 𝒟⇩∘ r = ℛ⇩∘ r" by (auto intro!: vsubset_antisym)

lemma vimage_eq_imp_vcomp:
assumes "r ⇩∘ A = s ⇩∘ B"
shows "(t ∘⇩∘ r) ⇩∘ A = (t ∘⇩∘ s) ⇩∘ B"
using assms by (metis vcomp_vimage)

text‹Previous connections.›

lemma vcomp_rel_vconst: "r ∘⇩∘ (vconst_on A c) = A ×⇩∘ (r ⇩∘ set {c})"
by auto

lemma vcomp_VLambda:
"(λb∈⇩∘((λa∈⇩∘A. g a) ⇩∘ A). f b) ∘⇩∘ (λa∈⇩∘A. g a) = (λa∈⇩∘A. (f ∘ g) a)"
using VLambda_iff1 by (auto intro!: vsubset_antisym)+

text‹Further special properties.›

lemma vimage_vsubset:
assumes "r ⊆⇩∘ A ×⇩∘ B"
shows "r ⇩∘ C ⊆⇩∘ B"
using assms by auto

lemma vimage_vdomain_vsubset: "r ⇩∘ A ⊆⇩∘ r ⇩∘ 𝒟⇩∘ r" by auto

lemma vdomain_vsubset_VUnion2: "𝒟⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ 𝒟⇩∘ r"
then obtain y where "⟨x, y⟩ ∈⇩∘ r" by auto
then have "set {set {x}, set {x, y}} ∈⇩∘ r" unfolding vpair_def by auto
with insert_commute have xy_Ur: "set {x, y} ∈⇩∘ ⋃⇩∘r"
unfolding VUnion_iff by auto
define Ur where "Ur = ⋃⇩∘r"
from xy_Ur show "x ∈⇩∘ ⋃⇩∘(⋃⇩∘r)"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

lemma vrange_vsubset_VUnion2: "ℛ⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
proof(intro vsubsetI)
fix y assume "y ∈⇩∘ ℛ⇩∘ r"
then obtain x where "⟨x, y⟩ ∈⇩∘ r" by auto
then have "set {set {x}, set {x, y}} ∈⇩∘ r" unfolding vpair_def by auto
with insert_commute have xy_Ur: "set {x, y} ∈⇩∘ ⋃⇩∘r"
unfolding VUnion_iff by auto
define Ur where "Ur = ⋃⇩∘r"
from xy_Ur show "y ∈⇩∘ ⋃⇩∘(⋃⇩∘r)"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

lemma vfield_vsubset_VUnion2: "ℱ⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
using vdomain_vsubset_VUnion2 vrange_vsubset_VUnion2
by (auto simp: app_vfield_def)

subsubsection‹Inverse image›

definition invimage :: "V ⇒ V"
where "invimage D = VLambda D (λ⟨r, A⟩. r¯⇩∘ ⇩∘ A)"

abbreviation app_invimage :: "V ⇒ V ⇒ V" (infixr ‹-⇩∘› 90)
where "r -⇩∘ A ≡ invimage (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_invimage_def: "r -⇩∘ A = r¯⇩∘ ⇩∘ A" unfolding invimage_def by simp

lemma invimage_small[simp]: "small {a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r} ⊆ vfst  elts r"
using image_iff by fastforce
have small: "small (vfst  elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma invimageI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r -⇩∘ A⟩ ∈⇩∘ invimage D"
using assms unfolding invimage_def by (simp add: VLambda_iff2)

lemma invimageD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ invimage D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r -⇩∘ A"
using assms unfolding invimage_def by auto

lemma invimageE[elim]:
assumes "x ∈⇩∘ invimage D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r -⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding invimage_def by auto

lemma app_invimageI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A"
shows "a ∈⇩∘ r -⇩∘ A"
using assms invimage_def by auto

lemma app_invimageD[dest]:
assumes "a ∈⇩∘ r -⇩∘ A"
shows "a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A)"
using assms using invimage_def by auto

lemma app_invimageE[elim]:
assumes "a ∈⇩∘ r -⇩∘ A"
obtains b where "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A"
using assms unfolding invimage_def by auto

lemma app_invimageI1:
assumes "a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A)"
shows "a ∈⇩∘ r -⇩∘ A"
using assms unfolding vimage_def
by (simp add: invimage_def app_vimageI1 vlrestriction_vconverse)

lemma app_invimageD1:
assumes "a ∈⇩∘ r -⇩∘ A"
shows "a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A)"
using assms by fastforce

lemma app_invimageE1:
assumes "a ∈⇩∘ r -⇩∘ A " and "a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A) ⟹ P"
shows P
using assms unfolding invimage_def by auto

lemma app_invimageI2:
assumes "a ∈⇩∘ r¯⇩∘ ⇩∘ A"
shows "a ∈⇩∘ r -⇩∘ A"
using assms unfolding invimage_def by simp

lemma app_invimageD2:
assumes "a ∈⇩∘ r -⇩∘ A"
shows "a ∈⇩∘ r¯⇩∘ ⇩∘ A"
using assms unfolding invimage_def by simp

lemma app_invimageE2:
assumes "a ∈⇩∘ r -⇩∘ A" and "a ∈⇩∘ r¯⇩∘ ⇩∘ A ⟹ P"
shows P
unfolding vimage_def by (simp add: assms app_invimageD2)

lemma invimage_iff: "a ∈⇩∘ r -⇩∘ A ⟷ (∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r)" by auto

lemma invimage_iff1: "a ∈⇩∘ r -⇩∘ A ⟷ a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A)" by auto

lemma invimage_iff2: "a ∈⇩∘ r -⇩∘ A ⟷ a ∈⇩∘ r¯⇩∘ ⇩∘ A" by auto

text‹Set operations.›

lemma invimage_vempty[simp]: "0 -⇩∘ A = 0" by (auto intro!: vsubset_antisym)

lemma invimage_of_vempty[simp]: "r -⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma invimage_vsingleton_in[intro, simp]:
assumes "b ∈⇩∘ A"
shows "set {⟨a, b⟩} -⇩∘ A = set {a}"
using assms by auto

lemma invimage_vsingleton_nin[intro, simp]:
assumes "b ∉⇩∘ A"
shows "set {⟨a, b⟩} -⇩∘ A = 0"
using assms by auto

lemma invimage_vsingleton_vinsert[intro, simp]:
"set {⟨a, b⟩} -⇩∘ vinsert b A = set {a}"
by auto

lemma invimage_mono:
assumes "r' ⊆⇩∘ r" and "A' ⊆⇩∘ A"
shows "(r' -⇩∘ A') ⊆⇩∘ (r -⇩∘ A)"
using assms by fastforce

lemma invimage_vinsert: "r -⇩∘ (vinsert a A) = r -⇩∘ set {a} ∪⇩∘ r -⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma invimage_vunion_left: "(r ∪⇩∘ s) -⇩∘ A = r -⇩∘ A ∪⇩∘ s -⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma invimage_vunion_right: "r -⇩∘ (A ∪⇩∘ B) = r -⇩∘ A ∪⇩∘ r -⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma invimage_vintersection: "r -⇩∘ (A ∩⇩∘ B) ⊆⇩∘ r -⇩∘ A ∩⇩∘ r -⇩∘ B" by auto

lemma invimage_vdiff: "r -⇩∘ A -⇩∘ r -⇩∘ B ⊆⇩∘ r -⇩∘ (A -⇩∘ B)" by auto

text‹Special properties.›

lemma invimage_set_def: "r -⇩∘ A = set {a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}" by fastforce

lemma invimage_eq_vdomain_vrestriction: "r -⇩∘ A = 𝒟⇩∘ (r ↾⇧r⇩∘ A)" by fastforce

lemma invimage_vrange[simp]: "r -⇩∘ ℛ⇩∘ r = 𝒟⇩∘ r"
unfolding invimage_def by (auto intro!: vsubset_antisym)

lemma invimage_vrange_vsubset[simp]:
assumes "ℛ⇩∘ r ⊆⇩∘ B"
shows "r -⇩∘ B = 𝒟⇩∘ r"
using assms unfolding app_invimage_def by (blast intro!: vsubset_antisym)

text‹Connections.›

lemma invimage_vid_on[simp]: "vid_on A -⇩∘ B = A ∩⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma invimage_vconst_on_vsubset_vdomain[simp]: "vconst_on A c -⇩∘ B ⊆⇩∘ A"
unfolding invimage_def by auto

lemma invimage_vconst_on_ne[simp]:
assumes "c ∈⇩∘ B"
shows "vconst_on A c -⇩∘ B = A"
by (simp add: assms invimage_eq_vdomain_vrestriction vrrestriction_vconst_on)

lemma invimage_vconst_on_vempty[simp]:
assumes "c ∉⇩∘ B"
shows "vconst_on A c -⇩∘ B = 0"
using assms by auto

lemma invimage_vcomp: "(r ∘⇩∘ s) -⇩∘ x = s -⇩∘ (r -⇩∘ x) "
by (simp add: invimage_def vconverse_vcomp vcomp_vimage)

lemma invimage_vconverse[simp]: "r¯⇩∘ -⇩∘ A = r ⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma invimage_vlrestriction[simp]: "(r ↾⇧l⇩∘ A) -⇩∘ B = A ∩⇩∘ r -⇩∘ B" by auto

lemma invimage_vrrestriction[simp]: "(r ↾⇧r⇩∘ A) -⇩∘ B = (r -⇩∘ (A ∩⇩∘ B))"
by (auto intro!: vsubset_antisym)

lemma invimage_vrestriction[simp]: "(r ↾⇩∘ A) -⇩∘ B = A ∩⇩∘ (r -⇩∘ (A ∩⇩∘ B))"
by blast

text‹Previous connections.›

lemma vcomp_vconst_on_rel_vtimes: "vconst_on A c ∘⇩∘ r = (r -⇩∘ A) ×⇩∘ set {c}"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ r -⇩∘ A ×⇩∘ set {c}"
then obtain a where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ r -⇩∘ A" by auto
then obtain b where ab: "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A" using invimage_iff by auto
with ‹b ∈⇩∘ A› show "x ∈⇩∘ vconst_on A c ∘⇩∘ r" unfolding x_def by auto
qed auto

lemma vdomain_vcomp[simp]: "𝒟⇩∘ (r ∘⇩∘ s) = s -⇩∘ 𝒟⇩∘ r" by blast

lemma vrange_vcomp[simp]: "ℛ⇩∘ (r ∘⇩∘ s) = r ⇩∘ ℛ⇩∘ s" by blast

lemma vdomain_vcomp_vsubset:
assumes "ℛ⇩∘ s ⊆⇩∘ 𝒟⇩∘ r"
shows "𝒟⇩∘ (r ∘⇩∘ s) = 𝒟⇩∘ s"
using assms by simp

subsection‹Classification of relations›

subsubsection‹Binary relation›

locale vbrelation =
fixes r :: V
assumes vbrelation: "vpairs r = r"

text‹Rules.›

lemma vpairs_eqI[intro!]:
assumes "⋀x. x ∈⇩∘ r ⟹ ∃a b. x = ⟨a, b⟩"
shows "vpairs r = r"
using assms by auto

lemma vpairs_eqD[dest]:
assumes "vpairs r = r"
shows "⋀x. x ∈⇩∘ r ⟹ ∃a b. x = ⟨a, b⟩"
using assms by auto

lemma vpairs_eqE[elim!]:
assumes "vpairs r = r" and "(⋀x. x ∈⇩∘ r ⟹ ∃a b. x = ⟨a, b⟩) ⟹ P"
shows P
using assms by auto

lemmas vbrelationI[intro!] = vbrelation.intro
lemmas vbrelationD[dest!] = vbrelation.vbrelation

lemma vbrelationE[elim!]:
assumes "vbrelation r" and "(vpairs r = r) ⟹ P"
shows P
using assms unfolding vbrelation_def by auto

lemma vbrelationE1[elim]:
assumes "vbrelation r" and "x ∈⇩∘ r"
obtains a b where "x = ⟨a, b⟩"
using assms by auto

lemma vbrelationD1[dest]:
assumes "vbrelation r" and "x ∈⇩∘ r"
shows "∃a b. x = ⟨a, b⟩"
using assms by auto

lemma (in vbrelation) vbrelation_vinE:
assumes "x ∈⇩∘ r"
obtains a b where "x = ⟨a, b⟩" and "a ∈⇩∘ 𝒟⇩∘ r" and "b ∈⇩∘ ℛ⇩∘ r"
using assms vbrelation_axioms by blast

text‹Set operations.›

lemma vbrelation_vsubset:
assumes "vbrelation s" and "r ⊆⇩∘ s"
shows "vbrelation r"
using assms by auto

lemma vbrelation_vinsert[simp]: "vbrelation (vinsert ⟨a, b⟩ r) ⟷ vbrelation r"
by auto

lemma (in vbrelation) vbrelation_vinsertI[intro, simp]:
"vbrelation (vinsert ⟨a, b⟩ r)"
using vbrelation_axioms by auto

lemma vbrelation_vinsertD[dest]:
assumes "vbrelation (vinsert ⟨a, b⟩ r)"
shows "vbrelation r"
using assms by auto

lemma vbrelation_vunion: "vbrelation (r ∪⇩∘ s) ⟷ vbrelation r ∧ vbrelation s"
by auto

lemma vbrelation_vunionI:
assumes "vbrelation r" and "vbrelation s"
shows "vbrelation (r ∪⇩∘ s)"
using assms by auto

lemma vbrelation_vunionD[dest]:
assumes "vbrelation (r ∪⇩∘ s)"
shows "vbrelation r" and "vbrelation s"
using assms by auto

lemma (in vbrelation) vbrelation_vintersectionI: "vbrelation (r ∩⇩∘ s)"
using vbrelation_axioms by auto

lemma (in vbrelation) vbrelation_vdiffI: "vbrelation (r -⇩∘ s)"
using vbrelation_axioms by auto

text‹Connections.›

lemma vbrelation_vempty: "vbrelation 0" by auto

lemma vbrelation_vsingleton: "vbrelation (set {⟨a, b⟩})" by auto

lemma vbrelation_vdoubleton: "vbrelation (set {⟨a, b⟩, ⟨c, d⟩})" by auto

lemma vbrelation_vid_on[simp]: "vbrelation (vid_on A)" by auto

lemma vbrelation_vconst_on[simp]: "vbrelation (vconst_on A c)" by auto

lemma vbrelation_VLambda[simp]: "vbrelation (VLambda A f)"
unfolding VLambda_def by (intro vbrelationI) auto

global_interpretation rel_VLambda: vbrelation ‹VLambda U f›
by (rule vbrelation_VLambda)

lemma vbrelation_vcomp:
assumes "vbrelation r" and "vbrelation s"
shows "vbrelation (r ∘⇩∘ s)"
using assms by auto

lemma (in vbrelation) vbrelation_vconverse: "vbrelation (r¯⇩∘)"
using vbrelation_axioms by clarsimp

lemma vbrelation_vlrestriction[intro, simp]: "vbrelation (r ↾⇧l⇩∘ A)" by auto

lemma vbrelation_vrrestriction[intro, simp]: "vbrelation (r ↾⇧r⇩∘ A)" by auto

lemma vbrelation_vrestriction[intro, simp]: "vbrelation (r ↾⇩∘ A)" by auto

text‹Previous connections.›

lemma (in vbrelation) vconverse_vconverse[simp]: "(r¯⇩∘)¯⇩∘ = r"
using vbrelation_axioms by auto

lemma vconverse_mono[simp]:
assumes "vbrelation r" and "vbrelation s"
shows "r¯⇩∘ ⊆⇩∘ s¯⇩∘ ⟷ r ⊆⇩∘ s"
using assms by (force intro: vconverse_vunion)+

lemma vconverse_inject[simp]:
assumes "vbrelation r" and "vbrelation s"
shows "r¯⇩∘ = s¯⇩∘ ⟷ r = s"
using assms by fast

lemma (in vbrelation) vconverse_vsubset_swap_2:
assumes "r¯⇩∘ ⊆⇩∘ s"
shows "r ⊆⇩∘ s¯⇩∘"
using assms vbrelation_axioms by auto

lemma (in vbrelation) vlrestriction_vdomain[simp]: "r ↾⇧l⇩∘ 𝒟⇩∘ r = r"
using vbrelation_axioms by (elim vbrelationE) auto

lemma (in vbrelation) vrrestriction_vrange[simp]: "r ↾⇧r⇩∘ ℛ⇩∘ r = r"
using vbrelation_axioms by (elim vbrelationE) auto

text‹Special properties.›

lemma brel_vsubset_vtimes:
"vbrelation r ⟷ r ⊆⇩∘ set (vfst  elts r) ×⇩∘ set (vsnd  elts r)"
by force

lemma vsubset_vtimes_vbrelation:
assumes "r ⊆⇩∘ A ×⇩∘ B"
shows "vbrelation r"
using assms by auto

lemma (in vbrelation) vbrelation_vintersection_vdomain:
assumes "vdisjnt (𝒟⇩∘ r) (𝒟⇩∘ s)"
shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "⟨a, b⟩ ∈⇩∘ r ∩⇩∘ s"
by (metis vbrelationE1 vbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed simp

lemma (in vbrelation) vbrelation_vintersection_vrange:
assumes "vdisjnt (ℛ⇩∘ r) (ℛ⇩∘ s)"
shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "⟨a, b⟩ ∈⇩∘ r ∩⇩∘ s"
by (metis vbrelationE1 vbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed simp

lemma (in vbrelation) vbrelation_vintersection_vfield:
assumes "vdisjnt (vfield r) (vfield s)"
shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "⟨a, b⟩ ∈⇩∘ r ∩⇩∘ s"
by (metis vbrelationE1 vbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed auto

lemma (in vbrelation) vdomain_vrange_vtimes: "r ⊆⇩∘ 𝒟⇩∘ r ×⇩∘ ℛ⇩∘ r"
using vbrelation by auto

lemma (in vbrelation) vbrelation_vsubset_vtimes:
assumes "𝒟⇩∘ r ⊆⇩∘ A" and "ℛ⇩∘ r ⊆⇩∘ B"
shows "r ⊆⇩∘ A ×⇩∘ B"
proof(intro vsubsetI)
fix x assume prems: "x ∈⇩∘ r"
with vbrelation obtain a b where x_def: "x = ⟨a, b⟩" by auto
from prems have a: "a ∈⇩∘ 𝒟⇩∘ r" and b: "b ∈⇩∘ ℛ⇩∘ r" unfolding x_def by auto
with assms have "a ∈⇩∘ A" and "b ∈⇩∘ B" by auto
then show "x ∈⇩∘ A ×⇩∘ B" unfolding x_def by simp
qed

lemma (in vbrelation) vlrestriction_vsubset_vrange[intro, simp]:
assumes "𝒟⇩∘ r ⊆⇩∘ A"
shows "r ↾⇧l⇩∘ A = r"
proof(intro vsubset_antisym)
show "r ⊆⇩∘ r ↾⇧l⇩∘ A"
by (rule vlrestriction_mono[OF assms, of r, unfolded vlrestriction_vdomain])
qed auto

lemma (in vbrelation) vrrestriction_vsubset_vrange[intro, simp]:
assumes "ℛ⇩∘ r ⊆⇩∘ B"
shows "r ↾⇧r⇩∘ B = r"
proof(intro vsubset_antisym)
show "r ⊆⇩∘ r ↾⇧r⇩∘ B"
by (rule vrrestriction_mono[OF assms, of r, unfolded vrrestriction_vrange])
qed auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_left[simp]:
assumes "ℛ⇩∘ r ⊆⇩∘ A"
shows "vid_on A ∘⇩∘ r = r"
using assms by auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_right[simp]:
assumes "𝒟⇩∘ r ⊆⇩∘ A"
shows "r ∘⇩∘ vid_on A = r"
using assms by auto

text‹Alternative forms of existing results.›

lemmas [intro, simp] = vbrelation.vconverse_vconverse
and [intro, simp] = vbrelation.vlrestriction_vsubset_vrange
and [intro, simp] = vbrelation.vrrestriction_vsubset_vrange

subsubsection‹Simple single-valued relation›

locale vsv = vbrelation r for r +
assumes vsv: "⟦ ⟨a, b⟩ ∈⇩∘ r; ⟨a, c⟩ ∈⇩∘ r ⟧ ⟹ b = c"

text‹Rules.›

lemmas (in vsv) [intro] = vsv_axioms

mk_ide rf vsv_def[unfolded vsv_axioms_def]
|intro vsvI[intro]|
|dest vsvD[dest]|
|elim vsvE[elim]|

text‹Set operations.›

lemma (in vsv) vsv_vinsert[simp]:
assumes "a ∉⇩∘ 𝒟⇩∘ r"
shows "vsv (vinsert ⟨a, b⟩ r)"
using assms vsv_axioms by blast

lemma vsv_vinsertD:
assumes "vsv (vinsert x r)"
shows "vsv r"
using assms by (intro vsvI) auto

lemma vsv_vunion[intro, simp]:
assumes "vsv r" and "vsv s" and "vdisjnt (𝒟⇩∘ r) (𝒟⇩∘ s)"
shows "vsv (r ∪⇩∘ s)"
proof
from assms have F: "⟦ ⟨a, b⟩ ∈⇩∘ r; ⟨a, c⟩ ∈⇩∘ s ⟧ ⟹ False" for a b c
using elts_0 by blast
fix a b c assume "⟨a, b⟩ ∈⇩∘ r ∪⇩∘ s" and "⟨a, c⟩ ∈⇩∘ r ∪⇩∘ s"
then consider
"⟨a, b⟩ ∈⇩∘ r ∧ ⟨a, c⟩ ∈⇩∘ r"
| "⟨a, b⟩ ∈⇩∘ r ∧ ⟨a, c⟩ ∈⇩∘ s"
| "⟨a, b⟩ ∈⇩∘ s ∧ ⟨a, c⟩ ∈⇩∘ r"
| "⟨a, b⟩ ∈⇩∘ s ∧ ⟨a, c⟩ ∈⇩∘ s"
by blast
then show "b = c" using assms by cases auto
qed (use assms in auto)

lemma (in vsv) vsv_vintersection[intro, simp]: "vsv (r ∩⇩∘ s)"
using vsv_axioms by blast

lemma (in vsv) vsv_vdiff[intro, simp]: "vsv (r -⇩∘ s)" using vsv_axioms by blast

text‹Connections.›

lemma vsv_vempty[simp]: "vsv 0" by auto

lemma vsv_vsingleton[simp]: "vsv (set {⟨a, b⟩})" by auto

global_interpretation rel_vsingleton: vsv ‹set {⟨a, b⟩}›
by (rule vsv_vsingleton)

lemma vsv_vdoubleton:
assumes "a ≠ c"
shows "vsv (set {⟨a, b⟩, ⟨c, d⟩})"
using assms by (auto simp: vinsert_set_insert_eq)

lemma vsv_vid_on[simp]: "vsv (vid_on A)" by auto

lemma vsv_vconst_on[simp]: "vsv (vconst_on A c)" by auto

lemma vsv_VLambda[simp]: "vsv (λa∈⇩∘A. f a)" by auto

global_interpretation rel_VLambda: vsv ‹(λa∈⇩∘A. f a)›
unfolding VLambda_def by (intro vsvI) auto

lemma vsv_vcomp:
assumes "vsv r" and "vsv s"
shows "vsv (r ∘⇩∘ s)"
using assms
by (intro vsvI; elim vsvE) (simp add: vbrelation_vcomp, metis vcompD)

lemma (in vsv) vsv_vlrestriction[intro, simp]: "vsv (r ↾⇧l⇩∘ A)"
using vsv_axioms by blast

lemma (in vsv) vsv_vrrestriction[intro, simp]: "vsv (r ↾⇧r⇩∘ A)"
using vsv_axioms by blast

lemma (in vsv) vsv_vrestriction[intro, simp]: `