1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================== *)
12 module Sin_azim_cross_dot= struct
22 let JBDNJJB=prove(`!u:real^3 v:real^3 w:real^3.
23 ~collinear {vec 0, u, v} /\ ~collinear {vec 0, u, w}
25 ?t:real. &0< t /\ sin(azim (vec 0) u v w)=t *(u cross v) dot w`,
28 THEN MRESA_TAC th3[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
29 THEN MRESA_TAC properties_coordinate[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
30 THEN MRESA_TAC azim[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`(w:real^3)`]
31 THEN POP_ASSUM (fun th->MRESA_TAC th [`e1_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e2_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e3_fan ((vec 0):real^3) (u:real^3) (v:real^3)`])
32 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
33 THEN DISCH_THEN (LABEL_TAC"YEU EM")
34 THEN DISCH_TAC THEN DISCH_TAC
35 THEN MRESA_TAC sincos1_of_u_fan[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`r1:real`; `psi:real`; `h1:real`]
36 THEN REMOVE_THEN "YEU EM" MP_TAC
37 THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;]
39 THEN REDUCE_VECTOR_TAC
41 THEN MP_TAC(SET_RULE`w =
42 (r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
43 (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
46 (u cross v) dot ((r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
47 (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
49 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
50 THEN REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF; e2_fan;e1_fan;e3_fan;
51 VECTOR_ARITH`A- vec 0= A`;CROSS_LADD; CROSS_RADD; CROSS_LMUL; CROSS_RMUL;CROSS_REFL;CROSS_RNEG;CROSS_LNEG;]
53 THEN REWRITE_TAC[NORM_MUL;REAL_INV_MUL; REAL_ABS_INV;REAL_INV_INV;REAL_ABS_NORM;DOT_SQUARE_NORM
54 ;REAL_ARITH`(r2 * sin (azim (vec 0) u v w)) *
55 (norm u * inv (norm (u cross v))) *
57 norm (u cross v) pow 2 =(r2* norm(u cross v)) * sin (azim (vec 0) u v w) *
58 ( inv (norm u) * norm u)*
59 ( inv (norm (u cross v))* norm (u cross (v:real^3)))`
61 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
62 THEN REDUCE_VECTOR_TAC
64 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
66 THEN ASSUME_TAC(ISPEC`u:real^3`NORM_POS_LE)
67 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u:real^3)) /\ &0 <= norm(u:real^3)==> &0 <norm(u:real^3)`)
69 THEN SUBGOAL_THEN`~(u cross v = vec 0)` ASSUME_TAC
70 THENL[ASM_REWRITE_TAC[CROSS_EQ_0];
72 MP_TAC(ISPECL[`u cross v :real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
73 THEN REDUCE_VECTOR_TAC
75 THEN MP_TAC(ISPEC`(norm(u cross v:real^3))`REAL_MUL_LINV)
77 THEN ASSUME_TAC(ISPEC`u cross v:real^3`NORM_POS_LE)
78 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u cross v:real^3)) /\ &0 <= norm(u cross v:real^3)==> &0 <norm(u cross v:real^3)`)
80 THEN MRESA_TAC REAL_LT_MUL[`r2:real`;`norm(u cross v:real^3)`]
81 THEN MP_TAC(REAL_ARITH`&0<(r2:real)*norm(u cross v:real^3)==> ~((r2:real)*norm(u cross v:real^3)= &0)`)
82 THEN REDUCE_VECTOR_TAC
84 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_MUL_LINV)
86 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_LT_INV)
90 THEN MP_TAC(SET_RULE`(u cross v) dot w = (r2 * norm (u cross v)) * sin (azim (vec 0) u v w) ==>
91 inv (r2 * norm (u cross v))*(r2 * norm (u cross v)) * sin (azim (vec 0) u v w)= inv (r2 * norm (u cross v)) *((u cross v) dot w)`)
92 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
93 THEN ASM_REWRITE_TAC[REAL_ARITH`inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)) *
94 sin (azim (vec 0) u v w)=(inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)))*
95 sin (azim (vec 0) u v w)`]
98 THEN EXISTS_TAC`inv (r2 * norm (u cross v)):real`
99 THEN ASM_REWRITE_TAC[]]);;