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).

question from:https://stackoverflow.com/questions/65834992/how-to-express-arrays-in-isabelle-hol

Answer 1

Without knowing more about the concrete applications it is hard to give good advice here.

I believe that the most standard way to do this is to use a function and not an array. If needed, you can express that the values are zero outside of a compact domain. However, sums over infinite objects in Isabelle are always zero.

If you really need something with a length: In the comments you said, you wanted to use int, but maybe your indices are positive anyway and you can convert them to nat, making it possible to use lists anyway?