(* ========================================================================= *)
(* 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). *)
(* ------------------------------------------------------------------------- *)
let trace = new_definition
`(trace:real^N^N->real) A = sum(1..dimindex(:N)) (\i. A$i$i)`;;
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 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 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 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;;