Re: [isabelle] Finite set datatype?

On Wed, Oct 6, 2010 at 5:10 PM, Jeremy Dawson <jeremy at> 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 for
> sets.

Type classes generalizing the standard set operations already exist;
they are defined in Lattices.thy. The notations for union,
intersection, {} and UNIV are now just type-specific abbreviations for
the general lattice operations sup, inf, bot, and top, respectively.

The Quotient_Examples/FSet.thy library that Christian referred to
already includes instances of the appropriate lattice classes, which
lets you avoid repeating the existing generic theorems.

instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"

Of course, the Set.thy library also contains a lot of set-specific
theorems that have no general counterpart. By generalizing more
theorems from Set.thy to the appropriate lattice classes, we could
make FSet.thy more useful.

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

Indeed, the set type no longer exists; "'a set" is just an
abbreviation for "'a => bool". But this doesn't mean that "'a set"
can't be made an instance of a type class -- you just need to provide
a generic instance for the function type. For example, the following
declaration from Lattices.thy makes type "'a set" into a lattice,
since type bool is already a lattice:

instantiation "fun" :: (type, lattice) lattice

  inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"

  sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"

- Brian

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