Experiments with ZF Set Theory in HOL and Isabelle
Most general purpose proof assistants support versions of<br />typed higher order logic. Experience has shown that these logics are capable<br />of representing most of the mathematical models needed in Computer<br />Science. However, perhaps there exist applications where ZF-style<br />set theory is more natural, or even necessary. Examples may include<br />Scott's classical inverse-limit construction of a model of the untyped lambda-calculus<br /> (D_inf) and the semantics of parts of the Z specification notation.<br /><br />This paper compares the representation and use of ZF set theory within<br />both HOL and Isabelle. The main case study is the construction of D_inf.<br />The advantages and disadvantages of higher-order set theory versus first-order<br />set theory are explored experimentally. This study also provides a<br />comparison of the proof infrastructure of HOL and Isabelle.