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).

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?
> >
>
>



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