[isabelle-dev] [isabelle] Countable instantiation addition
mathieu.giorgino at irit.fr
Thu Jul 21 19:51:45 CEST 2011
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
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))
> 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-dev at in.tum.de
More information about the isabelle-dev