# Re: [isabelle] Recursion on finite sets

If f does not take the remaining set A as an argument, then you can
define such a recursion operator completelty along the same lines as the
fold operator currently provided. It will require f to be
left-commutative: f a (f b c) = f b (f a c). See the TPHOLs 2005 paper
by Larry and me for more details. In fact, such an operator would be
welcome.
If the same development could be generalized to your f I am not sure.
Tobias
Andreas Lochbihler wrote:
> 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.*