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

[Fabian Immler]

> Am 26.02.2018 um 12:54 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> 
> Is there a case for moving some material from this file into the Analysis directory?
> 
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> Many of the results proved at the end of this file are quite straightforward anyway. As somebody with a lifting-and-transfer phobia, I don't feel qualified to make this decision. Possibly these techniques are overkill. I have already proved some of these results quite straightforwardly using linearity, and installed them not long ago.
For the record, "not long ago" is c8caefb20564. I generalized this to the same class constraints as in HMA_Connect in d97a28a006f9.

Yes, I guess these techniques are overkill for the (straightforward) proofs of
matrix_add_vect_distrib,
matrix_vector_right_distrib,
matrix_vector_right_distrib_diff,
matrix_diff_vect_distrib
(they are exactly the lemmas touched by d97a28a006f9). I left them in HMA_Connect.thy as examples for the transfer_hma method.

The remaining lemmas at the end of HMA_Connect are probably not so easy to move to the distribution: they involve concepts that are missing in HOL-Analysis, e.g., eigen_value, charpoly, or similar_matrix.

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?

Fabian



> Larry
> 
>> Begin forwarded message:
>> 
>> From: Fabian Immler <immler at in.tum.de>
>> Subject: Re: [isabelle] Matrix-Vector operation
>> Date: 26 February 2018 at 08:02:40 GMT
>> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
>> Cc: Omar Jasim <oajasim1 at sheffield.ac.uk>
>> 
>> Dear Omar,
>> 
>> Unfortunately, there are no lemmas on distributivity of *v in the distribution.
>> Some are currently in the AFP-entry Perron_Frobenius:
>> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
>> 
>> You can prove them (in HOL-Analysis) as follows:
>> 
>> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: ring_1 ^ 'n)"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf left_diff_distrib)
>> 
>> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_right)
>> 
>> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_left)
>> 
>> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v (v - w) = M *v v - M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf right_diff_distrib)
>> 
>> Those should probably be included in the next Isabelle release.
>> 
>> Hope this helps,
>> Fabian
>> 
>> 
>>> Am 25.02.2018 um 19:27 schrieb Omar Jasim <oajasim1 at sheffield.ac.uk>:
>>> 
>>> Hi,
>>> 
>>> This may be trivial but I have a difficulty proving the following lemma:
>>> 
>>> lemma
>>> fixes  A :: "real^3^3"
>>>   and x::"real^3"
>>> assumes "A>0"
>>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>>> 
>>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>>> related to this?
>>> 
>>> Cheers
>>> Omar
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5026 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180226/54b75526/attachment.bin>