[isabelle-dev] [isabelle] Countable instantiation addition

[Mathieu Giorgino]

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 <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