Email Gateway (Aug 22 2022 at 18:57): Email Gateway (Aug 22 2022 at 18:57):From: Ken Kubota <mail@kenkubota.de>
The following two papers might be useful:
From Types to Sets in Isabelle/HOL
https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2014.pdf
From Types to Sets by Local Type Definitions in Higher-Order Logic
http://andreipopescu.uk/pdf/fromTypesToSetsITP2016.pdf
In particular, page 2 of the second paper is of interest:
"On the downside, type-based theorems are less flexible, and therefore unsuitable for some developments. Indeed, when working with mathematical structures, it is often the case that they have the desired property only on a proper subset of the whole type."
"An additional nuance to this situation is specific to Isabelle/HOL, which allows users to annotate types with Haskell-like type-class constraints. This provides a further level of implicit reasoning."
Independently I had developed a similar mechanism in R0 in order to overcome the inflexibility mentioned above:
"Whenever a theorem of the form p_(oα)e_α is inferred, meaning that a mathematical entity (or object, element) e of any type α has property p (which in set theory is expressed by e ∈ p) [...] the new type p is attached to the entity (e_p) [...]".
http://www.owlofminerva.net/files/formulae.pdf (p. 11)
This provides a mechanism to introduce types from (sub)sets (of other types), and also provides the level of implicit reasoning mentioned above by coding the constraints directly within the new type (as part of the type definition).
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100
Last updated: Apr 26 2024 at 12:28 UTC