[isabelle] Finite set datatype?

Hi Palle,

There is even another one.

Palle Raabjerg writes:
 > 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.

For this very reason Cezary Kaliszyk and I introduced 
the finite set type using the quotient package. The theory 
is problably not yet extremely polished, but it is already
useful for us. The theory is in 


(I am using the latest snapshot, but it also should be
part of the latest stable release).

Below is a short theory which supplies all facts that are 
needed to make this type work with nominal. It might need
a few adjustments if you work with "old" nominal.

Hope this helps,

Attachment: Nominal2_FSet.thy
Description: Binary data

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