Re: [isabelle] Finite set datatype?



Hi Jeremy,

This "instantiation" command looks rather like the "instance" command - is that right?
but it seems to have definitions following it rather than before it.

Do you know whether its use is documented anywhere (and if so where) (I can't find it now, probably because I only have Isabelle2005 installed here now).

You can always find documentation on the latest release at
http://isabelle.in.tum.de/documentation.html . The document "Tutorial on Type Classes" documents the new (from 2006) class infrastructure from a user's point of view. Moreover, Section 5.6 of the Isar Reference Manual contains syntax diagrams etc. Technical details and background can be found in a paper by Haftmann and Wenzel: http://www4.informatik.tu-muenchen.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf

So I can't really see how it would work - would you be able to define a type class that encompasses sets and finite sets, and enables you to define the power set function Pow, and get all the relevant theorems about it ?

I think power sets cannot be defined, since there is no corresponding notion on functions... (I am not even completely sure how it would work if sets had their own type constructor...). But most other constructs and notation it works fine.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.