[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 

  ~HOL/Quotient_Examples/FSet.thy

(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,
Christian

Attachment: Nominal2_FSet.thy
Description: Binary data



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