[isabelle-dev] [isabelle] Countable instantiation addition
giorgino at irit.fr
Fri Jul 22 14:26:28 CEST 2011
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
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
countable_classI[of "to_nat o Rep_<type>"]
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.
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 <krauss at 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-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-
> > dev
More information about the isabelle-dev