# [isabelle] fold definitions over sets

```Dear all,

recently, I came across an alternative way to define
a fold on finite sets. In contrast to the Isabelle
library version (discussed in the recent TPHOLs Paper),
it has a slightly more general type:

fold : [['a, 'b] => 'b, 'b, 'a set] => 'b

but still fulfills (for finite sets S) the computational
rules:

fold f b {} = b

\<forall> a b c. (f a (f b c)) = (f b (f a c)) ==>
fold f b (insert a S) = f a (fold f b (S - {a}))

It does neither assume ACn, although
\<forall> a b c. (f a (f b c)) = (f b (f a c))
implies this, if f has type instance ['a, 'a] => 'a
and is furthermore right-neutral.

It is strictly more general: you can define the
cardinality of finite sets by this fold, but not
by the old one, for example.

The same algorithmic scheme would work for multi-sets too,

A) Is this something widely known? (Refs ?)
Is it existing in other libraries of HOL systems?

B) Wouldn't it be a better candidate
for the Isabelle/HOL library?

-bu

```

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