Email Gateway (Aug 22 2022 at 16:39): Email Gateway (Aug 22 2022 at 16:39):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear list,
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 (Qv E))"
So please, is there a transpose of a vector defined in Isabelle/HOL?
Many thanks
Omar
Email Gateway (Aug 22 2022 at 16:39):From: "Thiemann, Rene" <Rene.Thiemann@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é
Email Gateway (Aug 22 2022 at 16:40):From: Omar Jasim <oajasim1@sheffield.ac.uk>
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
Email Gateway (Aug 22 2022 at 16:40):From: "Thiemann, Rene" <Rene.Thiemann@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 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é
Email Gateway (Aug 22 2022 at 16:40):From: Omar Jasim <oajasim1@sheffield.ac.uk>
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
Email Gateway (Aug 22 2022 at 16:40):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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.
Cheers,
René
Email Gateway (Aug 22 2022 at 16:40):From: Makarius <makarius@sketis.net>
The theory name Matrix is already used in session Jordan_Normal_Form, so
you need to rename your own theory -- it appears as Draft.Matrix above.
(Draft is the implicit session name for the PIDE editor session).
Makarius
Email Gateway (Aug 22 2022 at 16:40):From: Omar Jasim <oajasim1@sheffield.ac.uk>
My theory name is different but I think that there are two different
theories which have the same name "Matrix.thy". The first
"HOL/Matrix_LP/Matrix.thy" and the second " Jordan_Normal_Form/Matrix.thy".
Omar
Email Gateway (Aug 22 2022 at 16:40):From: Makarius <makarius@sketis.net>
In Isabelle2017 imports from other sessions should always use the unique
qualified name -- the Prover IDE should actually resolve that correctly
for files opened in the editor as well, i.e. Draft.Matrix should not occur.
I've made a quick test as follows:
* start Isabelle/jEdit with AFP/thys as session root directory (option
-d on the command line or a suitable entry in ISABELLE_HOME_USER/ROOTS)
* open theory file $ISABELLE_HOME/src/HOL/Matrix_LP/Matrix.thy
-- it correctly gets the formal theory name HOL-Matrix_LP.Matrix (e.g.
hover over the entry in the Theories dockable)
* open theory file $AFP/Jordan_Normal_Form/Matrix.thy -- it correctly
gets the formal theory name Jordan_Normal_Form.Matrix
* import both into the Scratch theory:
theory Scratch
imports "HOL-Matrix_LP.Matrix" "Jordan_Normal_Form.Matrix"
begin
This correctly produces the failure:
exception THEORY raised (line 230 of "context.ML"):
Duplicate theory name
{..., Factorial_Ring, Missing_Ring, Module, Ring_Hom,
Jordan_Normal_Form.Matrix}
{..., Complex, MacLaurin, Complex_Main, Lattice_Algebras,
HOL-Matrix_LP.Matrix}
So no Draft.Matrix to be seen here.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC