[isabelle-dev] [isabelle] Countable instantiation addition

[Mathieu Giorgino]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev