[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