That is such a bad luck for me... It seems I had verified it wasn't in the repository a little too soon (like for Imperative_HOL...). But at least I have learned Isabelle/ML. I don't think there is any additional feature in my version. It defines mutual recursive functions from the mutual types to natural numbers and proves their injectivity in a separate lemma that is used in the instantiation.
So as I understand your method, the only addition would be the definition of these executable functions, which does not seem so useful. It also proves countability only from the type names and without "instance ..." but then what it does is less clear (less integrated into existing features). In the case of typedef and records, countability can easily be proven by using: countable_classI[of "to_nat o Rep_<type>"] and Rep_<type>_inject It can perhaps allow to write a simpler method. My version also does not need "instance ..." and can infer the needed constrains (sorts) thanks to the Isabelle type inference but then what we obtain is not so explicit. Regards, Mathieu Le jeudi 21 juillet 2011 13:51:17 Brian Huffman a écrit : > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev