Re: [isabelle] Finite set datatype?

Christian Urban wrote:
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,

Recently I contemplated defining a finite set type and also a type class which would have included finite sets and (unrestricted) sets, thus not having to repeat lots of definitions and theorems which already exist for sets.

But as I understood it (tell me if this is not so) the set type was removed from Isabelle a couple of years ago, so this would no longer be possible.


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