*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Finite set datatype?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Thu, 07 Oct 2010 11:10:05 +1100*In-reply-to*: <20101006103854.8EC41492313@talisker.in.tum.de>*References*: <4CAC4CC3.3020506@it.uu.se> <20101006103854.8EC41492313@talisker.in.tum.de>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

Christian Urban wrote:

Hi Palle, There is even another one. Palle Raabjerg writes: > Hi all,>> I have a very short, possibly stupid question:> Is there a finite set datatype in Isabelle?>> I want to include a set type in the definition of a nominal datatype.> But Isabelle's standard set datatype can express infinite sets, and> since a requirement for a nominal datatype is a proof of finite support,> they don't seem to work here.For this very reason Cezary Kaliszyk and I introducedthe finite set type using the quotient package. The theoryis problably not yet extremely polished, but it is alreadyuseful for us. The theory is in~HOL/Quotient_Examples/FSet.thy (I am using the latest snapshot, but it also should be part of the latest stable release).Below is a short theory which supplies all facts that areneeded to make this type work with nominal. It might needa few adjustments if you work with "old" nominal. Hope this helps, Christian

Jeremy

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

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

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

- Previous by Date: Re: [isabelle] Prove by instantiation
- Next by Date: [isabelle] Fwd: Re: G.U.T.
- Previous by Thread: [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