(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)




module  Sin_azim_cross_dot= struct



open Sphere;;
open Tactic_fan;;
open Lemma_fan;;		



let JBDNJJB=prove(`!u:real^3 v:real^3 w:real^3.
~collinear {vec 0, u, v} /\ ~collinear {vec 0, u, w}
==>
?t:real. &0< t /\ sin(azim (vec 0) u v w)=t *(u cross v) dot w`,

REPEAT STRIP_TAC
THEN MRESA_TAC th3[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
THEN MRESA_TAC properties_coordinate[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
THEN MRESA_TAC azim[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`(w:real^3)`]
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)`])
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"YEU EM")
THEN DISCH_TAC THEN DISCH_TAC
THEN MRESA_TAC sincos1_of_u_fan[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`r1:real`; `psi:real`; `h1:real`]
THEN REMOVE_THEN "YEU EM" MP_TAC
THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`w =
      (r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
      (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
      h2 % u ==>
(u cross v) dot w =
(u cross v) dot ((r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
      (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
      h2 % u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
THEN REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF; e2_fan;e1_fan;e3_fan;
VECTOR_ARITH`A- vec 0= A`;CROSS_LADD; CROSS_RADD; CROSS_LMUL; CROSS_RMUL;CROSS_REFL;CROSS_RNEG;CROSS_LNEG;]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[NORM_MUL;REAL_INV_MUL; REAL_ABS_INV;REAL_INV_INV;REAL_ABS_NORM;DOT_SQUARE_NORM
;REAL_ARITH`(r2 * sin (azim (vec 0) u v w)) *
 (norm u * inv (norm (u cross v))) *
 inv (norm u) *
 norm (u cross v) pow 2 =(r2* norm(u cross v)) * sin (azim (vec 0) u v w) *
 ( inv (norm u) * norm u)*
( inv (norm (u cross v))* norm (u cross (v:real^3)))`
]
THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
THEN REDUCE_VECTOR_TAC
THEN RESA_TAC
THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASSUME_TAC(ISPEC`u:real^3`NORM_POS_LE)
THEN MP_TAC(REAL_ARITH`~(&0 =norm(u:real^3)) /\ &0 <= norm(u:real^3)==> &0 <norm(u:real^3)`)
THEN RESA_TAC
THEN SUBGOAL_THEN`~(u cross v = vec 0)` ASSUME_TAC
THENL[ASM_REWRITE_TAC[CROSS_EQ_0];

MP_TAC(ISPECL[`u cross v :real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
THEN REDUCE_VECTOR_TAC
THEN RESA_TAC
THEN MP_TAC(ISPEC`(norm(u cross v:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN ASSUME_TAC(ISPEC`u cross v:real^3`NORM_POS_LE)
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)`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`r2:real`;`norm(u cross v:real^3)`]
THEN MP_TAC(REAL_ARITH`&0<(r2:real)*norm(u cross v:real^3)==> ~((r2:real)*norm(u cross v:real^3)= &0)`)
THEN REDUCE_VECTOR_TAC
THEN RESA_TAC
THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_MUL_LINV)
THEN RESA_TAC
THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_LT_INV)
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(u cross v) dot w = (r2 * norm (u cross v)) * sin (azim (vec 0) u v w) ==>
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)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)) *
 sin (azim (vec 0) u v w)=(inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)))*
 sin (azim (vec 0) u v w)`]
THEN REDUCE_ARITH_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`inv (r2 * norm (u cross v)):real`
THEN ASM_REWRITE_TAC[]]);;


end;;