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
  ~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

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.

Jeremy







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