[isabelle] the hereditarily finite sets



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.