[isabelle-dev] [isabelle] Countable instantiation addition
peter.lammich at uni-muenster.de
Thu Jul 21 19:02:41 CEST 2011
This is definitely a useful tool for ImperativeHOL ... One could
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.
> Mathieu Giorgino
More information about the isabelle-dev