(* ========================================================================= *)
(* Determinant and trace of a square matrix. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/vectors.ml";;
needs "Library/permutations.ml";;
needs "Library/floor.ml";;
needs "Library/products.ml";;
prioritize_real();;
(* ------------------------------------------------------------------------- *)
(* Trace of a matrix (this is relatively easy). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Definition of determinant. *)
(* ------------------------------------------------------------------------- *)
let det = new_definition
`det(A:real^N^N) =
sum { p | p permutes 1..dimindex(:N) }
(\p. sign(p) * product (1..dimindex(:N)) (\i. A$i$(p i)))`;;let IN_DIMINDEX_SWAP = prove
(`!m n j. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N)
==> 1 <= swap(m,n) j /\ swap(m,n) j <= dimindex(:N)`,
REWRITE_TAC[swap] THEN ARITH_TAC);;
let LAMBDA_BETA_PERM = prove
(`!p i. p permutes 1..dimindex(:N) /\ 1 <= i /\ i <= dimindex(:N)
==> ((lambda) g :A^N) $ p(i) = g(p i)`,
let DET_CMUL = prove
(`!A:real^N^N c. det(c %% A) = c pow dimindex(:N) * det A`,
let DET_NEG = prove
(`!A:real^N^N. det(--A) = --(&1) pow dimindex(:N) * det A`,
let DET_LOWERTRIANGULAR = prove
(`!A:real^N^N.
(!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ i < j ==> A$i$j = &0)
==> det(A) = product(1..dimindex(:N)) (\i. A$i$i)`,
let DET_UPPERTRIANGULAR = prove
(`!A:real^N^N.
(!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ j < i ==> A$i$j = &0)
==> det(A) = product(1..dimindex(:N)) (\i. A$i$i)`,
let DET_DIAGONAL = prove
(`!A:real^N^N.
(!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j) ==> A$i$j = &0)
==> det(A) = product(1..dimindex(:N)) (\i. A$i$i)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
DET_LOWERTRIANGULAR THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
LT_REFL]);;
let DET_PERMUTE_COLUMNS = prove
(`!A:real^N^N p.
p permutes 1..dimindex(:N)
==> det((lambda i j. A$i$p(j)):real^N^N) = sign(p) * det(A)`,
let DET_IDENTICAL_ROWS = prove
(`!A:real^N^N i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j) /\
row i A = row j A
==> det A = &0`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`A:real^N^N`; `swap(i:num,j:num)`]
DET_PERMUTE_ROWS) THEN
ASM_SIMP_TAC[
PERMUTES_SWAP;
IN_NUMSEG;
SIGN_SWAP] THEN
MATCH_MP_TAC(REAL_ARITH `a = b ==> b = -- &1 * a ==> a = &0`) THEN
AP_TERM_TAC THEN FIRST_X_ASSUM(MP_TAC o SYM) THEN
SIMP_TAC[row;
CART_EQ;
LAMBDA_BETA] THEN
REWRITE_TAC[swap] THEN ASM_MESON_TAC[]);;
let DET_IDENTICAL_COLUMNS = prove
(`!A:real^N^N i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j) /\
column i A = column j A
==> det A = &0`,
let DET_ZERO_ROW = prove
(`!A:real^N^N i.
1 <= i /\ i <= dimindex(:N) /\ row i A = vec 0 ==> det A = &0`,
let DET_ROW_ADD = prove
(`!a b c k.
1 <= k /\ k <= dimindex(:N)
==> det((lambda i. if i = k then a + b else c i):real^N^N) =
det((lambda i. if i = k then a else c i):real^N^N) +
det((lambda i. if i = k then b else c i):real^N^N)`,
let DET_ROW_MUL = prove
(`!a b c k.
1 <= k /\ k <= dimindex(:N)
==> det((lambda i. if i = k then c % a else b i):real^N^N) =
c * det((lambda i. if i = k then a else b i):real^N^N)`,
let DET_ROW_OPERATION = prove
(`!A:real^N^N i.
1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j)
==> det(lambda k. if k = i then row i A + c % row j A else row k A) =
det A`,
let DET_ROW_SPAN = prove
(`!A:real^N^N i x.
1 <= i /\ i <= dimindex(:N) /\
x
IN span {row j A | 1 <= j /\ j <= dimindex(:N) /\ ~(j = i)}
==> det(lambda k. if k = i then row i A + x else row k A) =
det A`,
GEN_TAC THEN GEN_TAC THEN
REWRITE_TAC[
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN REPEAT DISCH_TAC THEN
MATCH_MP_TAC
SPAN_INDUCT_ALT THEN CONJ_TAC THENL
[AP_TERM_TAC THEN SIMP_TAC[
CART_EQ;
LAMBDA_BETA;
VECTOR_ADD_RID] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[row;
LAMBDA_BETA];
ALL_TAC] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[
IN_ELIM_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `j:num`) (SUBST_ALL_TAC o SYM)) THEN
ONCE_REWRITE_TAC[VECTOR_ARITH
`a + c % x + y:real^N = (a + y) + c % x`] THEN
ABBREV_TAC `z = row i (A:real^N^N) + y` THEN
ASM_SIMP_TAC[
DET_ROW_MUL;
DET_ROW_ADD] THEN
MATCH_MP_TAC(REAL_RING `d = &0 ==> a + c * d = a`) THEN
MATCH_MP_TAC
DET_IDENTICAL_ROWS THEN
MAP_EVERY EXISTS_TAC [`i:num`; `j:num`] THEN
ASM_SIMP_TAC[row;
LAMBDA_BETA;
CART_EQ]);;
let DET_LINEAR_ROW_VSUM = prove
(`!a c s k.
FINITE s /\ 1 <= k /\ k <= dimindex(:N)
==> det((lambda i. if i = k then vsum s a else c i):real^N^N) =
sum s
(\j. det((lambda i. if i = k then a(j) else c i):real^N^N))`,
let BOUNDED_FUNCTIONS_BIJECTIONS_1 = prove
(`!p. p
IN {(y,g) | y
IN s /\
g
IN {f | (!i. 1 <= i /\ i <= k ==> f i
IN s) /\
(!i. ~(1 <= i /\ i <= k) ==> f i = i)}}
==> (\(y,g) i. if i = SUC k then y else g(i)) p
IN
{f | (!i. 1 <= i /\ i <= SUC k ==> f i
IN s) /\
(!i. ~(1 <= i /\ i <= SUC k) ==> f i = i)} /\
(\h. h(SUC k),(\i. if i = SUC k then i else h(i)))
((\(y,g) i. if i = SUC k then y else g(i)) p) = p`,
REWRITE_TAC[
FORALL_PAIR_THM;
IN_ELIM_PAIR_THM] THEN
CONV_TAC(REDEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[
IN_ELIM_THM] THEN
MAP_EVERY X_GEN_TAC [`y:num`; `h:num->num`] THEN REPEAT STRIP_TAC THENL
[ASM_MESON_TAC[
LE];
ASM_MESON_TAC[
LE; ARITH_RULE `~(1 <= i /\ i <= SUC k) ==> ~(i = SUC k)`];
REWRITE_TAC[
PAIR_EQ;
FUN_EQ_THM] THEN
ASM_MESON_TAC[ARITH_RULE `~(SUC k <= k)`]]);;
let BOUNDED_FUNCTIONS_BIJECTIONS_2 = prove
(`!h. h
IN {f | (!i. 1 <= i /\ i <= SUC k ==> f i
IN s) /\
(!i. ~(1 <= i /\ i <= SUC k) ==> f i = i)}
==> (\h. h(SUC k),(\i. if i = SUC k then i else h(i))) h
IN
{(y,g) | y
IN s /\
g
IN {f | (!i. 1 <= i /\ i <= k ==> f i
IN s) /\
(!i. ~(1 <= i /\ i <= k) ==> f i = i)}} /\
(\(y,g) i. if i = SUC k then y else g(i))
((\h. h(SUC k),(\i. if i = SUC k then i else h(i))) h) = h`,
REWRITE_TAC[
IN_ELIM_PAIR_THM] THEN
CONV_TAC(REDEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[
IN_ELIM_THM] THEN
X_GEN_TAC `h:num->num` THEN REPEAT STRIP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN ARITH_TAC;
ASM_MESON_TAC[ARITH_RULE `i <= k ==> i <= SUC k /\ ~(i = SUC k)`];
ASM_MESON_TAC[ARITH_RULE `i <= SUC k /\ ~(i = SUC k) ==> i <= k`];
REWRITE_TAC[
FUN_EQ_THM] THEN ASM_MESON_TAC[
LE_REFL]]);;
let FINITE_BOUNDED_FUNCTIONS = prove
(`!s k.
FINITE s
==>
FINITE {f | (!i. 1 <= i /\ i <= k ==> f(i)
IN s) /\
(!i. ~(1 <= i /\ i <= k) ==> f(i) = i)}`,
REWRITE_TAC[
RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
INDUCT_TAC THENL
[REWRITE_TAC[ARITH_RULE `~(1 <= i /\ i <= 0)`] THEN
SIMP_TAC[GSYM
FUN_EQ_THM; SET_RULE `{x | x = y} = {y}`;
FINITE_RULES];
ALL_TAC] THEN
UNDISCH_TAC `
FINITE(s:num->bool)` THEN POP_ASSUM MP_TAC THEN
REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
DISCH_THEN(MP_TAC o MATCH_MP
FINITE_PRODUCT) THEN
DISCH_THEN(MP_TAC o ISPEC `\(y:num,g) i. if i = SUC k then y else g(i)` o
MATCH_MP
FINITE_IMAGE) THEN
MATCH_MP_TAC(TAUT `a = b ==> a ==> b`) THEN AP_TERM_TAC THEN
REWRITE_TAC[
EXTENSION;
IN_IMAGE] THEN
X_GEN_TAC `h:num->num` THEN EQ_TAC THENL
[STRIP_TAC THEN ASM_SIMP_TAC[
BOUNDED_FUNCTIONS_BIJECTIONS_1]; ALL_TAC] THEN
DISCH_TAC THEN EXISTS_TAC
`(\h. h(SUC k),(\i. if i = SUC k then i else h(i))) h` THEN
PURE_ONCE_REWRITE_TAC[
CONJ_SYM] THEN CONV_TAC (RAND_CONV SYM_CONV) THEN
MATCH_MP_TAC
BOUNDED_FUNCTIONS_BIJECTIONS_2 THEN ASM_REWRITE_TAC[]);;
let DET_LINEAR_ROWS_VSUM_LEMMA = prove
(`!s k a c.
FINITE s /\ k <= dimindex(:N)
==> det((lambda i. if i <= k then vsum s (a i) else c i):real^N^N) =
sum {f | (!i. 1 <= i /\ i <= k ==> f(i)
IN s) /\
!i. ~(1 <= i /\ i <= k) ==> f(i) = i}
(\f. det((lambda i. if i <= k then a i (f i) else c i)
:real^N^N))`,
let lemma = prove
(`(lambda i. if i <= 0 then x(i) else y(i)) = (lambda i. y i)`,
SIMP_TAC[CART_EQ; ARITH; LAMBDA_BETA; ARITH_RULE
`1 <= k ==> ~(k <= 0)`]) in
ONCE_REWRITE_TAC[IMP_CONJ] THEN
REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
INDUCT_TAC THENL
[REWRITE_TAC[lemma; LE_0] THEN GEN_TAC THEN
REWRITE_TAC[ARITH_RULE `~(1 <= i /\ i <= 0)`] THEN
REWRITE_TAC[GSYM FUN_EQ_THM; SET_RULE `{x | x = y} = {y}`] THEN
REWRITE_TAC[SUM_SING];
ALL_TAC] THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
ASM_SIMP_TAC[ARITH_RULE `SUC k <= n ==> k <= n`] THEN REPEAT STRIP_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LE] THEN
REWRITE_TAC[TAUT
`(if a \/ b then c else d) = (if a then c else if b then c else d)`] THEN
ASM_SIMP_TAC[DET_LINEAR_ROW_VSUM; ARITH_RULE `1 <= SUC k`] THEN
ONCE_REWRITE_TAC[TAUT
`(if a then b else if c then d else e) =
(if c then (if a then b else d) else (if a then b else e))`] THEN
ASM_SIMP_TAC[ARITH_RULE `i <= k ==> ~(i = SUC k)`] THEN
ASM_SIMP_TAC[SUM_SUM_PRODUCT; FINITE_BOUNDED_FUNCTIONS] THEN
MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
EXISTS_TAC `\(y:num,g) i. if i = SUC k then y else g(i)` THEN
EXISTS_TAC `\h. h(SUC k),(\i. if i = SUC k then i else h(i))` THEN
CONJ_TAC THENL [ACCEPT_TAC BOUNDED_FUNCTIONS_BIJECTIONS_2; ALL_TAC] THEN
X_GEN_TAC `p:num#(num->num)` THEN
DISCH_THEN(STRIP_ASSUME_TAC o MATCH_MP BOUNDED_FUNCTIONS_BIJECTIONS_1) THEN
ASM_REWRITE_TAC[] THEN
SPEC_TAC(`p:num#(num->num)`,`q:num#(num->num)`) THEN
REWRITE_TAC[FORALL_PAIR_THM] THEN
CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
MAP_EVERY X_GEN_TAC [`y:num`; `g:num->num`] THEN AP_TERM_TAC THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA] THEN
REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
ASM_MESON_TAC[LE; ARITH_RULE `~(SUC k <= k)`]);;
let DET_LINEAR_ROWS_VSUM = prove
(`!s a.
FINITE s
==> det((lambda i. vsum s (a i)):real^N^N) =
sum {f | (!i. 1 <= i /\ i <= dimindex(:N) ==> f(i)
IN s) /\
!i. ~(1 <= i /\ i <= dimindex(:N)) ==> f(i) = i}
(\f. det((lambda i. a i (f i)):real^N^N))`,
let DET_ROWS_MUL = prove
(`!a c. det((lambda i. c(i) % a(i)):real^N^N) =
product(1..dimindex(:N)) (\i. c(i)) *
det((lambda i. a(i)):real^N^N)`,
let DET_MATRIX_EQ_0 = prove
(`!f:real^N->real^N.
linear f
==> (det(matrix f) = &0 <=>
~(?g. linear g /\ f o g = I /\ g o f = I))`,
let CRAMER_LEMMA_TRANSP = prove
(`!A:real^N^N x:real^N.
1 <= k /\ k <= dimindex(:N)
==> det((lambda i. if i = k
then vsum(1..dimindex(:N)) (\i. x$i % row i A)
else row i A):real^N^N) =
x$k * det A`,
let CRAMER_LEMMA = prove
(`!A:real^N^N x:real^N.
1 <= k /\ k <= dimindex(:N)
==> det((lambda i j. if j = k then (A**x)$i else A$i$j):real^N^N) =
x$k * det(A)`,
let CRAMER = prove
(`!A:real^N^N x b.
~(det(A) = &0)
==> (A ** x = b <=>
x = lambda k.
det((lambda i j. if j = k then b$i else A$i$j):real^N^N) /
det(A))`,
let CRAMER_MATRIX_LEFT = prove
(`!A:real^N^N X:real^N^N B:real^N^N.
~(det A = &0)
==> (X ** A = B <=>
X = lambda k l.
det((lambda i j. if j = l then B$k$i else A$j$i):real^N^N) /
det A)`,
let CRAMER_MATRIX_RIGHT = prove
(`!A:real^N^N X:real^N^N B:real^N^N.
~(det A = &0)
==> (A ** X = B <=>
X = lambda k l.
det((lambda i j. if j = k then B$i$l else A$i$j):real^N^N) /
det A)`,
let CRAMER_MATRIX_RIGHT_INVERSE = prove
(`!A:real^N^N A':real^N^N.
A ** A' = mat 1 <=>
~(det A = &0) /\
A' = lambda k l.
det((lambda i j. if j = k then if i = l then &1 else &0
else A$i$j):real^N^N) /
det A`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `det(A:real^N^N) = &0` THENL
[ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o AP_TERM `det:real^N^N->real`) THEN
ASM_REWRITE_TAC[
DET_MUL;
DET_I] THEN REAL_ARITH_TAC;
ASM_SIMP_TAC[
CRAMER_MATRIX_RIGHT] THEN AP_TERM_TAC THEN
SIMP_TAC[
CART_EQ;
LAMBDA_BETA] THEN
REPEAT(GEN_TAC THEN STRIP_TAC) THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
LAMBDA_BETA; mat]]);;
let CRAMER_MATRIX_LEFT_INVERSE = prove
(`!A:real^N^N A':real^N^N.
A' ** A = mat 1 <=>
~(det A = &0) /\
A' = lambda k l.
det((lambda i j. if j = l then if i = k then &1 else &0
else A$j$i):real^N^N) /
det A`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `det(A:real^N^N) = &0` THENL
[ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o AP_TERM `det:real^N^N->real`) THEN
ASM_REWRITE_TAC[
DET_MUL;
DET_I] THEN REAL_ARITH_TAC;
ASM_SIMP_TAC[
CRAMER_MATRIX_LEFT] THEN AP_TERM_TAC THEN
SIMP_TAC[
CART_EQ;
LAMBDA_BETA] THEN
REPEAT(GEN_TAC THEN STRIP_TAC) THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
LAMBDA_BETA; mat] THEN MESON_TAC[]]);;
let cofactor = new_definition
`(cofactor:real^N^N->real^N^N) A =
lambda i j. det((lambda k l. if k = i /\ l = j then &1
else if k = i \/ l = j then &0
else A$k$l):real^N^N)`;;let COFACTOR_COLUMN = prove
(`!A:real^N^N.
cofactor A =
lambda i j. det((lambda k l. if l = j then if k = i then &1 else &0
else A$k$l):real^N^N)`,
let COFACTOR_ROW = prove
(`!A:real^N^N.
cofactor A =
lambda i j. det((lambda k l. if k = i then if l = j then &1 else &0
else A$k$l):real^N^N)`,
let COFACTOR_0 = prove
(`cofactor(mat 0:real^N^N) = if dimindex(:N) = 1 then mat 1 else mat 0`,
let DET_2 = prove
(`!A:real^2^2. det A = A$1$1 * A$2$2 - A$1$2 * A$2$1`,
let DET_3 = prove
(`!A:real^3^3.
det(A) = A$1$1 * A$2$2 * A$3$3 +
A$1$2 * A$2$3 * A$3$1 +
A$1$3 * A$2$1 * A$3$2 -
A$1$1 * A$2$3 * A$3$2 -
A$1$2 * A$2$1 * A$3$3 -
A$1$3 * A$2$2 * A$3$1`,
let DET_4 = prove
(`!A:real^4^4.
det(A) = A$1$1 * A$2$2 * A$3$3 * A$4$4 +
A$1$1 * A$2$3 * A$3$4 * A$4$2 +
A$1$1 * A$2$4 * A$3$2 * A$4$3 +
A$1$2 * A$2$1 * A$3$4 * A$4$3 +
A$1$2 * A$2$3 * A$3$1 * A$4$4 +
A$1$2 * A$2$4 * A$3$3 * A$4$1 +
A$1$3 * A$2$1 * A$3$2 * A$4$4 +
A$1$3 * A$2$2 * A$3$4 * A$4$1 +
A$1$3 * A$2$4 * A$3$1 * A$4$2 +
A$1$4 * A$2$1 * A$3$3 * A$4$2 +
A$1$4 * A$2$2 * A$3$1 * A$4$3 +
A$1$4 * A$2$3 * A$3$2 * A$4$1 -
A$1$1 * A$2$2 * A$3$4 * A$4$3 -
A$1$1 * A$2$3 * A$3$2 * A$4$4 -
A$1$1 * A$2$4 * A$3$3 * A$4$2 -
A$1$2 * A$2$1 * A$3$3 * A$4$4 -
A$1$2 * A$2$3 * A$3$4 * A$4$1 -
A$1$2 * A$2$4 * A$3$1 * A$4$3 -
A$1$3 * A$2$1 * A$3$4 * A$4$2 -
A$1$3 * A$2$2 * A$3$1 * A$4$4 -
A$1$3 * A$2$4 * A$3$2 * A$4$1 -
A$1$4 * A$2$1 * A$3$2 * A$4$3 -
A$1$4 * A$2$2 * A$3$3 * A$4$1 -
A$1$4 * A$2$3 * A$3$1 * A$4$2`,
let GRASSMANN_PLUCKER_2 = prove
(`!x1 x2 y1 y2:real^2.
det(vector[x1;x2]) * det(vector[y1;y2]) =
det(vector[y1;x2]) * det(vector[x1;y2]) +
det(vector[y2;x2]) * det(vector[y1;x1])`,
let GRASSMANN_PLUCKER_3 = prove
(`!x1 x2 x3 y1 y2 y3:real^3.
det(vector[x1;x2;x3]) * det(vector[y1;y2;y3]) =
det(vector[y1;x2;x3]) * det(vector[x1;y2;y3]) +
det(vector[y2;x2;x3]) * det(vector[y1;x1;y3]) +
det(vector[y3;x2;x3]) * det(vector[y1;y2;x1])`,
let GRASSMANN_PLUCKER_4 = prove
(`!x1 x2 x3 x4:real^4 y1 y2 y3 y4:real^4.
det(vector[x1;x2;x3;x4]) * det(vector[y1;y2;y3;y4]) =
det(vector[y1;x2;x3;x4]) * det(vector[x1;y2;y3;y4]) +
det(vector[y2;x2;x3;x4]) * det(vector[y1;x1;y3;y4]) +
det(vector[y3;x2;x3;x4]) * det(vector[y1;y2;x1;y4]) +
det(vector[y4;x2;x3;x4]) * det(vector[y1;y2;y3;x1])`,
let INTEGER_DET = prove
(`!M:real^N^N.
(!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N)
==> integer(M$i$j))
==> integer(det M)`,
let ORTHOGONAL_TRANSFORMATION_ORTHOGONAL_EIGENVECTORS = prove
(`!f:real^N->real^N v w a b.
orthogonal_transformation f /\ f v = a % v /\ f w = b % w /\ ~(a = b)
==> orthogonal v w`,
REWRITE_TAC[
orthogonal_transformation] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(fun th ->
MP_TAC(SPECL [`v:real^N`; `v:real^N`] th) THEN
MP_TAC(SPECL [`v:real^N`; `w:real^N`] th) THEN
MP_TAC(SPECL [`w:real^N`; `w:real^N`] th)) THEN
ASM_REWRITE_TAC[
DOT_LMUL;
DOT_RMUL; orthogonal] THEN
REWRITE_TAC[REAL_MUL_ASSOC; REAL_RING `x * y = y <=> x = &1 \/ y = &0`] THEN
REWRITE_TAC[
DOT_EQ_0] THEN
ASM_CASES_TAC `v:real^N = vec 0` THEN ASM_REWRITE_TAC[
DOT_LZERO] THEN
ASM_CASES_TAC `w:real^N = vec 0` THEN ASM_REWRITE_TAC[
DOT_RZERO] THEN
ASM_CASES_TAC `(v:real^N) dot w = &0` THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `~(a:real = b)` THEN CONV_TAC REAL_RING);;
let SCALING_LINEAR = prove
(`!f:real^M->real^N c.
(f(vec 0) = vec 0) /\ (!x y. dist(f x,f y) = c * dist(x,y))
==> linear(f)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!v w. ((f:real^M->real^N) v) dot (f w) = c pow 2 * (v dot w)`
ASSUME_TAC THENL
[FIRST_ASSUM(MP_TAC o GEN `v:real^M` o
SPECL [`v:real^M`; `vec 0 :real^M`]) THEN
REWRITE_TAC[dist] THEN ASM_REWRITE_TAC[
VECTOR_SUB_RZERO] THEN
DISCH_TAC THEN ASM_REWRITE_TAC[
DOT_NORM_NEG; GSYM dist] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[linear;
VECTOR_EQ] THEN
ASM_REWRITE_TAC[
DOT_LADD;
DOT_RADD;
DOT_LMUL;
DOT_RMUL] THEN
REAL_ARITH_TAC);;
let ISOMETRY_LINEAR = prove
(`!f:real^M->real^N.
(f(vec 0) = vec 0) /\ (!x y. dist(f x,f y) = dist(x,y))
==> linear(f)`,
let ISOMETRY_IMP_AFFINITY = prove
(`!f:real^M->real^N.
(!x y. dist(f x,f y) = dist(x,y))
==> ?h. linear h /\ !x. f(x) = f(vec 0) + h(x)`,
REPEAT STRIP_TAC THEN
EXISTS_TAC `\x. (f:real^M->real^N) x - f(vec 0)` THEN
REWRITE_TAC[VECTOR_ARITH `a + (x - a):real^N = x`] THEN
MATCH_MP_TAC
ISOMETRY_LINEAR THEN REWRITE_TAC[
VECTOR_SUB_REFL] THEN
ASM_REWRITE_TAC[NORM_ARITH `dist(x - a:real^N,y - a) = dist(x,y)`]);;
let FINITE_INDEX_NUMSEG_SPECIAL = prove
(`!s a:A.
FINITE s /\ a
IN s
==> ?f. (!i j. i
IN 1..CARD s /\ j
IN 1..CARD s /\ f i = f j
==> i = j) /\
s =
IMAGE f (1..CARD s) /\
f 1 = a`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
FINITE_INDEX_NUMSEG]) THEN
DISCH_THEN(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `?k. k
IN 1..CARD(s:A->bool) /\ (a:A) = f k`
STRIP_ASSUME_TAC THENL[ASM SET_TAC[]; ALL_TAC] THEN
EXISTS_TAC `(f:num->A) o swap(1,k)` THEN
SUBGOAL_THEN `1
IN 1..CARD(s:A->bool)` ASSUME_TAC THENL
[REWRITE_TAC[
IN_NUMSEG;
LE_REFL; ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
ASM_SIMP_TAC[
CARD_EQ_0;
ARITH_EQ] THEN ASM SET_TAC[];
ALL_TAC] THEN
ASM_REWRITE_TAC[
o_THM; swap] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
UNDISCH_THEN `s =
IMAGE (f:num->A) (1..CARD(s:A->bool))`
(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
REWRITE_TAC[
EXTENSION;
IN_IMAGE;
o_THM] THEN
X_GEN_TAC `b:A` THEN EQ_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `swap(1,k) i` THEN
REWRITE_TAC[swap] THEN ASM_MESON_TAC[swap]);;
let pth = prove
(`!a:real^N. a = a + vec 0 /\
{} =
IMAGE (\x. a + x) {} /\
{} =
IMAGE (
IMAGE (\x. a + x)) {} /\
(:real^N) =
IMAGE (\x. a + x) (:real^N) /\
(:real^N->bool) =
IMAGE (
IMAGE (\x. a + x)) (:real^N->bool) /\
[] =
MAP (\x. a + x) []`,
REWRITE_TAC[
IMAGE_CLAUSES;
VECTOR_ADD_RID;
MAP] THEN
REWRITE_TAC[SET_RULE `
UNIV =
IMAGE f
UNIV <=> !y. ?x. f x = y`] THEN
REWRITE_TAC[
SURJECTIVE_IMAGE] THEN
REWRITE_TAC[VECTOR_ARITH `a + y:real^N = x <=> y = x - a`;
EXISTS_REFL])
and qth =
prove
(`!a:real^N.
((!P. (!x. P x) <=> (!x. P (a + x))) /\
(!P. (?x. P x) <=> (?x. P (a + x))) /\
(!Q. (!s. Q s) <=> (!s. Q(
IMAGE (\x. a + x) s))) /\
(!Q. (?s. Q s) <=> (?s. Q(
IMAGE (\x. a + x) s))) /\
(!Q. (!s. Q s) <=> (!s. Q(
IMAGE (
IMAGE (\x. a + x)) s))) /\
(!Q. (?s. Q s) <=> (?s. Q(
IMAGE (
IMAGE (\x. a + x)) s))) /\
(!P. (!g:real^1->real^N. P g) <=> (!g. P ((\x. a + x) o g))) /\
(!P. (?g:real^1->real^N. P g) <=> (?g. P ((\x. a + x) o g))) /\
(!P. (!g:num->real^N. P g) <=> (!g. P ((\x. a + x) o g))) /\
(!P. (?g:num->real^N. P g) <=> (?g. P ((\x. a + x) o g))) /\
(!Q. (!l. Q l) <=> (!l. Q(
MAP (\x. a + x) l))) /\
(!Q. (?l. Q l) <=> (?l. Q(
MAP (\x. a + x) l)))) /\
((!P. {x | P x} =
IMAGE (\x. a + x) {x | P(a + x)}) /\
(!Q. {s | Q s} =
IMAGE (
IMAGE (\x. a + x)) {s | Q(
IMAGE (\x. a + x) s)}) /\
(!R. {l | R l} =
IMAGE (
MAP (\x. a + x)) {l | R(
MAP (\x. a + x) l)}))`,
GEN_TAC THEN MATCH_MP_TAC
QUANTIFY_SURJECTION_HIGHER_THM THEN
X_GEN_TAC `y:real^N` THEN EXISTS_TAC `y - a:real^N` THEN
VECTOR_ARITH_TAC) in
let GEOM_ORIGIN_CONV avoid tm =
let x,tm0 = dest_forall tm in
let th0 = ISPEC x pth in
let x' = genvar(type_of x) in
let ith = ISPEC x' qth in
let th1 = PARTIAL_EXPAND_QUANTS_CONV avoid (ASSUME(concl ith)) tm0 in
let th2 = CONV_RULE(RAND_CONV(SUBS_CONV(CONJUNCTS th0))) th1 in
let th3 = INST[x,x'] (PROVE_HYP ith th2) in
let ths = TRANSLATION_INVARIANTS x in
let thr = REFL x in
let th4 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV)
[
BETA_THM;ADD_ASSUM(concl thr) ths] th3 in
let th5 = MK_FORALL x (PROVE_HYP thr th4) in
GEN_REWRITE_RULE (RAND_CONV o TRY_CONV) [
FORALL_SIMP] th5
and GEOM_TRANSLATE_CONV avoid a tm =
let cth = CONJUNCT2(ISPEC a pth)
and vth = ISPEC a qth in
let th1 = PARTIAL_EXPAND_QUANTS_CONV avoid (ASSUME(concl vth)) tm in
let th2 = CONV_RULE(RAND_CONV(SUBS_CONV(CONJUNCTS cth))) th1 in
let th3 = PROVE_HYP vth th2 in
let ths = TRANSLATION_INVARIANTS a in
let thr = REFL a in
let th4 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV)
[
BETA_THM;ADD_ASSUM(concl thr) ths] th3 in
PROVE_HYP thr th4 in
GEOM_ORIGIN_CONV,GEOM_TRANSLATE_CONV;;
let pth = prove
(`!f.
orthogonal_transformation (f:real^N->real^N)
==> (vec 0 = f(vec 0) /\
{} =
IMAGE f {} /\
{} =
IMAGE (
IMAGE f) {} /\
(:real^N) =
IMAGE f (:real^N) /\
(:real^N->bool) =
IMAGE (
IMAGE f) (:real^N->bool) /\
[] =
MAP f []) /\
((!P. (!x. P x) <=> (!x. P (f x))) /\
(!P. (?x. P x) <=> (?x. P (f x))) /\
(!Q. (!s. Q s) <=> (!s. Q (
IMAGE f s))) /\
(!Q. (?s. Q s) <=> (?s. Q (
IMAGE f s))) /\
(!Q. (!s. Q s) <=> (!s. Q (
IMAGE (
IMAGE f) s))) /\
(!Q. (?s. Q s) <=> (?s. Q (
IMAGE (
IMAGE f) s))) /\
(!P. (!g:real^1->real^N. P g) <=> (!g. P (f o g))) /\
(!P. (?g:real^1->real^N. P g) <=> (?g. P (f o g))) /\
(!P. (!g:num->real^N. P g) <=> (!g. P (f o g))) /\
(!P. (?g:num->real^N. P g) <=> (?g. P (f o g))) /\
(!Q. (!l. Q l) <=> (!l. Q(
MAP f l))) /\
(!Q. (?l. Q l) <=> (?l. Q(
MAP f l)))) /\
((!P. {x | P x} =
IMAGE f {x | P(f x)}) /\
(!Q. {s | Q s} =
IMAGE (
IMAGE f) {s | Q(
IMAGE f s)}) /\
(!R. {l | R l} =
IMAGE (
MAP f) {l | R(
MAP f l)}))`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(ASSUME_TAC o
MATCH_MP
ORTHOGONAL_TRANSFORMATION_SURJECTIVE) THEN
CONJ_TAC THENL
[REWRITE_TAC[
IMAGE_CLAUSES;
MAP] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
CONJ_TAC THENL [ASM_MESON_TAC[
LINEAR_0]; ALL_TAC] THEN
REWRITE_TAC[SET_RULE `
UNIV =
IMAGE f
UNIV <=> !y. ?x. f x = y`] THEN
ASM_REWRITE_TAC[
SURJECTIVE_IMAGE];
MATCH_MP_TAC
QUANTIFY_SURJECTION_HIGHER_THM THEN ASM_REWRITE_TAC[]])
and oth =
prove
(`!f:real^N->real^N.
orthogonal_transformation f /\
(2 <= dimindex(:N) ==> det(matrix f) = &1)
==> linear f /\
(!x y. f x = f y ==> x = y) /\
(!y. ?x. f x = y) /\
(!x. norm(f x) = norm x) /\
(2 <= dimindex(:N) ==> det(matrix f) = &1)`,
GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[ASM_SIMP_TAC[
ORTHOGONAL_TRANSFORMATION_LINEAR];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_INJECTIVE];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_SURJECTIVE];
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION]])
and arithconv = REWRITE_CONV[DIMINDEX_1; DIMINDEX_2; DIMINDEX_3;
ARITH_RULE `1 <= 1`;
DIMINDEX_GE_1] THENC
NUM_REDUCE_CONV in
fun k tm ->
let x,bod = dest_forall tm in
let th0 = ISPECL [x; mk_small_numeral k]
ROTATION_RIGHTWARD_LINE in
let th1 = EXISTS_GENVAR_RULE
(MP th0 (EQT_ELIM(arithconv(lhand(concl th0))))) in
let [a;f],tm1 = strip_exists(concl th1) in
let th_orth,th2 = CONJ_PAIR(ASSUME tm1) in
let th_det,th2a = CONJ_PAIR th2 in
let th_works,th_zero = CONJ_PAIR th2a in
let thc,thq = CONJ_PAIR(PROVE_HYP th2 (UNDISCH(ISPEC f pth))) in
let th3 = CONV_RULE(RAND_CONV(SUBS_CONV(GSYM th_works::CONJUNCTS thc)))
(EXPAND_QUANTS_CONV(ASSUME(concl thq)) bod) in
let th4 = PROVE_HYP thq th3 in
let thps = CONJUNCTS(MATCH_MP oth (CONJ th_orth th_det)) in
let th5 = LINEAR_INVARIANTS f thps in
let th6 = PROVE_HYP th_orth
(GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV) [
BETA_THM; th5] th4) in
let ntm = mk_forall(a,mk_imp(concl th_zero,rand(concl th6))) in
let th7 = MP(SPEC a (ASSUME ntm)) th_zero in
let th8 = DISCH ntm (EQ_MP (SYM th6) th7) in
if intersect (frees(concl th8)) [a;f] = [] then
let th9 = PROVE_HYP th1 (itlist SIMPLE_CHOOSE [a;f] th8) in
let th10 = DISCH ntm (GEN x (UNDISCH th9)) in
let a' = variant (frees(concl th10))
(mk_var(fst(dest_var x),snd(dest_var a))) in
CONV_RULE(LAND_CONV (GEN_ALPHA_CONV a')) th10
else
let mtm = list_mk_forall([a;f],mk_imp(hd(hyp th8),rand(concl th6))) in
let th9 = EQ_MP (SYM th6) (UNDISCH(SPECL [a;f] (ASSUME mtm))) in
let th10 = itlist SIMPLE_CHOOSE [a;f] (DISCH mtm th9) in
let th11 = GEN x (PROVE_HYP th1 th10) in
MATCH_MP
MONO_FORALL th11;;
let cth0 = prove
(`!f:real^M->real^N.
linear f
==> vec 0 = f(vec 0) /\
{} =
IMAGE f {} /\
{} =
IMAGE (
IMAGE f) {}`,
REWRITE_TAC[
IMAGE_CLAUSES] THEN MESON_TAC[
LINEAR_0])
and cth1 =
prove
(`!f:real^M->real^N.
(!y. ?x. f x = y)
==> (:real^N) =
IMAGE f (:real^M) /\
(:real^N->bool) =
IMAGE (
IMAGE f) (:real^M->bool)`,
REWRITE_TAC[SET_RULE `
UNIV =
IMAGE f
UNIV <=> !y. ?x. f x = y`] THEN
REWRITE_TAC[
SURJECTIVE_IMAGE])
and sths = (CONJUNCTS o
prove)
(`(!f:real^M->real^N.
linear f /\ (!x. norm(f x) = norm x)
==> (!x y. f x = f y ==> x = y)) /\
(!f:real^N->real^N.
linear f /\ (!x. norm(f x) = norm x) ==> (!y. ?x. f x = y)) /\
(!f:real^N->real^N. linear f /\ (!x y. f x = f y ==> x = y)
==> (!y. ?x. f x = y)) /\
(!f:real^N->real^N. linear f /\ (!y. ?x. f x = y)
==> (!x y. f x = f y ==> x = y))`,
CONJ_TAC THENL
[ONCE_REWRITE_TAC[GSYM
VECTOR_SUB_EQ] THEN
SIMP_TAC[GSYM
LINEAR_SUB; GSYM
NORM_EQ_0];
MESON_TAC[
ORTHOGONAL_TRANSFORMATION_SURJECTIVE;
ORTHOGONAL_TRANSFORMATION_INJECTIVE;
ORTHOGONAL_TRANSFORMATION;
LINEAR_SURJECTIVE_IFF_INJECTIVE]])
and aths = (CONJUNCTS o
prove)
(`(!f s P. (!y. y
IN IMAGE f s ==> P y) <=> (!x. x
IN s ==> P(f x))) /\
(!f s P. (!u. u
IN IMAGE (
IMAGE f) s ==> P u) <=>
(!t. t
IN s ==> P(
IMAGE f t))) /\
(!f s P. (?y. y
IN IMAGE f s /\ P y) <=> (?x. x
IN s /\ P(f x))) /\
(!f s P. (?u. u
IN IMAGE (
IMAGE f) s /\ P u) <=>
(?t. t
IN s /\ P(
IMAGE f t)))`,
SET_TAC[]) in
fun avoid (asl,w as gl) ->
let f,wff = dest_forall w in
let vs,bod = strip_forall wff in
let ant,cons = dest_imp bod in
let hths = CONJUNCTS(ASSUME ant) in
let fths = hths @ mapfilter (USABLE_CONCLUSION f hths) sths in
let cths = mapfilter (USABLE_CONCLUSION f fths) [cth0; cth1]
and vconv =
try let vth = USABLE_CONCLUSION f fths
QUANTIFY_SURJECTION_HIGHER_THM in
PROVE_HYP vth o PARTIAL_EXPAND_QUANTS_CONV avoid (ASSUME(concl vth))
with Failure _ -> ALL_CONV
and bths = LINEAR_INVARIANTS f fths in
(MAP_EVERY X_GEN_TAC (f::vs) THEN DISCH_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) cths THEN
CONV_TAC(LAND_CONV vconv) THEN
GEN_REWRITE_TAC (LAND_CONV o REDEPTH_CONV) [bths] THEN
REWRITE_TAC[] THEN
REWRITE_TAC(mapfilter (ADD_ASSUM ant o ISPEC f) aths) THEN
GEN_REWRITE_TAC (LAND_CONV o REDEPTH_CONV) [bths] THEN
REWRITE_TAC[]) gl;;
let pth = prove
(`!a:real^N. ~(a = vec 0)
==> vec 0 = norm(a) % vec 0 /\
a = norm(a) % inv(norm a) % a /\
{} =
IMAGE (\x. norm(a) % x) {} /\
{} =
IMAGE (
IMAGE (\x. norm(a) % x)) {} /\
(:real^N) =
IMAGE (\x. norm(a) % x) (:real^N) /\
(:real^N->bool) =
IMAGE (
IMAGE (\x. norm(a) % x)) (:real^N->bool) /\
[] =
MAP (\x. norm(a) % x) []`,
REWRITE_TAC[
IMAGE_CLAUSES;
VECTOR_MUL_ASSOC;
VECTOR_MUL_RZERO;
MAP] THEN
SIMP_TAC[
NORM_EQ_0;
REAL_MUL_RINV;
VECTOR_MUL_LID] THEN
GEN_TAC THEN DISCH_TAC THEN
REWRITE_TAC[SET_RULE `
UNIV =
IMAGE f
UNIV <=> !y. ?x. f x = y`] THEN
ASM_REWRITE_TAC[
SURJECTIVE_IMAGE] THEN
X_GEN_TAC `y:real^N` THEN EXISTS_TAC `inv(norm(a:real^N)) % y:real^N` THEN
ASM_SIMP_TAC[
VECTOR_MUL_ASSOC;
NORM_EQ_0;
REAL_MUL_RINV;
VECTOR_MUL_LID])
and qth =
prove
(`!a:real^N.
~(a = vec 0)
==> ((!P. (!r:real. P r) <=> (!r. P(norm a * r))) /\
(!P. (?r:real. P r) <=> (?r. P(norm a * r))) /\
(!P. (!x:real^N. P x) <=> (!x. P (norm(a) % x))) /\
(!P. (?x:real^N. P x) <=> (?x. P (norm(a) % x))) /\
(!Q. (!s:real^N->bool. Q s) <=>
(!s. Q(
IMAGE (\x. norm(a) % x) s))) /\
(!Q. (?s:real^N->bool. Q s) <=>
(?s. Q(
IMAGE (\x. norm(a) % x) s))) /\
(!Q. (!s:(real^N->bool)->bool. Q s) <=>
(!s. Q(
IMAGE (
IMAGE (\x. norm(a) % x)) s))) /\
(!Q. (?s:(real^N->bool)->bool. Q s) <=>
(?s. Q(
IMAGE (
IMAGE (\x. norm(a) % x)) s))) /\
(!P. (!g:real^1->real^N. P g) <=>
(!g. P ((\x. norm(a) % x) o g))) /\
(!P. (?g:real^1->real^N. P g) <=>
(?g. P ((\x. norm(a) % x) o g))) /\
(!P. (!g:num->real^N. P g) <=>
(!g. P ((\x. norm(a) % x) o g))) /\
(!P. (?g:num->real^N. P g) <=>
(?g. P ((\x. norm(a) % x) o g))) /\
(!Q. (!l. Q l) <=> (!l. Q(
MAP (\x:real^N. norm(a) % x) l))) /\
(!Q. (?l. Q l) <=> (?l. Q(
MAP (\x:real^N. norm(a) % x) l)))) /\
((!P. {x:real^N | P x} =
IMAGE (\x. norm(a) % x) {x | P(norm(a) % x)}) /\
(!Q. {s:real^N->bool | Q s} =
IMAGE (
IMAGE (\x. norm(a) % x))
{s | Q(
IMAGE (\x. norm(a) % x) s)}) /\
(!R. {l:(real^N)list | R l} =
IMAGE (
MAP (\x:real^N. norm(a) % x))
{l | R(
MAP (\x:real^N. norm(a) % x) l)}))`,
GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC(TAUT
`(a /\ b) /\ c /\ d ==> (a /\ b /\ c) /\ d`) THEN
CONJ_TAC THENL
[ASM_MESON_TAC[
NORM_EQ_0; REAL_FIELD `~(x = &0) ==> x * inv x * a = a`];
MP_TAC(ISPEC `\x:real^N. norm(a:real^N) % x`
(INST_TYPE [`:real^1`,`:C`]
QUANTIFY_SURJECTION_HIGHER_THM)) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
ASM_SIMP_TAC[
SURJECTIVE_SCALING;
NORM_EQ_0]])
and lth =
prove
(`(!b:real^N. ~(b = vec 0) ==> (P(b) <=> Q(inv(norm b) % b)))
==> P(vec 0) /\ (!b. norm(b) = &1 ==> Q b) ==> (!b. P b)`,
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `b:real^N = vec 0` THEN ASM_SIMP_TAC[] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_SIMP_TAC[
NORM_MUL;
REAL_ABS_INV;
REAL_ABS_NORM;
REAL_MUL_LINV;
NORM_EQ_0]) in
fun avoid tm ->
let x,tm0 = dest_forall tm in
let cth = UNDISCH(ISPEC x pth)
and vth = UNDISCH(ISPEC x qth) in
let th1 = ONCE_REWRITE_CONV[cth] tm0 in
let th2 = CONV_RULE (RAND_CONV
(PARTIAL_EXPAND_QUANTS_CONV avoid vth)) th1 in
let th3 = SCALING_THEOREMS x in
let th3' = (end_itlist CONJ (map
(fun th -> let avs,_ = strip_forall(concl th) in
let gvs = map (genvar o type_of) avs in
GENL gvs (SPECL gvs th))
(CONJUNCTS th3))) in
let th4 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV)
[
BETA_THM; th3'] th2 in
MATCH_MP lth (GEN x (DISCH_ALL th4));;
let oth = prove
(`!f:real^M->real^N.
linear f /\ (!x. norm(f x) = norm x)
==> linear f /\
(!x y. f x = f y ==> x = y) /\
(!x. norm(f x) = norm x)`,
MESON_TAC[
PRESERVES_NORM_INJECTIVE])
and cth =
prove
(`linear(f:real^M->real^N)
==> vec 0 = f(vec 0) /\
{} =
IMAGE f {} /\
{} =
IMAGE (
IMAGE f) {} /\
[] =
MAP f []`,
REWRITE_TAC[
IMAGE_CLAUSES;
MAP; GSYM
LINEAR_0]) in
fun dth th ->
let ath = GEN_ALL th
and eth = MATCH_MP
ISOMETRY_UNIV_UNIV dth
and avoid = variables(concl th) in
let f,bod = dest_exists(concl eth) in
let fimage = list_mk_icomb "IMAGE" [f]
and fmap = list_mk_icomb "MAP" [f]
and fcompose = list_mk_icomb "o" [f] in
let fimage2 = list_mk_icomb "IMAGE" [fimage] in
let lin,iso = CONJ_PAIR(ASSUME bod) in
let olduniv = rand(rand(concl dth))
and newuniv = rand(lhand(concl dth)) in
let oldty = fst(dest_fun_ty(type_of olduniv))
and newty = fst(dest_fun_ty(type_of newuniv)) in
let newvar v =
let n,t = dest_var v in
variant avoid (mk_var(n,tysubst[newty,oldty] t)) in
let newterm v =
try let v' = newvar v in
tryfind (fun f -> mk_comb(f,v')) [f;fimage;fmap;fcompose;fimage2]
with Failure _ -> v in
let specrule th =
let v = fst(dest_forall(concl th)) in SPEC (newterm v) th in
let sth = SUBS(CONJUNCTS(MATCH_MP cth lin)) ath in
let fth = SUBS[SYM(MATCH_MP
LINEAR_0 lin)] (repeat specrule sth) in
let thps = CONJUNCTS(MATCH_MP oth (ASSUME bod)) in
let th5 = LINEAR_INVARIANTS f thps in
let th6 = GEN_REWRITE_RULE REDEPTH_CONV [th5] fth in
let th7 = PROVE_HYP eth (SIMPLE_CHOOSE f th6) in
GENL (map newvar (fst(strip_forall(concl ath)))) th7;;
let bth = prove
(`dimindex(:M) = dimindex(:N)
==> ?f:real^M->real^N.
(linear f /\ (!y. ?x. f x = y)) /\
(!x. norm(f x) = norm x)`,
REWRITE_TAC[SET_RULE `(!y. ?x. f x = y) <=>
IMAGE f
UNIV =
UNIV`] THEN
DISCH_TAC THEN REWRITE_TAC[GSYM
CONJ_ASSOC] THEN
MATCH_MP_TAC
ISOMETRY_UNIV_SUBSPACE THEN
REWRITE_TAC[
SUBSPACE_UNIV;
DIM_UNIV] THEN FIRST_ASSUM ACCEPT_TAC)
and pth =
prove
(`!f:real^M->real^N.
linear f /\ (!y. ?x. f x = y)
==> (vec 0 = f(vec 0) /\
{} =
IMAGE f {} /\
{} =
IMAGE (
IMAGE f) {} /\
(:real^N) =
IMAGE f (:real^M) /\
(:real^N->bool) =
IMAGE (
IMAGE f) (:real^M->bool) /\
[] =
MAP f []) /\
((!P. (!x. P x) <=> (!x. P (f x))) /\
(!P. (?x. P x) <=> (?x. P (f x))) /\
(!Q. (!s. Q s) <=> (!s. Q (
IMAGE f s))) /\
(!Q. (?s. Q s) <=> (?s. Q (
IMAGE f s))) /\
(!Q. (!s. Q s) <=> (!s. Q (
IMAGE (
IMAGE f) s))) /\
(!Q. (?s. Q s) <=> (?s. Q (
IMAGE (
IMAGE f) s))) /\
(!P. (!g:real^1->real^N. P g) <=> (!g. P (f o g))) /\
(!P. (?g:real^1->real^N. P g) <=> (?g. P (f o g))) /\
(!P. (!g:num->real^N. P g) <=> (!g. P (f o g))) /\
(!P. (?g:num->real^N. P g) <=> (?g. P (f o g))) /\
(!Q. (!l. Q l) <=> (!l. Q(
MAP f l))) /\
(!Q. (?l. Q l) <=> (?l. Q(
MAP f l)))) /\
((!P. {x | P x} =
IMAGE f {x | P(f x)}) /\
(!Q. {s | Q s} =
IMAGE (
IMAGE f) {s | Q(
IMAGE f s)}) /\
(!R. {l | R l} =
IMAGE (
MAP f) {l | R(
MAP f l)}))`,
GEN_TAC THEN
SIMP_TAC[SET_RULE `
UNIV =
IMAGE f
UNIV <=> (!y. ?x. f x = y)`;
SURJECTIVE_IMAGE] THEN
MATCH_MP_TAC MONO_AND THEN
REWRITE_TAC[
QUANTIFY_SURJECTION_HIGHER_THM] THEN
REWRITE_TAC[
IMAGE_CLAUSES;
MAP] THEN MESON_TAC[
LINEAR_0]) in
fun dth th ->
let eth = EXISTS_GENVAR_RULE (MATCH_MP bth dth) in
let f,bod = dest_exists(concl eth) in
let lsth,neth = CONJ_PAIR(ASSUME bod) in
let cth,qth = CONJ_PAIR(MATCH_MP pth lsth) in
let th1 = CONV_RULE
(EXPAND_QUANTS_CONV qth THENC SUBS_CONV(CONJUNCTS cth)) th in
let ith = LINEAR_INVARIANTS f (neth::CONJUNCTS lsth) in
let th2 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV) [
BETA_THM;ith] th1 in
let th3 = GEN f (DISCH bod th2) in
MP (CONV_RULE (REWR_CONV
LEFT_FORALL_IMP_THM) th3) eth;;