> Am 26.02.2018 um 12:54 schrieb Lawrence Paulson <l...@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 <imm...@in.tum.de> >> Subject: Re: [isabelle] Matrix-Vector operation >> Date: 26 February 2018 at 08:02:40 GMT >> To: isabelle-users <isabelle-us...@cl.cam.ac.uk> >> Cc: Omar Jasim <oajas...@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 <oajas...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
