[isabelle-dev] [isabelle] Countable instantiation addition

[Gerwin Klein]

On 21/07/2011, at 8:15 PM, Alexander Krauss wrote:
> It comes in the form of a method, so it has to be invoked explicitly, but like this it doesn't produce any penalty when it is not used.

A separate command like this method looks like the right way to do such things. 

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. 

The methods would not have to work on every kind of data type (just failing if they can't prove their goal), and the list of available ones could be easily extended using the same Isar setup mechanisms that we use for proof methods, attributes, and other things. 

The command would not pollute normal datatype usage and would not need to be integrated with the datatype package, keeping the code separate. The interface would just be the user-visible final definition of the datatype as in Brian's case.

Cheers,
Gerwin