module Lemma_fan = struct
open Sphere;;
open Fan_defs;;
open Tactic_fan;;
(* ========================================================================== *)
(* COLLINEAR *)
(* ========================================================================== *)
let th3a12=prove(`!x v u.(~
collinear {x,v,u} ==>
DISJOINT {x,u} {v})`,
(
let th=prove(`{x,v,u}={x,v,u}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC
THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
let th3a=prove(`!x v u.(~
collinear {x,v,u} ==>
DISJOINT {x,v} {u})`,
(
let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC
THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
let th3c= prove(`!x v u. ~
collinear {x,v,u} ==> ~(u
IN aff {x,v})`,
REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_NOT
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM;
COLLINEAR_3;
COLLINEAR_LEMMA; VECTOR_ARITH` a-b=
vec 0 <=> a = b`; DE_MORGAN_THM]
THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ARITH `u'+v'= &1 <=> v'= &1 -u'`]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[VECTOR_ARITH`(u = u' % x + (&1 - u') % v) <=> (u - v = u' % (x-v))`] THEN SET_TAC[]);;
let th3=prove(`!x v u. ~
collinear {x,v,u} ==> ~ (x=v) /\ ~(x=u) /\
DISJOINT {x,v} {u}/\
DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u
IN aff {x,v})`,
MESON_TAC[th3a;th3b;th3b1;th3c;th3d;th3a12]);;
let collinear1_fan=prove(`!x v u. ~
collinear {x,u,v} <=> ~(u
IN aff {x,v})/\ ~ (x=v)`,
(
let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
REPEAT GEN_TAC THEN EQ_TAC
THENL[
MESON_TAC[th3;lem];
REWRITE_TAC[SET_RULE`~(t1) /\ ~ t2<=> ~(t2\/ t1)`;COLLINEAR_3_EXPAND;aff; AFFINE_HULL_2;IN_ELIM_THM]
THEN MATCH_MP_TAC MONO_NOT THEN MATCH_MP_TAC MONO_OR THEN STRIP_TAC
THENL[
REWRITE_TAC[];
STRIP_TAC THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1- (u':real)` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]));;
let properties_inside_collinear0_fan=prove(`!(x:real^3) (u:real^3) (w:real^3) a:real.
&0 <a /\ a< &1
/\ ~collinear{x,w,u}
==> ~collinear{x,(&1 - a) % u + a % w,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
collinear1_fan]
THEN STRIP_TAC THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MATCH_MP_TAC MONO_NOT
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v % u
<=> a % w = u' % x + (v+a- &1) % u`]
THEN MP_TAC(REAL_ARITH`&0< a ==> ~(a= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`a:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
a % w = u' % x + (v+a- &1) % u:real^3
==> (inv ( a))%(a % w) = (inv (a))%(u' % x + (v+a- &1) % u)
`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C= (A*B)%C`;VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN EXISTS_TAC `(inv a * (u':real))`
THEN EXISTS_TAC `(inv a * (v +a - &1 :real))`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv a * (u') + inv a * (v +a - &1)=inv a* (a+ (u'+v) - &1)`;REAL_ARITH`t3'+ &1 - &1=t3'`]);;
let properties_inside_collinear1_fan=prove(`!(x:real^3) (u:real^3) (w:real^3) a:real.
&0 <a /\ a< &1
/\ ~collinear{x,w,u}
==> ~collinear{x,(&1 - a) % u + a % w,w}`,
REPEAT STRIP_TAC THEN
MRESAL_TAC
properties_inside_collinear0_fan[`(x:real^3)`;` (w:real^3)`;`(u:real^3)`;`&1-a:real`][VECTOR_ARITH`(&1 - (&1 - a)) % w + (&1 - a) % u=(&1 - a) % u + a % w`;]
THENL[ ASM_TAC THEN REAL_ARITH_TAC;
STRIP_TAC THENL[ASM_TAC THEN REAL_ARITH_TAC;
ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]]]);;
let properties_inside_collinear_fan=prove(`!(x:real^3) (u:real^3) (w:real^3) a:real.
&0 <a /\ a< &1
/\ ~collinear{x,u,w}
==> ~collinear{x,(&1 - a) % u + a % w,u}
/\ ~collinear{x,(&1 - a) % u + a % w,w}`,
let notcoplanar_imp_notcollinear_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3.
~coplanar {x,v,u,w}==> ~collinear {x,u,w} /\ ~collinear {x,v,u}
/\ ~collinear {x,v,w}`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR [`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN RESA_TAC
THEN MRESAL_TAC
NOT_COPLANAR_NOT_COLLINEAR [`x:real^3`;`v:real^3`;`w:real^3`;`u:real^3`][SET_RULE`{A,B,C,D}={A,B,D,C}`]);;
(* ========================================================================== *)
(* COLLINEAR and CONTINUOUS *)
(* ========================================================================== *)
(* ========================================================================== *)
(* CYCLIC SET *)
(* ========================================================================== *)
let property_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v
==> ~(v=x) /\ ~(u=x)/\ ~collinear {
vec 0, v-x, u-x}`,
(
let th= prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2}`, SET_TAC[]) in
(let th1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN affine hull {x,v}
`,REPEAT GEN_TAC THEN REWRITE_TAC[AFFINE_HULL_2;INTER; IN_ELIM_THM] THEN EXISTS_TAC`&1` THEN EXISTS_TAC `&0` THEN
MESON_TAC[REAL_ARITH`&1+ &0= &1`; VECTOR_ARITH`x= &1 % x + &0 % v`])
in
(let th2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2} INTER affine hull {x,v}
`, REWRITE_TAC[INTER;IN_ELIM_THM] THEN REWRITE_TAC[th;th1]) in
REPEAT GEN_TAC THEN
REWRITE_TAC[COLLINEAR_LEMMA;DE_MORGAN_THM;VECTOR_ARITH`a-b=vec 0 <=> a=b`;cyclic_set;] THEN STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(v:real^3)=(x:real^3) <=> x=v`] THEN STRIP_TAC
THENL[ STRIP_TAC THEN
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];
STRIP_TAC THENL[
STRIP_TAC THEN
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];
STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"a")
THEN DISCH_TAC
THEN REMOVE_THEN "a" MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`(c:real) % ((v:real^3)-(x:real^3))=(u:real^3)-x <=> u = (&1 - c) % x+c % v`]
THEN DISCH_TAC
THEN SUBGOAL_THEN `(u:real^3) IN affine hull {(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[
REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]
THEN EXISTS_TAC `&1 - (c:real)`
THEN EXISTS_TAC`c:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - (c:real) +c= &1`;];
MP_TAC(ISPECL[`u:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`]th)
THEN DISCH_TAC
THEN ASM_TAC
THEN SET_TAC[INTER]
]]]))));;
let property_of_cyclic_set1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v ==> ~collinear {x, v, w1}`,
(
let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in
REPEAT GEN_TAC THEN DISCH_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`;`u:real^3`; `w2:real^3`] property_of_cyclic_set) THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_3]));;
let property_of_cyclic_set2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v
==> ~collinear {x, v, w2}`,
(
let th=prove(`{u,w1,w2}={w2,w1,u}`,SET_TAC[]) in
( let th1=prove(`{u,w1,w2}={w1,w2,u}`,SET_TAC[]) in
REPEAT GEN_TAC THEN DISCH_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w2:real^3`;`w1:real^3`; `u:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[th1;COLLINEAR_3])));;
let property_of_cyclic_set3=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v
==> ~
collinear {x, v, u}`,
(
let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in
REPEAT GEN_TAC THEN DISCH_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_MESON_TAC[COLLINEAR_3;th]));;
let properties_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v
==> ~(v=x) /\ ~(u=x)/\ ~collinear {
vec 0, v-x, u-x}
/\ ~collinear {x, v, u}
/\ ~collinear {x, v, w1}
/\ ~collinear {x, v, w2}`,
(* ========================================================================== *)
(* the properties in normal vector *)
(* ========================================================================== *)
let imp_norm_not_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(
norm ( v - x) = &0)`,
REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(v:real^3)-(x:real^3)=
vec 0` ASSUME_TAC THENL
[POP_ASSUM MP_TAC THEN MESON_TAC[
NORM_EQ_0];
SUBGOAL_THEN `(v:real^3) = (x:real^3)` ASSUME_TAC THENL
[POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;
ASM_TAC THEN SET_TAC[]]]);;
let imp_norm_gl_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(
norm ( v - x)) > &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(
norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
[ASM_MESON_TAC[
imp_norm_not_zero_fan];
MP_TAC (ISPEC `(v:real^3)-(x:real^3)`
NORM_POS_LE) THEN DISCH_TAC THEN
SUBGOAL_THEN `
norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL
[POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
MP_TAC (ISPEC `
norm((v:real^3)-(x:real^3))`
REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]]);;
let imp_norm_ge_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(
norm ( v - x)) >= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(
norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
[ASM_MESON_TAC[
imp_norm_not_zero_fan];
MP_TAC (ISPEC `(v:real^3)-(x:real^3)`
NORM_POS_LE) THEN DISCH_TAC THEN
SUBGOAL_THEN `
norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL
[POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
MP_TAC (ISPEC `
norm((v:real^3)-(x:real^3))`
REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
let norm_of_normal_vector_is_unit_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==>
norm(inv(
norm ( v - x))% (v-x))= &1`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
NORM_MUL] THEN SUBGOAL_THEN ` inv(
norm ( (v:real^3) - (x:real^3))) >= &0` ASSUME_TAC THENL[ ASM_MESON_TAC[
imp_norm_ge_zero_fan];
SUBGOAL_THEN ` ~(
norm ( (v:real^3) - (x:real^3))= &0)` ASSUME_TAC THENL
[ASM_MESON_TAC[
imp_norm_not_zero_fan];
SUBGOAL_THEN ` abs(inv(
norm ( (v:real^3) - (x:real^3))))= inv(
norm ( (v:real^3) - (x:real^3)))` ASSUME_TAC THENL
[ASM_MESON_TAC[
REAL_ABS_REFL;REAL_ARITH `(a:real)>= &0 <=> &0 <= a`; ];
MP_TAC(ISPEC `
norm ( (v:real^3) - (x:real^3))` REAL_MUL_LINV)THEN ASM_REWRITE_TAC[]]]]);;
let IMP_NORM_FAN=prove(`!va:real^3 vb:real^3. ~(va = vb)
==> ~(
norm (va-vb) = &0) /\ &0 <=
norm (va-vb) /\ &0 <
norm (va-vb) /\ &0 <= inv (
norm (va-vb))
/\ &0 < inv (
norm (va-vb)) /\ inv (
norm (va-vb)) *
norm (va-vb) = &1`,
REPEAT GEN_TAC
THEN DISCH_TAC
THEN MRESA_TAC
imp_norm_not_zero_fan[`va:real^3`;`vb:real^3`]
THEN ASSUME_TAC(ISPEC`va-vb:real^3`
NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(
norm(va-vb:real^3)= &0) /\ &0 <=
norm(va-vb:real^3)==> &0 <
norm(va-vb:real^3)`)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LE_INV `
norm(va-vb:real^3)`
THEN MRESA1_TAC
REAL_LT_INV `
norm(va-vb:real^3)`
THEN MRESA1_TAC REAL_MUL_LINV `
norm(va-vb:real^3)`
THEN ASM_REWRITE_TAC[]);;
(* ========================================================================== *)
(* the normal coordinate is the definiton of frame in flyspeck *)
(* ========================================================================== *)
let e3_fan=new_definition`e3_fan (x:real^3) (v:real^3) (u:real^3) = inv(norm((v:real^3)-(x:real^3))) % ((v:real^3)-(x:real^3))`;;
let e2_fan=new_definition`e2_fan (x:real^3) (v:real^3) (u:real^3) = inv(norm((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3)))) % ((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))) `;;
let e1_is_normal_fan=prove(`!x:real^3 v:real^3 u:real^3.
~(v=x) /\ ~(u=x) /\ ~(
collinear {
vec 0, v-x, u-x}) ==>
e1_fan x v u
dot e1_fan x v u = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
REWRITE_TAC[
e1_fan;
DOT_CROSS] THEN
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]
e2_orthogonal_e3_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]
e2_is_normal_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]
e3_is_normal_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let udot_e1_fan1=prove(`!x:real^3 v:real^3 u:real^3.
~(v=x) /\ ~(u=x) /\ ~(
collinear {
vec 0, v-x, u-x})
==> &0 <= (u - x)
dot e1_fan x v u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3` ;`v:real^3` ;`u:real^3`]
udot_e1_fan) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let module_of_vector =prove(`!x:real^3 v:real^3 u:real^3 w:real^3 r:real psi:real h:real.
~(v=x) /\ ~(u=x) /\ ~(
collinear {
vec 0, v-x, u-x})
/\ (&0 < r) /\ (w=(r *
cos psi) %
e1_fan x v u + (r *
sin psi) %
e2_fan x v u + h % (v-x))
==>
sqrt(((w
cross (
e3_fan x v u))
dot e1_fan x v u) pow 2 + ((w
cross (
e3_fan x v u))
dot e2_fan x v u) pow 2) = r`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[
CROSS_LADD;
CROSS_LMUL;] THEN
MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]
orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[]
THEN DISCH_THEN (LABEL_TAC "a") THEN
MP_TAC (ISPECL [`
e1_fan (x:real^3) (v:real^3) (u:real^3)`;`
e2_fan (x:real^3) (v:real^3) (u:real^3)`;
`
e3_fan (x:real^3) (v:real^3) (u:real^3)`]
ORTHONORMAL_CROSS) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]
vcross_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL[`
e1_fan (x:real^3) (v:real^3) (u:real^3)`;`
e3_fan (x:real^3) (v:real^3) (u:real^3)`]
CROSS_SKEW)
THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[
DOT_LADD;
DOT_LMUL;
DOT_LZERO;
DOT_LNEG]
THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[
orthonormal] THEN DISCH_TAC THEN ASM_REWRITE_TAC[
DOT_SYM]
THEN REWRITE_TAC[REAL_ARITH `-- &0 = &0`; REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH `(a:real) * &1 = a`;
REAL_ARITH `(a:real) + &0 = a`;REAL_ARITH `&0 + (a:real) = a`;
REAL_POW_MUL; REAL_ARITH `-- &1 pow 2 = &1`;
REAL_ARITH `(d:real) * (b:real) + d * (c:real) = d * ( b + c)`;
SIN_CIRCLE;
sqrt] THEN MATCH_MP_TAC
SELECT_UNIQUE
THEN REWRITE_TAC[
BETA_THM] THEN GEN_TAC THEN EQ_TAC
THENL[
STRIP_TAC THEN SUBGOAL_THEN `((y:real) - (r:real))* (y + r) = &0` ASSUME_TAC
THENL[
REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ARITH `((a:real)- (b:real)) * (c:real)= a *c - b * c`;
REAL_ARITH`(y:real) * (r:real)= r * y`; REAL_ARITH `((a:real) +(b:real)) - ((b:real) + (c:real))= a - c`;
REAL_ARITH `(a:real)- (c:real)= &0 <=> a = c`]
THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
MP_TAC (ISPECL [`(y:real)- (r:real)`; `(y:real)+(r:real)` ]
REAL_ENTIRE) THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL
[POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]];
DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
(* ========================================================================== *)
(* COPLANAR (^_^) *)
(* ========================================================================== *)
let continuous_coplanar_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3.
~(
coplanar{x,v,u,w})
==>(!t:real. ~(t= &0) ==> ~coplanar {x,v,u,(&1-t)%u+t%w} )`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC`~(
coplanar{x,v,u,w:real^3})`
THEN MATCH_MP_TAC MONO_NOT
THEN REWRITE_TAC[
COPLANAR_DET_EQ_0;VECTOR_ARITH`((&1 - t) % u + t % w) - x=(&1 - t) % (u-x) + t % (w - x):real^3`;
DET_3;
VECTOR_3;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT
;REAL_ARITH`(v - x)$1 * (u - x)$2 * ((&1 - t) * (u - x)$3 + t * (w - x)$3) +
(v - x)$2 * (u - x)$3 * ((&1 - t) * (u - x)$1 + t * (w - x)$1) +
(v - x)$3 * (u - x)$1 * ((&1 - t) * (u - x)$2 + t * (w - x)$2) -
(v - x)$1 * (u - x)$3 * ((&1 - t) * (u - x)$2 + t * (w - x)$2) -
(v - x)$2 * (u - x)$1 * ((&1 - t) * (u - x)$3 + t * (w - x)$3) -
(v - x)$3 * (u - x)$2 * ((&1 - t) * (u - x)$1 + t * (w - x)$1)=
t*((v - x)$1 * (u - x)$2 * ((w - x)$3) +
(v - x)$2 * (u - x)$3 * ( (w - x)$1) +
(v - x)$3 * (u - x)$1 * ((w - x)$2) -
(v - x)$1 * (u - x)$3 * ((w - x)$2) -
(v - x)$2 * (u - x)$1 * ( (w - x)$3) -
(v - x)$3 * (u - x)$2 * ( (w - x)$1)):real`;
REAL_ENTIRE]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let injective_azim_coplanar=prove(`!x:real^3 v:real^3 u:real^3 w:real^3.
~coplanar {x,v,u,w}
==>
!a:real b:real. ~(a= &0) /\ ~(b= &0)/\ (\(t:real).
azim x v u ((&1 - t) % u + t % w))a=(\(t:real).
azim x v u ((&1 - t) % u + t % w))b==>a=b`,
REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
continuous_coplanar_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM(fun
th -> MP_TAC(ISPEC`a:real`
th)THEN ASSUME_TAC(
th))
THEN POP_ASSUM(fun
th -> MP_TAC(ISPEC`b:real`
th))
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,B,D,C}`]
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`(&1 - a) % u + a % w:real^3`;`u:real^3`]
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`(&1 - b) % u + b % w:real^3`;`u:real^3`]
THEN MRESA_TAC
AZIM_EQ [`x:real^3`;`v:real^3`;`u:real^3`;`(&1 - b) % u + b % w:real^3`;`(&1 - a) % u + a % w:real^3`;]
THEN MRESA_TAC
AZIM_EQ_0 [`x:real^3`;`v:real^3`;`(&1 - a) % u + a % w:real^3`;`(&1 - b) % u + b % w:real^3`;]
THEN MRESA_TAC
AZIM_EQ_0_PI_IMP_COPLANAR [`x:real^3`;`v:real^3`;`(&1 - a) % u + a % w:real^3`;`(&1 - b) % u + b % w:real^3`;]
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC`~coplanar {x,v,u,w:real^3}`
THEN REWRITE_TAC[
COPLANAR_DET_EQ_0;VECTOR_ARITH`((&1 - t) % u + t % w) - x=(&1 - t) % (u-x) + t % (w - x):real^3`;
DET_3;
VECTOR_3;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT]
THEN STRIP_TAC
THEN REWRITE_TAC[REAL_ARITH`(v - x)$1 *
((&1 - a) * (u - x)$2 + a * (w - x)$2) *
((&1 - b) * (u - x)$3 + b * (w - x)$3) +
(v - x)$2 *
((&1 - a) * (u - x)$3 + a * (w - x)$3) *
((&1 - b) * (u - x)$1 + b * (w - x)$1) +
(v - x)$3 *
((&1 - a) * (u - x)$1 + a * (w - x)$1) *
((&1 - b) * (u - x)$2 + b * (w - x)$2) -
(v - x)$1 *
((&1 - a) * (u - x)$3 + a * (w - x)$3) *
((&1 - b) * (u - x)$2 + b * (w - x)$2) -
(v - x)$2 *
((&1 - a) * (u - x)$1 + a * (w - x)$1) *
((&1 - b) * (u - x)$3 + b * (w - x)$3) -
(v - x)$3 *
((&1 - a) * (u - x)$2 + a * (w - x)$2) *
((&1 - b) * (u - x)$1 + b * (w - x)$1)=
(b-a)*((v - x)$1 * (u - x)$2 * (w - x)$3 +
(v - x)$2 * (u - x)$3 * (w - x)$1 +
(v - x)$3 * (u - x)$1 * (w - x)$2 -
(v - x)$1 * (u - x)$3 * (w - x)$2 -
(v - x)$2 * (u - x)$1 * (w - x)$3 -
(v - x)$3 * (u - x)$2 * (w - x)$1)`;
REAL_ENTIRE]
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC);;
(* ========================================================================== *)
(* the sphere coordinate is the definiton of frame in flyspeck *)
(* ========================================================================== *)
let SINCOS_PRINCIPAL_VALUE_FAN = prove(
`!x:real. ?y:real. (&0<= y /\ y < &2*
pi) /\ (
sin(y) =
sin(x) /\
cos(y) =
cos(x))`,
GEN_TAC THEN MP_TAC(SPECL [`x:real`]
SINCOS_PRINCIPAL_VALUE) THEN STRIP_TAC THEN
DISJ_CASES_TAC(REAL_ARITH`((y:real) < &0)\/ (&0 <= y)`) THENL
[ EXISTS_TAC `(y:real)+ &2 *
pi` THEN ASSUME_TAC(
PI_POS)
THEN ASM_REWRITE_TAC[
SIN_PERIODIC;
COS_PERIODIC] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
EXISTS_TAC `(y:real)` THEN ASSUME_TAC(
PI_POS)
THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let sin_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {
vec 0, v-x, u-x} /\ &0 < r1
/\ u - x = (r1 *
cos psi) % (
e1_fan x v u) + (r1 *
sin psi) % (
e2_fan x v u) + h1 % (v-x)
==>
sin psi = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
dot_e2_fan)
THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[
DOT_LADD;
DOT_LMUL]
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
e1_orthogonal_e2_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`;
REAL_ARITH`(a:real) * &1= a`]
THEN DISCH_TAC
THEN MATCH_MP_TAC(ISPECL [`
sin (psi:real)`;`&0`; `r1:real`]
REAL_EQ_LCANCEL_IMP) THEN ASM_REWRITE_TAC[]
THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
let cos_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {
vec 0, v-x, u-x} /\ &0 < r1
/\ u - x = (r1 *
cos psi) % (
e1_fan x v u) + (r1 *
sin psi) % (
e2_fan x v u) + h1 % (v-x)
==>
cos psi = &1`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)-(x:real^3)`; `r1:real`; `psi:real`; `h1:real`]
module_of_vector) THEN ASM_REWRITE_TAC[] THEN
POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)] THEN ASSUME_TAC(
th))
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `
e3_fan (x:real^3) (v:real^3)(u:real^3)`;`
e1_fan (x:real^3) (v:real^3)(u:real^3)`]
CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[
th])
THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `
e3_fan (x:real^3) (v:real^3)(u:real^3)`;`
e2_fan (x:real^3) (v:real^3)(u:real^3)`]
CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[
th])
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC(ISPECL[`
e1_fan (x:real^3) (v:real^3)(u:real^3)`; `
e2_fan (x:real^3) (v:real^3)(u:real^3)`;`
e3_fan (x:real^3) (v:real^3)(u:real^3)`]
ORTHONORMAL_CROSS )THEN POP_ASSUM (fun th-> REWRITE_TAC[
th]) THEN STRIP_TAC THEN
POP_ASSUM (fun th-> REWRITE_TAC[
th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[
th]) THEN
POP_ASSUM (fun th-> REWRITE_TAC[
CROSS_SKEW;
th])
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`]
dot_e2_fan)THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC THEN MP_TAC(ISPECL[ `
e2_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]
DOT_SYM) THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2 +(a:real)=a`] THEN
MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`]
udot_e1_fan1) THEN ASM_REWRITE_TAC[
DOT_LNEG;] THEN DISCH_TAC
THEN MP_TAC(ISPECL[ `
e1_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]
DOT_SYM) THEN DISCH_TAC THEN
POP_ASSUM (fun th-> REWRITE_TAC[
th]) THEN REWRITE_TAC[
POW_2_SQRT_ABS;
REAL_ABS_NEG] THEN
MP_TAC(ISPECL[ `((u:real^3)-(x:real^3))
dot e1_fan (x:real^3) (v:real^3)(u:real^3)`]
REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_TAC
THEN
MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `r1:real`; `psi:real`; `h1:real`]
sin_of_u_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`
(r1 *
cos psi) %
e1_fan x v u + (r1 * &0) %
e2_fan x v u + h1 % (v - x)=
(r1 *
cos psi) %
e1_fan x v u + h1 % (v - x)`] THEN DISCH_TAC THEN
SUBGOAL_THEN`((u:real^3) - (x:real^3))
dot e1_fan x (v:real^3) u = (((r1:real) *
cos (psi:real)) %
e1_fan x v u + (h1:real) % (v - x))
dot e1_fan x v u` ASSUME_TAC
THENL[ASM_MESON_TAC[];
POP_ASSUM MP_TAC THEN REWRITE_TAC[
DOT_LADD;
DOT_LMUL] THEN POP_ASSUM MP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
e3_mul_dist_fan) THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
e1_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[
DOT_LMUL;
DOT_SYM]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
e1_is_normal_fan) THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)* &1+ (b:real)*(c:real)* &0= a`] THEN REPEAT DISCH_TAC
THEN MP_TAC(ISPECL[`&1`;`
cos (psi:real)`; `r1:real`]
REAL_EQ_LCANCEL_IMP) THEN REWRITE_TAC[REAL_ARITH`(a:real)* &1=a`; REAL_ARITH`&1 = (a:real) <=> a= &1`] THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let sincos1_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
~collinear {x,v,u} /\ &0 < r1
/\ u - x = (r1 *
cos psi) % (
e1_fan x v u) + (r1 *
sin psi) % (
e2_fan x v u) + h1 % (v-x)
==>
sin psi = &0 /\
cos psi = &1`,
REPEAT STRIP_TAC
THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={U,X,V}`]
THEN DISCH_TAC
THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={V,X,U}`]
THEN ONCE_REWRITE_TAC[
COLLINEAR_3]
THEN DISCH_TAC
THEN MRESA_TAC
th3[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC
sincos_of_u_fan[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`;`r1:real`; `psi:real`; `h1:real`])
;;
(*------------------------------------------------------------*)
(* change spherical coordinate in fan *)
(*------------------------------------------------------------*)
(*---------------------------------------------------------------------------------------*)
(* the function of change coordinate is(spherecial) continuous *)
(*---------------------------------------------------------------------------------------*)
(* ========================================================================== *)
(* AFFINE *)
(* ========================================================================== *)
(* local definitions *)
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_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_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_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_2=prove(`!x u v w.
DISJOINT {x, u} {v, w}
==> aff_gt {x, u} {v, w} =
{y | ?t1 t2 t3 t4.
&0 < t3 /\
&0 < t4 /\
t1 + t2 + t3 +t4= &1 /\
y =
t1 % x + t2 %u + t3 % v + t4 % w}`,
AFF_TAC);;
let AFF_GE_1_1=prove(`!x:real^3 v:real^3.
~(x=v)
==> aff_ge {x} {v} = {y:real^3 | ?t1:real t2:real. (&0 <= t2 ) /\ (
t1 + t2 = &1) /\ (y =
t1 % x + t2 % v )}`,
let aff_subset_aff_ge=prove(`!x:real^3 v:real^3 w:real^3.
DISJOINT {x,v} {w}
==> aff {x,v}
SUBSET aff_ge {x,v} {w}`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MP_TAC(ISPECL[`(x:real^3) `;` (v:real^3)`;` (w:real^3)`]
AFF_GE_2_1) THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC
THEN ASM_REWRITE_TAC[aff;
AFFINE_HULL_2;
SUBSET;
AFF_GE_2_1;
IN_ELIM_THM]
THEN GEN_TAC THEN STRIP_TAC
THEN EXISTS_TAC`u:real` THEN EXISTS_TAC`v':real` THEN EXISTS_TAC`&0`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`a=b +c + &0 % d<=>a=b+c`]
THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
let COMPLEMENT_SET_FAN=prove(`!x:real^3 v:real^3 u:real^3 y:real^3 w:real^3 t1:real t2:real t3:real.
~( w
IN aff {x, v}) /\ ~(t3 = &0) /\ (
t1 + t2 + t3 = &1)
==>
t1 % x + t2 % v + t3 % w
IN
complement_set {x, v}`,
REPEAT GEN_TAC THEN ASSUME_TAC(
affine_hull_2_fan) THEN STRIP_TAC THEN
REWRITE_TAC[
complement_set;
IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
IN_ELIM_THM] THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[
IN_ELIM_THM] THEN REPEAT DISCH_TAC THEN
SUBGOAL_THEN ` (t3:real) % w =((t1':real)- (t1:real)) % (x:real^3) + ((t2':real)- (t2:real)) % (v:real^3) ` ASSUME_TAC
THENL
[POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;
REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "b") THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN(LABEL_TAC "d")
THEN REPEAT STRIP_TAC THEN USE_THEN "c" MP_TAC THEN REWRITE_TAC[CONTRAPOS_THM] THEN
EXISTS_TAC `((t1':real) - (t1:real))/(t3:real)` THEN EXISTS_TAC `((t2':real) - (t2:real))/(t3:real)`
THEN SUBGOAL_THEN `((t1':real) - (t1:real))/(t3:real)+ ((t2':real) - (t2:real))/(t3:real) = &1` ASSUME_TAC THENL
[REWRITE_TAC[
real_div] THEN REWRITE_TAC[REAL_ARITH `a*b+c*b=(a+c)*b`] THEN
SUBGOAL_THEN `(t1':real) - (t1:real) + (t2':real) - (t2:real) - (t3:real) = &0` ASSUME_TAC THENL
[REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
SUBGOAL_THEN `(t1':real) - (t1:real) + (t2':real) - (t2:real) = (t3:real)` ASSUME_TAC THENL
[POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
ASM_MESON_TAC[
REAL_MUL_RINV]]];
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
real_div] THEN
REWRITE_TAC[VECTOR_ARITH ` (((t1':real) - (t1:real)) * inv (t3:real)) % (x:real^3) + (((t2':real) - (t2:real)) * inv t3) % (v:real^3) = inv t3 % ((t1' -
t1) % x + (t2' - t2) % v)`] THEN
SUBGOAL_THEN `(t3:real) % (w:real^3) = t3 %( inv t3 % (((t1':real) - (t1:real)) % (x:real^3) + ((t2':real) - (t2:real)) % (v:real^3)))` ASSUME_TAC THENL
[REWRITE_TAC[VECTOR_ARITH ` (t3:real) % (inv t3 % (((t1':real) - (t1:real)) % (x:real^3) + ((t2':real) - (t2:real)) % (v:real^3)))= (t3 * inv t3) % ((t1' -
t1) % x + (t2' - t2) % v) `] THEN
SUBGOAL_THEN `((t3:real) * inv (t3:real) = &1) ` ASSUME_TAC THENL
[ASM_MESON_TAC[
REAL_MUL_RINV];
ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC];
ASM_MESON_TAC[
VECTOR_MUL_LCANCEL_IMP]]]]);;
let aff_ge_inter_aff_ge=prove(`!(x:real^3) (v:real^3) (w:real^3).
~collinear {x,v,w}
==>
aff_ge {x} {v , w} = aff_ge {x , v} {w}
INTER aff_ge {x , w} {v}`,
REPEAT STRIP_TAC THEN MRESA_TAC
th3 [`x:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GE_1_2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GE_2_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`w:real^3`;`v:real^3`]
AFF_GE_2_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[
INTER;
IN_ELIM_THM;
EXTENSION]THEN GEN_TAC THEN EQ_TAC
THENL(*1*)[
STRIP_TAC THEN STRIP_TAC
THENL(*2*)[
EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_MESON_TAC[];
EXISTS_TAC `(t1:real)` THEN
EXISTS_TAC `(t3:real)` THEN EXISTS_TAC `(t2:real)`
THEN
ASM_MESON_TAC[REAL_ARITH `(t1:real)+ (t3:real) +(t2:real)=
t1 + t2 + t3`;VECTOR_ARITH `
t1 % x + t2 % v + t3 % w = (t1:real) % (x:real^3) + (t3:real) % (w:real^3) + (t2:real) % (v:real^3)`]](*2*);
STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(PATH_CONV "rrlr" o ONCE_DEPTH_CONV )[
th] THEN ASSUME_TAC(
th)) THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(PATH_CONV "rrlr" o ONCE_DEPTH_CONV )[SYM(
th)] THEN ASSUME_TAC(
th))
THEN DISJ_CASES_TAC(SET_RULE`t3 - t2' = &0 \/ ~((t3:real) - (t2':real) = &0) `)
THENL[POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`A-B= &0 <=> A=B`]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`t1':real`
THEN EXISTS_TAC`t3':real`
THEN EXISTS_TAC`t2':real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % w + t3' % v = t1' % x + t3' % v + t2' % w`;
REAL_ARITH`t1' + t3' + t2'=t1' + t2' + t3'`]
THEN ASM_TAC THEN REAL_ARITH_TAC;
REWRITE_TAC[VECTOR_ARITH
`a % x + b % y + c % z= a1 % x + b1 % z +
c1 % y <=> (c-b1) % z = (a1-a) % x + (c1-b)% y`]
THEN REWRITE_TAC[REAL_ARITH`a+b+c=a1+b1+c1<=> c1-b=(a-a1)+(c-b1)`]
THEN MRESA1_TAC REAL_MUL_LINV`t3 - t2'`
THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
THEN MP_TAC(SET_RULE`
(t3 - t2') % w = (t1' -
t1) % x + (t3' - t2) % v:real^3
==> (inv (t3 - t2'))%((t3 - t2') % w ) = (inv (t3 - t2'))%((t1' -
t1) % x + (t3' - t2) % v:real^3)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C= (A*B)%C`;VECTOR_ARITH`&1 %A=A`;VECTOR_ARITH`A%(B+C)=A%B+A%C`] THEN ASSUME_TAC(SYM(
th)))
THEN STRIP_TAC
THEN SUBGOAL_THEN`w
IN aff{(x:real^3),v}` ASSUME_TAC
THENL[REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM;] THEN EXISTS_TAC`inv(t3-t2') *(t1'-t1)`
THEN EXISTS_TAC`inv(t3-t2') *(t3'-t2)` THEN ASM_REWRITE_TAC[REAL_ARITH`A*B+A*C=A*(B+C)`];
ASM_SET_TAC[]]]]);;
let SCALE_AFF_TAC th=REPEAT GEN_TAC
THEN DISCH_TAC
THEN REPEAT GEN_TAC
THEN MRESAL_TAC th[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`&1 - a* t2- a* t3:real`
THEN EXISTS_TAC`a* t2:real`
THEN EXISTS_TAC`a* t3:real`
THEN ONCE_REWRITE_TAC[TAUT`A/\B/\C/\D<=>D/\ A/\B/\C`]
THEN STRIP_TAC
THENL[
ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC `t1+t2+t3= &1:real`
THEN REWRITE_TAC[REAL_ARITH`A+B+C= &1<=>A= &1- B -C:real`]
THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN VECTOR_ARITH_TAC;
MP_TAC(ISPECL[`a:real`;`(t2:real)`]REAL_LT_MUL)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`a:real`;`(t3:real)`]
THEN MRESA_TAC REAL_LE_MUL[`a:real`;`(t2:real)`]
THEN MRESA_TAC REAL_LE_MUL[`a:real`;`(t3:real)`]
THEN ASM_TAC
THEN REAL_ARITH_TAC];;
let origin_is_not_aff_gt_fan=prove(`!x:real^3 v:real^3 u:real^3.
~(u
IN aff {x,v}) /\
DISJOINT {x} {v,u}==> ~(x
IN aff_gt {x} {v,u})`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN REWRITE_TAC[GSYM
FORALL_NOT_THM;DE_MORGAN_THM]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`~( &0< (t2:real))\/ ( &0< (t2:real))`)
THENL[ASM_MESON_TAC[];
DISJ_CASES_TAC(REAL_ARITH`~( &0< (t3:real))\/ ( &0< (t3:real))`)
THENL[ASM_MESON_TAC[];
DISJ_CASES_TAC(REAL_ARITH`~( t1+t2+(t3:real)= &1)\/ ( t1+t2+(t3:real)= &1)`)
THENL[ASM_MESON_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`A+B+C= &1<=>A= &1- B -C:real`]
THEN DISCH_TAC
THEN MP_TAC(REAL_ARITH`&0<t3:real==> ~(t3= &0)`)
THEN RESA_TAC
THEN MP_TAC(ISPEC`(t3:real)`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[VECTOR_ARITH`A=( &1-B-C) %A+B%E+C%D <=> C%(D-A)= (--B)%(E-A)`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`t3 % (u - x) = (--t2) % (v - x):real^3 ==> (inv (t3))%(t3 % (u - x)) = (inv (t3))%((--t2) % (v - x))`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[VECTOR_ARITH`A-B=C%(V-B)<=>A=( &1-C)%B+C%V`]
THEN FIND_ASSUM MP_TAC `~(u
IN aff {x,v}:real^3->bool)`
THEN MATCH_MP_TAC MONO_NOT
THEN STRIP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`&1 - inv t3 * --t2:real`
THEN EXISTS_TAC`inv t3 * --t2:real`
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC]]]);;
let properties_of_collinear4_points_fan=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
~collinear{x,v,u}
/\ v1
IN aff_gt {x} {v,u}
==> ~collinear{x,v1,v}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN MRESA_TAC
AFF_GT_1_2[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th;
IN_ELIM_THM])
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[
collinear1_fan;]
THEN FIND_ASSUM MP_TAC`~(u
IN aff {x, v:real^3})`
THEN MATCH_MP_TAC MONO_NOT
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`
t1 % x + t2 % v + t3 % u = u' % x + v' % v <=> t3 % u = (u'-t1) % x + (v'-t2) % v`;]
THEN MP_TAC (REAL_ARITH`&0< t3==> ~(t3= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV `(t3:real)`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`t3 % u = (u'-t1) % x + (v'-t2) % v ==> (inv (t3)) % (t3) % ( u) = (inv (t3)) % ( (u'-t1) % x + (v'-t2) % v:real^3)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(A%B%C=(A*B)%C:real^3)`;VECTOR_ARITH`A%(B+C)=A%B+A%C`])
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`inv t3 * ((u' -
t1):real)`
THEN EXISTS_TAC`inv t3 * ((v' - t2):real)`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv t3 * (u' -
t1) + inv t3 * (v' - t2)=inv t3 *(t3+ (u'+v') -( t1+ t2+t3))`;REAL_ARITH`A+ &1- &1=A`]);;
let properties_of_coplanar=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
~collinear{x,v,u}
/\ v1
IN aff_gt {x} {v,u}
==>
coplanar{x,v1,v,u}`,
REPEAT STRIP_TAC
THEN REWRITE_TAC[
coplanar]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN MRESA_TAC
AFF_GT_1_2[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th;
IN_ELIM_THM])
THEN STRIP_TAC
THEN EXISTS_TAC`x:real^3`
THEN EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`u:real^3`
THEN SUBGOAL_THEN`(x:real^3)
IN affine hull {x,v,u:real^3}` ASSUME_TAC
THENL[REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM]
THEN EXISTS_TAC`&1`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN REDUCE_ARITH_TAC
THEN VECTOR_ARITH_TAC;
SUBGOAL_THEN`(v:real^3)
IN affine hull {x,v,u:real^3}` ASSUME_TAC
THENL[ REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1`
THEN EXISTS_TAC`&0`
THEN REDUCE_ARITH_TAC
THEN VECTOR_ARITH_TAC;
SUBGOAL_THEN`(u:real^3)
IN affine hull {x,v,u:real^3}` ASSUME_TAC
THENL[
REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1`
THEN REDUCE_ARITH_TAC
THEN VECTOR_ARITH_TAC;
SUBGOAL_THEN`(v1:real^3)
IN affine hull {x,v,u:real^3}` ASSUME_TAC
THENL[
REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM]
THEN EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN ASM_REWRITE_TAC[];
ASM_TAC
THEN SET_TAC[]]]]]);;
let aff_gt_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3.
DISJOINT {x} {v,u}
==>
aff_gt {x} {v,u}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_gt1_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear {x,v1,u}
/\ v1
IN aff_ge {x} {v,u}
==>
aff_gt {x} {v1,u}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v1:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v1:real^3`;`u:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u) + t3' % u
=(t1'+ t2'*t1) % x + (t2'* t2) % v + (t2' * t3 + t3') % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2:real`
THEN EXISTS_TAC`t2' * t3 +t3':real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + t2' * t2 + t2' * t3 + t3'=
t1'+t2'*(t1+t2+t3)+t3'`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_gt12_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear {x,v1,v}
/\ v1
IN aff_ge {x} {v,u}
==>
aff_gt {x} {v1,v}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v1:real^3`;`v:real^3`]
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v1:real^3`;`v:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u) + t3' % v
=(t1'+ t2'*t1) % x + (t2'* t2+t3') % v + (t2' * t3 ) % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2 +t3':real`
THEN EXISTS_TAC`t2' * t3 :real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + (t2' * t2 +t3')+ t2' * t3 =
t1'+t2'*(t1+t2+t3)+t3'`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_gt2_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear {x,v1,u} /\ ~collinear {x,v1,v}
/\ v1
IN aff_gt {x} {v,u}
==>
azim x v1 v u=
pi`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v1:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESA_TAC
AZIM_EQ_PI[`x:real^3`;`v1:real^3`;`v:real^3`;`u:real^3`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`v1 =
t1 % x + t2 % v + t3 % u
<=> t2 % v = (--t1) % x + v1 + (--t3) % u`]
THEN MP_TAC(REAL_ARITH`&0<t2==> ~( t2= &0)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0<t3==> -- t3< &0`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
THEN MRESA1_TAC
REAL_LT_INV`t2:real`
THEN MRESAL_TAC
REAL_LT_LMUL[`inv t2:real`;`-- t3:real`;`&0`][REAL_ARITH`A * &0= &0`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`t2 % v = --t1 % x + v1 + --t3 % u:real^3 ==> (inv (t2))%(t2 % v ) = (inv (t2))%( --t1 % x + v1 + --t3 % u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C+D)=A%B+A%C+A%D`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_LT_2_1[`x:real^3`;`v1:real^3`;`u:real^3`][
IN_ELIM_THM;
SUBSET]
THEN EXISTS_TAC`(inv t2 * --t1):real`
THEN EXISTS_TAC`inv t2:real`
THEN EXISTS_TAC`(inv t2 * --t3):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv t2 * (--t1) + inv t2 + inv t2 * (--t3)=
inv t2 * (t2+ &1 -(
t1 +t2 +t3))`; REAL_ARITH`A+ &1- &1=A`]);;
let remove_variable_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 t1:real t2:real t3:real.
&0 < t3
/\ w =
t1 % x + t2 % v + t3 % u
==> u= inv(t3) % w - (inv(t3)*t1) % x- (inv(t3) * t2) % v`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`w = t1'' % x + t2'' % v + t3'' % u <=> t3'' % u = w-t1'' % x - t2'' % (v:real^3)`]
THEN MP_TAC(REAL_ARITH `&0 < (t3:real) ==> ~(t3 = &0)`)
THEN MP_TAC(ISPEC`(t3:real)`
REAL_LT_INV)
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th] THEN ASSUME_TAC(
th))
THEN STRIP_TAC THEN STRIP_TAC
THEN MP_TAC(ISPEC`(t3:real)`REAL_MUL_LINV)
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th] THEN ASSUME_TAC(
th))
THEN STRIP_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
t3 % u = w-t1 % x - t2 % v:real^3
==> (inv (t3))%(t3 % u) = (inv (t3))%( w-t1 % x - t2 % v:real^3)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th;VECTOR_ARITH`A%B%C= (A*B)%C`;VECTOR_ARITH`&1 %A=A`;VECTOR_ARITH`A%(B-C-D)=A%B-A%C-A%D`] THEN ASSUME_TAC(
th)));;
let aff_gt_inter_aff_gt=prove(`!(x:real^3) (v:real^3) (w:real^3).
~collinear {x,v,w}
==>
aff_gt {x} {v , w} = aff_gt {x , v} {w}
INTER aff_gt {x , w} {v}`,
REPEAT STRIP_TAC THEN MRESA_TAC
th3 [`x:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GT_1_2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GT_2_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`w:real^3`;`v:real^3`]
AFF_GT_2_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[
INTER;
IN_ELIM_THM;
EXTENSION]THEN GEN_TAC THEN EQ_TAC
THENL(*1*)[
STRIP_TAC THEN STRIP_TAC
THENL(*2*)[
EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_MESON_TAC[];
EXISTS_TAC `(t1:real)` THEN
EXISTS_TAC `(t3:real)` THEN EXISTS_TAC `(t2:real)`
THEN
ASM_MESON_TAC[REAL_ARITH `(t1:real)+ (t3:real) +(t2:real)=
t1 + t2 + t3`;VECTOR_ARITH `
t1 % x + t2 % v + t3 % w = (t1:real) % (x:real^3) + (t3:real) % (w:real^3) + (t2:real) % (v:real^3)`]](*2*);
STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(PATH_CONV "rrlr" o ONCE_DEPTH_CONV )[
th] THEN ASSUME_TAC(
th)) THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(PATH_CONV "rrlr" o ONCE_DEPTH_CONV )[SYM(
th)] THEN ASSUME_TAC(
th))
THEN DISJ_CASES_TAC(SET_RULE`t3 - t2' = &0 \/ ~((t3:real) - (t2':real) = &0) `)
THENL[POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`A-B= &0 <=> A=B`]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`t1':real`
THEN EXISTS_TAC`t3':real`
THEN EXISTS_TAC`t2':real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % w + t3' % v = t1' % x + t3' % v + t2' % w`;
REAL_ARITH`t1' + t3' + t2'=t1' + t2' + t3'`]
THEN ASM_TAC THEN REAL_ARITH_TAC;
REWRITE_TAC[VECTOR_ARITH
`a % x + b % y + c % z= a1 % x + b1 % z +
c1 % y <=> (c-b1) % z = (a1-a) % x + (c1-b)% y`]
THEN REWRITE_TAC[REAL_ARITH`a+b+c=a1+b1+c1<=> c1-b=(a-a1)+(c-b1)`]
THEN MRESA1_TAC REAL_MUL_LINV`t3 - t2'`
THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
THEN MP_TAC(SET_RULE`
(t3 - t2') % w = (t1' -
t1) % x + (t3' - t2) % v:real^3
==> (inv (t3 - t2'))%((t3 - t2') % w ) = (inv (t3 - t2'))%((t1' -
t1) % x + (t3' - t2) % v:real^3)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C= (A*B)%C`;VECTOR_ARITH`&1 %A=A`;VECTOR_ARITH`A%(B+C)=A%B+A%C`] THEN ASSUME_TAC(SYM(
th)))
THEN STRIP_TAC
THEN SUBGOAL_THEN`w
IN aff{(x:real^3),v}` ASSUME_TAC
THENL[REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM;] THEN EXISTS_TAC`inv(t3-t2') *(t1'-t1)`
THEN EXISTS_TAC`inv(t3-t2') *(t3'-t2)` THEN ASM_REWRITE_TAC[REAL_ARITH`A*B+A*C=A*(B+C)`];
ASM_SET_TAC[]]]]);;
let aff_gt3_subset_aff_gt=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear{x,v,v1}
/\ v1
IN aff_gt {x} {v,u}
==>
aff_gt {x} {v,v1}
SUBSET aff_gt {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`v1:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`v1:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % v + t3' % (
t1 % x + t2 % v + t3 % u)
=(t1'+ t3'*t1) % x + (t2'+ t3' * t2) % v + (t3' * t3) % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t3' * t1:real`
THEN EXISTS_TAC`t2' + t3' * t2:real`
THEN EXISTS_TAC`t3' * t3:real`
THEN MRESA_TAC
REAL_LT_MUL[`t3':real`;`t2:real`]
THEN MRESA_TAC
REAL_LT_MUL[`t3':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t3' *
t1) + (t2' + t3' * t2) + t3' * t3=
t1'+ t2' + t3'*(t1+t2+t3)`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_ge1_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear{x,v1,u}
/\ v1
IN aff_ge {x} {v,u}
==>
aff_ge {x} {v1,u}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v1:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v1:real^3`;`u:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u) + t3' % u
=(t1'+ t2'*t1) % x + (t2'* t2) % v + (t2' * t3 + t3') % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2:real`
THEN EXISTS_TAC`t2' * t3 +t3':real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + t2' * t2 + t2' * t3 + t3'=
t1'+t2'*(t1+t2+t3)+t3'`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_ge_1_1_subset_aff_ge_fan=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~(x=v1)
/\ v1
IN aff_ge {x} {v,u}
==>
aff_ge {x} {v1}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GE_1_1[`x:real^3`;`v1:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u)
=(t1'+ t2'*t1) % x + (t2'* t2) % v + (t2' * t3 ) % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2:real`
THEN EXISTS_TAC`t2' * t3 :real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + t2' * t2 + t2' * t3 =
t1'+t2'*(t1+t2+t3)`; REAL_ARITH`A* &1=A`]);;
let decomposition_planar_by_angle_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3.
~
collinear {x,v,u} /\ ~collinear {x,v,w}
/\ w
IN aff_ge {x,v} {u}
==> u
IN aff_gt {x} {v,w} \/ w
IN aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
aff_ge_inter_aff_ge[`(x:real^3)`;`(v:real^3)`;`(u:real^3)`][
INTER;
IN_ELIM_THM]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_EQ_0_GE[`x:real^3`;`v:real^3`;`w:real^3`; `u:real^3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(
th)])
THEN MRESA_TAC
AZIM_EQ_0_ALT[`x:real^3`;`v:real^3`;`w:real^3`; `u:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`(&0 < t2) \/ &0 <= --(t2:real)`)
THENL[
SUBGOAL_THEN `u
IN aff_gt {x} {v,w:real^3}` ASSUME_TAC
THENL[
MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN MP_TAC(REAL_ARITH`&0< t3==> &0 <= t3:real`)
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC THEN SET_TAC[]];
MRESA_TAC
remove_variable_fan[`x:real^3`; `v:real^3`; `w:real^3`;`u:real^3`;`t1:real`;`t2:real`;`t3:real`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(
th);])
THEN DISCH_TAC
THEN REWRITE_TAC[VECTOR_ARITH`inv t3 % u - (inv t3 *
t1) % x - (inv t3 * t2) % v
=(--inv t3 *
t1) % x + inv t3 % u + (inv t3 * (--t2)) % v`]
THEN MP_TAC(REAL_ARITH`&0<t3==> ~( t3= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
THEN MRESA1_TAC
REAL_LT_INV`t3:real`
THEN MP_TAC(REAL_ARITH`&0< inv t3==> &0 <= inv t3`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`inv t3:real`;`-- (t2:real)`]
THEN DISCH_TAC
THEN SUBGOAL_THEN `w
IN aff_ge {x, u} {v:real^3}` ASSUME_TAC
THENL[
MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GE_2_1[`x:real^3`;`u:real^3`;`v:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`(--inv t3 *
t1):real`
THEN EXISTS_TAC`inv t3:real`
THEN EXISTS_TAC`(inv t3 * --t2):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`--inv t3 *
t1 + inv t3 + inv t3 * --t2=
inv t3 * (t3+ &1- (
t1 +t2 + t3))`; REAL_ARITH`a + &1 - &1 =a`];
POP_ASSUM MP_TAC THEN SET_TAC[]]]);;
let point_in_aff_ge=prove(`!(x:real^3) (v:real^3) (w:real^3).
~collinear {x,v,w}
==>
x
IN aff_ge {x} {v,w}
/\ v
IN aff_ge {x} {v,w}
/\ w
IN aff_ge {x} {v,w}`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC
th3 [`x:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GE_1_2)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[
IN_ELIM_THM]
THEN STRIP_TAC
THENL[ EXISTS_TAC`&1:real`
THEN EXISTS_TAC`&0:real`
THEN EXISTS_TAC`&0:real`
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC
THENL[ EXISTS_TAC`&0:real`
THEN EXISTS_TAC`&1:real`
THEN EXISTS_TAC`&0:real`
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC;
EXISTS_TAC`&0:real`
THEN EXISTS_TAC`&0:real`
THEN EXISTS_TAC`&1:real`
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC]]);;
let aff_ge_subset_aff_gt_union_aff_ge=prove(`!(x:real^3) (v:real^3) (w:real^3).
~collinear {x,v,w}
==>
aff_ge {x} {v , w}
SUBSET (aff_gt {x , v} {w})
UNION (aff_ge {x} {v})`,
REPEAT STRIP_TAC THEN MRESA_TAC
th3 [`x:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GE_1_2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GT_2_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]
AFF_GE_1_1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM]
THEN GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `(&0 <= (t3:real)) <=> (&0 < t3) \/ ( t3 = &0)`; TAUT `(a \/ b) /\ (c \/ d) /\ e /\ f <=> ((a \/ b)/\ c /\ e /\ f) \/ ((a \/ b) /\ d /\ e /\ f)`;
EXISTS_OR_THM] THEN
MATCH_MP_TAC MONO_OR THEN
SUBGOAL_THEN `((?t1:real t2:real t3:real.
(&0 < t2 \/ t2 = &0) /\
&0< t3 /\
t1 + t2 + t3 = &1 /\
(x':real^3) =
t1 % x + t2 % v + t3 % w)
==> (?t1 t2 t3.
&0< t3 /\
t1 + t2 + t3 = &1 /\ x' =
t1 % x + t2 % v + t3 % w))` ASSUME_TAC
THENL
[MESON_TAC[];
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `(&0< (t2:real) \/ (t2 = &0)) <=> ( &0<= t2)`] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN
POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC [REAL_ARITH `(a:real)+ &0 = a`; VECTOR_ARITH `&0 % (w:real^3) =
vec 0`;
VECTOR_ARITH ` ((x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v:real^3) +
vec 0)<=> ( x' =
t1 % x + t2 % v )` ]
THEN MESON_TAC[]]);;
let pos_in_aff_ge_fan=prove(`!x:real^3 v:real^3 u:real^3 a:real.
DISJOINT {x} {v,u}
/\ &0<a /\ a< &1
==>
(&1-a)%v + a % u
IN aff_ge {x} {v,u:real^3}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1 -a:real`
THEN EXISTS_TAC`a:real`
THEN MP_TAC(REAL_ARITH`&0< a /\ a < &1 ==> &0 <= &1 - a /\ &0 <= a`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC);;
let aff_gt1_subset_aff_gt=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~collinear {x,v1,u}
/\ v1
IN aff_gt {x} {v,u}
==>
aff_gt {x} {v1,u}
SUBSET aff_gt {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v1:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v1:real^3`;`u:real^3`][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u) + t3' % u
=(t1'+ t2'*t1) % x + (t2'* t2) % v + (t2' * t3 + t3') % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2:real`
THEN EXISTS_TAC`t2' * t3 +t3':real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LT_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LT_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + t2' * t2 + t2' * t3 + t3'=
t1'+t2'*(t1+t2+t3)+t3'`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let aff_ge_eq_aff_gt_union_aff_ge=prove(`!(x:real^3) (v:real^3) (w:real^3).
~collinear {x,v,w}
==>
aff_ge {x} {v , w} = (aff_gt {x} {v,w})
UNION (aff_ge {x} {v})
UNION (aff_ge {x} {w})`,
REPEAT STRIP_TAC THEN MRESA_TAC
th3 [`x:real^3`;`v:real^3`;`w:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GE_1_2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]
AFF_GT_1_2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]
AFF_GE_1_1)
THEN MP_TAC(ISPECL[`x:real^3`;`w:real^3`]
AFF_GE_1_1) THEN RESA_TAC THEN RESA_TAC
THEN ASM_REWRITE_TAC[
EXTENSION;
UNION;
IN_ELIM_THM]
THEN GEN_TAC THEN EQ_TAC
THENL[STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2/\ &0<=t3==> (t2= &0)\/ (t3= &0)\/ (&0<t2 /\ &0<t3)`)
THEN RESA_TAC
THENL[
SUBGOAL_THEN `(?t1' t2'.
&0 <= t2' /\
t1' + t2' = &1 /\
t1 % x + &0 % v + t3 % w = t1' % x + t2' % w:real^3)`ASSUME_TAC
THENL[
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t3:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC THEN SET_TAC[]];
SUBGOAL_THEN `(?t1' t2'.
&0 <= t2' /\
t1' + t2' = &1 /\
t1 % x + t2 % v + &0 % w = t1' % x + t2' % v:real^3)`ASSUME_TAC
THENL[
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC THEN SET_TAC[]];
SUBGOAL_THEN `(?t1' t2' t3'.
&0 < t2' /\
&0 < t3' /\
t1' + t2' + t3' = &1 /\
t1 % x + t2 % v + t3 % w = t1' % x + t2' % v + t3' % w:real^3)`ASSUME_TAC
THENL[
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC THEN SET_TAC[]]];
STRIP_TAC
THENL[
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`&0:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
EXISTS_TAC`t1:real`
THEN EXISTS_TAC`&0:real`
THEN EXISTS_TAC`t2:real`
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC]]);;
let aff_ge1_1_subset_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
DISJOINT {x} {v,u} /\ ~(x=v1)
/\ v1
IN aff_ge {x} {v,u}
==>
aff_ge {x} {v1}
SUBSET aff_ge {x} {v,u}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GE_1_1[`x:real^3`;`v1:real^3`;][
IN_ELIM_THM;
SUBSET]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % (
t1 % x + t2 % v + t3 % u)
=(t1'+ t2'*t1) % x + (t2'* t2) % v + (t2' * t3 ) % u:real^3`]
THEN STRIP_TAC
THEN EXISTS_TAC`t1' + t2' * t1:real`
THEN EXISTS_TAC`t2' * t2:real`
THEN EXISTS_TAC`t2' * t3:real`
THEN MP_TAC(REAL_ARITH`&0<t2'==> &0<= t2'`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t2:real`]
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`t3:real`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t2' *
t1) + t2' * t2 + t2' * t3 =
t1'+t2'*(t1+t2+t3)`; REAL_ARITH`A* &1=A`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;
let properties1_inside_fan=prove(`!x:real^3 u:real^3 w:real^3.
DISJOINT {x} {u,w}
/\ &0<a /\ a< &1
==> (&1-a)%u+ a%w
IN aff_ge {x} {u,w:real^3}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`u:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1 -a:real`
THEN EXISTS_TAC`a:real`
THEN MP_TAC(REAL_ARITH`&0< a /\ a < &1 ==> &0 <= &1 - a /\ &0 <= a`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC);;
let properties_inside_collinear1_fan=prove(`!x:real^3 u:real^3 w:real^3.
~collinear{x,u,w}
/\ &0<a /\ a< &1
==> aff_ge {x} {u}
INTER aff_ge {x} {(&1-a)%u+ a%w,w:real^3}
SUBSET aff_ge {x} {}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
properties_inside_collinear_fan[`(x:real^3)`;`(u:real^3)`;`(w:real^3)`;`a:real`]
THEN MRESA_TAC
th3[`(x:real^3)`;`((&1-a)%u+ a%w:real^3)`;`(w:real^3)`]
THEN MRESA_TAC
th3[`(x:real^3)`;`u:real^3`;`(w:real^3)`]
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`(&1-a)%u+ a%w:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GE_1_1[`x:real^3`;`u:real^3`][
IN_ELIM_THM;
INTER;
SUBSET;
AFF_GE_EQ_AFFINE_HULL;
AFFINE_HULL_1]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`&1`
THEN REDUCE_VECTOR_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2' /\ &0 <= t3==> (t2'= &0 /\ t3 = &0)\/ (&0< t2' \/ &0 <t3) `)
THEN RESA_TAC
THENL[REDUCE_ARITH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC;
STRIP_TAC THEN
REWRITE_TAC[VECTOR_ARITH`
t1 % x + t2 % u = t1' % x + t2' % ((&1 - a) % u + a % w) + t3 % w
<=> (t2'* a + t3) % w = (t1-t1') % x +( t2-t2' * (&1-a))% u :real^3`]
THEN MRESA_TAC
REAL_LT_MUL[`t2':real`;`a:real`]
THEN MP_TAC(REAL_ARITH` &0< t2'*(a) /\ &0<= t3 ==> &0 < t2'*(a)+t3 /\ ~(t2'*(a)+t3:real= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t2'*(a)+t3:real`
THEN MRESA1_TAC
REAL_LT_INV`t2'*(a)+t3:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(t2'* a + t3) % w = (t1-t1') % x +( t2-t2' * (&1-a))% u:real^3
==> (inv (t2' * a+t3))%((t2'* a + t3) % w) = (inv (t2' * a+t3))%( (t1-t1') % x +( t2-t2' * (&1-a))% u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`w
IN aff {x,u:real^3}`ASSUME_TAC
THENL[REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv (t2' * a+t3)) * (
t1 - t1'):real`
THEN EXISTS_TAC`(inv (t2' * a+t3) * (t2 - t2' *(&1- a))):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (t2' * a + t3) * (
t1 - t1') + inv (t2' * a + t3) * (t2 - t2' * (&1 - a))
= inv (t2' * a + t3) * ((t2'*a +t3)+(
t1 + t2) -(t1'+ t2' +t3) ):real`; REAL_ARITH`A+ &1- &1= A`];
ASM_MESON_TAC[]];
STRIP_TAC THEN
REWRITE_TAC[VECTOR_ARITH`
t1 % x + t2 % u = t1' % x + t2' % ((&1 - a) % u + a % w) + t3 % w
<=> (t2'* a + t3) % w = (t1-t1') % x +( t2-t2' * (&1-a))% u :real^3`]
THEN MP_TAC(REAL_ARITH`&0<a==> &0<=a`) THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`t2':real`;`a:real`]
THEN MP_TAC(REAL_ARITH` &0<= t2'*(a) /\ &0< t3 ==> &0 < t2'*(a)+t3 /\ ~(t2'*(a)+t3:real= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t2'*(a)+t3:real`
THEN MRESA1_TAC
REAL_LT_INV`t2'*(a)+t3:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(t2'* a + t3) % w = (t1-t1') % x +( t2-t2' * (&1-a))% u:real^3
==> (inv (t2' * a+t3))%((t2'* a + t3) % w) = (inv (t2' * a+t3))%( (t1-t1') % x +( t2-t2' * (&1-a))% u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`w
IN aff {x,u:real^3}`ASSUME_TAC
THENL[
REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv (t2' * a+t3)) * (
t1 - t1'):real`
THEN EXISTS_TAC`(inv (t2' * a+t3) * (t2 - t2' *(&1- a))):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (t2' * a + t3) * (
t1 - t1') + inv (t2' * a + t3) * (t2 - t2' * (&1 - a))
= inv (t2' * a + t3) * ((t2'*a +t3)+(
t1 + t2) -(t1'+ t2' +t3) ):real`; REAL_ARITH`A+ &1- &1= A`];
ASM_MESON_TAC[]]]);;
let exists_in_aff_gt=prove(`!x:real^3 v:real^3 u:real^3.
~collinear {x,v,u} ==> ?y:real^3. y
IN aff_gt {x} {v, u}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&0 % x+ &1 / &2 % v+ &1/ &2 %u:real^3 `
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1/ &2`
THEN EXISTS_TAC`&1/ &2`
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC);;
let in_aff_2_2_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3.
~coplanar {x,v,u,w}
==>
(!t:real. &0< t /\ t< &1
==> (!t1:real t2:real t3:real. &0<t3 /\ t1+t2+t3= &1
==>
t1 % x + t2 % v + t3 % ((&1 - t) % u + t % w)
IN aff_gt {x,v} {u,w}))`,
REPEAT STRIP_TAC
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w:real^3`]
THEN SUBGOAL_THEN `
DISJOINT {x,v:real^3} {u,w:real^3}` ASSUME_TAC
THENL[
REWRITE_TAC[
DISJOINT_SYM;SET_RULE`{v:real^3,w:real^3}= {v}
UNION {w}`;
DISJOINT_UNION]
THEN REWRITE_TAC[SET_RULE`{v}
UNION {w}={v:real^3,w:real^3}`]
THEN ONCE_REWRITE_TAC[
DISJOINT_SYM]
THEN ASM_REWRITE_TAC[];
MRESAL_TAC
AFF_GT_2_2[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN EXISTS_TAC`t3*(&1-t):real`
THEN EXISTS_TAC`t3*(t):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`
t1 +t2+ t3 * (&1 - t) + t3 * t = t1+t2+t3:real`;VECTOR_ARITH`
t1 % x + t2 % v + t3 % ((&1 - t) % u + t % w) =
t1 % x + t2 % v + (t3 * (&1 - t)) % u + (t3 * t) % w:real^3`]
THEN STRIP_TAC THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_TAC
THEN REAL_ARITH_TAC]);;
let condition_to_in_aff_gt_by_angle=prove(`!x:real^3 v:real^3 u:real^3 s1:real.
~collinear {x,v,u} /\ &0< (v - x)
dot (u - x) /\ &0< s1
/\ s1<
atn ((
norm ((v - x)
cross (u - x))) * inv((v - x)
dot (u - x)))
==>
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u + x
IN aff_gt {x} {v, u}`,
REPEAT STRIP_TAC
THEN ASSUME_TAC(ISPEC`(
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x))):real`
ATN_BOUNDS)
THEN MP_TAC (REAL_ARITH`s1<
atn ((
norm ((v - x)
cross (u - x))) * inv((v - x)
dot (u - x)))
/\
atn ((
norm ((v - x)
cross (u - x))) * inv((v - x)
dot (u - x))) < pi/ &2
==> s1<
pi / &2`) THEN RESA_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN REWRITE_TAC[VECTOR_ARITH`
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u + x =
t1 % x + t2 % v + t3 % u
<=>
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u =
(t1- &1) % x + t2 % v + t3 % u`;
e1_fan;
e2_fan;
e3_fan;
CROSS_LMUL;
CROSS_RMUL]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`-- (A-B) = B-A:real^3`]
THEN SUBGOAL_THEN`~(
norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL[
ASM_REWRITE_TAC[
NORM_EQ_0;VECTOR_ARITH`v-x=
vec 0<=> x=v`];
MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; REAL_ARITH`(((A*B)*D)*D)=A*B*(D pow 2)`;]
THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A%(B-C)=A%B-A%C`]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`;
DOT_SQUARE_NORM;REAL_ARITH`(A*B*C pow 2) * D pow 2=A*B*(C*D) pow 2`;REAL_ARITH`A* &1 pow 2=A`;
NORM_MUL;
REAL_ABS_INV;
REAL_ABS_NORM;
REAL_INV_MUL;
REAL_INV_INV
; ]
THEN ASM_REWRITE_TAC[REAL_ARITH`A*(B*C) * D pow 2= A*C * D*(D*B)`;REAL_ARITH`A*B* &1= A*B`;VECTOR_ARITH`A-B+C%D-C%E=A-B+C%(D-E)`;VECTOR_ARITH`A-C%D+B%D=A+(B-C)%D`;
REAL_ARITH`A*B-(C*D*B)*E=B*(A-C*D*E)`]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_SKEW]
THEN SUBGOAL_THEN`~(
norm((v - x)
cross (u - x:real^3))= &0)` ASSUME_TAC
THENL[
ASM_REWRITE_TAC[
NORM_EQ_0]
THEN MP_TAC(ISPECL[`v-x:real^3`;`u-x:real^3`]
CROSS_EQ_0)
THEN ONCE_REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ASM_REWRITE_TAC[];
MP_TAC(ISPEC`
norm((v - x)
cross (u - x:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASSUME_TAC(ISPEC`(v - x)
cross (u - x:real^3)`
NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(
norm ((v - x)
cross (u - x:real^3)) = &0)/\ &0 <=
norm ((v - x)
cross (u - x:real^3))==> &0<
norm ((v - x)
cross (u - x:real^3)) `)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`
norm((v - x)
cross (u - x:real^3))`
THEN ASSUME_TAC(ISPEC`(v - x:real^3)`
NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(
norm ((v - x:real^3)) = &0)/\ &0 <=
norm ((v - x:real^3))==> &0<
norm ((v - x:real^3)) `)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`
norm((v - x:real^3))`
THEN MRESA1_TAC
COS_POS_PI2`s1:real`
THEN MRESA1_TAC
SIN_POS_PI2`s1:real`
THEN EXISTS_TAC`&1-(
sin s1 *
norm (v - x) * inv (
norm ((v - x)
cross (u - x))))
-(inv (
norm (v - x)) *
(
cos s1 -
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x:real^3))))`
THEN EXISTS_TAC `(inv (
norm (v - x)) *
(
cos s1 -
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x:real^3))))`
THEN EXISTS_TAC`(
sin s1 *
norm (v - x) * inv (
norm ((v - x)
cross (u - x:real^3))))`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<A-B<=> B<A`]
THEN ASSUME_TAC(
PI_WORKS)
THEN MP_TAC(REAL_ARITH`&0<
pi /\ &0< s1 ==> --(
pi / &2) < s1`)
THEN RESA_TAC
THEN MRESAL_TAC
TAN_MONO_LT[`s1:real`;`
atn (
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x))):real`][
ATN_TAN]
THEN MRESAL_TAC
REAL_LT_LMUL[`inv (
norm ((v - x)
cross (u - x:real^3)))`;`
tan s1:real`;`
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x:real^3))`][REAL_ARITH`A*B*C=(A*B)*C`;REAL_ARITH`&1*A=A`]
THEN MP_TAC(REAL_ARITH`&0<(v - x)
dot (u - x:real^3)==> ~((v - x)
dot (u - x:real^3)= &0)`)
THEN RESA_TAC
THEN MP_TAC(ISPEC`(v - x)
dot (u - x:real^3)`REAL_MUL_LINV)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0<
cos s1 ==> ~(
cos s1= &0)`)
THEN RESA_TAC
THEN MP_TAC(ISPEC`
cos s1`REAL_MUL_LINV)
THEN RESA_TAC
THEN MRESAL_TAC
REAL_LT_RMUL[`inv (
norm ((v - x)
cross (u - x:real^3)))*
tan s1:real`;`inv ((v - x)
dot (u - x:real^3))`;`(v - x)
dot (u - x:real^3)`][REAL_ARITH`(A*B)*C=A*C*B`;
tan]
THEN MRESAL_TAC
REAL_LT_RMUL[`inv (
norm ((v - x)
cross (u - x:real^3)))* ((v - x)
dot (u - x:real^3))*
sin s1 /
cos s1`;`&1`;`
cos s1`][REAL_ARITH`&1* A=A`;
real_div;REAL_ARITH`(A*B*C*D)*E=(C*A*B)*(D*E)`;REAL_ARITH`A* &1=A`]
THEN ASM_TAC THEN REAL_ARITH_TAC;
STRIP_TAC
THENL[
MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THENL[
REAL_ARITH_TAC;
VECTOR_ARITH_TAC]]]]]);;
let condition1_to_in_aff_gt_by_angle=prove(`!x:real^3 v:real^3 u:real^3 s1:real.
~collinear {x,v,u} /\ &0< s1 /\ s1< pi/ &2
/\ (v - x)
dot (u - x:real^3) <= &0
==>
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u + x
IN aff_gt {x} {v, u}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN REWRITE_TAC[VECTOR_ARITH`
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u + x =
t1 % x + t2 % v + t3 % u
<=>
sin s1 %
e1_fan x v u +
cos s1 %
e3_fan x v u =
(t1- &1) % x + t2 % v + t3 % u`;
e1_fan;
e2_fan;
e3_fan;
CROSS_LMUL;
CROSS_RMUL]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`-- (A-B) = B-A:real^3`]
THEN SUBGOAL_THEN`~(
norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL[
ASM_REWRITE_TAC[
NORM_EQ_0;VECTOR_ARITH`v-x=
vec 0<=> x=v`];
MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; REAL_ARITH`(((A*B)*D)*D)=A*B*(D pow 2)`;]
THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A%(B-C)=A%B-A%C`]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`;
DOT_SQUARE_NORM;REAL_ARITH`(A*B*C pow 2) * D pow 2=A*B*(C*D) pow 2`;REAL_ARITH`A* &1 pow 2=A`;
NORM_MUL;
REAL_ABS_INV;
REAL_ABS_NORM;
REAL_INV_MUL;
REAL_INV_INV
; ]
THEN ASM_REWRITE_TAC[REAL_ARITH`A*(B*C) * D pow 2= A*C * D*(D*B)`;REAL_ARITH`A*B* &1= A*B`;VECTOR_ARITH`A-B+C%D-C%E=A-B+C%(D-E)`;VECTOR_ARITH`A-C%D+B%D=A+(B-C)%D`;
REAL_ARITH`A*B-(C*D*B)*E=B*(A-C*D*E)`]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_SKEW]
THEN SUBGOAL_THEN`~(
norm((v - x)
cross (u - x:real^3))= &0)` ASSUME_TAC
THENL[
ASM_REWRITE_TAC[
NORM_EQ_0]
THEN MP_TAC(ISPECL[`v-x:real^3`;`u-x:real^3`]
CROSS_EQ_0)
THEN ONCE_REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ASM_REWRITE_TAC[];
MP_TAC(ISPEC`
norm((v - x)
cross (u - x:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASSUME_TAC(ISPEC`(v - x)
cross (u - x:real^3)`
NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(
norm ((v - x)
cross (u - x:real^3)) = &0)/\ &0 <=
norm ((v - x)
cross (u - x:real^3))==> &0<
norm ((v - x)
cross (u - x:real^3)) `)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`
norm((v - x)
cross (u - x:real^3))`
THEN ASSUME_TAC(ISPEC`(v - x:real^3)`
NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(
norm ((v - x:real^3)) = &0)/\ &0 <=
norm ((v - x:real^3))==> &0<
norm ((v - x:real^3)) `)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`
norm((v - x:real^3))`
THEN MRESA1_TAC
COS_POS_PI2`s1:real`
THEN MRESA1_TAC
SIN_POS_PI2`s1:real`
THEN EXISTS_TAC`&1-(
sin s1 *
norm (v - x) * inv (
norm ((v - x)
cross (u - x))))
-(inv (
norm (v - x)) *
(
cos s1 -
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x:real^3))))`
THEN EXISTS_TAC `(inv (
norm (v - x)) *
(
cos s1 -
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x:real^3))))`
THEN EXISTS_TAC`(
sin s1 *
norm (v - x) * inv (
norm ((v - x)
cross (u - x:real^3))))`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<A-B<=> B<A`]
THEN MATCH_MP_TAC(REAL_ARITH`&0<
cos s1 /\
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x)) <= &0==>
sin s1 * inv (
norm ((v - x)
cross (u - x))) * ((v - x)
dot (u - x)) <
cos s1`)
THEN ASM_REWRITE_TAC[REAL_ARITH`A *B *C<= &0<=> &0<= A*B*(-- C)`]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN MP_TAC(REAL_ARITH`&0<
sin s1==> &0<=
sin s1`) THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN MP_TAC(REAL_ARITH`&0< inv (
norm ((v - x)
cross (u - x)))==> &0<= inv (
norm ((v - x)
cross (u - x)))`) THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC;
STRIP_TAC
THENL[
MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THENL[
REAL_ARITH_TAC;
VECTOR_ARITH_TAC]]]]]);;
let scale_in_edges_fan=prove(`!(x:real^3) (v:real^3) (u:real^3) (w:real^3).
DISJOINT {x} {v,u}
/\ w
IN aff_gt {x} {v,u}
==>
(?a t:real. &0<a /\ &0<t /\ t< &1
/\ a%(w-x) = (&1-t)% v+ t%u-x)`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[VECTOR_ARITH`w =
t1 % x + t2 % v + t3 % u
<=> w-x = ((t1+t2+t3)- &1) % x + (((t1+t2+t3) -t1)- t3)% (v-x) + t3 % (u-x):real^3`]
THEN ASM_REWRITE_TAC[REAL_ARITH`&1- &1= &0`] THEN REDUCE_VECTOR_TAC
THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3 /\ t1+t2+t3= &1 ==> ~(&1-t1= &0)/\ &0< &1-
t1`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV `(&1-t1:real)`
THEN MRESA1_TAC
REAL_LT_INV `(&1-t1:real)`
THEN MRESA_TAC
REAL_LT_MUL [`inv(&1-t1:real)`;`t3:real`]
THEN MRESA_TAC
REAL_LT_MUL [`inv(&1-t1:real)`;`t2:real`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[REAL_ARITH`inv (&1 -
t1) * t2=inv (&1 -
t1) * ((t1+t2+t3)-t1)- inv(&1-t1)*t3:real`]
THEN RESA_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
w - x = (&1 -
t1 - t3) % (v - x) + t3 % (u - x):real^3
==> (inv (&1-
t1))%(w - x ) = (inv (&1-t1))%((&1 -
t1 - t3) % (v - x) + t3 % (u - x))
`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C= (A*B)%C`;VECTOR_ARITH`A%(B+C)=A%B+A%C`;REAL_ARITH`inv (&1 -
t1) * (&1 -
t1 - t3)=inv (&1 -
t1) * (&1 -
t1) - inv (&1 -
t1) * (t3)`;VECTOR_ARITH`(&1-A)%(U-X)+A%(V-X)=(&1-A)%U+A%V-X`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`inv(&1- t1:real)`
THEN EXISTS_TAC`inv(&1-t1) *t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`A< &1<=> &0< &1- A`]);;
let aff_gt_imp_not_collinear=prove(`!x u v w:real^3.
~collinear{x,v,u}/\ w
IN aff_gt{x,v} {u}==> ~collinear{x,v,w}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN ASM_REWRITE_TAC[
collinear_fan;aff;
AFFINE_HULL_2;
IN_ELIM_THM;]
THEN DISCH_THEN(LABEL_TAC"A")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "A" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`
t1 % x + t2 % v + t3 % u = u' % x + v' % v<=>
t3 % u = (u'-t1) % x + (v'-t2) % v`]
THEN MP_TAC(REAL_ARITH`&0<t3==> ~(t3= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`t3 % u = (u' -
t1) % x + (v' - t2) % v:real^3
==> (inv (t3))%(t3 % u ) = (inv (t3))%( (u' -
t1) % x + (v' - t2) % v)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`(inv (t3)) * (u' -
t1):real`
THEN EXISTS_TAC`(inv (t3)) * (v' -t2):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (t3) * (u' -
t1) + inv (t3) * (v'- t2)
= inv (t3) * (t3+ (u'+v')- (
t1 + t2 +t3)):real`; REAL_ARITH`A+ &1- &1= A`]);;
let aff_gt_1_2_scale_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 a:real.
&0< a /\ a % (u-x)= w-x /\ ~collinear {x,w,v}
==> aff_gt {x} {u,v} =aff_gt {x} {w,v}`,
REPEAT GEN_TAC
THEN GEOM_ORIGIN_TAC `x:real^3`
THEN REDUCE_VECTOR_TAC
THEN REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0<a:real==> ~(a= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV `a:real`
THEN MRESA1_TAC
REAL_LT_INV`a:real`
THEN FIND_ASSUM(MP_TAC)`a %u=w:real^3`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
a%u=w:real^3
==> (inv (a))%(a%u) = (inv (a))%(w)`)
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C:real^3`]
THEN REWRITE_TAC[VECTOR_ARITH`&1 % u= inv a % w<=> inv a % w= u`]
THEN STRIP_TAC
THEN MRESA_TAC
COLLINEAR_SPECIAL_SCALE[`a:real`;`u:real^3`;`v:real^3`]
THEN MRESA_TAC
th3[`((
vec 0):real^3)` ;` (u:real^3)`;`(v:real^3) `;]
THEN MRESA_TAC
th3[`((
vec 0):real^3)` ;` (w:real^3)`;`(v:real^3) `;]
THEN MRESAL_TAC
AFF_GT_1_2[`(
vec 0):real^3`;`u:real^3`;`v:real^3`][
IN_ELIM_THM;
EXTENSION]
THEN MRESAL_TAC
AFF_GT_1_2[`(
vec 0):real^3`;`w:real^3`;`v:real^3`][
IN_ELIM_THM]
THEN REDUCE_VECTOR_TAC
THEN GEN_TAC THEN EQ_TAC
THENL[ STRIP_TAC
THEN EXISTS_TAC`&1- inv a * t2-t3:real`
THEN EXISTS_TAC `inv a * t2:real`
THEN EXISTS_TAC `t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - inv a * t2 - t3 + inv a * t2 + t3 = &1`;VECTOR_ARITH`(A*B)%C=B%(A%C)`]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[];
STRIP_TAC
THEN EXISTS_TAC`&1- a * t2-t3:real`
THEN EXISTS_TAC `a * t2:real`
THEN EXISTS_TAC `t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - a * t2 - t3 + a * t2 + t3 = &1`;VECTOR_ARITH`(A*B)%C=B%(A%C)`]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]]);;
let in_aff_gt_1_2=prove(`!x:real^3 v:real^3 u:real^3 t:real.
DISJOINT {x} {v,u} /\ &0< t /\ t< &1==> (&1-t)% v+ t% u
IN aff_gt {x} {v,u}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM;]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1 - t:real`
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1 - t<=> t< &1`;REAL_ARITH`&0 + &1 - t + t= &1`]
THEN VECTOR_ARITH_TAC);;
let sym_line1_fan=prove(`!x y z:real^N. x
IN aff {y, z} /\ ~(x=y)
==> z
IN aff {x,y}`,
REPEAT GEN_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`(v= &0)\/ ~(v= &0)`)
THENL[ ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN RESA_TAC
THEN REDUCE_VECTOR_TAC
THEN RESA_TAC
THEN SET_TAC[];
MP_TAC(ISPEC`(v:real)`REAL_MUL_LINV)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`inv(v:real)`
THEN EXISTS_TAC`-- inv(v:real) *u`
THEN ASM_REWRITE_TAC[REAL_ARITH` inv v + --inv v * u = inv v * (v+ &1- (u+v)) `;REAL_ARITH`A+ &1 - &1= A`;VECTOR_ARITH`inv v % (u % y + v % z) + (--inv v * u) % y=(inv v * v) % z `]
THEN REDUCE_VECTOR_TAC]);;
let sym_line0_fan=prove( `!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {x} {y,z}
==> aff {x,z}
SUBSET aff {x,y}`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
DISJOINT {x} {y,z}==> ~(x=y:real^N)`)
THEN RESA_TAC
THEN MRESA_TAC
sym_line1_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN MP_TAC(SET_RULE`x
IN aff {x, y} /\ z
IN aff {x, y} ==> {x, z:real^N}
SUBSET aff {x, y}`)
THEN REWRITE_TAC[
POINT_IN_LINE;]
THEN RESA_TAC
THEN MRESA_TAC
HULL_MONO[`affine:(real^N->bool)->bool`;` {x, z:real^N}`;`aff {x, y:real^N}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_AFFINE_EQ ]);;
let sym_line_fan=prove(`!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {x} {y,z}
==> aff {x,z} = aff {x,y}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
sym_line0_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN MRESA_TAC
sym_line0_fan[`x:real^N`;`z:real^N`;`y:real^N`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]);;
let sym_line01_fan=prove(`!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {y} {x,z}
==> aff {y,x}
SUBSET aff {y,z}`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`y
IN aff {y, z} /\ x
IN aff {y, z} ==> {y,x:real^N}
SUBSET aff {y,z}`)
THEN ASM_REWRITE_TAC[
POINT_IN_LINE;]
THEN STRIP_TAC
THEN MRESA_TAC
HULL_MONO[`affine:(real^N->bool)->bool`;` {y,x:real^N}`;`aff { y,z:real^N}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_AFFINE_EQ ]);;
let sym_line02_fan=prove(`!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {y} {x,z}
==> aff {y,z}
SUBSET aff {y,x}`,
REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
DISJOINT {y} {x,z}==> ~(x=y:real^N)`)
THEN RESA_TAC
THEN MRESA_TAC
sym_line1_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN MP_TAC(SET_RULE`y
IN aff {y, x} /\ z
IN aff {y, x} ==> {y,z:real^N}
SUBSET aff {y,x}`)
THEN ASM_REWRITE_TAC[
POINT_IN_LINE;]
THEN STRIP_TAC
THEN MRESA_TAC
HULL_MONO[`affine:(real^N->bool)->bool`;` {y,z:real^N}`;`aff { y,x:real^N}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_AFFINE_EQ ]
THEN POP_ASSUM MP_TAC
THEN ASSUME_TAC(SET_RULE`{y,x}={x,y}`)
THEN POP_ASSUM (fun th-> ASM_REWRITE_TAC[
th;])
THEN REWRITE_TAC[aff]
THEN RESA_TAC);;
let sym_line_fan0=prove(`!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {x} {y,z} /\
DISJOINT {y} {x,z}
==> aff {x,z} = aff {y,z}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
sym_line_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN SUBGOAL_THEN `y
IN aff {x,z:real^N}` ASSUME_TAC
THENL[ASM_REWRITE_TAC[
POINT_IN_LINE1];
MRESA_TAC
sym_line_fan[`y:real^N`;`x:real^N`;`z:real^N`]
THEN ASSUME_TAC(SET_RULE`{x,y}={y,x:real^N}`)
THEN ASM_REWRITE_TAC[]]);;
let sym_line_fan1=prove(`!x y z:real^N. x
IN aff {y, z} /\
DISJOINT {y} {x,z}
==> aff {y,z} = aff {y,x}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
sym_line01_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN MRESA_TAC
sym_line02_fan[`x:real^N`;`y:real^N`;`z:real^N`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]);;
let place_there_point_line_fan=prove(`!x:real^3 y:real^3 z:real^3.
~(x=y)/\ z
IN aff {x,y}==> ?t:real. &0<t /\ t< &1 /\ (&1-t)%y+t % z
IN aff_ge {x} {y}`,
REPEAT GEN_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN RESA_TAC
THEN MRESAL_TAC
AFF_GE_1_1[`x:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN DISJ_CASES_TAC(REAL_ARITH`&0<= v \/ v< &0`)
THENL[EXISTS_TAC`&1/ &2`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1/ &2 /\ &1/ &2< &1`]
THEN EXISTS_TAC`&1/ &2 *u`
THEN EXISTS_TAC`&1/ &2*(&1+v)`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1/ &2 *u + &1/ &2 * (&1 + v)= &1/ &2 *(&1 +(u+v))`;REAL_ARITH`&1 / &2 * (&1 + &1) = &1`;VECTOR_ARITH`(&1 - &1 / &2) % y + &1 / &2 % (u % x + v % y) =
(&1 / &2 * u) % x + (&1 / &2 * (&1 + v)) % y`]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1/ &2`]
THEN MATCH_MP_TAC
REAL_LE_ADD
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
EXISTS_TAC`inv u`
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`v< &0 <=> (u+v)< u `]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&1< u==> &0< u /\ ~(u= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV `u:real`
THEN MRESA1_TAC
REAL_INV_LT_1 `u:real`
THEN MRESA1_TAC REAL_MUL_LINV `u:real`
THEN EXISTS_TAC`&1`
THEN EXISTS_TAC `&0`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &0 /\ &1 + &0 = &1/\ u+ &1 - &1 =u`;VECTOR_ARITH`(&1 - inv u) % y + inv u % (u % x + v % y)=(&1 - inv u*(u+ &1- (u+v))) % y + (inv u * u) % x /\ (&1 - &1) % y + &1 % x = &1 % x + &0 % y`]]);;
let permutes_4points_collinear=prove(`!x y z w:real^N.
~(x=y)/\ ~(x=z) /\ y
IN aff {x,z}/\ ~collinear{x,y,w}==> ~collinear{x,z,w}`,
REWRITE_TAC[
collinear_fan]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`~(x=y)/\ ~(x=z) ==>
DISJOINT {x} {y, z:real^N}`)
THEN RESA_TAC
THEN MRESA_TAC
sym_line_fan1[`y:real^N`;`x:real^N`;`z:real^N`]);;
let permutes_4points_collinear1=prove(`!x y z w:real^N.
~(x=y)/\ ~(x=z) /\ y
IN aff {x,z}/\ ~collinear{x,z,w}==> ~collinear{x,y,w}`,
REWRITE_TAC[
collinear_fan]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`~(x=y)/\ ~(x=z) ==>
DISJOINT {x} {y, z:real^N}`)
THEN RESA_TAC
THEN MRESA_TAC
sym_line01_fan[`y:real^N`;`x:real^N`;`z:real^N`]
THEN ASM_TAC THEN SET_TAC[]);;
let in_aff_gt_eq_azim=prove(`!x y z
w0 w1:real^3.
~(x=z) /\ y
IN aff_gt {x} {z}==>
azim x y
w0 w1=
azim x z
w0 w1`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GT_1_1[`x:real^3`;`z:real^3`][
IN_ELIM_THM;SET_RULE`
DISJOINT {x} {z}<=> ~(x=z)`]
THEN ASM_TAC
THEN GEOM_ORIGIN_TAC `x:real^3`
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`u % (x +
vec 0) + v%(x+ z)= (u+v)%x+v %z`;VECTOR_ARITH`(x + y = &1 % x + v % z)<=> y = v % z`]
THEN RESA_TAC
THEN ASM_TAC THEN SET_TAC[
AZIM_SPECIAL_SCALE]);;
let no_origin_aff_ge_is_aff_gt=prove(`!x y z:real^3.
~(x=y) /\ ~(x=z) /\ z
IN aff_ge {x} {y}==> z
IN aff_gt {x} {y}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GT_1_1[`x:real^3`;`y:real^3`][
IN_ELIM_THM;SET_RULE`
DISJOINT {x} {z}<=> ~(x=z)`]
THEN MRESAL_TAC
AFF_GE_1_1[`x:real^3`;`y:real^3`][
IN_ELIM_THM;SET_RULE`
DISJOINT {x} {z}<=> ~(x=z)`]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2`)
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN RESA_TAC
THEN REDUCE_VECTOR_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN EXISTS_TAC`t1:real`
THEN EXISTS_TAC`t2:real`
THEN ASM_REWRITE_TAC[]);;
let aff_ge_2_1_is_exists_point_inaff_ge_1_2=prove(`!x:real^3 y:real^3 z:real^3 w:real^3.
DISJOINT {x} {y,w} /\
DISJOINT {x,y} {w}/\ z
IN aff_ge {x,y} {w}==> ?t. &0<t /\ t< &1 /\ (&1-t) %y+ t%z
IN aff_ge {x} {y,w}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GE_2_1[`x:real^3`;`y:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GE_1_2[`x:real^3`;`y:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN DISJ_CASES_TAC(REAL_ARITH`&0<= t2 \/ t2 < &0`)
THENL[EXISTS_TAC`&1/ &2`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1/ &2/\ &1/ &2 < &1`]
THEN EXISTS_TAC`&1/ &2 * t1:real`
THEN EXISTS_TAC`&1/ &2 * (t2+ &1):real`
THEN EXISTS_TAC`&1/ &2 * t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 / &2 *
t1 + &1 / &2 * (t2 + &1) + &1 / &2 * t3 = &1/ &2 *(&1 +(t1+t2+t3))`;VECTOR_ARITH`(&1 - &1 / &2) % y + &1 / &2 % (
t1 % x + t2 % y + t3 % w) =
(&1 / &2 *
t1) % x + (&1 / &2 * (t2 + &1)) % y + (&1 / &2 * t3) % w`;REAL_ARITH`&1/ &2 *(&1 + &1)= &1`]
THEN STRIP_TAC
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1/ &2`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
EXISTS_TAC`inv(&1 - t2):real`
THEN MP_TAC(REAL_ARITH`t2< &0 ==> &0< &1 -t2 /\ &1< &1 -t2 /\ &0<= &1 -t2 /\ ~(&1- t2= &0) `)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`&1-t2`
THEN MRESA1_TAC
REAL_LE_INV`&1-t2`
THEN MRESA1_TAC REAL_MUL_LINV `&1- t2:real`
THEN MRESA1_TAC
REAL_INV_LT_1`&1- t2`
THEN EXISTS_TAC`inv(&1 - t2)* t1:real`
THEN EXISTS_TAC`inv(&1 - t2)* t2 + &1 - inv(&1 - t2):real`
THEN EXISTS_TAC`inv(&1 - t2)* t3`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1 - t2) *
t1 +
(inv (&1 - t2) * t2 + &1 - inv (&1 - t2)) +
inv (&1 - t2) * t3= inv (&1 - t2) * (
t1 +t2+t3)+ &1 - inv (&1 - t2) /\ inv (&1 - t2) * &1 + &1 - inv (&1 - t2) = &1`;VECTOR_ARITH`(&1 - inv (&1 - t2)) % y + inv (&1 - t2) % (
t1 % x + t2 % y + t3 % w) =
(inv (&1 - t2) *
t1) % x +
(inv (&1 - t2) * t2 + &1 - inv (&1 - t2)) % y +
(inv (&1 - t2) * t3) % w`;REAL_ARITH`inv (&1 - t2) * t2 + &1 - inv (&1 - t2)= &1 - inv (&1 - t2) *(&1-t2)`;REAL_ARITH`&0<= &1 - &1`]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[]]);;
let point_in_aff_gt_2_1_change_point_in_aff_gt_1_2=prove(` !x:real^3 v:real^3 u:real^3 y:real^3.
~collinear {x,v,u}
/\ y
IN aff_gt {x} {v,u}
==> u
IN aff_gt {x,v} {y}`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN MRESA_TAC
properties_of_collinear4_points_fan[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN REMOVE_THEN "YEU" MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`;]
THEN MRESA_TAC
th3[`x:real^3`;`y:real^3`;`v:real^3`;]
THEN MRESA_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`;]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`y:real^3`;][
IN_ELIM_THM]
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0< t3==> ~(t3= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC
REAL_LT_INV`t3:real`
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
THEN EXISTS_TAC`-- inv t3 * t1:real`
THEN EXISTS_TAC`-- inv t3 * t2:real`
THEN EXISTS_TAC`inv t3 :real`
THEN ASM_REWRITE_TAC[REAL_ARITH`--inv t3 *
t1 + --inv t3 * t2 + inv t3= inv t3 *( t3 + &1- (t1+t2+t3))`;REAL_ARITH`A+ &1- &1 =A`;VECTOR_ARITH`(--inv t3 *
t1) % x +
(--inv t3 * t2) % v +
inv t3 % (
t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u`]
THEN VECTOR_ARITH_TAC);;
let pos_in_aff_gt_fan=prove(`!x:real^3 v:real^3 u:real^3 a:real.
DISJOINT {x} {v,u}
/\ &0<a /\ a< &1
==>
(&1-a)%v + a % u
IN aff_gt {x} {v,u:real^3}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1 -a:real`
THEN EXISTS_TAC`a:real`
THEN MP_TAC(REAL_ARITH`&0< a /\ a < &1 ==> &0 < &1 - a /\ &0 < a`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC);;
let pos_in_aff_gt_2_1_fan=prove(`!x:real^3 v:real^3 u:real^3 a:real.
DISJOINT {x,v} {u}
/\ &0<a /\ a< &1
==>
(&1-a)%v + a % u
IN aff_gt {x,v} {u:real^3}`,
REPEAT STRIP_TAC
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1 -a:real`
THEN EXISTS_TAC`a:real`
THEN MP_TAC(REAL_ARITH`&0< a /\ a < &1 ==> &0 < &1 - a /\ &0 < a`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN REAL_ARITH_TAC);;
(* ========================================================================== *)
(* SEGMENT (^_^) *)
(* ========================================================================== *)
let segment_in_segment=prove(`!x y z:real^N. z
IN segment [x,y]==> (!t. &0<= t /\ t<= &1 ==> (&1-t) %z +t %y
IN segment[x,y])`,
REWRITE_TAC[
segment;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`(&1- t)* u+t:real`
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - t) % ((&1 - u) % x + u % y) + t % y =
(&1 - ((&1 - t) * u + t)) % x + ((&1 - t) * u + t) % y:real^N`]
THEN STRIP_TAC
THENL[MATCH_MP_TAC
REAL_LE_ADD
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1- t<=> t<= &1`];
REWRITE_TAC[REAL_ARITH`(&1 - t) * u + t <= &1<=> &0<= (&1 - t) * (&1-u)`]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1- t<=> t<= &1`]]);;
let segmentsubset_aff_gt=prove(`!x y z w:real^N.
DISJOINT {x} {y,z}/\ w
IN aff_gt {x} {y,z}
==> !t. &0<= t /\ t< &1 ==> (&1-t) %w+t%z
IN aff_gt {x} {y,z}`,
REPEAT GEN_TAC THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^N`;`y:real^N`;`z:real^N`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`(&1-t)*t1:real`
THEN EXISTS_TAC`(&1-t)*t2:real`
THEN EXISTS_TAC`(&1-t)*t3+t:real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - t) % (
t1 % x + t2 % y + t3 % z) + t % z =
((&1 - t) *
t1) % x + ((&1 - t) * t2) % y + ((&1 - t) * t3 + t) % z:real^N`;REAL_ARITH`(&1 - t) *
t1 + (&1 - t) * t2 + (&1 - t) * t3 + t=(&1 - t) * (
t1 + t2 +t3) + t/\ (&1 - t) * &1 + t = &1`]
THEN STRIP_TAC
THENL[MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1- t<=> t< &1`];
MATCH_MP_TAC (REAL_ARITH`&0<A /\ &0<=B==> &0< A+B`)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1- t<=> t< &1`]]);;
(* ========================================================================== *)
(* SOME LINEAR FUNCTIONS (^_^) *)
(* ========================================================================== *)
let linear_inj_fan=prove(`!x:real^3 v:real^3 u:real^3.
~collinear{x,v,u}
==>(!(a:real^2) (b:real^2). (\(t:real^2). t$1 %(v-x)+t$2 %(u-x))(a)=(\(t:real^2). t$1 %(v-x)+t$2 %(u-x))(b) ==>a=b)`,
REPEAT GEN_TAC
THEN DISCH_TAC
THEN ASSUME_TAC(ISPECL[`x:real^3`;` v:real^3`;`u:real^3`]
linear_aff_fan)
THEN MP_TAC(ISPEC`(\(t:real^2). t$1 %(v-x)+t$2 %(u-x):real^3)`
LINEAR_INJECTIVE_0)
THEN RESP_TAC
THEN REMOVE_ASSUM_TAC
THEN GEN_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`(a:real^2)$2= &0 \/ ~(a$2= &0)`)
THENL[
ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
VECTOR_MUL_EQ_0;VECTOR_ARITH`A-B=
vec 0<=> B=A`]
THEN MP_TAC(ISPECL[`x:real^3`;` v:real^3`;`u:real^3`]
th3)
THEN RESA_TAC
THEN ASM_TAC
THEN SIMP_TAC[
LAMBDA_BETA;
CART_EQ; DIMINDEX_2;
FORALL_2;
VEC_COMPONENT; ARITH];
REWRITE_TAC[VECTOR_ARITH`A+B=
vec 0<=>B= --A`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`a$2 % (u - x) = --((a:real^2)$1 % (v - x:real^3)) ==> (inv (a$2)) % a$2 % (u - x) = (inv (a$2)) % (--(a$1 % (v - x)))`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th]
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(A%B%C=(A*B)%C:real^3)`])
THEN MP_TAC(ISPEC`(a:real^2)$2`REAL_MUL_LINV)
THEN RESA_TAC
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[VECTOR_ARITH`A-B=C%(--(D%(U-B)))<=> A= (&1+C*D)%B+(--C*D)%U:real^3`]
THEN MP_TAC(ISPECL[`x:real^3`;` v:real^3`;`u:real^3`]
th3)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN DISCH_THEN(LABEL_TAC"A")
THEN DISCH_TAC
THEN SUBGOAL_THEN `F`ASSUME_TAC
THENL[
REMOVE_THEN "A" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`(&1 + inv ((a:real^2)$2) * a$1)`
THEN EXISTS_TAC`(--inv ((a:real^2)$2) * a$1)`
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
ASM_MESON_TAC[]]]);;
(* ========================================================================== *)
(* AFFINE AND DOT *)
(* ========================================================================== *)
let exp_aff_ge_by_dot=prove(`!x:real^3 v:real^3 u:real^3.
~collinear {x,v,u}
==> aff_ge {x,v} {u}={w:real^3| (w-x)
dot (
e2_fan x v u)= &0 /\ &0 <= (w-x)
dot (
e1_fan x v u) }`,
(
let CROSS_LAGRANGE1 = prove
(`!x y z. (x cross y) cross z = (x dot z) % y - (z dot y) % x`,
VEC3_TAC) in
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN RES_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]AFF_GE_2_1) THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate) THEN RESA_TAC
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
THENL[
STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`(a % x + b +c) -x= (a- &1)% x + b + c `] THEN
REMOVE_ASSUM_TAC THEN SYM_ASSUM_TAC THEN REWRITE_TAC[VECTOR_ARITH`((a-(a+b+c)) % x + b % v +c % u)= b % (v-x) + c % (u-x)`]
THEN ASM_REWRITE_TAC[DOT_LADD;DOT_LMUL]
THEN REDUCE_ARITH_TAC
THEN ASM_MESON_TAC[REAL_LE_MUL] ;
STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
THEN DISCH_THEN(LABEL_TAC"b")
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3)( v:real^3) (u:real^3)`;
`e3_fan (x:real^3) (v:real^3) (u:real^3)`;]ORTHONORMAL_IMP_SPANNING) THEN ASM_REWRITE_TAC[SPAN_3;EXTENSION]
THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(x':real^3)-(x:real^3)`th)) THEN REWRITE_TAC[SET_RULE`(a:real^3) IN (:real^3)`;IN_ELIM_THM] THEN RES_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[DOT_LADD;DOT_LMUL]
THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"c")
THEN FIND_ASSUM(MP_TAC)`orthonormal (e1_fan (x:real^3) (v:real^3) (u:real^3)) (e2_fan x v u) (e3_fan x v u)`
THEN REWRITE_TAC[orthonormal] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC THEN DISCH_THEN (LABEL_TAC"a")
THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[DOT_LADD;DOT_LMUL;] THEN REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
THEN ASM_REWRITE_TAC[e1_fan;e2_fan;CROSS_LMUL;VECTOR_ARITH`a% b% v=(a*b)%v`;CROSS_LAGRANGE1]
THEN REDUCE_VECTOR_TAC THEN REWRITE_TAC[VECTOR_ARITH`a%(x- b % v)+ c % v=(c- a* b) % v+ a % x `;
e3_fan;VECTOR_ARITH`a% b% v=(a*b)%v`]
THEN STRIP_TAC THEN
EXISTS_TAC
`&1 - ((((w:real) -
((u':real) * inv (norm (inv (norm ((v:real^3) - (x:real^3))) % (v - x) cross ((u:real^3) - x)))) *
(inv (norm (v - x)) % (v - x) dot (u - x))) *
inv (norm (v - x)))+
((u':real) * inv (norm (e3_fan (x:real^3) (v:real^3) (u:real^3) cross (u - x)))))`
THEN EXISTS_TAC
`(((w:real) -
((u':real) * inv (norm (inv (norm ((v:real^3) - (x:real^3))) % (v - x) cross ((u:real^3) - x)))) *
(inv (norm (v - x)) % (v - x) dot (u - x))) *
inv (norm (v - x)))`
THEN EXISTS_TAC
` ((u':real) * inv (norm (e3_fan (x:real^3) (v:real^3) (u:real^3) cross (u - x))))`
THEN
STRIP_TAC
THENL[
SUBGOAL_THEN `~(collinear {vec 0, v-x, u-x})==> ~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC
THENL[
MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL]
THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP)
THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ];
POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM COLLINEAR_3]
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{a,b,c}={b,a,c}`] THEN RED_TAC
THEN
MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`] imp_norm_ge_zero_fan)
THEN REDUCE_VECTOR_TAC THEN RES_TAC THEN
MP_TAC(ISPECL[`u':real`;`inv (norm ((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))))`]
REAL_LE_MUL) THEN RES_TAC THEN POP_ASSUM MATCH_MP_TAC THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC];
STRIP_TAC THENL[REAL_ARITH_TAC;
REWRITE_TAC[e3_fan] THEN POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]));;
let exp_aff_ge_by_dot_1_1=prove(`!x:real^3 v:real^3 u:real^3.
~collinear {x,v,u}
==>
aff_ge {x} {v}={w:real^3| (w-x)
dot (
e2_fan x v u)= &0 /\ &0 <= (w-x)
dot (
e3_fan x v u)
/\ (w-x)
dot (
e1_fan x v u)= &0 }`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
th3)
THEN RES_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]
AFF_GE_1_1) THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
properties_coordinate) THEN RESA_TAC
THEN REWRITE_TAC[
EXTENSION;
IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
THENL[
STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`(a % x + b) -x= (a- &1)% x + b `]
THEN
REMOVE_ASSUM_TAC THEN SYM_ASSUM_TAC THEN REWRITE_TAC[VECTOR_ARITH`((a-(a+b)) % x + b % v)= b % (v-x)`]
THEN ASM_REWRITE_TAC[
DOT_LADD;
DOT_LMUL]
THEN REDUCE_ARITH_TAC THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM(
th)])`
dist (v,x) %
e3_fan x v u = v- x:real^3`
THEN REWRITE_TAC[
DOT_LMUL]
THEN FIND_ASSUM(MP_TAC)`
orthonormal (
e1_fan (x:real^3) (v:real^3) (u:real^3)) (
e2_fan x v u) (
e3_fan x v u)`
THEN REWRITE_TAC[
orthonormal] THEN RESA_TAC THEN REDUCE_ARITH_TAC THEN MP_TAC(ISPECL[`v:real^3`;`x:real^3`]
DIST_POS_LE)
THEN MESON_TAC[
REAL_LE_MUL];
STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
THEN DISCH_THEN(LABEL_TAC"b") THEN DISCH_THEN (LABEL_TAC "c")
THEN MP_TAC(ISPECL[`
e1_fan (x:real^3) (v:real^3) (u:real^3)`;`
e2_fan (x:real^3)( v:real^3) (u:real^3)`;
`
e3_fan (x:real^3) (v:real^3) (u:real^3)`;]
ORTHONORMAL_IMP_SPANNING) THEN ASM_REWRITE_TAC[
SPAN_3;
EXTENSION]
THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(x':real^3)-(x:real^3)`
th)) THEN REWRITE_TAC[SET_RULE`(a:real^3)
IN (:real^3)`;
IN_ELIM_THM] THEN RES_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[
DOT_LADD;
DOT_LMUL]
THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"d")
THEN FIND_ASSUM(MP_TAC)`
orthonormal (
e1_fan (x:real^3) (v:real^3) (u:real^3)) (
e2_fan x v u) (
e3_fan x v u)`
THEN REWRITE_TAC[
orthonormal] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[
DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[
DOT_LADD;
DOT_LMUL]
THEN ASM_REWRITE_TAC[
DOT_SYM]
THEN REDUCE_ARITH_TAC THEN DISCH_TAC
THEN DISCH_TAC THEN REMOVE_THEN "d" MP_TAC THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC
THEN DISCH_TAC
THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[
DOT_LADD;
DOT_LMUL;] THEN REWRITE_TAC[
DOT_SYM] THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[
e3_fan;VECTOR_ARITH`a% b% v=(a*b)%v`;
VECTOR_ARITH`a-b=c %(v-b)<=> a= (&1-c) % b + c % v`] THEN DISCH_THEN (LABEL_TAC"a")
THEN STRIP_TAC THEN
EXISTS_TAC
`&1 - (w:real) * (inv (
norm ((v:real^3) - (x:real^3))))`
THEN EXISTS_TAC
`(w:real) * (inv (
norm ((v:real^3) - (x:real^3))))`
THEN
STRIP_TAC
THENL[
MP_TAC(ISPECL[`v:real^3`;`x:real^3`]
imp_norm_ge_zero_fan) THEN RES_TAC THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
STRIP_TAC THENL[REAL_ARITH_TAC;
ASM_REWRITE_TAC[]]]]);;
(****************************************************************************)
(* the conditions to add azim *)
(****************************************************************************)
let sum1_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v /\ (
azim x v u w1 +
azim x v w1 w2) < &2 *
pi
==>
azim x v u w2 =
azim x v u w1+
azim x v w1 w2
`,
(
let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
REPEAT GEN_TAC THEN STRIP_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim)
THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC
THEN
POP_ASSUM (fun th-> MP_TAC (ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `y:real` ] AZIM_UNIQUE)
THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)` ] AZIM_UNIQUE)
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[ ASM_MESON_TAC[REAL_LE_ADD];
ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
]]));;
let sum3_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
((
azim x v u w1 +
azim x v w1 w2) < &2 *
pi)
/\
(~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
==>
azim x v u w2 =
azim x v u w1+
azim x v w1 w2
`,
(
let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
(let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a")
THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b")
THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
THEN USE_THEN "b" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim)
THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC
THEN
POP_ASSUM (fun th-> MP_TAC (ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `y:real` ] AZIM_UNIQUE)
THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)` ] AZIM_UNIQUE)
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[
ASM_MESON_TAC[REAL_LE_ADD];
ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]])));;
let sum2_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
cyclic_set {u, w1, w2} x v /\
azim x v u w1 <=
azim x v u w2
==>
azim x v u w2 =
azim x v u w1 +
azim x v w1 w2
`,
(
let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
REPEAT GEN_TAC THEN STRIP_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim)
THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN REPEAT STRIP_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)` ] AZIM_UNIQUE)
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 )
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]));;
let sum4_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
azim x v u w1 <=
azim x v u w2
/\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
==>
azim x v u w2 =
azim x v u w1 +
azim x v w1 w2
`,
(
let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
(let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in
REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a1")
THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b1")
THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
THEN USE_THEN "b1" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim)
THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`])
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN REPEAT STRIP_TAC
THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)` ] AZIM_UNIQUE)
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 )
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC
)));;
let sum5_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
azim x v w1 w2 <=
azim x v u w2
/\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
/\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
/\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
==>
azim x v u w2 =
azim x v u w1 +
azim x v w1 w2
`,
REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC"1") THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`(
azim x v u w2)= &0 \/ ~(
azim x v u w2 = &0)`)
THENL(*1*)[
SUBGOAL_THEN`
azim x v w1 w2 = &0` ASSUME_TAC
THENL(*2*)[
REPEAT(POP_ASSUM MP_TAC) THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]
azim) THEN REAL_ARITH_TAC;
(*2*)
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]
AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]
AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
SUBGOAL_THEN`
azim x v w2 w1 =
azim x v w2 u` ASSUME_TAC
THENL(*3*)[ASM_MESON_TAC[];(*3*)
REWRITE_TAC[REAL_ARITH`&0 = a + &0 <=> a= &0`] THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w2:real^3`;`u:real^3`;`w1:real^3`]
AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`]
AZIM_EQ_0) THEN ASM_REWRITE_TAC[]]];
DISJ_CASES_TAC(REAL_ARITH`(
azim x v w1 w2)= &0 \/ ~(
azim x v w1 w2 = &0)`)
THENL(*4*)[
ASM_REWRITE_TAC[REAL_ARITH`b = a + &0 <=> b= a`] THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]
AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[]THEN ASM_MESON_TAC[
AZIM_EQ_ALT] ;(*4*)
REMOVE_THEN"1" MP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]
AZIM_COMPL
) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]
AZIM_COMPL
) THEN ASM_REWRITE_TAC[REAL_ARITH`a=b-c <=> c= b-a`] THEN DISCH_TAC THEN DISCH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`a-b=c+a-d<=> d=b+c`;REAL_ARITH`a-b<=a-d<=> d<=b`] THEN ASM_MESON_TAC[
sum4_azim_fan]]
]);;
(* ========================================================================== *)
(* AZIM *)
(* ========================================================================== *)
let th = prove
(`!x:real^3 v:real^3 u:real^3 w:real^3.
~collinear {x,v,u} /\ ~collinear{x,v,w}
==> {y:real^3 | ~collinear {x,v,y} /\
azim x v u w =
azim x v u y} =
aff_gt {x , v} {w}`,
let th1=prove(`(!x:real^3 v:real^3 u:real^3 w:real^3 t1:real t2:real t3:real. (t3 > &0) /\ (
t1 + t2 + t3 = &1)
/\
DISJOINT {x,v} {w} /\ ~collinear {x,v,u}/\ ~collinear {x,v,w}
==>
azim x v u w =
azim x v u (
t1 % x + t2 % v + t3 % w))`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ASSUME_TAC(
AFF_GT_2_1)
THEN POP_ASSUM(MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`w:real^3`])
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ABBREV_TAC `(y:real^3)= (t1:real) % (x:real^3) + (t2:real) % (v:real^3) + (t3:real) % (w:real^3)`
THEN SUBGOAL_THEN `(y:real^3)
IN aff_gt {(x:real^3),(v:real^3)} {w:real^3}` ASSUME_TAC
THENL[
ASM_REWRITE_TAC[
IN_ELIM_THM] THEN EXISTS_TAC `t1:real`
THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real`
THEN EXPAND_TAC "y" THEN ASM_MESON_TAC[REAL_ARITH`(a:real)> &0 <=> &0 < a ` ];
POP_ASSUM MP_TAC THEN
ASSUME_TAC(
th) THEN POP_ASSUM(MP_TAC o ISPECL [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`])
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN REWRITE_TAC[
IN_ELIM_THM] THEN ASM_SET_TAC[]]);;
let th2= prove(`!x:real^3 v:real^3 w:real^3. ~(x=v)==> (w
IN complement_set {x,v}==> ~
collinear {x,v,w})`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[CONTRAPOS_THM;
COLLINEAR_3;
COLLINEAR_LEMMA;
complement_set;
IN_ELIM_THM;
affine_hull_2_fan] THEN STRIP_TAC
THENL[
ASM_MESON_TAC[VECTOR_ARITH`(x-v=
vec 0)<=> (x=v)`];
EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_ARITH`&0+ &1 = &1`; VECTOR_ARITH`&0 % x=
vec 0`; VECTOR_ARITH`w=
vec 0 + &1 % v <=> w - v =
vec 0`] THEN ASM_SET_TAC[];
EXISTS_TAC `c:real` THEN EXISTS_TAC `&1 - (c:real)` THEN REWRITE_TAC[REAL_ARITH`c+ &1 - c = &1`; VECTOR_ARITH`w=c % x + (&1 - c) % v <=> w - v = c % (x-v)`] THEN ASM_SET_TAC[]]);;
(* ========================================================================== *)
(* CARD *)
(* ========================================================================== *)
let CARD_SING=prove(`!x:real^3 s:real^3->bool.
FINITE s
/\ s={x}
==>
CARD s = 1`,
REPEAT STRIP_TAC THEN
MP_TAC(SET_RULE`(s:real^3->bool)={(x:real^3)} ==> ~(s={}) /\ x
IN s /\ s
DELETE x ={}`)
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPEC`s:real^3->bool`
CARD_EQ_0) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ISPECL[`x:real^3`;`s:real^3->bool`]
CARD_DELETE) THEN ASM_REWRITE_TAC[
CARD_CLAUSES]
THEN ARITH_TAC);;
(* ========================================================================== *)
(* CLOSED AFF *)
(* ========================================================================== *)
(*--------------------------------------------------------------------------------------------*)
(* The properties of ballnorm_fan (x:real^3)={y:real^3 | dist(x,y) = &1} *)
(*--------------------------------------------------------------------------------------------*)
(*--------------------------------------------------------------------------------------------*)
(* The properties of fan in norm ball *)
(*--------------------------------------------------------------------------------------------*)
(* ========================================================================== *)
(* RCONE *)
(* ========================================================================== *)
(* rcone^0(x,v,h) *)
let conditions_in_rcone_fan=prove(`!x v u w:real^3 s:real.
~collinear {x,v,u}/\ w
IN aff_gt {x} {v,u} /\ &0<s /\ s< pi/ &2 /\u
IN rcone_fan x v (
cos s)==> w
IN rcone_fan x v (
cos s) `,
REWRITE_TAC[
rcone_fan;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN DISCH_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(u:real^3)`;]
THEN MRESAL_TAC
AFF_GT_1_2[`(x:real^3)` ;` (v:real^3)`;` (u:real^3) `;][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
dist;VECTOR_ARITH`(
t1 % x + t2 % v + t3 % u) - x=((t1+t2+t3)- &1) % x + t2 % (v-x) + t3 % (u-x)`;REAL_ARITH`&1 - &1= &0`;REAL_ARITH`A>B<=> B<A`;
DOT_LADD;
DOT_LMUL]
THEN REDUCE_VECTOR_TAC
THEN REDUCE_ARITH_TAC
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< t3==> &0<= t3`) THEN RESA_TAC
THEN MRESA1_TAC
REAL_ABS_REFL`t3:real`
THEN MRESA_TAC
NORM_MUL[`t3:real`;`u-x:real^3`]
THEN MP_TAC(REAL_ARITH`&0< t2==> &0<= t2`) THEN RESA_TAC
THEN MRESA1_TAC
REAL_ABS_REFL`t2:real`
THEN MRESA_TAC
NORM_MUL[`t2:real`;`v-x:real^3`]
THEN MRESA_TAC
REAL_LT_LMUL[`t3:real`;`
norm (u - x) *
norm (v - x:real^3) * (
cos s):real`;`(u - x)
dot (v - x:real^3)`]
THEN MRESA1_TAC
COS_BOUNDS`s:real`
THEN MRESA1_TAC
DOT_POS_LE`(v - x):real^3`
THEN MRESA_TAC
REAL_LE_MUL[`t2:real`;`(v-x)
dot (v-x:real^3)`;]
THEN MRESA_TAC
REAL_LE_LMUL[`t2*((v - x:real^3)
dot (v-x)):real`;`
cos s:real`;`&1`]
THEN POP_ASSUM MP_TAC THEN REDUCE_ARITH_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
DOT_SQUARE_NORM;]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH` t3 *
norm (u - x) *
norm (v - x) *
cos s< t3 * ((u - x)
dot (v - x))
/\(t2 *
norm (v - x) pow 2) *
cos s <= t2 * ((v - x)
dot (v - x))
==> (t2 *
norm (v - x:real^3) + t3 *
norm (u - x)) *
norm (v - x) *
cos s< t2 * ((v - x)
dot (v - x))+ t3 * ((u - x)
dot (v - x))`)
THEN RESA_TAC
THEN MRESA_TAC
NORM_TRIANGLE[`t2 %(v - x:real^3)`;`t3 % (u - x:real^3)`]
THEN MRESA1_TAC
NORM_POS_LE`(v - x):real^3`
THEN MRESA1_TAC
COS_POS_PI2`(s):real`
THEN MP_TAC(REAL_ARITH`&0<
cos s:real ==> &0<=
cos s`) THEN RESA_TAC
THEN MRESA_TAC
REAL_LE_MUL[`
norm (v-x:real^3)`;`
cos s:real`]
THEN MRESA_TAC
REAL_LE_RMUL[`
norm (t2 % (v - x) + t3 % (u - x):real^3):real`;`t2 *
norm (v - x:real^3) + t3 *
norm (u - x)`;`
norm (v - x:real^3) *
cos s`]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC);;
let not_empty_rcone_fan_inter_aff_gt=prove(`!x v u:real^3 h:real.
~collinear {x,v,u} /\ &0< h /\ h<=
pi==>
~(
rcone_fan x v (
cos h)
INTER aff_gt {x} {v, u}={})`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`~(
norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL(*1*)[ASM_REWRITE_TAC[
NORM_EQ_0;VECTOR_ARITH`v-x=
vec 0<=> x=v`];
ASM_REWRITE_TAC[
rcone_fan;SET_RULE`~(A={})<=> ?y. y
IN A`;
INTER;
IN_ELIM_THM]
THEN DISJ_CASES_TAC(REAL_ARITH`(v - x)
dot (u - x:real^3) <= &0 \/ &0< (v - x)
dot (u - x)`)
THENL(*2*)[ABBREV_TAC`s1= min h (
pi / &2) / &2:real`
THEN MP_TAC(REAL_ARITH` &0<
pi /\ min h (
pi / &2) / &2 =s1 /\ &0< h:real ==> &0<= s1 /\ &0<s1 /\ s1< h/\ s1<pi/ &2`)
THEN ASM_REWRITE_TAC[
PI_WORKS]
THEN STRIP_TAC
THEN EXISTS_TAC`
sin (s1) % (
e1_fan x v u) + (
cos s1) %(
e3_fan x v u)+x :real^3 `
THEN REWRITE_TAC[
dist;
vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`;
DOT_LADD;
DOT_RADD;
DOT_RMUL;
DOT_LMUL;]
THEN MRESAL_TAC
properties_coordinate[`x:real^3`;`v:real^3`;`u:real^3`][
orthonormal]
THEN ONCE_REWRITE_TAC[
DOT_SYM]
THEN ASSUME_TAC(ISPEC`s1:real`
SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`
sin s *
sin s +
cos s *
cos s =(
sin s) pow 2 + (
cos s) pow 2`;
e3_fan;
DOT_RMUL; ]
THEN ONCE_REWRITE_TAC[GSYM
vector_norm;]
THEN REWRITE_TAC[
DOT_SQUARE_NORM;]
THEN MRESAL1_TAC
SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th); REAL_ARITH`&1* &1= &1`])
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN ASSUME_TAC(ISPEC`v-x:real^3`
NORM_POS_LE)
THEN STRIP_TAC
THENL(*3*)[ MATCH_MP_TAC
REAL_LT_LMUL
THEN MP_TAC(REAL_ARITH`~(
norm (v - x:real^3) = &0)/\ &0 <=
norm (v - x)==> &0<
norm (v - x) `)
THEN RESA_TAC
THEN MATCH_MP_TAC
COS_MONO_LT
THEN ASM_REWRITE_TAC[];(*3*)
MRESA_TAC
condition1_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`u:real^3`;`s1:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
e3_fan]](*3*);(*2*)
SUBGOAL_THEN`&0<(
atn ((
norm ((v - x)
cross (u - x))) * inv((v - x)
dot (u - x:real^3))))` ASSUME_TAC
THENL(*3*)[MP_TAC(ISPEC`(v - x)
dot (u - x:real^3)`
REAL_LT_INV)
THEN RESA_TAC
THEN ASSUME_TAC(
PI_WORKS)
THEN MP_TAC(REAL_ARITH`&0<
pi ==> --(
pi / &2) < &0`)
THEN RESA_TAC
THEN MRESAL_TAC
ATN_MONO_LT[`&0:real`;` (
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x))):real`][
ATN_0]
THEN POP_ASSUM MATCH_MP_TAC
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~(
norm((v - x)
cross (u - x:real^3))= &0)` ASSUME_TAC
THENL(*4*)[
ASM_REWRITE_TAC[
NORM_EQ_0]
THEN MP_TAC(ISPECL[`v-x:real^3`;`u-x:real^3`]
CROSS_EQ_0)
THEN ONCE_REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ASM_REWRITE_TAC[];(*4*)
POP_ASSUM MP_TAC
THEN MP_TAC(ISPEC`(v - x)
cross (u - x:real^3)`
NORM_POS_LE)
THEN REAL_ARITH_TAC](*4*);(*3*)
ASSUME_TAC(ISPEC`(
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x))):real`
ATN_BOUNDS)
THEN ABBREV_TAC`s2=
atn ((
norm ((v - x)
cross (u - x))) * inv((v - x)
dot (u - x))):real`
THEN ABBREV_TAC`s1= min (h:real) (s2:real) / &2`
THEN MP_TAC(REAL_ARITH`&0< h /\ s1= min (h:real) (s2) / &2 /\ &0<
pi /\ &0< s2 /\ s2 < pi/ &2==> &0<= s1 /\ &0<s1 /\ s1<pi/ &2 /\ s1<h/\ s1< s2
`)
THEN REWRITE_TAC[
PI_WORKS]
THEN RESA_TAC
THEN EXISTS_TAC`
sin (s1) % (
e1_fan x v u) + (
cos s1) %(
e3_fan x v u)+x :real^3 `
THEN REWRITE_TAC[
dist;
vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`;
DOT_LADD;
DOT_RADD;
DOT_RMUL;
DOT_LMUL;]
THEN MRESAL_TAC
properties_coordinate[`x:real^3`;`v:real^3`;`u:real^3`][
orthonormal]
THEN ONCE_REWRITE_TAC[
DOT_SYM]
THEN ASSUME_TAC(ISPEC`s1:real`
SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`
sin s *
sin s +
cos s *
cos s =(
sin s) pow 2 + (
cos s) pow 2`;
e3_fan;
DOT_RMUL; ]
THEN ONCE_REWRITE_TAC[GSYM
vector_norm;]
THEN REWRITE_TAC[
DOT_SQUARE_NORM;]
THEN MRESAL1_TAC
SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th); REAL_ARITH`&1* &1= &1`])
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN ASSUME_TAC(ISPEC`v-x:real^3`
NORM_POS_LE)
THEN STRIP_TAC
THENL(*4*)[ MATCH_MP_TAC
REAL_LT_LMUL
THEN MP_TAC(REAL_ARITH`~(
norm (v - x:real^3) = &0)/\ &0 <=
norm (v - x)==> &0<
norm (v - x) `)
THEN RESA_TAC
THEN MATCH_MP_TAC
COS_MONO_LT
THEN ASM_REWRITE_TAC[];(*4*)
MRESA_TAC
condition_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`u:real^3`;`s1:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
e3_fan]]]]]);;
(* ========================================================================== *)
(* TOPOLOGY COMPONENT YFAN *)
(* ========================================================================== *)
(* ========================================================================== *)
(* BASIC PROPERTIES OF CONVEX *)
(* ========================================================================== *)
let expansion_convex_fan=prove(`!(v:real^3) (u:real^3) (w:real^3) (t:real) s:real.
&0 <= t /\ t<= &1
/\ &0 <=s /\ s <= &1
==> (&1-s)%v+s%((&1-t)%u+ t%w)
IN convex hull{v,u,w}`,
REWRITE_TAC[REAL_ARITH`A<= &1 <=> &0<= &1 -A`]
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[
CONVEX_HULL_3;
IN_ELIM_THM;]
THEN EXISTS_TAC`&1 - (s:real)`
THEN EXISTS_TAC`(s:real)*(&1 - (t:real))`
THEN EXISTS_TAC`(s:real)*(t:real)`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`s%((&1-t)%u+ t%w)= (s*(&1-t))%u+ (s*t)%w:real^3`]
THEN STRIP_TAC
THENL[MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC
THENL[MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_TAC
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]]);;
let expansion1_convex_fan=prove(`!(v:real^3) (u:real^3) s:real.
&0 <=s /\ s <= &1
==> (&1-s)%v+s%u
IN convex hull{v,u}`,
REPEAT STRIP_TAC
THEN MP_TAC(ISPECL[`(v:real^3)`;` (u:real^3)`;` (u:real^3)`;` &0`;`s:real`]
expansion_convex_fan)
THEN ASM_REWRITE_TAC[SET_RULE`{A,B,B}={A,B}`]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN REAL_ARITH_TAC);;
(* ========================================================================== *)
(* CROSS_DOT (^_^) *)
(* ========================================================================== *)
let cross_dot_fully_surrounded_fan=prove(`!x:real^3 v1:real^3 u1:real^3 v:real^3.
~collinear{x,v1,u1}
/\ ~collinear{x,v1,v}
/\ &0<
azim x v1 v u1
/\
azim x v1 v u1 <
pi
==> &0 < ((v1 - x)
cross (v - x))
dot (u1 - x)`,
REPEAT STRIP_TAC
THEN MRESA1_TAC
SIN_POS_PI`
azim x v1 v (u1:real^3)`
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_TRANSLATION[`-- x:real^3`;`x:real^3`;`v1:real^3`;` v:real^3`;`u1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`x-x=
vec 0`;VECTOR_ARITH`(-- X)+A= A-X:real^3`]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN MRESA_TAC
JBDNJJB[`(v1-x):real^3`;`v-x:real^3`;`u1-x:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN RESA_TAC
THEN MRESAL_TAC
REAL_LT_LMUL_EQ [` &0:real `;`(((v1 - x)
cross (v - x))
dot ((u1 - x):real^3)):real`;`t:real`][REAL_ARITH`a * &0 = &0`]);;
let cross_dot_fully_surrounded_ge_fan=prove(`!x:real^3 v1:real^3 u1:real^3 v:real^3.
~collinear{x,v1,u1}
/\ ~collinear{x,v1,v}
/\ &0<=
azim x v1 v u1
/\
azim x v1 v u1 <=
pi
==> &0 <= ((v1 - x)
cross (v - x))
dot (u1 - x)`,
REPEAT STRIP_TAC
THEN MRESA1_TAC
SIN_POS_PI_LE`
azim x v1 v (u1:real^3)`
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_TRANSLATION[`-- x:real^3`;`x:real^3`;`v1:real^3`;` v:real^3`;`u1:real^3`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`x-x=
vec 0`;VECTOR_ARITH`(-- X)+A= A-X:real^3`]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN MRESA_TAC
JBDNJJB[`(v1-x):real^3`;`v-x:real^3`;`u1-x:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN RESA_TAC
THEN MRESAL_TAC
REAL_LE_LMUL_EQ [` &0:real `;`(((v1 - x)
cross (v - x))
dot ((u1 - x):real^3)):real`;`t:real`][REAL_ARITH`a * &0 = &0`]);;
let cut_inside_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 w1:real^3.
~collinear {x,v,w1} /\ ~collinear {x,u,w} /\ ~collinear {x,v,u}
/\ ~collinear {x,v,w}
/\ &0<
azim x u w v /\
azim x u w v <
pi
/\ &0<
azim x v u w1 /\
azim x v u w1 <
pi
/\ &0<
azim x v w1 w /\
azim x v w1 w <
pi
==> ~(aff_ge {x,v} {w1}
INTER aff_gt {x} {u,w:real^3}={})`,
REWRITE_TAC[SET_RULE`~(A={})<=> ?x. x
IN A`;
IN_ELIM_THM;
INTER]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`u:real^3`;`w:real^3`]
THEN MRESAL_TAC
AFF_GE_2_1[`x:real^3`;`v:real^3`;`w1:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`u:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"CON")
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`w1:real^3`;`u:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"CON BE")
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"CON EM")
THEN ABBREV_TAC`a1=(v-x):real^3`
THEN ABBREV_TAC`a2=(w1-x):real^3`
THEN ABBREV_TAC`a3=(w-x) :real^3`
THEN ABBREV_TAC`a4=(u-x):real^3`
THEN ABBREV_TAC`va=a1
cross a2:real^3`
THEN ABBREV_TAC`vb=a3
cross a4:real^3`
THEN EXISTS_TAC`(vb:real^3)
cross (va:real^3)+(x:real^3)`
THEN STRIP_TAC
THENL(*2*)[
EXISTS_TAC`&1-(vb:real^3)
dot (a2:real^3)+ vb
dot (a1:real^3)`
THEN EXISTS_TAC`(vb:real^3)
dot (a2:real^3)`
THEN EXISTS_TAC`--((vb:real^3)
dot (a1:real^3))`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - vb
dot a2 + vb
dot a1) + vb
dot a2 + --(vb
dot a1) = &1`]
THEN SUBGOAL_THEN `&0<= --((vb:real^3)
dot (a1:real^3))` ASSUME_TAC
THENL(*3*)[
EXPAND_TAC"vb"
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN REWRITE_TAC[
DOT_LNEG]
THEN REMOVE_THEN "CON"MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[
CROSS_LAGRANGE;
VECTOR_MUL_LNEG]
THEN EXPAND_TAC"a1"
THEN EXPAND_TAC"a2"
THEN VECTOR_ARITH_TAC];(*2*)
ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN EXPAND_TAC"vb"
THEN REWRITE_TAC[
CROSS_LAGRANGE;]
THEN EXISTS_TAC`&1+(va:real^3)
dot (a4:real^3)- va
dot (a3:real^3)`
THEN EXISTS_TAC`((va:real^3)
dot (a3:real^3))`
THEN EXISTS_TAC`--(va:real^3)
dot (a4:real^3)`
THEN ASM_REWRITE_TAC[
DOT_LNEG;
VECTOR_MUL_LNEG;REAL_ARITH`(&1 + va
dot a4 - va
dot a3) + va
dot a3 + --(va
dot a4) = &1`;]
THEN STRIP_TAC
THENL(*3*)[
EXPAND_TAC"va"
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN REWRITE_TAC[
DOT_LNEG;
CROSS_TRIPLE]
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REAL_ARITH_TAC;
EXPAND_TAC"a3"
THEN EXPAND_TAC"a4"
THEN REWRITE_TAC[VECTOR_ARITH`(&1+A-B)%X+B%U+ --(A%V)=X-(A%(V-X)-B%(U-X))`]
THEN VECTOR_ARITH_TAC]]);;
let exists_cut_in_edge_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 w1:real^3.
~collinear {x,v,w1} /\ ~collinear {x,u,w} /\ ~collinear {x,v,u}
/\ ~collinear {x,v,w}
/\ &0<
azim x u w v /\
azim x u w v <
pi
/\ &0<
azim x v u w1 /\
azim x v u w1 <
pi
/\ &0<
azim x v w1 w /\
azim x v w1 w <
pi
==> ?a. &0< a /\ a< &1
/\ (&1-a) %u + a % w
IN aff_ge {x,v} {w1:real^3}`,
REPEAT STRIP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`u:real^3`;`w:real^3`]
THEN MRESAL_TAC
AFF_GE_2_1[`x:real^3`;`v:real^3`;`w1:real^3`][
IN_ELIM_THM]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`u:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN MRESA_TAC
cut_inside_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?x. x
IN A`;
INTER;]
THEN REWRITE_TAC[
IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`inv(&1-t1')*t3'`
THEN MP_TAC(REAL_ARITH`&0< t2' /\ &0< t3' /\ t1'+t2'+t3'= &1==> &0 < &1- t1' /\ ~(&1- t1' = &0)/\ t2'+t3'= &1- t1'`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ISPEC`&1- (t1':real)`
REAL_LT_INV)
THEN RESA_TAC
THEN MP_TAC(ISPEC`&1- (t1':real)`REAL_MUL_LINV)
THEN RESA_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`
t2' + t3' = &1 - t1':real
==> (inv ( &1 - t1'))*(t2' + t3') = (inv ( &1 - t1'))*( &1 - t1':real)
`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[REAL_ARITH`A*(B+C)= &1<=> &1 -A*C=A*B`;REAL_ARITH`A< &1 <=> &0< &1-A`]
THEN STRIP_TAC
THEN MRESA_TAC
REAL_LT_MUL[`inv (&1- t1'):real`;`t2':real`;]
THEN MRESA_TAC
REAL_LT_MUL[`inv (&1- t1'):real`;`t3':real`;]
THEN REWRITE_TAC[VECTOR_ARITH`(A*B)%X+(A*C)%Y=A%(B%X+C%Y)`; VECTOR_ARITH`A%(t2' % u + t3' % w)= A%((t1'%x +t2' % u + t3' % w) - t1' %x) :real^3`]
THEN FIND_ASSUM MP_TAC`x' = t1' % x + t2' % u + t3' % w:real^3`
THEN DISCH_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(
th)])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(
t1 % x + t2 % v + t3 % w1) - t1' % x=(t1-t1') % x + t2 % v + t3 % w1`;
VECTOR_ARITH`A%(B+C+D)=A%B+A%C+A%D`;VECTOR_ARITH`A%B%C=(A*B)%C`]
THEN EXISTS_TAC`(inv (&1 - t1') * (
t1 - t1')):real`
THEN EXISTS_TAC`(inv (&1 - t1') * t2):real`
THEN EXISTS_TAC`(inv (&1 - t1') * t3):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1 - t1') * (
t1 - t1') + inv (&1 - t1') * t2 + inv (&1 - t1') * t3
=inv (&1 - t1') * ((
t1 +t2 + t3)-t1')`]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN REAL_ARITH_TAC);;
let properties_of_fully_surrounded1_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 w1:real^3.
~coplanar {x,v,u,w}/\ &0<
azim x u w v /\
azim x u w v <
pi
==> &0 <
azim x v u w /\
azim x v u w <
pi`,
REPEAT STRIP_TAC
THEN MRESA_TAC
azim[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(w:real^3)`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THENL[
MP_TAC(REAL_ARITH` &0<=
azim x v u (w:real^3) ==>
azim x v u w = &0 \/ &0<
azim x v u w`)
THEN RESA_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_IMP_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];
MP_TAC(REAL_ARITH` (
azim x v u w =
pi) \/ (
pi <
azim x v u w) \/
azim x v u w<
pi`)
THEN RESA_TAC
THENL[
MRESA_TAC
AZIM_EQ_0_PI_IMP_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];
MP_TAC(REAL_ARITH`pi<
azim x v u w /\
azim x v u w < &2 *
pi ==> &0<
azim x v u w -
pi /\
azim x v u w - pi<
pi`)
THEN RESA_TAC
THEN MRESAL1_TAC
SIN_POS_PI`
azim x v u (w:real^3) -pi`[
SIN_SUB;
SIN_PI;
COS_PI;REAL_ARITH`&0< A * -- &1 -B * &0 <=> A < &0`]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_TRANSLATION[`-- x:real^3`;`x:real^3`;`v:real^3`;` u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`x-x=
vec 0`;VECTOR_ARITH`(-- X)+A= A-X:real^3`]
THEN DISCH_TAC
THEN MRESA_TAC
JBDNJJB[`(v-x):real^3`;`u-x:real^3`;`w-x:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESAL_TAC
REAL_LT_LMUL_EQ[`(((v - x)
cross (u - x))
dot (w - x:real^3))`;`&0`;`t:real`][REAL_ARITH`A * &0= &0`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
DOT_LNEG;
CROSS_TRIPLE]
THEN MRESA1_TAC
SIN_POS_PI`
azim x u (w:real^3) v`
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_TRANSLATION[`-- x:real^3`;`x:real^3`;`u:real^3`;` w:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`x-x=
vec 0`;VECTOR_ARITH`(-- X)+A= A-X:real^3`]
THEN DISCH_TAC
THEN MRESA_TAC
JBDNJJB[`(u-x):real^3`;`w-x:real^3`;`v-x:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESAL_TAC
REAL_LT_LMUL_EQ[`&0`;`(((u - x)
cross (w - x))
dot (v - x:real^3))`;`t':real`][REAL_ARITH`A * &0= &0`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]])
;;
let inequality4_aim_in_convex_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 a:real.
~coplanar {x,v,u,w}/\ &0<
azim x u w v /\
azim x u w v <
pi
/\ &0< a /\ a < &1
==>
&0<
azim x v u ((&1 - a) % u + a % w)
/\
azim x v u ((&1 - a) % u + a % w)<
azim x v u w `,
REPEAT STRIP_TAC
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC
properties_of_fully_surrounded1_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN MRESA_TAC
WEDGE_LUNE_GT[`x:real^3`;` v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM (fun th-> MP_TAC(SYM(
th)))
THEN DISCH_TAC
THEN MRESA_TAC
in_aff_2_2_fan[`x:real^3`;` v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM(fun th-> MRESA1_TAC
th `a:real`)
THEN POP_ASSUM(fun th-> MRESAL_TAC
th [`&0:real`;`&0`;`&1`][REAL_ARITH`&0< &1/\ &0+ &0 + &1 = &1`;
wedge;
IN_ELIM_THM])
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REDUCE_VECTOR_TAC
THEN DISCH_TAC THEN DISCH_TAC
THEN ASM_REWRITE_TAC[]);;
let cut_in_angle_fan=prove(`!x:real^3 v:real^3 u:real^3 w:real^3 y:real^3.
~coplanar {x,v,u,w} /\ ~collinear {x,u,y}
/\ &0<
azim x u w v /\
azim x u w v<
pi
/\
azim x u w y<
azim x u w v /\ &0<
azim x u w y
==> let a1=(v-x):real^3 in
let a2=w-x:real^3 in
let a3=(y-x):real^3 in
let a4=(u-x) :real^3 in
let va=a1
cross a2:real^3 in
let vb=a3
cross a4:real^3 in
let v3= (vb:real^3)
cross (va:real^3)+(x:real^3)
in v3
IN aff_gt {x} {v,w:real^3}`,
REPEAT STRIP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ABBREV_TAC`a1=(v-x):real^3`
THEN ABBREV_TAC`a2=(y-x):real^3`
THEN ABBREV_TAC`a3=(u-x) :real^3`
THEN ABBREV_TAC`a4=w-x:real^3`
THEN ABBREV_TAC`va=a1
cross a4:real^3`
THEN ABBREV_TAC`vb=a2
cross a3:real^3`
THEN ABBREV_TAC`v3= (vb:real^3)
cross (va:real^3)+(x:real^3)`
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(w:real^3) `;]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&1-(vb:real^3)
dot (a4:real^3)+vb
dot (a1:real^3)`
THEN EXISTS_TAC`((vb:real^3)
dot (a4:real^3))`
THEN EXISTS_TAC`(--((vb:real^3)
dot (a1:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - vb
dot a4 + vb
dot a1) + (vb
dot a4) + --(vb
dot a1) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`]
THEN MP_TAC(REAL_ARITH`
azim x u w v<
pi
/\
azim x u w y<
azim x u w v==>
azim x u w (y:real^3)<
pi`)
THEN RESA_TAC
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE;] THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN ASM_REWRITE_TAC[
DOT_LNEG;REAL_ARITH`--(--A)=A`]
THEN DISCH_TAC
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v==>
azim x u w y<=
azim x u w (v:real^3)`)
THEN RESA_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v/\ &0<
azim x u w y/\
azim x u w v <
pi /\
azim x u w v =
azim x u w y +
azim x u y v==> ~(
azim x u y (v:real^3)= &0)/\ &0<
azim x u y v/\
azim x u y v < pi/\ ~(
azim x u y (v:real^3)=
pi)`)
THEN RESA_TAC
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN ASM_REWRITE_TAC[
DOT_LNEG] );;
(* ========================================================================== *)
(* GRAPH (^_^) *)
(* ========================================================================== *)
let CARD_2_FAN=prove(`!v:A w:A. ~(v=w)
==>
CARD {v,w}=2`,
REPEAT STRIP_TAC
THEN SUBGOAL_THEN`FINITE {v,w:A}`ASSUME_TAC
THENL[ SIMP_TAC[
HAS_SIZE;
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY;
IN_INSERT;
NOT_IN_EMPTY];
ASSUME_TAC(SET_RULE `v:A
IN {v:A,w:A} `)
THEN MP_TAC(ISPECL[`v:A`;`{v:A,w:A}`;]
CARD_DELETE)
THEN RESA_TAC
THEN MP_TAC(SET_RULE `v
IN {v,w}==>{v:A,w:A}
DELETE v
PSUBSET {v,w}`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`{v:A,w:A}
DELETE v`;`{v:A,w:A}`]
CARD_PSUBSET)
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN FIND_ASSUM MP_TAC`FINITE {v:A,w:A}`
THEN DISCH_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN DISCH_TAC
THEN MP_TAC(ARITH_RULE`
CARD ({v, w}
DELETE v) <
CARD {v, w}/\
CARD ({v, w}
DELETE v) =
CARD {v, w}-1
<=>
CARD ({v, w}
DELETE v) +1=
CARD {v:A, w:A}`)
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th;])
THEN REWRITE_TAC[ARITH_RULE`A=A`]
THEN DISCH_TAC
THEN SUBGOAL_THEN `w:A
IN ({v:A,w:A}
DELETE v)` ASSUME_TAC
THENL[
ASM_SET_TAC[];
MP_TAC(ISPECL[`{v:A,w:A}`;`v:A`]
FINITE_DELETE)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`w:A`;`{v:A,w:A}
DELETE v`;]
CARD_DELETE)
THEN RESA_TAC
THEN MP_TAC(SET_RULE `w
IN ({v,w}
DELETE v)==>{v:A,w:A}
DELETE v
DELETE w
PSUBSET {v,w}
DELETE v`)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`{v:A,w:A}
DELETE v
DELETE w`;`{v:A,w:A}
DELETE v`]
CARD_PSUBSET)
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN FIND_ASSUM MP_TAC`FINITE ({v:A,w:A}
DELETE v)`
THEN DISCH_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN DISCH_TAC
THEN MP_TAC(ARITH_RULE`
CARD ({v, w}
DELETE v
DELETE w) <
CARD ({v, w}
DELETE v)/\
CARD ({v, w}
DELETE v
DELETE w) =
CARD ({v, w}
DELETE v)-1
<=>
CARD ({v, w}
DELETE v
DELETE w) +1=
CARD ({v:A, w:A}
DELETE v)`)
THEN POP_ASSUM (fun th->REWRITE_TAC[
th])
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th;])
THEN REWRITE_TAC[ARITH_RULE`A=A`]
THEN DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[])
THEN POP_ASSUM (fun th->REWRITE_TAC[])
THEN ASSUME_TAC(SET_RULE `{v, w}
DELETE v:A
DELETE w:A={}`)
THEN POP_ASSUM (fun th->REWRITE_TAC[
th;
CARD_CLAUSES; ARITH_RULE `0+1=1`])
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"B")
THEN DISCH_TAC
THEN REMOVE_THEN "B" MP_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(
th);ARITH_RULE` 1+1=2`])
THEN SET_TAC[]]]);;
(* ========================================================================== *)
(* CONDITION OF CROSS DOT 4 POINT (^_^) *)
(* ========================================================================== *)
let condition_cross_dot_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
let va = a1
cross a2 in
let vb = a3
cross a4 in
let v3 = va
cross vb + x in
~collinear {x,v,u}
/\ &0<(a1
cross a2)
dot a4 /\ &0 < --((a1
cross a2)
dot a3)
==> v3
IN aff_gt {x} {v,u}`,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ABBREV_TAC`a1=(y-x):real^3`
THEN ABBREV_TAC`a2=(z-x):real^3`
THEN ABBREV_TAC`a3=(v-x) :real^3`
THEN ABBREV_TAC`a4=u-x:real^3`
THEN ABBREV_TAC`va=a1
cross a2:real^3`
THEN ABBREV_TAC`vb=a3
cross a4:real^3`
THEN ABBREV_TAC`v3= (va:real^3)
cross (vb:real^3)+(x:real^3)`
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(u:real^3) `;]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&1-(va:real^3)
dot (a4:real^3)+va
dot (a3:real^3)`
THEN EXISTS_TAC`((va:real^3)
dot (a4:real^3))`
THEN EXISTS_TAC`(--((va:real^3)
dot (a3:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH` (&1 - va
dot a4 + va
dot a3) + (va
dot a4) + --(va
dot a3) = &1`]
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"vb"
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`A+ B + --U%C=A +B-U%C:real^3`]
THEN EXPAND_TAC"a3"
THEN EXPAND_TAC"a4"
THEN VECTOR_ARITH_TAC);;
let aff_gt_2_1_crossr_dot_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,y,z}
/\ u
IN aff_gt {x,y} {z}
/\ &0<(a1
cross a2)
dot a3
==> &0<(a1
cross a4)
dot a3 `,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`y:real^3`;`z:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`y:real^3`;`z:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % y + w % z) - x=((u'+v'+w) - &1) % x + v' % (y-x) + w % (z - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
CROSS_RMUL;
CROSS_RADD;
CROSS_REFL;]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
DOT_LMUL]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]);;
let aff_gt_2_1_rcross_dot_4pointl=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,y,z}
/\ u
IN aff_gt {x,z} {y}
/\ &0<(a1
cross a2)
dot a3
==> &0<(a4
cross a2)
dot a3 `,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`z:real^3`;`y:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`z:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % z + w % y) - x=((u'+v'+w) - &1) % x + v' % (z-x) + w % (y - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
CROSS_LMUL;
CROSS_LADD;
CROSS_REFL;]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
DOT_LMUL]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]);;
let aff_gt_2_1_cross_dotr_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,y,v}
/\ u
IN aff_gt {x,y} {v}
/\ &0<(a1
cross a2)
dot a3
==> &0<(a1
cross a2)
dot a4 `,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`y:real^3`;`v:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`y:real^3`;`v:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % z + w % y) - x=((u'+v'+w) - &1) % x + v' % (z-x) + w % (y - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
DOT_RMUL;
DOT_RADD;
DOT_CROSS_SELF]
THEN REDUCE_ARITH_TAC
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]);;
let aff_gt_2_1_cross_dotl_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,z,v}
/\ u
IN aff_gt {x,z} {v}
/\ &0<(a1
cross a2)
dot a3
==> &0<(a1
cross a2)
dot a4 `,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`z:real^3`;`v:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`z:real^3`;`v:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % z + w % y) - x=((u'+v'+w) - &1) % x + v' % (z-x) + w % (y - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
DOT_RMUL;
DOT_RADD;
DOT_CROSS_SELF]
THEN REDUCE_ARITH_TAC
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]);;
let aff_gt_2_1r_rcross_dotl_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,v,y}
/\ u
IN aff_gt {x,v} {y}
/\ &0<(a1
cross a2)
dot a3
==> &0<(a4
cross a2)
dot a3 `,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`y:real^3`]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % z + w % y) - x=((u'+v'+w) - &1) % x + v' % (z-x) + w % (y - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
CROSS_LMUL;
CROSS_LADD;
DOT_LMUL;
DOT_LADD;
DOT_CROSS_SELF]
THEN REDUCE_ARITH_TAC
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]);;
let aff_gt_1_2_cross_dotr_4point=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
~collinear {x,v,u}
/\ y
IN aff_gt {x} {v,u}
/\ &0<(a1
cross a2)
dot a3
==> &0< --((a1
cross a2)
dot a4)`,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`u:real^3`]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][
IN_ELIM_THM]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(u' % x + v' % z + w % y) - x=((u'+v'+w) - &1) % x + v' % (z-x) + w % (y - x)`;REAL_ARITH`&1- &1= &0`]
THEN REDUCE_VECTOR_TAC
THEN REWRITE_TAC[
CROSS_LNEG;
CROSS_LMUL;
CROSS_LADD;
CROSS_REFL;
DOT_LMUL;
DOT_LADD;]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;
CROSS_TRIPLE]
THEN REWRITE_TAC[
CROSS_TRIPLE;
CROSS_REFL;
DOT_LZERO]
THEN REDUCE_ARITH_TAC
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_SKEW;]
THEN REWRITE_TAC[
DOT_LNEG;REAL_ARITH`--(A* (--B))=A*B`]
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE;]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC
REAL_LT_RCANCEL_IMP[`&0`;`((u - x)
cross (z - x))
dot (v - x:real^3)`;`t3:real`;][REAL_ARITH`&0 * A= &0`]
THEN POP_ASSUM MATCH_MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC);;
let exists_esilon_real=prove(`!a:real b:real.
&0<a ==> ?t. &0< t /\ t< &1 /\
(!h. &0< h /\ h< t==> &0< a- h * b)`,
REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(REAL_ARITH`b <= &0 \/ &0< b`)
THENL[ EXISTS_TAC`&1/ &2`
THEN REWRITE_TAC[REAL_ARITH`&0< &1/ &2 /\ &1/ &2< &1`;]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC(REAL_ARITH`&0<a /\ &0<= h*(-- b)==> &0< a-h*b`)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= --B<=> B<= &0`]
THEN ASM_TAC THEN REAL_ARITH_TAC;
ABBREV_TAC`
t1= (min (inv (b:real) * a) (&1)) / &2`
THEN MRESA1_TAC
REAL_LT_INV`b:real`
THEN MRESA_TAC
REAL_LT_MUL[`inv b:real`;`a:real`]
THEN MP_TAC(REAL_ARITH`&0 < inv b * a /\
t1= (min (inv (b:real) * a) (&1)) / &2
==> &0<
t1 /\ t1< &1 /\ t1< inv b * a`)
THEN RESA_TAC
THEN EXISTS_TAC `t1:real`
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`h<
t1 /\ t1< inv b *a==> &0< inv b *a- h`)
THEN RESA_TAC
THEN MRESA_TAC
REAL_LT_MUL[`b:real`;`inv b *a- h:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`b * (inv b * a - h)= (inv b * b) * a- h *b `]
THEN MP_TAC(REAL_ARITH`&0<b==> ~(b= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`b:real`
THEN REAL_ARITH_TAC]);;
let invariant_cross_dotr_esilon_3piont=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
&0<(a1
cross a2)
dot a3
==>
?t. &0< t /\ t< &1 /\
(!h. &0< h /\ h< t==>
&0< ((a1
cross a2)
dot ((&1 - h) % v + h % u-x)))`,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - h) % v + h % u-x=(&1 - h) % (v-x) + h % (u-x)`;]
THEN REWRITE_TAC[
DOT_RMUL;
DOT_RADD;]
THEN REWRITE_TAC[REAL_ARITH`(&1-h)*A+h*B=A-h*(A-B)`]
THEN MATCH_MP_TAC
exists_esilon_real
THEN ASM_REWRITE_TAC[]);;
let invariant_rcross_dot_esilon_3piont=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
&0<(a1
cross a2)
dot a3
==>
?t. &0< t /\ t< &1 /\
(!h. &0< h /\ h< t==>
&0< (((&1 - h) % y + h % u-x)
cross a2)
dot a3)`,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - h) % v + h % u-x=(&1 - h) % (v-x) + h % (u-x)`;]
THEN REWRITE_TAC[
CROSS_LMUL;
CROSS_LADD;
DOT_LMUL;
DOT_LADD;]
THEN REWRITE_TAC[REAL_ARITH`(&1-h)*A+h*B=A-h*(A-B)`]
THEN MATCH_MP_TAC
exists_esilon_real
THEN ASM_REWRITE_TAC[]);;
let invariant_crossr_dot_esilon_3piont=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
&0<(a1
cross a2)
dot a3
==>
?t. &0< t /\ t< &1 /\
(!h. &0< h /\ h< t==>
&0< (a1
cross ((&1 - h) % z + h % u-x))
dot a3)`,
REPEAT GEN_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - h) % v + h % u-x=(&1 - h) % (v-x) + h % (u-x)`;]
THEN REWRITE_TAC[
CROSS_RMUL;
CROSS_RADD;
DOT_LMUL;
DOT_LADD;]
THEN REWRITE_TAC[REAL_ARITH`(&1-h)*A+h*B=A-h*(A-B)`]
THEN MATCH_MP_TAC
exists_esilon_real
THEN ASM_REWRITE_TAC[]);;
let condition_4point_aff_gt_1_2inter_aff_gt_1_2=prove(`!x:real^3 y:real^3 z:real^3 v:real^3 u:real^3 w:real^3 a:real.
let a1 = y - x in
let a2 = z - x in
let a3 = v - x in
let a4 = u - x in
let a5 = w - x in
~collinear {x,v,u}
/\ ~collinear {x,u,w}
/\ ~collinear {x,y,z}
/\ &0< a /\ a< &1
/\ y
IN aff_gt {x} {v,u}
/\ &0<(a3
cross a4)
dot a5
/\ (!h. &0< h /\ h< a==> ~collinear {x,v,(&1-h)%u+h%w})
/\ &0<(a3
cross a1)
dot a2
==> ?t. &0< t /\ t< &1 /\
(!h. &0< h /\ h< t==> ~(aff_gt {x} {y,z}
INTER aff_gt {x} {v,(&1-h)%u+h%w}={}))`,
REPEAT STRIP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE]
THEN STRIP_TAC
THEN MRESA_TAC
aff_gt_1_2_cross_dotr_4point[`x:real^3`;`y:real^3`;`z:real^3`;`v:real^3`;`u:real^3`;]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN MRESA_TAC
invariant_cross_dotr_esilon_3piont[`x:real^3`; `z:real^3`;`y:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN MRESA_TAC
properties_of_collinear4_points_fan[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN MRESA_TAC
point_in_aff_gt_2_1_change_point_in_aff_gt_1_2[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN MRESA_TAC
aff_gt_2_1r_rcross_dotl_4point[`x:real^3`;`y:real^3`;`z:real^3`;`v:real^3`;`u:real^3`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN MRESA_TAC
invariant_rcross_dot_esilon_3piont[`x:real^3`; `u:real^3`;`z:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"EM")
THEN ABBREV_TAC`
t1= min (min t t') a:real`
THEN MP_TAC(REAL_ARITH`&0<t/\ t< &1 /\ &0< t' /\ t'< &1 /\ &0< a /\ a < &1 /\
t1=min (min t t') a ==> &0<
t1 /\
t1 < &1`)
THEN RESA_TAC
THEN EXISTS_TAC`t1:real`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y1. y1
IN A`]
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`a1=(y-x):real^3`
THEN ABBREV_TAC`a2=(z-x):real^3`
THEN ABBREV_TAC`a3=(v-x) :real^3`
THEN ABBREV_TAC`a4=(&1 - h) % u + h % w-x:real^3`
THEN ABBREV_TAC`va=a1
cross a2:real^3`
THEN ABBREV_TAC`vb=a3
cross a4:real^3`
THEN ABBREV_TAC`v3= (vb:real^3)
cross (va:real^3)+(x:real^3)`
THEN EXISTS_TAC `v3:real^3`
THEN MP_TAC(REAL_ARITH`h<
t1 /\ t1< &1 /\
t1=min (min t t') a==> h<t' /\ h< &1 /\ h< t /\ h<a`)
THEN RESA_TAC
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `h:real`)
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN REWRITE_TAC[
DOT_LNEG]
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE]
THEN REWRITE_TAC[GSYM
DOT_LNEG]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_SKEW]
THEN RESA_TAC
THEN MRESA_TAC
th3[`x:real^3`;`u:real^3`;`w:real^3`;]
THEN MRESA_TAC
pos_in_aff_gt_2_1_fan [`x:real^3`;`u:real^3`;`w:real^3`;`h:real`]
THEN MRESAL_TAC
aff_gt_2_1_cross_dotl_4point[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`(&1 - h) % u + h % w:real^3`][VECTOR_ARITH`((&1 - h) % u + h % w) - x=(&1 - h) % u + h % w - x`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE]
THEN STRIP_TAC
THEN MRESA_TAC
aff_gt_inter_aff_gt [`(x:real^3)`;`(v:real^3)`;`(u:real^3)`]
THEN MP_TAC(SET_RULE`y
IN aff_gt {x} {v, u} /\ aff_gt {x} {v, u} = aff_gt {x, v} {u}
INTER aff_gt {x, u} {v}
==> y
IN aff_gt {x, v} {u:real^3}`)
THEN RESA_TAC
THEN MRESAL_TAC
aff_gt_2_1r_rcross_dotl_4point[`x:real^3`;`u:real^3`;`(&1 - h) % u + h % w:real^3`;`v:real^3`;`y:real^3`][VECTOR_ARITH`((&1 - h) % u + h % w) - x=(&1 - h) % u + h % w - x`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[
CROSS_TRIPLE]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN STRIP_TAC
THEN MRESAL_TAC
condition_cross_dot_4point[`x:real^3`;`v:real^3`;`(&1 - h) % u + h % w:real^3`;`y:real^3`;`z:real^3` ][VECTOR_ARITH`((&1 - h) % u + h % w) - x=(&1 - h) % u + h % w - x`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC
condition_cross_dot_4point[`x:real^3`; `z:real^3`;`y:real^3` ;`v:real^3`;`(&1 - h) % u + h % w:real^3`][VECTOR_ARITH`((&1 - h) % u + h % w) - x=(&1 - h) % u + h % w - x`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_RNEG]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_SKEW]
THEN REWRITE_TAC[
DOT_LNEG;REAL_ARITH`--(--A)=A`]
THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC
th`h:real`)
THEN REMOVE_THEN "LINH" (fun th-> MRESA1_TAC
th`h:real`)
THEN SET_TAC[]);;
end;;