(* ========================================================================= *)
(* Complex transcendentals and their real counterparts. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/determinants.ml";;
needs "Multivariate/canal.ml";;
prioritize_complex();;
(* ------------------------------------------------------------------------- *)
(* The complex exponential function. *)
(* ------------------------------------------------------------------------- *)
let CEXP_CONVERGES_UNIFORMLY = prove
(`!R e. &0 < R /\ &0 < e
==> ?N. !n z. n >= N /\ norm(z) < R
==> norm(vsum(0..n) (\i. z pow i / Cx(&(
FACT i))) -
cexp(z)) <= e`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`R:real`; `e / &2`]
CEXP_CONVERGES_UNIFORMLY_CAUCHY) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `N:num` THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`n:num`; `z:complex`] THEN STRIP_TAC THEN
MP_TAC(SPEC `z:complex`
CEXP_CONVERGES) THEN
REWRITE_TAC[sums;
LIM_SEQUENTIALLY;
FROM_0;
INTER_UNIV; dist] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `M:num` (MP_TAC o SPEC `n + M + 1`)) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`n + 1`; `n + M + 1`; `z:complex`]) THEN
ASM_SIMP_TAC[ARITH_RULE `(n >= N ==> n + 1 >= N) /\ M <= n + M + 1`] THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
VSUM_ADD_SPLIT;
LE_0] THEN
CONV_TAC(ONCE_DEPTH_CONV(ALPHA_CONV `i:num`)) THEN NORM_ARITH_TAC);;
let CEXP_ADD = prove
(`!w z. cexp(w + z) = cexp(w) * cexp(z)`,
REPEAT GEN_TAC THEN
MP_TAC(SPECL [`w:complex`; `z:complex`]
CEXP_ADD_MUL) THEN
MP_TAC(SPEC `z:complex`
CEXP_NEG_LMUL) THEN CONV_TAC COMPLEX_FIELD);;
let CEXP_BOUND_BLEMMA = prove
(`!B. (!z. norm(z) <= &1 / &2 ==> norm(cexp z) <= B)
==> !z. norm(z) <= &1 / &2 ==> norm(cexp z) <= &1 + B / &2`,
let CSIN_ADD = prove
(`!w z. csin(w + z) = csin(w) * ccos(z) + ccos(w) * csin(z)`,
let CCOS_ADD = prove
(`!w z. ccos(w + z) = ccos(w) * ccos(z) - csin(w) * csin(z)`,
let CSIN_DOUBLE = prove
(`!z. csin(Cx(&2) * z) = Cx(&2) * csin(z) * ccos(z)`,
REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`;
CSIN_ADD] THEN
CONV_TAC COMPLEX_RING);;
let CCOS_DOUBLE = prove
(`!z. ccos(Cx(&2) * z) = (ccos(z) pow 2) - (csin(z) pow 2)`,
REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`;
CCOS_ADD] THEN
CONV_TAC COMPLEX_RING);;
let CSIN_SUB = prove
(`!w z. csin(w - z) = csin(w) * ccos(z) - ccos(w) * csin(z)`,
let CCOS_SUB = prove
(`!w z. ccos(w - z) = ccos(w) * ccos(z) + csin(w) * csin(z)`,
let COMPLEX_ADD_CSIN = prove
(`!w z. csin(w) + csin(z) =
Cx(&2) * csin((w + z) / Cx(&2)) * ccos((w - z) / Cx(&2))`,
SIMP_TAC[
COMPLEX_MUL_CSIN_CCOS; COMPLEX_RING `Cx(&2) * x / Cx(&2) = x`] THEN
REPEAT GEN_TAC THEN BINOP_TAC THEN AP_TERM_TAC THEN CONV_TAC COMPLEX_RING);;
let COMPLEX_ADD_CCOS = prove
(`!w z. ccos(w) + ccos(z) =
Cx(&2) * ccos((w + z) / Cx(&2)) * ccos((w - z) / Cx(&2))`,
SIMP_TAC[
COMPLEX_MUL_CCOS_CCOS; COMPLEX_RING `Cx(&2) * x / Cx(&2) = x`] THEN
REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [
COMPLEX_ADD_SYM] THEN
BINOP_TAC THEN AP_TERM_TAC THEN CONV_TAC COMPLEX_RING);;
let COMPLEX_SUB_CCOS = prove
(`!w z. ccos(w) - ccos(z) =
Cx(&2) * csin((w + z) / Cx(&2)) * csin((z - w) / Cx(&2))`,
SIMP_TAC[
COMPLEX_MUL_CSIN_CSIN; COMPLEX_RING `Cx(&2) * x / Cx(&2) = x`] THEN
REPEAT GEN_TAC THEN BINOP_TAC THEN AP_TERM_TAC THEN CONV_TAC COMPLEX_RING);;
let CCOS_DOUBLE_CCOS = prove
(`!z. ccos(Cx(&2) * z) = Cx(&2) * ccos z pow 2 - Cx(&1)`,
GEN_TAC THEN REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`;
CCOS_ADD] THEN
MP_TAC(SPEC `z:complex`
CSIN_CIRCLE) THEN CONV_TAC COMPLEX_RING);;
let CCOS_DOUBLE_CSIN = prove
(`!z. ccos(Cx(&2) * z) = Cx(&1) - Cx(&2) * csin z pow 2`,
GEN_TAC THEN REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`;
CCOS_ADD] THEN
MP_TAC(SPEC `z:complex`
CSIN_CIRCLE) THEN CONV_TAC COMPLEX_RING);;
let CEXP_EULER = prove
(`!z. cexp(ii * z) = ccos(z) + ii * csin(z)`,
REWRITE_TAC[ccos; csin] THEN CONV_TAC COMPLEX_FIELD);;
let DEMOIVRE = prove
(`!z n. (ccos z + ii * csin z) pow n =
ccos(Cx(&n) * z) + ii * csin(Cx(&n) * z)`,
let REAL_EXP_MONO_LT = prove
(`!x y. exp(x) < exp(y) <=> x < y`,
REPEAT GEN_TAC THEN MATCH_MP_TAC(REAL_ARITH
`(x < y ==> f < g) /\ (x = y ==> f = g) /\ (y < x ==> g < f)
==> (f < g <=> x < y)`) THEN
SIMP_TAC[
REAL_EXP_MONO_IMP]);;
let SIN_ADD = prove
(`!x y. sin(x + y) = sin(x) * cos(y) + cos(x) * sin(y)`,
let COS_ADD = prove
(`!x y. cos(x + y) = cos(x) * cos(y) - sin(x) * sin(y)`,
let SIN_SUB = prove
(`!w z. sin(w - z) = sin(w) * cos(z) - cos(w) * sin(z)`,
let COS_SUB = prove
(`!w z. cos(w - z) = cos(w) * cos(z) + sin(w) * sin(z)`,
let COS_DOUBLE_SIN = prove
(`!x. cos(&2 * x) = &1 - &2 * sin x pow 2`,
GEN_TAC THEN REWRITE_TAC[REAL_RING `&2 * x = x + x`;
COS_ADD] THEN
MP_TAC(SPEC `x:real`
SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
let EULER = prove
(`!z. cexp(z) = Cx(exp(Re z)) * (Cx(cos(Im z)) + ii * Cx(sin(Im z)))`,
let RE_CSIN = prove
(`!z. Re(csin z) = (exp(Im z) + exp(--(Im z))) / &2 * sin(Re z)`,
let IM_CSIN = prove
(`!z. Im(csin z) = (exp(Im z) - exp(--(Im z))) / &2 * cos(Re z)`,
let RE_CCOS = prove
(`!z. Re(ccos z) = (exp(Im z) + exp(--(Im z))) / &2 * cos(Re z)`,
let IM_CCOS = prove
(`!z. Im(ccos z) = (exp(--(Im z)) - exp(Im z)) / &2 * sin(Re z)`,
let IVT_INCREASING_RE = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f continuous at (Cx x)) /\
Re(f(Cx a)) <= y /\ y <= Re(f(Cx b))
==> ?x. a <= x /\ x <= b /\ Re(f(Cx x)) = y`,
let IVT_DECREASING_RE = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f continuous at (Cx x)) /\
Re(f(Cx b)) <= y /\ y <= Re(f(Cx a))
==> ?x. a <= x /\ x <= b /\ Re(f(Cx x)) = y`,
let IVT_INCREASING_IM = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f continuous at (Cx x)) /\
Im(f(Cx a)) <= y /\ y <= Im(f(Cx b))
==> ?x. a <= x /\ x <= b /\ Im(f(Cx x)) = y`,
let IVT_DECREASING_IM = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f continuous at (Cx x)) /\
Im(f(Cx b)) <= y /\ y <= Im(f(Cx a))
==> ?x. a <= x /\ x <= b /\ Im(f(Cx x)) = y`,
let log_def = new_definition
`log y = @x. exp(x) = y`;;
let LOG_MUL = prove
(`!x y. &0 < x /\ &0 < y ==> (log(x * y) = log(x) + log(y))`,
let LOG_INJ = prove
(`!x y. &0 < x /\ &0 < y ==> (log(x) = log(y) <=> x = y)`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM
REAL_EXP_INJ] THEN
ASM_SIMP_TAC[
EXP_LOG]);;
let LOG_DIV = prove
(`!x y. &0 < x /\ &0 < y ==> log(x / y) = log(x) - log(y)`,
let PI_WORKS = prove
(`&0 < pi /\ sin(pi) = &0 /\ !x. &0 < x /\ x < pi ==> ~(sin x = &0)`,
let COS_POS_PI = prove
(`!x. --(pi / &2) < x /\ x < pi / &2 ==> &0 < cos(x)`,
GEN_TAC THEN MP_TAC(SPEC `abs x`
COS_POS_PI2) THEN REWRITE_TAC[
COS_ABS] THEN
ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[
COS_0] THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
let COS_EQ_0 = prove
(`!x. cos(x) = &0 <=> ?n. integer n /\ x = (n + &1 / &2) * pi`,
GEN_TAC THEN REWRITE_TAC[
COS_SIN;
SIN_EQ_0] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `--n:real` THEN ASM_REWRITE_TAC[
INTEGER_NEG] THEN
ASM_REAL_ARITH_TAC);;
let COS_ZERO_PI = prove
(`!x. cos(x) = &0 <=>
(?n. x = (&n + &1 / &2) * pi) \/ (?n. x = --((&n + &1 / &2) * pi))`,
GEN_TAC THEN REWRITE_TAC[
COS_EQ_0;
INTEGER_CASES;
RIGHT_OR_DISTRIB] THEN
REWRITE_TAC[
EXISTS_OR_THM;
LEFT_AND_EXISTS_THM] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN SIMP_TAC[
UNWIND_THM2] THEN EQ_TAC THEN
DISCH_THEN(DISJ_CASES_THEN (X_CHOOSE_THEN `n:num` SUBST1_TAC)) THENL
[DISJ1_TAC THEN EXISTS_TAC `n:num`;
ASM_CASES_TAC `n = 0` THENL
[DISJ1_TAC THEN EXISTS_TAC `0`;
DISJ2_TAC THEN EXISTS_TAC `n - 1`];
DISJ1_TAC THEN EXISTS_TAC `n:num`;
DISJ2_TAC THEN EXISTS_TAC `n + 1`] THEN
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_ADD;
ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
REAL_ARITH_TAC);;
let SIN_ZERO = prove
(`!x. (sin(x) = &0) <=> (?n.
EVEN n /\ x = &n * (pi / &2)) \/
(?n.
EVEN n /\ x = --(&n * (pi / &2)))`,
let COS_ZERO = prove
(`!x. cos(x) = &0 <=> (?n. ~EVEN n /\ (x = &n * (pi / &2))) \/
(?n. ~EVEN n /\ (x = --(&n * (pi / &2))))`,
let COS_ONE_2PI = prove
(`!x. (cos(x) = &1) <=> (?n. x = &n * &2 * pi) \/ (?n. x = --(&n * &2 * pi))`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
[FIRST_ASSUM(MP_TAC o SPEC `sin(x)` o MATCH_MP (REAL_RING
`c = &1 ==> !s. s pow 2 + c pow 2 = &1 ==> s = &0`)) THEN
REWRITE_TAC[
SIN_ZERO_PI;
SIN_CIRCLE] THEN
DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `n:num` SUBST_ALL_TAC)) THEN
POP_ASSUM MP_TAC THEN REWRITE_TAC[
COS_NEG;
COS_NPI;
REAL_POW_NEG] THEN
COND_CASES_TAC THEN REWRITE_TAC[
REAL_POW_ONE] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[
EVEN_EXISTS]) THEN
REWRITE_TAC[
OR_EXISTS_THM] THEN MATCH_MP_TAC
MONO_EXISTS THEN
SIMP_TAC[GSYM REAL_OF_NUM_MUL] THEN REAL_ARITH_TAC;
FIRST_X_ASSUM (DISJ_CASES_THEN CHOOSE_TAC) THEN
ASM_REWRITE_TAC[
COS_NEG; REAL_MUL_ASSOC; REAL_OF_NUM_MUL;
COS_NPI;
REAL_POW_NEG;
EVEN_MULT; ARITH;
REAL_POW_ONE]]);;
let COS_PI6 = prove
(`cos(pi / &6) = sqrt(&3) / &2`,
MP_TAC(ISPEC `pi / &6`
COS_TREBLE_COS) THEN
REWRITE_TAC[REAL_ARITH `&3 * x / &6 = x / &2`;
COS_PI2] THEN
REWRITE_TAC[REAL_RING `&0 = &4 * c pow 3 - &3 * c <=>
c = &0 \/ (&2 * c) pow 2 = &3`] THEN
SUBGOAL_THEN `&0 < cos(pi / &6)` ASSUME_TAC THENL
[MATCH_MP_TAC
COS_POS_PI THEN MP_TAC
PI_POS THEN REAL_ARITH_TAC;
DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
[ASM_MESON_TAC[
REAL_LT_REFL]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o AP_TERM `sqrt`) THEN
ASM_SIMP_TAC[
POW_2_SQRT;
REAL_LE_MUL;
REAL_LT_IMP_LE;
REAL_POS] THEN
REAL_ARITH_TAC]);;
let SIN_PI6 = prove
(`sin(pi / &6) = &1 / &2`,
MP_TAC(SPEC `pi / &6`
SIN_CIRCLE) THEN REWRITE_TAC[
COS_PI6] THEN
SIMP_TAC[
REAL_POW_DIV;
SQRT_POW_2;
REAL_POS] THEN MATCH_MP_TAC(REAL_FIELD
`~(s + &1 / &2 = &0) ==> s pow 2 + &3 / &2 pow 2 = &1 ==> s = &1 / &2`) THEN
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(x + &1 / &2 = &0)`) THEN
MATCH_MP_TAC
SIN_POS_PI THEN MP_TAC
PI_POS THEN REAL_ARITH_TAC);;
let SIN_POS_PI_REV = prove
(`!x. &0 <= x /\ x <= &2 * pi /\ &0 < sin x ==> &0 < x /\ x < pi`,
GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
ASM_REWRITE_TAC[
SIN_0;
REAL_LT_REFL] THEN
ASM_CASES_TAC `x = pi` THEN
ASM_REWRITE_TAC[
SIN_PI;
REAL_LT_REFL] THEN
ASM_CASES_TAC `x = &2 * pi` THEN
ASM_REWRITE_TAC[
SIN_NPI;
REAL_LT_REFL] THEN
REPEAT STRIP_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[GSYM
REAL_NOT_LE] THEN DISCH_TAC THEN
SUBGOAL_THEN `&0 < sin(&2 * pi - x)` MP_TAC THENL
[MATCH_MP_TAC
SIN_POS_PI THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[
SIN_SUB;
SIN_NPI;
COS_NPI] THEN ASM_REAL_ARITH_TAC]);;
let SINCOS_TOTAL_PI2 = prove
(`!x y. &0 <= x /\ &0 <= y /\ x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t <= pi / &2 /\ x = cos t /\ y = sin t`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `y:real`
SIN_TOTAL_POS) THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`x pow 2 + y pow 2 = &1
==> (&1 < y ==> &1 pow 2 < y pow 2) /\ &0 <= x * x
==> y <= &1`)) THEN
SIMP_TAC[
REAL_LE_SQUARE;
REAL_POW_LT2;
REAL_POS; ARITH];
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `t:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `x = cos t \/ x = --(cos t)` MP_TAC THENL
[MP_TAC(SPEC `t:real`
SIN_CIRCLE);
MP_TAC(SPEC `t:real`
COS_POS_PI_LE)] THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD]);;
let SINCOS_TOTAL_PI = prove
(`!x y. &0 <= y /\ x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t <= pi /\ x = cos t /\ y = sin t`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `&0 <= x \/ &0 <= --x`) THENL
[MP_TAC(SPECL [`x:real`; `y:real`]
SINCOS_TOTAL_PI2);
MP_TAC(SPECL [`--x:real`; `y:real`]
SINCOS_TOTAL_PI2)] THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `t:real`; EXISTS_TAC `pi - t`] THEN
ASM_REWRITE_TAC[
SIN_SUB;
COS_SUB;
SIN_PI;
COS_PI] THEN
ASM_REAL_ARITH_TAC);;
let SINCOS_TOTAL_2PI = prove
(`!x y. x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t < &2 * pi /\ x = cos t /\ y = sin t`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = &1 /\ y = &0` THENL
[EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[
SIN_0;
COS_0] THEN
MP_TAC
PI_POS THEN REAL_ARITH_TAC;
ALL_TAC] THEN
DISJ_CASES_TAC(REAL_ARITH `&0 <= y \/ &0 <= --y`) THENL
[MP_TAC(SPECL [`x:real`; `y:real`]
SINCOS_TOTAL_PI);
MP_TAC(SPECL [`x:real`; `--y:real`]
SINCOS_TOTAL_PI)] THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `t:real`; EXISTS_TAC `&2 * pi - t`] THEN
ASM_REWRITE_TAC[
SIN_SUB;
COS_SUB;
SIN_NPI;
COS_NPI] THENL
[MP_TAC
PI_POS THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REPEAT(POP_ASSUM MP_TAC) THEN ASM_CASES_TAC `t = &0` THEN
ASM_REWRITE_TAC[
SIN_0;
COS_0] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
let CEXP_EQ_1 = prove
(`!z. cexp z = Cx(&1) <=> Re(z) = &0 /\ ?n. integer n /\ Im(z) = &2 * n * pi`,
let CEXP_EQ = prove
(`!w z. cexp w = cexp z <=> ?n. integer n /\ w = z + Cx(&2 * n * pi) * ii`,
let SIN_COS_EQ = prove
(`!x y. sin y = sin x /\ cos y = cos x <=>
?n. integer n /\ y = x + &2 * n * pi`,
let SIN_COS_INJ = prove
(`!x y. sin x = sin y /\ cos x = cos y /\ abs(x - y) < &2 * pi ==> x = y`,
let CCOS_EQ_0 = prove
(`!z. ccos z = Cx(&0) <=> ?n. integer n /\ z = Cx((n + &1 / &2) * pi)`,
let CCOS_EQ_1 = prove
(`!z. ccos z = Cx(&1) <=> ?n. integer n /\ z = Cx(&2 * n * pi)`,
GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV)
[COMPLEX_RING `z = Cx(&2) * z / Cx(&2)`] THEN
REWRITE_TAC[
CCOS_DOUBLE_CSIN; COMPLEX_RING
`a - Cx(&2) * s pow 2 = a <=> s = Cx(&0)`] THEN
REWRITE_TAC[
CSIN_EQ_0;
CX_MUL] THEN
EQ_TAC THEN MATCH_MP_TAC
MONO_EXISTS THEN SIMP_TAC[] THEN
CONV_TAC COMPLEX_RING);;
let CSIN_EQ_1 = prove
(`!z. csin z = Cx(&1) <=> ?n. integer n /\ z = Cx((&2 * n + &1 / &2) * pi)`,
let CSIN_EQ_MINUS1 = prove
(`!z. csin z = --Cx(&1) <=>
?n. integer n /\ z = Cx((&2 * n + &3 / &2) * pi)`,
GEN_TAC THEN REWRITE_TAC[COMPLEX_RING `z:complex = --w <=> --z = w`] THEN
REWRITE_TAC[GSYM
CSIN_NEG;
CSIN_EQ_1] THEN
REWRITE_TAC[COMPLEX_RING `--z:complex = w <=> z = --w`] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
EXISTS_TAC `--(n + &1)` THEN
ASM_SIMP_TAC[
INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let SIN_EQ_1 = prove
(`!x. sin x = &1 <=> ?n. integer n /\ x = (&2 * n + &1 / &2) * pi`,
let CX_SINH = prove
(`Cx((exp x - inv(exp x)) / &2) = --ii * csin(ii * Cx x)`,
REWRITE_TAC[csin; COMPLEX_RING `--ii * ii * z = z /\ ii * ii * z = --z`] THEN
REWRITE_TAC[
CEXP_NEG; GSYM
CX_EXP; GSYM
CX_INV;
CX_SUB;
CX_DIV] THEN
CONV_TAC COMPLEX_FIELD);;
let CX_COSH = prove
(`Cx((exp x + inv(exp x)) / &2) = ccos(ii * Cx x)`,
REWRITE_TAC[ccos; COMPLEX_RING `--ii * ii * z = z /\ ii * ii * z = --z`] THEN
REWRITE_TAC[
CEXP_NEG; GSYM
CX_EXP; GSYM
CX_INV;
CX_ADD;
CX_DIV] THEN
CONV_TAC COMPLEX_FIELD);;
let NORM_CSIN_POW_2 = prove
(`!z. norm(csin z) pow 2 =
(exp(&2 * Im z) + inv(exp(&2 * Im z)) - &2 * cos(&2 * Re z)) / &4`,
let CSIN_EQ = prove
(`!w z. csin w = csin z <=>
?n. integer n /\
(w = z + Cx(&2 * n * pi) \/ w = --z + Cx((&2 * n + &1) * pi))`,
let CCOS_EQ = prove
(`!w z. ccos(w) = ccos(z) <=>
?n. integer n /\
(w = z + Cx(&2 * n * pi) \/ w = --z + Cx(&2 * n * pi))`,
let SIN_EQ = prove
(`!x y. sin x = sin y <=>
?n. integer n /\
(x = y + &2 * n * pi \/ x = --y + (&2 * n + &1) * pi)`,
let COS_EQ = prove
(`!x y. cos x = cos y <=>
?n. integer n /\
(x = y + &2 * n * pi \/ x = --y + &2 * n * pi)`,
let TAYLOR_CEXP = prove
(`!n z. norm(cexp z - vsum(0..n) (\k. z pow k / Cx(&(
FACT k))))
<= exp(abs(Re z)) * (norm z) pow (n + 1) / &(
FACT n)`,
let TAYLOR_CSIN_RAW = prove
(`!n z. norm(csin z -
vsum(0..n) (\k. if
ODD k
then --ii * (ii * z) pow k / Cx(&(
FACT k))
else Cx(&0)))
<= exp(abs(Im z)) * (norm z) pow (n + 1) / &(
FACT n)`,
let TAYLOR_CSIN = prove
(`!n z. norm(csin z -
vsum(0..n) (\k. --Cx(&1) pow k *
z pow (2 * k + 1) / Cx(&(
FACT(2 * k + 1)))))
<= exp(abs(Im z)) * norm(z) pow (2 * n + 3) / &(
FACT(2 * n + 2))`,
let TAYLOR_CCOS_RAW = prove
(`!n z. norm(ccos z -
vsum(0..n) (\k. if
EVEN k
then (ii * z) pow k / Cx(&(
FACT k))
else Cx(&0)))
<= exp(abs(Im z)) * (norm z) pow (n + 1) / &(
FACT n)`,
let TAYLOR_CCOS = prove
(`!n z. norm(ccos z -
vsum(0..n) (\k. --Cx(&1) pow k *
z pow (2 * k) / Cx(&(
FACT(2 * k)))))
<= exp(abs(Im z)) * norm(z) pow (2 * n + 2) / &(
FACT(2 * n + 1))`,
let Arg_DEF = new_definition
`Arg z = if z = Cx(&0) then &0
else @t. &0 <= t /\ t < &2 * pi /\
z = Cx(norm(z)) * cexp(ii * Cx t)`;;let ARG = prove
(`!z. &0 <= Arg(z) /\ Arg(z) < &2 * pi /\
z = Cx(norm z) * cexp(ii * Cx(Arg z))`,
let ARG_UNIQUE = prove
(`!a r z. &0 < r /\ Cx r * cexp(ii * Cx a) = z /\ &0 <= a /\ a < &2 * pi
==> Arg z = a`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN
MATCH_MP_TAC(COMPLEX_RING `ii * x = ii * y ==> x = y`) THEN
MATCH_MP_TAC
COMPLEX_EQ_CEXP THEN CONJ_TAC THENL
[REWRITE_TAC[
IM_MUL_II;
RE_CX] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x < p /\ &0 <= y /\ y < p
==> abs(x - y) < p`) THEN
ASM_SIMP_TAC[
ARG];
MATCH_MP_TAC(COMPLEX_RING
`!a b. Cx a = Cx b /\ ~(Cx b = Cx(&0)) /\
Cx a * w = Cx b * z ==> w = z`) THEN
MAP_EVERY EXISTS_TAC [`norm(z:complex)`; `r:real`] THEN
ASM_REWRITE_TAC[GSYM
ARG] THEN ASM_SIMP_TAC[
CX_INJ;
REAL_LT_IMP_NZ] THEN
EXPAND_TAC "z" THEN
REWRITE_TAC[
NORM_CEXP_II;
COMPLEX_NORM_MUL;
COMPLEX_NORM_CX] THEN
ASM_REAL_ARITH_TAC]);;
let ARG_INV = prove
(`!z. ~(real z /\ &0 <= Re z) ==> Arg(inv z) = &2 * pi - Arg z`,
let ARG_EQ = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> (Arg w = Arg z <=> ?x. &0 < x /\ w = Cx(x) * z)`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[ALL_TAC; STRIP_TAC THEN ASM_SIMP_TAC[
ARG_MUL_CX]] THEN
DISCH_TAC THEN
MAP_EVERY (MP_TAC o CONJUNCT2 o CONJUNCT2 o C SPEC
ARG)
[`z:complex`; `w:complex`] THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(fun th -> CONV_TAC(SUBS_CONV(CONJUNCTS th))) THEN
EXISTS_TAC `norm(w:complex) / norm(z:complex)` THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
COMPLEX_NORM_NZ;
CX_DIV] THEN
REWRITE_TAC[
COMPLEX_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
COMPLEX_DIV_RMUL;
COMPLEX_NORM_ZERO;
CX_INJ]);;
let ARG_INV_EQ_0 = prove
(`!z. Arg(inv z) = &0 <=> Arg z = &0`,
GEN_TAC THEN REWRITE_TAC[
ARG_EQ_0;
REAL_INV_EQ] THEN
MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
REWRITE_TAC[real] THEN DISCH_TAC THEN ASM_REWRITE_TAC[
complex_inv;
RE] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[
REAL_ADD_RID] THEN
ASM_CASES_TAC `Re z = &0` THEN ASM_REWRITE_TAC[
real_div;
REAL_MUL_LZERO] THEN
ASM_SIMP_TAC[REAL_FIELD `~(x = &0) ==> x * inv(x pow 2) = inv x`] THEN
REWRITE_TAC[
REAL_LE_INV_EQ]);;
let ARG_LE_DIV_SUM = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0)) /\ Arg(w) <= Arg(z)
==> Arg(z) = Arg(w) + Arg(z / w)`,
let ARG_LE_DIV_SUM_EQ = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> (Arg(w) <= Arg(z) <=> Arg(z) = Arg(w) + Arg(z / w))`,
let REAL_SUB_ARG = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg w - Arg z = if Arg(z) <= Arg(w) then Arg(w / z)
else Arg(w / z) - &2 * pi`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
[MP_TAC(ISPECL [`z:complex`; `w:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
MP_TAC(ISPECL [`w:complex`; `z:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[REAL_ARITH `a - (a + b):real = --b`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM
COMPLEX_INV_DIV] THEN
MATCH_MP_TAC(REAL_ARITH `x = &2 * pi - y ==> --x = y - &2 * pi`) THEN
MATCH_MP_TAC
ARG_INV THEN REWRITE_TAC[GSYM
ARG_EQ_0] THEN
ONCE_REWRITE_TAC[GSYM
COMPLEX_INV_DIV] THEN
REWRITE_TAC[
ARG_INV_EQ_0] THEN
MP_TAC(ISPECL [`w:complex`; `z:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC]);;
let REAL_ADD_ARG = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg(w) + Arg(z) =
if Arg w + Arg z < &2 * pi
then Arg(w * z)
else Arg(w * z) + &2 * pi`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`w * z:complex`; `z:complex`]
REAL_SUB_ARG) THEN
MP_TAC(SPECL [`z:complex`; `w * z:complex`]
ARG_LE_DIV_SUM_EQ) THEN
ASM_SIMP_TAC[
COMPLEX_ENTIRE; COMPLEX_FIELD
`~(z = Cx(&0)) ==> (w * z) / z = w`] THEN
ASM_CASES_TAC `Arg (w * z) = Arg z + Arg w` THEN ASM_REWRITE_TAC[] THENL
[ASM_MESON_TAC[
ARG; REAL_ADD_SYM];
SIMP_TAC[REAL_ARITH `wz - z = w - &2 * pi <=> w + z = wz + &2 * pi`] THEN
REWRITE_TAC[REAL_ARITH `w + p < p <=> ~(&0 <= w)`;
ARG]]);;
let ARG_MUL = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg(w * z) = if Arg w + Arg z < &2 * pi
then Arg w + Arg z
else (Arg w + Arg z) - &2 * pi`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
REAL_ADD_ARG) THEN
REAL_ARITH_TAC);;
let ARG_CNJ = prove
(`!z. Arg(cnj z) = if real z /\ &0 <= Re z then Arg z else &2 * pi - Arg z`,
let ARG_REAL = prove
(`!z. real z ==> Arg z = if &0 <= Re z then &0 else pi`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[
ARG_EQ_PI;
ARG_EQ_0] THEN ASM_REAL_ARITH_TAC);;
let ARG_CEXP = prove
(`!z. &0 <= Im z /\ Im z < &2 * pi ==> Arg(cexp(z)) = Im z`,
let ROTATE2D_POLAR = prove
(`!r t s. rotate2d t (vector[r * cos(s); r * sin(s)]) =
vector[r * cos(t + s); r * sin(t + s)]`,
let ARG_ROTATE2D = prove
(`!t z. ~(z = Cx(&0)) /\ &0 <= t + Arg z /\ t + Arg z < &2 * pi
==> Arg(rotate2d t z) = t + Arg z`,
let ARG_ROTATE2D_UNIQUE = prove
(`!t a z. ~(z = Cx(&0)) /\ Arg(rotate2d t z) = a
==> ?n. integer n /\ t = &2 * n * pi + (a - Arg z)`,
REPEAT STRIP_TAC THEN
MP_TAC(last(CONJUNCTS(ISPEC `rotate2d t z`
ARG))) THEN
ASM_REWRITE_TAC[
NORM_ROTATE2D] THEN
REWRITE_TAC[
ROTATE2D_COMPLEX] THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [
ARG] THEN
ASM_REWRITE_TAC[COMPLEX_RING `a * z * b = z * c <=> z = Cx(&0) \/ a * b = c`;
CX_INJ;
COMPLEX_NORM_ZERO; GSYM
CEXP_ADD;
CEXP_EQ] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_AND THEN
REWRITE_TAC[GSYM
CX_ADD; GSYM
CX_SUB;
CX_INJ; COMPLEX_RING
`ii * t + ii * z = ii * a + n * ii <=> t = n + (a - z)`]);;
let ARG_ROTATE2D_UNIQUE_2PI = prove
(`!s t z. ~(z = Cx(&0)) /\
&0 <= s /\ s < &2 * pi /\ &0 <= t /\ t < &2 * pi /\
Arg(rotate2d s z) = Arg(rotate2d t z)
==> s = t`,
let th = prove
(`!f w z. linear f /\ (!x. norm(f x) = norm x) /\
(2 <= dimindex(:2) ==> det(matrix f) = &1)
==> f w / f z = w / z`,
let th = prove
(`!f t z. linear f /\ (!x. norm(f x) = norm x) /\
(2 <= dimindex(:2) ==> det(matrix f) = &1)
==> rotate2d t (f z) = f(rotate2d t z)`,
REWRITE_TAC[DIMINDEX_2;
LE_REFL] THEN REPEAT STRIP_TAC THEN
MP_TAC(SPEC `f:complex->complex`
ROTATION_ROTATE2D) THEN
ASM_REWRITE_TAC[
ORTHOGONAL_TRANSFORMATION] THEN
DISCH_THEN(X_CHOOSE_THEN `s:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[GSYM
ROTATE2D_ADD] THEN REWRITE_TAC[REAL_ADD_SYM]) in
add_linear_invariants [th];;
let ROTATE2D_SUB_ARG = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> rotate2d(Arg w - Arg z) = rotate2d(Arg(w / z))`,
let NULLHOMOTOPIC_ORTHOGONAL_TRANSFORMATION = prove
(`!f:real^N->real^N.
orthogonal_transformation f /\ det(matrix f) = &1
==>
homotopic_with orthogonal_transformation ((:real^N),(:real^N)) f I`,
let lemma0 = prove
(`!a x:real^N.
2 <= dimindex(:N) /\ a IN span {basis 1,basis 2}
==> reflect_along (vector[a$1; a$2]:real^2) (lambda i. x$i) =
(lambda i. reflect_along a x$i)`,
REPEAT STRIP_TAC THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; reflect_along; VECTOR_SUB_COMPONENT;
VECTOR_MUL_COMPONENT; DIMINDEX_2; FORALL_2; VECTOR_2; ARITH] THEN
CONJ_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
AP_TERM_TAC THEN BINOP_TAC THEN REWRITE_TAC[dot] THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_EQ_SUPERSET THEN
ASM_SIMP_TAC[FINITE_NUMSEG; IN_NUMSEG; FORALL_2; DIMINDEX_2; LAMBDA_BETA;
ARITH; VECTOR_2; SUBSET_NUMSEG] THEN
REWRITE_TAC[ARITH_RULE
`(1 <= i /\ i <= n) /\ ~(1 <= i /\ i <= 2) <=>
1 <= i /\ 3 <= i /\ i <= n`] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [SPAN_2]) THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
SIMP_TAC[BASIS_COMPONENT] THEN
REPEAT STRIP_TAC THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO]) THEN
ASM_ARITH_TAC) in
let lemma1 = prove
(`!a b:real^2 r.
~(a = vec 0) /\ ~(b = vec 0)
==> homotopic_with orthogonal_transformation ((:real^2),(:real^2))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN
MP_TAC(SPEC `reflect_along (a:real^2) o reflect_along b`
ROTATION_ROTATE2D) THEN
ANTS_TAC THENL
[REPEAT(FIRST_X_ASSUM(MP_TAC o
MATCH_MP ROTOINVERSION_MATRIX_REFLECT_ALONG)) THEN
REWRITE_TAC[rotoinversion_matrix] THEN
SIMP_TAC[ORTHOGONAL_MATRIX_MATRIX;
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG;
ORTHOGONAL_TRANSFORMATION_COMPOSE; MATRIX_COMPOSE;
LINEAR_REFLECT_ALONG; DET_MUL] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
ONCE_REWRITE_TAC[HOMOTOPIC_WITH_SYM] THEN
ASM_REWRITE_TAC[homotopic_with] THEN
EXISTS_TAC `\z. rotate2d (drop(fstcart z) * t) (sndcart z)` THEN
SIMP_TAC[ORTHOGONAL_TRANSFORMATION_ROTATE2D; SNDCART_PASTECART;
ETA_AX; FSTCART_PASTECART; DROP_VEC; I_THM; NORM_ROTATE2D;
REAL_MUL_LZERO; REAL_MUL_LID; SUBSET; FORALL_IN_IMAGE; IN_UNIV;
FORALL_IN_PCROSS; IN_SPHERE_0; ROTATE2D_ZERO] THEN
REWRITE_TAC[ROTATE2D_COMPLEX] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_MUL THEN
SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_SNDCART] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
REWRITE_TAC[CONTINUOUS_ON_CEXP; CX_MUL] THEN
ONCE_REWRITE_TAC[COMPLEX_RING `ii * x * t = (ii * t) * x`] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_LMUL THEN
MATCH_MP_TAC CONTINUOUS_ON_CX_DROP THEN
SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_FSTCART]]) in
let lemma2 = prove
(`!a b:real^N r.
2 <= dimindex(:N) /\
~(a = vec 0) /\ ~(b = vec 0) /\
{a,b} SUBSET span {basis 1,basis 2}
==> homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`homotopic_with orthogonal_transformation
((:real^N),(:real^N))
((\z. (lambda i. if i <= 2 then (fstcart z)$i
else (sndcart z)$i):real^N) o
(\z. pastecart
(((reflect_along (vector [(a:real^N)$1; a$2]) o
reflect_along (vector [(b:real^N)$1; b$2]))
:real^2->real^2)(fstcart z))
(sndcart z)) o
(\z:real^N. pastecart ((lambda i. z$i) :real^2) z))
((\z. (lambda i. if i <= 2 then (fstcart z)$i
else (sndcart z)$i):real^N) o
I o
(\z:real^N. pastecart ((lambda i. z$i) :real^2) z))`
MP_TAC THENL
[MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `(:real^2) PCROSS (:real^N)` THEN
REWRITE_TAC[SUBSET_UNIV] THEN CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN
ONCE_REWRITE_TAC[LINEAR_COMPONENTWISE] THEN
SIMP_TAC[LAMBDA_BETA] THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN ASM_CASES_TAC `i <= 2` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[linear; FSTCART_ADD; FSTCART_CMUL;
SNDCART_ADD; SNDCART_CMUL] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REWRITE_TAC[LIFT_ADD; LIFT_CMUL]] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^2) PCROSS (:real^N)` THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; PASTECART_IN_PCROSS] THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN
MATCH_MP_TAC LINEAR_PASTECART THEN REWRITE_TAC[LINEAR_ID] THEN
SIMP_TAC[linear; CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT]] THEN
SUBGOAL_THEN
`I = \z:real^(2,N)finite_sum. pastecart (fstcart z) (sndcart z)`
SUBST1_TAC THENL
[REWRITE_TAC[PASTECART_FST_SND; I_DEF]; ALL_TAC] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_PCROSS THEN
EXISTS_TAC `orthogonal_transformation:(real^2->real^2)->bool` THEN
EXISTS_TAC `\f:real^N->real^N. f = I` THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[GSYM I_DEF; ETA_AX] THEN MATCH_MP_TAC lemma1 THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN
REWRITE_TAC[SING_SUBSET; SPAN_2; IN_ELIM_THM; IN_UNIV] THEN
DISCH_THEN(REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
REWRITE_TAC[CART_EQ; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
DIMINDEX_2; FORALL_2; VECTOR_2] THEN
SIMP_TAC[BASIS_COMPONENT; ARITH; DIMINDEX_2; VEC_COMPONENT;
DIMINDEX_GE_1; LE_REFL] THEN
MATCH_MP_TAC(TAUT
`(r ==> q) /\ (s ==> p) ==> a /\ ~p /\ ~q ==> ~s /\ ~r`) THEN
SIMP_TAC[REAL_MUL_RZERO; REAL_MUL_LZERO; REAL_MUL_RID;
REAL_ADD_LID; REAL_ADD_RID];
REWRITE_TAC[HOMOTOPIC_WITH_REFL; SUBSET_UNIV; I_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_ID];
SIMP_TAC[o_DEF; FSTCART_PASTECART; SNDCART_PASTECART;
LAMBDA_BETA; DIMINDEX_2; ARITH; I_THM] THEN
REWRITE_TAC[ORTHOGONAL_TRANSFORMATION; NORM_EQ] THEN
X_GEN_TAC `f:real^2->real^2` THEN GEN_TAC THEN STRIP_TAC THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [linear]) THEN
SIMP_TAC[linear; CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN GEN_TAC THEN
GEN_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT];
X_GEN_TAC `v:real^N` THEN REWRITE_TAC[dot; GSYM REAL_POW_2] THEN
SUBGOAL_THEN `dimindex(:N) = 2 + (dimindex(:N) - 2)` SUBST1_TAC THENL
[ASM_ARITH_TAC; ALL_TAC] THEN
ASM_SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`] THEN
BINOP_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[dot; DIMINDEX_2; GSYM REAL_POW_2]) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(lambda i. (v:real^N)$i):real^2`) THEN
MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THEN
MATCH_MP_TAC SUM_EQ_NUMSEG THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
`2 <= n ==> !i. i <= 2 ==> i <= n`)) THEN
SIMP_TAC[LAMBDA_BETA; DIMINDEX_2];
ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> 2 + n - 2 = n`] THEN
MATCH_MP_TAC SUM_EQ_NUMSEG THEN
SIMP_TAC[ARITH_RULE `2 + 1 <= i ==> 1 <= i`;
LAMBDA_BETA; DIMINDEX_2] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_ARITH_TAC]]];
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
REWRITE_TAC[IN_UNIV; GSYM FUN_EQ_THM] THEN
SIMP_TAC[o_DEF; FSTCART_PASTECART; SNDCART_PASTECART;
LAMBDA_BETA; DIMINDEX_2; ARITH; I_THM] THEN
RULE_ASSUM_TAC(REWRITE_RULE[INSERT_SUBSET; EMPTY_SUBSET]) THEN
ASM_SIMP_TAC[lemma0] THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_2; ARITH; COND_ID] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `i:num`] THEN STRIP_TAC THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `(a:real^N)$i = &0 /\ (b:real^N)$i = &0` ASSUME_TAC THENL
[FIRST_X_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
REWRITE_TAC[SPAN_2; IN_ELIM_THM; IN_UNIV] THEN REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
BASIS_COMPONENT] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
(REAL_ARITH_TAC ORELSE ASM_ARITH_TAC);
ASM_REWRITE_TAC[reflect_along; VECTOR_SUB_COMPONENT; REAL_MUL_RZERO;
VECTOR_MUL_COMPONENT; REAL_SUB_RZERO]]]) in
let lemma3 = prove
(`!a b:real^N r.
~(a = vec 0) /\ ~(b = vec 0)
==> homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `dimindex(:N) = 1` THENL
[ASM_SIMP_TAC[o_DEF; I_DEF; REFLECT_ALONG_1D; VECTOR_NEG_NEG] THEN
REWRITE_TAC[HOMOTOPIC_WITH_REFL; SUBSET_UNIV; CONTINUOUS_ON_ID] THEN
REWRITE_TAC[ORTHOGONAL_TRANSFORMATION_ID];
FIRST_X_ASSUM(MP_TAC o MATCH_MP(ARITH_RULE
`~(n = 1) ==> 1 <= n ==> 2 <= n`)) THEN
REWRITE_TAC[DIMINDEX_GE_1] THEN DISCH_TAC] THEN
MP_TAC(ISPECL [`span{a:real^N,b}`; `span{basis 1:real^N,basis 2}`]
ORTHOGONAL_TRANSFORMATION_INTO_SUBSPACE) THEN
REWRITE_TAC[SUBSPACE_SPAN; DIM_SPAN] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[DIM_INSERT; SPAN_SING; SPAN_EMPTY;
IN_SING; DIM_EMPTY] THEN
MATCH_MP_TAC(ARITH_RULE `m <= 2 /\ n = 2 ==> m <= n`) THEN
CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
ASM_SIMP_TAC[BASIS_NONZERO; ARITH] THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
COND_CASES_TAC THEN REWRITE_TAC[] THEN
FIRST_X_ASSUM(CHOOSE_THEN (MP_TAC o AP_TERM `(\x:real^N. x$1)`)) THEN
ASM_SIMP_TAC[BASIS_COMPONENT; VECTOR_MUL_COMPONENT;
ARITH; DIMINDEX_GE_1] THEN
REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `f:real^N->real^N` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `f:real^N->real^N` ORTHOGONAL_TRANSFORMATION_INVERSE_o) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^N` STRIP_ASSUME_TAC)] THEN
SUBGOAL_THEN
`homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(g o (f o (reflect_along a o reflect_along b) o (g:real^N->real^N)) o f)
(g o (f o I o (g:real^N->real^N)) o f)`
MP_TAC THENL
[ALL_TAC;
ASM_REWRITE_TAC[o_ASSOC] THEN ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID]] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR; LINEAR_CONTINUOUS_ON] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR; LINEAR_CONTINUOUS_ON] THEN
ASM_REWRITE_TAC[I_O_ID] THEN
MP_TAC(ISPEC `f:real^N->real^N` REFLECT_ALONG_LINEAR_IMAGE) THEN
ASM_REWRITE_TAC[GSYM ORTHOGONAL_TRANSFORMATION] THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN
SUBGOAL_THEN
`!h:real^N->real^N.
orthogonal_transformation (g o h o (f:real^N->real^N)) <=>
orthogonal_transformation h`
(fun th -> REWRITE_TAC[th; ETA_AX])
THENL
[GEN_TAC THEN EQ_TAC THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE] THEN
DISCH_TAC THEN
SUBGOAL_THEN `h:real^N->real^N = f o (g o h o f) o (g:real^N->real^N)`
SUBST1_TAC THENL
[ALL_TAC; ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE]] THEN
ASM_REWRITE_TAC[o_ASSOC] THEN ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID];
ALL_TAC] THEN
SUBGOAL_THEN
`(f:real^N->real^N) o (reflect_along a o reflect_along b) o g =
reflect_along (f a) o reflect_along (f b)`
SUBST1_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN
ASM_REWRITE_TAC[o_DEF];
MATCH_MP_TAC lemma2 THEN RULE_ASSUM_TAC
(REWRITE_RULE[GSYM NORM_EQ_0; ORTHOGONAL_TRANSFORMATION]) THEN
ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
SUBSET_TRANS)) THEN
ASM_SIMP_TAC[GSYM SPAN_LINEAR_IMAGE; IMAGE_CLAUSES] THEN
REWRITE_TAC[SPAN_INC]]) in
GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MP_TAC(ISPECL [`f:real^N->real^N`; `dimindex(:N)`]
ORTHOGONAL_TRANSFORMATION_GENERATED_BY_REFLECTIONS) THEN
ASM_REWRITE_TAC[ARITH_RULE `n:num <= a + n`] THEN
DISCH_THEN(X_CHOOSE_THEN `l:(real^N)list` STRIP_ASSUME_TAC) THEN
UNDISCH_TAC `ALL (\v:real^N. ~(v = vec 0)) l` THEN
UNDISCH_TAC `orthogonal_transformation(f:real^N->real^N)` THEN
MATCH_MP_TAC(TAUT `r /\ (p /\ q ==> s) ==> r ==> p ==> q ==> s`) THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
SPEC_TAC(`l:(real^N)list`,`l:(real^N)list`) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN
WF_INDUCT_TAC `LENGTH(l:(real^N)list)` THEN POP_ASSUM MP_TAC THEN
SPEC_TAC(`l:(real^N)list`,`l:(real^N)list`) THEN
MATCH_MP_TAC list_INDUCT THEN
REWRITE_TAC[ALL; ITLIST; HOMOTOPIC_WITH_REFL] THEN
REWRITE_TAC[REWRITE_RULE[GSYM I_DEF] CONTINUOUS_ON_ID;
ORTHOGONAL_TRANSFORMATION_I; SUBSET_UNIV] THEN
X_GEN_TAC `a:real^N` THEN MATCH_MP_TAC list_INDUCT THEN
REWRITE_TAC[ALL; ITLIST; I_O_ID; DET_MATRIX_REFLECT_ALONG] THEN
REWRITE_TAC[ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG] THEN
CONJ_TAC THENL [MESON_TAC[REAL_ARITH `~(-- &1 = &1)`]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`b:real^N`; `l:(real^N)list`] THEN
REPLICATE_TAC 2 (DISCH_THEN(K ALL_TAC)) THEN
DISCH_THEN(MP_TAC o SPEC `l:(real^N)list`) THEN
REWRITE_TAC[LENGTH; ARITH_RULE `n < SUC(SUC n)`] THEN
SIMP_TAC[LINEAR_COMPOSE; LINEAR_REFLECT_ALONG; MATRIX_COMPOSE;
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG;
ORTHOGONAL_TRANSFORMATION_COMPOSE; ORTHOGONAL_TRANSFORMATION_LINEAR] THEN
DISCH_THEN(fun th ->
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN MP_TAC th) THEN
ASM_SIMP_TAC[DET_MUL; DET_MATRIX_REFLECT_ALONG; REAL_ARITH
`-- &1 * -- &1 * x = x`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] HOMOTOPIC_WITH_TRANS) THEN
GEN_REWRITE_TAC RAND_CONV [MESON[I_O_ID] `f = I o f`] THEN
REWRITE_TAC[o_ASSOC] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[LINEAR_CONTINUOUS_ON; ORTHOGONAL_TRANSFORMATION_LINEAR] THEN
ABBREV_TAC `g = ITLIST (\v:real^N h. reflect_along v o h) l I` THEN
SUBGOAL_THEN
`(\f:real^N->real^N.
orthogonal_transformation (f o g)) = orthogonal_transformation`
SUBST1_TAC THENL [ALL_TAC; MATCH_MP_TAC lemma3 THEN ASM_REWRITE_TAC[]] THEN
REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `f:real^N->real^N` THEN
EQ_TAC THEN ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE] THEN
DISCH_TAC THEN
MP_TAC(ISPEC `g:real^N->real^N` ORTHOGONAL_TRANSFORMATION_INVERSE_o) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `h:real^N->real^N` THEN
STRIP_TAC THEN
SUBGOAL_THEN `f = ((f:real^N->real^N) o (g:real^N->real^N)) o h`
SUBST1_TAC THENL
[ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID];
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE]]);;
let CTAN_ADD = prove
(`!w z. ~(ccos(w) = Cx(&0)) /\
~(ccos(z) = Cx(&0)) /\
~(ccos(w + z) = Cx(&0))
==> ctan(w + z) = (ctan w + ctan z) / (Cx(&1) - ctan(w) * ctan(z))`,
REPEAT GEN_TAC THEN REWRITE_TAC[ctan;
CSIN_ADD;
CCOS_ADD] THEN
CONV_TAC COMPLEX_FIELD);;
let CTAN_DOUBLE = prove
(`!z. ~(ccos(z) = Cx(&0)) /\ ~(ccos(Cx(&2) * z) = Cx(&0))
==> ctan(Cx(&2) * z) =
(Cx(&2) * ctan z) / (Cx(&1) - ctan(z) pow 2)`,
let CTAN_SUB = prove
(`!w z. ~(ccos(w) = Cx(&0)) /\
~(ccos(z) = Cx(&0)) /\
~(ccos(w - z) = Cx(&0))
==> ctan(w - z) = (ctan w - ctan z) / (Cx(&1) + ctan(w) * ctan(z))`,
let COMPLEX_ADD_CTAN = prove
(`!w z. ~(ccos(w) = Cx(&0)) /\
~(ccos(z) = Cx(&0))
==> ctan(w) + ctan(z) = csin(w + z) / (ccos(w) * ccos(z))`,
REWRITE_TAC[ctan;
CSIN_ADD] THEN CONV_TAC COMPLEX_FIELD);;
let COMPLEX_SUB_CTAN = prove
(`!w z. ~(ccos(w) = Cx(&0)) /\
~(ccos(z) = Cx(&0))
==> ctan(w) - ctan(z) = csin(w - z) / (ccos(w) * ccos(z))`,
REWRITE_TAC[ctan;
CSIN_SUB] THEN CONV_TAC COMPLEX_FIELD);;
let HAS_COMPLEX_DERIVATIVE_CTAN = prove
(`!z. ~(ccos z = Cx(&0))
==> (ctan
has_complex_derivative (inv(ccos(z) pow 2))) (at z)`,
REPEAT STRIP_TAC THEN
GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV) [GSYM ETA_AX] THEN
REWRITE_TAC[ctan] THEN COMPLEX_DIFF_TAC THEN
MP_TAC(SPEC `z:complex`
CSIN_CIRCLE) THEN
POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD);;
let tan_def = new_definition
`tan(x) = Re(ctan(Cx x))`;;
let TAN_ADD = prove
(`!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0) /\ ~(cos(x + y) = &0)
==> tan(x + y) = (tan(x) + tan(y)) / (&1 - tan(x) * tan(y))`,
let TAN_SUB = prove
(`!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0) /\ ~(cos(x - y) = &0)
==> tan(x - y) = (tan(x) - tan(y)) / (&1 + tan(x) * tan(y))`,
let TAN_DOUBLE = prove
(`!x. ~(cos(x) = &0) /\ ~(cos(&2 * x) = &0)
==> tan(&2 * x) = (&2 * tan(x)) / (&1 - (tan(x) pow 2))`,
let REAL_ADD_TAN = prove
(`!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0)
==> tan(x) + tan(y) = sin(x + y) / (cos(x) * cos(y))`,
let REAL_SUB_TAN = prove
(`!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0)
==> tan(x) - tan(y) = sin(x - y) / (cos(x) * cos(y))`,
let COS_TAN = prove
(`!x. abs(x) < pi / &2 ==> cos(x) = &1 / sqrt(&1 + tan(x) pow 2)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_FIELD
`sqrt(s) pow 2 = s /\ c pow 2 * s = &1 /\ ~(&1 + c * sqrt s = &0)
==> c = &1 / sqrt s`) THEN
SUBGOAL_THEN `&0 < &1 + tan x pow 2` ASSUME_TAC THENL
[MP_TAC(SPEC `tan x`
REAL_LE_SQUARE) THEN REAL_ARITH_TAC; ALL_TAC] THEN
ASM_SIMP_TAC[
SQRT_POW_2;
REAL_LT_IMP_LE] THEN CONJ_TAC THENL
[REWRITE_TAC[tan] THEN
MATCH_MP_TAC(REAL_FIELD
`s pow 2 + c pow 2 = &1 /\ &0 < c
==> c pow 2 * (&1 + (s / c) pow 2) = &1`) THEN
ASM_SIMP_TAC[
SIN_CIRCLE;
COS_POS_PI;
REAL_BOUNDS_LT];
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
ASM_SIMP_TAC[
SIN_CIRCLE;
COS_POS_PI;
REAL_BOUNDS_LT;
SQRT_POS_LT;
REAL_LT_MUL]]);;
let SIN_TAN = prove
(`!x. abs(x) < pi / &2 ==> sin(x) = tan(x) / sqrt(&1 + tan(x) pow 2)`,
let SIN_MONO_LT = prove
(`!x y. --(pi / &2) <= x /\ x < y /\ y <= pi / &2 ==> sin(x) < sin(y)`,
let SIN_MONO_LE = prove
(`!x y. --(pi / &2) <= x /\ x <= y /\ y <= pi / &2 ==> sin(x) <= sin(y)`,
let SIN_MONO_LT_EQ = prove
(`!x y. --(pi / &2) <= x /\ x <= pi / &2 /\ --(pi / &2) <= y /\ y <= pi / &2
==> (sin(x) < sin(y) <=> x < y)`,
let SIN_MONO_LE_EQ = prove
(`!x y. --(pi / &2) <= x /\ x <= pi / &2 /\ --(pi / &2) <= y /\ y <= pi / &2
==> (sin(x) <= sin(y) <=> x <= y)`,
let SIN_INJ_PI = prove
(`!x y. --(pi / &2) <= x /\ x <= pi / &2 /\
--(pi / &2) <= y /\ y <= pi / &2 /\
sin(x) = sin(y)
==> x = y`,
let COS_MONO_LE_EQ = prove
(`!x y. &0 <= x /\ x <= pi /\ &0 <= y /\ y <= pi
==> (cos(x) <= cos(y) <=> y <= x)`,
let COS_INJ_PI = prove
(`!x y. &0 <= x /\ x <= pi /\ &0 <= y /\ y <= pi /\ cos(x) = cos(y)
==> x = y`,
let TAN_MONO_LE = prove
(`!x y. --(pi / &2) < x /\ x <= y /\ y < pi / &2 ==> tan(x) <= tan(y)`,
let TAN_MONO_LT_EQ = prove
(`!x y. --(pi / &2) < x /\ x < pi / &2 /\ --(pi / &2) < y /\ y < pi / &2
==> (tan(x) < tan(y) <=> x < y)`,
let TAN_MONO_LE_EQ = prove
(`!x y. --(pi / &2) < x /\ x < pi / &2 /\ --(pi / &2) < y /\ y < pi / &2
==> (tan(x) <= tan(y) <=> x <= y)`,
let TAN_BOUND_PI2 = prove
(`!x. abs(x) < pi / &4 ==> abs(tan x) < &1`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM
TAN_PI4] THEN
REWRITE_TAC[GSYM
TAN_NEG; REAL_ARITH `abs(x) < a <=> --a < x /\ x < a`] THEN
CONJ_TAC THEN MATCH_MP_TAC
TAN_MONO_LT THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
let SIN_PI6_STRADDLE = prove
(`!a b. &0 <= a /\ a <= b /\ b <= &4 /\
sin(a / &6) <= &1 / &2 /\ &1 / &2 <= sin(b / &6)
==> a <= pi /\ pi <= b`,
let CLOG_WORKS = prove
(`!z. ~(z = Cx(&0))
==> cexp(clog z) = z /\ --pi < Im(clog z) /\ Im(clog z) <= pi`,
let CLOG_EQ = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0)) ==> (clog w = clog z <=> w = z)`,
let RE_CLOG = prove
(`!z. ~(z = Cx(&0)) ==> Re(clog z) = log(norm z)`,
REPEAT STRIP_TAC THEN FIRST_X_ASSUM
(MP_TAC o AP_TERM `norm:complex->real` o MATCH_MP
CEXP_CLOG) THEN
REWRITE_TAC[
NORM_CEXP] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
LOG_EXP]);;
let CX_LOG = prove
(`!z. &0 < z ==> Cx(log z) = clog(Cx z)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(fun th ->
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
[SYM(MATCH_MP
EXP_LOG th)]) THEN
REWRITE_TAC[
CX_EXP] THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
CLOG_CEXP THEN REWRITE_TAC[
IM_CX] THEN
MP_TAC
PI_POS THEN REAL_ARITH_TAC);;
let RE_CLOG_POS_LT = prove
(`!z. ~(z = Cx(&0)) ==> (abs(Im(clog z)) < pi / &2 <=> &0 < Re(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th])
MP_TAC) THEN
SIMP_TAC[
RE_CEXP;
REAL_LT_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> --(p / &2) < x /\ x < p / &2 \/
--(p / &2) <= p + x /\ p + x <= p / &2 \/
--(p / &2) <= x - p /\ x - p <= p / &2`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
COS_ADD;
COS_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let RE_CLOG_POS_LE = prove
(`!z. ~(z = Cx(&0)) ==> (abs(Im(clog z)) <= pi / &2 <=> &0 <= Re(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th])
MP_TAC) THEN
SIMP_TAC[
RE_CEXP;
REAL_LE_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> --(p / &2) <= x /\ x <= p / &2 \/
--(p / &2) < p + x /\ p + x < p / &2 \/
--(p / &2) < x - p /\ x - p < p / &2`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
COS_ADD;
COS_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let IM_CLOG_POS_LT = prove
(`!z. ~(z = Cx(&0)) ==> (&0 < Im(clog z) /\ Im(clog z) < pi <=> &0 < Im(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th])
MP_TAC) THEN
SIMP_TAC[
IM_CEXP;
REAL_LT_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> &0 < x /\ x < p \/
&0 <= x + p /\ x + p <= p \/
&0 <= x - p /\ x - p <= p`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
SIN_ADD;
SIN_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let IM_CLOG_POS_LE = prove
(`!z. ~(z = Cx(&0)) ==> (&0 <= Im(clog z) <=> &0 <= Im(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th])
MP_TAC) THEN
SIMP_TAC[
IM_CEXP;
REAL_LE_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> &0 <= x /\ x <= p \/
&0 < x + p /\ x + p < p \/
&0 < p - x /\ p - x < p`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
SIN_ADD;
SIN_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let CNJ_CLOG = prove
(`!z. (Im z = &0 ==> &0 < Re z) ==> cnj(clog z) = clog(cnj z)`,
let CLOG_INV = prove
(`!z. (Im(z) = &0 ==> &0 < Re z) ==> clog(inv z) = --(clog z)`,
let CNJ_CSQRT = prove
(`!z. (Im z = &0 ==> &0 <= Re(z)) ==> cnj(csqrt z) = csqrt(cnj z)`,
let CPOW_0 = prove
(`!z. Cx(&0) cpow z = Cx(&0)`,
REWRITE_TAC[cpow]);;
let CPOW_N = prove
(`!z. z cpow (Cx(&n)) = if z = Cx(&0) then Cx(&0) else z pow n`,
GEN_TAC THEN REWRITE_TAC[cpow] THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[
CEXP_N;
CEXP_CLOG]);;
let CPOW_EQ_0 = prove
(`!w z. w cpow z = Cx(&0) <=> w = Cx(&0)`,
REPEAT GEN_TAC THEN REWRITE_TAC[cpow] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
CEXP_NZ]);;
let CPOW_MUL_REAL = prove
(`!x y z. real x /\ real y /\ &0 <= Re x /\ &0 <= Re y
==> (x * y) cpow z = x cpow z * y cpow z`,
let CLOG_MUL = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> clog(w * z) =
if Im(clog w + clog z) <= --pi then
(clog(w) + clog(z)) + ii * Cx(&2 * pi)
else if Im(clog w + clog z) > pi then
(clog(w) + clog(z)) - ii * Cx(&2 * pi)
else clog(w) + clog(z)`,
let CLOG_MUL_SIMPLE = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0)) /\
--pi < Im(clog(w)) + Im(clog(z)) /\
Im(clog(w)) + Im(clog(z)) <= pi
==> clog(w * z) = clog(w) + clog(z)`,
let CLOG_NEG = prove
(`!z. ~(z = Cx(&0))
==> clog(--z) = if Im(z) <= &0 /\ ~(Re(z) < &0 /\ Im(z) = &0)
then clog(z) + ii * Cx(pi)
else clog(z) - ii * Cx(pi)`,
REPEAT STRIP_TAC THEN
SUBST1_TAC(SIMPLE_COMPLEX_ARITH `--z = --Cx(&1) * z`) THEN
ASM_SIMP_TAC[
CLOG_MUL; COMPLEX_RING `~(--Cx(&1) = Cx(&0))`] THEN
REWRITE_TAC[
CLOG_NEG_1;
IM_ADD;
IM_MUL_II;
RE_CX] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH
`--p < x /\ x <= p ==> ~(p + x <= --p)`] THEN
REWRITE_TAC[REAL_ARITH `p + x > p <=> &0 < x`] THEN
ASM_SIMP_TAC[GSYM
IM_CLOG_EQ_PI] THEN
ONCE_REWRITE_TAC[REAL_ARITH `Im z <= &0 <=> ~(&0 < Im z)`] THEN
ASM_SIMP_TAC[GSYM
IM_CLOG_POS_LT] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH `x <= p ==> (x < p <=> ~(x = p))`] THEN
REWRITE_TAC[TAUT `~(a /\ ~b) /\ ~b <=> ~a /\ ~b`] THEN
ASM_CASES_TAC `Im(clog z) = pi` THEN ASM_REWRITE_TAC[
PI_POS] THEN
ASM_CASES_TAC `&0 < Im(clog z)` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
CX_MUL] THEN CONV_TAC COMPLEX_RING);;
let CLOG_MUL_II = prove
(`!z. ~(z = Cx(&0))
==> clog(ii * z) = if &0 <= Re(z) \/ Im(z) < &0
then clog(z) + ii * Cx(pi / &2)
else clog(z) - ii * Cx(&3 * pi / &2)`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[
CLOG_MUL;
II_NZ;
CLOG_II] THEN
REWRITE_TAC[
IM_ADD;
IM_MUL_II;
RE_CX] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH
`--p < x /\ x <= p ==> ~(p / &2 + x <= --p)`] THEN
REWRITE_TAC[REAL_ARITH `p / &2 + x > p <=> p / &2 < x`] THEN
REWRITE_TAC[REAL_ARITH `Im z < &0 <=> ~(&0 <= Im z)`] THEN
ASM_SIMP_TAC[GSYM
RE_CLOG_POS_LE; GSYM
IM_CLOG_POS_LE] THEN
MATCH_MP_TAC(MESON[]
`(p <=> ~q) /\ x = a /\ y = b
==> ((if p then x else y) = (if q then b else a))`) THEN
CONJ_TAC THENL
[MP_TAC
PI_POS THEN REAL_ARITH_TAC;
REWRITE_TAC[
CX_MUL;
CX_DIV] THEN CONV_TAC COMPLEX_RING]);;
let CLOG_MUL_UNWINDING = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> clog(w * z) =
clog(w) + clog(z) -
Cx(&2 * pi) * ii * unwinding(clog w + clog z)`,
let CTAN_CATN = prove
(`!z. ~(z pow 2 = --Cx(&1)) ==> ctan(catn z) = z`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[catn; ctan; csin; ccos;
COMPLEX_RING `--i * i / Cx(&2) * z = --(i * i) / Cx(&2) * z`;
COMPLEX_RING `i * i / Cx(&2) * z = (i * i) / Cx(&2) * z`] THEN
REWRITE_TAC[
COMPLEX_POW_II_2; GSYM
COMPLEX_POW_2] THEN
REWRITE_TAC[COMPLEX_RING `--Cx(&1) / Cx(&2) * x = --(Cx(&1) / Cx(&2) * x)`;
CEXP_NEG] THEN
SUBGOAL_THEN
`~(cexp(Cx(&1) / Cx(&2) *
(clog((Cx(&1) - ii * z) / (Cx(&1) + ii * z)))) pow 2 = --Cx(&1))`
ASSUME_TAC THENL
[REWRITE_TAC[GSYM
CEXP_N;
CEXP_SUB; COMPLEX_RING
`Cx(&2) * Cx(&1) / Cx(&2) * z = z`] THEN
ASM_SIMP_TAC[
CEXP_CLOG;
COMPLEX_POW_II_2;
COMPLEX_FIELD `~(w = Cx(&0)) /\ ~(z = Cx(&0)) ==> ~(w / z = Cx(&0))`;
COMPLEX_FIELD `~(w = Cx(&0)) ==> (x / w = y <=> x = y * w)`;
COMPLEX_FIELD
`ii pow 2 = --Cx(&1) /\ ~(z pow 2 = --Cx(&1))
==> ~(Cx(&1) - ii * z = Cx(&0)) /\ ~(Cx(&1) + ii * z = Cx(&0))`] THEN
POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD;
ALL_TAC] THEN
REWRITE_TAC[COMPLEX_RING `-- --Cx (&1) / Cx (&2) = Cx(&1) / Cx(&2)`] THEN
ASM_SIMP_TAC[
CEXP_NZ; COMPLEX_FIELD
`~(z = Cx(&0)) /\ ~(z pow 2 = --Cx(&1))
==> ((inv(z) - z) / (Cx(&2) * ii)) / ((inv(z) + z) / Cx(&2)) =
inv ii * ((Cx(&1) - z pow 2) / (Cx(&1) + z pow 2))`] THEN
ASM_SIMP_TAC[GSYM
CEXP_N;
CEXP_SUB;
COMPLEX_RING `Cx(&2) * Cx(&1) / Cx(&2) * z = z`] THEN
ASM_SIMP_TAC[
CEXP_CLOG; COMPLEX_FIELD
`~(z pow 2 = --Cx(&1))
==> ~((Cx(&1) - ii * z) / (Cx(&1) + ii * z) = Cx(&0))`] THEN
UNDISCH_TAC `~(z pow 2 = --Cx(&1))` THEN CONV_TAC COMPLEX_FIELD);;
let CATN_CTAN = prove
(`!z. abs(Re z) < pi / &2 ==> catn(ctan z) = z`,
REPEAT STRIP_TAC THEN REWRITE_TAC[catn; ctan; csin; ccos] THEN
ASM_SIMP_TAC[COMPLEX_FIELD
`ii * (a / (Cx(&2) * ii)) / (b / Cx(&2)) = a / b`] THEN
SIMP_TAC[COMPLEX_FIELD
`ii / Cx(&2) * x = y <=> x = Cx(&2) * --(ii * y)`] THEN
SUBGOAL_THEN `~(cexp(ii * z) pow 2 = --Cx(&1))` ASSUME_TAC THENL
[SUBGOAL_THEN `--Cx(&1) = cexp(ii * Cx pi)` SUBST1_TAC THENL
[REWRITE_TAC[
CEXP_EULER; GSYM
CX_SIN; GSYM
CX_COS;
SIN_PI;
COS_PI] THEN
CONV_TAC COMPLEX_RING;
ALL_TAC] THEN
REWRITE_TAC[GSYM
CEXP_N;
CEXP_EQ] THEN
DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[
IM_MUL_CX;
IM_MUL_II;
IM_ADD;
RE_CX;
IM_II;
REAL_MUL_RID] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(z) < p / &2 /\ (w = &0 \/ abs(w) >= &2 * p)
==> ~(&2 * z = p + w)`) THEN
ASM_REWRITE_TAC[
REAL_ABS_MUL;
REAL_ABS_PI;
REAL_ABS_NUM] THEN
SIMP_TAC[
real_ge; REAL_MUL_ASSOC;
REAL_LE_RMUL_EQ;
PI_POS] THEN
REWRITE_TAC[
REAL_ENTIRE;
PI_NZ] THEN
MP_TAC(SPEC `n:real`
REAL_ABS_INTEGER_LEMMA) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
ASM_SIMP_TAC[
CEXP_NEG;
CEXP_NZ;
COMPLEX_MUL_LNEG; COMPLEX_FIELD
`~(w = Cx(&0)) /\ ~(w pow 2 = --Cx(&1))
==> (Cx(&1) - (w - inv w) / (w + inv w)) /
(Cx(&1) + (w - inv w) / (w + inv w)) =
inv(w) pow 2`] THEN
REWRITE_TAC[GSYM
CEXP_N; GSYM
CEXP_NEG] THEN
MATCH_MP_TAC
CLOG_CEXP THEN REWRITE_TAC[
IM_MUL_CX;
IM_NEG;
IM_MUL_II] THEN
ASM_REAL_ARITH_TAC]);;
let RE_CATN_BOUNDS = prove
(`!z. (Re z = &0 ==> abs(Im z) < &1) ==> abs(Re(catn z)) < pi / &2`,
REWRITE_TAC[catn;
complex_div; GSYM
CX_INV; GSYM
COMPLEX_MUL_ASSOC] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
RE_MUL_II;
IM_MUL_CX] THEN
MATCH_MP_TAC(REAL_ARITH `abs x < p ==> abs(--(inv(&2) * x)) < p / &2`) THEN
MATCH_MP_TAC(REAL_ARITH `(--p < x /\ x <= p) /\ ~(x = p) ==> abs x < p`) THEN
SUBGOAL_THEN `~(z = ii) /\ ~(z = --ii)` STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN
DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN SUBST1_TAC th) THEN
REWRITE_TAC[
RE_II;
IM_II;
RE_NEG;
IM_NEG] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[GSYM
complex_div] THEN CONJ_TAC THENL
[SUBGOAL_THEN `~((Cx(&1) - ii * z) / (Cx(&1) + ii * z) = Cx(&0))`
(fun th -> MESON_TAC[th;
CLOG_WORKS]) THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
ALL_TAC] THEN
DISCH_TAC THEN
MP_TAC(ISPEC `clog((Cx(&1) - ii * z) / (Cx(&1) + ii * z))`
EULER) THEN
ASM_REWRITE_TAC[
SIN_PI;
COS_PI;
CX_NEG] THEN
REWRITE_TAC[COMPLEX_RING
`x = y * (--Cx(&1) + z * Cx(&0)) <=> x + y = Cx(&0)`] THEN
REWRITE_TAC[
CX_EXP] THEN
ASM_SIMP_TAC[
CEXP_CLOG; COMPLEX_FIELD
`~(z = ii) /\ ~(z = --ii)
==> ~((Cx(&1) - ii * z) / (Cx(&1) + ii * z) = Cx(&0))`] THEN
REWRITE_TAC[GSYM
CX_EXP] THEN DISCH_THEN(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[
IM_ADD;
IM_CX;
REAL_ADD_RID;
IM_COMPLEX_DIV_LEMMA] THEN
DISCH_TAC THEN UNDISCH_TAC `Re z = &0 ==> abs (Im z) < &1` THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `ii * z = --Cx(Im z)` SUBST_ALL_TAC THENL
[ASM_REWRITE_TAC[
COMPLEX_EQ;
RE_NEG;
IM_NEG;
RE_MUL_II;
IM_MUL_II;
RE_CX;
IM_CX;
REAL_NEG_0];
ALL_TAC] THEN
UNDISCH_TAC
`Im(clog((Cx(&1) - --Cx(Im z)) / (Cx(&1) + --Cx(Im z)))) = pi` THEN
REWRITE_TAC[
COMPLEX_SUB_RNEG; GSYM
complex_sub] THEN
REWRITE_TAC[GSYM
CX_ADD; GSYM
CX_SUB; GSYM
CX_DIV] THEN
SUBGOAL_THEN `&0 < (&1 + Im z) / (&1 - Im z)` ASSUME_TAC THENL
[MATCH_MP_TAC
REAL_LT_DIV THEN ASM_REAL_ARITH_TAC;
ASM_SIMP_TAC[GSYM
CX_LOG;
IM_CX;
PI_NZ]]);;
let ATN_TAN = prove
(`!y. tan(atn y) = y`,
GEN_TAC THEN REWRITE_TAC[
tan_def; atn] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC `Re(ctan(catn(Cx y)))` THEN
CONJ_TAC THENL [REWRITE_TAC[GSYM
CX_ATN;
RE_CX]; ALL_TAC] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
RE_CX] THEN AP_TERM_TAC THEN
MATCH_MP_TAC
CTAN_CATN THEN MATCH_MP_TAC(COMPLEX_RING
`~(z = ii) /\ ~(z = --ii) ==> ~(z pow 2 = --Cx(&1))`) THEN
CONJ_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[
IM_II;
IM_CX;
IM_NEG] THEN REAL_ARITH_TAC);;
let TAN_ATN = prove
(`!x. --(pi / &2) < x /\ x < pi / &2 ==> atn(tan(x)) = x`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
tan_def; atn] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC `Re(catn(ctan(Cx x)))` THEN
CONJ_TAC THENL [REWRITE_TAC[GSYM
CX_TAN;
RE_CX]; ALL_TAC] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
RE_CX] THEN AP_TERM_TAC THEN
MATCH_MP_TAC
CATN_CTAN THEN REWRITE_TAC[
RE_CX] THEN
ASM_REAL_ARITH_TAC);;
let ATN_1 = prove
(`atn(&1) = pi / &4`,
MP_TAC(AP_TERM `atn`
TAN_PI4) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC
TAN_ATN THEN MP_TAC
PI_POS THEN REAL_ARITH_TAC);;
let ATN_NEG = prove
(`!x. atn(--x) = --(atn x)`,
GEN_TAC THEN MP_TAC(SPEC `atn(x)`
TAN_NEG) THEN REWRITE_TAC[
ATN_TAN] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC
TAN_ATN THEN
MP_TAC(SPEC `x:real`
ATN_BOUNDS) THEN REAL_ARITH_TAC);;
let ATN_LT_PI4 = prove
(`!x. abs(x) < &1 ==> abs(atn x) < pi / &4`,
GEN_TAC THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 < x ==> &0 < y) /\
(x < &0 ==> y < &0) /\
((x = &0) ==> (y = &0)) /\
(x < a ==> y < b) /\
(--a < x ==> --b < y)
==> abs(x) < a ==> abs(y) < b`) THEN
SIMP_TAC[
ATN_LT_PI4_POS;
ATN_LT_PI4_NEG;
ATN_0] THEN CONJ_TAC THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM
ATN_0] THEN
SIMP_TAC[
ATN_MONO_LT]);;
let TAN_SEC = prove
(`!x. ~(cos(x) = &0) ==> (&1 + (tan(x) pow 2) = inv(cos x) pow 2)`,
let TAN_ABS_GE_X = prove
(`!x. abs(x) < pi / &2 ==> abs(x) <= abs(tan x)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `abs(atn(tan x))` THEN REWRITE_TAC[
ATN_ABS_LE_X] THEN
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
TAN_ATN THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
let ABS_SQUARE_EQ_1 = prove
(`!x. x pow 2 = &1 <=> abs(x) = &1`,
REWRITE_TAC[REAL_RING `x pow 2 = &1 <=> x = &1 \/ x = -- &1`] THEN
REAL_ARITH_TAC);;
let CASN_BODY_LEMMA = prove
(`!z. ~(ii * z + csqrt(Cx(&1) - z pow 2) = Cx(&0))`,
GEN_TAC THEN MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN
CONV_TAC COMPLEX_FIELD);;
let CASN_CSIN = prove
(`!z. abs(Re z) < pi / &2 \/ (abs(Re z) = pi / &2 /\ Im z = &0)
==> casn(csin z) = z`,
let CASN_UNIQUE = prove
(`!w z. csin(z) = w /\
(abs(Re z) < pi / &2 \/ (abs(Re z) = pi / &2 /\ Im z = &0))
==> casn w = z`,
let CACS_BODY_LEMMA = prove
(`!z. ~(z + ii * csqrt(Cx(&1) - z pow 2) = Cx(&0))`,
GEN_TAC THEN MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN
CONV_TAC COMPLEX_FIELD);;
let CACS_CCOS = prove
(`!z. &0 < Re z /\ Re z < pi \/
Re(z) = &0 /\ &0 <= Im(z) \/
Re(z) = pi /\ Im(z) <= &0
==> cacs(ccos z) = z`,
let CACS_UNIQUE = prove
(`!w z.
ccos z = w /\
(&0 < Re z /\ Re z < pi \/
Re(z) = &0 /\ &0 <= Im(z) \/
Re(z) = pi /\ Im(z) <= &0)
==> cacs(w) = z`,
let RE_CASN = prove
(`!z. Re(casn z) = Im(clog(ii * z + csqrt(Cx(&1) - z pow 2)))`,
let RE_CACS = prove
(`!z. Re(cacs z) = Im(clog(z + ii * csqrt(Cx(&1) - z pow 2)))`,
let CCOS_CASN_NZ = prove
(`!z. ~(z pow 2 = Cx(&1)) ==> ~(ccos(casn z) = Cx(&0))`,
REWRITE_TAC[ccos; casn;
CEXP_NEG; COMPLEX_RING `ii * --ii * z = z`;
COMPLEX_RING `--ii * --ii * z = --z`] THEN
SIMP_TAC[
CEXP_CLOG;
CASN_BODY_LEMMA;
COMPLEX_FIELD `~(x = Cx(&0))
==> ((x + inv(x)) / Cx(&2) = Cx(&0) <=>
x pow 2 = --Cx(&1))`] THEN
SIMP_TAC[
CSQRT; COMPLEX_FIELD
`s pow 2 = Cx(&1) - z pow 2
==> ((ii * z + s) pow 2 = --Cx(&1) <=>
ii * s * z = Cx(&1) - z pow 2)`] THEN
GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC(COMPLEX_RING
`~(x pow 2 + y pow 2 = Cx(&0)) ==> ~(ii * x = y)`) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN CONV_TAC COMPLEX_RING);;
let CSIN_CACS_NZ = prove
(`!z. ~(z pow 2 = Cx(&1)) ==> ~(csin(cacs z) = Cx(&0))`,
REWRITE_TAC[csin; cacs;
CEXP_NEG; COMPLEX_RING `ii * --ii * z = z`;
COMPLEX_RING `--ii * --ii * z = --z`] THEN
SIMP_TAC[
CEXP_CLOG;
CACS_BODY_LEMMA;
COMPLEX_FIELD `~(x = Cx(&0))
==> ((x - inv(x)) / (Cx(&2) * ii) = Cx(&0) <=>
x pow 2 = Cx(&1))`] THEN
SIMP_TAC[
CSQRT; COMPLEX_FIELD
`s pow 2 = Cx(&1) - z pow 2
==> ((z + ii * s) pow 2 = Cx(&1) <=>
ii * s * z = Cx(&1) - z pow 2)`] THEN
GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC(COMPLEX_RING
`~(x pow 2 + y pow 2 = Cx(&0)) ==> ~(ii * x = y)`) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN CONV_TAC COMPLEX_RING);;
let CCOS_CSIN_CSQRT = prove
(`!z. &0 < cos(Re z) \/ cos(Re z) = &0 /\ Im(z) * sin(Re z) <= &0
==> ccos(z) = csqrt(Cx(&1) - csin(z) pow 2)`,
let CSIN_CCOS_CSQRT = prove
(`!z. &0 < sin(Re z) \/ sin(Re z) = &0 /\ &0 <= Im(z) * cos(Re z)
==> csin(z) = csqrt(Cx(&1) - ccos(z) pow 2)`,
let CASN_CACS_SQRT_POS = prove
(`!z. (&0 < Re z \/ Re z = &0 /\ &0 <= Im z)
==> casn(z) = cacs(csqrt(Cx(&1) - z pow 2))`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[casn; cacs] THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(COMPLEX_RING `w = z ==> ii * z + s = s + ii * w`) THEN
MATCH_MP_TAC
CSQRT_UNIQUE THEN
ASM_REWRITE_TAC[
CSQRT] THEN CONV_TAC COMPLEX_RING);;
let CACS_CASN_SQRT_POS = prove
(`!z. (&0 < Re z \/ Re z = &0 /\ &0 <= Im z)
==> cacs(z) = casn(csqrt(Cx(&1) - z pow 2))`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[casn; cacs] THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(COMPLEX_RING `w = z ==> z + ii * s = ii * s + w`) THEN
MATCH_MP_TAC
CSQRT_UNIQUE THEN
ASM_REWRITE_TAC[
CSQRT] THEN CONV_TAC COMPLEX_RING);;
let CSIN_CACS = prove
(`!z. &0 < Re z \/ Re(z) = &0 /\ &0 <= Im z
==> csin(cacs z) = csqrt(Cx(&1) - z pow 2)`,
GEN_TAC THEN DISCH_TAC THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
CSIN_CASN] THEN
AP_TERM_TAC THEN MATCH_MP_TAC
CACS_CASN_SQRT_POS THEN
ASM_REWRITE_TAC[]);;
let CCOS_CASN = prove
(`!z. &0 < Re z \/ Re(z) = &0 /\ &0 <= Im z
==> ccos(casn z) = csqrt(Cx(&1) - z pow 2)`,
GEN_TAC THEN DISCH_TAC THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
CCOS_CACS] THEN
AP_TERM_TAC THEN MATCH_MP_TAC
CASN_CACS_SQRT_POS THEN
ASM_REWRITE_TAC[]);;
let SIN_ASN = prove
(`!y. --(&1) <= y /\ y <= &1 ==> sin(asn(y)) = y`,
REWRITE_TAC[REAL_ARITH `--(&1) <= y /\ y <= &1 <=> abs(y) <= &1`] THEN
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ASN;
CX_SIN;
CSIN_CASN]);;
let ASN_SIN = prove
(`!x. --(pi / &2) <= x /\ x <= pi / &2 ==> asn(sin(x)) = x`,
let ASN_BOUNDS_LT = prove
(`!y. --(&1) < y /\ y < &1 ==> --(pi / &2) < asn(y) /\ asn(y) < pi / &2`,
GEN_TAC THEN REWRITE_TAC[asn] THEN
MP_TAC(SPEC `Cx y`
CASN_BOUNDS) THEN
REWRITE_TAC[
RE_CX] THEN REAL_ARITH_TAC);;
let ASN_BOUNDS = prove
(`!y. --(&1) <= y /\ y <= &1 ==> --(pi / &2) <= asn(y) /\ asn(y) <= pi / &2`,
let ASN_NEG = prove
(`!x. -- &1 <= x /\ x <= &1 ==> asn(--x) = --asn(x)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
[GSYM(MATCH_MP
SIN_ASN th)]) THEN
REWRITE_TAC[GSYM
SIN_NEG] THEN MATCH_MP_TAC
ASN_SIN THEN
REWRITE_TAC[REAL_ARITH `--a <= --x /\ --x <= a <=> --a <= x /\ x <= a`] THEN
ASM_SIMP_TAC[
ASN_BOUNDS]);;
let COS_ASN_NZ = prove
(`!x. --(&1) < x /\ x < &1 ==> ~(cos(asn(x)) = &0)`,
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ASN;
CX_COS;
REAL_ARITH `--(&1) < x /\ x < &1 ==> abs(x) <= &1`] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
CCOS_CASN_NZ THEN
SIMP_TAC[COMPLEX_RING `x pow 2 = Cx(&1) <=> x = Cx(&1) \/ x = --Cx(&1)`] THEN
REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
ASM_REAL_ARITH_TAC);;
let ASN_MONO_LT_EQ = prove
(`!x y. abs(x) <= &1 /\ abs(y) <= &1 ==> (asn(x) < asn(y) <=> x < y)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `sin(asn(x)) < sin(asn(y))` THEN CONJ_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SIN_MONO_LT_EQ THEN
ONCE_REWRITE_TAC[
CONJ_ASSOC] THEN CONJ_TAC THEN MATCH_MP_TAC
ASN_BOUNDS;
BINOP_TAC THEN MATCH_MP_TAC
SIN_ASN] THEN
ASM_REAL_ARITH_TAC);;
let COS_ASN = prove
(`!x. --(&1) <= x /\ x <= &1 ==> cos(asn x) = sqrt(&1 - x pow 2)`,
let COS_ACS = prove
(`!y. --(&1) <= y /\ y <= &1 ==> cos(acs(y)) = y`,
REWRITE_TAC[REAL_ARITH `--(&1) <= y /\ y <= &1 <=> abs(y) <= &1`] THEN
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ACS;
CX_COS;
CCOS_CACS]);;
let ACS_BOUNDS_LT = prove
(`!y. --(&1) < y /\ y < &1 ==> &0 < acs(y) /\ acs(y) < pi`,
GEN_TAC THEN REWRITE_TAC[acs] THEN
MP_TAC(SPEC `Cx y`
CACS_BOUNDS) THEN
REWRITE_TAC[
RE_CX] THEN REAL_ARITH_TAC);;
let ACS_NEG = prove
(`!x. -- &1 <= x /\ x <= &1 ==> acs(--x) = pi - acs(x)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
[GSYM(MATCH_MP
COS_ACS th)]) THEN
ONCE_REWRITE_TAC[GSYM
COS_NEG] THEN REWRITE_TAC[GSYM
COS_PERIODIC_PI] THEN
REWRITE_TAC[REAL_ARITH `--x + y:real = y - x`] THEN MATCH_MP_TAC
ACS_COS THEN
SIMP_TAC[REAL_ARITH `&0 <= p - x /\ p - x <= p <=> &0 <= x /\ x <= p`] THEN
ASM_SIMP_TAC[
ACS_BOUNDS]);;
let SIN_ACS_NZ = prove
(`!x. --(&1) < x /\ x < &1 ==> ~(sin(acs(x)) = &0)`,
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ACS;
CX_SIN;
REAL_ARITH `--(&1) < x /\ x < &1 ==> abs(x) <= &1`] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
CSIN_CACS_NZ THEN
SIMP_TAC[COMPLEX_RING `x pow 2 = Cx(&1) <=> x = Cx(&1) \/ x = --Cx(&1)`] THEN
REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
ASM_REAL_ARITH_TAC);;
let ACS_MONO_LT_EQ = prove
(`!x y. abs(x) <= &1 /\ abs(y) <= &1 ==> (acs(x) < acs(y) <=> y < x)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `cos(acs(y)) < cos(acs(x))` THEN CONJ_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC
COS_MONO_LT_EQ THEN
ONCE_REWRITE_TAC[
CONJ_ASSOC] THEN CONJ_TAC THEN MATCH_MP_TAC
ACS_BOUNDS;
BINOP_TAC THEN MATCH_MP_TAC
COS_ACS] THEN
ASM_REAL_ARITH_TAC);;
let ACS_MONO_LT = prove
(`!x y. --(&1) <= x /\ x < y /\ y <= &1 ==> acs(y) < acs(x)`,
REPEAT GEN_TAC THEN
MP_TAC(SPECL [`y:real`; `x:real`]
ACS_MONO_LT_EQ) THEN
REAL_ARITH_TAC);;
let ACS_MONO_LE = prove
(`!x y. --(&1) <= x /\ x <= y /\ y <= &1 ==> acs(y) <= acs(x)`,
REPEAT GEN_TAC THEN
MP_TAC(SPECL [`y:real`; `x:real`]
ACS_MONO_LE_EQ) THEN
REAL_ARITH_TAC);;
let SIN_ACS = prove
(`!x. --(&1) <= x /\ x <= &1 ==> sin(acs x) = sqrt(&1 - x pow 2)`,
let ACS_INJ = prove
(`!x y. abs(x) <= &1 /\ abs(y) <= &1 ==> (acs x = acs y <=> x = y)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
ASM_SIMP_TAC[
ACS_MONO_LE_EQ] THEN REAL_ARITH_TAC);;
let ACS_ATN = prove
(`!x. -- &1 < x /\ x < &1 ==> acs(x) = pi / &2 - atn(x / sqrt(&1 - x pow 2))`,
let ASN_ACS = prove
(`!x. -- &1 <= x /\ x <= &1 ==> asn(x) = pi / &2 - acs(x)`,
let ACS_ASN = prove
(`!x. -- &1 <= x /\ x <= &1 ==> acs(x) = pi / &2 - asn(x)`,
SIMP_TAC[
ASN_ACS] THEN REAL_ARITH_TAC);;
let ASN_ATN = prove
(`!x. -- &1 < x /\ x < &1 ==> asn(x) = atn(x / sqrt(&1 - x pow 2))`,
let ASN_ACS_SQRT_NEG = prove
(`!x. -- &1 <= x /\ x <= &0 ==> asn(x) = --acs(sqrt(&1 - x pow 2))`,
REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `x = --y <=> (--x:real) = y`] THEN
ASM_SIMP_TAC[GSYM
ASN_NEG; REAL_ARITH `x <= &0 ==> x <= &1`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `(x:real) pow 2 = (--x) pow 2`] THEN
MATCH_MP_TAC
ASN_ACS_SQRT_POS THEN ASM_REAL_ARITH_TAC);;
let ACS_ASN_SQRT_NEG = prove
(`!x. -- &1 <= x /\ x <= &0 ==> acs(x) = pi - asn(sqrt(&1 - x pow 2))`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `--x:real`
ACS_ASN_SQRT_POS) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; SIMP_TAC[
REAL_POW_NEG; ARITH]] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM
REAL_NEG_NEG] THEN
MATCH_MP_TAC
ACS_NEG THEN ASM_REAL_ARITH_TAC);;
let LIM_POWN = prove
(`!z. norm(z) < &1 ==> ((\n. z pow n) --> Cx(&0)) sequentially`,
let COMPLEX_ROOT_POLYFUN = prove
(`!n z a.
1 <= n
==> (z pow n = a <=>
vsum(0..n) (\i. (if i = 0 then --a else if i = n then Cx(&1)
else Cx(&0)) * z pow i) = Cx(&0))`,
let COMPLEX_ROOT_UNITY_EQ = prove
(`!n j k. ~(n = 0)
==> (cexp(Cx(&2) * Cx pi * ii * Cx(&j / &n)) =
cexp(Cx(&2) * Cx pi * ii * Cx(&k / &n)) <=> (j == k) (mod n))`,
let CONTINUOUS_WITHIN_UPPERHALF_ARG = prove
(`!z. ~(z = Cx(&0))
==> (Cx o Arg) continuous (at z) within {z | &0 <= Im z}`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `real z /\ &0 <= Re z` THEN
ASM_SIMP_TAC[
CONTINUOUS_AT_ARG;
CONTINUOUS_AT_WITHIN] THEN
FIRST_X_ASSUM(CONJUNCTS_THEN2
(ASSUME_TAC o GEN_REWRITE_RULE I [real]) MP_TAC) THEN
SUBGOAL_THEN `~(Re z = &0)` ASSUME_TAC THENL
[DISCH_TAC THEN UNDISCH_TAC `~(z = Cx(&0))` THEN
ASM_REWRITE_TAC[
COMPLEX_EQ;
RE_CX;
IM_CX];
GEN_REWRITE_TAC LAND_CONV [
REAL_LE_LT]] THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPEC `rotate2d (pi / &2) z`
CONTINUOUS_AT_ARG) THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[
ROTATE2D_PI2; real;
IM_MUL_II]; ALL_TAC] THEN
REWRITE_TAC[
continuous_at;
continuous_within] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
REWRITE_TAC[
o_THM; dist; GSYM
CX_SUB;
COMPLEX_NORM_CX] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[
IN_ELIM_THM] THEN
X_GEN_TAC `w:complex` THEN STRIP_TAC THEN
SUBGOAL_THEN `Arg z = &0` ASSUME_TAC THENL
[ASM_SIMP_TAC[
ARG_EQ_0; real;
REAL_LT_IMP_LE]; ALL_TAC] THEN
ASM_CASES_TAC `Arg w = &0` THEN
ASM_REWRITE_TAC[
REAL_SUB_REFL;
REAL_ABS_NUM] THEN
SUBGOAL_THEN `&0 < Arg w` ASSUME_TAC THENL
[ASM_REWRITE_TAC[
ARG;
REAL_LT_LE]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `rotate2d (pi / &2) w`) THEN
ASM_REWRITE_TAC[GSYM
ROTATE2D_SUB;
NORM_ROTATE2D] THEN
MP_TAC(ISPECL [`pi / &2`; `z:complex`]
ARG_ROTATE2D) THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN MP_TAC
PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[
REAL_ADD_RID] THEN
MATCH_MP_TAC(REAL_ARITH
`w' = p + w ==> abs(w' - p) < e ==> abs(w - &0) < e`) THEN
MATCH_MP_TAC
ARG_ROTATE2D THEN CONJ_TAC THENL
[DISCH_TAC THEN UNDISCH_TAC `&0 < Arg w` THEN
ASM_REWRITE_TAC[
Arg_DEF;
REAL_LT_REFL];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
ARG_LE_PI]) THEN
MP_TAC(SPEC `w:complex`
ARG) THEN REAL_ARITH_TAC]);;
let ROOT_1 = prove
(`!n. ~(n = 0) ==> root n (&1) = &1`,
SIMP_TAC[root;
REAL_POS;
REAL_POW_EQ_1;
CONJ_ASSOC] THEN
REWRITE_TAC[REAL_ARITH `&0 <= u /\ abs u = &1 <=> u = &1`] THEN
SIMP_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
CONV_TAC REAL_RAT_REDUCE_CONV);;
let ROOT_2 = prove
(`!x. root 2 x = sqrt x`,
GEN_TAC THEN REWRITE_TAC[sqrt; root] THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `y:real` THEN
ASM_CASES_TAC `x:real = y pow 2` THEN
ASM_REWRITE_TAC[REAL_POW_2;
REAL_LE_SQUARE] THEN REAL_ARITH_TAC);;
let ROOT_WORKS = prove
(`!n x.
ODD n \/ ~(n = 0) /\ &0 <= x
==> (&0 <= x ==> &0 <= root n x) /\ (root n x) pow n = x`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
REWRITE_TAC[root] THEN CONV_TAC SELECT_CONV THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(REAL_ARITH `x = &0 \/ &0 < x \/ &0 < --x`)
THENL
[EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[
REAL_POW_ZERO];
EXISTS_TAC `exp(log x / &n)` THEN REWRITE_TAC[
REAL_EXP_POS_LE] THEN
ASM_SIMP_TAC[GSYM
REAL_EXP_N;
REAL_DIV_LMUL; REAL_OF_NUM_EQ;
EXP_LOG];
FIRST_X_ASSUM(DISJ_CASES_THEN ASSUME_TAC) THENL
[ALL_TAC; ASM_REAL_ARITH_TAC] THEN
EXISTS_TAC `--exp(log(--x) / &n)` THEN REWRITE_TAC[
REAL_POW_NEG] THEN
ASM_SIMP_TAC[GSYM
NOT_ODD; REAL_ARITH `&0 < --x ==> ~(&0 <= x)`] THEN
ASM_SIMP_TAC[GSYM
REAL_EXP_N;
REAL_DIV_LMUL; REAL_OF_NUM_EQ;
EXP_LOG;
REAL_NEG_NEG]]);;
let ROOT_UNIQUE = prove
(`!n x y. y pow n = x /\ (
ODD n \/ ~(n = 0) /\ &0 <= y) ==> root n x = y`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
UNDISCH_THEN `(y:real) pow n = x` (SUBST_ALL_TAC o SYM) THEN
MATCH_MP_TAC
REAL_ROOT_POW THEN ASM_REWRITE_TAC[]);;
let REAL_ROOT_MUL = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y
==> root n (x * y) = root n x * root n y`,
let REAL_ROOT_DIV = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y
==> root n (x / y) = root n x / root n y`,
let ROOT_MONO_LT = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ x < y ==> root n x < root n y`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 <= x /\ &0 <= y ==> (v <= u ==> y <= x))
==> &0 <= x /\ x < y ==> u < v`) THEN
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(root n y) pow n <= (root n x) pow n` MP_TAC THENL
[MATCH_MP_TAC
REAL_POW_LE2 THEN ASM_SIMP_TAC[
ROOT_POS_LE];
ASM_SIMP_TAC[
REAL_POW_ROOT]]);;
let ROOT_INJ = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y ==> (root n x = root n y <=> x = y)`,
let REAL_ROOT_LE = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y
==> (root n x <= y <=> x <= y pow n)`,
let REAL_LE_ROOT = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y
==> (x <= root n y <=> x pow n <= y)`,
let LOG_ROOT = prove
(`!n x. ~(n = 0) /\ &0 < x ==> log(root n x) = log x / &n`,
let ROOT_EXP_LOG = prove
(`!n x. ~(n = 0) /\ &0 < x ==> root n x = exp(log x / &n)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
ROOT_POS_LT) THEN
REWRITE_TAC[GSYM
REAL_EXP_LOG] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
AP_TERM_TAC THEN ASM_SIMP_TAC[
LOG_ROOT]);;
let rpow = new_definition
`x rpow y = if &0 < x then exp(y * log x)
else if x = &0 then if y = &0 then &1 else &0
else if ?m n. ODD(m) /\ ODD(n) /\ (abs y = &m / &n)
then --(exp(y * log(--x)))
else exp(y * log(--x))`;;let RPOW_POW = prove
(`!x n. x rpow &n = x pow n`,
REPEAT GEN_TAC THEN REWRITE_TAC[rpow] THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[
REAL_EXP_N;
EXP_LOG] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_POW_ZERO; REAL_OF_NUM_EQ] THEN
ASM_SIMP_TAC[
EXP_LOG; REAL_ARITH `~(&0 < x) /\ ~(x = &0) ==> &0 < --x`] THEN
REWRITE_TAC[
REAL_POW_NEG;
REAL_ABS_NUM] THEN
SUBGOAL_THEN `(?p q.
ODD(p) /\
ODD(q) /\ &n = &p / &q) <=>
ODD n`
(fun th -> SIMP_TAC[th; GSYM
NOT_ODD;
REAL_NEG_NEG;
COND_ID]) THEN
EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[REPEAT GEN_TAC THEN ASM_CASES_TAC `q = 0` THEN
ASM_REWRITE_TAC[
ARITH_ODD] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
`~(q = &0) ==> (n = p / q <=> q * n = p)`] THEN
REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
ASM_MESON_TAC[
ODD_MULT];
DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`n:num`; `1`] THEN
ASM_REWRITE_TAC[
REAL_DIV_1;
ARITH_ODD]]);;
let RPOW_LT2 = prove
(`!x y z. &0 <= x /\ x < y /\ &0 < z ==> x rpow z < y rpow z`,
let RPOW_LE2 = prove
(`!x y z. &0 <= x /\ x <= y /\ &0 <= z ==> x rpow z <= y rpow z`,
let RPOW_LNEG = prove
(`!x y. --x rpow y =
if ?m n.
ODD m /\
ODD n /\ abs y = &m / &n
then --(x rpow y) else x rpow y`,
let RPOW_EQ_0 = prove
(`!x y. x rpow y = &0 <=> x = &0 /\ ~(y = &0)`,
REPEAT GEN_TAC THEN REWRITE_TAC[rpow] THEN
ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[
REAL_LT_REFL] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_NEG_EQ_0;
REAL_EXP_NZ]) THEN
REAL_ARITH_TAC);;
let RPOW_ADD = prove
(`!x y z. &0 < x ==> x rpow (y + z) = x rpow y * x rpow z`,
let RPOW_ADD_ALT = prove
(`!x y z. &0 <= x /\ (x = &0 /\ y + z = &0 ==> y = &0 \/ z = &0)
==> x rpow (y + z) = x rpow y * x rpow z`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[
REAL_LE_LT;
RPOW_ADD] THEN
REWRITE_TAC[
RPOW_ZERO] THEN
ASM_CASES_TAC `y = &0` THEN
ASM_REWRITE_TAC[REAL_MUL_LID; REAL_ADD_LID] THEN
ASM_CASES_TAC `y + z = &0` THEN ASM_REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC);;
let RPOW_SQRT = prove
(`!x. &0 <= x ==> x rpow (&1 / &2) = sqrt x`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(REAL_RING
`x pow 2 = y pow 2 /\ (x + y = &0 ==> x = &0 /\ y = &0)
==> x = y`) THEN
CONJ_TAC THENL
[ASM_SIMP_TAC[
SQRT_POW_2] THEN
ASM_SIMP_TAC[GSYM
RPOW_POW;
RPOW_RPOW] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
REWRITE_TAC[
RPOW_POW;
REAL_POW_1];
MATCH_MP_TAC(REAL_ARITH
`&0 <= x /\ &0 <= y ==> x + y = &0 ==> x = &0 /\ y = &0`) THEN
ASM_SIMP_TAC[
SQRT_POS_LE;
RPOW_POS_LE]]);;
let REAL_ROOT_RPOW = prove
(`!n x. ~(n = 0) /\ (&0 <= x \/
ODD n) ==> root n x = x rpow (inv(&n))`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
ASM_SIMP_TAC[
ROOT_0;
RPOW_ZERO;
REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN
ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
[ASM_SIMP_TAC[
ROOT_EXP_LOG; rpow;
REAL_LT_LE] THEN AP_TERM_TAC THEN
REAL_ARITH_TAC;
ASM_REWRITE_TAC[rpow] THEN COND_CASES_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
REAL_ABS_INV;
REAL_ABS_NUM] THEN
REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[ARITH]] THEN
MATCH_MP_TAC
ROOT_UNIQUE THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; GSYM
REAL_EXP_N; GSYM
NOT_ODD] THEN
ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
`~(n = &0) ==> n * &1 / n * x = x`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `--x:real = y <=> x = --y`] THEN
MATCH_MP_TAC
EXP_LOG THEN ASM_REAL_ARITH_TAC]);;