Re: [isabelle] Vector transpose
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).
On 27 February 2018 at 12:03, Thiemann, Rene <Rene.Thiemann at uibk.ac.at>
> 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
> 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 uibk.ac.at
> > Dear Omar,
> > if you’re not working with “real^’a” but with “real mat” from
> > 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
> >> 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