Email Gateway (Aug 18 2022 at 16:10): Email Gateway (Aug 18 2022 at 16:10):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
Hi all,
I have a very short, possibly stupid question:
Is there a finite set datatype in Isabelle?
I want to include a set type in the definition of a nominal datatype.
But Isabelle's standard set datatype can express infinite sets, and
since a requirement for a nominal datatype is a proof of finite support,
they don't seem to work here.
I figure there should at least be a theory, or notion of 'finite set'
somewhere, as the 'set' function effectively guarantees the finiteness
of the sets it converts from lists.
So yes, is there an actual finite set datatype, or would it be possible
to define one?
Or must I use lists in the nominal datatype to somehow emulate finite sets?
Regards,
Palle Raabjerg
Email Gateway (Aug 18 2022 at 16:10):From: Lars Noschinski <noschinl@in.tum.de>
There is the theory Fset in library which defines a finite set type.
-- Lars
Email Gateway (Aug 18 2022 at 16:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Palle,
I actually must correct my quite misleading heading of this file: the
type fset itself is indeed infinite.
Christian hints should indeed suffice.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 16:11):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Christian Urban wrote:
Recently I contemplated defining a finite set type and also a type class
which would have included finite sets and (unrestricted) sets, thus not
having to repeat lots of definitions and theorems which already exist
for sets.
But as I understood it (tell me if this is not so) the set type was
removed from Isabelle a couple of years ago, so this would no longer be
possible.
Jeremy
Email Gateway (Aug 18 2022 at 16:12):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Oct 6, 2010 at 5:10 PM, Jeremy Dawson <jeremy@rsise.anu.edu.au> wrote:
Recently I contemplated defining a finite set type and also a type class
which would have included finite sets and (unrestricted) sets, thus not
having to repeat lots of definitions and theorems which already exist for
sets.
Type classes generalizing the standard set operations already exist;
they are defined in Lattices.thy. The notations for union,
intersection, {} and UNIV are now just type-specific abbreviations for
the general lattice operations sup, inf, bot, and top, respectively.
The Quotient_Examples/FSet.thy library that Christian referred to
already includes instances of the appropriate lattice classes, which
lets you avoid repeating the existing generic theorems.
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
begin
...
Of course, the Set.thy library also contains a lot of set-specific
theorems that have no general counterpart. By generalizing more
theorems from Set.thy to the appropriate lattice classes, we could
make FSet.thy more useful.
But as I understood it (tell me if this is not so) the set type was removed
from Isabelle a couple of years ago, so this would no longer be possible.
Indeed, the set type no longer exists; "'a set" is just an
abbreviation for "'a => bool". But this doesn't mean that "'a set"
can't be made an instance of a type class -- you just need to provide
a generic instance for the function type. For example, the following
declaration from Lattices.thy makes type "'a set" into a lattice,
since type bool is already a lattice:
instantiation "fun" :: (type, lattice) lattice
begin
definition
inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
...
Email Gateway (Aug 18 2022 at 16:12):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Brian,
Thanks for this - I'll have to look at it when I've got more time.
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).
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 ?
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 16:12):From: Alexander Krauss <krauss@in.tum.de>
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
Last updated: Apr 23 2024 at 04:18 UTC