(* ========================================================================= *)
(* Results intended for Flyspeck. *)
(* ========================================================================= *)
needs "Multivariate/polytope.ml";;
needs "Multivariate/realanalysis.ml";;
needs "Multivariate/geom.ml";;
needs "Multivariate/cross.ml";;
prioritize_vector();;
(* ------------------------------------------------------------------------- *)
(* Not really Flyspeck-specific but needs both angles and cross products. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Other miscelleneous lemmas. *)
(* ------------------------------------------------------------------------- *)
let NOT_COPLANAR_0_4_IMP_INDEPENDENT = prove
(`!v1 v2 v3:real^N. ~coplanar {vec 0,v1,v2,v3} ==> independent {v1,v2,v3}`,
REPEAT GEN_TAC THEN REWRITE_TAC[independent; CONTRAPOS_THM] THEN
REWRITE_TAC[dependent] THEN
SUBGOAL_THEN
`!v1 v2 v3:real^N. v1
IN span {v2,v3} ==> coplanar{vec 0,v1,v2,v3}`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[coplanar] THEN
MAP_EVERY EXISTS_TAC [`vec 0:real^N`; `v2:real^N`; `v3:real^N`] THEN
SIMP_TAC[
AFFINE_HULL_EQ_SPAN;
HULL_INC;
IN_INSERT] THEN
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET] THEN
ASM_SIMP_TAC[
SPAN_SUPERSET;
IN_INSERT] THEN
POP_ASSUM MP_TAC THEN SPEC_TAC(`v1:real^N`,`v1:real^N`) THEN
REWRITE_TAC[GSYM
SUBSET] THEN MATCH_MP_TAC
SPAN_MONO THEN SET_TAC[];
REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPECL [`v1:real^N`; `v2:real^N`; `v3:real^N`]);
FIRST_X_ASSUM(MP_TAC o SPECL [`v2:real^N`; `v3:real^N`; `v1:real^N`]);
FIRST_X_ASSUM(MP_TAC o SPECL [`v3:real^N`; `v1:real^N`; `v2:real^N`])]
THEN REWRITE_TAC[
INSERT_AC] THEN DISCH_THEN MATCH_MP_TAC THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`a
IN s ==> s
SUBSET t ==> a
IN t`)) THEN
MATCH_MP_TAC
SPAN_MONO THEN SET_TAC[]]);;
let COPLANAR_SCALE_ALL = prove
(`!a b c x y z.
~(a = &0) /\ ~(b = &0) /\ ~(c = &0)
==> (coplanar {vec 0,a % x,b % y,c % z} <=> coplanar {vec 0,x,y,z})`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[
COPLANAR_SPECIAL_SCALE] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN
ASM_SIMP_TAC[
COPLANAR_SPECIAL_SCALE] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN
ASM_SIMP_TAC[
COPLANAR_SPECIAL_SCALE]);;
let DROPOUT_BASIS_3 = prove
(`(dropout 3:real^3->real^2) (basis 1) = basis 1 /\
(dropout 3:real^3->real^2) (basis 2) = basis 2 /\
(dropout 3:real^3->real^2) (basis 3) = vec 0`,
let SLICE_DROPOUT_3 = prove
(`!P t. slice 3 t {x | P((dropout 3:real^3->real^2) x)} = {x | P x}`,
REPEAT GEN_TAC THEN REWRITE_TAC[slice] THEN
REWRITE_TAC[
EXTENSION;
IN_IMAGE;
IN_ELIM_THM;
IN_INTER] THEN
X_GEN_TAC `y:real^2` THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
DISCH_TAC THEN EXISTS_TAC `(pushin 3 t:real^2->real^3) y` THEN
ASM_SIMP_TAC[DIMINDEX_2; DIMINDEX_3;
DROPOUT_PUSHIN; ARITH] THEN
SIMP_TAC[pushin;
LAMBDA_BETA;
LT_REFL; DIMINDEX_3; ARITH]);;
let FORALL_PAD2D3D_THM = prove
(`!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))`,
GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[pad2d3d] THEN
SIMP_TAC[
LAMBDA_BETA; DIMINDEX_3; ARITH;
LT_REFL];
FIRST_X_ASSUM(MP_TAC o SPEC `(lambda i. (y:real^3)$i):real^2`) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
SIMP_TAC[
CART_EQ; pad2d3d; DIMINDEX_3; ARITH;
LAMBDA_BETA; DIMINDEX_2;
ARITH_RULE `i < 3 <=> i <= 2`] THEN
REWRITE_TAC[ARITH_RULE `i <= 3 <=> i <= 2 \/ i = 3`] THEN
ASM_MESON_TAC[]]);;
let QUANTIFY_PAD2D3D_THM = prove
(`(!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))) /\
(!P. (?y:real^3. y$3 = &0 /\ P y) <=> (?x. P(pad2d3d x)))`,
REWRITE_TAC[MESON[] `(?y. P y) <=> ~(!x. ~P x)`] THEN
REWRITE_TAC[GSYM
FORALL_PAD2D3D_THM] THEN MESON_TAC[]);;
let INJECTIVE_PAD2D3D = prove
(`!x y. pad2d3d x = pad2d3d y ==> x = y`,
SIMP_TAC[
CART_EQ; pad2d3d;
LAMBDA_BETA; DIMINDEX_3; DIMINDEX_2] THEN
REWRITE_TAC[ARITH_RULE `i < 3 <=> i <= 2`] THEN
MESON_TAC[ARITH_RULE `i <= 2 ==> i <= 3`]);;
let PLANE_LINEAR_IMAGE_EQ = prove
(`!f:real^M->real^N p.
linear f /\ (!x y. f x = f y ==> x = y)
==> (plane(
IMAGE f p) <=> plane p)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[plane] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`?u. u
IN IMAGE f (:real^M) /\
?v. v
IN IMAGE f (:real^M) /\
?w. w
IN IMAGE (f:real^M->real^N) (:real^M) /\
~collinear {u, v, w} /\
IMAGE f p = affine hull {u, v, w}` THEN
CONJ_TAC THENL
[REWRITE_TAC[
RIGHT_AND_EXISTS_THM;
IN_IMAGE;
IN_UNIV] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `{u,v,w}
SUBSET IMAGE (f:real^M->real^N) p` MP_TAC THENL
[ASM_REWRITE_TAC[
HULL_SUBSET]; SET_TAC[]];
REWRITE_TAC[
EXISTS_IN_IMAGE;
IN_UNIV] THEN
REWRITE_TAC[SET_RULE `{f a,f b,f c} =
IMAGE f {a,b,c}`] THEN
ASM_SIMP_TAC[
AFFINE_HULL_LINEAR_IMAGE] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN BINOP_TAC THENL
[ASM_MESON_TAC[
COLLINEAR_LINEAR_IMAGE_EQ]; ASM SET_TAC[]]]);;
let ROTATION_PLANE_HORIZONTAL = prove
(`!s. plane s
==> ?a f.
orthogonal_transformation f /\ det(matrix f) = &1 /\
IMAGE f (
IMAGE (\x. a + x) s) = {z:real^3 | z$3 = &0}`,
let lemma = prove
(`span {z:real^3 | z$3 = &0} = {z:real^3 | z$3 = &0}`,
REWRITE_TAC[SPAN_EQ_SELF; subspace; IN_ELIM_THM] THEN
SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT;
DIMINDEX_3; ARITH] THEN REAL_ARITH_TAC) in
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [plane]) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`; `c:real^3`] THEN
MAP_EVERY (fun t ->
ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
ALL_TAC])
[`a:real^3 = b`; `a:real^3 = c`; `b:real^3 = c`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC) THEN
ASM_SIMP_TAC[AFFINE_HULL_INSERT_SPAN; IN_INSERT; NOT_IN_EMPTY] THEN
EXISTS_TAC `--a:real^3` THEN
REWRITE_TAC[SET_RULE `IMAGE (\x:real^3. --a + x) {a + x | x | x IN s} =
IMAGE (\x. --a + a + x) s`] THEN
REWRITE_TAC[VECTOR_ARITH `--a + a + x:real^3 = x`; IMAGE_ID] THEN
REWRITE_TAC[SET_RULE `{x - a:real^x | x = b \/ x = c} = {b - a,c - a}`] THEN
MP_TAC(ISPEC `span{b - a:real^3,c - a}`
ROTATION_LOWDIM_HORIZONTAL) THEN
REWRITE_TAC[DIMINDEX_3] THEN ANTS_TAC THENL
[MATCH_MP_TAC LET_TRANS THEN
EXISTS_TAC `CARD{b - a:real^3,c - a}` THEN
SIMP_TAC[DIM_SPAN; DIM_LE_CARD; FINITE_RULES] THEN
SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:real^3->real^3` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
ASM_SIMP_TAC[GSYM SPAN_LINEAR_IMAGE] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM lemma] THEN
MATCH_MP_TAC DIM_EQ_SPAN THEN CONJ_TAC THENL
[ASM_MESON_TAC[IMAGE_SUBSET; SPAN_INC; SUBSET_TRANS]; ALL_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2` THEN CONJ_TAC THENL
[MP_TAC(ISPECL [`{z:real^3 | z$3 = &0}`; `(:real^3)`] DIM_EQ_SPAN) THEN
REWRITE_TAC[SUBSET_UNIV; DIM_UNIV; DIMINDEX_3; lemma] THEN
MATCH_MP_TAC(TAUT `~r /\ (~p ==> q) ==> (q ==> r) ==> p`) THEN
REWRITE_TAC[ARITH_RULE `~(x <= 2) <=> 3 <= x`] THEN
REWRITE_TAC[EXTENSION; SPAN_UNIV; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `vector[&0;&0;&1]:real^3`) THEN
REWRITE_TAC[IN_UNIV; VECTOR_3] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `dim {b - a:real^3,c - a}` THEN
CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[LE_REFL; DIM_INJECTIVE_LINEAR_IMAGE;
ORTHOGONAL_TRANSFORMATION_INJECTIVE]] THEN
MP_TAC(ISPEC `{b - a:real^3,c - a}` INDEPENDENT_BOUND_GENERAL) THEN
SIMP_TAC[CARD_CLAUSES; FINITE_RULES; IN_SING; NOT_IN_EMPTY] THEN
ASM_REWRITE_TAC[VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`; ARITH] THEN
DISCH_THEN MATCH_MP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE (RAND_CONV o RAND_CONV)
[SET_RULE `{a,b,c} = {b,a,c}`]) THEN
REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
REWRITE_TAC[independent; CONTRAPOS_THM; dependent] THEN
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; RIGHT_OR_DISTRIB] THEN
REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {a,b} DELETE b = {a}`;
SET_RULE `~(a = b) ==> {a,b} DELETE a = {b}`;
VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`] THEN
REWRITE_TAC[SPAN_BREAKDOWN_EQ; SPAN_EMPTY; IN_SING] THEN
ONCE_REWRITE_TAC[VECTOR_SUB_EQ] THEN MESON_TAC[COLLINEAR_LEMMA; INSERT_AC]);;
let COPLANAR_DET_EQ_0 = prove
(`!v0 v1 (v2: real^3) v3.
coplanar {v0,v1,v2,v3} <=>
det(vector[v1 - v0; v2 - v0; v3 - v0]) = &0`,
let AFFSIGN = prove
(`affsign sgn s t =
{y | ?f. y = vsum (s
UNION t) (\v. f v % v) /\
(!w. w
IN t ==> sgn(f w)) /\
sum (s
UNION t) f = &1}`,
let AFFSIGN_INJECTIVE_LINEAR_IMAGE = prove
(`!f:real^M->real^N sgn s t v.
linear f /\ (!x y. f x = f y ==> x = y)
==> (affsign sgn (
IMAGE f s) (
IMAGE f t) =
IMAGE f (affsign sgn s t))`,
let lemma0 = prove
(`vsum s (\x. u x % x) = vsum {x | x IN s /\ ~(u x = &0)} (\x. u x % x)`,
MATCH_MP_TAC VSUM_SUPERSET THEN SIMP_TAC[SUBSET; IN_ELIM_THM] THEN
REWRITE_TAC[TAUT `p /\ ~(p /\ ~q) <=> p /\ q`] THEN
SIMP_TAC[o_THM; VECTOR_MUL_LZERO]) in
let lemma1 = prove
(`!f:real^M->real^N s.
linear f /\ (!x y. f x = f y ==> x = y)
==> (sum(IMAGE f s) u = &1 /\ vsum(IMAGE f s) (\x. u x % x) = y <=>
sum s (u o f) = &1 /\ f(vsum s (\x. (u o f) x % x)) = y)`,
REPEAT STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o funpow 3 lhand o snd) THEN
ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN
MATCH_MP_TAC(MESON[] `(p ==> z = x) ==> (p /\ x = y <=> p /\ z = y)`) THEN
DISCH_TAC THEN ONCE_REWRITE_TAC[lemma0] THEN
SUBGOAL_THEN
`{y | y IN IMAGE (f:real^M->real^N) s /\ ~(u y = &0)} =
IMAGE f {x | x IN s /\ ~(u(f x) = &0)}`
SUBST1_TAC THENL [ASM SET_TAC[]; CONV_TAC SYM_CONV] THEN
SUBGOAL_THEN `FINITE {x | x IN s /\ ~(u((f:real^M->real^N) x) = &0)}`
ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE
(LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN
ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
REWRITE_TAC[GSYM sum; support; NEUTRAL_REAL_ADD; o_THM] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ];
W(MP_TAC o PART_MATCH (lhs o rand) VSUM_IMAGE o lhand o snd) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
ASM_SIMP_TAC[LINEAR_VSUM; o_DEF; GSYM LINEAR_CMUL]]) in
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[EXTENSION; IN_AFFSIGN] THEN
REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_AFFSIGN] THEN
REWRITE_TAC[GSYM IMAGE_UNION] THEN
FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP lemma1 th]) THEN
X_GEN_TAC `y:real^N` THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `vsum (s UNION t) (\x. (u o (f:real^M->real^N)) x % x)` THEN
ASM_REWRITE_TAC[] THEN
EXISTS_TAC `(u:real^N->real) o (f:real^M->real^N)` THEN
ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[o_THM];
MP_TAC(ISPEC `f:real^M->real^N` LINEAR_INJECTIVE_LEFT_INVERSE) THEN
ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^M` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^M`
(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^M->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(u:real^M->real) o (g:real^N->real^M)` THEN
ASM_REWRITE_TAC[o_DEF; ETA_AX]]);;
let IN_AFFSIGN_TRANSLATION = prove
(`!sgn s t a v:real^N.
affsign sgn s t v
==> affsign sgn (
IMAGE (\x. a + x) s) (
IMAGE (\x. a + x) t) (a + v)`,
REPEAT GEN_TAC THEN REWRITE_TAC[affsign;
lin_combo] THEN
ONCE_REWRITE_TAC[SET_RULE `(!x. s x ==> p x) <=> (!x. x
IN s ==> p x)`] THEN
DISCH_THEN(X_CHOOSE_THEN `f:real^N->real`
(CONJUNCTS_THEN2 SUBST_ALL_TAC STRIP_ASSUME_TAC)) THEN
EXISTS_TAC `\x. (f:real^N->real)(x - a)` THEN
ASM_REWRITE_TAC[GSYM
IMAGE_UNION] THEN REPEAT CONJ_TAC THENL
[ALL_TAC;
ASM_REWRITE_TAC[
FORALL_IN_IMAGE; ETA_AX;
VECTOR_ARITH `(a + x) - a:real^N = x`];
W(MP_TAC o PART_MATCH (lhs o rand)
SUM_IMAGE o lhs o snd) THEN
SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
ASM_REWRITE_TAC[
o_DEF;
VECTOR_ADD_SUB; ETA_AX]] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`a + vsum {x | x
IN s
UNION t /\ ~(f x = &0)} (\v:real^N. f v % v)` THEN
CONJ_TAC THENL
[AP_TERM_TAC THEN MATCH_MP_TAC
VSUM_SUPERSET THEN
REWRITE_TAC[
VECTOR_MUL_EQ_0;
SUBSET;
IN_ELIM_THM] THEN MESON_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `vsum (
IMAGE (\x:real^N. a + x)
{x | x
IN s
UNION t /\ ~(f x = &0)})
(\v. f(v - a) % v)` THEN
CONJ_TAC THENL
[ALL_TAC;
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
VSUM_SUPERSET THEN
CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[
IMP_CONJ;
FORALL_IN_IMAGE;
VECTOR_MUL_EQ_0] THEN
REWRITE_TAC[
VECTOR_ADD_SUB] THEN SET_TAC[]] THEN
SUBGOAL_THEN `
FINITE {x:real^N | x
IN s
UNION t /\ ~(f x = &0)}`
ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE
(LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN
ONCE_REWRITE_TAC[
ITERATE_EXPAND_CASES] THEN
REWRITE_TAC[GSYM sum; support;
NEUTRAL_REAL_ADD] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ;
ARITH_EQ];
ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
VSUM_IMAGE o rhs o snd) THEN
ASM_SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[
o_DEF;
VECTOR_ADD_SUB] THEN
ASM_SIMP_TAC[
VECTOR_ADD_LDISTRIB;
VSUM_ADD] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[
VSUM_RMUL] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
VECTOR_MUL_LID] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC
SUM_SUPERSET THEN SET_TAC[]);;
let AFF_GE_1_1 = prove
(`!x v w.
DISJOINT {x} {v}
==> aff_ge {x} {v} =
{y | ?t1 t2.
&0 <= t2 /\
t1 + t2 = &1 /\
y = t1 % x + t2 % v }`,
AFF_TAC);;
let AFF_GE_1_2 = prove
(`!x v w.
DISJOINT {x} {v,w}
==> aff_ge {x} {v,w} =
{y | ?t1 t2 t3.
&0 <= t2 /\ &0 <= t3 /\
t1 + t2 + t3 = &1 /\
y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GE_2_1 = prove
(`!x v w.
DISJOINT {x,v} {w}
==> aff_ge {x,v} {w} =
{y | ?t1 t2 t3.
&0 <= t3 /\
t1 + t2 + t3 = &1 /\
y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GT_1_1 = prove
(`!x v w.
DISJOINT {x} {v}
==> aff_gt {x} {v} =
{y | ?t1 t2.
&0 < t2 /\
t1 + t2 = &1 /\
y = t1 % x + t2 % v}`,
AFF_TAC);;
let AFF_GT_1_2 = prove
(`!x v w.
DISJOINT {x} {v,w}
==> aff_gt {x} {v,w} =
{y | ?t1 t2 t3.
&0 < t2 /\ &0 < t3 /\
t1 + t2 + t3 = &1 /\
y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GT_2_1 = prove
(`!x v w.
DISJOINT {x,v} {w}
==> aff_gt {x,v} {w} =
{y | ?t1 t2 t3.
&0 < t3 /\
t1 + t2 + t3 = &1 /\
y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GT_3_1 = prove
(`!v w x y.
DISJOINT {v,w,x} {y}
==> aff_gt {v,w,x} {y} =
{z | ?t1 t2 t3 t4.
&0 < t4 /\
t1 + t2 + t3 + t4 = &1 /\
z = t1 % v + t2 % w + t3 % x + t4 % y}`,
AFF_TAC);;
let AFF_LT_1_1 = prove
(`!x v.
DISJOINT {x} {v}
==> aff_lt {x} {v} =
{y | ?t1 t2.
t2 < &0 /\
t1 + t2 = &1 /\
y = t1 % x + t2 % v}`,
AFF_TAC);;
let AFF_LT_2_1 = prove
(`!x v w.
DISJOINT {x,v} {w}
==> aff_lt {x,v} {w} =
{y | ?t1 t2 t3.
t3 < &0 /\
t1 + t2 + t3 = &1 /\
y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GE_1_2_0 = prove
(`!v w.
~(v = vec 0) /\ ~(w = vec 0)
==> aff_ge {vec 0} {v,w} = {a % v + b % w | &0 <= a /\ &0 <= b}`,
SIMP_TAC[
AFF_GE_1_2;
SET_RULE `
DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
ONCE_REWRITE_TAC[MESON[]
`(?a b c. P b c /\ Q b c /\ R a b c /\ S b c) <=>
(?b c. P b c /\ Q b c /\ S b c /\ ?a. R a b c)`] THEN
REWRITE_TAC[REAL_ARITH `t + s:real = &1 <=> t = &1 - s`;
EXISTS_REFL] THEN
SET_TAC[]);;
let AFF_GE_2_1_0 = prove
(`!v w.
DISJOINT {vec 0, v} {w}
==> aff_ge {vec 0, v} {w} = {s % v + t % w |s,t| &0 <= t}`,
SIMP_TAC[
AFF_GE_2_1;
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> q /\ p /\ r`] THEN
ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
REWRITE_TAC[REAL_ARITH `t + u = &1 <=> t = &1 - u`;
UNWIND_THM2] THEN
SET_TAC[]);;
let CONVEX_AFFSIGN = prove
(`!sgn. (!x y u. sgn(x) /\ sgn(y) /\ &0 <= u /\ u <= &1
==> sgn((&1 - u) * x + u * y))
==> !s t:real^N->bool. convex(affsign sgn s t)`,
let AFF_GE_0_N = prove
(`!s:real^N->bool.
FINITE s /\ ~(vec 0
IN s)
==> aff_ge {vec 0} s =
{y | ?u. (!x. x
IN s ==> &0 <= u x) /\
y = vsum s (\x. u x % x)}`,
let CONIC_AFF_GE_0 = prove
(`!s:real^N->bool.
FINITE s /\ ~(vec 0
IN s) ==> conic(aff_ge {vec 0} s)`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[
AFF_GE_0_N; conic] THEN
REWRITE_TAC[
IN_ELIM_THM] THEN GEN_TAC THEN X_GEN_TAC `c:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\v. c * (u:real^N->real) v` THEN
REWRITE_TAC[GSYM
VECTOR_MUL_ASSOC;
VSUM_LMUL] THEN
ASM_MESON_TAC[
REAL_LE_MUL]);;
let ANGLES_ADD_AFF_GE = prove
(`!u v w x:real^N.
~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x
IN aff_ge {u} {v,w}
==> angle(v,u,x) + angle(x,u,w) = angle(v,u,w)`,
let AFF_GE_2_1_0_DROPOUT_3 = prove
(`!w z:real^3.
~collinear{vec 0,basis 3,z}
==> (w
IN aff_ge {vec 0,basis 3} {z} <=>
(dropout 3 w)
IN aff_ge {vec 0:real^2} {dropout 3 z})`,
let AFF_GE_2_1_0_SEMIALGEBRAIC = prove
(`!x y z:real^3.
~collinear {vec 0,x,y} /\ ~collinear {vec 0,x,z}
==> (z
IN aff_ge {vec 0,x} {y} <=>
(x cross y) cross x cross z = vec 0 /\
&0 <= (x cross z) dot (x cross y))`,
let HALFLINE_EXPLICIT = prove
(`!x y:real^N.
aff_ge {x} {y} =
{z | ?t1 t2. &0 <= t2 /\ t1 + t2 = &1 /\ z = t1 % x + t2 % y}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^N = y` THENL
[ASM_REWRITE_TAC[
HALFLINE_REFL]; AFF_TAC] THEN
REWRITE_TAC[REAL_ARITH `x + y = &1 <=> x = &1 - y`] THEN
REWRITE_TAC[VECTOR_ARITH `(&1 - x) % v + x % v:real^N = v`;
MESON[] `(?x y. P y /\ x = f y /\ Q x y) <=> (?y. P y /\ Q (f y) y)`] THEN
REWRITE_TAC[
IN_ELIM_THM;
IN_SING;
EXTENSION] THEN MESON_TAC[
REAL_POS]);;
let HALFLINE = prove
(`!x y:real^N.
aff_ge {x} {y} =
{z | ?t. &0 <= t /\ z = (&1 - t) % x + t % y}`,
REWRITE_TAC[
HALFLINE_EXPLICIT; REAL_ARITH `x + y = &1 <=> x = &1 - y`] THEN
SET_TAC[]);;
let orthonormal = new_definition
`orthonormal e1 e2 e3 <=>
e1 dot e1 = &1 /\ e2 dot e2 = &1 /\ e3 dot e3 = &1 /\
e1 dot e2 = &0 /\ e1 dot e3 = &0 /\ e2 dot e3 = &0 /\
&0 < (e1 cross e2) dot e3`;;let ORTHONORMAL_LINEAR_IMAGE = prove
(`!f. linear(f) /\ (!x. norm(f x) = norm x) /\
(2 <= dimindex(:3) ==> det(matrix f) = &1)
==> !e1 e2 e3. orthonormal (f e1) (f e2) (f e3) <=>
orthonormal e1 e2 e3`,
let ORTHONORMAL_PERMUTE = prove
(`!e1 e2 e3. orthonormal e1 e2 e3 ==> orthonormal e2 e3 e1`,
REWRITE_TAC[orthonormal] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[GSYM
CROSS_TRIPLE] THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
DOT_SYM] THEN ASM_REWRITE_TAC[]);;
let ORTHONORMAL_CROSS = prove
(`!e1 e2 e3.
orthonormal e1 e2 e3
==> e2 cross e3 = e1 /\ e3 cross e1 = e2 /\ e1 cross e2 = e3`,
SUBGOAL_THEN
`!e1 e2 e3. orthonormal e1 e2 e3 ==> e3 cross e1 = e2`
(fun th -> MESON_TAC[th;
ORTHONORMAL_PERMUTE]) THEN
GEOM_BASIS_MULTIPLE_TAC 1 `e1:real^3` THEN X_GEN_TAC `k:real` THEN
REWRITE_TAC[orthonormal;
DOT_LMUL;
DOT_RMUL] THEN
SIMP_TAC[
DOT_BASIS_BASIS; DIMINDEX_3; ARITH;
REAL_MUL_RID] THEN
REWRITE_TAC[REAL_RING `k * k = &1 <=> k = &1 \/ k = -- &1`] THEN
ASM_CASES_TAC `k = -- &1` THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ASM_CASES_TAC `k = &1` THEN
ASM_REWRITE_TAC[
VECTOR_MUL_LID; REAL_MUL_LID;
REAL_MUL_RID] THEN
SIMP_TAC[cross;
DOT_3;
VECTOR_3;
CART_EQ;
FORALL_3; DIMINDEX_3;
BASIS_COMPONENT; DIMINDEX_3; ARITH;
REAL_POS] THEN
REWRITE_TAC[
REAL_MUL_LZERO;
REAL_SUB_RZERO;
REAL_ADD_RID;
REAL_MUL_LID] THEN
REPEAT GEN_TAC THEN
ASM_CASES_TAC `(e2:real^3)$1 = &0` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(e3:real^3)$1 = &0` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
REAL_MUL_RZERO;
REAL_SUB_RZERO; REAL_ADD_LID] THEN
REWRITE_TAC[
REAL_SUB_LZERO;
REAL_MUL_RID] THEN
MATCH_MP_TAC(REAL_ARITH
`(u = &1 /\ v = &1 /\ w = &0 ==> a = b /\ --c = d \/ a = --b /\ c = d) /\
(a = --b /\ c = d ==> x <= &0)
==> (u = &1 /\ v = &1 /\ w = &0 /\ &0 < x
==> a:real = b /\ --c:real = d)`) THEN
CONJ_TAC THENL [CONV_TAC REAL_RING; ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN
MATCH_MP_TAC(REAL_ARITH
`&0 <= x * x /\ &0 <= y * y ==> --x * x + y * -- y <= &0`) THEN
REWRITE_TAC[
REAL_LE_SQUARE]);;
let ORTHONORMAL_IMP_NONZERO = prove
(`!e1 e2 e3. orthonormal e1 e2 e3
==> ~(e1 = vec 0) /\ ~(e2 = vec 0) /\ ~(e3 = vec 0)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[orthonormal;
DOT_LZERO] THEN REAL_ARITH_TAC);;
let ORTHONORMAL_IMP_DISTINCT = prove
(`!e1 e2 e3. orthonormal e1 e2 e3 ==> ~(e1 = e2) /\ ~(e1 = e3) /\ ~(e2 = e3)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[orthonormal;
DOT_LZERO] THEN REAL_ARITH_TAC);;
let AZIM_EXISTS = prove
(`!v w w1 w2.
?theta. &0 <= theta /\ theta < &2 * pi /\
?h1 h2.
!e1 e2 e3.
orthonormal e1 e2 e3 /\
dist(w,v) % e3 = w - v /\
~(w = v)
==> ?psi r1 r2.
w1 - v = (r1 * cos psi) % e1 +
(r1 * sin psi) % e2 +
h1 % (w - v) /\
w2 - v = (r2 * cos (psi + theta)) % e1 +
(r2 * sin (psi + theta)) % e2 +
h2 % (w - v) /\
(~collinear {v, w, w1} ==> &0 < r1) /\
(~collinear {v, w, w2} ==> &0 < r2)`,
let azim_def = new_definition
`azim v w w1 w2 =
if collinear {v,w,w1} \/ collinear {v,w,w2} then &0
else @theta. &0 <= theta /\ theta < &2 * pi /\
?h1 h2.
!e1 e2 e3.
orthonormal e1 e2 e3 /\
dist(w,v) % e3 = w - v /\
~(w = v)
==> ?psi r1 r2.
w1 - v = (r1 * cos psi) % e1 +
(r1 * sin psi) % e2 +
h1 % (w - v) /\
w2 - v = (r2 * cos (psi + theta)) % e1 +
(r2 * sin (psi + theta)) % e2 +
h2 % (w - v) /\
&0 < r1 /\ &0 < r2`;;let azim = prove
(`!v w w1 w2:real^3.
&0 <= azim v w w1 w2 /\ azim v w w1 w2 < &2 * pi /\
?h1 h2.
!e1 e2 e3.
orthonormal e1 e2 e3 /\
dist(w,v) % e3 = w - v /\
~(w = v)
==> ?psi r1 r2.
w1 - v = (r1 * cos psi) % e1 +
(r1 * sin psi) % e2 +
h1 % (w - v) /\
w2 - v = (r2 * cos (psi + azim v w w1 w2)) % e1 +
(r2 * sin (psi + azim v w w1 w2)) % e2 +
h2 % (w - v) /\
(~collinear {v, w, w1} ==> &0 < r1) /\
(~collinear {v, w, w2} ==> &0 < r2)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[
azim_def] THEN
COND_CASES_TAC THENL
[ALL_TAC;
RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN ASM_REWRITE_TAC[] THEN
CONV_TAC SELECT_CONV THEN
MP_TAC(ISPECL [`v:real^3`; `w:real^3`; `w1:real^3`; `w2:real^3`]
AZIM_EXISTS) THEN
ASM_REWRITE_TAC[]] THEN
SIMP_TAC[
PI_POS;
REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH;
REAL_LE_REFL] THEN
FIRST_X_ASSUM DISJ_CASES_TAC THENL
[MP_TAC(ISPECL [`v:real^3`; `w:real^3`; `w2:real^3`; `w1:real^3`]
AZIM_EXISTS) THEN
DISCH_THEN(CHOOSE_THEN(MP_TAC o CONJUNCT2 o CONJUNCT2)) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`h2:real`; `h1:real`] THEN
DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`h1:real`; `h2:real`] THEN
MAP_EVERY X_GEN_TAC [`e1:real^3`; `e2:real^3`; `e3:real^3`] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`e1:real^3`; `e2:real^3`; `e3:real^3`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `psi:real` THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
REAL_ADD_RID] THEN
MAP_EVERY X_GEN_TAC [`r2:real`; `r1:real`] THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`&0`; `r2:real`];
MP_TAC(ISPECL [`v:real^3`; `w:real^3`; `w1:real^3`; `w2:real^3`]
AZIM_EXISTS) THEN
DISCH_THEN(CHOOSE_THEN(MP_TAC o CONJUNCT2 o CONJUNCT2)) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`h1:real`; `h2:real`] THEN
DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`h1:real`; `h2:real`] THEN
MAP_EVERY X_GEN_TAC [`e1:real^3`; `e2:real^3`; `e3:real^3`] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`e1:real^3`; `e2:real^3`; `e3:real^3`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `psi:real` THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
REAL_ADD_RID] THEN
MAP_EVERY X_GEN_TAC [`r1:real`; `r2:real`] THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`r1:real`; `&0`]] THEN
ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
[SET_RULE `{v,w,x} = {w,v,x}`]) THEN
ONCE_REWRITE_TAC[
COLLINEAR_3] THEN ASM_REWRITE_TAC[] THEN
UNDISCH_THEN `dist(w:real^3,v) % e3 = w - v` (SUBST1_TAC o SYM) THEN
REWRITE_TAC[GSYM
DOT_CAUCHY_SCHWARZ_EQUAL] THEN
RULE_ASSUM_TAC(REWRITE_RULE[orthonormal]) THEN
ASM_REWRITE_TAC[
DOT_LADD;
DOT_RADD;
DOT_LMUL;
DOT_RMUL;
REAL_MUL_RZERO] THEN
ONCE_REWRITE_TAC[
DOT_SYM] THEN ASM_REWRITE_TAC[
REAL_MUL_RZERO] THEN
REWRITE_TAC[REAL_ADD_LID;
REAL_ADD_RID;
REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `(r * c) * (r * c):real = r pow 2 * c pow 2`] THEN
REWRITE_TAC[REAL_ARITH `r * c + r * s + f:real = r * (s + c) + f`] THEN
REWRITE_TAC[
SIN_CIRCLE] THEN REWRITE_TAC[REAL_RING
`(d * h * d) pow 2 = (d * d) * (r * &1 + h * d * h * d) <=>
d = &0 \/ r = &0`] THEN
ASM_REWRITE_TAC[
DIST_EQ_0;
REAL_POW_EQ_0; ARITH] THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[
REAL_MUL_LZERO;
DOT_LZERO]);;
let AZIM_UNIQUE = prove
(`!v w w1 w2 h1 h2 r1 r2 e1 e2 e3 psi theta.
&0 <= theta /\
theta < &2 * pi /\
orthonormal e1 e2 e3 /\
dist(w,v) % e3 = w - v /\
~(w = v) /\
&0 < r1 /\ &0 < r2 /\
w1 - v = (r1 * cos psi) % e1 +
(r1 * sin psi) % e2 +
h1 % (w - v) /\
w2 - v = (r2 * cos (psi + theta)) % e1 +
(r2 * sin (psi + theta)) % e2 +
h2 % (w - v)
==> azim v w w1 w2 = theta`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `~collinear{v:real^3,w,w2} /\ ~collinear {v,w,w1}`
STRIP_ASSUME_TAC THENL
[ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
ONCE_REWRITE_TAC[
COLLINEAR_3] THEN REWRITE_TAC[
COLLINEAR_LEMMA] THEN
ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[
VECTOR_SUB_EQ] THEN
UNDISCH_THEN `dist(w:real^3,v) % e3 = w - v` (SUBST1_TAC o SYM) THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC; VECTOR_ARITH
`a + b + c % x:real^N = d % x <=> a + b + (c - d) % x = vec 0`] THEN
ASM_SIMP_TAC[
ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT_0] THEN
ASM_SIMP_TAC[
CONJ_ASSOC;
REAL_LT_IMP_NZ;
SIN_CIRCLE; REAL_RING
`s pow 2 + c pow 2 = &1 ==> (r * c = &0 /\ r * s = &0 <=> r = &0)`];
ALL_TAC] THEN
SUBGOAL_THEN `(azim v w w1 w2 - theta) / (&2 * pi) = &0` MP_TAC THENL
[ALL_TAC; MP_TAC
PI_POS THEN CONV_TAC REAL_FIELD] THEN
MATCH_MP_TAC
REAL_EQ_INTEGERS_IMP THEN
ASM_SIMP_TAC[
REAL_SUB_RZERO;
REAL_ABS_DIV;
REAL_ABS_MUL;
REAL_ABS_NUM;
REAL_ABS_PI;
REAL_LT_LDIV_EQ;
REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH;
PI_POS;
INTEGER_CLOSED; REAL_MUL_LID] THEN
MP_TAC(ISPECL [`v:real^3`; `w:real^3`; `w1:real^3`; `w2:real^3`] azim) THEN
ASM_REWRITE_TAC[] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_SIMP_TAC[REAL_ARITH
`&0 <= x /\ x < k /\ &0 <= y /\ y < k ==> abs(x - y) < k`] THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`k1:real`; `k2:real`] THEN
DISCH_THEN(MP_TAC o SPECL [`e1:real^3`; `e2:real^3`; `e3:real^3`]) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`phi:real`; `s1:real`; `s2:real`] THEN
UNDISCH_THEN `dist(w:real^3,v) % e3 = w - v` (SUBST1_TAC o SYM) THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC] THEN
ASM_SIMP_TAC[
ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> (c /\ d) /\ a /\ b`] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o MATCH_MP (REAL_FIELD
`r * c = r' * c' /\ r * s = r' * s' /\ u:real = v
==> s pow 2 + c pow 2 = &1 /\ s' pow 2 + c' pow 2 = &1 /\
&0 < r /\ (r pow 2 = r' pow 2 ==> r = r')
==> s = s' /\ c = c'`))) THEN
ASM_REWRITE_TAC[
SIN_CIRCLE; GSYM
REAL_EQ_SQUARE_ABS] THEN
ASM_SIMP_TAC[REAL_ARITH
`&0 < x /\ &0 < y ==> (abs x = abs y <=> x = y)`] THEN
REWRITE_TAC[
SIN_COS_EQ] THEN
REWRITE_TAC[REAL_ARITH
`psi + theta = (phi + az) + x:real <=> psi = phi + x + (az - theta)`] THEN
DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[
REAL_EQ_ADD_LCANCEL] THEN
REWRITE_TAC[REAL_ARITH
`&2 * m * pi + x = &2 * n * pi <=> x = (n - m) * &2 * pi`] THEN
DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
ASM_SIMP_TAC[
PI_POS; REAL_FIELD `&0 < pi ==> (x * &2 * pi) / (&2 * pi) = x`;
INTEGER_CLOSED]);;
let AZIM_TRANSLATION = prove
(`!a v w w1 w2. azim (a + v) (a + w) (a + w1) (a + w2) = azim v w w1 w2`,
REPEAT GEN_TAC THEN REWRITE_TAC[
azim_def] THEN
REWRITE_TAC[VECTOR_ARITH `(a + w) - (a + v):real^3 = w - v`;
VECTOR_ARITH `a + w:real^3 = a + v <=> w = v`;
NORM_ARITH `dist(a + v,a + w) = dist(v,w)`] THEN
REWRITE_TAC[SET_RULE
`{a + x,a + y,a + z} =
IMAGE (\x:real^3. a + x) {x,y,z}`] THEN
REWRITE_TAC[
COLLINEAR_TRANSLATION_EQ]);;
let AZIM_LINEAR_IMAGE = prove
(`!f. linear f /\ (!x. norm(f x) = norm x) /\
(2 <= dimindex(:3) ==> det(matrix f) = &1)
==> !v w w1 w2. azim (f v) (f w) (f w1) (f w2) = azim v w w1 w2`,
let AZIM_DEGENERATE = prove
(`(!v w w1 w2. v = w ==> azim v w w1 w2 = &0) /\
(!v w w1 w2. collinear{v,w,w1} ==> azim v w w1 w2 = &0) /\
(!v w w1 w2. collinear{v,w,w2} ==> azim v w w1 w2 = &0)`,
let AZIM_SCALE_ALL = prove
(`!a v w1 w2.
&0 < a /\ &0 < b /\ &0 < c
==> azim (vec 0) (a % v) (b % w1) (c % w2) = azim (vec 0) v w1 w2`,
let AZIM_ARG = prove
(`!x y:real^3. azim (vec 0) (basis 3) x y = Arg(dropout 3 y / dropout 3 x)`,
let AZIM_EQ = prove
(`!v0 v1 w x y.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x} /\ ~collinear{v0,v1,y}
==> (azim v0 v1 w x = azim v0 v1 w y <=> y
IN aff_gt {v0,v1} {x})`,
let AZIM_EQ_ALT = prove
(`!v0 v1 w x y.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x} /\ ~collinear{v0,v1,y}
==> (azim v0 v1 w x = azim v0 v1 w y <=> x
IN aff_gt {v0,v1} {y})`,
ASM_SIMP_TAC[GSYM
AZIM_EQ] THEN MESON_TAC[]);;
let AZIM_EQ_0 = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = &0 <=> w
IN aff_gt {v0,v1} {x})`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `azim v0 v1 w x = azim v0 v1 w w` THEN CONJ_TAC THENL
[REWRITE_TAC[
AZIM_REFL];
ASM_SIMP_TAC[
AZIM_EQ]]);;
let AZIM_EQ_0_ALT = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = &0 <=> x
IN aff_gt {v0,v1} {w})`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `azim v0 v1 w x = azim v0 v1 w w` THEN CONJ_TAC THENL
[REWRITE_TAC[
AZIM_REFL];
ASM_SIMP_TAC[
AZIM_EQ_ALT]]);;
let AZIM_EQ_0_GE = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = &0 <=> w
IN aff_ge {v0,v1} {x})`,
let AZIM_COMPL_EQ_0 = prove
(`!z w w1 w2.
~collinear {z,w,w1} /\ ~collinear {z,w,w2} /\ azim z w w1 w2 = &0
==> azim z w w2 w1 = &0`,
let AZIM_COMPL = prove
(`!z w w1 w2.
~collinear {z,w,w1} /\ ~collinear {z,w,w2}
==> azim z w w2 w1 = if azim z w w1 w2 = &0 then &0
else &2 * pi - azim z w w1 w2`,
let AZIM_EQ_PI_SYM = prove
(`!z w w1 w2.
~collinear {z, w, w1} /\ ~collinear {z, w, w2}
==> (azim z w w1 w2 = pi <=> azim z w w2 w1 = pi)`,
REPEAT STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_COMPL o lhand o rand o snd) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let AZIM_EQ_0_SYM = prove
(`!z w w1 w2.
~collinear {z, w, w1} /\ ~collinear {z, w, w2}
==> (azim z w w1 w2 = &0 <=> azim z w w2 w1 = &0)`,
let AZIM_EQ_0_GE_ALT = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = &0 <=> x
IN aff_ge {v0,v1} {w})`,
let AZIM_EQ_PI = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = pi <=> w
IN aff_lt {v0,v1} {x})`,
let AZIM_EQ_PI_ALT = prove
(`!v0 v1 w x.
~collinear{v0,v1,w} /\ ~collinear{v0,v1,x}
==> (azim v0 v1 w x = pi <=> x
IN aff_lt {v0,v1} {w})`,
let AZIM_EQ_0_PI_IMP_COPLANAR = prove
(`!v0 v1 w1 w2.
azim v0 v1 w1 w2 = &0 \/ azim v0 v1 w1 w2 = pi
==> coplanar {v0,v1,w1,w2}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `collinear {v0:real^3,v1,w1}` THENL
[MP_TAC(ISPECL [`v0:real^3`; `v1:real^3`; `w1:real^3`; `w2:real^3`]
NOT_COPLANAR_NOT_COLLINEAR) THEN
ASM_REWRITE_TAC[] THEN CONV_TAC TAUT;
POP_ASSUM MP_TAC] THEN
ASM_CASES_TAC `collinear {v0:real^3,v1,w2}` THENL
[MP_TAC(ISPECL [`v0:real^3`; `v1:real^3`; `w2:real^3`; `w1:real^3`]
NOT_COPLANAR_NOT_COLLINEAR) THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
INSERT_AC] THEN CONV_TAC TAUT;
POP_ASSUM MP_TAC] THEN
MAP_EVERY (fun t -> SPEC_TAC(t,t))
[`w2:real^3`; `w1:real^3`; `v1:real^3`; `v0:real^3`] THEN
GEOM_ORIGIN_TAC `v0:real^3` THEN
GEOM_BASIS_MULTIPLE_TAC 3 `v1:real^3` THEN
X_GEN_TAC `w:real` THEN GEN_REWRITE_TAC LAND_CONV [
REAL_LE_LT] THEN
ASM_CASES_TAC `w = &0` THEN ASM_REWRITE_TAC[] THENL
[ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
SIMP_TAC[
AZIM_SPECIAL_SCALE] THEN
ASM_SIMP_TAC[
AZIM_ARG;
COLLINEAR_SPECIAL_SCALE] THEN
REWRITE_TAC[
COLLINEAR_BASIS_3;
ARG_EQ_0_PI] THEN
REWRITE_TAC[real;
IM_COMPLEX_DIV_EQ_0] THEN
REWRITE_TAC[
complex_mul; cnj;
IM;
RE] THEN
REWRITE_TAC[REAL_ARITH `x * --y + a * b = &0 <=> x * y = a * b`] THEN
REWRITE_TAC[
RE_DEF;
IM_DEF] THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
DISCH_TAC THEN DISCH_TAC THEN
SIMP_TAC[dropout;
LAMBDA_BETA; DIMINDEX_3; ARITH; DIMINDEX_2] THEN
DISCH_TAC THEN REWRITE_TAC[coplanar] THEN
MAP_EVERY EXISTS_TAC [`vec 0:real^3`; `w % basis 3:real^3`; `w1:real^3`] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = d
INSERT {a,b,c}`] THEN
ONCE_REWRITE_TAC[
INSERT_SUBSET] THEN REWRITE_TAC[
HULL_SUBSET] THEN
SIMP_TAC[
AFFINE_HULL_EQ_SPAN;
IN_INSERT;
HULL_INC] THEN
REWRITE_TAC[
SPAN_BREAKDOWN_EQ;
SPAN_EMPTY;
IN_SING] THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_SUB_RZERO] THEN
REPEAT(POP_ASSUM MP_TAC) THEN
SIMP_TAC[
CART_EQ; DIMINDEX_2;
FORALL_2;
FORALL_3; dropout;
LAMBDA_BETA;
DIMINDEX_2; DIMINDEX_3; ARITH;
VEC_COMPONENT; ARITH;
VECTOR_SUB_COMPONENT;
VECTOR_MUL_COMPONENT;
BASIS_COMPONENT] THEN
REPEAT STRIP_TAC THEN
REWRITE_TAC[
REAL_MUL_RZERO;
REAL_SUB_RZERO] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN
REWRITE_TAC[
RIGHT_EXISTS_AND_THM] THEN
ASM_SIMP_TAC[
EXISTS_REFL; REAL_FIELD
`&0 < w ==> (x - k * w * &1 - y = &0 <=> k = (x - y) / w)`] THEN
SUBGOAL_THEN `~((w1:real^3)$2 = &0) \/ ~((w2:real^3)$1 = &0)`
STRIP_ASSUME_TAC THENL
[REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING;
EXISTS_TAC `(w2:real^3)$2 / (w1:real^3)$2` THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
EXISTS_TAC `(w2:real^3)$1 / (w1:real^3)$1` THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD]);;
let AZIM_SAME_WITHIN_AFF_GE_ALT = prove
(`!a u v w z.
v
IN aff_ge {a} {u,w} /\ ~collinear{a,u,v} /\ ~collinear{a,u,w}
==> azim a u z v = azim a u z w`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
AZIM_SAME_WITHIN_AFF_GE) THEN
ASM_CASES_TAC `collinear {a:real^3,u,z}` THEN
ASM_SIMP_TAC[
AZIM_DEGENERATE] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_COMPL o lhand o snd) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_COMPL o rand o snd) THEN
ASM_SIMP_TAC[]);;
let COLLINEAR_WITHIN_AFF_GE_COLLINEAR = prove
(`!a u v w:real^N.
v
IN aff_ge {a} {u,w} /\ collinear{a,u,w} ==> collinear{a,v,w}`,
GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `w:real^N = vec 0` THENL
[ASM_REWRITE_TAC[
COLLINEAR_2;
INSERT_AC]; ALL_TAC] THEN
ASM_CASES_TAC `u:real^N = vec 0` THENL
[ONCE_REWRITE_TAC[
AFF_GE_DISJOINT_DIFF] THEN
ASM_REWRITE_TAC[SET_RULE `{a}
DIFF {a,b} = {}`] THEN
REWRITE_TAC[GSYM
CONVEX_HULL_AFF_GE] THEN
ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN
ASM_SIMP_TAC[
COLLINEAR_3_AFFINE_HULL] THEN
MESON_TAC[
CONVEX_HULL_SUBSET_AFFINE_HULL;
SUBSET];
ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN
ASM_REWRITE_TAC[
COLLINEAR_LEMMA_ALT] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `a:real`)) THEN
ASM_SIMP_TAC[
AFF_GE_1_2_0; SET_RULE
`
DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
REWRITE_TAC[
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[GSYM
VECTOR_ADD_RDISTRIB;
VECTOR_MUL_ASSOC] THEN
MESON_TAC[]]);;
let AZIM_EQ_IMP = prove
(`!v0 v1 w x y.
~collinear {v0, v1, w} /\
~collinear {v0, v1, y} /\
x
IN aff_gt {v0, v1} {y}
==> azim v0 v1 w x = azim v0 v1 w y`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `v1:real^3 = v0` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_CASES_TAC `collinear {v0:real^3,v1,x}` THENL
[ALL_TAC; ASM_SIMP_TAC[
AZIM_EQ_ALT]] THEN
UNDISCH_TAC `collinear {v0:real^3,v1,x}` THEN
MATCH_MP_TAC(TAUT
`(s /\ p ==> r) ==> p ==> ~q /\ ~r /\ s ==> t`) THEN
ASM_SIMP_TAC[
COLLINEAR_3_IN_AFFINE_HULL] THEN
ASM_CASES_TAC `y:real^3 = v0` THEN
ASM_SIMP_TAC[
HULL_INC;
IN_INSERT] THEN
ASM_CASES_TAC `y:real^3 = v1` THEN
ASM_SIMP_TAC[
HULL_INC;
IN_INSERT] THEN
ASM_SIMP_TAC[
AFF_GT_2_1; SET_RULE
`
DISJOINT {a,b} {c} <=> ~(c = a) /\ ~(c = b)`] THEN
REWRITE_TAC[
AFFINE_HULL_2;
IN_ELIM_THM;
LEFT_AND_EXISTS_THM] THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC
[`t1:real`; `t2:real`; `t3:real`; `s1:real`; `s2:real`] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
FIRST_X_ASSUM(MP_TAC o AP_TERM `(%) (inv t3) :real^3->real^3`) THEN
ASM_SIMP_TAC[
VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC; REAL_MUL_LINV;
REAL_LT_IMP_NZ; VECTOR_ARITH
`x:real^N = y + z + &1 % w <=> w = x - (y + z)`] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
EXISTS_TAC `inv t3 * s1 - inv t3 * t1:real` THEN
EXISTS_TAC `inv t3 * s2 - inv t3 * t2:real` THEN CONJ_TAC THENL
[ASM_SIMP_TAC[REAL_FIELD
`&0 < t ==> (inv t * a - inv t * b + inv t * c - inv t * d = &1 <=>
(a + c) - (b + d) = t)`] THEN
ASM_REAL_ARITH_TAC;
VECTOR_ARITH_TAC]);;
let dihV = new_definition
`dihV w0 w1 w2 w3 =
let va = w2 - w0 in
let vb = w3 - w0 in
let vc = w1 - w0 in
let vap = ( vc dot vc) % va - ( va dot vc) % vc in
let vbp = ( vc dot vc) % vb - ( vb dot vc) % vc in
arcV (vec 0) vap vbp`;;let DIHV = prove
(`dihV (w0:real^N) w1 w2 w3 =
let va = w2 - w0 in
let vb = w3 - w0 in
let vc = w1 - w0 in
let vap = (vc dot vc) % va - (va dot vc) % vc in
let vbp = (vc dot vc) % vb - (vb dot vc) % vc in
angle(vap,vec 0,vbp)`,
let DIHV_TRANSLATION_EQ = prove
(`!a w0 w1 w2 w3:real^N.
dihV (a + w0) (a + w1) (a + w2) (a + w3) = dihV w0 w1 w2 w3`,
REWRITE_TAC[
DIHV; VECTOR_ARITH `(a + x) - (a + y):real^N = x - y`]);;
let DIHV_LINEAR_IMAGE = prove
(`!f:real^M->real^N w0 w1 w2 w3.
linear f /\ (!x. norm(f x) = norm x)
==> dihV (f w0) (f w1) (f w2) (f w3) = dihV w0 w1 w2 w3`,
let DIHV_RANGE = prove
(`!w0 w1 w2 w3. &0 <= dihV w0 w1 w2 w3 /\ dihV w0 w1 w2 w3 <= pi`,
REWRITE_TAC[
DIHV] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
REWRITE_TAC[
ANGLE_RANGE]);;
let COS_AZIM_DIHV = prove
(`!v w v1 v2:real^3.
~collinear {v,w,v1} /\ ~collinear {v,w,v2}
==> cos(azim v w v1 v2) = cos(dihV v w v1 v2)`,
let AZIM_DIHV_SAME = prove
(`!v w v1 v2:real^3.
~collinear {v,w,v1} /\ ~collinear {v,w,v2} /\
azim v w v1 v2 < pi
==> azim v w v1 v2 = dihV v w v1 v2`,
let AZIM_DIHV_COMPL = prove
(`!v w v1 v2:real^3.
~collinear {v,w,v1} /\ ~collinear {v,w,v2} /\
pi <= azim v w v1 v2
==> azim v w v1 v2 = &2 * pi - dihV v w v1 v2`,
REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `x = &2 * pi - y <=> y = &2 * pi - x`] THEN
MATCH_MP_TAC
COS_INJ_PI THEN
REWRITE_TAC[
COS_SUB;
SIN_NPI;
COS_NPI;
REAL_MUL_LZERO] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[
COS_AZIM_DIHV;
REAL_ADD_RID; REAL_MUL_LID] THEN
ASM_REWRITE_TAC[
DIHV_RANGE] THEN MATCH_MP_TAC(REAL_ARITH
`p <= x /\ x < &2 * p ==> &0 <= &2 * p - x /\ &2 * p - x <= p`) THEN
ASM_SIMP_TAC[azim]);;
let AZIM_DIVH = prove
(`!v w v1 v2:real^3.
~collinear {v,w,v1} /\ ~collinear {v,w,v2}
==> azim v w v1 v2 = if azim v w v1 v2 < pi then dihV v w v1 v2
else &2 * pi - dihV v w v1 v2`,
let AZIM_DIHV_EQ_0 = prove
(`!v0 v1 w1 w2.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> (azim v0 v1 w1 w2 = &0 <=> dihV v0 v1 w1 w2 = &0)`,
REPEAT STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_DIVH o lhs o lhs o snd) THEN
ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN
ONCE_REWRITE_TAC[REAL_ARITH `a:real = p - b <=> b = p - a`] THEN
DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[REAL_ARITH `&2 * p - (&2 * p - a) = &0 <=> a = &0`] THEN
MATCH_MP_TAC(REAL_ARITH
`a < &2 * pi /\ ~(a < pi) ==> (a = &0 <=> &2 * pi - a = &0)`) THEN
ASM_REWRITE_TAC[azim]);;
let AZIM_DIHV_EQ_PI = prove
(`!v0 v1 w1 w2.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> (azim v0 v1 w1 w2 = pi <=> dihV v0 v1 w1 w2 = pi)`,
REPEAT STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_DIVH o lhs o lhs o snd) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let AZIM_EQ_0_PI_EQ_COPLANAR = prove
(`!v0 v1 w1 w2.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> (azim v0 v1 w1 w2 = &0 \/ azim v0 v1 w1 w2 = pi <=>
coplanar {v0,v1,w1,w2})`,
let DIHV_EQ_0_PI_EQ_COPLANAR = prove
(`!v0 v1 w1 w2:real^3.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> (dihV v0 v1 w1 w2 = &0 \/ dihV v0 v1 w1 w2 = pi <=>
coplanar {v0,v1,w1,w2})`,
let DIHV_SYM = prove
(`!v0 v1 v2 v3:real^N.
dihV v0 v1 v3 v2 = dihV v0 v1 v2 v3`,
REPEAT GEN_TAC THEN REWRITE_TAC[
DIHV] THEN
CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
REWRITE_TAC[
DOT_SYM;
ANGLE_SYM]);;
let DIHV_NEG = prove
(`!v0 v1 v2 v3. dihV (--v0) (--v1) (--v2) (--v3) = dihV v0 v1 v2 v3`,
let DIHV_NEG_0 = prove
(`!v1 v2 v3. dihV (vec 0) (--v1) (--v2) (--v3) = dihV (vec 0) v1 v2 v3`,
let DIHV_ARCV = prove
(`!e u v w:real^N.
orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\ ~(e = u)
==> dihV u e v w = arcV u v w`,
let AZIM_DIHV_SAME_STRONG = prove
(`!v w v1 v2:real^3.
~collinear {v,w,v1} /\ ~collinear {v,w,v2} /\
azim v w v1 v2 <= pi
==> azim v w v1 v2 = dihV v w v1 v2`,
let AZIM_ARCV = prove
(`!e u v w:real^3.
orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\
~collinear{u,e,v} /\ ~collinear{u,e,w} /\
azim u e v w <= pi
==> azim u e v w = arcV u v w`,
let COLLINEAR_AZIM_0_OR_PI = prove
(`!u e v w. collinear {u,v,w} ==> azim u e v w = &0 \/ azim u e v w = pi`,
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `collinear{u:real^3,e,v}` THEN
ASM_SIMP_TAC[
AZIM_DEGENERATE] THEN
ASM_CASES_TAC `collinear{u:real^3,e,w}` THEN
ASM_SIMP_TAC[
AZIM_DEGENERATE] THEN
ASM_SIMP_TAC[
AZIM_EQ_0_PI_EQ_COPLANAR] THEN
ONCE_REWRITE_TAC[SET_RULE `{u,e,v,w} = {u,v,w,e}`] THEN
ASM_MESON_TAC[
NOT_COPLANAR_NOT_COLLINEAR]);;
let REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE = prove
(`!f:real^M->real^N g h k x s.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
f continuous (at x within s) /\ g continuous (at x within s) /\
h continuous (at x within s) /\ k continuous (at x within s)
==> (\x. dihV (f x) (g x) (h x) (k x))
real_continuous (at x within s)`,
let REAL_CONTINUOUS_AT_DIHV_COMPOSE = prove
(`!f:real^M->real^N g h k x.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
f continuous (at x) /\ g continuous (at x) /\
h continuous (at x) /\ k continuous (at x)
==> (\x. dihV (f x) (g x) (h x) (k x))
real_continuous (at x)`,
let REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE = prove
(`!f:real->real^N g h k x s.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
f continuous (atreal x within s) /\ g continuous (atreal x within s) /\
h continuous (atreal x within s) /\ k continuous (atreal x within s)
==> (\x. dihV (f x) (g x) (h x) (k x))
real_continuous
(atreal x within s)`,
let REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE = prove
(`!f:real->real^N g h k x.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
f continuous (atreal x) /\ g continuous (atreal x) /\
h continuous (atreal x) /\ k continuous (atreal x)
==> (\x. dihV (f x) (g x) (h x) (k x))
real_continuous (atreal x)`,
let REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE = prove
(`!f:real^M->real^3 g h k x s.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
~(k x
IN aff_ge {f x,g x} {h x}) /\
f continuous (at x within s) /\ g continuous (at x within s) /\
h continuous (at x within s) /\ k continuous (at x within s)
==> (\x. azim (f x) (g x) (h x) (k x))
real_continuous (at x within s)`,
let REAL_CONTINUOUS_AT_AZIM_COMPOSE = prove
(`!f:real^M->real^3 g h k x.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
~(k x
IN aff_ge {f x,g x} {h x}) /\
f continuous (at x) /\ g continuous (at x) /\
h continuous (at x) /\ k continuous (at x)
==> (\x. azim (f x) (g x) (h x) (k x))
real_continuous (at x)`,
let REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE = prove
(`!f:real->real^3 g h k x s.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
~(k x
IN aff_ge {f x,g x} {h x}) /\
f continuous (atreal x within s) /\ g continuous (atreal x within s) /\
h continuous (atreal x within s) /\ k continuous (atreal x within s)
==> (\x. azim (f x) (g x) (h x) (k x))
real_continuous
(atreal x within s)`,
let REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE = prove
(`!f:real->real^3 g h k x.
~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
~(k x
IN aff_ge {f x,g x} {h x}) /\
f continuous (atreal x) /\ g continuous (atreal x) /\
h continuous (atreal x) /\ k continuous (atreal x)
==> (\x. azim (f x) (g x) (h x) (k x))
real_continuous (atreal x)`,
let ZENITH_EXISTS = prove
(`!u v w:real^3.
~(u = v) /\ ~(w = v)
==> (?u' r phi e3.
phi = arcV v u w /\
r = dist(u,v) /\
dist(w,v) % e3 = w - v /\
u' dot e3 = &0 /\
u = v + u' + (r * cos phi) % e3)`,
ONCE_REWRITE_TAC[VECTOR_ARITH
`u:real^3 = v + u' + x <=> u - v = u' + x`] THEN
GEN_GEOM_ORIGIN_TAC `v:real^3` ["u'";
let SPHERICAL_COORDINATES = prove
(`!u v w u' e1 e2 e3 r phi theta.
~collinear {v, w, u} /\
~collinear {v, w, u'} /\
orthonormal e1 e2 e3 /\
dist(w,v) % e3 = w - v /\
(v + e1)
IN aff_gt {v, w} {u} /\
r = dist(v,u') /\
phi = arcV v u' w /\
theta = azim v w u u'
==> u' = v + (r * cos theta * sin phi) % e1 +
(r * sin theta * sin phi) % e2 +
(r * cos phi) % e3`,
ONCE_REWRITE_TAC[VECTOR_ARITH
`u':real^3 = u + v + w <=> u' - u = v + w`] THEN
GEN_GEOM_ORIGIN_TAC `v:real^3` ["e1";
let wedge = new_definition
`wedge v0 v1 w1 w2 = {y | ~collinear {v0,v1,y} /\
&0 < azim v0 v1 w1 y /\
azim v0 v1 w1 y < azim v0 v1 w1 w2}`;;let WEDGE_ALT = prove
(`!v0 v1 w1 w2.
~(v0 = v1)
==> wedge v0 v1 w1 w2 = {y | ~(y
IN affine hull {v0,v1}) /\
&0 < azim v0 v1 w1 y /\
azim v0 v1 w1 y < azim v0 v1 w1 w2}`,
let WEDGE_LINEAR_IMAGE = prove
(`!f. linear f /\ (!x. norm(f x) = norm x) /\
(2 <= dimindex(:3) ==> det(matrix f) = &1)
==> !v w w1 w2. wedge (f v) (f w) (f w1) (f w2) =
IMAGE f (wedge v w w1 w2)`,
let WEDGE_SPECIAL_SCALE = prove
(`!a v w1 w2.
&0 < a /\
~collinear{vec 0,a % v,w1} /\
~collinear{vec 0,a % v,w2}
==> wedge (vec 0) (a % v) w1 w2 = wedge (vec 0) v w1 w2`,
let WEDGE_DEGENERATE = prove
(`(!z w w1 w2. z = w ==> wedge z w w1 w2 = {}) /\
(!z w w1 w2. collinear{z,w,w1} ==> wedge z w w1 w2 = {}) /\
(!z w w1 w2. collinear{z,w,w2} ==> wedge z w w1 w2 = {})`,
let AFF_GT_LEMMA = prove
(`!v1 v2:real^N.
&0 < t1 /\ ~(v2 = vec 0)
==> aff_gt {vec 0} {t1 % basis 1, v2} =
{a % basis 1 + b % v2 | &0 < a /\ &0 < b}`,
let WEDGE_LUNE_GT = prove
(`!v0 v1 w1 w2.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2} /\
&0 < azim v0 v1 w1 w2 /\ azim v0 v1 w1 w2 < pi
==> wedge v0 v1 w1 w2 = aff_gt {v0,v1} {w1,w2}`,
let lemma = prove
(`!a x:real^3. (?a. x = a % basis 3) <=> dropout 3 x:real^2 = vec 0`,
SIMP_TAC[CART_EQ; FORALL_2; FORALL_3; DIMINDEX_2; DIMINDEX_3;
dropout; LAMBDA_BETA; BASIS_COMPONENT; ARITH; REAL_MUL_RID;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RZERO; UNWIND_THM1] THEN
MESON_TAC[]) in
REWRITE_TAC[wedge] THEN GEOM_ORIGIN_TAC `v0:real^3` THEN
GEOM_BASIS_MULTIPLE_TAC 3 `v1:real^3` THEN
X_GEN_TAC `w:real` THEN GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN
ASM_CASES_TAC `w = &0` THEN ASM_REWRITE_TAC[] THENL
[ASM_REWRITE_TAC[VECTOR_MUL_LZERO; INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
ASM_SIMP_TAC[AZIM_SPECIAL_SCALE; COLLINEAR_SPECIAL_SCALE] THEN
POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`w1:real^3`; `w2:real^3`] THEN
REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ONCE_REWRITE_TAC[TAUT `~a /\ b /\ c <=> ~(~a ==> ~(b /\ c))`] THEN
ASM_SIMP_TAC[AZIM_ARG] THEN REWRITE_TAC[COLLINEAR_BASIS_3] THEN
RULE_ASSUM_TAC(REWRITE_RULE[COLLINEAR_BASIS_3]) THEN STRIP_TAC THEN
REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN
W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_SPECIAL_SCALE o rand o snd) THEN
SUBGOAL_THEN
`~(w1:real^3 = vec 0) /\ ~(w2:real^3 = vec 0) /\
~(w1 = basis 3) /\ ~(w2 = basis 3)`
STRIP_ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_neg o concl))) THEN
ASM_REWRITE_TAC[DROPOUT_BASIS_3; DROPOUT_0; DROPOUT_MUL; VECTOR_MUL_RZERO];
ALL_TAC] THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN
DISCH_THEN(DISJ_CASES_THEN (SUBST_ALL_TAC o SYM)) THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_neg o concl))) THEN
ASM_REWRITE_TAC[DROPOUT_BASIS_3; DROPOUT_0; DROPOUT_MUL; VECTOR_MUL_RZERO];
DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[AFFSIGN_ALT; aff_gt_def; sgn_gt; IN_ELIM_THM] THEN
REWRITE_TAC[SET_RULE `{a,b} UNION {c,d} = {a,b,d,c}`] THEN
REWRITE_TAC[SET_RULE `x IN {a} <=> a = x`] THEN
ASM_SIMP_TAC[FINITE_INSERT; FINITE_UNION; AFFINE_HULL_FINITE_STEP_GEN;
RIGHT_EXISTS_AND_THM; REAL_LT_ADD; REAL_HALF; FINITE_EMPTY] THEN
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_SUB_RZERO] THEN
MATCH_MP_TAC EQ_TRANS THEN
EXISTS_TAC `{y | (dropout 3:real^3->real^2) y IN
aff_gt {vec 0}
{dropout 3 (w1:real^3),dropout 3 (w2:real^3)}}` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[AFFSIGN_ALT; aff_gt_def; sgn_gt; IN_ELIM_THM] THEN
REWRITE_TAC[SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
REWRITE_TAC[SET_RULE `x IN {a} <=> a = x`] THEN
ASM_SIMP_TAC[FINITE_INSERT; FINITE_UNION; AFFINE_HULL_FINITE_STEP_GEN;
RIGHT_EXISTS_AND_THM; REAL_LT_ADD; REAL_HALF; FINITE_EMPTY] THEN
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_SUB_RZERO] THEN
REWRITE_TAC[REAL_EQ_SUB_RADD; RIGHT_AND_EXISTS_THM] THEN
REWRITE_TAC[REAL_ARITH `&1 = x + v <=> v = &1 - x`] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
ONCE_REWRITE_TAC[MESON[]
`(?a b c d. P a b c d) <=> (?b c d a. P a b c d)`] THEN
REWRITE_TAC[UNWIND_THM2] THEN
ONCE_REWRITE_TAC[MESON[]
`(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
REWRITE_TAC[UNWIND_THM2] THEN REWRITE_TAC[VECTOR_ARITH
`y - a - b - c:real^N = vec 0 <=> y - b - c = a`] THEN
REWRITE_TAC[LEFT_EXISTS_AND_THM; lemma] THEN
REWRITE_TAC[DROPOUT_SUB; DROPOUT_MUL] THEN
REWRITE_TAC[VECTOR_ARITH `y - a - b:real^2 = vec 0 <=> y = a + b`] THEN
REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN MESON_TAC[VECTOR_ADD_SYM]] THEN
MATCH_MP_TAC(SET_RULE
`{x | P x} = s ==> {y | P(dropout 3 y)} = {y | dropout 3 y IN s}`) THEN
MP_TAC(CONJ (ASSUME `~((dropout 3:real^3->real^2) w1 = vec 0)`)
(ASSUME `~((dropout 3:real^3->real^2) w2 = vec 0)`)) THEN
UNDISCH_TAC `Arg(dropout 3 (w2:real^3) / dropout 3 (w1:real^3)) < pi` THEN
UNDISCH_TAC `&0 < Arg(dropout 3 (w2:real^3) / dropout 3 (w1:real^3))` THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w2`,`v2:complex`) THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w1`,`v1:complex`) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN GEOM_BASIS_MULTIPLE_TAC 1 `v1:complex` THEN
X_GEN_TAC `v1:real` THEN GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN
ASM_CASES_TAC `v1 = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
SIMP_TAC[AFF_GT_LEMMA] THEN
REWRITE_TAC[COMPLEX_CMUL; COMPLEX_BASIS; COMPLEX_VEC_0] THEN
ASM_SIMP_TAC[ARG_DIV_CX; COMPLEX_MUL_RID; CX_INJ] THEN DISCH_TAC THEN
POP_ASSUM_LIST(K ALL_TAC) THEN X_GEN_TAC `z:complex` THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; IN_ELIM_THM] THEN CONJ_TAC THENL
[X_GEN_TAC `w:complex` THEN STRIP_TAC THEN
MP_TAC(SPECL [`\t. Arg(Cx t + Cx(&1 - t) * z)`;
`&0`; `&1`; `Arg w`] REAL_IVT_DECREASING) THEN
REWRITE_TAC[REAL_POS; REAL_SUB_REFL; COMPLEX_MUL_LZERO] THEN
REWRITE_TAC[REAL_SUB_RZERO; COMPLEX_ADD_LID; COMPLEX_MUL_LID] THEN
ASM_SIMP_TAC[COMPLEX_ADD_RID; ARG_NUM; REAL_LT_IMP_LE] THEN ANTS_TAC THENL
[REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; IN_REAL_INTERVAL] THEN
X_GEN_TAC `t:real` THEN STRIP_TAC THEN
ONCE_REWRITE_TAC[GSYM o_DEF] THEN REWRITE_TAC[o_ASSOC] THEN
MATCH_MP_TAC CONTINUOUS_WITHINREAL_COMPOSE THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ADD THEN CONJ_TAC THENL
[GEN_REWRITE_TAC LAND_CONV [SYM(CONJUNCT2(SPEC_ALL I_O_ID))] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS] THEN
REWRITE_TAC[I_DEF; REAL_CONTINUOUS_WITHIN_ID];
MATCH_MP_TAC CONTINUOUS_COMPLEX_MUL THEN
REWRITE_TAC[CONTINUOUS_CONST] THEN ONCE_REWRITE_TAC[GSYM o_DEF] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS] THEN
SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_CONST;
REAL_CONTINUOUS_WITHIN_ID]];
MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
EXISTS_TAC `{z | &0 <= Im z}` THEN CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_WITHIN_UPPERHALF_ARG THEN
ASM_CASES_TAC `t = &1` THENL
[ASM_REWRITE_TAC[REAL_SUB_REFL] THEN CONV_TAC COMPLEX_RING;
ALL_TAC] THEN
DISCH_THEN(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[IM_ADD; IM_CX; IM_MUL_CX; REAL_ADD_LID; REAL_ENTIRE] THEN
ASM_REWRITE_TAC[REAL_SUB_0] THEN
ASM_MESON_TAC[ARG_LT_PI; REAL_LT_IMP_NZ; REAL_LT_TRANS];
REWRITE_TAC[FORALL_IN_IMAGE; SUBSET; IN_REAL_INTERVAL] THEN
REWRITE_TAC[IN_ELIM_THM; IM_ADD; IM_CX; IM_MUL_CX] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ADD_LID] THEN
MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[GSYM ARG_LE_PI] THEN
ASM_REAL_ARITH_TAC]];
REWRITE_TAC[IN_REAL_INTERVAL] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` MP_TAC) THEN
ASM_CASES_TAC `t = &0` THENL
[ASM_REWRITE_TAC[REAL_SUB_RZERO; COMPLEX_ADD_LID; COMPLEX_MUL_LID] THEN
ASM_MESON_TAC[REAL_LT_REFL];
ALL_TAC] THEN
ASM_CASES_TAC `t = &1` THENL
[ASM_REWRITE_TAC[REAL_SUB_REFL; COMPLEX_MUL_LZERO] THEN
REWRITE_TAC[COMPLEX_ADD_RID; ARG_NUM] THEN ASM_MESON_TAC[REAL_LT_REFL];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_LE_LT] THEN
ASM_REWRITE_TAC[] THEN ABBREV_TAC `u = Cx t + Cx(&1 - t) * z` THEN
ASM_CASES_TAC `u = Cx(&0)` THENL
[ASM_MESON_TAC[ARG_0; REAL_LT_REFL]; ALL_TAC] THEN
STRIP_TAC THEN
EXISTS_TAC `norm(w:complex) / norm(u:complex) * t` THEN
EXISTS_TAC `norm(w:complex) / norm(u:complex) * (&1 - t)` THEN
ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_DIV; COMPLEX_NORM_NZ; REAL_SUB_LT] THEN
SIMP_TAC[CX_MUL; GSYM COMPLEX_MUL_ASSOC; GSYM COMPLEX_ADD_LDISTRIB] THEN
ASM_REWRITE_TAC[CX_DIV] THEN
ASM_SIMP_TAC[CX_INJ; COMPLEX_NORM_ZERO; COMPLEX_FIELD
`~(nu = Cx(&0)) ==> (w = nw / nu * u <=> nu * w = nw * u)`] THEN
GEN_REWRITE_TAC (BINOP_CONV o RAND_CONV) [ARG] THEN
ASM_REWRITE_TAC[COMPLEX_MUL_AC]];
MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
SUBGOAL_THEN `Cx a + Cx b * z = complex(a + b * Re z,b * Im z)`
SUBST1_TAC THENL
[REWRITE_TAC[COMPLEX_EQ; RE; IM; RE_ADD; IM_ADD; RE_CX; IM_CX;
RE_MUL_CX; IM_MUL_CX] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[COMPLEX_EQ; IM; IM_CX] THEN
SUBGOAL_THEN `&0 < Im z` ASSUME_TAC THENL
[ASM_REWRITE_TAC[GSYM ARG_LT_PI]; ALL_TAC] THEN
ASM_SIMP_TAC[ARG_ATAN_UPPERHALF; REAL_LT_MUL; REAL_LT_IMP_NZ; IM] THEN
REWRITE_TAC[RE; REAL_SUB_LT; ATN_BOUNDS] THEN
REWRITE_TAC[REAL_ARITH `pi / &2 - x < pi / &2 - y <=> y < x`] THEN
REWRITE_TAC[ATN_MONO_LT_EQ] THEN
ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_MUL] THEN
ASM_SIMP_TAC[REAL_FIELD `&0 < z ==> w / z * b * z = b * w`] THEN
ASM_REAL_ARITH_TAC]);;
let WEDGE_LUNE_GE = prove
(`!v0 v1 w1 w2.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2} /\
&0 < azim v0 v1 w1 w2 /\ azim v0 v1 w1 w2 < pi
==> {x | &0 <= azim v0 v1 w1 x /\
azim v0 v1 w1 x <= azim v0 v1 w1 w2} =
aff_ge {v0,v1} {w1,w2}`,
let WEDGE_LUNE = prove
(`!v0 v1 w1 w2.
~coplanar{v0,v1,w1,w2} /\ azim v0 v1 w1 w2 < pi
==> wedge v0 v1 w1 w2 = aff_gt {v0,v1} {w1,w2}`,
let WEDGE = prove
(`wedge v1 v2 w1 w2 =
if collinear{v1,v2,w1} \/ collinear{v1,v2,w2} then {}
else
let z = v2 - v1 in
let u1 = w1 - v1 in
let u2 = w2 - v1 in
let n = z cross u1 in
let d = n dot u2 in
if w2
IN (aff_ge {v1,v2} {w1}) then {}
else if w2
IN (aff_lt {v1,v2} {w1}) then aff_gt {v1,v2,w1} {v1 + n}
else if d > &0 then aff_gt {v1,v2} {w1,w2}
else (:real^3)
DIFF aff_ge {v1,v2} {w1,w2}`,
REPEAT GEN_TAC THEN COND_CASES_TAC THENL
[FIRST_X_ASSUM DISJ_CASES_TAC THEN
ASM_SIMP_TAC[
WEDGE_DEGENERATE];
POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC] THEN
ASM_SIMP_TAC[GSYM
AZIM_EQ_0_GE_ALT] THEN
ASM_CASES_TAC `azim v1 v2 w1 w2 = &0` THENL
[ASM_REWRITE_TAC[wedge] THEN
ASM_REWRITE_TAC[
REAL_LT_ANTISYM;
LET_DEF;
LET_END_DEF;
EMPTY_GSPEC];
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM
AZIM_EQ_PI_ALT] THEN
ASM_CASES_TAC `azim v1 v2 w1 w2 = pi` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
LET_DEF;
LET_END_DEF] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
GEOM_ORIGIN_TAC `v1:real^3` THEN
REWRITE_TAC[
VECTOR_ADD_RID; TRANSLATION_INVARIANTS `v1:real^3`] THEN
REWRITE_TAC[
VECTOR_SUB_RZERO;
VECTOR_ADD_LID] THEN
GEOM_BASIS_MULTIPLE_TAC 3 `v2:real^3` THEN
X_GEN_TAC `v2:real` THEN
GEN_REWRITE_TAC LAND_CONV [REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
(STRIP_TAC THENL
[ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
INSERT_AC;
COLLINEAR_2]; ALL_TAC]) THEN
ASM_SIMP_TAC[
AZIM_SPECIAL_SCALE;
COLLINEAR_SPECIAL_SCALE;
REAL_LT_IMP_NZ;
WEDGE_SPECIAL_SCALE] THEN
(REPEAT GEN_TAC THEN
MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
[ASM_REWRITE_TAC[
COLLINEAR_2;
INSERT_AC] THEN NO_TAC; ALL_TAC])
[`w1:real^3 = vec 0`; `w2:real^3 = vec 0`; `w1:real^3 = basis 3`;
`w2:real^3 = basis 3`] THEN
ASM_CASES_TAC `w1:real^3 = v2 % basis 3` THENL
[ASM_REWRITE_TAC[
COLLINEAR_LEMMA] THEN MESON_TAC[]; ALL_TAC] THEN
ASM_CASES_TAC `w2:real^3 = v2 % basis 3` THENL
[ASM_REWRITE_TAC[
COLLINEAR_LEMMA] THEN MESON_TAC[]; ALL_TAC])
THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
EXTENSION] THEN X_GEN_TAC `y:real^3` THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`(dropout 3 (y:real^3))
IN
aff_gt {vec 0:real^2,dropout 3 (w1:real^3)}
{rotate2d (pi / &2) (dropout 3 (w1:real^3))}` THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE LAND_CONV [
AZIM_ARG]) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE (RAND_CONV o LAND_CONV)
[
AZIM_ARG]) THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
[
COLLINEAR_BASIS_3])) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN
REWRITE_TAC[wedge;
IN_ELIM_THM;
AZIM_ARG;
COLLINEAR_BASIS_3] THEN
SPEC_TAC(`(dropout 3:real^3->real^2) y`,`x:real^2`) THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w2`,`v2:real^2`) THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w1`,`v1:real^2`) THEN
GEOM_BASIS_MULTIPLE_TAC 1 `v1:complex` THEN
X_GEN_TAC `v:real` THEN GEN_REWRITE_TAC LAND_CONV [
REAL_LE_LT] THEN
ASM_CASES_TAC `v = &0` THEN ASM_REWRITE_TAC[
VECTOR_MUL_LZERO] THEN
REWRITE_TAC[
COMPLEX_CMUL;
COMPLEX_BASIS;
COMPLEX_VEC_0] THEN
SIMP_TAC[
ARG_DIV_CX;
COMPLEX_MUL_RID] THEN
REWRITE_TAC[real;
RE_DIV_CX;
IM_DIV_CX;
CX_INJ] THEN
ASM_SIMP_TAC[
REAL_LT_LDIV_EQ;
REAL_EQ_LDIV_EQ;
REAL_MUL_LZERO] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
ARG_LT_PI;
ROTATE2D_PI2] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AFF_GT_2_1 o rand o rand o snd) THEN
ASM_REWRITE_TAC[
DISJOINT_INSERT;
DISJOINT_EMPTY;
IN_SING] THEN
ANTS_TAC THENL
[CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
ASM_REWRITE_TAC[
COMPLEX_ENTIRE;
II_NZ;
CX_INJ] THEN
DISCH_THEN(MP_TAC o AP_TERM `Re`) THEN
REWRITE_TAC[
RE_MUL_II;
RE_CX;
IM_CX] THEN ASM_REAL_ARITH_TAC;
DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[
COMPLEX_CMUL;
IN_ELIM_THM;
COMPLEX_MUL_RZERO] THEN
ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?b c a. P a b c)`] THEN
REWRITE_TAC[REAL_ARITH `t1 + t2 = &1 <=> t1 = &1 - t2`] THEN
REWRITE_TAC[
RIGHT_EXISTS_AND_THM;
UNWIND_THM2;
COMPLEX_ADD_LID] THEN
EQ_TAC THENL
[DISCH_TAC THEN
MAP_EVERY EXISTS_TAC [`Re x / v`; `Im x / v`] THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
COMPLEX_EQ;
IM_ADD;
RE_ADD] THEN
REWRITE_TAC[
RE_MUL_CX;
IM_MUL_CX;
RE_CX;
IM_CX;
RE_II;
IM_II] THEN
UNDISCH_TAC `~(v = &0)` THEN CONV_TAC REAL_FIELD;
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`s:real`; `t:real`] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[
COMPLEX_EQ;
IM_ADD;
RE_ADD] THEN
REWRITE_TAC[
RE_MUL_CX;
IM_MUL_CX;
RE_CX;
IM_CX;
RE_II;
IM_II] THEN
ASM_SIMP_TAC[
REAL_MUL_RZERO; REAL_MUL_LID;
REAL_LT_MUL; REAL_ADD_LID;
REAL_MUL_LZERO] THEN
MAP_EVERY UNDISCH_TAC [`&0 < v`; `&0 < t`] THEN
CONV_TAC REAL_FIELD];
ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AFF_GT_3_1 o rand o rand o snd) THEN
ANTS_TAC THENL
[REWRITE_TAC[SET_RULE
`
DISJOINT {a,b,c} {x} <=> ~(x = a) /\ ~(x = b) /\ ~(x = c)`] THEN
ASM_SIMP_TAC[
CROSS_EQ_0;
CROSS_EQ_SELF;
VECTOR_MUL_EQ_0;
REAL_LT_IMP_NZ;
REAL_LT_IMP_NZ;
BASIS_NONZERO; DIMINDEX_3;
ARITH;
COLLINEAR_SPECIAL_SCALE];
DISCH_THEN SUBST1_TAC] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AFF_GT_2_1 o rand o lhand o snd) THEN
REWRITE_TAC[
ROTATE2D_PI2] THEN ANTS_TAC THENL
[REWRITE_TAC[SET_RULE `
DISJOINT {a,b} {x} <=> ~(x = a) /\ ~(x = b)`] THEN
REWRITE_TAC[
COMPLEX_ENTIRE; COMPLEX_RING `ii * x = x <=> x = Cx(&0)`;
COMPLEX_VEC_0;
II_NZ] THEN
ASM_REWRITE_TAC[GSYM
COMPLEX_VEC_0; GSYM
COLLINEAR_BASIS_3];
DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[
IN_ELIM_THM;
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
ONCE_REWRITE_TAC[MESON[]
`(?a b c d. P a b c d) <=> (?d c b a. P a b c d)`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `s + t = &1 <=> s = &1 - t`] THEN
REWRITE_TAC[
UNWIND_THM2;
RIGHT_EXISTS_AND_THM] THEN
ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
REWRITE_TAC[
UNWIND_THM2;
RIGHT_EXISTS_AND_THM] THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM] THEN
SIMP_TAC[
CART_EQ;
FORALL_2;
FORALL_3; DIMINDEX_2; DIMINDEX_3;
dropout;
LAMBDA_BETA;
BASIS_COMPONENT; ARITH;
REAL_MUL_RID;
VECTOR_MUL_COMPONENT;
VEC_COMPONENT;
REAL_MUL_RZERO;
UNWIND_THM1;
VECTOR_ADD_COMPONENT; cross;
VECTOR_3;
REWRITE_RULE[
RE_DEF;
IM_DEF]
RE_MUL_II;
REWRITE_RULE[
RE_DEF;
IM_DEF]
IM_MUL_II;
REAL_ADD_LID;
REAL_MUL_LZERO;
REAL_SUB_REFL;
REAL_ADD_RID;
REAL_SUB_LZERO;
REAL_SUB_RZERO] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `s:real` THEN
REWRITE_TAC[
RIGHT_EXISTS_AND_THM] THEN
ASM_SIMP_TAC[
EXISTS_REFL; REAL_FIELD
`&0 < v ==> (x = a * v + b <=> a = (x - b) / v)`] THEN
REWRITE_TAC[
REAL_MUL_RNEG; REAL_MUL_ASSOC] THEN EQ_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `t / v2:real`; EXISTS_TAC `t * v2:real`] THEN
ASM_SIMP_TAC[
REAL_DIV_RMUL;
REAL_LT_DIV;
REAL_LT_IMP_NZ;
REAL_LT_MUL];
ALL_TAC] THEN
REWRITE_TAC[
CROSS_LMUL] THEN
SIMP_TAC[cross;
BASIS_COMPONENT; DIMINDEX_3; ARITH;
DOT_3;
VECTOR_3;
VECTOR_MUL_COMPONENT;
REAL_MUL_LZERO;
REAL_SUB_RZERO;
REAL_NEG_0;
REAL_MUL_RZERO;
REAL_SUB_LZERO; REAL_MUL_LID;
REAL_ADD_RID] THEN
REWRITE_TAC[REAL_ARITH
`(v * --x2) * y1 + (v * x1) * y2 > &0 <=> &0 < v * (x1 * y2 - x2 * y1)`] THEN
ASM_SIMP_TAC[
REAL_LT_MUL_EQ;
REAL_SUB_LT] THEN
REWRITE_TAC[
AZIM_ARG;
COLLINEAR_BASIS_3] THEN STRIP_TAC THEN
SUBGOAL_THEN
`w1$2 * w2$1 < w1$1 * w2$2 <=>
Arg(dropout 3 (w2:real^3) / dropout 3 (w1:real^3)) < pi`
SUBST1_TAC THENL
[MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `&0 < Im(dropout 3 (w2:real^3) / dropout 3 (w1:real^3))` THEN
CONJ_TAC THENL
[REWRITE_TAC[
IM_COMPLEX_DIV_GT_0] THEN
REWRITE_TAC[
complex_mul; cnj;
RE_DEF;
IM_DEF; complex] THEN
SIMP_TAC[dropout;
VECTOR_2;
LAMBDA_BETA; DIMINDEX_3; ARITH;
DIMINDEX_2] THEN
REAL_ARITH_TAC;
REWRITE_TAC[GSYM
ARG_LT_PI] THEN ASM_MESON_TAC[
ARG_LT_NZ]];
ALL_TAC] THEN
COND_CASES_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand)
AFF_GT_SPECIAL_SCALE o rand o snd) THEN
ASM_REWRITE_TAC[
FINITE_INSERT;
FINITE_EMPTY;
IN_INSERT;
NOT_IN_EMPTY] THEN
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC
WEDGE_LUNE THEN
ASM_SIMP_TAC[GSYM
AZIM_EQ_0_PI_EQ_COPLANAR;
COLLINEAR_BASIS_3] THEN
ASM_REWRITE_TAC[
AZIM_ARG];
ALL_TAC] THEN
REWRITE_TAC[wedge] THEN
GEN_REWRITE_TAC (funpow 3 RAND_CONV) [SET_RULE `{a,b} = {b,a}`] THEN
W(MP_TAC o PART_MATCH (rand o rand)
WEDGE_LUNE_GE o rand o rand o snd) THEN
ASM_SIMP_TAC[
COLLINEAR_SPECIAL_SCALE;
REAL_LT_IMP_NZ;
AZIM_SPECIAL_SCALE] THEN
ASM_REWRITE_TAC[
AZIM_ARG;
COLLINEAR_BASIS_3] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[
ARG_LT_NZ] THEN
ONCE_REWRITE_TAC[GSYM
ARG_INV_EQ_0] THEN
ASM_REWRITE_TAC[
COMPLEX_INV_DIV] THEN
ONCE_REWRITE_TAC[GSYM
COMPLEX_INV_DIV] THEN
ASM_SIMP_TAC[
ARG_INV; GSYM
ARG_EQ_0] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
EXTENSION;
IN_DIFF;
IN_UNIV;
IN_ELIM_THM;
ARG] THEN
REWRITE_TAC[
REAL_NOT_LE] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w1`,`w:complex`) THEN
SPEC_TAC(`(dropout 3:real^3->real^2) w2`,`z:complex`) THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `x3:real^3` THEN
SPEC_TAC(`(dropout 3:real^3->real^2) x3`,`x:complex`) THEN
GEN_TAC THEN REWRITE_TAC[
COMPLEX_VEC_0] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
COMPLEX_VEC_0]) THEN
ASM_CASES_TAC `x = Cx(&0)` THEN ASM_REWRITE_TAC[] THENL
[ASM_REWRITE_TAC[
complex_div;
COMPLEX_MUL_LZERO;
REAL_NOT_LT;
ARG;
ARG_0];
ALL_TAC] THEN
ASM_REWRITE_TAC[
ARG_LT_NZ] THEN
MAP_EVERY UNDISCH_TAC
[`~(Arg (z / w) < pi)`;
`~(Arg (z / w) = pi)`;
`~(Arg (z / w) = &0)`;
`~(x = Cx (&0))`;
`~(w = Cx (&0))`;
`~(z = Cx (&0))`] THEN
POP_ASSUM_LIST(K ALL_TAC) THEN REWRITE_TAC[GSYM
COMPLEX_VEC_0] THEN
GEOM_BASIS_MULTIPLE_TAC 1 `w:complex` THEN
X_GEN_TAC `w:real` THEN GEN_REWRITE_TAC LAND_CONV [
REAL_LE_LT] THEN
ASM_CASES_TAC `w = &0` THEN ASM_REWRITE_TAC[
VECTOR_MUL_LZERO] THEN
REWRITE_TAC[
COMPLEX_CMUL;
COMPLEX_BASIS;
COMPLEX_VEC_0] THEN
SIMP_TAC[
ARG_DIV_CX;
COMPLEX_MUL_RID] THEN
REWRITE_TAC[real;
RE_DIV_CX;
IM_DIV_CX;
CX_INJ] THEN
SIMP_TAC[
complex_div;
ARG_MUL_CX] THEN
SIMP_TAC[
ARG_INV; GSYM
ARG_EQ_0;
ARG_INV_EQ_0] THEN
DISCH_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[GSYM
complex_div] THEN
ASM_CASES_TAC `Arg x = &0` THEN ASM_REWRITE_TAC[] THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
ARG_EQ_0]) THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
REAL] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
complex_div;
CX_INJ] THEN
ASM_SIMP_TAC[
ARG_MUL_CX;
REAL_LT_LE] THEN
ASM_SIMP_TAC[
ARG_INV; GSYM
ARG_EQ_0];
ALL_TAC] THEN
REWRITE_TAC[IMP_IMP; GSYM
CONJ_ASSOC] THEN
SIMP_TAC[
PI_POS; REAL_ARITH
`&0 < pi ==> (~(z = &0) /\ ~(z = pi) /\ ~(z < pi) <=> pi < z)`] THEN
STRIP_TAC THEN REWRITE_TAC[
REAL_LT_SUB_RADD] THEN
DISJ_CASES_TAC(REAL_ARITH `Arg z <= Arg x \/ Arg x < Arg z`) THENL
[ASM_REWRITE_TAC[GSYM
REAL_NOT_LE] THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
ASM_SIMP_TAC[GSYM
ARG_LE_DIV_SUM] THEN
SIMP_TAC[
ARG;
REAL_LT_IMP_LE];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(ISPECL [`x:complex`; `z:complex`]
ARG_LE_DIV_SUM) THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN DISCH_THEN SUBST1_TAC THEN
MATCH_MP_TAC(REAL_ARITH
`&0 <= x /\ ~(x = &0) /\ y = k - z ==> k < y + x + z`) THEN
ASM_REWRITE_TAC[
ARG] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM
COMPLEX_INV_DIV] THEN
MATCH_MP_TAC
ARG_INV THEN REWRITE_TAC[
REAL] THEN
DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
ABBREV_TAC `t = Re(z / x)` THEN UNDISCH_TAC `Arg x < Arg z` THEN
UNDISCH_TAC `z / x = Cx t` THEN
ASM_SIMP_TAC[COMPLEX_FIELD
`~(x = Cx(&0)) ==> (z / x = t <=> z = t * x)`] THEN
ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[
COMPLEX_MUL_LZERO] THEN
ASM_SIMP_TAC[
ARG_MUL_CX;
REAL_LT_LE]);;
let COPLANAR_AZIM_EQ = prove
(`!v0 v1 w1 a.
(collinear{v0,v1,w1} ==> ~(a = &0))
==> coplanar {z | azim v0 v1 w1 z = a}`,
let delta_x = new_definition
`delta_x x1 x2 x3 x4 x5 x6 =
x1*x4*(--x1 + x2 + x3 -x4 + x5 + x6) +
x2*x5*(x1 - x2 + x3 + x4 -x5 + x6) +
x3*x6*(x1 + x2 - x3 + x4 + x5 - x6)
-x2*x3*x4 - x1*x3*x5 - x1*x2*x6 -x4*x5*x6:real`;;let VOLUME_OF_CLOSED_TETRAHEDRON = prove
(`!x1 x2 x3 x4:real^3.
measure(convex hull {x1,x2,x3,x4}) =
sqrt(
delta_x (dist(x1,x2) pow 2) (dist(x1,x3) pow 2) (dist(x1,x4) pow 2)
(dist(x3,x4) pow 2) (dist(x2,x4) pow 2) (dist(x2,x3) pow 2))
/ &12`,
let VOLUME_OF_TETRAHEDRON = prove
(`!v1 v2 v3 v4:real^3.
measure(conv0 {v1,v2,v3,v4}) =
let x12 = dist(v1,v2) pow 2 in
let x13 = dist(v1,v3) pow 2 in
let x14 = dist(v1,v4) pow 2 in
let x23 = dist(v2,v3) pow 2 in
let x24 = dist(v2,v4) pow 2 in
let x34 = dist(v3,v4) pow 2 in
sqrt(
delta_x x12 x13 x14 x34 x24 x23)/(&12)`,
let VOLUME_BALL = prove
(`!z:real^3 r. &0 <= r ==> measure(ball(z,r)) = &4 / &3 * pi * r pow 3`,
let VOLUME_FRUSTT_STRONG = prove
(`!v0 v1:real^3 h a.
&0 < a
==> bounded(frustt v0 v1 h a) /\
convex(frustt v0 v1 h a) /\
measurable(frustt v0 v1 h a) /\
measure(frustt v0 v1 h a) =
if v1 = v0 \/ &1 <= a \/ h < &0 then &0
else pi * ((h / a) pow 2 - h pow 2) * h / &3`,
let VOLUME_FRUSTT = prove
(`!v0 v1:real^3 h a.
&0 < a
==> measurable(frustt v0 v1 h a) /\
measure(frustt v0 v1 h a) =
if v1 = v0 \/ &1 <= a \/ h < &0 then &0
else pi * ((h / a) pow 2 - h pow 2) * h / &3`,
let MEASURE_ELLIPSOID = prove
(`!t r. &0 <= r
==> measurable(ellipsoid t r) /\
measure(ellipsoid t r) =
abs(t$1 * t$2 * t$3) * &4 / &3 * pi * r pow 3`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_X_ASSUM(SUBST1_TAC o SYM o
SPEC `vec 0:real^3` o MATCH_MP
VOLUME_BALL) THEN
REWRITE_TAC[normball; ellipsoid] THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
REWRITE_TAC[GSYM ball] THEN MATCH_MP_TAC
MEASURE_SCALE THEN
REWRITE_TAC[
MEASURABLE_BALL]);;
let MEASURE_OPEN_SECTOR_LT = prove
(`!t r. &0 <= t /\ t <= &2 * pi
==> measure {x:real^2 | norm(x) < r /\ &0 < Arg x /\ Arg x < t} =
if &0 <= r then t * r pow 2 / &2 else &0`,
let HAS_MEASURE_LUNE = prove
(`!z:real^3 w r w1 w2.
&0 <= r /\ ~(w = z) /\
~collinear {z,w,w1} /\ ~collinear {z,w,w2} /\ ~(dihV z w w1 w2 = pi)
==> (ball(z,r)
INTER aff_gt {z,w} {w1,w2})
has_measure (dihV z w w1 w2 * &2 * r pow 3 / &3)`,
GEOM_ORIGIN_TAC `z:real^3` THEN
GEOM_BASIS_MULTIPLE_TAC 3 `w:real^3` THEN
X_GEN_TAC `w:real` THEN GEN_REWRITE_TAC LAND_CONV [
REAL_LE_LT] THEN
ASM_CASES_TAC `w = &0` THEN ASM_REWRITE_TAC[] THENL
[ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
DISCH_TAC THEN REPEAT GEN_TAC THEN
ASM_SIMP_TAC[
DIHV_SPECIAL_SCALE] THEN
MP_TAC(ISPECL [`{}:real^3->bool`; `{w1:real^3,w2:real^3}`;
`w:real`; `basis 3:real^3`]
AFF_GT_SPECIAL_SCALE) THEN
ASM_CASES_TAC `w1:real^3 = vec 0` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_CASES_TAC `w2:real^3 = vec 0` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_REWRITE_TAC[
FINITE_INSERT;
FINITE_EMPTY;
IN_INSERT;
NOT_IN_EMPTY] THEN
ASM_CASES_TAC `w1:real^3 = w % basis 3` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_CASES_TAC `w2:real^3 = w % basis 3` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_SIMP_TAC[
COLLINEAR_SPECIAL_SCALE] THEN
ASM_CASES_TAC `w1:real^3 = basis 3` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_CASES_TAC `w2:real^3 = basis 3` THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
ASM_SIMP_TAC[
VECTOR_MUL_EQ_0;
REAL_LT_IMP_NZ] THEN STRIP_TAC THEN
ASM_CASES_TAC `azim (vec 0) (basis 3) w1 w2 = &0` THENL
[MP_TAC(ASSUME `azim (vec 0) (basis 3) w1 w2 = &0`) THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_DIVH o lhs o lhand o snd) THEN
ASM_REWRITE_TAC[
PI_POS] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
REAL_MUL_LZERO;
HAS_MEASURE_0] THEN
MATCH_MP_TAC
COPLANAR_IMP_NEGLIGIBLE THEN
MATCH_MP_TAC
COPLANAR_SUBSET THEN
EXISTS_TAC `affine hull {vec 0:real^3,basis 3,w1,w2}` THEN
CONJ_TAC THENL
[ASM_MESON_TAC[
COPLANAR_AFFINE_HULL_COPLANAR;
AZIM_EQ_0_PI_IMP_COPLANAR];
ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE `t
SUBSET u ==> (s
INTER t)
SUBSET u`) THEN
SIMP_TAC[
aff_gt_def;
AFFSIGN;
sgn_gt;
AFFINE_HULL_FINITE;
FINITE_INSERT;
FINITE_EMPTY] THEN
REWRITE_TAC[SET_RULE `{a,b}
UNION {c,d} = {a,b,c,d}`] THEN
REWRITE_TAC[
SUBSET;
IN_ELIM_THM] THEN GEN_TAC THEN
MATCH_MP_TAC
MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `&0 < azim (vec 0) (basis 3) w1 w2` ASSUME_TAC THENL
[ASM_REWRITE_TAC[
REAL_LT_LE; azim]; ALL_TAC] THEN
ASM_CASES_TAC `azim (vec 0) (basis 3) w1 w2 < pi` THENL
[ASM_SIMP_TAC[GSYM
AZIM_DIHV_SAME; GSYM
WEDGE_LUNE_GT] THEN
ASM_SIMP_TAC[
HAS_MEASURE_MEASURABLE_MEASURE;
MEASURABLE_BALL_WEDGE;
VOLUME_BALL_WEDGE];
ALL_TAC] THEN
ASM_CASES_TAC `azim (vec 0) (basis 3) w1 w2 = pi` THENL
[MP_TAC(ISPECL [`vec 0:real^3`; `basis 3:real^3`; `w1:real^3`; `w2:real^3`]
AZIM_DIVH) THEN
ASM_REWRITE_TAC[
REAL_LT_REFL] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`dihV (vec 0) (basis 3) w1 w2 = azim (vec 0) (basis 3) w2 w1`
SUBST1_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_COMPL o rand o snd) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `x:real = y - z <=> z = y - x`] THEN
MATCH_MP_TAC
AZIM_DIHV_COMPL THEN
ASM_REWRITE_TAC[GSYM
REAL_NOT_LT];
ALL_TAC] THEN
SUBGOAL_THEN `&0 < azim (vec 0) (basis 3) w2 w1 /\
azim (vec 0) (basis 3) w2 w1 < pi`
ASSUME_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand)
AZIM_COMPL o lhand o rand o snd) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
MP_TAC(ISPECL [`vec 0:real^3`; `basis 3:real^3`; `w1:real^3`; `w2:real^3`]
azim) THEN
REWRITE_TAC[
CONJ_ASSOC] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBST1_TAC(SET_RULE `{w1:real^3,w2} = {w2,w1}`) THEN
ASM_SIMP_TAC[GSYM
AZIM_DIHV_SAME; GSYM
WEDGE_LUNE_GT] THEN
ASM_SIMP_TAC[
HAS_MEASURE_MEASURABLE_MEASURE;
MEASURABLE_BALL_WEDGE;
VOLUME_BALL_WEDGE]);;
let AFF_GT_SHUFFLE = prove
(`!s t v:real^N.
FINITE s /\
FINITE t /\
vec 0
IN s /\ ~(vec 0
IN t) /\
~(v
IN s) /\ ~(--v
IN s) /\ ~(v
IN t)
==> aff_gt (v
INSERT s) t =
aff_gt s (v
INSERT t)
UNION
aff_gt s (--v
INSERT t)
UNION
aff_gt s t`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[
aff_gt_def;
AFFSIGN_ALT;
sgn_gt] THEN
REWRITE_TAC[SET_RULE `(v
INSERT s)
UNION t = v
INSERT (s
UNION t)`;
SET_RULE `s
UNION (v
INSERT t) = v
INSERT (s
UNION t)`] THEN
ASM_SIMP_TAC[
FINITE_INSERT;
FINITE_UNION;
AFFINE_HULL_FINITE_STEP_GEN;
RIGHT_EXISTS_AND_THM;
REAL_LT_ADD;
REAL_HALF;
FINITE_EMPTY] THEN
REWRITE_TAC[
IN_INSERT] THEN
ASM_SIMP_TAC[SET_RULE
`~(a
IN s)
==> ((w
IN s
UNION t ==> w = a \/ w
IN t ==> P w) <=>
(w
IN t ==> P w))`] THEN
REWRITE_TAC[SET_RULE `x
IN (s
UNION t)
==> x
IN t ==> P x <=> x
IN t ==> P x`] THEN
REWRITE_TAC[
EXTENSION;
IN_UNION;
IN_ELIM_THM] THEN
X_GEN_TAC `y:real^N` THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `v:real` ASSUME_TAC) THEN
ASM_CASES_TAC `&0 < v` THENL
[DISJ1_TAC THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[];
DISJ2_TAC] THEN
ASM_CASES_TAC `v = &0` THENL
[DISJ2_TAC THEN
FIRST_ASSUM(fun th -> MP_TAC th THEN MATCH_MP_TAC
MONO_EXISTS) THEN
ASM_REWRITE_TAC[
REAL_SUB_RZERO;
VECTOR_MUL_LZERO;
VECTOR_SUB_RZERO];
DISJ1_TAC] THEN
EXISTS_TAC `--v:real` THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `f:real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\x:real^N. if x = vec 0 then f(x) + &2 * v else f(x)` THEN
REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[];
ASM_SIMP_TAC[
SUM_CASES_1;
FINITE_UNION;
IN_UNION] THEN REAL_ARITH_TAC;
REWRITE_TAC[VECTOR_ARITH `--a % --x:real^N = a % x`] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
MATCH_MP_TAC
VSUM_EQ THEN REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[
VECTOR_MUL_RZERO]];
DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
[DISCH_THEN(X_CHOOSE_THEN `a:real`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `f:real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `--a:real` THEN
EXISTS_TAC `\x:real^N. if x = vec 0 then &2 * a + f(vec 0) else f x` THEN
ASM_SIMP_TAC[
SUM_CASES_1;
FINITE_UNION;
IN_UNION] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH `y - --a % v:real^N = y - a % --v`] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
MATCH_MP_TAC
VSUM_EQ THEN REPEAT GEN_TAC THEN REWRITE_TAC[] THEN
DISCH_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[
VECTOR_MUL_RZERO];
GEN_REWRITE_TAC RAND_CONV [
SWAP_EXISTS_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN REPEAT STRIP_TAC THEN
EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[
REAL_SUB_RZERO] THEN
VECTOR_ARITH_TAC]]);;
let MEASURE_LUNE_DECOMPOSITION = prove
(`!v1 v2 v3:real^3.
&0 <= r /\ ~coplanar {vec 0, v1, v2, v3}
==> measure(ball(vec 0,r)
INTER aff_gt {vec 0} {v1,v2,v3}) +
measure(ball(vec 0,r)
INTER aff_gt {vec 0} {--v1,v2,v3}) =
dihV (vec 0) v1 v2 v3 * &2 * r pow 3 / &3`,
let SOLID_TRIANGLE_CONGRUENT_NEG = prove
(`!r v1 v2 v3:real^N.
measure(ball(vec 0,r)
INTER aff_gt {vec 0} {--v1, --v2, --v3}) =
measure(ball(vec 0,r)
INTER aff_gt {vec 0} {v1, v2, v3})`,
REPEAT GEN_TAC THEN
SUBGOAL_THEN
`ball(vec 0:real^N,r)
INTER aff_gt {vec 0} {--v1, --v2, --v3} =
IMAGE (--)
(ball(vec 0,r)
INTER aff_gt {vec 0} {v1, v2, v3})`
SUBST1_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
MEASURE_ORTHOGONAL_IMAGE_EQ THEN
REWRITE_TAC[
ORTHOGONAL_TRANSFORMATION; linear;
NORM_NEG] THEN
CONJ_TAC THEN VECTOR_ARITH_TAC] THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SURJECTIVE_IMAGE_EQ THEN
CONJ_TAC THENL [MESON_TAC[
VECTOR_NEG_NEG]; ALL_TAC] THEN
REWRITE_TAC[
IN_INTER;
IN_BALL_0;
NORM_NEG] THEN
REWRITE_TAC[
AFFSIGN_ALT;
aff_gt_def;
sgn_gt;
IN_ELIM_THM] THEN
REWRITE_TAC[SET_RULE `{a}
UNION {b,c,d} = {a,b,d,c}`] THEN
REWRITE_TAC[SET_RULE `x
IN {a} <=> a = x`] THEN
ASM_SIMP_TAC[
FINITE_INSERT;
FINITE_UNION;
AFFINE_HULL_FINITE_STEP_GEN;
RIGHT_EXISTS_AND_THM;
REAL_LT_ADD;
REAL_HALF;
FINITE_EMPTY] THEN
ASM_REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_SUB_RZERO] THEN
REWRITE_TAC[VECTOR_ARITH `vec 0:real^N = --x <=> vec 0 = x`] THEN
REWRITE_TAC[VECTOR_ARITH `--x - a % --w:real^N = --(x - a % w)`] THEN
REWRITE_TAC[
VECTOR_NEG_EQ_0]);;
let VOLUME_SOLID_TRIANGLE = prove
(`!r v0 v1 v2 v3:real^3.
&0 < r /\ ~coplanar{v0, v1, v2, v3}
==> measure(ball(v0,r)
INTER aff_gt {v0} {v1,v2,v3}) =
let a123 = dihV v0 v1 v2 v3 in
let a231 = dihV v0 v2 v3 v1 in
let a312 = dihV v0 v3 v1 v2 in
(a123 + a231 + a312 - pi) * r pow 3 / &3`,
let tac convl =
W(MP_TAC o PART_MATCH (lhs o rand)
MEASURE_BALL_AFF_GT_SHUFFLE o
convl o lhand o lhand o snd) THEN
ASM_REWRITE_TAC[
UNION_EMPTY;
IN_INSERT;
IN_UNION;
NOT_IN_EMPTY] THEN
REWRITE_TAC[SET_RULE `(a
INSERT s)
UNION t = a
INSERT (s
UNION t)`] THEN
ASM_SIMP_TAC[
UNION_EMPTY;
REAL_LT_IMP_LE] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[DISCH_THEN(STRIP_THM_THEN SUBST_ALL_TAC) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INSERT_AC]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
COPLANAR_3]) THEN
FIRST_ASSUM CONTR_TAC;
MATCH_MP_TAC
NOT_COPLANAR_0_4_IMP_INDEPENDENT THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INSERT_AC]) THEN
ASM_REWRITE_TAC[
INSERT_AC]];
DISCH_THEN SUBST1_TAC] in
GEN_TAC THEN GEOM_ORIGIN_TAC `v0:real^3` THEN
CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`measure(ball(vec 0:real^3,r)
INTER aff_gt {vec 0,v1,v2,v3} {}) =
&4 / &3 * pi * r pow 3`
MP_TAC THENL
[MP_TAC(SPECL [`vec 0:real^3`; `r:real`]
VOLUME_BALL) THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN
MATCH_MP_TAC(SET_RULE `t =
UNIV ==> s
INTER t = s`) THEN
REWRITE_TAC[
AFF_GT_EQ_AFFINE_HULL] THEN
SIMP_TAC[
AFFINE_HULL_EQ_SPAN;
HULL_INC;
IN_INSERT;
SPAN_INSERT_0] THEN
REWRITE_TAC[SET_RULE `s =
UNIV <=>
UNIV SUBSET s`] THEN
MATCH_MP_TAC
CARD_GE_DIM_INDEPENDENT THEN
ASM_SIMP_TAC[
DIM_UNIV; DIMINDEX_3;
SUBSET_UNIV] THEN
ASM_SIMP_TAC[
NOT_COPLANAR_0_4_IMP_INDEPENDENT] THEN
SIMP_TAC[
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY] THEN
REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
MAP_EVERY (fun t ->
ASM_CASES_TAC t THENL
[FIRST_X_ASSUM SUBST_ALL_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INSERT_AC;
COPLANAR_3]) THEN
ASM_MESON_TAC[];
ASM_REWRITE_TAC[]])
[`v3:real^3 = v2`; `v3:real^3 = v1`; `v2:real^3 = v1`] THEN
CONV_TAC NUM_REDUCE_CONV;
ALL_TAC] THEN
SUBGOAL_THEN
`~(coplanar {vec 0:real^3,v1,v2,v3}) /\
~(coplanar {vec 0,--v1,v2,v3}) /\
~(coplanar {vec 0,v1,--v2,v3}) /\
~(coplanar {vec 0,--v1,--v2,v3}) /\
~(coplanar {vec 0,--v1,--v2,v3}) /\
~(coplanar {vec 0,--v1,v2,--v3}) /\
~(coplanar {vec 0,v1,--v2,--v3}) /\
~(coplanar {vec 0,--v1,--v2,--v3}) /\
~(coplanar {vec 0,--v1,--v2,--v3})`
STRIP_ASSUME_TAC THENL
[REPLICATE_TAC 3
(REWRITE_TAC[
COPLANAR_INSERT_0_NEG] THEN
ONCE_REWRITE_TAC[SET_RULE `{vec 0,a,b,c} = {vec 0,b,c,a}`]) THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
MAP_EVERY tac
[I; lhand; rand;
lhand o lhand; rand o lhand; lhand o rand; rand o rand] THEN
MP_TAC(ISPECL [`v1:real^3`; `v2:real^3`; `v3:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
MP_TAC(ISPECL [`v2:real^3`; `v3:real^3`; `v1:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
MP_TAC(ISPECL [`v3:real^3`; `v1:real^3`; `v2:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
MP_TAC(ISPECL [`--v1:real^3`; `--v2:real^3`; `--v3:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
MP_TAC(ISPECL [`--v2:real^3`; `--v3:real^3`; `--v1:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
MP_TAC(ISPECL [`--v3:real^3`; `--v1:real^3`; `--v2:real^3`]
MEASURE_LUNE_DECOMPOSITION) THEN
ASM_REWRITE_TAC[
VECTOR_NEG_NEG] THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
INSERT_AC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INSERT_AC]) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
DIHV_NEG_0] THEN
REWRITE_TAC[
SOLID_TRIANGLE_CONGRUENT_NEG] THEN
REWRITE_TAC[
INSERT_AC] THEN REAL_ARITH_TAC);;
let SLICE_SPECIAL_WEDGE = prove
(`!w1 w2.
~collinear {vec 0, basis 3, w1} /\ ~collinear {vec 0, basis 3, w2}
==> slice 3 t (wedge (vec 0) (basis 3) w1 w2) =
{z | &0 < Arg(z / dropout 3 w1) /\
Arg(z / dropout 3 w1) < Arg(dropout 3 w2 / dropout 3 w1)}`,
let VOLUME_FRUSTT_WEDGE = prove
(`!v0 v1:real^3 w1 w2 h a.
&0 < a /\ ~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> bounded(frustt v0 v1 h a
INTER wedge v0 v1 w1 w2) /\
measurable(frustt v0 v1 h a
INTER wedge v0 v1 w1 w2) /\
measure(frustt v0 v1 h a
INTER wedge v0 v1 w1 w2) =
if &1 <= a \/ h < &0 then &0
else azim v0 v1 w1 w2 * ((h / a) pow 2 - h pow 2) * h / &6`,
let VOLUME_CONIC_CAP_COMPL = prove
(`!v0 v1:real^3 w1 w2 r a.
&0 <= r
==> measure(
conic_cap v0 v1 r a
INTER wedge v0 v1 w1 w2) +
measure(
conic_cap v0 v1 r (--a)
INTER wedge v0 v1 w1 w2) =
azim v0 v1 w1 w2 * &2 * r pow 3 / &3`,
let lemma = prove
(`!f:real^N->real^N s t t' u.
measurable(s) /\ measurable(t) /\ measurable(u) /\
orthogonal_transformation f /\
s SUBSET u /\ t' SUBSET u /\ s INTER t' = {} /\
negligible(u DIFF (s UNION t')) /\
((!y. ?x. f x = y) ==> IMAGE f t = t')
==> measure s + measure t = measure u`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `orthogonal_transformation(f:real^N->real^N)` THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_SURJECTIVE] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
EXISTS_TAC
`measure(s:real^N->bool) + measure(t':real^N->bool)` THEN
CONJ_TAC THENL [ASM_MESON_TAC[MEASURE_ORTHOGONAL_IMAGE_EQ]; ALL_TAC] THEN
W(MP_TAC o PART_MATCH (rhs o rand) MEASURE_DISJOINT_UNION o
lhand o snd) THEN
ASM_REWRITE_TAC[DISJOINT] THEN ANTS_TAC THENL
[ASM_MESON_TAC[MEASURABLE_LINEAR_IMAGE; ORTHOGONAL_TRANSFORMATION_LINEAR];
DISCH_THEN(SUBST1_TAC o SYM)] THEN
MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
NEGLIGIBLE_SUBSET)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]) in
REWRITE_TAC[conic_cap; rcone_gt; NORMBALL_BALL; rconesgn] THEN
GEOM_ORIGIN_TAC `v0:real^3` THEN
REWRITE_TAC[VECTOR_SUB_RZERO; DIST_0; real_gt] THEN
GEOM_BASIS_MULTIPLE_TAC 3 `v1:real^3` THEN
X_GEN_TAC `v1:real` THEN
GEN_REWRITE_TAC LAND_CONV [REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
STRIP_TAC THENL
[ASM_SIMP_TAC[VECTOR_MUL_LZERO; WEDGE_DEGENERATE; AZIM_DEGENERATE] THEN
REWRITE_TAC[INTER_EMPTY; MEASURE_EMPTY] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM VOLUME_BALL_WEDGE] THEN REPEAT STRIP_TAC THEN
ASM_CASES_TAC `collinear {vec 0:real^3,v1 % basis 3,w1}` THENL
[ASM_SIMP_TAC[WEDGE_DEGENERATE; AZIM_DEGENERATE] THEN
REWRITE_TAC[INTER_EMPTY; MEASURE_EMPTY] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM VOLUME_BALL_WEDGE] THEN REPEAT STRIP_TAC THEN
ASM_CASES_TAC `collinear {vec 0:real^3,v1 % basis 3,w2}` THENL
[ASM_SIMP_TAC[WEDGE_DEGENERATE; AZIM_DEGENERATE] THEN
REWRITE_TAC[INTER_EMPTY; MEASURE_EMPTY] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[WEDGE_SPECIAL_SCALE] THEN
MAP_EVERY UNDISCH_TAC
[`~collinear{vec 0:real^3,v1 % basis 3,w1}`;
`~collinear{vec 0:real^3,v1 % basis 3,w2}`] THEN
ASM_SIMP_TAC[COLLINEAR_SPECIAL_SCALE] THEN REPEAT DISCH_TAC THEN
REWRITE_TAC[NORM_MUL; DOT_RMUL] THEN
ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_ARITH
`&0 < v1 ==> n * (abs v1 * y) * a = v1 * n * y * a`] THEN
MATCH_MP_TAC lemma THEN
MP_TAC(ISPECL
[`vec 0:real^3`; `basis 3:real^3`; `w1:real^3`; `w2:real^3`;
`r:real`; `a:real`] MEASURABLE_CONIC_CAP_WEDGE) THEN
MP_TAC(ISPECL
[`vec 0:real^3`; `basis 3:real^3`; `w1:real^3`; `w2:real^3`;
`r:real`; `--a:real`] MEASURABLE_CONIC_CAP_WEDGE) THEN
REWRITE_TAC[conic_cap; rcone_gt; NORMBALL_BALL; rconesgn] THEN
REWRITE_TAC[VECTOR_SUB_RZERO; DIST_0; real_gt] THEN
REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[MEASURABLE_BALL_WEDGE] THEN
SIMP_TAC[NORM_BASIS; DOT_BASIS; DIMINDEX_3; ARITH; REAL_MUL_LID] THEN
EXISTS_TAC `(\x. vector[x$1; x$2; --(x$3)]):real^3->real^3` THEN
EXISTS_TAC `(ball(vec 0,r) INTER {x | norm x * a > x$3}) INTER
wedge (vec 0:real^3) (basis 3) w1 w2` THEN
CONJ_TAC THENL
[REWRITE_TAC[ORTHOGONAL_TRANSFORMATION; linear] THEN
REWRITE_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VECTOR_3; vector_norm; DOT_3;
VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REPEAT(GEN_TAC ORELSE CONJ_TAC ORELSE AP_TERM_TAC) THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_ELIM_THM; real_gt] THEN
MESON_TAC[REAL_LT_ANTISYM];
ALL_TAC] THEN
CONJ_TAC THENL
[MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `rcone_eq (vec 0:real^3) (basis 3) a` THEN
SIMP_TAC[NEGLIGIBLE_RCONE_EQ; BASIS_NONZERO; DIMINDEX_3; ARITH] THEN
REWRITE_TAC[SUBSET; rcone_eq; rconesgn; VECTOR_SUB_RZERO; DIST_0] THEN
SIMP_TAC[DOT_BASIS; NORM_BASIS; DIMINDEX_3; ARITH] THEN
REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN_INTER; IN_UNION] THEN
GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
ASM_REWRITE_TAC[] THEN
REWRITE_TAC[IN_INTER; IN_BALL_0; IN_ELIM_THM; VECTOR_3] THEN
X_GEN_TAC `x:real^3` THEN
SUBGOAL_THEN `norm(vector [x$1; x$2; --(x$3)]:real^3) = norm(x:real^3)`
SUBST1_TAC THENL
[REWRITE_TAC[NORM_EQ; DOT_3; VECTOR_3] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH `n * a > --x <=> n * --a < x`] THEN
MATCH_MP_TAC(TAUT `(a ==> (b <=> b')) ==> (a /\ b <=> a /\ b')`) THEN
STRIP_TAC THEN
REWRITE_TAC[COLLINEAR_BASIS_3; wedge; AZIM_ARG] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
SUBGOAL_THEN `(dropout 3 :real^3->real^2) (vector [x$1; x$2; --(x$3)]) =
(dropout 3 :real^3->real^2) x`
(fun th -> REWRITE_TAC[th]) THEN
SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; dropout; LAMBDA_BETA; ARITH;
VECTOR_3]);;
let VOLUME_CONIC_CAP_WEDGE = prove
(`!v0 v1:real^3 w1 w2 r a.
~collinear {v0,v1,w1} /\ ~collinear {v0,v1,w2}
==> bounded(
conic_cap v0 v1 r a
INTER wedge v0 v1 w1 w2) /\
measurable(
conic_cap v0 v1 r a
INTER wedge v0 v1 w1 w2) /\
measure(
conic_cap v0 v1 r a
INTER wedge v0 v1 w1 w2) =
if &1 < a \/ r < &0 then &0
else azim v0 v1 w1 w2 / &3 * (&1 - max a (-- &1)) * r pow 3`,
REWRITE_TAC[
BOUNDED_CONIC_CAP_WEDGE;
MEASURABLE_CONIC_CAP_WEDGE] THEN
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `&0 <= a` THEN
ASM_SIMP_TAC[
VOLUME_CONIC_CAP_WEDGE_MEDIUM;
REAL_ARITH `&0 <= a ==> abs a = a /\ max a (-- &1) = a`] THEN
MP_TAC(ISPECL [`v0:real^3`; `v1:real^3`; `w1:real^3`; `w2:real^3`;
`r:real`; `--a:real`]
VOLUME_CONIC_CAP_WEDGE_MEDIUM) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`v0:real^3`; `v1:real^3`; `w1:real^3`; `w2:real^3`;
`r:real`; `a:real`]
VOLUME_CONIC_CAP_COMPL) THEN
ASM_CASES_TAC `r < &0` THENL
[REWRITE_TAC[
conic_cap;
NORMBALL_BALL] THEN
SUBGOAL_THEN `ball(v0:real^3,r) = {}`
(fun th -> SIMP_TAC[th;
INTER_EMPTY;
MEASURE_EMPTY]) THEN
REWRITE_TAC[
BALL_EQ_EMPTY] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_REWRITE_TAC[GSYM
REAL_NOT_LT;
REAL_ABS_NEG] THEN
ASM_SIMP_TAC[REAL_ARITH `~(&0 <= a) ==> ~(&1 < a) /\ abs a = --a`] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
[ASM_SIMP_TAC[REAL_ARITH `&1 < --a ==> max a (-- &1) = -- &1`] THEN
REAL_ARITH_TAC;
ASM_SIMP_TAC[REAL_ARITH `~(&1 < --a) ==> max a (-- &1) = a`] THEN
REAL_ARITH_TAC]);;
let is_sphere= new_definition
`is_sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;let c_cone = new_definition
`c_cone (v,w:real^3, r:real)=
{x:real^3 | ((x-v) dot w = norm (x-v)* norm w* r)}`;;let primitive = new_definition `primitive (C:real^3->bool) =
((?v0 v1 v2 v3 r. (C = solid_triangle v0 {v1,v2,v3} r)) \/
(?v0 v1 v2 v3. (C = conv0 {v0,v1,v2,v3})) \/
(?v0 v1 v2 v3 h a. &0 < a /\
(C = frustt v0 v1 h a INTER wedge v0 v1 v2 v3)) \/
(?v0 v1 v2 v3 r c. (C = conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3)) \/
(?a b. (C = rect a b)) \/
(?t r. (C = ellipsoid t r)) \/
(?v0 v1 v2 v3 r. (C = normball v0 r INTER wedge v0 v1 v2 v3)))`;;let MEASURABLE_RULES = prove
(`(!C. primitive C ==> measurable C) /\
(!Z. NULLSET Z ==> measurable Z) /\
(!X t. measurable X ==> (measurable (
IMAGE (scale t) X))) /\
(!X v. measurable X ==> (measurable (
IMAGE ((+) v) X))) /\
(!(s:real^3->bool) t. (measurable s /\ measurable t)
==> measurable (s
UNION t)) /\
(!(s:real^3->bool) t. (measurable s /\ measurable t)
==> measurable (s
INTER t)) /\
(!(s:real^3->bool) t. (measurable s /\ measurable t)
==> measurable (s
DIFF t))`,
let vol_solid_triangle = new_definition `vol_solid_triangle v0 v1 v2 v3 r =
let a123 = dihV v0 v1 v2 v3 in
let a231 = dihV v0 v2 v3 v1 in
let a312 = dihV v0 v3 v1 v2 in
(a123 + a231 + a312 - pi)*(r pow 3)/(&3)`;;let vol_conv = new_definition `vol_conv v1 v2 v3 v4 =
let x12 = dist(v1,v2) pow 2 in
let x13 = dist(v1,v3) pow 2 in
let x14 = dist(v1,v4) pow 2 in
let x23 = dist(v2,v3) pow 2 in
let x24 = dist(v2,v4) pow 2 in
let x34 = dist(v3,v4) pow 2 in
sqrt(delta_x x12 x13 x14 x34 x24 x23)/(&12)`;;
let vol_rect = new_definition `vol_rect a b =
if (a$1 < b$1) /\ (a$2 < b$2) /\ (a$3 < b$3) then
(b$3-a$3)*(b$2-a$2)*(b$1-a$1) else &0`;;
let volume_props = prove
(`(!C. measurable C ==> vol C >= &0) /\
(!Z. NULLSET Z ==> (vol Z = &0)) /\
(!X Y. measurable X /\ measurable Y /\ NULLSET (
SDIFF X Y)
==> (vol X = vol Y)) /\
(!X t. (measurable X) /\ (measurable (
IMAGE (scale t) X))
==> (vol (
IMAGE (scale t) X) = abs(t$1 * t$2 * t$3)*vol(X))) /\
(!X v. measurable X ==> (vol (
IMAGE ((+) v) X) = vol X)) /\
(!v0 v1 v2 v3 r. (r > &0) /\ ~coplanar{v0,v1,v2,v3}
==> vol (
solid_triangle v0 {v1,v2,v3} r) =
vol_solid_triangle v0 v1 v2 v3 r) /\
(!v0 v1 v2 v3. vol(conv0 {v0,v1,v2,v3}) =
vol_conv v0 v1 v2 v3) /\
(!v0 v1 v2 v3 h a. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\
(h >= &0) /\ (a > &0) /\ (a <= &1)
==> vol(frustt v0 v1 h a
INTER wedge v0 v1 v2 v3) =
vol_frustt_wedge v0 v1 v2 v3 h a) /\
(!v0 v1 v2 v3 r c. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\
(r >= &0) /\ (c >= -- (&1)) /\ (c <= &1)
==> (vol(
conic_cap v0 v1 r c
INTER wedge v0 v1 v2 v3) =
vol_conic_cap_wedge v0 v1 v2 v3 r c)) /\
(!(a:real^3) (b:real^3). vol(rect a b) =
vol_rect a b) /\
(!v0 v1 v2 v3 r. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\
(r >= &0)
==> (vol(normball v0 r
INTER wedge v0 v1 v2 v3) =
vol_ball_wedge v0 v1 v2 v3 r))`,