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_1970"› 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" and "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

lemma ex1D: "∃!x. P x ⟹ P x ⟹ P y ⟹ x = y" by clarsimp

text‹\newpage›

end