[isabelle-dev] Countable instantiation addition

[Alexander Krauss]

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.

Alex