# Re: [isabelle] the hereditarily finite sets

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

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