我试图将我在this answer给出的论点翻译成Isabelle，而我managed几乎完全证明了这一点。但是，我还需要证明：
"(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
(∑q | q ∈ {1..n/d}. f (q/(n/d)))" for d :: nat
我的想法是使用这个定理：
sum.reindex_bij_witness
但是，我无法实例化与定理的集合S，T相关的变换i，j。原则上，设置应该是：
S = {k. k ∈ {1..n} ∧ d dvd k}
T = {q. q ∈ {1..n/d}}
i k = k/d
j q = q d
我相信有打字错误。也许我应该使用div？
首先，请注意，你应该写gcd a b = 1而不是coprime a b。这是等效的（至少对于所有具有GCD的类型），但使用起来更方便。
其次，我不会写像⋀n. F n = …这样的假设。把它写成defines更有意义，即
lemma
fixes F :: "nat ⇒ complex"
defines "F ≡ (λn. …)"
第三，{q. q ∈ {1..n/d}}与{1..n/d}完全相同，所以我建议你这样写。
要回答你的实际问题：如果你在问题中写的是你在Isabelle和n以及d中写的是nat类型，你应该知道{q. q ∈ {1..n/d}}实际上意味着{1..real n / real d}。如果n / d > 1，这实际上是一组无限的实数，可能不是你想要的。
你真正想要的可能是设置{1..n div d}，其中div表示对自然数的划分。这是一组有限的自然数。
然后你可以很容易地证明以下内容：
lemma
fixes f :: "real ⇒ complex" and n d :: nat
assumes "d > 0" "d dvd n"
shows "(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
(∑q∈{1..n div d}. f (q/(n/d)))"
by (rule sum.reindex_bij_witness[of _ "λk. k * d" "λk. k div d"])
(use assms in ‹force simp: div_le_mono›)+
div和/表示相同的功能，即Rings.divide.divide。然而，/出于历史原因（也许是对Pascal的美好记忆），/还强加了类型类限制inverse，即它只适用于具有inverse函数的类型。
在大多数实际情况中，这意味着div是对环的一般分割操作，而/只适用于场（或分环，或者像“正式幂级数”那样'几乎'场的事物）。
如果你为自然数a / b和a写b，那么这是一个类型错误。伊莎贝尔的强制系统然后推断你可能打算写real a / real b，这就是你得到的。
在这种情况下查看输出是一个好主意，以确保推断的强制符合您的预期。
如果您应用某些规则（例如使用apply (rule …)）并且它失败并且您不明白为什么，那么有一个小技巧可以找到。如果在using [[unify_trace_failure]]之前添加apply，则会收到一条错误消息，指出统一失败的确切位置。在这种情况下，消息是
The following types do not unify:
(nat ⇒ complex) ⇒ nat set ⇒ complex
(real ⇒ complex) ⇒ real set ⇒ complex
这表明在某个地方存在一个总和，它应该是对一组自然的总和。