# Re: [isabelle] Finite set datatype?

```On 10/08/2010 04:36 AM, Brian Huffman wrote:
```
```On Wed, Oct 6, 2010 at 5:10 PM, Jeremy Dawson<jeremy at rsise.anu.edu.au>  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}"
begin
...

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
begin

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

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

- Brian
```
```
Brian,

Thanks for this - I'll have to look at it when I've got more time.

```
This "instantiation" command looks rather like the "instance" command - is that right?
```but it seems to have definitions following it rather than before it.

```
Do you know whether its use is documented anywhere (and if so where) (I can't find it now, probably because I only have Isabelle2005 installed here now).
```
```
So I can't really see how it would work - would you be able to define a type class that encompasses sets and finite sets, and enables you to define the power set function Pow, and get all the relevant theorems about it ?
```
Regards,

Jeremy

```

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