Re: [isabelle] Vector transpose

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.


> Am 27.02.2018 um 11:56 schrieb Thiemann, Rene <Rene.Thiemann 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?

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