  We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of
Separation in generic extensions of models of set theory by using the
fundamental theorems of forcing. We also formalize the satisfaction of the
axioms of Extensionality, Foundation, Union, and Powerset. The axiom of
Infinity is likewise treated, under additional assumptions on the ground model.
In order to achieve these goals, we extended Paulson's library on
constructibility with renaming of variables for internalized formulas, improved
results on definitions by recursion on well-founded relations, and sharpened
hypotheses in his development of relativization and absoluteness.
