Re: [isabelle] the hereditarily finite sets



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
Description: Binary data

Attachment: codat.pdf
Description: Adobe PDF document



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.