[opentheory-users] new_specification

[Ramana Kumar]

Hello OpenTheory!

There has been some activity recently considering Rob Arthan's
proposal for HOL Constant Definition Done Right [1]. For those
unfamiliar, that proposal includes a rule for introducing new
constants by conservative extension with a (potentially loose)
specification, and it subsumes the functionality of the new_definition
and new_specification rules currently implemented in the various HOL
provers.

The rule has a host of benefits detailed in the paper. My aim here is
to encourage OpenTheory and HOL Light to adopt it as well - or at
least to invite discussion on that possibility.

As I understand it, work is being done to implement this new rule in
HOL4 and ProofPower, as a replacement for the primitive rule for
defining a new constant by an equation. Of course, as it stands, this
breaks compatibility with OpenTheory, since the new rule cannot be
reduced to the definitional mechanisms provided in OpenTheory.

It would be wonderful to maintain the possibility of proof export,
hence my invitation to consider the new rule for OpenTheory.

Cheers,
Ramana

[1] http://www.lemma-one.com/papers/hcddr.pdf