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 <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. 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 >
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
