[isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Thiemann, Rene]

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 <immler at in.tum.de>:
> 
> 
>> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson <lp15 at 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 <immler at in.tum.de <mailto:immler at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev