Hello everyone, Attached is an implementation of a "countable_typedef" method that I just wrote. (It works in a very similar manner to the "countable_datatype" method.) Since records are implemented as typedefs of product types, the same method works for record types as well. I'd be happy to add this to Library/Countable.thy if anyone wants me to.
I haven't had time to study Mathieu's ML library yet, but if it has any features or capabilities that my system lacks, we should definitely try to incorporate those into whatever ends up in the next Isabelle release. I also need to remember to add an item to the NEWS file letting people know that these new proof methods exist. - Brian On Thu, Jul 21, 2011 at 11:15 AM, Alexander Krauss <kra...@in.tum.de> wrote: > Hi Matthieu, > >> 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). > > It seems that for datatypes we now have such functionality, implemented four > weeks ago by Brian Huffman: > > http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f > > It comes in the form of a method, so it has to be invoked explicitly, but > like this it doesn't produce any penalty when it is not used. If you want to > contribute an extension to records/typedefs, you are welcome, but you > probably want to study Brian's implementation first. I assume that he is > also the most appropriate person to review patches for this functionality. > > Alex > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >
Countable_Typedef.thy
Description: application/isabelle-theory
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
