[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.