[isabelle] Define a list over an interval


Just wondering if any of you know how to define an list over an interval? I want to use it within the following definition:

consts lambda_term :: "vector \<Rightarrow> vector \<Rightarrow> "
lambda_term_def: "lambda_term (ith \<lambda> i) == (innerproduct (ith
v n) (ith u i))/(innerproduct (ith u i) (ith u i))"

Where u,v are vectors and Lambda is a scalar. I am trying to run it
over the interval where n is a fixed variable which can be any number,
and i runs from 1 to (n-1). I wonder if you are about at all today?

i.e. I might use v_4 which would find the answer for lambda_1, lambda_2, and lambda_3.


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Attachment stripped: Original attachment type: "text/plain", name: "unnamed"]

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.