*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Finite set datatype?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 7 Oct 2010 10:36:27 -0700*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4CAD0FDD.5000001@rsise.anu.edu.au>*References*: <4CAC4CC3.3020506@it.uu.se> <20101006103854.8EC41492313@talisker.in.tum.de> <4CAD0FDD.5000001@rsise.anu.edu.au>*Sender*: huffman.brian.c at gmail.com

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

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

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

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

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

- Previous by Date: [isabelle] Proving finiteness for inductive sets
- 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