From types to sets by local type definitions in higher-order logic

Types in Higher-Order Logic (HOL) are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its soundness. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.

The final publication is available at Springer
via http://dx.doi.org/10.1007/978-3-319-43144-4_13

Published as: Kunčar O., Popescu A. (2016) From Types to Sets by Local Type Definitions in Higher-Order Logic. In: Blanchette J., Merz S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science, vol 9807. Springer, Cham