Re: [isabelle] Finite set datatype?
Christian Urban wrote:
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
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,
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and