*To*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Vector transpose*From*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Date*: Tue, 27 Feb 2018 12:08:39 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4AF39831-97E0-491E-960C-B8D977855CF2@exchange.uibk.ac.at>*References*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com> <FDFF8848-06A0-4300-AF7B-ADBB9F30A489@exchange.uibk.ac.at> <4AF39831-97E0-491E-960C-B8D977855CF2@exchange.uibk.ac.at>

Thanks again. I was just thinking about this idea and I believe it will work. I hope that a don't need AFP entries and HOL theories work with eigenvalues of a matrix (real^'a^'a). Cheers Omar On 27 February 2018 at 12:03, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote: > Dear Omar, > > looking into this again, I just realized that there is already a > “transpose” operation for matrices > in Cartesian_Euclidean_Space. And if you want to convert a vector into a > matrix > of dimension 1 x n or n x 1, then you use rowvector and columnvector. > > For finding these constants you can for instance use > > find_consts "(_,_) vec => ((_,_)vec,_) vec” > > So most likely, you will not require HMA_Connect for the task below. > > Cheers, > René > > > Am 27.02.2018 um 11:56 schrieb Thiemann, Rene <Rene.Thiemann at uibk.ac.at > >: > > > > Dear Omar, > > > > if you’re not working with “real^’a” but with “real mat” from > AFP/Jordan_Normal_Form/Matrix, > > then you find “transpose_mat”. However, there “norm” is not defined. > > > > However, using AFP/Perron_Frobenius/HMA_Connect you might easily be > able to define transpose for “real^’a” > > and then reuse the results for transpose_mat via the transfer-package. > > > > For instance, eigen_vectors for “real^’a^’a” are defined like this, and > results are just transferred. > > > > Cheers, > > René > > > >> I was looking for a transpose of a vector (real^'a) but I couldn't find > it. > >> Probably there is no such definition. The problem I faced is: > >> > >> lemma > >> fixes E :: "(real, 6) vec" > >> and Q :: "((real, 6) vec, 6) vec" > >> and B:: "((real, 3) vec, 6) vec" > >> shows "norm((E v* Q) v* B) = norm(transpose (B) *v (Q*v E))" > >> > >> So please, is there a transpose of a vector defined in Isabelle/HOL? > > > >

**References**:**[isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Thiemann, Rene

**Re: [isabelle] Vector transpose***From:*Thiemann, Rene

- Previous by Date: Re: [isabelle] Vector transpose
- Next by Date: Re: [isabelle] Vector transpose
- Previous by Thread: Re: [isabelle] Vector transpose
- Next by Thread: [isabelle] 1/0 = 0?
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list