伊莎贝尔:setprod 问题

Question

下面的等式在 Isabelle 中是否成立:

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

如果是，我如何证明？

(* 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 ? *)

Answer 1

仅当您添加假设 inj f 说明 f 是单射时，引理才成立。然后引理来自库引理 setprod_reindex_id，可以使用命令 find_theorems setprod image 找到它。

setprod_reindex_id [unfolded id_def] 为您提供您要求的引理的通用版本。