*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] the hereditarily finite sets*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Tue, 27 Mar 2012 02:49:44 -0700 (PDT)*Cc*: cl-isabelle-users at lists.cam.ac.uk

Dear Larry, We (Dmitriy Traytel, Jasmin Blanchette and myself) are prototyping a new (co)datatype package for Isabelle/HOL allowing for nonfree type constructors. With this package, hereditarily finite sets can simply be defined as datatype hfset = Fold hfset fset where 'a fset is the type of finite sets, as defined, e.g., in HOL/Quotient_Examples/FSet. The package proves the expected distinctness, cases, induction and recursion theorems. However, it is currently in a rather raw form. I have used the package to define the type "hfset". To avoid any dependency on our files, I have extracted the relevant types, constants and theorems in the attached theory HFSET.thy that only depends on HOL/Quotient_Examples/FSet. If you are interested, we can also send you the proved version including its prerequisites. The package can also be used to define things like finite possibly non-well-founded sets, as codatatype hfset = Fold hfset fset or heredinarily k-sets, where k is a fixed cardinal. All the best, Andrei PS: The attached paper describes the new package. --- On Mon, 3/26/12, cl-isabelle-users-request at lists.cam.ac.uk <cl-isabelle-users-request at lists.cam.ac.uk> wrote: From: cl-isabelle-users-request at lists.cam.ac.uk <cl-isabelle-users-request at lists.cam.ac.uk> Subject: Cl-isabelle-users Digest, Vol 81, Issue 22 To: cl-isabelle-users at lists.cam.ac.uk Date: Monday, March 26, 2012, 6:00 AM Send Cl-isabelle-users mailing list submissions to cl-isabelle-users at lists.cam.ac.uk To subscribe or unsubscribe via the World Wide Web, visit https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users or, via email, send a message with subject or body 'help' to cl-isabelle-users-request at lists.cam.ac.uk You can reach the person managing the list at cl-isabelle-users-owner at lists.cam.ac.uk When replying, please edit your Subject line so it is more specific than "Re: Contents of Cl-isabelle-users digest..." Today's Topics: 1. the hereditarily finite sets (Lawrence Paulson) 2. Re: the hereditarily finite sets (Andreas Lochbihler) 3. Re: the hereditarily finite sets (Lawrence Paulson) ---------------------------------------------------------------------- Message: 1 Date: Sun, 25 Mar 2012 14:43:17 +0100 From: Lawrence Paulson <lp15 at cam.ac.uk> Subject: [isabelle] the hereditarily finite sets To: isabelle-users <isabelle-users at cl.cam.ac.uk> Message-ID: <F216DC0C-E676-416E-BEC3-2C1A18FD044A at cam.ac.uk> Content-Type: text/plain; charset=us-ascii Is anybody aware of a formalisation of the hereditarily finite sets in Isabelle/HOL? This would be a type hf along with constructors empty :: hf insert :: hf => hf => hf with a membership relation defined by member x (insert y z) == x=y | member x z and also satisfying extensionality: x=y <-> (ALL z. member z x = member z y) (In Isabelle/ZF, the hereditarily finite sets are precisely the elements of Vset(nat).) Larry ------------------------------ Message: 2 Date: Sun, 25 Mar 2012 21:18:46 +0200 From: Andreas Lochbihler <andreas.lochbihler at kit.edu> Subject: Re: [isabelle] the hereditarily finite sets To: Lawrence Paulson <lp15 at cam.ac.uk> Cc: isabelle-users <isabelle-users at cl.cam.ac.uk> Message-ID: <9D1941DA-C51A-4EE4-8EBD-6273C8D07F80 at kit.edu> Content-Type: text/plain; charset=us-ascii Hi Larry, The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP. Actually, it specialises the more general type 'a =>f 'b with constructors finfun_const :: 'b => ('a =>f 'b) finfun_update :: ('a =>f 'b) => 'a => 'b => ('a =>f 'b) and an application operator finfun_apply :: ('a =>f 'b) => 'a => 'b finfun_apply (finfun_update f x y) z = (if z = x then y else finfun_apply f z f = g <--> (ALL x. finfun_apply f x = finfun_apply g x) holds. FinFunSet (or FinFunPred) specialise 'b to bool and thus yield hereditarily finite sets or predicates. Andreas Am 25.03.2012 um 15:43 schrieb Lawrence Paulson: > Is anybody aware of a formalisation of the hereditarily finite sets in Isabelle/HOL? > > This would be a type hf along with constructors > empty :: hf > insert :: hf => hf => hf > with a membership relation defined by > member x (insert y z) == x=y | member x z > and also satisfying extensionality: > x=y <-> (ALL z. member z x = member z y) > > (In Isabelle/ZF, the hereditarily finite sets are precisely the elements of Vset(nat).) > > Larry > > ------------------------------ Message: 3 Date: Sun, 25 Mar 2012 21:30:57 +0100 From: Lawrence Paulson <lp15 at cam.ac.uk> Subject: Re: [isabelle] the hereditarily finite sets To: Andreas Lochbihler <andreas.lochbihler at kit.edu> Cc: isabelle-users <isabelle-users at cl.cam.ac.uk> Message-ID: <57DFB312-ED7D-46B4-A095-44AAE3EC9A7E at cam.ac.uk> Content-Type: text/plain; charset=us-ascii Thanks, but I believe that you are describing finite sets rather than hereditarily finite sets. I should have mentioned, the membership function should have the following type: member :: hf => hf => bool That is, we have one single type rather than separate types of sets and elements. It sounds like this hasn't been formalised before...? Larry On 25 Mar 2012, at 20:18, Andreas Lochbihler wrote: > Hi Larry, > > The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP. End of Cl-isabelle-users Digest, Vol 81, Issue 22 *************************************************

**Attachment:
HFSET.thy**

**Attachment:
codat.pdf**

- Previous by Date: Re: [isabelle] [isabelle-dev] Difference between " induct " and " induct_tac "
- Next by Date: [isabelle] PhD/Postdoc Positions in Theoretical Computer Science at FAU Erlangen-Nürnberg
- Previous by Thread: Re: [isabelle] the hereditarily finite sets
- Next by Thread: [isabelle] class instantiation via class.pred
- Cl-isabelle-users March 2012 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