# [isabelle] Recursion on finite sets

Hi all,

`I am looking for some way of defining a function recursively over finite
``sets.
``For a datatype t, the datatype package automatically generates a
``recursion operator t_rec with which primitive-recursively functions over
`` that datatype can be defined. For finite sets, I haven't found
``anything similar. The only thing I have found is the fold combinator in
``Finite_Set of type "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set =>
``'a" where "fold f g z A" is f folded over the (multiset) image of A
``under g with initial value z.
``But I would rather like to have some function finite_rec :: "('b set =>
``'b => 'a => 'a) => 'a => 'b set => 'a" that satisfies
`
"finite_rec f z {} = z" and
"[| finite A; ~ (x : A) |]
==> finite f z (insert x A) = f A x (finite_rec f A z)"
for all "well-formed" functions f.

`Is there already something there that I can use like finite_rec or can
``finite_rec be somehow defined using existing fold?
`
Best,
Andreas

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