Email Gateway (Aug 18 2022 at 18:42): Email Gateway (Aug 18 2022 at 18:42):From: Ashley Yakeley <ashleyy@microsoft.com>
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
Email Gateway (Aug 18 2022 at 18:43):From: Peter Gammie <peteg42@gmail.com>
Ashley,
This is precisely what typedef does.
See Section 8.5 in the Isabelle tutorial (accompanying the distribution).
There are also lots of examples in the HOL source itself.
cheers
peter
Email Gateway (Aug 18 2022 at 18:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Ashley,
There are also lots of examples in the HOL source itself.
a nice recent is src/HOL/Library/Saturated.thy which demonstrates a
bunch of good default practice.
Hope this helps,
Florian
signature.asc
Last updated: May 06 2024 at 12:29 UTC