# 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 _)" [12] 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)"
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 ("(_/ ββ©β _)" [51, 51] 50)

subsubsectionβΉSubsetsβΊ

abbreviation vsubset :: "V β V β bool"
where "vsubset β‘ less"
abbreviation vsubset_eq :: "V β V β bool"
where "vsubset_eq β‘ less_eq"

and vsubset ("(_/ ββ©β _)" [51, 51] 50)
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)"

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 vunion :: "V β V β V"  (infixl "βͺβ©β" 65)
where "vunion β‘ sup"

abbreviation VInter :: "V β V" (βΉββ©ββΊ)
where "ββ©β A β‘ β¨ (elts A)"

abbreviation VUnion :: "V β V" (βΉββ©ββΊ)
where "ββ©βA β‘ β¨ (elts A)"

subsubsectionβΉMiscellaneousβΊ

notation app (βΉ_β¦_β¦βΊ [999, 50] 999)

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"
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"
using assms by auto

lemma some_in_set_if_set_neq_vempty[simp]:
assumes "A β  0"
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:
shows "b β  a"
using assms by auto

lemma vset_neq_2:
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"
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"

lemma vball_cong_simp[cong]:
assumes "A = B" and "βx. x ββ©β B =simp=> P x β· 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"
using assms by (simp cong: conj_cong)

lemma vbex_cong_simp[cong]:
assumes "A = B" and "βx. x ββ©β B =simp=> P x β· Q x "
using assms by (simp add:  simp_implies_def)

subsectionβΉSubsetβΊ

textβΉRules.βΊ

lemma vsubset_antisym:
shows "A = B"
using assms by simp

lemma vsubsetI:
using assms by auto

lemma vpsubsetI:
using assms unfolding less_V_def by auto

lemma vsubsetD:
using assms by auto

lemma vsubsetE:
shows P
using assms by auto

lemma vpsubsetE:
using assms unfolding less_V_def by (meson V_equalityI vsubsetE)

textβΉElementary properties.βΊ

lemma vsubset_transitive[intro]:
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"
using assms by auto

lemma vsubset_vdoubleton_leftI[intro]:
shows "set {a, b} ββ©β A"
using assms by auto

lemma vsubset_vinsert_leftD[dest]:
assumes "vinsert a A ββ©β B"
using assms by auto

lemma vsubset_vinsert_leftI[intro]:
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]:
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.βΊ

using assms by auto

subsectionβΉEqualityβΊ

textβΉRules.βΊ

lemma vequalityD1:
assumes "A = B"
using assms by simp

lemma vequalityD2:
assumes "A = B"
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βΊ

by (metis Int_def inf_V_def)

by (rule down[of _ A]) auto

textβΉRules.βΊ

unfolding vintersection_def by simp

lemma vintersectionI[intro!]:
using assms by simp

lemma vintersectionD1[dest]:
using assms by simp

lemma vintersectionD2[dest]:
using assms by simp

lemma vintersectionE[elim!]:
shows P
using assms by simp

textβΉElementary properties.βΊ

unfolding inf_V_def by simp

textβΉPrevious set operations.βΊ

by clarsimp

lemma vsubset_vintersection_rightD[dest]:
using assms by auto

lemma vsubset_vintersection_rightI[intro]:
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

textβΉSpecial properties.βΊ

lemma vintersection_function_mono:
assumes "mono f"
using assms by (fact mono_inf)

subsectionβΉBinary unionβΊ

by (rule down[of _ βΉA βͺβ©β BβΊ]) (auto simp: elts_sup_iff)

textβΉRules.βΊ

unfolding Un_def sup_V_def by simp

lemma vunionI1:
using assms by simp

lemma vunionI2:
using assms by simp

lemma vunionCI[intro!]:
using assms by clarsimp

lemma vunionE[elim!]:
shows P
using assms by auto

textβΉElementary properties.βΊ

lemma vunion_union: "A βͺβ©β B = set (elts A βͺ elts B)" by auto

textβΉPrevious set operations.βΊ

lemma vsubset_vunion_leftD[dest]:
using assms by auto

lemma vsubset_vunion_leftI[intro]:
using assms by auto

by auto

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:
by auto

lemma vunion_vinsert_commutativity_right:
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"
using assms by (fact mono_sup)

subsectionβΉSet differenceβΊ

definition vdiff :: "V β V β V" (infixl βΉ-β©ββΊ 65)

by (rule down[of _ A]) simp

textβΉRules.βΊ

unfolding vdiff_def by simp

lemma vdiffI[intro!]:
using assms by simp

lemma vdiffD1:
using assms by simp

lemma vdiffD2:
shows P
using assms by simp

lemma vdiffE[elim!]:
shows P
using assms by simp

textβΉPrevious set operations.βΊ

lemma vsubset_vdiff:
using assms by auto

lemma vinsert_vdiff_nin[simp]:
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]:
shows "set {a} -β©β A = 0"
using assms by auto

lemma vdiff_vsingleton_nin[simp]:
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]:
shows "A -β©β set {a} = A"
using assms by auto

lemma vdiff_vsubset:
using assms by auto

lemma vdiff_vinsert_left_in[simp]:
using assms by auto

lemma vdiff_vinsert_left_nin:
shows "(vinsert a A) -β©β B = vinsert a (A -β©β B)"
using assms by auto

lemma vdiff_vinsert_right_nin[simp]:
using assms by auto

textβΉSpecial properties.βΊ

lemma vunion_complement:
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:
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:
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

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:
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:
using assms by simp

lemma VPowD:
using assms by (simp add: Pow_def)

lemma VPowE[elim]:
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:
shows "VPow A ββ©β VPow B"
using assms by simp

subsectionβΉSingletons, using insertβΊ

textβΉRules.βΊ

lemma vsingletonI[intro!]: "x ββ©β set {x}" by auto

lemma vsingletonD[dest!]:
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:
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:
shows "A = 0 β¨ A = set {x}"
using assms by auto

lemma vsubset_vsingleton_iff: "a ββ©β set {x} β· a = 0 β¨ a = set {x}" by auto

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"
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"
unfolding VInter_def by auto

lemma VInterI[intro]:
assumes "A β  0" and "βx. x ββ©β A βΉ a ββ©β x"
using assms by auto

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

lemma VInterD[dest]:
using assms by (cases βΉA = 0βΊ) auto

lemma VInterE1[elim]:
shows R
using assms elts_0 unfolding Inter_eq by blast

lemma VInterE2[elim]:
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*)
shows P
using assms by auto

textβΉElementary properties.βΊ

lemma VInter_Inter: "ββ©β A = set (β (elts  (elts A)))"

lemma VInter_eq:
assumes [simp]: "A β  0"
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)

proof(intro vsubset_antisym vsubsetI)
qed

lemma VInter_antimono:
assumes "B β  0" and "B ββ©β A"
using assms by blast

lemma VInter_vsubset:
assumes "βx. x ββ©β A βΉ x ββ©β B" and "A β  0"
using assms by auto

lemma VInter_vinsert:
assumes "A β  0"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vunion:
assumes "A β  0" and "B β  0"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vintersection:
using assms by auto

textβΉElementary properties.βΊ

lemma VInter_lower:
using assms by auto

lemma VInter_greatest:
assumes "A β  0" and "βx. x ββ©β A βΉ B ββ©β x"
using assms by auto

subsectionβΉUnion of elementsβΊ

lemma Union_eq_VUnion: "β(elts  elts A) = {a. βx ββ©β A. a ββ©β x}" by auto

by (fold Union_eq_VUnion) simp

unfolding Sup_V_def by auto

textβΉRules.βΊ

lemma VUnionI[intro]:
using assms by auto

lemma VUnionE[elim!]:
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_mono:
using assms 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 VUnion_vsubsetI:
using assms by auto

lemma VUnion_upper:
using assms by auto

lemma VUnion_least:
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β©)}"

by (rule down[of _ r]) clarsimp

textβΉRules.βΊ

lemma vpairsI[intro]:
using assms unfolding vpairs_def by auto

lemma vpairsD[dest]:
using assms unfolding vpairs_def by auto

lemma vpairsE[elim]:
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_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

by auto

lemma vpairs_mono:
shows "vpairs r ββ©β vpairs s"
using assms by blast

lemma vpairs_vunion: "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:
using assms by force

lemma vpairs_ex_vsnd:
using assms by force

subsectionβΉCartesian productsβΊ

textβΉ
The following lemma is based on Theorem 6.2 from
\cite{takeuti_introduction_1971}.
βΊ

proof(intro vsubsetI)
then obtain a b where x_def: "x = β¨a, bβ©" and "a ββ©β A" and "b ββ©β B" by clarsimp
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"

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]:
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"
using assms by auto

lemma vdisjnt_nin_left:
assumes "vdisjnt B A" and "a ββ©β A"
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.
βΊ

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βΊ

by (induct b) (simp_all add: plus_V_succ_right)

by (induct b) (simp_all add: mult_succ nat_omega_simps)

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:
obtains m where "n = mβ©β"
using assms unfolding Ο_def by clarsimp

lemma omega_prev:
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:
shows "a + b = b + a"
using assms by (metis Groups.add_ac(2) nat_of_omega ord_of_nat_plus)

lemma omega_vinetrsection[intro]:
proof-
from nat_into_Ord[OF assms(1)] nat_into_Ord[OF assms(2)] Ord_linear_le
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 βΉ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 "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
βΊ

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βΊ

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}"

by (rule down[of _ βΉA Γβ©β AβΊ]) blast

textβΉRules.βΊ

lemma vid_on_eqI:
assumes "a = b" and "a ββ©β A"
using assms by (simp add: vid_on_def)

lemma vid_onI[intro!]:
by (rule vid_on_eqI) (simp_all add: assms)

lemma vid_onD[dest!]:
using assms unfolding vid_on_def by auto

lemma vid_onE[elim!]:
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:
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_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.βΊ

subsubsectionβΉConstant functionβΊ

definition vconst_on :: "V β V β V"
where "vconst_on A c = set {β¨a, cβ© | a. a ββ©β A}"

by (rule down[of _ βΉA Γβ©β set {c}βΊ]) auto

textβΉRules.βΊ

lemma vconst_onI[intro!]:
using assms unfolding vconst_on_def by simp

lemma vconst_onD[dest!]:
using assms unfolding vconst_on_def by simp

lemma vconst_onE[elim!]:
assumes "x ββ©β vconst_on A c"
using assms unfolding vconst_on_def 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:
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:
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!]:
using assms unfolding VLambda_def by auto

using assms unfolding VLambda_def by auto

lemma VLambdaE[elim!]:
obtains a where "a ββ©β A" and "x = β¨a, f aβ©"
using assms unfolding VLambda_def 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*):
by (auto simp: vinsert_set_insert_eq)

lemma VLambda_mono:
using assms by auto

lemma VLambda_vinsert:
by auto

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)

(is βΉsmall ?sβΊ)
proof-
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β©"
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!]:
using assms unfolding vcomp_def by auto

lemma vcompD[dest!]:
using assms unfolding vcomp_def by auto

lemma vcompE[elim!]:
using assms unfolding vcomp_def by clarsimp

textβΉElementary properties.βΊ

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:
using assms by auto

lemma vcomp_vinsert_left[simp]:
by auto

lemma vcomp_vinsert_right[simp]:
by auto

textβΉConnections.βΊ

lemma vcomp_vid_on_idem[simp]: "vid_on A ββ©β vid_on A = vid_on A" by auto

lemma vcomp_vconst_on_vid_on[simp]: "vconst_on A c ββ©β vid_on A = vconst_on A c"
by auto

by auto

textβΉSpecial properties.βΊ

lemma vcomp_vsubset_vtimes:
using assms by auto

lemma vcomp_obtain_middle[elim]:
using assms by auto

subsubsectionβΉConverse relationβΊ

definition vconverse :: "V β V"

where "rΒ―β©β β‘ vconverse (set {r}) β¦rβ¦"

unfolding vconverse_def by simp

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)"
by blast
qed (use image_iff vpairs_iff_elts in fastforce)
show ?thesis unfolding eq by (rule replacement) auto
qed

textβΉRules.βΊ

lemma vconverseI[intro!]:
using assms unfolding vconverse_def by auto

lemma vconverseD[dest]:
using assms unfolding vconverse_def by auto

lemma vconverseE[elim]:
using assms unfolding vconverse_def by auto

lemma app_vconverseI[sym, intro!]:
using assms unfolding vconverse_def by auto

lemma app_vconverseD[sym, dest]:
using assms unfolding vconverse_def by simp

lemma app_vconverseE[elim!]:
using assms unfolding vconverse_def by auto

textβΉSet operations.βΊ

lemma vconverse_vempty[simp]: "0Β―β©β = 0" by auto

by (auto simp: vinsert_set_insert_eq)

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

subsubsectionβΉLeft restrictionβΊ

definition vlrestriction :: "V β V"
where "vlrestriction D =

abbreviation app_vlrestriction :: "V β V β V" (infixr βΉβΎβ§lβ©ββΊ 80)

unfolding vlrestriction_def by simp

by (rule down[of _ r]) auto

textβΉRules.βΊ

lemma vlrestrictionI[intro!]:
using assms unfolding vlrestriction_def by (simp add: VLambda_iff2)

lemma vlrestrictionD[dest]:
using assms unfolding vlrestriction_def by auto

lemma vlrestrictionE[elim]:
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionI[intro!]:
using assms unfolding vlrestriction_def by simp

lemma app_vlrestrictionD[dest]:
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionE[elim]:
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]:
using assms by auto

lemma vlrestriction_vsingleton_nin[simp]:
using assms by auto

lemma vlrestriction_mono:
using assms by auto

lemma vlrestriction_vinsert_nin[simp]:
using assms by auto

lemma vlrestriction_vinsert_in:
using assms by auto

textβΉConnections.βΊ

lemma vlrestriction_vconst_on: "(vconst_on A c) βΎβ§lβ©β B = (vconst_on B c) βΎβ§lβ©β A"
by auto

lemma vlrestriction_vconst_on_commute:
using assms by auto

textβΉPrevious connections.βΊ

lemma vcomp_rel_vid_on[simp]: "r ββ©β vid_on A = r βΎβ§lβ©β A" by auto

lemma vcomp_vconst_on:
by auto

textβΉSpecial properties.βΊ

by (rule vsubsetI) blast

subsubsectionβΉRight restrictionβΊ

definition vrrestriction :: "V β V"
where "vrrestriction D =

abbreviation app_vrrestriction :: "V β V β V" (infixr βΉβΎβ§rβ©ββΊ 80)

unfolding vrrestriction_def by simp

by (rule down[of _ r]) auto

textβΉRules.βΊ

lemma vrrestrictionI[intro!]:
using assms unfolding vrrestriction_def by (simp add: VLambda_iff2)

lemma vrrestrictionD[dest]:
using assms unfolding vrrestriction_def by auto

lemma vrrestrictionE[elim]:
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionI[intro!]:
using assms unfolding vrrestriction_def by simp

lemma app_vrrestrictionD[dest]:
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionE[elim]:
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]:
using assms by auto

lemma vrrestriction_vsingleton_nin[simp]:
using assms by auto

lemma vrrestriction_mono:
using assms by auto

lemma vrrestriction_vinsert_nin[simp]:
using assms by auto

lemma vrrestriction_vinsert_in:
using assms by auto

textβΉConnections.βΊ

lemma vrrestriction_vconst_on:
shows "(vconst_on A c) βΎβ§rβ©β B = vconst_on A c"
using assms by auto

textβΉPrevious connections.βΊ

by (auto intro!: vsubset_antisym)

by auto

textβΉSpecial properties.βΊ

subsubsectionβΉRestrictionβΊ

definition vrestriction :: "V β V"
where "vrestriction D =

abbreviation app_vrestriction :: "V β V β V" (infixr βΉβΎβ©ββΊ 80)

lemma app_vrestriction_def:
unfolding vrestriction_def by simp

lemma vrestriction_small[simp]:
by (rule down[of _ r]) auto

textβΉRules.βΊ

lemma vrestrictionI[intro!]:
using assms unfolding vrestriction_def by (simp add: VLambda_iff2)

lemma vrestrictionD[dest]:
using assms unfolding vrestriction_def by auto

lemma vrestrictionE[elim]:
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionI[intro!]:
using assms unfolding vrestriction_def by simp

lemma app_vrestrictionD[dest]:
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionE[elim]:
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]:
using assms by auto

lemma vrestriction_vsingleton_nin_left[simp]:
using assms by auto

lemma vrestriction_vsingleton_nin_right[simp]:
using assms by auto

lemma vrestriction_mono:
using assms by auto

lemma vrestriction_vinsert_nin[simp]:
using assms by auto

lemma vrestriction_vinsert_in:
using assms by auto

textβΉConnections.βΊ

lemma vrestriction_vconst_on_ex:
using assms by auto

lemma vrestriction_vconst_on_nex:
shows "(vconst_on A c) βΎβ©β B = 0"
using assms by auto

textβΉPrevious connections.βΊ

textβΉSpecial properties.βΊ

subsectionβΉPropertiesβΊ

subsubsectionβΉDomainβΊ

definition vdomain :: "V β V"

abbreviation app_vdomain :: "V β V" (βΉπβ©ββΊ)
where "πβ©β r β‘ vdomain (set {r}) β¦rβ¦"

unfolding vdomain_def by simp

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!]:
using assms unfolding vdomain_def by auto

lemma vdomainD[dest]:
using assms unfolding vdomain_def by auto

lemma vdomainE[elim]:
using assms unfolding vdomain_def by auto

lemma app_vdomainI[intro]:
using assms unfolding vdomain_def by auto

lemma app_vdomainD[dest]:
using assms unfolding vdomain_def by auto

lemma app_vdomainE[elim]:
using assms unfolding vdomain_def by clarsimp

textβΉSet operations.βΊ

lemma vdomain_vempty[simp]: "πβ©β 0 = 0" by (auto intro!: vsubset_antisym)

by (auto simp: vinsert_set_insert_eq)

lemma vdomain_mono:
using assms by blast

by (auto intro!: vsubset_antisym)

by (auto intro!: vsubset_antisym)

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)

by (auto intro!: vsubset_antisym)

textβΉSpecial properties.βΊ

lemma vdomain_vsubset_vtimes:
using assms by auto

subsubsectionβΉRangeβΊ

definition vrange :: "V β V"

abbreviation app_vrange :: "V β V" (βΉββ©ββΊ)
where "ββ©β r β‘ vrange (set {r}) β¦rβ¦"

unfolding vrange_def by simp

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]:
using assms unfolding vrange_def by auto

lemma vrangeD[dest]:
using assms unfolding vrange_def by auto

lemma vrangeE[elim]:
using assms unfolding vrange_def by auto

lemma app_vrangeI[intro]:
using assms unfolding vrange_def by auto

lemma app_vrangeD[dest]:
using assms unfolding vrange_def by simp

lemma app_vrangeE[elim]:
using assms unfolding vrange_def by clarsimp

textβΉSet operations.βΊ

lemma vrange_vempty[simp]: "ββ©β 0 = 0" by (auto intro!: vsubset_antisym)

by (auto simp: vinsert_set_insert_eq)

lemma vrange_mono:
using assms by force

by (auto intro!: vsubset_antisym)

by (auto intro!: vsubset_antisym)

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

textβΉPrevious connectionsβΊ

by (auto intro!: vsubset_antisym)

by (auto intro!: vsubset_antisym)

textβΉSpecial properties.βΊ

lemma vrange_vsubset_vtimes:
using assms by auto

lemma vrange_VLambda_vsubset:
using assms by auto

by (rule vsubsetI) auto

lemma vrange_vsubset:
using assms by auto

subsubsectionβΉFieldβΊ

definition vfield :: "V β V"

abbreviation app_vfield :: "V β V" (βΉβ±β©ββΊ)
where "β±β©β r β‘ vfield (set {r}) β¦rβ¦"

textβΉRules.βΊ

lemma vfieldI[intro!]:
using assms unfolding vfield_def by auto

lemma vfieldD[dest]:
using assms unfolding vfield_def by auto

lemma vfieldE[elim]:
using assms unfolding vfield_def by auto

lemma app_vfieldI1[intro]:
using assms unfolding vfield_def by simp

lemma app_vfieldI2[intro]:
using assms by auto

lemma app_vfieldI3[intro]:
using assms by auto

lemma app_vfieldD[dest]:
using assms unfolding vfield_def by simp

lemma app_vfieldE[elim]:
shows P
using assms by auto

lemma app_vfield_vpairE[elim]:
using assms unfolding app_vfield_def by blast

textβΉSet operations.βΊ

lemma vfield_vempty[simp]: "β±β©β 0 = 0" by (auto intro!: vsubset_antisym)

by (auto simp: vinsert_set_insert_eq)

lemma vfield_mono:
using assms by fastforce

by (auto intro!: vsubset_antisym)

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

by (auto intro!: vsubset_antisym)

subsubsectionβΉImageβΊ

definition vimage :: "V β V"

abbreviation app_vimage :: "V β V β V" (infixr βΉβ©ββΊ 90)
where "r β©β A β‘ vimage (set {β¨r, Aβ©}) β¦β¨r, Aβ©β¦"

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!]:
using assms unfolding vimage_def by (simp add: VLambda_iff2)

lemma vimageD[dest]:
shows "β¨r, Aβ© ββ©β D" and "s = r β©β A"
using assms unfolding vimage_def by auto

lemma vimageE[elim]:
using assms unfolding vimage_def by auto

lemma app_vimageI1:
shows "x ββ©β r β©β A"
using assms unfolding vimage_def by simp

lemma app_vimageI2[intro]:
using assms app_vimageI1 by auto

lemma app_vimageD[dest]:
assumes "x ββ©β r β©β A"
using assms unfolding vimage_def by simp

lemma app_vimageE[elim]:
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)

proof-
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]:
shows "set {β¨a, bβ©} β©β A = set {b}"
using assms by auto

lemma vimage_vsingleton_nin[intro, simp]:
using assms by auto

lemma vimage_vsingleton_vinsert[simp]: "set {β¨a, bβ©} β©β vinsert a A = set {b}"
by auto

lemma vimage_mono:
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
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"
proof(intro vsubset_antisym vsubsetI)
then show "x ββ©β X Γβ©β Z" unfolding x_def using assms by auto
next
then obtain a c where x_def: "x = β¨a, cβ©" and "a ββ©β X" and "c ββ©β Z" by auto
using assms unfolding x_def by (meson VSigmaI app_vimageE vcompI)
qed

textβΉConnections.βΊ

by (auto intro!: vsubset_antisym)

lemma vimage_vconst_on_ne[simp]:
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

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.βΊ

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:
using assms by auto

lemma vimage_vdomain_vsubset: "r β©β A ββ©β r β©β πβ©β r" by auto

proof(intro vsubsetI)
then have "set {set {x}, set {x, y}} ββ©β r" unfolding vpair_def by auto
unfolding VUnion_iff by auto
define Ur where "Ur = ββ©βr"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

proof(intro vsubsetI)
then have "set {set {x}, set {x, y}} ββ©β r" unfolding vpair_def by auto
unfolding VUnion_iff by auto
define Ur where "Ur = ββ©βr"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

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

proof-
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!]:
using assms unfolding invimage_def by (simp add: VLambda_iff2)

lemma invimageD[dest]:
shows "β¨r, Aβ© ββ©β D" and "s = r -β©β A"
using assms unfolding invimage_def by auto

lemma invimageE[elim]:
using assms unfolding invimage_def by auto

lemma app_invimageI[intro]:
shows "a ββ©β r -β©β A"
using assms invimage_def by auto

lemma app_invimageD[dest]:
using assms using invimage_def by auto

lemma app_invimageE[elim]:
assumes "a ββ©β r -β©β A"
using assms unfolding invimage_def by auto

lemma app_invimageI1:
using assms unfolding vimage_def
by (simp add: invimage_def app_vimageI1 vlrestriction_vconverse)

lemma app_invimageD1:
assumes "a ββ©β r -β©β A"
using assms by fastforce

lemma app_invimageE1:
shows P
using assms unfolding invimage_def by auto

lemma app_invimageI2:
assumes "a ββ©β rΒ―β©β β©β A"
using assms unfolding invimage_def by simp

lemma app_invimageD2:
assumes "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_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]:
shows "set {β¨a, bβ©} -β©β A = set {a}"
using assms by auto

lemma invimage_vsingleton_nin[intro, simp]:
using assms by auto

lemma invimage_vsingleton_vinsert[intro, simp]:
"set {β¨a, bβ©} -β©β vinsert b A = set {a}"
by auto

lemma invimage_mono:
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_vrange[simp]: "r -β©β ββ©β r = πβ©β r"
unfolding invimage_def by (auto intro!: vsubset_antisym)

lemma invimage_vrange_vsubset[simp]:
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)

unfolding invimage_def by auto

lemma invimage_vconst_on_ne[simp]:
shows "vconst_on A c -β©β B = A"
by (simp add: assms invimage_eq_vdomain_vrestriction vrrestriction_vconst_on)

lemma invimage_vconst_on_vempty[simp]:
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.βΊ

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
qed auto

lemma vdomain_vcomp[simp]: "πβ©β (r ββ©β s) = s -β©β πβ©β r" by blast

lemma vdomain_vcomp_vsubset:
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:
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]:
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"
using assms by auto

lemma vbrelation_vunionD[dest]:
shows "vbrelation r" and "vbrelation s"
using assms by auto

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_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"
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.βΊ

using vbrelation_axioms by auto

lemma vconverse_mono[simp]:
assumes "vbrelation r" and "vbrelation s"
using assms by (force intro: vconverse_vunion)+

lemma vconverse_inject[simp]:
assumes "vbrelation r" and "vbrelation s"
using assms by fast

lemma (in vbrelation) vconverse_vsubset_swap_2:
using assms vbrelation_axioms by auto

using vbrelation_axioms by (elim vbrelationE) auto

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:
shows "vbrelation r"
using assms by auto

lemma (in vbrelation) vbrelation_vintersection_vdomain:
shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
by (metis vbrelationE1 vbrelation_vintersectionI)
with assms show "x ββ©β 0" by auto
qed simp

lemma (in vbrelation) vbrelation_vintersection_vrange:
shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
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)
by (metis vbrelationE1 vbrelation_vintersectionI)
with assms show "x ββ©β 0" by auto
qed auto

using vbrelation by auto

lemma (in vbrelation) vbrelation_vsubset_vtimes:
proof(intro vsubsetI)
fix x assume prems: "x ββ©β r"
with vbrelation obtain a b where x_def: "x = β¨a, bβ©" by auto
with assms have "a ββ©β A" and "b ββ©β B" by auto
qed

lemma (in vbrelation) vlrestriction_vsubset_vrange[intro, simp]:
shows "r βΎβ§lβ©β A = r"
proof(intro vsubset_antisym)
by (rule vlrestriction_mono[OF assms, of r, unfolded vlrestriction_vdomain])
qed auto

lemma (in vbrelation) vrrestriction_vsubset_vrange[intro, simp]:
shows "r βΎβ§rβ©β B = r"
proof(intro vsubset_antisym)
by (rule vrrestriction_mono[OF assms, of r, unfolded vrrestriction_vrange])
qed auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_left[simp]:
shows "vid_on A ββ©β r = r"
using assms by auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_right[simp]:
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 +

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]:
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)"
proof
using elts_0 by blast
then consider
by blast
then show "b = c" using assms by cases auto
qed (use assms in auto)

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"
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"
lemma (in vsv) vsv_vrestriction[intro, simp]: `