Re: [isabelle] Isabelle Interval Help

One more thought: you might be able to use the foldl function from theory List. Something like "foldl f a [0..<n]". This iterates f over [0,...,n-1] with start value "a".


Steven Obua wrote:
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".



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