Isabelle: Issue with setprod

问题:

Does the following equality hold in Isabelle:

setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set))

If yes, how can I prove it?

(* tested with Isabelle2013-2 *)
theory Notepad
imports
  Main
  "~~/src/HOL/Library/Polynomial"
begin

notepad
begin{
fix f :: "'n∷finite ⇒ ('a::comm_ring_1 poly)"

have "finite (UNIV :: 'n∷finite set)" by simp
from this have "setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set))" 
sorry (* can this be proven ? *)

回答1:

The lemma holds only if you add the assumption inj f stating that f is injective. The lemma then follows from the library lemma setprod_reindex_id, which can be found using the command find_theorems setprod image.

setprod_reindex_id [unfolded id_def] gives you a generalized version of the lemma you asked for.