Dear all, with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a mat”. However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get the additional constraint that the dimensions of the matrix must be non-zero.
To be more precise, assume the following two lemmas (where I omit sort-constraints): lemma one: fixes A B :: “‘a^’n^’m” shows “A + B = B + A” lemma two: fixes A B :: “‘a mat” shows “A : carrier_mat n m ==> B : carrier_mat n m ==> A + B = B + A” From “two” and HMA_Connect you can easily get “one”. But from “one” and HMA_Connect you only get “three” via transfer: lemma three: fixes A B :: “‘a mat” shows “n ~= 0 ==> m ~= 0 ==> A : carrier_mat n m ==> B : carrier_mat n m ==> A + B = B + A” To obtain “two” from “three", one would have to manually proof the result for the corner cases “n = 0 \/ m = 0”. But indeed, Fabian is completely right that lemmas for determinants, etc. are duplicates. Actually, the JNF-matrices “‘a mat” have been developed from scratch (without HMA_Connect), by manually copying and adapting several proofs from the distribution. Cheers, René > Am 26.02.2018 um 18:28 schrieb Fabian Immler <imm...@in.tum.de>: > > >> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson <l...@cam.ac.uk>: >> >> I was at the meeting in Logroño and my impression was that we had to live >> with these different formalisations. There was no way to unify them and the >> best one could hope to transfer certain results from one formalisation to >> another using local types in some incredibly complicated way. > HMA_Connect shows a way to unify (at least parts of) them: it makes explicit > that 'a^'n^'m can be seen as a subtype of 'a mat. > > This makes it possible to avoid duplications: for example, results about > eigenvalues are only proved once for 'a mat and are transferred to the > "subtype" 'a^'n^'m. > In contrast to that, we do have duplicate developments for determinants, > multiplication etc. in isabelle and the AFP. We should be able to get rid of > those. > > Ideally, one would do the developments for 'a^'n^'m, but I am not sure how > well theorems can be transferred in that direction... > > Fabian > > >> If there really is a common basis for formalising linear algebra than I >> would be thrilled to see it, and I'm sure we could figure out a way to >> implement this. >> >> Larry >> >>> On 26 Feb 2018, at 14:57, Fabian Immler <imm...@in.tum.de >>> <mailto:imm...@in.tum.de>> wrote: >>> >>> We do have the problem that AFP/Jordan_Normal_Form/Matrix and >>> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and >>> that there are formalizations of (aspects of) linear algebra for both of >>> them. Last year in Logrono, there was the proposal to put all linear >>> algebra on the common foundation of a locale for modules, but apparently >>> nobody has found the time and motivation to push this much further. >>> >>> Perhaps a more humble first step towards unifying the existing theories >>> would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do >>> the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec. >>> >>> Any opinions on that? >> > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
