Dear all,

with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a 
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 

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.


> Am 26.02.2018 um 18:28 schrieb Fabian Immler <>:
>> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson <>:
>> 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 < 
>>> <>> 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 mailing list

Reply via email to