search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
616 stars 138 forks source link

Auxiliary constants from datatype package #875

Open tanyongkiam opened 3 years ago

tanyongkiam commented 3 years ago

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 commented 1 year ago

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).