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> 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.