Re: [isabelle] Finite set datatype?
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
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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and