*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Finite set datatype?*From*: Jeremy Dawson <jlcaadawson at netspeed.com.au>*Date*: Fri, 08 Oct 2010 10:55:38 +1100*Cc*: Jeremy Dawson <jeremy at rsise.anu.edu.au>, USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTikuQjAJsHmfHJSbcJ9QKyODEcqpntTGPMkBcu+Q@mail.gmail.com>*Organization*: ANU*References*: <4CAC4CC3.3020506@it.uu.se> <20101006103854.8EC41492313@talisker.in.tum.de> <4CAD0FDD.5000001@rsise.anu.edu.au> <AANLkTikuQjAJsHmfHJSbcJ9QKyODEcqpntTGPMkBcu+Q@mail.gmail.com>*Reply-to*: jeremy at rsise.anu.edu.au*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

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.

but it seems to have definitions following it rather than before it.

Regards, Jeremy

**Follow-Ups**:**Re: [isabelle] Finite set datatype?***From:*Alexander Krauss

**References**:**[isabelle] Finite set datatype?***From:*Palle Raabjerg

**[isabelle] Finite set datatype?***From:*Christian Urban

**Re: [isabelle] Finite set datatype?***From:*Jeremy Dawson

**Re: [isabelle] Finite set datatype?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Finite set datatype?
- Next by Date: Re: [isabelle] Finite set datatype?
- Previous by Thread: Re: [isabelle] Finite set datatype?
- Next by Thread: Re: [isabelle] Finite set datatype?
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list