[isabelle-dev] [isabelle] Countable instantiation addition

[Brian Huffman]

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
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Countable_Typedef.thy
Type: application/isabelle-theory
Size: 1515 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110721/818df159/attachment-0002.bin>