Email Gateway (Aug 18 2022 at 11:26): Email Gateway (Aug 18 2022 at 11:26):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:27):From: Steven Obua <obua@in.tum.de>
RF Todd wrote:
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
Email Gateway (Aug 18 2022 at 11:27):From: Tobias Nipkow <nipkow@in.tum.de>
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".
Tobias
Steven Obua wrote:
Last updated: May 03 2024 at 04:19 UTC