1 (* ========================================================================= *)
2 (* The Cayley-Hamilton theorem (for real matrices). *)
3 (* ========================================================================= *)
5 needs "Multivariate/complexes.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* Powers of a square matrix (mpow) and sums of matrices (msum). *)
9 (* ------------------------------------------------------------------------- *)
11 parse_as_infix("mpow",(24,"left"));;
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)`;;
17 let msum = new_definition
18 `msum = iterate (matrix_add)`;;
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]);;
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]);;
31 let MSUM_CLAUSES = prove
32 (`(!(f:A->real^N^M). msum {} f = mat 0) /\
33 (!x (f:A->real^N^M) 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]);;
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]);;
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]);;
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]);;
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]);;
65 FINITE s ==> msum s (\i. --(f(i))) = --(msum s f)`,
66 ONCE_REWRITE_TAC[MATRIX_NEG_MINUS1] THEN
67 REWRITE_TAC[MSUM_CMUL]);;
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]);;
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
79 let MSUM_SUPPORT = prove
80 (`!f s. msum (support (+) f s) f = msum s f`,
81 SIMP_TAC[msum; iterate; SUPPORT_SUPPORT]);;
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]);;
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)`;
95 REPEAT GEN_TAC THEN MATCH_MP_TAC MSUM_EQ THEN SIMP_TAC[IN_ELIM_THM]);;
98 (`!f x. msum {x} f = f(x)`,
99 SIMP_TAC[MSUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; MATRIX_ADD_RID]);;
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]);;
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]);;
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) /\
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]);;
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)
129 REWRITE_TAC[MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_MATRIX_ADD;
130 NEUTRAL_MATRIX_ADD; msum]);;
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]);;
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]);;
144 (`!A:real^N^N n. A mpow (SUC n) = A mpow n ** A`,
145 REWRITE_TAC[ADD1; MPOW_ADD; MPOW_1]);;
147 (* ------------------------------------------------------------------------- *)
148 (* The main lemma underlying the proof. *)
149 (* ------------------------------------------------------------------------- *)
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
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[]);;
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)
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
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))) =
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]]]);;
218 (* ------------------------------------------------------------------------- *)
219 (* Show that cofactor and determinant are n-1 and n degree polynomials. *)
220 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
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]);;
246 let POLYFUN_N_SUM = prove
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[]);;
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);;
286 let COFACTOR_ENTRY_AS_POLYFUN = prove
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)`
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[]);;
315 let DETERMINANT_AS_POLYFUN = prove
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[]);;
332 (* ------------------------------------------------------------------------- *)
333 (* Hence define characteristic polynomial coefficients. *)
334 (* ------------------------------------------------------------------------- *)
336 let char_poly = new_specification ["char_poly"]
337 (REWRITE_RULE[SKOLEM_THM] DETERMINANT_AS_POLYFUN);;
339 (* ------------------------------------------------------------------------- *)
340 (* Now the Cayley-Hamilton proof. *)
341 (* ------------------------------------------------------------------------- *)
343 let COFACTOR_AS_MATRIC_POLYNOMIAL = prove
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);;
358 let MATRIC_POWER_DIFFERENCE = prove
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
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
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];
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]]]);;
391 let MATRIC_CHARPOLY_DIFFERENCE = prove
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]]]);;
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
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
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]]);;