A mechanized translation from higher-order logic to set theory


In order to make existing formalizations available for set-theoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This covers all fundamental primitives, particularly type classes. The translation produces LCF-style theorems that are checked by Isabelle’s inference kernel. Type checking is replaced by explicit reasoning about set membership.

In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP 2010), volume 6172 of Lecture Notes in Computer Science, pages 323–338. Springer Verlag, 2010.