如何在Isabelle/HOL中表示数组？

Question

我正在尝试表达数组，但不知道具体如何表达。例如，在下面的玩具引理中，断言一系列数字的和等于某些东西：

lemma " ∑ {x |x. x ∈ {0..(n::nat)} } = n*(n+1) div 2"

，我如何为给定的数组A[i] = i, i = 0..n表达这一点？

我试图使用imports Complex_Main "~~/src/HOL/Analysis/Finite_Cartesian_Product"中的向量(vec)来说明它，但没有成功

如下所示：

lemma test_array:
  fixes n::nat and A::"(nat,3) vec"
  shows "∑ {A $ x |x. x ∈ {0..(3::nat)} } = 3*4 div 2"

首先，我不知道如何让vec接受有关其大小的参数n。其次，结论部分"∑ {A $ x |x. x ∈ {0..(3::nat)} }存在一些类型错误。也许vec不是正确的解决方案。因此这里就有了这个问题。

在Isabelle中，是否有任何(最好是标准的)方法来表示范围内i的数组A[i]？

(为了澄清，我不需要像在编程中那样可以修改的命令式数组；我只需要具有预先知道的大小但不固定为3之类的大小的数学数组)。

Answer 1

如果不了解更多具体的应用程序，就很难在这里给出好的建议。

我认为最标准的方法是使用函数而不是数组。如果需要，您可以在紧凑域之外表示这些值为零。然而，Isabelle中无限对象的和总是为零。

如果你真的需要一个长度的东西:在你说的评论中，你想使用int，但也许你的索引是正的，你可以将它们转换成nat，使得使用列表成为可能？