It does not work for any datatype (for example as soon as a non-countable type is used in the datatype) but it could be integrated in the datatype package with some checks.
However, I don't know if the time penalty (which isn't so big but there anyway) on a so much used feature worth the benefit... unless it would be present as an option (perhaps even with a recursive call on included non- instantiated types). And an option would be mostly equivalent to (in fact even less flexible than) a new command or an ML call subsequent to the datatype definition. Mathieu Le jeudi 21 juillet 2011 19:02:41 Peter Lammich a écrit : > 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)) > > Peter > > 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 > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev