Re: [isabelle] Vector transpose

Dear Omar,

I would recommend to look at the general Isabelle and AFP documentation and in particular the installation instruction.
The error might indicate that you imported some ROOT file twice, or that you you import a theory-file in two different ways,
or that indeed you work with two versions of a “Matrix.thy” (e.g., the one in the AFP/Jordan_Normal_Form and a local file) 
which is not supported.


> Am 27.02.2018 um 12:44 schrieb Omar Jasim <oajasim1 at>:
> Thanks Rene for this. I have a problem with calling AFP in Isabelle/HOL 2017 under Windows 10. I didn't have such problem with the previous versions but it seems the ROOT file is changed in this version. However, the called theory from AFP "imports Perron_Frobenius.HMA_Connect" is loaded with all associated theories but I have the following error message:
> exception THEORY raised (line 230 of "context.ML"):
>   Duplicate theory name
>   {..., Complex, MacLaurin, Complex_Main, Lattice_Algebras, Draft.Matrix}
>   {..., Factorial_Ring, Missing_Ring, Module, Ring_Hom, Jordan_Normal_Form.Matrix}
> Omar 
> On 27 February 2018 at 10:56, Thiemann, Rene <Rene.Thiemann at> wrote:
> 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.