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.