Abstract: 
This entry is a new formalisation of ZFC set theory in Isabelle/HOL. It is
logically equivalent to Obua's HOLZF; the point is to have the closest
possible integration with the rest of Isabelle/HOL, minimising the amount of
new notations and exploiting type classes.
There is a type V of sets and a function elts :: V => V
set mapping a set to its elements. Classes simply have type V
set, and a predicate identifies the small classes: those that correspond
to actual sets. Type classes connected with orders and lattices are used to
minimise the amount of new notation for concepts such as the subset relation,
union and intersection. Basic concepts — Cartesian products, disjoint sums,
natural numbers, functions, etc. — are formalised.
More advanced settheoretic concepts, such as transfinite induction,
ordinals, cardinals and the transitive closure of a set, are also provided.
The definition of addition and multiplication for general sets (not just
ordinals) follows Kirby.
The theory provides two type classes with the aim of facilitating
developments that combine V with other Isabelle/HOL types:
embeddable, the class of types that can be injected into V
(including V itself as well as V*V, etc.), and
small, the class of types that correspond to some ZF set.
extrahistory =
Change history:
[20200128]: Generalisation of the "small" predicate and order types to arbitrary sets;
ordinal exponentiation;
introduction of the coercion ord_of_nat :: "nat => V";
numerous new lemmas. (revision 6081d5be8d08) 
BibTeX: 
@article{ZFC_in_HOLAFP,
author = {Lawrence C. Paulson},
title = {Zermelo Fraenkel Set Theory in HigherOrder Logic},
journal = {Archive of Formal Proofs},
month = oct,
year = 2019,
note = {\url{http://isaafp.org/entries/ZFC_in_HOL.html},
Formal proof development},
ISSN = {2150914x},
}
