# Re: [isabelle] the hereditarily finite sets

I don't know of a pre-existing formalization, but I couldn't resist
looking for a way to formalize this myself. I found an approach that
looks promising:
Start with a "raw" tree datatype using lists instead of finite sets:
datatype hf0 = Node "hf0 list"
(or equivalently, datatype hf0 = Empty | Insert hf0 hf0)
Define a linear order on type hf0 using a lexicographic order on the
lists. Then define a predicate "normal :: hf0 => bool" asserting that
all lists in the whole tree are in strict sorted order. Finally,
define type hf as a subtype:
typedef hf = "{a. normal a}"
I got as far as defining insert and member on type hf, but I didn't
prove extensionality. For this, I guess you would need a lemma stating
that "set xs = set ys ==> xs = ys" for strictly sorted lists xs and
ys. There might be some relevant stuff in List.thy already, but I'm
not sure.
- Brian
On Sun, Mar 25, 2012 at 3:43 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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
>
>

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