legacy/oldfan/JBDNJJB.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11
  12 module  Sin_azim_cross_dot= struct
  13
  14
  15
  16 open Sphere;;
  17 open Tactic_fan;;
  18 open Lemma_fan;;
  19
  20
  21
  22 let JBDNJJB=prove(`!u:real^3 v:real^3 w:real^3.
  23 ~collinear {vec 0, u, v} /\ ~collinear {vec 0, u, w}
  24 ==>
  25 ?t:real. &0< t /\ sin(azim (vec 0) u v w)=t *(u cross v) dot w`,
  26
  27 REPEAT STRIP_TAC
  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;]
  38 THEN REDUCE_ARITH_TAC
  39 THEN REDUCE_VECTOR_TAC
  40 THEN STRIP_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 +
  44       h2 % u ==>
  45 (u cross v) dot w =
  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 +
  48       h2 % u)`)
  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;]
  52 THEN REDUCE_ARITH_TAC
  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))) *
  56  inv (norm u) *
  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)))`
  60 ]
  61 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
  62 THEN REDUCE_VECTOR_TAC
  63 THEN RESA_TAC
  64 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
  65 THEN RESA_TAC
  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)`)
  68 THEN RESA_TAC
  69 THEN SUBGOAL_THEN`~(u cross v = vec 0)` ASSUME_TAC
  70 THENL[ASM_REWRITE_TAC[CROSS_EQ_0];
  71
  72 MP_TAC(ISPECL[`u cross v :real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
  73 THEN REDUCE_VECTOR_TAC
  74 THEN RESA_TAC
  75 THEN MP_TAC(ISPEC`(norm(u cross v:real^3))`REAL_MUL_LINV)
  76 THEN RESA_TAC
  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)`)
  79 THEN RESA_TAC
  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
  83 THEN RESA_TAC
  84 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_MUL_LINV)
  85 THEN RESA_TAC
  86 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_LT_INV)
  87 THEN RESA_TAC
  88 THEN REDUCE_ARITH_TAC
  89 THEN STRIP_TAC
  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)`]
  96 THEN REDUCE_ARITH_TAC
  97 THEN STRIP_TAC
  98 THEN EXISTS_TAC`inv (r2 * norm (u cross v)):real`
  99 THEN ASM_REWRITE_TAC[]]);;
 100
 101
 102 end;;