[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.