[isabelle-dev] Countable instantiation addition
krauss at in.tum.de
Thu Jul 21 22:54:28 CEST 2011
On 07/21/2011 09:47 PM, Gerwin Klein wrote:
> The idea has potential for generalisation. Could we turn this into
> something similar to Haskell's "deriving"?
> The command would take a datatype and a list of instantiation methods
> that each know how to instantiate a datatype for a specific type
> class, e.g. enum, countable, order, etc. An instantiation method
> would be basically a usual proof method plus some small part that
> knows how to set up the specific instantiation goal (probably the
> same code for pretty much all applications of this) plus some
> background theory that provides the basic setup.
I like this approach. You ask for something explicitly and then you get
it, but you don't have to remember a new obscure syntax for every bit of
it. You would just write
datatype foo = ....
deriving countable, finite,
Several existing things fit into this scheme: When I define a fresh
"datatype foo = Bar" in Main, it automatically becomes an instance of
the following type classes:
- equal (executable equality, for code generation)
- term_of (reifiable term structure, for code generation)
- size (size function, for termination proofs)
- full_exhaustive (for exhaustive quickcheck)
(there is actually a large zoo of type classes for quickcheck...)
This doesn't mean that we have to make every last thing explicit, but a
mechanism would make sense.
Note that in general, a proof method is not enough, since we have to
define overloaded constants. Here, countable is an exception since the
class has no parameters.
More information about the isabelle-dev