Re: [isabelle] Recursion on finite sets

Hi Andreas,

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.

Hmmm... How would you specify well-formed? It seems this is not easy...

As far as I know, Finite_Set.fold is all we have at the moment.


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