The proof you need is below.
It could probably be tidied up further.
I used definitions of row, column and dotprod to delay the introduction
of the sum constant. (Of course, it's possible that I also thus managed
to break the definition of matrix_prod.) In this way, I could eliminate
some uses of FCP, without having to worry about the way FCP might
interact with sum. Then, I needed some lemmas about sum which allowed
me to move them around.
The proof assumes the repository version of HOL. In particular, the %%
infix operator has been replaced by ' (apostrophe).
Michael
--
open bossLib fcpTheory listTheory wordsLib realTheory realLib
simpLib boolTheory boolLib mesonLib Parse fcpLib;
val _ = type_abbrev ("matrix", ``:(real ** 'a) ** 'b``);
val dotprod_def = Define`
dotprod (u : real[??]) (v: real[??]) = sum (0,dimindex(:??)) (??i. u ' i
* v ' i)
`;
val dotprod_FCP = prove(
``(dotprod ($FCP f : real[??]) v = sum (0,dimindex(:??)) (??i. f i * v '
i)) ??
(dotprod u ($FCP f : real[??]) = sum (0,dimindex(:??)) (??i. u ' i * f
i))``,
SRW_TAC [fcpLib.FCP_ss][dotprod_def, SUM_EQ]);
val row_def = Define`
row (A:real[??][??]) i = A ' i : real[??]
`
val row_FCP = prove(
``k < dimindex(:??) ==>
(row ((FCP i j. f i j):real[??][??]) k = FCP j. f k j)``,
SRW_TAC [fcpLib.FCP_ss][row_def]);
val column_def = Define`
column (A:real[??][??]) k = (FCP i. A ' i ' k):real[??]
`;
val column_FCP = prove(
``k < dimindex (:??) ==>
(column ((FCP i j. f i j):real[??][??]) k = FCP i. f i k)``,
SRW_TAC [fcpLib.FCP_ss][column_def]);
val matrix_prod_def = Define`
matrix_prod (A:('p , 'm) matrix) (B:('n, 'p) matrix) =
(FCP i j. dotprod (row A i) (column B j)): ('n , 'm) matrix`;
val _ = overload_on ("**",``matrix_prod``)
val SUM_MULT_L = prove(
``sum (m,n) (\i. f i) * c = sum (m,n) (\i. f i * c)``,
Induct_on `n` THEN SRW_TAC [][sum, REAL_RDISTRIB]);
val SUM_MULT_R = prove(
``c * sum (m,n) (\i. f i) = sum (m,n) (\i. c * f i)``,
Induct_on `n` THEN SRW_TAC [][sum, REAL_LDISTRIB]);
val SUM_PLUS = prove(
``sum (m,n) f + sum (m,n) g = sum (m,n) (\i. f i + g i)``,
Induct_on `n` THEN SRW_TAC [][sum] THEN
POP_ASSUM (fn th => ONCE_REWRITE_TAC [SYM th]) THEN
SRW_TAC [][AC REAL_ADD_ASSOC REAL_ADD_COMM]);
val SUM_SUM = prove(
``sum (m,n) (\i. sum (k,l) (\j. f i j)) =
sum (k,l) (\j. sum (m,n) (\i. f i j))``,
Induct_on `n` THEN SRW_TAC [][sum] THEN1
(Induct_on `l` THEN SRW_TAC [][sum]) THEN
SRW_TAC [][SUM_PLUS]);
val matrix_prod_assoc = prove(
``A ** (B ** C) = (A ** B) ** C``,
SRW_TAC [fcpLib.FCP_ss][matrix_prod_def, row_FCP, column_FCP,
dotprod_FCP] THEN
SRW_TAC [][dotprod_def, SUM_MULT_L, SUM_MULT_R] THEN
SRW_TAC [][SimpLHS, Once SUM_SUM] THEN
MATCH_MP_TAC SUM_EQ THEN SRW_TAC [][] THEN
MATCH_MP_TAC SUM_EQ THEN SRW_TAC [][] THEN
SRW_TAC [fcpLib.FCP_ss][row_def, column_def,
AC REAL_MUL_COMM REAL_MUL_ASSOC])
------------------------------------------------------------------------------
This SF.net email is sponsored by Sprint
What will you do first with EVO, the first 4G phone?
Visit sprint.com/first -- http://p.sf.net/sfu/sprint-com-first
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
