100/cayley_hamilton.ml

   1 (* ========================================================================= *)
   2 (* The Cayley-Hamilton theorem (for real matrices).                          *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/complexes.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Powers of a square matrix (mpow) and sums of matrices (msum).             *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 parse_as_infix("mpow",(24,"left"));;
  12
  13 let mpow = define
  14   `(!A:real^N^N. A mpow 0 = (mat 1 :real^N^N)) /\
  15    (!A:real^N^N n. A mpow (SUC n) = A ** A mpow n)`;;
  16
  17 let msum = new_definition
  18  `msum = iterate (matrix_add)`;;
  19
  20 let NEUTRAL_MATRIX_ADD = prove
  21  (`neutral((+):real^N^M->real^N^M->real^N^M) = mat 0`,
  22   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
  23   MESON_TAC[MATRIX_ADD_RID; MATRIX_ADD_LID]);;
  24
  25 let MONOIDAL_MATRIX_ADD = prove
  26  (`monoidal((+):real^N^M->real^N^M->real^N^M)`,
  27   REWRITE_TAC[monoidal; NEUTRAL_MATRIX_ADD] THEN
  28   REWRITE_TAC[MATRIX_ADD_LID; MATRIX_ADD_ASSOC] THEN
  29   REWRITE_TAC[MATRIX_ADD_SYM]);;
  30
  31 let MSUM_CLAUSES = prove
  32  (`(!(f:A->real^N^M). msum {} f = mat 0) /\
  33    (!x (f:A->real^N^M) s.
  34         FINITE(s)
  35         ==> (msum (x INSERT s) f =
  36              if x IN s then msum s f else f(x) + msum s f))`,
  37   REWRITE_TAC[msum; GSYM NEUTRAL_MATRIX_ADD] THEN
  38   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  39   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
  40
  41 let MSUM_MATRIX_RMUL = prove
  42  (`!(f:A->real^N^M) (A:real^P^N) s.
  43         FINITE s ==> msum s (\i. f(i) ** A) = msum s f ** A`,
  44   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  45   SIMP_TAC[MSUM_CLAUSES; MATRIX_MUL_LZERO; MATRIX_ADD_RDISTRIB]);;
  46
  47 let MSUM_MATRIX_LMUL = prove
  48  (`!(f:A->real^P^N) (A:real^N^M) s.
  49         FINITE s ==> msum s (\i. A ** f(i)) = A ** msum s f`,
  50   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  51   SIMP_TAC[MSUM_CLAUSES; MATRIX_MUL_RZERO; MATRIX_ADD_LDISTRIB]);;
  52
  53 let MSUM_ADD = prove
  54  (`!f g s. FINITE s ==> (msum s (\x. f(x) + g(x)) = msum s f + msum s g)`,
  55   SIMP_TAC[msum; ITERATE_OP; MONOIDAL_MATRIX_ADD]);;
  56
  57 let MSUM_CMUL = prove
  58  (`!(f:A->real^N^M) c s.
  59         FINITE s ==>  msum s (\i. c %% f(i)) = c %% msum s f`,
  60   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  61   SIMP_TAC[MSUM_CLAUSES; MATRIX_CMUL_ADD_LDISTRIB; MATRIX_CMUL_RZERO]);;
  62
  63 let MSUM_NEG = prove
  64  (`!(f:A->real^N^M) s.
  65         FINITE s ==>  msum s (\i. --(f(i))) = --(msum s f)`,
  66   ONCE_REWRITE_TAC[MATRIX_NEG_MINUS1] THEN
  67   REWRITE_TAC[MSUM_CMUL]);;
  68
  69 let MSUM_SUB = prove
  70  (`!f g s. FINITE s ==> (msum s (\x. f(x) - g(x)) = msum s f - msum s g)`,
  71   REWRITE_TAC[MATRIX_SUB; MATRIX_NEG_MINUS1] THEN
  72   SIMP_TAC[MSUM_ADD; MSUM_CMUL]);;
  73
  74 let MSUM_CLAUSES_LEFT = prove
  75  (`!f m n. m <= n ==> msum(m..n) f = f(m) + msum(m+1..n) f`,
  76   SIMP_TAC[GSYM NUMSEG_LREC; MSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
  77   ARITH_TAC);;
  78
  79 let MSUM_SUPPORT = prove
  80  (`!f s. msum (support (+) f s) f = msum s f`,
  81   SIMP_TAC[msum; iterate; SUPPORT_SUPPORT]);;
  82
  83 let MSUM_EQ = prove
  84  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> (msum s f = msum s g)`,
  85   REWRITE_TAC[msum] THEN
  86   MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
  87
  88 let MSUM_RESTRICT_SET = prove
  89  (`!P s f. msum {x:A | x IN s /\ P x} f =
  90            msum s (\x. if P x then f(x) else mat 0)`,
  91   ONCE_REWRITE_TAC[GSYM MSUM_SUPPORT] THEN
  92   REWRITE_TAC[support; NEUTRAL_MATRIX_ADD; IN_ELIM_THM] THEN
  93   REWRITE_TAC[MESON[] `~((if P x then f x else a) = a) <=> P x /\ ~(f x = a)`;
  94               GSYM CONJ_ASSOC] THEN
  95   REPEAT GEN_TAC THEN MATCH_MP_TAC MSUM_EQ THEN SIMP_TAC[IN_ELIM_THM]);;
  96
  97 let MSUM_SING = prove
  98  (`!f x. msum {x} f = f(x)`,
  99   SIMP_TAC[MSUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; MATRIX_ADD_RID]);;
 100
 101 let MSUM_IMAGE = prove
 102  (`!f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
 103            ==> (msum (IMAGE f s) g = msum s (g o f))`,
 104   REWRITE_TAC[msum; GSYM NEUTRAL_MATRIX_ADD] THEN
 105   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
 106
 107 let MSUM_OFFSET = prove
 108  (`!p f m n. msum(m+p..n+p) f = msum(m..n) (\i. f(i + p))`,
 109   SIMP_TAC[NUMSEG_OFFSET_IMAGE; MSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
 110   REWRITE_TAC[o_DEF]);;
 111
 112 let MSUM_COMPONENT = prove
 113  (`!f:A->real^N^M i j s.
 114         1 <= i /\ i <= dimindex(:M) /\
 115         1 <= j /\ j <= dimindex(:N) /\
 116         FINITE s
 117         ==> (msum s f)$i$j = sum s (\a. f(a)$i$j)`,
 118   REPLICATE_TAC 3 GEN_TAC THEN
 119   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 120   REPEAT DISCH_TAC THEN
 121   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 122   SIMP_TAC[MSUM_CLAUSES; SUM_CLAUSES] THEN
 123   ASM_SIMP_TAC[MATRIX_ADD_COMPONENT; MAT_COMPONENT; COND_ID]);;
 124
 125 let MSUM_CLAUSES_NUMSEG = prove
 126  (`(!m. msum(m..0) f = if m = 0 then f(0) else mat 0) /\
 127    (!m n. msum(m..SUC n) f = if m <= SUC n then msum(m..n) f + f(SUC n)
 128                              else msum(m..n) f)`,
 129   REWRITE_TAC[MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_MATRIX_ADD;
 130               NEUTRAL_MATRIX_ADD; msum]);;
 131
 132 let MPOW_ADD = prove
 133  (`!A:real^N^N m n. A mpow (m + n) = A mpow m ** A mpow n`,
 134   GEN_TAC THEN INDUCT_TAC THEN
 135   ASM_REWRITE_TAC[ADD_CLAUSES; mpow; MATRIX_MUL_LID] THEN
 136   REWRITE_TAC[MATRIX_MUL_ASSOC]);;
 137
 138 let MPOW_1 = prove
 139  (`!A:real^N^N. A mpow 1 = A`,
 140   REWRITE_TAC[num_CONV `1`; mpow] THEN
 141   REWRITE_TAC[SYM(num_CONV `1`); MATRIX_MUL_RID]);;
 142
 143 let MPOW_SUC = prove
 144  (`!A:real^N^N n. A mpow (SUC n) = A mpow n ** A`,
 145   REWRITE_TAC[ADD1; MPOW_ADD; MPOW_1]);;
 146
 147 (* ------------------------------------------------------------------------- *)
 148 (* The main lemma underlying the proof.                                      *)
 149 (* ------------------------------------------------------------------------- *)
 150
 151 let MATRIC_POLYFUN_EQ_0 = prove
 152  (`!n A:num->real^N^M.
 153         (!x. msum(0..n) (\i. x pow i %% A i) = mat 0) <=>
 154         (!i. i IN 0..n ==> A i = mat 0)`,
 155   SIMP_TAC[CART_EQ; MSUM_COMPONENT; MAT_COMPONENT; LAMBDA_BETA;
 156            FINITE_NUMSEG; COND_ID;
 157            ONCE_REWRITE_RULE[REAL_MUL_SYM] MATRIX_CMUL_COMPONENT] THEN
 158   REWRITE_TAC[MESON[]
 159    `(!x i. P i ==> !j. Q j ==> R x i j) <=>
 160     (!i. P i ==> !j. Q j ==> !x. R x i j)`] THEN
 161   REWRITE_TAC[REAL_POLYFUN_EQ_0] THEN MESON_TAC[]);;
 162
 163 let MATRIC_POLY_LEMMA = prove
 164  (`!(A:real^N^N) B (C:real^N^N) n.
 165         (!x. msum (0..n) (\i. (x pow i) %% B i) ** (A - x %% mat 1) = C)
 166         ==> C = mat 0`,
 167   SIMP_TAC[GSYM MSUM_MATRIX_RMUL; FINITE_NUMSEG; MATRIX_SUB_LDISTRIB] THEN
 168   REWRITE_TAC[MATRIX_MUL_RMUL] THEN ONCE_REWRITE_TAC[MATRIX_MUL_LMUL] THEN
 169   ONCE_REWRITE_TAC[MATRIX_CMUL_ASSOC] THEN
 170   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 171   SIMP_TAC[MSUM_SUB; FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN
 172   SUBGOAL_THEN
 173    `!x. msum(0..SUC n)
 174          (\i. x pow i %% (((if i = 0 then (--C:real^N^N) else mat 0) +
 175                            (if i <= n then B i ** (A:real^N^N) else mat 0)) -
 176                           (if i = 0 then mat 0 else B(i - 1) ** mat 1))) =
 177         mat 0`
 178   MP_TAC THENL
 179    [SIMP_TAC[MATRIX_CMUL_SUB_LDISTRIB; MSUM_SUB; FINITE_NUMSEG;
 180              MATRIX_CMUL_ADD_LDISTRIB; MSUM_ADD] THEN
 181     ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[MATRIX_CMUL_RZERO] THEN
 182     ONCE_REWRITE_TAC[MESON[]
 183      `(if p then mat 0 else x) = (if ~p then x else mat 0)`] THEN
 184     REWRITE_TAC[GSYM MSUM_RESTRICT_SET; IN_NUMSEG] THEN
 185     REWRITE_TAC[ARITH_RULE `(0 <= i /\ i <= SUC n) /\ i = 0 <=> i = 0`;
 186       ARITH_RULE `(0 <= i /\ i <= SUC n) /\ i <= n <=> 0 <= i /\ i <= n`;
 187       ARITH_RULE `(0 <= i /\ i <= SUC n) /\ ~(i = 0) <=>
 188                   1 <= i /\ i <= SUC n`] THEN
 189     REWRITE_TAC[SING_GSPEC; GSYM numseg; MSUM_SING; real_pow] THEN
 190     REWRITE_TAC[MATRIX_CMUL_LID] THEN
 191     FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC ONCE_DEPTH_CONV [GSYM th]) THEN
 192     REWRITE_TAC[MATRIX_NEG_SUB] THEN REWRITE_TAC[MATRIX_SUB; AC MATRIX_ADD_AC
 193      `(((A:real^N^N) + --B) + B) + C = (--B + B) + A + C`] THEN
 194     REWRITE_TAC[MATRIX_ADD_LNEG; MATRIX_ADD_LID] THEN
 195     REWRITE_TAC[num_CONV `1`] THEN REWRITE_TAC[ADD1; MSUM_OFFSET] THEN
 196     REWRITE_TAC[ADD_CLAUSES; ADD_SUB; MATRIX_ADD_RNEG];
 197     REWRITE_TAC[MATRIC_POLYFUN_EQ_0; IN_NUMSEG; LE_0] THEN DISCH_TAC THEN
 198     SUBGOAL_THEN `!i:num. B(n - i) = (mat 0:real^N^N)` MP_TAC THENL
 199      [MATCH_MP_TAC num_INDUCTION THEN CONJ_TAC THENL
 200        [FIRST_X_ASSUM(MP_TAC o SPEC `SUC n`) THEN
 201         REWRITE_TAC[LE_REFL; SUB_0; NOT_SUC; ARITH_RULE `~(SUC n <= n)`] THEN
 202         REWRITE_TAC[MATRIX_ADD_LID; SUC_SUB1; MATRIX_MUL_RID] THEN
 203         REWRITE_TAC[MATRIX_SUB_LZERO; MATRIX_NEG_EQ_0];
 204         X_GEN_TAC `m:num` THEN DISCH_TAC THEN
 205         DISJ_CASES_TAC(ARITH_RULE `n - SUC m = n - m \/ m < n`) THEN
 206         ASM_REWRITE_TAC[] THEN
 207         FIRST_X_ASSUM(MP_TAC o SPEC `n - m:num`) THEN
 208         ASM_SIMP_TAC[ARITH_RULE `m < n ==> ~(n - m = 0)`;
 209                      ARITH_RULE `n - m <= SUC n /\ n - m <= n`] THEN
 210         REWRITE_TAC[MATRIX_MUL_LZERO; MATRIX_ADD_LID; MATRIX_SUB_LZERO] THEN
 211         REWRITE_TAC[MATRIX_MUL_RID; MATRIX_NEG_EQ_0] THEN
 212         ASM_SIMP_TAC[ARITH_RULE `n - m - 1 = n - SUC m`]];
 213       DISCH_THEN(MP_TAC o SPEC `n:num`) THEN REWRITE_TAC[SUB_REFL] THEN
 214       DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `0`) THEN
 215       ASM_REWRITE_TAC[LE_0; MATRIX_MUL_LZERO; MATRIX_ADD_RID] THEN
 216       REWRITE_TAC[MATRIX_SUB_RZERO; MATRIX_NEG_EQ_0]]]);;
 217
 218 (* ------------------------------------------------------------------------- *)
 219 (* Show that cofactor and determinant are n-1 and n degree polynomials.      *)
 220 (* ------------------------------------------------------------------------- *)
 221
 222 let POLYFUN_N_CONST = prove
 223  (`!c n. ?b. !x. c = sum(0..n) (\i. b i * x pow i)`,
 224   REPEAT STRIP_TAC THEN
 225   EXISTS_TAC `\i. if i = 0 then c else &0` THEN
 226   REWRITE_TAC[COND_RAND; COND_RATOR; REAL_MUL_LZERO] THEN
 227   REWRITE_TAC[GSYM SUM_RESTRICT_SET; IN_NUMSEG] THEN
 228   REWRITE_TAC[ARITH_RULE `(0 <= i /\ i <= n) /\ i = 0 <=> i = 0`] THEN
 229   REWRITE_TAC[SING_GSPEC; SUM_SING; real_pow; REAL_MUL_RID]);;
 230
 231 let POLYFUN_N_ADD = prove
 232  (`!f g. (?b. !x. f(x) = sum(0..n) (\i. b i * x pow i)) /\
 233          (?c. !x. g(x) = sum(0..n) (\i. c i * x pow i))
 234          ==> ?d. !x. f(x) + g(x) = sum(0..n) (\i. d i * x pow i)`,
 235   REPEAT STRIP_TAC THEN
 236   EXISTS_TAC `\i. (b:num->real) i + c i` THEN
 237   ASM_REWRITE_TAC[SUM_ADD_NUMSEG; REAL_ADD_RDISTRIB]);;
 238
 239 let POLYFUN_N_CMUL = prove
 240  (`!f c. (?b. !x. f(x) = sum(0..n) (\i. b i * x pow i))
 241          ==> ?b. !x. c * f(x) = sum(0..n) (\i. b i * x pow i)`,
 242   REPEAT STRIP_TAC THEN
 243   EXISTS_TAC `\i. c * (b:num->real) i` THEN
 244   ASM_REWRITE_TAC[SUM_LMUL; GSYM REAL_MUL_ASSOC]);;
 245
 246 let POLYFUN_N_SUM = prove
 247  (`!f s. FINITE s /\
 248          (!a. a IN s ==> ?b. !x. f x a = sum(0..n) (\i. b i * x pow i))
 249          ==> ?b. !x. sum s (f x) = sum(0..n) (\i. b i * x pow i)`,
 250   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 251   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 252   SIMP_TAC[SUM_CLAUSES; FORALL_IN_INSERT; NOT_IN_EMPTY; POLYFUN_N_CONST] THEN
 253   REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
 254   MATCH_MP_TAC POLYFUN_N_ADD THEN ASM_SIMP_TAC[]);;
 255
 256 let POLYFUN_N_PRODUCT = prove
 257  (`!f s n. FINITE s /\
 258            (!a:A. a IN s ==> ?c d. !x. f x a = c + d * x) /\ CARD(s) <= n
 259            ==> ?b. !x. product s (f x) = sum(0..n) (\i. b i * x pow i)`,
 260   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 261   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 262   SIMP_TAC[PRODUCT_CLAUSES; POLYFUN_N_CONST; FORALL_IN_INSERT] THEN
 263   REPEAT GEN_TAC THEN DISCH_THEN(fun th ->
 264     DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN MP_TAC th) THEN
 265   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 266   ASM_SIMP_TAC[CARD_CLAUSES] THEN
 267   INDUCT_TAC THENL [ARITH_TAC; REWRITE_TAC[LE_SUC]] THEN DISCH_TAC THEN
 268   FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[] THEN
 269   DISCH_THEN(X_CHOOSE_TAC `b:num->real`) THEN
 270   FIRST_X_ASSUM(X_CHOOSE_THEN `c:real` (X_CHOOSE_TAC `d:real`)) THEN
 271   ASM_REWRITE_TAC[] THEN
 272   EXISTS_TAC `\i. (if i <= n then c * b i else &0) +
 273                   (if ~(i = 0) then d * b(i - 1) else &0)` THEN
 274   X_GEN_TAC `x:real` THEN
 275   REWRITE_TAC[REAL_ADD_RDISTRIB; SUM_ADD_NUMSEG] THEN
 276   REWRITE_TAC[COND_RAND; COND_RATOR; GSYM SUM_LMUL; REAL_MUL_LZERO] THEN
 277   REWRITE_TAC[GSYM SUM_RESTRICT_SET; IN_NUMSEG] THEN
 278   REWRITE_TAC[ARITH_RULE
 279    `((0 <= i /\ i <= SUC n) /\ i <= n <=> 0 <= i /\ i <= n) /\
 280     ((0 <= i /\ i <= SUC n) /\ ~(i = 0) <=> 1 <= i /\ i <= SUC n)`] THEN
 281   REWRITE_TAC[GSYM numseg] THEN
 282   REWRITE_TAC[MESON[num_CONV `1`; ADD1] `1..SUC n = 0+1..n+1`] THEN
 283   REWRITE_TAC[SUM_OFFSET; ADD_SUB; REAL_POW_ADD] THEN
 284   BINOP_TAC THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN REAL_ARITH_TAC);;
 285
 286 let COFACTOR_ENTRY_AS_POLYFUN = prove
 287  (`!A:real^N^N x i j.
 288         1 <= i /\ i <= dimindex(:N) /\
 289         1 <= j /\ j <= dimindex(:N)
 290         ==> ?c. !x. cofactor(A - x %% mat 1)$i$j =
 291                     sum(0..dimindex(:N)-1) (\i. c(i) * x pow i)`,
 292   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[cofactor; LAMBDA_BETA; det] THEN
 293   MATCH_MP_TAC POLYFUN_N_SUM THEN
 294   SIMP_TAC[FINITE_PERMUTATIONS; FINITE_NUMSEG; FORALL_IN_GSPEC] THEN
 295   X_GEN_TAC `p:num->num` THEN DISCH_TAC THEN
 296   MATCH_MP_TAC POLYFUN_N_CMUL THEN
 297   SUBGOAL_THEN `1..dimindex(:N) = i INSERT ((1..dimindex(:N)) DELETE i)`
 298   SUBST1_TAC THENL
 299    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE; IN_NUMSEG] THEN ASM_ARITH_TAC;
 300     SIMP_TAC[PRODUCT_CLAUSES; FINITE_DELETE; FINITE_NUMSEG]] THEN
 301   ASM_REWRITE_TAC[IN_DELETE; IN_NUMSEG] THEN
 302   MATCH_MP_TAC POLYFUN_N_CMUL THEN
 303   MATCH_MP_TAC POLYFUN_N_PRODUCT THEN
 304   SIMP_TAC[CARD_DELETE; FINITE_DELETE; FINITE_NUMSEG] THEN
 305   ASM_REWRITE_TAC[IN_NUMSEG; IN_DELETE; CARD_NUMSEG_1; LE_REFL] THEN
 306   X_GEN_TAC `k:num` THEN STRIP_TAC THEN
 307   SUBGOAL_THEN `(p:num->num) k IN 1..dimindex(:N)` MP_TAC THENL
 308    [ASM_MESON_TAC[PERMUTES_IN_IMAGE; IN_NUMSEG]; ALL_TAC] THEN
 309   ASM_SIMP_TAC[IN_NUMSEG; LAMBDA_BETA] THEN STRIP_TAC THEN
 310   ASM_CASES_TAC `(p:num->num) k = j` THEN ASM_REWRITE_TAC[] THENL
 311    [REPEAT(EXISTS_TAC `&0`) THEN REAL_ARITH_TAC; ALL_TAC] THEN
 312   ASM_SIMP_TAC[MATRIX_SUB_COMPONENT; MATRIX_CMUL_COMPONENT; MAT_COMPONENT] THEN
 313   REWRITE_TAC[REAL_ARITH `a - x * d:real = a + (--d) * x`] THEN MESON_TAC[]);;
 314
 315 let DETERMINANT_AS_POLYFUN = prove
 316  (`!A:real^N^N.
 317         ?c. !x. det(A - x %% mat 1) =
 318                 sum(0..dimindex(:N)) (\i. c(i) * x pow i)`,
 319   GEN_TAC THEN REWRITE_TAC[det] THEN
 320   MATCH_MP_TAC POLYFUN_N_SUM THEN
 321   SIMP_TAC[FINITE_PERMUTATIONS; FINITE_NUMSEG; FORALL_IN_GSPEC] THEN
 322   X_GEN_TAC `p:num->num` THEN DISCH_TAC THEN
 323   MATCH_MP_TAC POLYFUN_N_CMUL THEN MATCH_MP_TAC POLYFUN_N_PRODUCT THEN
 324   SIMP_TAC[FINITE_NUMSEG; CARD_NUMSEG_1; LE_REFL; IN_NUMSEG] THEN
 325   X_GEN_TAC `k:num` THEN STRIP_TAC THEN
 326   SUBGOAL_THEN `(p:num->num) k IN 1..dimindex(:N)` MP_TAC THENL
 327    [ASM_MESON_TAC[PERMUTES_IN_IMAGE; IN_NUMSEG]; ALL_TAC] THEN
 328   ASM_SIMP_TAC[IN_NUMSEG; LAMBDA_BETA] THEN STRIP_TAC THEN
 329   ASM_SIMP_TAC[MATRIX_SUB_COMPONENT; MATRIX_CMUL_COMPONENT; MAT_COMPONENT] THEN
 330   REWRITE_TAC[REAL_ARITH `a - x * d:real = a + (--d) * x`] THEN MESON_TAC[]);;
 331
 332 (* ------------------------------------------------------------------------- *)
 333 (* Hence define characteristic polynomial coefficients.                      *)
 334 (* ------------------------------------------------------------------------- *)
 335
 336 let char_poly = new_specification ["char_poly"]
 337   (REWRITE_RULE[SKOLEM_THM] DETERMINANT_AS_POLYFUN);;
 338
 339 (* ------------------------------------------------------------------------- *)
 340 (* Now the Cayley-Hamilton proof.                                            *)
 341 (* ------------------------------------------------------------------------- *)
 342
 343 let COFACTOR_AS_MATRIC_POLYNOMIAL = prove
 344  (`!A:real^N^N. ?C.
 345       !x. cofactor(A - x %% mat 1) =
 346           msum(0..dimindex(:N)-1) (\i. x pow i %% C i)`,
 347   GEN_TAC THEN SIMP_TAC[CART_EQ; MSUM_COMPONENT; FINITE_NUMSEG] THEN
 348   MP_TAC(ISPEC `A:real^N^N` COFACTOR_ENTRY_AS_POLYFUN) THEN
 349   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 350   REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[LAMBDA_SKOLEM] THEN
 351   DISCH_THEN(X_CHOOSE_THEN `c:(num->real)^N^N` ASSUME_TAC) THEN
 352   EXISTS_TAC `(\i. lambda j k. ((c:(num->real)^N^N)$j$k) i):num->real^N^N` THEN
 353   MAP_EVERY X_GEN_TAC [`x:real`; `i:num`] THEN STRIP_TAC THEN
 354   X_GEN_TAC `j:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
 355   MATCH_MP_TAC SUM_EQ_NUMSEG THEN REPEAT STRIP_TAC THEN
 356   ASM_SIMP_TAC[MATRIX_CMUL_COMPONENT; LAMBDA_BETA] THEN REAL_ARITH_TAC);;
 357
 358 let MATRIC_POWER_DIFFERENCE = prove
 359  (`!A:real^N^N x n.
 360         A mpow (SUC n) - x pow (SUC n) %% mat 1 =
 361         msum (0..n) (\i. x pow i %% A mpow (n - i)) ** (A - x %% mat 1)`,
 362   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL
 363    [REWRITE_TAC[MSUM_CLAUSES_NUMSEG; real_pow; SUB_0; mpow] THEN
 364     REWRITE_TAC[MATRIX_MUL_RID; MATRIX_CMUL_LID; MATRIX_MUL_LID] THEN
 365     REWRITE_TAC[REAL_MUL_RID];
 366     MATCH_MP_TAC EQ_TRANS THEN
 367     EXISTS_TAC
 368      `(A mpow SUC n - x pow SUC n %% mat 1) ** A +
 369       (x pow (SUC n) %% mat 1 :real^N^N) ** (A - x %% mat 1:real^N^N)` THEN
 370     CONJ_TAC THENL
 371      [GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MPOW_SUC] THEN
 372       REWRITE_TAC[MATRIX_SUB_RDISTRIB; MATRIX_SUB_LDISTRIB] THEN
 373       REWRITE_TAC[MATRIX_SUB; MATRIX_MUL_LMUL; MATRIX_MUL_LID] THEN
 374       REWRITE_TAC[GSYM MATRIX_ADD_ASSOC] THEN AP_TERM_TAC THEN
 375       REWRITE_TAC[MATRIX_ADD_ASSOC; MATRIX_ADD_LNEG; MATRIX_ADD_LID] THEN
 376       REWRITE_TAC[real_pow; MATRIX_CMUL_ASSOC] THEN REWRITE_TAC[REAL_MUL_AC];
 377
 378       ASM_REWRITE_TAC[MSUM_CLAUSES_NUMSEG; LE_0] THEN
 379       REWRITE_TAC[SUB_REFL; mpow; MATRIX_ADD_RDISTRIB] THEN
 380       AP_THM_TAC THEN AP_TERM_TAC THEN
 381       SIMP_TAC[GSYM MSUM_MATRIX_RMUL; FINITE_NUMSEG] THEN
 382       MATCH_MP_TAC MSUM_EQ THEN REWRITE_TAC[FINITE_NUMSEG] THEN
 383       X_GEN_TAC `i:num` THEN REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN
 384       ASM_SIMP_TAC[MATRIX_MUL_LMUL] THEN AP_TERM_TAC THEN
 385       ASM_SIMP_TAC[ARITH_RULE `i <= n ==> SUC n - i = SUC(n - i)`] THEN
 386       REWRITE_TAC[MPOW_SUC; GSYM MATRIX_MUL_ASSOC] THEN AP_TERM_TAC THEN
 387       REWRITE_TAC[MATRIX_SUB_LDISTRIB; MATRIX_SUB_RDISTRIB] THEN
 388       REWRITE_TAC[MATRIX_MUL_RMUL; MATRIX_MUL_LMUL] THEN
 389       REWRITE_TAC[MATRIX_MUL_LID; MATRIX_MUL_RID]]]);;
 390
 391 let MATRIC_CHARPOLY_DIFFERENCE = prove
 392  (`!A:real^N^N. ?B.
 393       !x. msum(0..dimindex(:N)) (\i. char_poly A i %% A mpow i) -
 394           sum(0..dimindex(:N)) (\i. char_poly A i * x pow i) %% mat 1 =
 395           msum(0..(dimindex(:N)-1)) (\i. x pow i %% B i) ** (A - x %% mat 1)`,
 396   GEN_TAC THEN SPEC_TAC(`dimindex(:N)`,`n:num`) THEN
 397   SPEC_TAC(`char_poly(A:real^N^N)`,`c:num->real`) THEN
 398   GEN_TAC THEN INDUCT_TAC THEN
 399   SIMP_TAC[MSUM_CLAUSES_NUMSEG; SUM_CLAUSES_NUMSEG; LE_0] THENL
 400    [EXISTS_TAC `(\i. mat 0):num->real^N^N` THEN
 401     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[MSUM_CLAUSES_NUMSEG] THEN
 402     REWRITE_TAC[real_pow; MATRIX_MUL_LMUL; MATRIX_MUL_LZERO; mpow;
 403                 REAL_MUL_RID; MATRIX_CMUL_RZERO; MATRIX_SUB_REFL];
 404     FIRST_X_ASSUM(X_CHOOSE_TAC `B:num->real^N^N`) THEN
 405     REWRITE_TAC[MATRIX_SUB; MATRIX_NEG_ADD; MATRIX_CMUL_ADD_RDISTRIB] THEN
 406     ONCE_REWRITE_TAC[AC MATRIX_ADD_AC
 407      `(A + B) + (C + D):real^N^N = (A + C) + (B + D)`] THEN
 408     ASM_REWRITE_TAC[GSYM MATRIX_SUB] THEN
 409     REWRITE_TAC[GSYM MATRIX_CMUL_ASSOC; GSYM MATRIX_CMUL_SUB_LDISTRIB] THEN
 410     REWRITE_TAC[MATRIC_POWER_DIFFERENCE; SUC_SUB1] THEN
 411     EXISTS_TAC `(\i. (if i <= n - 1 then B i else mat 0) +
 412                      c(SUC n) %% A mpow (n - i)):num->real^N^N` THEN
 413     X_GEN_TAC `x:real` THEN REWRITE_TAC[MATRIX_CMUL_ADD_LDISTRIB] THEN
 414     SIMP_TAC[MSUM_ADD; FINITE_NUMSEG; MATRIX_ADD_RDISTRIB] THEN
 415     REWRITE_TAC[GSYM MATRIX_MUL_LMUL] THEN
 416     BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THENL
 417      [REWRITE_TAC[COND_RAND; COND_RATOR; MATRIX_CMUL_RZERO] THEN
 418       REWRITE_TAC[GSYM MSUM_RESTRICT_SET; IN_NUMSEG] THEN
 419       REWRITE_TAC[numseg; ARITH_RULE
 420        `(0 <= i /\ i <= n) /\ i <= n - 1 <=> 0 <= i /\ i <= n - 1`];
 421       SIMP_TAC[GSYM MSUM_CMUL; FINITE_NUMSEG; MATRIX_CMUL_ASSOC] THEN
 422       REWRITE_TAC[REAL_MUL_SYM]]]);;
 423
 424 let CAYLEY_HAMILTON = prove
 425  (`!A:real^N^N. msum(0..dimindex(:N)) (\i. char_poly A i %% A mpow i) = mat 0`,
 426   GEN_TAC THEN MATCH_MP_TAC MATRIC_POLY_LEMMA THEN MATCH_MP_TAC(MESON[]
 427    `!g. (!x. g x = k) /\ (?a b c. !x. f a b c x = g x)
 428         ==> ?a b c. !x. f a b c x = k`) THEN
 429   EXISTS_TAC
 430    `\x. (msum(0..dimindex(:N)) (\i. char_poly A i %% (A:real^N^N) mpow i) -
 431          sum(0..dimindex(:N)) (\i. char_poly A i * x pow i) %% mat 1) +
 432         sum(0..dimindex(:N)) (\i. char_poly A i * x pow i) %% mat 1` THEN
 433   REWRITE_TAC[] THEN CONJ_TAC THENL
 434    [REWRITE_TAC[MATRIX_SUB; GSYM MATRIX_ADD_ASSOC; MATRIX_ADD_LNEG] THEN
 435     REWRITE_TAC[MATRIX_ADD_RID];
 436     X_CHOOSE_THEN `B:num->real^N^N` (fun th -> ONCE_REWRITE_TAC[th])
 437      (ISPEC `A:real^N^N` MATRIC_CHARPOLY_DIFFERENCE) THEN
 438     REWRITE_TAC[GSYM char_poly; GSYM MATRIX_MUL_LEFT_COFACTOR] THEN
 439     REWRITE_TAC[GSYM MATRIX_ADD_RDISTRIB] THEN
 440     REWRITE_TAC[GSYM COFACTOR_TRANSP; TRANSP_MATRIX_SUB] THEN
 441     REWRITE_TAC[TRANSP_MATRIX_CMUL; TRANSP_MAT] THEN
 442     X_CHOOSE_THEN `C:num->real^N^N` (fun th -> ONCE_REWRITE_TAC[th])
 443      (ISPEC `transp A:real^N^N` COFACTOR_AS_MATRIC_POLYNOMIAL) THEN
 444     MAP_EVERY EXISTS_TAC
 445      [`A:real^N^N`; `(\i. B i + C i):num->real^N^N`; `dimindex(:N)-1`] THEN
 446     SIMP_TAC[GSYM MSUM_ADD; FINITE_NUMSEG; MATRIX_CMUL_ADD_LDISTRIB]]);;