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.


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.