Email Gateway (Aug 22 2022 at 13:54): Email Gateway (Aug 22 2022 at 13:54):From: Daniel Horne <d.horne@danielhorne.co.uk>
Hi.
I've found myself running into a few situations where I want to define a
type as "an object of (existing type a) for which (boolean expression is
true)".
Suppose, for example, that I want to represent identifiers in a language
I'm trying to model. Naturally, I'd think of using the primitives
defined in string.thy, but as not all strings are valid identifiers, I'd
define a function such as
fun is_identifier :: "string => bool"
But thereafter I'd need to code it in lemmas as taking is_identifier as
an assumption. I'd tend to think it'd be neater to have identifier being
a type defined as "string which satisfies is_identifier", and was
wondering if there was a way to do this?
Thanks,
Daniel Horne
Email Gateway (Aug 22 2022 at 13:54):From: Peter Lammich <lammich@in.tum.de>
typedef id = "Collect is_identifier"
<proof that there is at least one identifier>
does what you want. However, there is no true subtyping, so using
the new type as string requires some manual work, which may be slightly
simplified by the lifting/transfer package.
Email Gateway (Aug 22 2022 at 13:55):From: Lars Hupel <hupel@in.tum.de>
Hi Daniel,
other people have suggested using "typedef" to introduce a new type.
There is even a way to have the system automatically coerce an
"identifier" to a "string" where one is expected by virtue of coercions.
(The other way would technically be possible but virtually useless.)
However, keep in mind that introducing a new type also requires logical
effort. For example, existing constants on strings need to be lifted to
the new type (concatenation comes to mind). Also, you need to transfer
lemmas from the base type to the subtype using the "transfer" method.
Another possibility would be to use an anonymous context:
context
fixes a b c :: string
assumes a: "is_identifier a"
assumes b: "is_identifier b"
assumes c: "is_identifier c"
begin
...
end
This gives you a block in your theory where you can use these "regular"
values as identifiers. Of course this only works when you need a fixed
number of them. If that's the case, it's the solution which is much
easier to work with. (You might also want to look into the concept of
"locales" in Isabelle if you're deciding to go down that route.)
Cheers
Lars
Last updated: Apr 16 2024 at 20:15 UTC