From Types to Sets in Isabelle/HOL Extented Abstract

Abstract. HOL types are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Is-abelle/HOL), where a new type can be defined whenever a nonempty set is ex-hibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We analyze some undesired consequences of this limitation and propose a more expressive type-definition rule that addresses it. The new expres-sive power opens the opportunity for a package that relativizes type-based state-ments to more flexible set-based variants—to streamline this process, we further implement a rule that transforms the implicit type-class constraints into explicit assumptions. Moreover, our tool is an interesting use case of Lifting and Transfer.