Auxiliary constants from datatype package

[tanyongkiam]

Isabelle's datatype package introduces a bunch of helpful constants on datatype definitions, see 2.1.5 Auxiliary Constants http://isabelle.in.tum.de/dist/Isabelle2020/doc/datatypes.pdf (thanks to @IlmariReissumies for the link)

These seem like they could be nice additions in an upgraded datatype package too.

[mn200]

The link above has bit-rotted. The relevant language from the 2022 Isabelle release says:

The datatype command introduces various constants in addition to the constructors. With each datatype are associated set functions, a map function, a predicator, a relator, discriminators, and selectors, all of which can be given custom names.

For HOL's list type, these constants would be (in the order above): LIST_TO_SET, MAP, EVERY, LIST_REL, NULL, HD and TL. HOL doesn't provide a discriminator for the CONS case; the Isabelle manual suggests its automation won’t either, because one discriminator is enough for a two-constructor type. Isabelle provides nice-syntax to allow users to pick their custom names for these constants; defaults are invented otherwise. Isabelle also allows the addition of a clause ensuring TL [] = [] (one could similarly imagine setting up HD [] = ARB, though this is clearly far less useful).

[talsewell]

Some of these were added to Isabelle as part of the BNF change. The aux constants are added to a BNF database and used by other tools in the system.

Anyway, at least the set, map and relator are pretty useful. It wouldn't be hard to add code to generate them by default.

[ordinarymath]

I think that getting MAP and REL generated automatically would be a priority. Have no idea how to do it thou. Should I be trying to get it done in PrimRec or with the datatypes.

[talsewell]

I would guess that you'd follow roughly the same approach as DataSize, that is, let the underlying datatype definition complete, and then generate an additional "map" function programmatically.

I started fiddling with an implementation already. The thing blocking me is, for this to do "the right thing" for datatypes defined using other datatypes, there ought to be a way to look up the constants for existing types. This probably belongs with the TypeBase. Maybe it's no big deal to add more optional stuff into the TypeBase, but it feels like more work than just writing a definition-generating gadget.

[ordinarymath]

I would think the fields should be added to TypeBase

[talsewell]

Oh, there's already an "extra" field in there, maybe it just needs a sensible scheme.

[talsewell]

Some progress on this, I've written some code that generates some _set constants.

I have no idea why I started with _set considering _rel and _map are more obviously useful.

I've parked this code here, with a bunch of work to be done to integrate and test it:
https://github.com/talsewell/HOL/tree/add-data-set

Does anyone want to pick that up? If we can get something like this plugged in and tested for one kind of automatically derived constant, we could generalise that to more of them.

There's probably a bit of work to be done to call it automatically, handle the initial special datatypes, and maybe to allow the user to turn things off if they might fail.

[mn200]

The interesting constants in this world more or less automatically fall out of the BNF construction so I’d be hesitant about putting too much time into this given that I want to switch our package to also do things BNFishly.