*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] the hereditarily finite sets*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 25 Mar 2012 14:43:17 +0100

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

**Follow-Ups**:**Re: [isabelle] the hereditarily finite sets***From:*Andreas Lochbihler

**Re: [isabelle] the hereditarily finite sets***From:*Brian Huffman

- Previous by Date: Re: [isabelle] declaration attribute
- Next by Date: Re: [isabelle] the hereditarily finite sets
- Previous by Thread: Re: [isabelle] [isabelle-dev] Relations vs. Predicates
- Next by Thread: Re: [isabelle] the hereditarily finite sets
- 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