How to express arrays in Isabelle/HOL?

Question

I am trying to express arrays, but don't know exactly how. For example, in the following toy lemma that asserts the sum of a series of numbers equals to certain things:

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

, how can I express this for an given array A[i] = i, i = 0..n?

I tried to state it unsuccessfully using vectors (vec) from imports Complex_Main "~~/src/HOL/Analysis/Finite_Cartesian_Product"

as follows:

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

First of all, I don't know how to get vec to accept a parameter n about its size. Secondly, the conclusion part "∑ {A $ x |x. x ∈ {0..(3::nat)} } has some type errors. Maybe vec isn't the right solution. Hence the question here.

In Isabelle, is there any (preferably standard) way to express the array A[i] for i in a range?

(To clarify, I do not need imperative arrays that can be modified as in programming; I just needed mathematical arrays with a size that is known in advance but not fixed to something like 3).

Answer 1

等待大神解答