[isabelle] Isabelle Interval Help



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.

Regards,

Rachel



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


[Attachment stripped: Original attachment type: "application/octet-stream", name: "GramSchmidt.thy"]


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