# [isabelle] Finite set datatype?

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Finite set datatype?
*From*: Palle Raabjerg <palle.raabjerg at it.uu.se>
*Date*: Wed, 06 Oct 2010 12:17:39 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.12) Gecko/20100917 Icedove/3.0.8

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

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