[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:220.127.116.11) Gecko/20100917 Icedove/3.0.8
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and