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

[Lawrence Paulson]

Is there a realistic prospect for uniting these two formalisations of linear 
algebra?
Larry

> On 27 Feb 2018, at 11:05, Thiemann, Rene  wrote:
> 
> 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.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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 :
> 
> 
>> 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-...@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