Email Gateway (Aug 18 2022 at 16:10): Email Gateway (Aug 18 2022 at 16:10):From: Christian Urban <urbanc@in.tum.de>
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
Nominal2_FSet.thy
Last updated: Apr 26 2024 at 08:19 UTC