Isabelle/HOL does not have subtypes in the sense of substitutability. This means that if you need a value of type a
, then you have to provide a value of type a
- you cannot get along with a different type b
. In particular, Isabelle does not have the notion of subtype where the values of the subtype satisfy some additional property.
There are some ways to emulate certain aspects of subtypes, and this is where the notion subtype is used:
Substitution of type parameters allows you to sometimes create the illusion of subtyping. The
record
package uses this to extend records such that one can use an extended recordq
in place of the non-extended recordr
. Internally, the additional fields ofq
are stuffed into an additional type parameter of a generalisation ofr
's record type. Technically, there's no subtype polymorphism going on; consequently, the order of extending records matters.typedef
introduces a new typet
whose type universe is a non-empty subset of the values of some existing HOL typea
. Sometimes, this is referred to ast
being a subtype ofa
, but you do not get substitutability. You always have to explicitly mention the embedding morphismRep_t
when you want to use a value oft
as one ofa
. It does not matter whether you define your type withtypedef
or by some other means, any injective function can serve as such a coercion.Coercive subtyping as described in the Isabelle Reference Manual (section 12.4) makes Isabelle infer and insert such coercions automatically. This only works both the type and the subtype are type constructors without arguments. Use
declare [[coercion_enabled]]
to enable coercive subtyping and register your coercion function withdeclare [[coercion Rep_t]]
. Thus, you do not have to insert the embedding functions yourself.