RF Todd wrote:

Hi all,
I am just wondering if you know how to create a definition in Isabelle
or Isar over a specific interval.
I am trying to create the Gram-Schmidt Process in Isabelle and have
come across the problem of how to define:
(ith lambda i) = (innerproduct (ith v n) (ith u i))/(innerproduct (ith
u i) (ith u i)) over the interval i = 1,..,(n-1)

`I want to calculate each lambda starting with the first lambda and
``then finishing on the (n-1)th lambda. Not sure how to do this in
``Isabelle.
`

`There is no definitional construct in Isabelle for doing a definition in
``the style you suggest above.
`

`By the way, note that the use of the name "lambda" is probably confusing
``for most Isabelle users, as one thinks automatically of a function...
`
So, what is the type of lambda, v, and u ?

`It seems to be some kind of list of vectors? If this is so, then you
``cannot define lambda by saying what "ith lambda i" is for i=1..,,n-1.
``You would need to define a list of length n-1 such that the above
``property holds. Note also that list indices start with 0, not with 1.
`

`As Gram-Schmidt is basically a recursive procedure, you could define a
``recursive function that does the job of modelling this procedure. There
``is lots of support for defining recursive functions in Isabelle, but
``there is no support for defining things in the above "interval-style".
`
Best,
Steven