[isabelle-dev] [isabelle] Countable instantiation addition

Peter Lammich peter.lammich at uni-muenster.de
Thu Jul 21 19:02:41 CEST 2011

This is definitely a useful tool for ImperativeHOL ... One could 
probably integrate
it into the datatype package, such that datatypes automatically become 
countable (like Haskell infers some typeclasses automatically (on demand))


Mathieu Giorgino schrieb:
> Hi all,
> I have written a little ML library allowing to automatically prove, in most 
> cases, instantiations of types (typedefs, records and datatypes) as countable 
> (see ~~/src/HOL/Library/Countable). The style of the library is still a little 
> rough but I think it could be a nice addition to the Isabelle Library with 
> some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which 
> can only store values of countable types in its heap.
> However, as Lukas Bulwhan said to me, improving it and integrating it in 
> Isabelle while nobody use it would certainly be a lost of time.
> So here is my question: would anybody be interested in this addition ?
> I attach this library with a theory containing tests/examples.
> Anyway, if you have some advices for improving it, they would be welcome.
> Regards,
> Mathieu Giorgino

More information about the isabelle-dev mailing list