Hi,
the key theorem here is MATRIX_VECTOR_MUL_COMPONENT.
Here is a proof of your statement:
let MATRIXTWO_MUL_COMPONENT = prove
(`!A:real^2^2 x:real^2.
(A**x)$1 = A$1$1 * x$1 + A$1$2 * x$2 /\
(A**x)$2 = A$2$1 * x$1 + A$2$2 * x$2`,
SIMP_TAC[MATRIX_VECTOR_MUL_COMPONENT;
DIMINDEX_2; LE_REFL; ARITH_RULE `1 <= 2`] THEN
REWRITE_TAC[DOT_2]);;
Hope it helps,
Marco
2018-01-14 8:11 GMT+01:00 Michael Beeson <profbee...@gmail.com>:
> I've been reading the treatment of matrices in vectors.ml. I only need
> two by two matrices for now. I don't find a procedure MATRIX_ARITH
> analogous to VECTOR_ARITH or REAL_ARITH. Is there anything like that?
> Here's a sample I would like to use it on.
>
> let MATRIXTWO_MUL_COMPONENT = prove
> ( `!A:real^2^2 x:real^2.
> (A**x)$1 = A$1$1 * x$1 + A$1$2 * x$2 /\
> (A**x)$2 = A$2$1 * x$1 + A$2$2 * x$2`,
>
> .... I don't know how to prove it. Can anyone help?
> BTW, I am very thankful to all those who have helped me on this list so
> far.
>
> Michael Beeson
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
