# [isabelle] Subset Types

Is it possible to create types that are subsets of an existing type?

`For example, given a type T and a predicate "p :: T => bool", construct a
``type S consisting of those values of T that satisfy p. To create a value of
``type S, one must provide a value t :: T and a proof of "p t". To create a
``value of type "S1 => S2", one must provide a value of type "f :: T1 => T2"
``and a proof of "p1 t1 ==> p2 (f t1)", etc.
`

`Thus a value "t :: S" (or "s(t) :: S") would be a witness of "p t".
``Furthermore, there may exist classes C such that "S :: C" but not "T :: C"
``due to the assumptions in C.
`

`Locales behave a bit like this, inasmuch as one must provide values and
``prove predicates on them, but locales are not types.
`

`Examples: a type of prime "nat"s. A type that's a pair of rationals, with
``the first >= the second. A type of orthonormal pairs of vectors.
`

`-- Ashley Yakeley
``
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*