# [isabelle] Finite_Set comp_fun_commute

Dear Isabelle,
This question is directed at anybody familiar with the Finite_Set theory...
http://isabelle.in.tum.de/library/HOL/Finite_Set.html
... in particular, the Finite_Set.fold functional. Consider the term
Finite_Set.fold f s A
Various lemmas (e.g. Finite_Set.comp_fun_commute.fold_image) require me to show that f satisfies the "comp_fun_commute" property, i.e.
(1) f x o f y = f y o f x
for all x and y. This is too strong a requirement for me. I can show that (1) holds for all x and y in A, but not for all x and y in general. Morally, I *should* only have to show that f commutes when given inputs drawn from A.
It would be quite a bit of hassle for me to convert these lemmas to stronger versions. So I was wondering if anybody has come across this problem before, or knows how to easily strengthen these lemmas, or has any other advice on this topic?
Thanks,
john

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