Email Gateway (Aug 18 2022 at 19:32): Email Gateway (Aug 18 2022 at 19:32):From: Alexander Krauss <krauss@in.tum.de>
Hi all,
I wonder if it is possible (possibly via some tricks) to make datatype
constructors coincide with overloaded constants.
The only datatype in Isabelle/HOL with overloaded constructors is the
type "nat", where 0 is overloaded. That type is defined via an explicit
construction followed by rep_datatype, for bootstrapping reasons.
But there are situations where it is natural to use overloading in a
datatype, even for only syntactic reasons. For example, in a type of
regular expressions it would be natural to use +,*,0,1.
The only way to achieve this that I can think of is the following, but
it is rather tricky:
1) Define an auxiliary datatype with non-overloaded constructors
2) Define an isomorphic copy of that datatype. Define the overloaded
constants as the lifted constructors, possibly using lifting machinery.
3) Use rep_datatype on the isomorphic copy.
Has anybody got a better idea? I feel that the above is too technical to
be worth the effort.
Is it conceivable that a fully localized datatype package could do this
directly, when used in an instantiation target???
Alex
Email Gateway (Aug 18 2022 at 19:33):From: Makarius <makarius@sketis.net>
Yes, a properly datatype package would be able to do this. Constructor
definitions are just definitions.
It should now also work with sophisticated syntax translations attached to
them, because I've recently changed the "locale_const" scheme to use plain
name space aliases for the special case where a locally defined term does
not depend on context parameters. This means the syntax layer would see
the global foundation constant in any case, not a funny abbreviation.
So it is now merely a matter to go through all the primitive and derived
ML proofs of the package, and do the right thing wrt. "Free" variables.
Makarius
Email Gateway (Aug 18 2022 at 19:34):From: Alexander Krauss <krauss@in.tum.de>
Now that I've thought about this, I no longer see how this could work:
Suppose I want to define the type "'a re" of regular expressions, and
overload just 0: I cannot write
instantiation re :: (type) zero
begin
before the type re is defined. So defining re inside this instantiation
target won't work, unfortunately. To make this work, the package and the
target would need to interact in a non-standard way, which seems far
beyond the current architecture. Bad luck.
Anyway, for this application the advantage would just be syntactic, so
it is no big deal.
Alex
Last updated: Apr 26 2024 at 04:17 UTC