Disjoint sums over type classes in hol

Abstract

The standard versions of HOL only support disjoint sums over finite families of types. This paper introduces disjoint sums over type classes containing possibly a countably infinite number of monomorphic types. The result is a monomorphic sum type together with an overloaded function which represents the family of injections. Model-theoretic reasoning shows the soundness of the construction. In order to axiomatize the disjoint sums in HOL, datatypes are introduced which mirror the syntactic structure of type classes. The association of a type with its image in the sum type is represented by a HOL function carrier. This allows a translation of the set-theoretic axiomatization of disjoint sums to HOL. As an application, a sum type U is presented which contains isomorphic copies of many familiar HOL types. Finally, a Z universe is constructed which can server as the basis of a HOL model of the Z schema calculus.