[isabelle] Finite_Set comp_fun_commute

Dear Isabelle,

This question is directed at anybody familiar with the Finite_Set theory...


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


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