[isabelle-dev] Countable instantiation addition

[Mathieu Giorgino]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Countable.ML
Type: text/x-ocaml
Size: 12063 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110721/3b539b22/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Countable_Examples.thy
Type: application/isabelle-theory
Size: 4634 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110721/3b539b22/attachment-0003.bin>