[isabelle] Finite set datatype?



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.