text_formalization/local/VPWSHTO.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Local Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2012-04-01                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11
  12
  13 module  Vpwshto = struct
  14
  15
  16 open Sphere;;
  17 open Prove_by_refinement;;
  18 open Collect_geom;;
  19 open Fan_defs;;
  20 open Hypermap;;
  21 open Vol1;;
  22 open Fan;;
  23 open Topology;;
  24 open Fan_misc;;
  25 open Planarity;;
  26 open Pack_defs;;
  27
  28
  29 let NORM_COS_ANGLE_LE=prove(`!v u w w1:real^3.
  30 norm(v-w)=norm(v-w1)
  31 /\ ~(v=u) /\ ~(v=w)/\ ~(v=w1)
  32 ==> (norm (u-w)<= norm(u-w1)<=> cos(angle(u,v,w1))<= cos(angle(u,v,w)))`,
  33 REPEAT STRIP_TAC
  34 THEN MRESAL_TAC LAW_OF_COSINES[`v:real^3`;`u:real^3`;`w:real^3`][dist]
  35 THEN MRESAL_TAC LAW_OF_COSINES[`v:real^3`;`u:real^3`;`w1:real^3`][dist]
  36 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm(u-w:real^3)`;`norm(u-w1:real^3)`][NORM_POS_LE;REAL_ARITH`(a+b)- &2 * c<= (a+b)- &2 * c1<=> c1<= c`]
  37 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`]
  38 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`w1:real^3`]
  39 THEN MRESA_TAC REAL_LE_LMUL_EQ[`cos (angle (u,v,w1:real^3))`;` cos (angle (u,v,w:real^3))`;`norm(v-w1:real^3)`]
  40 THEN MRESA_TAC REAL_LE_LMUL_EQ[`norm(v-w1:real^3) *cos (angle (u,v,w1:real^3))`;` norm(v-w1:real^3)* cos (angle (u,v,w:real^3))`;`norm(v-u:real^3)`]);;
  41
  42
  43
  44
  45 let NORM_COS_ANGLE_LT=prove(`!v v1 u:real^3 u1 w w1:real^3.
  46 norm(v-w)=norm(v1-w1)
  47 /\  norm(v-u)=norm(v1-u1)
  48 /\ ~(v=u) /\ ~(v=w)/\ ~(v1=w1)
  49 ==> (norm (u-w)< norm(u1-w1)<=> (angle(u,v,w)) < (angle(u1,v1,w1)))`,
  50 REPEAT STRIP_TAC
  51 THEN MRESAL_TAC LAW_OF_COSINES[`v:real^3`;`u:real^3`;`w:real^3`][dist]
  52 THEN MRESAL_TAC LAW_OF_COSINES[`v1:real^3`;`u1:real^3`;`w1:real^3`][dist]
  53 THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NORM]
  54 THEN ONCE_REWRITE_TAC[REAL_LT_SQUARE_ABS]
  55 THEN ASM_REWRITE_TAC[NORM_POS_LE;REAL_ARITH`(a+b)- &2 * c< (a+b)- &2 * c1<=> c1< c`;]
  56 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`]
  57 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v1:real^3`;`w1:real^3`]
  58 THEN MRESA_TAC REAL_LT_LMUL_EQ[`cos (angle (u1,v1,w1:real^3))`;` cos (angle (u,v,w:real^3))`;`norm(v1-w1:real^3)`]
  59 THEN MRESA_TAC REAL_LT_LMUL_EQ[`norm(v1-w1:real^3) *cos (angle (u1,v1,w1:real^3))`;` norm(v1-w1:real^3)* cos (angle (u,v,w:real^3))`;`norm(v1-u1:real^3)`]
  60 THEN MATCH_MP_TAC COS_MONO_LT_EQ
  61 THEN REWRITE_TAC [ANGLE_RANGE]);;
  62
  63
  64 let NORM_COS_ANGLE_4POINT=prove(`!v u w w1:real^3.
  65 norm(v-w)=norm(u-w1)
  66 /\ ~(v=u) /\ ~(v=w)/\ ~(u=w1)
  67 ==> (norm (u-w)= norm(v-w1)<=>  cos(angle(v,u,w1))= cos(angle(u,v,w)))`,
  68 REPEAT STRIP_TAC
  69 THEN MRESAL_TAC LAW_OF_COSINES[`v:real^3`;`u:real^3`;`w:real^3`][dist]
  70 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`w1:real^3`][dist]
  71 THEN MRESAL_TAC DIST_EQ[`u:real^3`;`w:real^3`;`v:real^3`;`w1:real^3`][dist;REAL_ARITH`(a+b)- &2 * c= (a1+b)- &2 * c1<=> a1- &2 *c1= a- &2 *c`]
  72 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[NORM_SUB]
  73 THEN REWRITE_TAC[REAL_ARITH`a- &2 *c1= a- &2 *c<=> c1= c`]
  74 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`]
  75 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u:real^3`;`w1:real^3`][REAL_EQ_MUL_LCANCEL]
  76 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[NORM_SUB]
  77 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);;
  78
  79
  80
  81
  82
  83
  84 let MAX_COPLANAR_4POINT=prove(`!v x:real^3 u w w1:real^3.
  85 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
  86 /\ ~(v=w1) /\ ~(x=w1) /\ ~(u=w1)
  87 /\ norm(v-x)=t
  88 /\ norm(v-u)=a
  89 /\ norm(x-w)=a
  90 /\ norm(u-w)=a
  91 /\ y IN segment(v,w) INTER segment (x,u)
  92 /\ norm(x-w1)=a
  93 /\ norm(u-w1)=a
  94 ==> min (norm(v-w1)) (norm (x-u)) <= min (norm(v-w)) (norm (x-u))`,
  95 REPEAT STRIP_TAC
  96 THEN SUBGOAL_THEN`norm(y-w1)= norm(y-w:real^3)` ASSUME_TAC
  97 THENL[
  98 MRESAL_TAC DIST_EQ[`y:real^3`;`w1:real^3`;`y:real^3`;`w:real^3`][dist;]
  99 THEN MRESAL_TAC LAW_OF_COSINES[`x:real^3`;`y:real^3`;`w:real^3`][dist]
 100 THEN MRESAL_TAC LAW_OF_COSINES[`x:real^3`;`y:real^3`;`w1:real^3`][dist]
 101 THEN REWRITE_TAC[REAL_ARITH`a- &2 *c1= a- &2 *c<=> c1= c`]
 102 THEN MP_TAC(SET_RULE`y IN segment(v,w) INTER segment (x,u)
 103 ==> y IN segment(v,w)
 104 /\ y IN  segment (x,u:real^3)`)
 105 THEN ASM_REWRITE_TAC[IN_OPEN_SEGMENT]
 106 THEN STRIP_TAC
 107 THEN POP_ASSUM MP_TAC
 108 THEN POP_ASSUM MP_TAC
 109 THEN POP_ASSUM MP_TAC
 110 THEN REWRITE_TAC [IN_SEGMENT]
 111 THEN STRIP_TAC
 112 THEN POP_ASSUM(fun th->
 113  STRIP_TAC THEN STRIP_TAC
 114 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`]
 115 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`x:real^3`;`y:real^3`][REAL_EQ_MUL_LCANCEL]
 116 THEN MRESA_TAC ANGLE_EQ[`y:real^3`;`x:real^3`;`w:real^3`;`u:real^3`;`x:real^3`;`w:real^3`]
 117 THEN MRESA_TAC ANGLE_EQ[`y:real^3`;`x:real^3`;`w1:real^3`;`u:real^3`;`x:real^3`;`w1:real^3`]
 118 THEN POP_ASSUM MP_TAC
 119 THEN POP_ASSUM MP_TAC
 120 THEN MRESA1_TAC REAL_ABS_REFL`u':real`
 121 THEN ASM_REWRITE_TAC[th;VECTOR_ARITH`((&1 - u') % x + u' % u) - x=u' %(u-x)`;DOT_LMUL;NORM_MUL;REAL_ARITH`((u - x) dot (w - x)) * (u' * norm (u - x)) * norm (w - x) =
 122   (u' * ((u - x) dot (w - x))) * norm (u - x) * norm (w - x)`])
 123 THEN RESA_TAC
 124 THEN RESA_TAC
 125 THEN MRESAL_TAC CONGRUENT_TRIANGLES_SSS[`u:real^3`;`x:real^3`;`w:real^3`;`u:real^3`;`x:real^3`;`w1:real^3`][dist]
 126 THEN POP_ASSUM MP_TAC
 127 THEN ONCE_REWRITE_TAC[NORM_SUB]
 128 THEN RESA_TAC;
 129 MP_TAC(SET_RULE`y IN segment(v,w) INTER segment (x,u)
 130 ==> y IN segment(v,w:real^3)`)
 131 THEN ASM_REWRITE_TAC[IN_OPEN_SEGMENT]
 132 THEN STRIP_TAC
 133 THEN REMOVE_ASSUM_TAC
 134 THEN REMOVE_ASSUM_TAC
 135 THEN POP_ASSUM MP_TAC
 136 THEN REWRITE_TAC [IN_SEGMENT]
 137 THEN STRIP_TAC
 138 THEN POP_ASSUM(fun th->
 139 MRESAL_TAC NORM_TRIANGLE[`v-y:real^3`;`y-w1:real^3`][VECTOR_ARITH`A-B+B-C=A-C:real^3`]
 140 THEN POP_ASSUM MP_TAC
 141 THEN MRESA1_TAC REAL_ABS_REFL`u':real`
 142 THEN MRESAL1_TAC REAL_ABS_REFL`&1-u':real`[REAL_ARITH`&0<= &1- u<=> u<= &1`]
 143 THEN ASM_REWRITE_TAC[th;VECTOR_ARITH`v - ((&1 - u') % v + u' % w)=u' %(v-w)
 144 /\ ((&1 - u') % v + u' % w) - w= (&1- u') %(v-w)`;NORM_MUL; REAL_ARITH`u' * norm (v - w) + (&1 - u') * norm (v - w)=norm (v - w)`])
 145 THEN REAL_ARITH_TAC]);;
 146
 147
 148 let SUM_4ANGLE_4POINT_EQ_2PI=prove(`!v x:real^3 u w:real^3 y.
 149 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
 150 /\ y IN segment(v,w) INTER segment (x,u)
 151 ==> angle(x,v,u) + angle(v,u,w)+ angle(u,w,x)+angle(w,x,v)= &2 *pi`,
 152 REPEAT STRIP_TAC
 153 THEN MP_TAC(SET_RULE`y IN segment(v,w) INTER segment (x,u)
 154 ==> y IN segment(v,w:real^3)`)
 155 THEN ASM_REWRITE_TAC[IN_OPEN_SEGMENT]
 156 THEN STRIP_TAC
 157 THEN MRESAL_TAC ANGLES_ADD_BETWEEN[`v:real^3`;`w:real^3`;`y:real^3`;`u:real^3`][BETWEEN_IN_SEGMENT]
 158 THEN MRESAL_TAC ANGLES_ADD_BETWEEN[`v:real^3`;`w:real^3`;`y:real^3`;`x:real^3`][BETWEEN_IN_SEGMENT]
 159 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 160 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 161 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 162 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 163 THEN MP_TAC(SET_RULE`y IN segment(v,w) INTER segment (x,u)
 164 ==> y IN  segment (x,u:real^3)`)
 165 THEN ASM_REWRITE_TAC[IN_OPEN_SEGMENT]
 166 THEN STRIP_TAC
 167 THEN POP_ASSUM MP_TAC
 168 THEN POP_ASSUM MP_TAC
 169 THEN POP_ASSUM MP_TAC
 170 THEN REWRITE_TAC [IN_SEGMENT]
 171 THEN STRIP_TAC
 172 THEN POP_ASSUM(fun th->
 173 REPEAT STRIP_TAC
 174 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`]
 175 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`x:real^3`;`y:real^3`][REAL_EQ_MUL_LCANCEL]
 176 THEN MRESA_TAC ANGLE_EQ[`w:real^3`;`x:real^3`;`y:real^3`;`w:real^3`;`x:real^3`;`u:real^3`]
 177 THEN MRESA_TAC ANGLE_EQ[`y:real^3`;`x:real^3`;`v:real^3`;`u:real^3`;`x:real^3`;`v:real^3`]
 178 THEN MRESA_TAC ANGLE_EQ[`v:real^3`;`u:real^3`;`y:real^3`;`v:real^3`;`u:real^3`;`x:real^3`]
 179 THEN MRESA_TAC ANGLE_EQ[`y:real^3`;`u:real^3`;`w:real^3`;`x:real^3`;`u:real^3`;`w:real^3`]
 180 THEN POP_ASSUM MP_TAC
 181 THEN POP_ASSUM MP_TAC
 182 THEN POP_ASSUM MP_TAC
 183 THEN POP_ASSUM MP_TAC
 184 THEN MRESA1_TAC REAL_ABS_REFL`u':real`
 185 THEN MRESAL1_TAC REAL_ABS_REFL`&1-u':real`[REAL_ARITH`&0<= &1- u<=> u<= &1`]
 186 THEN ASM_REWRITE_TAC[th;VECTOR_ARITH`((&1 - u') % x + u' % u) - u= (&1- u') % (x-u)/\ ((&1 - u') % x + u' % u) - x= u' %(u-x)`;NORM_MUL;DOT_LMUL;DOT_RMUL;REAL_ARITH`a*(b*c)*d= (b*a) *c*d/\ a*c *b*d= (b*a) *c*d`])
 187 THEN RESA_TAC
 188 THEN RESA_TAC
 189 THEN RESA_TAC
 190 THEN RESA_TAC
 191 THEN REWRITE_TAC[REAL_ARITH`angle (x,v,u) +
 192  (angle (v,u,x) + angle (x,u,w)) +
 193  angle (u,w,x) +
 194  angle (u,x,v) +
 195  angle (w,x,u)
 196 = (angle (x,v,u)  + angle (u,x,v) +
 197  angle (v,u,x) )+ (angle (w,x,u) +
 198  angle (u,w,x) +angle (x,u,w) )`]
 199 THEN MRESA_TAC TRIANGLE_ANGLE_SUM[`v:real^3`;`x:real^3`;`u:real^3`]
 200 THEN MRESA_TAC TRIANGLE_ANGLE_SUM[`x:real^3`;`w:real^3`;`u:real^3`]
 201 THEN MRESA_TAC ANGLE_SYM[`u:real^3`;`x:real^3`;`v:real^3`]
 202 THEN MRESA_TAC ANGLE_SYM[`v:real^3`;`u:real^3`;`x:real^3`]
 203 THEN MRESA_TAC ANGLE_SYM[`u:real^3`;`w:real^3`;`x:real^3`]
 204 THEN MRESA_TAC ANGLE_SYM[`x:real^3`;`u:real^3`;`w:real^3`]
 205 THEN REAL_ARITH_TAC);;
 206
 207
 208 let EQ_DIAGONAL_MIN=prove(`!v v1 x:real^3 x1 u w u1 w1:real^3.
 209 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
 210 /\ ~(v1=x1)/\ ~(v1=u1) /\ ~(v1=w1) /\ ~(x1=u1)/\ ~(x1=w1) /\ ~(u1=w1)
 211 /\ norm(v-x)=t
 212 /\ norm(v-u)=a
 213 /\ norm(x-w)=a
 214 /\ norm(u-w)=a
 215 /\ y IN segment(v,w) INTER segment (x,u)
 216 /\ norm(v-w)=norm(x-u)
 217 /\ norm(v1-x1)=t
 218 /\ norm(v1-u1)=a
 219 /\ norm(x1-w1)=a
 220 /\ norm(u1-w1)=a
 221 /\ y1 IN segment(v1,w1) INTER segment (x1,u1)
 222 ==> min (norm(v1-w1)) (norm (x1-u1)) <= norm (x-u)`,
 223 REPEAT STRIP_TAC
 224 THEN DISJ_CASES_TAC(REAL_ARITH`norm (x-u:real^3)< min (norm(v1-w1:real^3)) (norm (x1-u1:real^3)) \/ min (norm(v1-w1)) (norm (x1-u1)) <= norm (x-u)`)
 225 THENL[
 226 MP_TAC (REAL_ARITH`norm (v - w:real^3) = norm (x - u:real^3)
 227 /\  norm (x-u) < min (norm(v1-w1)) (norm (x1-u1))
 228 ==> norm (x - u:real^3) < norm (x1 - u1:real^3)/\ norm (v - w:real^3) < norm (v1 - w1:real^3)`)
 229 THEN RESA_TAC
 230 THEN MRESA_TAC NORM_COS_ANGLE_LT[`x:real^3`;`x1:real^3`;`v:real^3`;`v1:real^3`;`w:real^3`;`w1:real^3`]
 231 THEN POP_ASSUM MP_TAC
 232 THEN ONCE_REWRITE_TAC[NORM_SUB]
 233 THEN RESA_TAC
 234 THEN MRESA_TAC NORM_COS_ANGLE_LT[`u:real^3`;`u1:real^3`;`v:real^3`;`v1:real^3`;`w:real^3`;`w1:real^3`]
 235 THEN POP_ASSUM MP_TAC
 236 THEN ONCE_REWRITE_TAC[NORM_SUB]
 237 THEN RESA_TAC
 238 THEN MRESA_TAC NORM_COS_ANGLE_LT[`v:real^3`;`v1:real^3`;`u:real^3`;`u1:real^3`;`x:real^3`;`x1:real^3`]
 239 THEN POP_ASSUM MP_TAC
 240 THEN ONCE_REWRITE_TAC[NORM_SUB]
 241 THEN RESA_TAC
 242 THEN MRESA_TAC NORM_COS_ANGLE_LT[`w:real^3`;`w1:real^3`;`u:real^3`;`u1:real^3`;`x:real^3`;`x1:real^3`]
 243 THEN POP_ASSUM MP_TAC
 244 THEN ONCE_REWRITE_TAC[NORM_SUB]
 245 THEN RESA_TAC
 246 THEN MP_TAC(REAL_ARITH`angle (v,x,w) < angle (v1,x1,w1)
 247 /\ angle (v,u,w) < angle (v1,u1,w1)/\
 248 angle (u,v,x) < angle (u1,v1,x1) /\angle (u,w,x) < angle (u1,w1,x1)
 249 ==> angle (u,v,x:real^3) +angle (v,u,w) + angle (u,w,x) + angle (v,x,w)
 250 < angle (u1,v1,x1:real^3) +angle (v1,u1,w1) + angle (u1,w1,x1) + angle (v1,x1,w1)`)
 251 THEN ASM_REWRITE_TAC[]
 252 THEN MRESA_TAC SUM_4ANGLE_4POINT_EQ_2PI[`v:real^3`;`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`]
 253 THEN MRESA_TAC SUM_4ANGLE_4POINT_EQ_2PI[`v1:real^3`;`x1:real^3`;`u1:real^3`;`w1:real^3`;`y1:real^3`]
 254 THEN MRESA_TAC ANGLE_SYM[`u:real^3`;`v:real^3`;`x:real^3`]
 255 THEN MRESA_TAC ANGLE_SYM[`u1:real^3`;`v1:real^3`;`x1:real^3`]
 256 THEN MRESA_TAC ANGLE_SYM[`v:real^3`;`x:real^3`;`w:real^3`]
 257 THEN MRESA_TAC ANGLE_SYM[`v1:real^3`;`x1:real^3`;`w1:real^3`]
 258 THEN REAL_ARITH_TAC;
 259 ASM_REWRITE_TAC[]]);;
 260
 261
 262
 263
 264
 265 let TWO_DIAGONAL_AT_MOST=prove_by_refinement(` &2 <=t /\ t<= &4
 266 ==>
 267 ?u w:real^3 v x y.
 268 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
 269 /\ norm(v-x)=t
 270 /\ norm(v-u)= &2
 271 /\ norm(x-w)= &2
 272 /\ norm(u-w)= &2
 273 /\ y IN segment(v,w) INTER segment (x,u)
 274 /\ norm(v-w)= norm(x-u)
 275 /\ (t<= norm(v-w) ==> norm(v-w)<= &1 + sqrt( &5) /\ t<= &1 + sqrt( &5))`,
 276 [REPEAT STRIP_TAC
 277 THEN ABBREV_TAC`b=(&1- t/ &2)`
 278 THEN ABBREV_TAC`c=(&1+ t/ &2)`
 279 THEN ABBREV_TAC`d=(sqrt(&4- (t/ &2- &1) pow 2))`
 280 THEN ABBREV_TAC`e= &2* inv(t+ &2) * d`
 281 THEN SUBGOAL_THEN`&0<= &4- (t/ &2- &1) pow 2` ASSUME_TAC;
 282 REWRITE_TAC[REAL_ARITH`&0<= A- B<=> B<=A`]
 283 THEN MATCH_MP_TAC REAL_RSQRT_LE
 284 THEN MRESAL_TAC SQRT_UNIQUE[`&4`;`&2`][REAL_ARITH`&0<= &2 /\ &2 pow 2= &4`]
 285 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 <= t / &2 - &1 <=> &2<= t`; REAL_ARITH`t / &2 - &1 <= &2 <=>  t<= &6`; REAL_ARITH`&0 <= &4`]
 286 THEN MP_TAC(REAL_ARITH`t<= &4==> t <= &6`)
 287 THEN RESA_TAC;
 288 SUBGOAL_THEN`~(&4- (t/ &2- &1) pow 2= &0)` ASSUME_TAC;
 289 REWRITE_TAC[REAL_ARITH`A-B= &0 <=> B=A`]
 290 THEN STRIP_TAC
 291 THEN MRESAL_TAC Collect_geom.EQ_POW2_COND[`t/ &2 - &1`;`&2`][REAL_ARITH`&2 pow 2= &4/\ &0<= &2`;REAL_ARITH`&0 <= t / &2 - &1<=> &2<= t`;REAL_ARITH`t / &2 - &1 = &2<=> t= &6`]
 292 THEN POP_ASSUM MP_TAC
 293 THEN MP_TAC(REAL_ARITH`t<= &4==> ~(t = &6)`)
 294 THEN RESA_TAC;
 295 SUBGOAL_THEN`b pow 2 + d pow 2= &4`ASSUME_TAC;
 296 MRESA1_TAC SQRT_POW_2`&4- (t/ &2- &1) pow 2`
 297 THEN EXPAND_TAC"b"
 298 THEN REAL_ARITH_TAC;
 299 MRESA1_TAC SQRT_EQ_0`&4- (t/ &2- &1) pow 2`
 300 THEN MP_TAC(REAL_ARITH`&2<= t==> &0<= t/\ (&1 - t / &2) - (&1 + t / &2)= -- t
 301 /\ (&1 + t / &2) - &2= -- (&1 - t / &2) /\ &0< t /\ &0< t+ &2/\ ~(t + &2= &0)
 302 /\ (&1 - t / &2) - &2= -- (&1 + t / &2) /\ ~(t<= &0)`)
 303 THEN RESA_TAC
 304 THEN SUBGOAL_THEN`&1 - t * inv (t + &2) = &2 * inv (t + &2)` ASSUME_TAC;
 305 REWRITE_TAC[REAL_ARITH`A-B *D=C *D<=> D *(B+C)= A:real`]
 306 THEN MATCH_MP_TAC REAL_MUL_LINV
 307 THEN ASM_REWRITE_TAC[];
 308 EXISTS_TAC`vec 0:real^3`
 309 THEN EXISTS_TAC`(vector[&2; &0; &0]):real^3`
 310 THEN EXISTS_TAC`(vector[b; d; &0]):real^3`
 311 THEN EXISTS_TAC`(vector[c; d; &0]):real^3`
 312 THEN EXISTS_TAC`(vector[&1;e; &0]):real^3`
 313 THEN STRIP_TAC;
 314 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
 315 THEN EXPAND_TAC"b"
 316 THEN EXPAND_TAC"c"
 317 THEN REWRITE_TAC[REAL_ARITH`&1 - t / &2 = &1 + t / &2 <=> t= &0`]
 318 THEN MP_TAC(REAL_ARITH`&2<=t==> ~(t= &0)`)
 319 THEN RESA_TAC;
 320 STRIP_TAC;
 321 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
 322 THEN EXPAND_TAC"b"
 323 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - t / &2= &0 <=> t= &2`;REAL_ARITH`&1 + t / &2= &0 <=> t= -- &2`;DE_MORGAN_THM];
 324 STRIP_TAC;
 325 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
 326 STRIP_TAC;
 327 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
 328 STRIP_TAC;
 329 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
 330 STRIP_TAC;
 331 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM;REAL_ARITH`~(&0= &2)`];
 332 STRIP_TAC;
 333 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 334            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 335            vector_neg; vector_sub; vector_mul; ARITH;]
 336 THEN REAL_ARITH_TAC;
 337 STRIP_TAC;
 338 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 339            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 340            vector_neg; vector_sub; vector_mul; ARITH;VECTOR_ARITH`A- vec 0=A`;
 341 REAL_ARITH`&0<= &2 /\ a * a= a pow 2/\ A+ &0 pow 2=A/\ &2 pow 2= &4`];
 342 STRIP_TAC;
 343 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 344            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 345            vector_neg; vector_sub; vector_mul; ARITH;
 346 REAL_ARITH`&0<= &2  /\ --a * --a= a pow 2/\ A- &0 =A/\ A+ &0 * &0=A/\ &2 pow 2= &4`]
 347 THEN ASM_REWRITE_TAC[REAL_ARITH`b * b= b pow 2`];
 348 STRIP_TAC;
 349 ONCE_REWRITE_TAC[NORM_SUB]
 350 THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 351            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 352            vector_neg; vector_sub; vector_mul; ARITH;VECTOR_ARITH`A- vec 0=A`;
 353 REAL_ARITH`&0<= &2 /\ a * a= a pow 2/\ A+ &0 pow 2=A/\ &2 pow 2= &4`];
 354 STRIP_TAC;
 355 REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
 356 THEN STRIP_TAC;
 357 STRIP_TAC;
 358 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
 359 EXISTS_TAC`t * inv(t+ &2)`
 360 THEN STRIP_TAC;
 361 MATCH_MP_TAC REAL_LT_MUL
 362 THEN ASM_REWRITE_TAC[]
 363 THEN MATCH_MP_TAC REAL_LT_INV
 364 THEN ASM_REWRITE_TAC[];
 365 STRIP_TAC;
 366 MATCH_MP_TAC REAL_LT_RCANCEL_IMP
 367 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`
 368 THEN EXISTS_TAC`t+ &2`
 369 THEN ASM_REWRITE_TAC[REAL_ARITH`(A *B) * C= A *(B*C)`]
 370 THEN REAL_ARITH_TAC;
 371 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 372            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 373            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`&2 * inv (t + &2) * b + t * inv (t + &2) * &2= &2 * inv (t + &2) * (b+t)`]
 374 THEN EXPAND_TAC"b"
 375 THEN REWRITE_TAC[REAL_ARITH`&1 = &2 * inv (t + &2) * (&1 - t / &2 + t)
 376 <=> inv (t + &2) * (t + &2)= &1`]
 377 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`;
 378 STRIP_TAC;
 379 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
 380 EXISTS_TAC`t * inv(t+ &2)`
 381 THEN STRIP_TAC;
 382 MATCH_MP_TAC REAL_LT_MUL
 383 THEN ASM_REWRITE_TAC[]
 384 THEN MATCH_MP_TAC REAL_LT_INV
 385 THEN ASM_REWRITE_TAC[];
 386 STRIP_TAC;
 387 MATCH_MP_TAC REAL_LT_RCANCEL_IMP
 388 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`
 389 THEN EXISTS_TAC`t+ &2`
 390 THEN ASM_REWRITE_TAC[REAL_ARITH`(A *B) * C= A *(B*C)`]
 391 THEN REAL_ARITH_TAC;
 392 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 393            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
 394            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`&2 * inv (t + &2) * b + t * inv (t + &2) * &2= &2 * inv (t + &2) * (b+t)`]
 395 THEN EXPAND_TAC"c"
 396 THEN REWRITE_TAC[REAL_ARITH`&1 = &2 * inv (t + &2) * (&1 + t / &2)
 397 <=> inv (t + &2) * (t + &2)= &1`]
 398 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`;
 399 STRIP_TAC;
 400 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 401            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ;
 402            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`a- &0=a `;VECTOR_ARITH`A- vec 0=A`]
 403 THEN REAL_ARITH_TAC;
 404 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a<=b <=> b>=a`]
 405 THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
 406            vector_add; vec; dot; cross; orthogonal; basis; NORM_LE_SQUARE;NORM_GE_SQUARE;
 407            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c/\ --c * --c + d * d= c pow 2 + d pow 2`;REAL_ARITH`a- &0=a `;VECTOR_ARITH`A- vec 0=A`]
 408 THEN MRESA1_TAC SQRT_POW_2`&4 - (t / &2 - &1) pow 2`
 409 THEN MRESAL1_TAC SQRT_POW_2`(&5)`[REAL_ARITH`&0<= &5`;REAL_ARITH`(&1 + sqrt (&5)) pow 2= &1 + &2 * sqrt(&5) + sqrt(&5) pow 2`]
 410 THEN EXPAND_TAC"c"
 411 THEN REWRITE_TAC[REAL_ARITH`(&1 + t / &2) pow 2 + &4 - (t / &2 - &1) pow 2
 412 =  &4 + &2 * t`;REAL_ARITH`&4 + &2 * t <= &1 + &2 * sqrt (&5) + &5<=>  t <= &1 + sqrt( &5) `; REAL_ARITH`&4 + &2 * t >= t pow 2<=> (t- &1) pow 2<= &5`]
 413 THEN STRIP_TAC
 414 THEN MRESAL_TAC REAL_LE_RSQRT[`t- &1`;`&5`][REAL_ARITH`A-B<= C<=> A<= B+C`]
 415 THEN MRESAL1_TAC SQRT_POS_LE`&5`[REAL_ARITH`&0<= &5`]
 416 THEN POP_ASSUM MP_TAC
 417 THEN REAL_ARITH_TAC]);;
 418
 419
 420
 421
 422
 423
 424
 425 let MAX_IF_COPLANAR=prove_by_refinement(`!v x:real^3  u w:real^3 a t.
 426  a<= t /\
 427 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
 428 /\ ~(collinear{v,x,u})
 429 /\ ~(collinear{w,x,u})
 430 /\ norm(v-x)=t
 431 /\ norm(v-u)=a
 432 /\ norm(x-w)=a
 433 /\ norm(u-w)=a
 434 /\ t<= norm(x-u)
 435 ==> ?w1 y.
 436 y IN segment(v,w1) INTER segment (x,u)
 437 /\ norm(x-w1)=a
 438 /\ norm(u-w1)=a
 439 /\ ~(v=w1)`,
 440 [REPEAT STRIP_TAC
 441 THEN ABBREV_TAC`b=norm(x-u:real^3)`
 442 THEN ABBREV_TAC`a1= inv(b) * (a pow 2 + b pow 2 -t pow 2)/ &2`
 443 THEN ABBREV_TAC`v1= (a1 * inv(b)) % (x-u:real^3) +u:real^3`
 444 THEN ABBREV_TAC`y1= (&1/ &2) %(u+x:real^3) `
 445 THEN ABBREV_TAC`b1= sqrt(a pow 2- (b/ &2) pow 2) `
 446 THEN ABBREV_TAC`w1= (b1* inv(norm(v1- v))) %(v1-v:real^3) +y1`
 447 THEN ABBREV_TAC`y= (&1- norm(v1-v:real^3) * inv(norm(v1-v)+b1)) %v + (norm(v1-v) * inv(norm(v1-v)+b1)) % w1:real^3`
 448 THEN SUBGOAL_THEN`~(y1=x:real^3)` ASSUME_TAC;
 449 EXPAND_TAC"y1"
 450 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) = x<=> x=u`]
 451 THEN ASM_REWRITE_TAC[];
 452 SUBGOAL_THEN`~(y1=u:real^3)` ASSUME_TAC;
 453 EXPAND_TAC"y1"
 454 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) = u<=> x=u`]
 455 THEN ASM_REWRITE_TAC[];
 456 SUBGOAL_THEN`y1 IN segment[u,x:real^3]`ASSUME_TAC;
 457 REWRITE_TAC[IN_SEGMENT]
 458 THEN EXISTS_TAC`&1/ &2`
 459 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1/ &2 /\ &1/ &2<= &1 /\ &1- &1/ &2= &1/ &2`;VECTOR_ARITH`A % x + A % u= A%(x+u)`];
 460 SUBGOAL_THEN`~(y1=w:real^3)` ASSUME_TAC;
 461 STRIP_TAC
 462 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 463 THEN MP_TAC(REAL_ARITH`&0 = &0`)
 464 THEN MRESA_TAC COLLINEAR_SUBSET[`{w,x,u:real^3}`;`segment[u,x:real^3]`]
 465 THEN ASM_REWRITE_TAC[COLLINEAR_SEGMENT]
 466 THEN MRESA_TAC ENDS_IN_SEGMENT[`u:real^3`;`x:real^3`]
 467 THEN POP_ASSUM MP_TAC
 468 THEN POP_ASSUM MP_TAC
 469 THEN POP_ASSUM MP_TAC
 470 THEN SET_TAC[];
 471 SUBGOAL_THEN`&0<=a pow 2 - (b / &2) pow 2` ASSUME_TAC;
 472 MRESAL_TAC CONGRUENT_TRIANGLES_SSS[`w:real^3`;`y1:real^3`;`u:real^3`;`w:real^3`;`y1:real^3`;`x:real^3`][dist]
 473 THEN POP_ASSUM MP_TAC
 474 THEN EXPAND_TAC"y1"
 475 THEN REWRITE_TAC[VECTOR_ARITH`(&1 / &2) % (u + x) - u = &1 / &2 % (x - u) /\ (&1 / &2) % (u + x) - x = (&1 / &2) % (u -x) `;NORM_MUL;]
 476 THEN SIMP_TAC[NORM_SUB]
 477 THEN ASM_REWRITE_TAC[]
 478 THEN STRIP_TAC
 479 THEN MRESAL_TAC ANGLES_ALONG_LINE[`u:real^3`;`x:real^3`;`y1:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT]
 480 THEN POP_ASSUM MP_TAC
 481 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 482 THEN ASM_REWRITE_TAC[REAL_ARITH`A+A= B <=> A= B/ &2`]
 483 THEN STRIP_TAC
 484 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`w:real^3`;`u:real^3`][dist]
 485 THEN POP_ASSUM MP_TAC
 486 THEN ONCE_REWRITE_TAC[NORM_SUB]
 487 THEN ASM_REWRITE_TAC[COS_PI2; REAL_ARITH`A * &0= &0/\ A- &0= A`]
 488 THEN EXPAND_TAC"y1"
 489 THEN REWRITE_TAC[VECTOR_ARITH`u - &1 / &2 % (u + x)= &1 / &2 % (u - x)`;NORM_MUL;REAL_ARITH`abs(&1/ &2)= &1/ &2`]
 490 THEN ASM_REWRITE_TAC[]
 491 THEN ONCE_REWRITE_TAC[NORM_SUB]
 492 THEN ASM_REWRITE_TAC[REAL_ARITH`&1/ &2 *A=A/ &2`]
 493 THEN RESA_TAC
 494 THEN REWRITE_TAC[REAL_ARITH`(A+B)-B=A`;REAL_LE_POW_2];
 495 SUBGOAL_THEN`&0< a pow 2 - (b / &2) pow 2` ASSUME_TAC;
 496 MRESAL_TAC CONGRUENT_TRIANGLES_SSS[`w:real^3`;`y1:real^3`;`u:real^3`;`w:real^3`;`y1:real^3`;`x:real^3`][dist]
 497 THEN POP_ASSUM MP_TAC
 498 THEN EXPAND_TAC"y1"
 499 THEN REWRITE_TAC[VECTOR_ARITH`(&1 / &2) % (u + x) - u = &1 / &2 % (x - u) /\ (&1 / &2) % (u + x) - x = (&1 / &2) % (u -x) `;NORM_MUL;]
 500 THEN SIMP_TAC[NORM_SUB]
 501 THEN ASM_REWRITE_TAC[]
 502 THEN STRIP_TAC
 503 THEN MRESAL_TAC ANGLES_ALONG_LINE[`u:real^3`;`x:real^3`;`y1:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT]
 504 THEN POP_ASSUM MP_TAC
 505 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 506 THEN ASM_REWRITE_TAC[REAL_ARITH`A+A= B <=> A= B/ &2`]
 507 THEN STRIP_TAC
 508 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`w:real^3`;`u:real^3`][dist]
 509 THEN POP_ASSUM MP_TAC
 510 THEN ONCE_REWRITE_TAC[NORM_SUB]
 511 THEN ASM_REWRITE_TAC[COS_PI2; REAL_ARITH`A * &0= &0/\ A- &0= A`]
 512 THEN EXPAND_TAC"y1"
 513 THEN REWRITE_TAC[VECTOR_ARITH`u - &1 / &2 % (u + x)= &1 / &2 % (u - x)`;NORM_MUL;REAL_ARITH`abs(&1/ &2)= &1/ &2`]
 514 THEN ASM_REWRITE_TAC[]
 515 THEN ONCE_REWRITE_TAC[NORM_SUB]
 516 THEN ASM_REWRITE_TAC[REAL_ARITH`&1/ &2 *A=A/ &2`]
 517 THEN RESA_TAC
 518 THEN REWRITE_TAC[REAL_ARITH`(A+B)-B=A`;REAL_LE_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]
 519 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`y1:real^3`;`w:real^3`][REAL_EQ_MUL_LCANCEL];
 520 MRESA1_TAC SQRT_WORKS`a pow 2 - (b / &2) pow 2`
 521 THEN
 522 MRESA1_TAC SQRT_POS_LT`a pow 2 - (b / &2) pow 2`
 523 THEN SUBGOAL_THEN`&0<= b1 * inv (norm(v1- v:real^3))`ASSUME_TAC;
 524 MATCH_MP_TAC REAL_LE_MUL
 525 THEN ASM_REWRITE_TAC[]
 526 THEN MATCH_MP_TAC REAL_LE_INV
 527 THEN REWRITE_TAC[NORM_POS_LE];
 528 MRESAL_TAC Planarity.IMP_NORM_FAN[`x:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
 529 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
 530 THEN SUBGOAL_THEN`~(v1=v:real^3)` ASSUME_TAC;
 531 EXPAND_TAC"v1"
 532 THEN REWRITE_TAC[VECTOR_ARITH`(a1 * inv b) % (x-u) + u = v<=> (a1 * inv b) % ( x-u) = v-u`]
 533 THEN STRIP_TAC
 534 THEN MP_TAC(SET_RULE`(a1 * inv b) % (x-u) = v - u:real^3
 535 ==>  norm((a1 * inv b) % ( x-u)) = norm( v - u)`)
 536 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 537 THEN ASM_REWRITE_TAC[NORM_MUL]
 538 THEN ONCE_REWRITE_TAC[NORM_SUB]
 539 THEN ASM_REWRITE_TAC[REAL_ARITH`(a*b)*c= a*(b*c)`;REAL_ABS_MUL]
 540 THEN MRESAL1_TAC REAL_ABS_REFL`inv b:real`[REAL_ARITH`A* &1=A`]
 541 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
 542 THEN POP_ASSUM MP_TAC
 543 THEN ONCE_REWRITE_TAC[NORM_SUB]
 544 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,x))<=>  a pow 2 + b pow 2 -t pow 2= &2 * a * b * cos (angle (v,u,x)) `]
 545 THEN STRIP_TAC
 546 THEN EXPAND_TAC"a1"
 547 THEN POP_ASSUM(fun th-> REWRITE_TAC[th;REAL_ABS_MUL;REAL_ARITH`(&2*A)/ &2=A`])
 548 THEN ASM_REWRITE_TAC[REAL_ABS_MUL]
 549 THEN MRESAL1_TAC REAL_ABS_REFL`b:real`[REAL_ARITH`A* &1=A`]
 550 THEN MRESAL1_TAC REAL_ABS_REFL`a:real`[REAL_ARITH`A* &1=A`]
 551 THEN ASM_REWRITE_TAC[REAL_ARITH`A *B* C*D=(A*C) *B*D /\ &1*A=A`]
 552 THEN STRIP_TAC
 553 THEN MP_TAC(SET_RULE`a * abs (cos (angle (v,u,x:real^3))) = a
 554 ==> inv(a) * (a * abs (cos (angle (v,u,x)))) = inv a * a`)
 555 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 556 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(A*B)*C/\ &1 *A =A`]
 557 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= cos (angle (v,u,x:real^3)) \/ &0<= -- cos (angle (v,u,x))`);
 558 MRESAL1_TAC REAL_ABS_REFL`cos (angle (v,u,x:real^3))`[REAL_ARITH`A* &1=A`]
 559 THEN STRIP_TAC
 560 THEN ASSUME_TAC(PI_WORKS)
 561 THEN MP_TAC(REAL_ARITH`&0< pi==> &0<= pi`)
 562 THEN RESA_TAC
 563 THEN MRESAL_TAC COS_INJ_PI[`angle (v,u,x:real^3)`;`&0`][COS_0;ANGLE_RANGE;REAL_ARITH`&0<= &0`]
 564 THEN MRESA_TAC COLLINEAR_ANGLE[`v:real^3`;`u:real^3`;`x:real^3`]
 565 THEN POP_ASSUM MP_TAC
 566 THEN REWRITE_TAC[]
 567 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 568 THEN RESA_TAC;
 569 MRESAL1_TAC REAL_ABS_REFL`-- cos (angle (v,u,x:real^3))`[REAL_ARITH`--A=  &1<=> A= -- &1`;REAL_ABS_NEG]
 570 THEN STRIP_TAC
 571 THEN ASSUME_TAC(PI_WORKS)
 572 THEN MP_TAC(REAL_ARITH`&0< pi==> &0<= pi`)
 573 THEN RESA_TAC
 574 THEN MRESAL_TAC COS_INJ_PI[`angle (v,u,x:real^3)`;`pi`][COS_PI;ANGLE_RANGE;REAL_ARITH`pi<= pi`]
 575 THEN MRESA_TAC COLLINEAR_ANGLE[`v:real^3`;`u:real^3`;`x:real^3`]
 576 THEN POP_ASSUM MP_TAC
 577 THEN REWRITE_TAC[]
 578 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 579 THEN RESA_TAC;
 580 MRESAL_TAC Planarity.IMP_NORM_FAN[`v1:real^3`;`v:real^3`][REAL_EQ_MUL_LCANCEL]
 581 THEN SUBGOAL_THEN`angle(v,u,x)= angle(v,u,y1:real^3)`ASSUME_TAC;
 582 MRESA_TAC ANGLE_EQ[`v:real^3`;`u:real^3`;`x:real^3`;`v:real^3`;`u:real^3`;`y1:real^3`]
 583 THEN EXPAND_TAC"y1"
 584 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % ( x - u)`;NORM_MUL;REAL_ARITH`abs(&1/ &2) *A=A/ &2`;REAL_ARITH`(A+B)- &2 * C= A-B<=> B=C`;DOT_RMUL]
 585 THEN REAL_ARITH_TAC;
 586 SUBGOAL_THEN`~(v=w1:real^3)` ASSUME_TAC;
 587 EXPAND_TAC"w1"
 588 THEN REWRITE_TAC[VECTOR_ARITH`v = (b1 * inv (norm (v1 - v))) % (v1 - v) + y1
 589 <=> v- y1 = (b1 * inv (norm (v1 - v))) % (v1 - v) `]
 590 THEN STRIP_TAC
 591 THEN MP_TAC(SET_RULE`v - y1 = (b1 * inv (norm (v1 - v))) % (v1 - v):real^3
 592 ==> norm(v - y1) = norm( (b1 * inv (norm (v1 - v))) % (v1 - v))`)
 593 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC (SYM th))
 594 THEN REWRITE_TAC[NORM_MUL]
 595 THEN MRESA1_TAC REAL_ABS_REFL`b1 * inv (norm(v1- v:real^3))`
 596 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ A* &1= A`]
 597 THEN STRIP_TAC
 598 THEN MP_TAC(SET_RULE`norm (v - y1:real^3) = b1
 599 ==> norm (v - y1) pow 2= b1 pow 2`)
 600 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC (SYM th))
 601 THEN ASM_REWRITE_TAC[]
 602 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`y1:real^3`][dist]
 603 THEN ONCE_REWRITE_TAC[NORM_SUB]
 604 THEN ASM_REWRITE_TAC[]
 605 THEN EXPAND_TAC"y1"
 606 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % ( x - u)`;NORM_MUL;REAL_ARITH`abs(&1/ &2) *A=A/ &2`;REAL_ARITH`(A+B)- &2 * C= A-B<=> B=C`]
 607 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
 608 THEN POP_ASSUM MP_TAC
 609 THEN ONCE_REWRITE_TAC[NORM_SUB]
 610 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,y1))
 611 <=>  a * b / &2* cos (angle (v,u,y1))= (a pow 2 + b pow 2- t pow 2  )/ &4`]
 612 THEN RESA_TAC
 613 THEN REWRITE_TAC[REAL_ARITH`(b / &2) pow 2 = (a pow 2 + b pow 2 - t pow 2) / &4<=> a pow 2= t pow 2`]
 614 THEN STRIP_TAC
 615 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 616 THEN ASM_TAC
 617 THEN REWRITE_TAC[REAL_ARITH`A+B-A=B`]
 618 THEN REPEAT STRIP_TAC
 619 THEN MP_TAC(REAL_ARITH`inv b * b pow 2 / &2 = (inv b * b) * b / &2`)
 620 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *A=A`]
 621 THEN STRIP_TAC
 622 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 623 THEN MP_TAC(VECTOR_ARITH`(b / &2 * inv b) % (x-u) + u= (inv b *b )/ &2 % (x-u) + u:real^3`)
 624 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (x-u) + u= &1/ &2 %(u+x)`]
 625 THEN STRIP_TAC
 626 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 627 THEN REMOVE_ASSUM_TAC
 628 THEN REMOVE_ASSUM_TAC
 629 THEN POP_ASSUM MP_TAC
 630 THEN REWRITE_TAC[]
 631 THEN ONCE_REWRITE_TAC[NORM_SUB]
 632 THEN STRIP_TAC
 633 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
 634 THEN REMOVE_ASSUM_TAC
 635 THEN POP_ASSUM MP_TAC
 636 THEN REWRITE_TAC[]
 637 THEN ONCE_REWRITE_TAC[REAL_ARITH`norm (y1 - v) * inv (norm (y1 - v)) =  inv (norm (y1 - v))* norm (y1 - v) `]
 638 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 % (y1 - v) = v - y1<=> y1=v`];
 639 SUBGOAL_THEN`norm(v1-u:real^3) pow 2+ norm(v1- v) pow 2= norm(v-u:real^3) pow 2`ASSUME_TAC;
 640 DISJ_CASES_TAC(SET_RULE`v1=u \/ ~(v1=u:real^3)`);
 641 ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0 pow 2+A= A`]
 642 THEN ONCE_REWRITE_TAC[NORM_SUB]
 643 THEN ASM_REWRITE_TAC[];
 644 MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`v1:real^3`][dist]
 645 THEN ONCE_REWRITE_TAC[NORM_SUB]
 646 THEN ASM_REWRITE_TAC[]
 647 THEN ONCE_REWRITE_TAC[NORM_SUB]
 648 THEN EXPAND_TAC"v1"
 649 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u= (a1 * inv b) % (x - u) `]
 650 THEN ASM_REWRITE_TAC[]
 651 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
 652 THEN POP_ASSUM MP_TAC
 653 THEN ONCE_REWRITE_TAC[NORM_SUB]
 654 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,y1))
 655 <=> a * b * cos (angle (v,u,y1))= (a pow 2 + b pow 2- t pow 2) / &2 `]
 656 THEN STRIP_TAC
 657 THEN MP_TAC(SET_RULE`a * b * cos (angle (v,u,y1:real^3))= (a pow 2 + b pow 2- t pow 2) / &2
 658 ==> inv b*(a * b * cos (angle (v,u,y1)))= inv b*((a pow 2 + b pow 2- t pow 2) / &2 )`)
 659 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 660 THEN REWRITE_TAC[REAL_ARITH`inv b * a * b * cos (angle (v,u,y1))= (inv b * b) * a * cos (angle (v,u,y1))`]
 661 THEN ASM_REWRITE_TAC[NORM_MUL;REAL_ARITH`&1*A=A`;REAL_ABS_MUL;REAL_ABS_INV]
 662 THEN MRESA1_TAC REAL_ABS_NORM`x-u:real^3`
 663 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &1=A /\ (A*B)*C=A*(B*C)/\ abs a pow 2= a pow 2`]
 664 THEN STRIP_TAC
 665 THEN SUBGOAL_THEN`abs a1= a *cos(angle(v, u, v1:real^3))` ASSUME_TAC;
 666 POP_ASSUM MP_TAC
 667 THEN DISJ_CASES_TAC(REAL_ARITH`&0 <= a1 \/ &0 <=(-- a1)`);
 668 MRESA1_TAC REAL_ABS_REFL`a1:real`
 669 THEN STRIP_TAC
 670 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 671 THEN MATCH_MP_TAC(SET_RULE`angle (v,u,x) = angle (v,u,v1)
 672 ==> a * cos (angle (v,u,x)) = a * cos (angle (v,u,v1:real^3))`)
 673 THEN MRESA_TAC ANGLE_EQ[`v:real^3`;`u:real^3`;`x:real^3`;`v:real^3`;`u:real^3`;`v1:real^3`]
 674 THEN EXPAND_TAC"v1"
 675 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u
 676 =(a1 * inv b) % (x - u)`;NORM_MUL;DOT_RMUL]
 677 THEN ASM_REWRITE_TAC[NORM_MUL;REAL_ARITH`&1*A=A`;REAL_ABS_MUL;REAL_ABS_INV]
 678 THEN REAL_ARITH_TAC;
 679 MRESAL1_TAC REAL_ABS_REFL`--a1:real`[REAL_ABS_NEG]
 680 THEN STRIP_TAC
 681 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`--(A*B)=A*(-- B)`])
 682 THEN MRESAL1_TAC COS_PERIODIC_PI`-- angle(v,u,y1:real^3)`[COS_NEG]
 683 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`--A+B=B-A`])
 684 THEN MATCH_MP_TAC(SET_RULE` angle (v,u,v1) =(pi -angle (v,u,y1) )
 685 ==> a * cos (pi-angle (v,u,y1) ) = a * cos (angle (v,u,v1:real^3))`)
 686 THEN MRESA_TAC (GEN_ALL ANGLE_EQ_PI_LEFT)[`v:real^3`;`v1:real^3`;`u:real^3`;`x:real^3`]
 687 THEN POP_ASSUM MP_TAC
 688 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 689 THEN ASM_REWRITE_TAC[]
 690 THEN STRIP_TAC
 691 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
 692 THEN POP_ASSUM MATCH_MP_TAC
 693 THEN ASM_REWRITE_TAC[ANGLE_BETWEEN;BETWEEN_IN_SEGMENT;IN_SEGMENT]
 694 THEN EXPAND_TAC"v1"
 695 THEN REWRITE_TAC[VECTOR_ARITH`( &1 - u1) % x + u1 % ((a1 * inv b) % (x - u) + u)
 696 = ( &1 -  u1 *( &1-a1 * inv b)) % x + (u1 * ( &1- a1 * inv b)) % u`]
 697 THEN EXISTS_TAC`inv (&1 - a1 * inv b)`
 698 THEN STRIP_TAC;
 699 REWRITE_TAC[REAL_LE_INV_EQ]
 700 THEN MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> &0<= &1- a*b`)
 701 THEN MATCH_MP_TAC REAL_LE_MUL
 702 THEN ASM_REWRITE_TAC[];
 703 STRIP_TAC;
 704 MATCH_MP_TAC REAL_INV_LE_1
 705 THEN MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> &1<= &1- a*b`)
 706 THEN MATCH_MP_TAC REAL_LE_MUL
 707 THEN ASM_REWRITE_TAC[];
 708 SUBGOAL_THEN`~( &1 - a1 * inv b = &0)`ASSUME_TAC;
 709 MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> ~( &1- a*b= &0)`)
 710 THEN MATCH_MP_TAC REAL_LE_MUL
 711 THEN ASM_REWRITE_TAC[];
 712 MRESA1_TAC REAL_MUL_LINV`&1 - a1 * inv b`
 713 THEN VECTOR_ARITH_TAC;
 714 REWRITE_TAC[REAL_ARITH`&2 * a * abs a1 * inv b * b * cos (angle (v,u,v1))
 715 = &2 *  abs a1 * (inv b * b) *( a* cos (angle (v,u,v1)))`]
 716 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
 717 THEN REAL_ARITH_TAC;
 718 POP_ASSUM (fun th-> MP_TAC th
 719 THEN ASM_REWRITE_TAC[]
 720 THEN EXPAND_TAC"v1"
 721 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u=(a1 * inv b) % (x - u) `;NORM_MUL]
 722 THEN ASM_REWRITE_TAC[REAL_ARITH`(abs (a1 * inv b) * b) pow 2= (a1 * inv b * b) pow 2/\ a* &1=a`;REAL_ARITH`A+B=C<=> B=C-A`]
 723 THEN STRIP_TAC
 724 THEN ASSUME_TAC th)
 725 THEN SUBGOAL_THEN`~(w1=y1:real^3)`ASSUME_TAC;
 726 EXPAND_TAC"w1"
 727 THEN REWRITE_TAC[VECTOR_ARITH`(b1 * inv (norm (v1 - v))) % (v1 - v) + y1 = y1<=> (b1 * inv (norm (v1 - v))) % (v1 - v)  = vec 0`;GSYM NORM_EQ_0;NORM_MUL;REAL_ABS_MUL]
 728 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
 729 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
 730 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)`]
 731 THEN MP_TAC(REAL_ARITH`&0< b1==> ~(b1 * &1= &0)`)
 732 THEN RESA_TAC;
 733 SUBGOAL_THEN`(u-x) dot (v1- v:real^3)= &0` ASSUME_TAC;
 734 DISJ_CASES_TAC(SET_RULE`v1=u\/ ~(u=v1:real^3)`);
 735 ASM_REWRITE_TAC[]
 736 THEN POP_ASSUM MP_TAC
 737 THEN EXPAND_TAC"v1"
 738 THEN REWRITE_TAC[VECTOR_ARITH`(a1 * inv b) % (x - u) + u=u<=> (a1 * inv b) % (x - u) = vec 0`;GSYM NORM_EQ_0;NORM_MUL;REAL_ENTIRE;REAL_ABS_MUL]
 739 THEN ASM_REWRITE_TAC[]
 740 THEN MRESA1_TAC REAL_ABS_REFL`inv b:real`
 741 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
 742 THEN RESA_TAC
 743 THEN REWRITE_TAC[REAL_ABS_ZERO]
 744 THEN EXPAND_TAC"a1"
 745 THEN REWRITE_TAC[REAL_ENTIRE;REAL_ABS_MUL]
 746 THEN ASM_REWRITE_TAC[REAL_ARITH`(A+B-C) / &2= &0<=> A+B=C`]
 747 THEN STRIP_TAC
 748 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist;COS_ANGLE]
 749 THEN POP_ASSUM MP_TAC
 750 THEN ONCE_REWRITE_TAC[NORM_SUB]
 751 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`t pow 2 = t pow 2 - &2 * a * b * ((v - u) dot (x - u)) * inv (a * b)<=> a * b * ((v - u) dot (x - u)) * inv (a * b)= &0`;REAL_ENTIRE;]
 752 THEN ASM_REWRITE_TAC[REAL_ENTIRE;REAL_INV_MUL]
 753 THEN STRIP_TAC
 754 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
 755 THEN ASM_REWRITE_TAC[DOT_LNEG;DOT_RNEG;DOT_SYM]
 756 THEN REAL_ARITH_TAC;
 757 POP_ASSUM MP_TAC
 758 THEN POP_ASSUM MP_TAC
 759 THEN POP_ASSUM MP_TAC
 760 THEN REMOVE_ASSUM_TAC
 761 THEN REPEAT STRIP_TAC
 762 THEN MRESAL_TAC LAW_OF_COSINES[`v1:real^3`;`u:real^3`;`v:real^3`][dist;COS_ANGLE]
 763 THEN POP_ASSUM MP_TAC
 764 THEN ONCE_REWRITE_TAC[NORM_SUB]
 765 THEN ASM_REWRITE_TAC[real_div;REAL_INV_MUL;REAL_ARITH`a pow 2 =
 766  a pow 2 -
 767  &2 *
 768  norm (u - v1) *
 769  norm (v - v1) *
 770  ((u - v1) dot (v - v1)) *
 771  inv (norm (v1 - u)) *
 772  inv (norm (v1 - v))
 773 <=> norm (u - v1) *
 774  norm (v - v1) *
 775  ((u - v1) dot (v - v1)) *
 776  inv (norm (v1 - u)) *
 777  inv (norm (v1 - v))= &0`;REAL_ENTIRE]
 778 THEN MP_TAC(REAL_ARITH` &0 < norm (v1 - v)/\ &0< inv (norm (v1 - v))==> ~( norm (v1 - v:real^3)= &0)/\ ~(inv (norm (v1 - v))= &0)`)
 779 THEN RESA_TAC
 780 THEN ONCE_REWRITE_TAC[NORM_SUB]
 781 THEN ASM_REWRITE_TAC[]
 782 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v1:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
 783 THEN ONCE_REWRITE_TAC[NORM_SUB]
 784 THEN MP_TAC(REAL_ARITH` &0< inv (norm (v1 - u:real^3))==>  ~(inv (norm (v1 - u))= &0)`)
 785 THEN RESA_TAC
 786 THEN EXPAND_TAC"v1"
 787 THEN REWRITE_TAC[VECTOR_ARITH`u - ((a1 * inv b) % (x - u) + u)= (a1 * inv b) % (--(x-u)) `;DOT_LMUL]
 788 THEN ASM_REWRITE_TAC[REAL_ENTIRE]
 789 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
 790 THEN RESA_TAC
 791 THEN REMOVE_ASSUM_TAC
 792 THEN REMOVE_ASSUM_TAC
 793 THEN REMOVE_ASSUM_TAC
 794 THEN REMOVE_ASSUM_TAC
 795 THEN REMOVE_ASSUM_TAC
 796 THEN REMOVE_ASSUM_TAC
 797 THEN REMOVE_ASSUM_TAC
 798 THEN REMOVE_ASSUM_TAC
 799 THEN POP_ASSUM MP_TAC
 800 THEN EXPAND_TAC"v1"
 801 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u)-u= (a1 * inv b) % ((x-u)) `;NORM_MUL]
 802 THEN ASM_REWRITE_TAC[REAL_ENTIRE;REAL_ABS_ZERO]
 803 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
 804 THEN RESA_TAC
 805 THEN RESA_TAC
 806 THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`--A = &0<=> A= &0`]
 807 THEN STRIP_TAC
 808 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
 809 THEN ASM_REWRITE_TAC[DOT_LNEG;DOT_RNEG;DOT_SYM]
 810 THEN REAL_ARITH_TAC;
 811 SUBGOAL_THEN`norm(x- w1:real^3)=a`ASSUME_TAC;
 812 MRESAL_TAC DIST_EQ[`x:real^3`;`w1:real^3`;`x:real^3`;`w:real^3`][dist]
 813 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`x:real^3`;`w1:real^3`][dist;COS_ANGLE]
 814 THEN EXPAND_TAC"w1"
 815 THEN REWRITE_TAC[VECTOR_ARITH`(y1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1))=  -- ((b1 * inv (norm (v1 - v))) % (v1 - v)) /\
 816 (((b1 * inv (norm (v1 - v))) % (v1 - v) + y1) - y1)=(b1 * inv (norm (v1 - v))) % (v1 - v) `;NORM_NEG;NORM_MUL;REAL_ABS_MUL]
 817 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
 818 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
 819 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ a* &1=a`;DOT_RMUL;]
 820 THEN EXPAND_TAC"y1"
 821 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - x= &1 / &2 % (u - x) `;NORM_MUL;VECTOR_ARITH`x - &1 / &2 % (u + x)= (-- &1 / &2) % (u - x)`;DOT_LMUL]
 822 THEN ONCE_REWRITE_TAC[NORM_SUB]
 823 THEN ASM_REWRITE_TAC[]
 824 THEN REAL_ARITH_TAC;
 825 SUBGOAL_THEN`norm(u- w1:real^3)=a`ASSUME_TAC;
 826 MRESAL_TAC DIST_EQ[`u:real^3`;`w1:real^3`;`u:real^3`;`w:real^3`][dist]
 827 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`u:real^3`;`w1:real^3`][dist;COS_ANGLE]
 828 THEN EXPAND_TAC"w1"
 829 THEN REWRITE_TAC[VECTOR_ARITH`(y1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1))=  -- ((b1 * inv (norm (v1 - v))) % (v1 - v)) /\
 830 (((b1 * inv (norm (v1 - v))) % (v1 - v) + y1) - y1)=(b1 * inv (norm (v1 - v))) % (v1 - v) `;NORM_NEG;NORM_MUL;REAL_ABS_MUL]
 831 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
 832 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
 833 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ a* &1=a`;DOT_RMUL;]
 834 THEN EXPAND_TAC"y1"
 835 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % (x - u) `;NORM_MUL;VECTOR_ARITH`u - &1 / &2 % (u + x)= (&1 / &2) % (u - x)`;DOT_LMUL]
 836 THEN ASM_REWRITE_TAC[]
 837 THEN REAL_ARITH_TAC;
 838 SUBGOAL_THEN`a1 * inv b<= &1/ &2`ASSUME_TAC;
 839 MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`x:real^3`][REAL_EQ_MUL_LCANCEL]
 840 THEN
 841 MRESA_TAC Trigonometry2.POW2_COND[`a:real`;`t:real`]
 842 THEN MP_TAC(REAL_ARITH`a pow 2 <= t pow 2 ==> (a pow 2 +b pow 2 - t pow 2)/ &2<= b pow 2 / &2`)
 843 THEN RESA_TAC
 844 THEN MRESA_TAC REAL_LE_LMUL[`inv b`;`(a pow 2 +b pow 2 - t pow 2)/ &2`;`b pow 2 / &2`]
 845 THEN MRESAL_TAC REAL_LE_RMUL[`a1:real`;`inv b * b pow 2 / &2`;`inv b`][REAL_ARITH`(inv b * b pow 2 / &2) * inv b= (inv b * b) pow 2 / &2/\ &1 pow 2 = &1`];
 846 EXISTS_TAC`w1:real^3`
 847 THEN EXISTS_TAC`y:real^3`
 848 THEN STRIP_TAC;
 849 ASM_REWRITE_TAC[INTER;IN_ELIM_THM;IN_SEGMENT]
 850 THEN STRIP_TAC;
 851 EXISTS_TAC`norm (v1 - v:real^3) * inv (norm (v1 - v) + b1)`
 852 THEN ASM_REWRITE_TAC[]
 853 THEN STRIP_TAC;
 854 MATCH_MP_TAC REAL_LT_MUL
 855 THEN ASM_REWRITE_TAC[]
 856 THEN MATCH_MP_TAC REAL_LT_INV
 857 THEN MATCH_MP_TAC(REAL_ARITH`&0< A /\ &0< B==> &0< A+B`)
 858 THEN ASM_REWRITE_TAC[];
 859 MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
 860 THEN RESA_TAC
 861 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
 862 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
 863 THEN MRESA_TAC REAL_LT_LMUL[`inv(norm(v1-v:real^3)+b1)`;`norm(v1-v:real^3)`;`norm(v1-v:real^3)+b1`]
 864 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
 865 THEN RESA_TAC;
 866 SUBGOAL_THEN`~(y=v1:real^3)<=> ~(v1= y1)`ASSUME_TAC;
 867 EXPAND_TAC"y"
 868 THEN REWRITE_TAC[VECTOR_ARITH`(&1-a) %u+ a%v= x<=> (&1-a) %(u-x)=  a%(x-v)`]
 869 THEN EXPAND_TAC"w1"
 870 THEN REWRITE_TAC[VECTOR_ARITH`v1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1)
 871 = (v1-y1) - ((b1 * inv (norm (v1 - v))) % (v1 - v))`;]
 872 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A%(B-C)= A%B-A%C`]
 873 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`;REAL_ARITH`(norm (v1 - v) * inv (norm (v1 - v) + b1)) * b1 * inv (norm (v1 - v))
 874 = inv (norm (v1 - v) + b1) * b1 * inv (norm (v1 - v)) *norm (v1 - v) /\ A * &1=A`]
 875 THEN ONCE_REWRITE_TAC[ VECTOR_ARITH` A%B-A%C=A%(B-C)`]
 876 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
 877 THEN RESA_TAC
 878 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
 879 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
 880 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
 881 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
 882  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
 883 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
 884  &1 `];
 885 ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v - v1) =
 886    (norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - y1) -
 887    (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - v)
 888 <=>
 889    (norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - y1) = vec 0`;VECTOR_MUL_EQ_0]
 890 THEN MRESA_TAC REAL_LT_MUL[`norm(v1-v:real^3)`;`inv (norm (v1 - v:real^3) + b1)`]
 891 THEN MP_TAC(REAL_ARITH`
 892 &0< norm (v1 - v) * inv (norm (v1 - v) + b1)
 893 ==>
 894 ~(norm (v1 - v) * inv (norm (v1 - v:real^3) + b1) = &0)`)
 895 THEN RESA_TAC
 896 THEN REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> A=B`];
 897 POP_ASSUM MP_TAC
 898 THEN DISJ_CASES_TAC(SET_RULE`(v1 = y1) \/ ~(v1 = y1:real^3)`);
 899 ASM_REWRITE_TAC[]
 900 THEN RESA_TAC
 901 THEN EXISTS_TAC`&1/ &2`
 902 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1/ &2/\ &1/ &2< &1`;VECTOR_ARITH`(&1 - &1 / &2) % x + &1 / &2 % u= &1/ &2 %(u+x)`];
 903 RESA_TAC
 904 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`y:real^3`;`v1:real^3`][REAL_EQ_MUL_LCANCEL]
 905 THEN EXISTS_TAC`(&1 - norm (v1 - v) * inv (norm (v1 - v:real^3) + b1)) * (&1 / &2 - a1 * inv b) + &1/ &2`
 906 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B/\C<=> C/\A/\B`]
 907 THEN STRIP_TAC;
 908 REWRITE_TAC[VECTOR_ARITH`y= (&1-u) %A+u%B<=> y-A= u%(B-A)`]
 909 THEN EXPAND_TAC"y"
 910 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[VECTOR_ARITH`((&1-u) %A+u%B)-y=  (&1-u) %(A-y)+u%(B-y)`;NORM_MUL]
 911 THEN ASM_REWRITE_TAC[]
 912 THEN EXPAND_TAC"w1"
 913 THEN REWRITE_TAC[VECTOR_ARITH`A%((B+C)-D)=A%B+A%(C-D)/\ A%E%B=(A*E)%B`;REAL_ARITH`(norm (v1 - v) * inv (norm (v1 - v) + b1)) * b1 * inv (norm (v1 - v))
 914 =inv (norm (v1 - v) + b1) * b1 * inv (norm (v1 - v)) *norm (v1 - v) `]
 915 THEN ASM_REWRITE_TAC[REAL_ARITH`a* &1= a`]
 916 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
 917 THEN RESA_TAC
 918 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
 919 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
 920 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
 921 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
 922  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
 923 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
 924  &1 `;];
 925 ASM_REWRITE_TAC[VECTOR_ARITH`A%(v-x)+ A%(y-v)+c= A%(y-x)+c`]
 926 THEN EXPAND_TAC"y1"
 927 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - x= &1/ &2 %(u-x)`]
 928 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - x) +
 929  (norm (v1 - v) * inv (norm (v1 - v) + b1)) % &1 / &2 % (u - x) =
 930  ((&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) * (&1 / &2 - a1 * inv b) + &1 / &2) % (u - x)
 931 <=> (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - &1/ &2 %(x+u)) =
 932  ((&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) * (&1 / &2 - a1 * inv b)) % (u - x)
 933 `]
 934 THEN EXPAND_TAC"v1"
 935 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - &1 / &2 % (x + u)
 936 = (&1/ &2- a1 * inv b) % (u-x) `]
 937 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`];
 938 STRIP_TAC;
 939 MATCH_MP_TAC(REAL_ARITH`&0<=A ==> &0< A+ &1/ &2`)
 940 THEN MATCH_MP_TAC REAL_LE_MUL
 941 THEN ASM_REWRITE_TAC[]
 942 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0<= norm (v1-v) +b1`)
 943 THEN RESA_TAC
 944 THEN MRESA1_TAC REAL_LE_INV`(norm(v1-v:real^3)+b1)`
 945 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
 946 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
 947 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
 948  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
 949 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
 950  &1 `;];
 951 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 952 THEN STRIP_TAC;
 953 MATCH_MP_TAC REAL_LE_MUL
 954 THEN ASM_REWRITE_TAC[];
 955 ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`];
 956 SUBGOAL_THEN`&0< a1 * inv b`ASSUME_TAC;
 957 MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`x:real^3`][REAL_EQ_MUL_LCANCEL]
 958 THEN
 959 MRESA_TAC Trigonometry2.POW2_COND[`t:real`;`b:real`]
 960 THEN MP_TAC(REAL_ARITH`t pow 2 <= b pow 2 /\ &0< a pow 2 ==> &0< (a pow 2 +b pow 2 - t pow 2)/ &2`)
 961 THEN ASM_REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]
 962 THEN STRIP_TAC
 963 THEN MRESA_TAC REAL_LT_MUL[`inv b`;`(a pow 2 +b pow 2 - t pow 2)/ &2`]
 964 THEN MRESA_TAC REAL_LT_MUL[`a1:real`;`inv b`];
 965 MP_TAC(REAL_ARITH`&0< a1 * inv b==>(&1 / &2 - a1 * inv b)< &1/ &2`)
 966 THEN RESA_TAC
 967 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v:real^3)==>b1 < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1 /\ &0<= norm (v1-v) +b1`)
 968 THEN RESA_TAC
 969 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
 970 THEN MRESA1_TAC REAL_LE_INV`(norm(v1-v:real^3)+b1)`
 971 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
 972 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
 973 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
 974  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
 975 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
 976  &1 `;];
 977 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 978 THEN MRESA_TAC REAL_LT_LMUL[`inv (norm (v1 - v:real^3) + b1)`;`b1:real`;`norm (v1 - v:real^3) + b1`]
 979 THEN MRESA_TAC REAL_LE_MUL[`inv (norm (v1 - v:real^3) + b1)`;`b1:real`]
 980 THEN MRESAL_TAC Real_ext.REAL_PROP_LT_LRMUL[`(inv (norm (v1 - v:real^3) + b1) * b1)`;`&1`;`(&1 / &2 - a1 * inv b)`;`&1/ &2`][REAL_ARITH`&0<= A-B<=> B<=A`]
 981 THEN POP_ASSUM MP_TAC
 982 THEN REAL_ARITH_TAC;
 983 ASM_REWRITE_TAC[]]);;
 984
 985
 986
 987
 988
 989
 990
 991
 992
 993
 994 let MAX_IF_COPLANAR1=prove_by_refinement(`!v x:real^3  u w:real^3 a a2 t.
 995  a<= t /\
 996 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
 997 /\ ~(collinear{v,x,u})
 998 /\ ~(collinear{w,x,u})
 999 /\ norm(v-x)=t
1000 /\ norm(v-u)=a
1001 /\ norm(x-w)=a2
1002 /\ norm(u-w)=a2
1003 /\ a2=t
1004 /\ t<= norm(x-u)
1005 ==> ?w1 y.
1006 y IN segment(v,w1) INTER segment (x,u)
1007 /\ norm(x-w1)=a2
1008 /\ norm(u-w1)=a2
1009 /\ ~(v=w1)`,
1010 [REPEAT STRIP_TAC
1011 THEN ABBREV_TAC`b=norm(x-u:real^3)`
1012 THEN ABBREV_TAC`a1= inv(b) * (a pow 2 + b pow 2 -t pow 2)/ &2`
1013 THEN ABBREV_TAC`v1= (a1 * inv(b)) % (x-u:real^3) +u:real^3`
1014 THEN ABBREV_TAC`y1= (&1/ &2) %(u+x:real^3) `
1015 THEN ABBREV_TAC`b1= sqrt(a2 pow 2- (b/ &2) pow 2) `
1016 THEN ABBREV_TAC`w1= (b1* inv(norm(v1- v))) %(v1-v:real^3) +y1`
1017 THEN ABBREV_TAC`y= (&1- norm(v1-v:real^3) * inv(norm(v1-v)+b1)) %v + (norm(v1-v) * inv(norm(v1-v)+b1)) % w1:real^3`
1018 THEN SUBGOAL_THEN`~(y1=x:real^3)` ASSUME_TAC;
1019 EXPAND_TAC"y1"
1020 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) = x<=> x=u`]
1021 THEN ASM_REWRITE_TAC[];
1022 SUBGOAL_THEN`~(y1=u:real^3)` ASSUME_TAC;
1023 EXPAND_TAC"y1"
1024 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) = u<=> x=u`]
1025 THEN ASM_REWRITE_TAC[];
1026 SUBGOAL_THEN`y1 IN segment[u,x:real^3]`ASSUME_TAC;
1027 REWRITE_TAC[IN_SEGMENT]
1028 THEN EXISTS_TAC`&1/ &2`
1029 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1/ &2 /\ &1/ &2<= &1 /\ &1- &1/ &2= &1/ &2`;VECTOR_ARITH`A % x + A % u= A%(x+u)`];
1030 SUBGOAL_THEN`~(y1=w:real^3)` ASSUME_TAC;
1031 STRIP_TAC
1032 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1033 THEN MP_TAC(REAL_ARITH`&0 = &0`)
1034 THEN MRESA_TAC COLLINEAR_SUBSET[`{w,x,u:real^3}`;`segment[u,x:real^3]`]
1035 THEN ASM_REWRITE_TAC[COLLINEAR_SEGMENT]
1036 THEN MRESA_TAC ENDS_IN_SEGMENT[`u:real^3`;`x:real^3`]
1037 THEN POP_ASSUM MP_TAC
1038 THEN POP_ASSUM MP_TAC
1039 THEN POP_ASSUM MP_TAC
1040 THEN SET_TAC[];
1041 SUBGOAL_THEN`&0<=a2 pow 2 - (b / &2) pow 2` ASSUME_TAC;
1042 MRESAL_TAC CONGRUENT_TRIANGLES_SSS[`w:real^3`;`y1:real^3`;`u:real^3`;`w:real^3`;`y1:real^3`;`x:real^3`][dist]
1043 THEN POP_ASSUM MP_TAC
1044 THEN EXPAND_TAC"y1"
1045 THEN REWRITE_TAC[VECTOR_ARITH`(&1 / &2) % (u + x) - u = &1 / &2 % (x - u) /\ (&1 / &2) % (u + x) - x = (&1 / &2) % (u -x) `;NORM_MUL;]
1046 THEN SIMP_TAC[NORM_SUB]
1047 THEN ASM_REWRITE_TAC[]
1048 THEN STRIP_TAC
1049 THEN MRESAL_TAC ANGLES_ALONG_LINE[`u:real^3`;`x:real^3`;`y1:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT]
1050 THEN POP_ASSUM MP_TAC
1051 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1052 THEN ASM_REWRITE_TAC[REAL_ARITH`A+A= B <=> A= B/ &2`]
1053 THEN STRIP_TAC
1054 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`w:real^3`;`u:real^3`][dist]
1055 THEN POP_ASSUM MP_TAC
1056 THEN ONCE_REWRITE_TAC[NORM_SUB]
1057 THEN ASM_REWRITE_TAC[COS_PI2; REAL_ARITH`A * &0= &0/\ A- &0= A`]
1058 THEN EXPAND_TAC"y1"
1059 THEN REWRITE_TAC[VECTOR_ARITH`u - &1 / &2 % (u + x)= &1 / &2 % (u - x)`;NORM_MUL;REAL_ARITH`abs(&1/ &2)= &1/ &2`]
1060 THEN ASM_REWRITE_TAC[]
1061 THEN ONCE_REWRITE_TAC[NORM_SUB]
1062 THEN ASM_REWRITE_TAC[REAL_ARITH`&1/ &2 *A=A/ &2`]
1063 THEN RESA_TAC
1064 THEN REWRITE_TAC[REAL_ARITH`(A+B)-B=A`;REAL_LE_POW_2];
1065 SUBGOAL_THEN`&0< a2 pow 2 - (b / &2) pow 2` ASSUME_TAC;
1066 MRESAL_TAC CONGRUENT_TRIANGLES_SSS[`w:real^3`;`y1:real^3`;`u:real^3`;`w:real^3`;`y1:real^3`;`x:real^3`][dist]
1067 THEN POP_ASSUM MP_TAC
1068 THEN EXPAND_TAC"y1"
1069 THEN REWRITE_TAC[VECTOR_ARITH`(&1 / &2) % (u + x) - u = &1 / &2 % (x - u) /\ (&1 / &2) % (u + x) - x = (&1 / &2) % (u -x) `;NORM_MUL;]
1070 THEN SIMP_TAC[NORM_SUB]
1071 THEN ASM_REWRITE_TAC[]
1072 THEN STRIP_TAC
1073 THEN MRESAL_TAC ANGLES_ALONG_LINE[`u:real^3`;`x:real^3`;`y1:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT]
1074 THEN POP_ASSUM MP_TAC
1075 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1076 THEN ASM_REWRITE_TAC[REAL_ARITH`A+A= B <=> A= B/ &2`]
1077 THEN STRIP_TAC
1078 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`w:real^3`;`u:real^3`][dist]
1079 THEN POP_ASSUM MP_TAC
1080 THEN ONCE_REWRITE_TAC[NORM_SUB]
1081 THEN ASM_REWRITE_TAC[COS_PI2; REAL_ARITH`A * &0= &0/\ A- &0= A`]
1082 THEN EXPAND_TAC"y1"
1083 THEN REWRITE_TAC[VECTOR_ARITH`u - &1 / &2 % (u + x)= &1 / &2 % (u - x)`;NORM_MUL;REAL_ARITH`abs(&1/ &2)= &1/ &2`]
1084 THEN ASM_REWRITE_TAC[]
1085 THEN ONCE_REWRITE_TAC[NORM_SUB]
1086 THEN ASM_REWRITE_TAC[REAL_ARITH`&1/ &2 *A=A/ &2`]
1087 THEN RESA_TAC
1088 THEN REWRITE_TAC[REAL_ARITH`(A+B)-B=A`;REAL_LE_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]
1089 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`y1:real^3`;`w:real^3`][REAL_EQ_MUL_LCANCEL];
1090 MRESA1_TAC SQRT_WORKS`a2 pow 2 - (b / &2) pow 2`
1091 THEN
1092 MRESA1_TAC SQRT_POS_LT`a2 pow 2 - (b / &2) pow 2`
1093 THEN SUBGOAL_THEN`&0<= b1 * inv (norm(v1- v:real^3))`ASSUME_TAC;
1094 MATCH_MP_TAC REAL_LE_MUL
1095 THEN ASM_REWRITE_TAC[]
1096 THEN MATCH_MP_TAC REAL_LE_INV
1097 THEN REWRITE_TAC[NORM_POS_LE];
1098 MRESAL_TAC Planarity.IMP_NORM_FAN[`x:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
1099 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
1100 THEN SUBGOAL_THEN`~(v1=v:real^3)` ASSUME_TAC;
1101 EXPAND_TAC"v1"
1102 THEN REWRITE_TAC[VECTOR_ARITH`(a1 * inv b) % (x-u) + u = v<=> (a1 * inv b) % ( x-u) = v-u`]
1103 THEN STRIP_TAC
1104 THEN MP_TAC(SET_RULE`(a1 * inv b) % (x-u) = v - u:real^3
1105 ==>  norm((a1 * inv b) % ( x-u)) = norm( v - u)`)
1106 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1107 THEN ASM_REWRITE_TAC[NORM_MUL]
1108 THEN ONCE_REWRITE_TAC[NORM_SUB]
1109 THEN ASM_REWRITE_TAC[REAL_ARITH`(a*b)*c= a*(b*c)`;REAL_ABS_MUL]
1110 THEN MRESAL1_TAC REAL_ABS_REFL`inv b:real`[REAL_ARITH`A* &1=A`]
1111 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
1112 THEN POP_ASSUM MP_TAC
1113 THEN ONCE_REWRITE_TAC[NORM_SUB]
1114 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,x))<=>  a pow 2 + b pow 2 -t pow 2= &2 * a * b * cos (angle (v,u,x)) `]
1115 THEN STRIP_TAC
1116 THEN EXPAND_TAC"a1"
1117 THEN POP_ASSUM(fun th-> REWRITE_TAC[th;REAL_ABS_MUL;REAL_ARITH`(&2*A)/ &2=A`])
1118 THEN ASM_REWRITE_TAC[REAL_ABS_MUL]
1119 THEN MRESAL1_TAC REAL_ABS_REFL`b:real`[REAL_ARITH`A* &1=A`]
1120 THEN MRESAL1_TAC REAL_ABS_REFL`a:real`[REAL_ARITH`A* &1=A`]
1121 THEN ASM_REWRITE_TAC[REAL_ARITH`A *B* C*D=(A*C) *B*D /\ &1*A=A`]
1122 THEN STRIP_TAC
1123 THEN MP_TAC(SET_RULE`a * abs (cos (angle (v,u,x:real^3))) = a
1124 ==> inv(a) * (a * abs (cos (angle (v,u,x)))) = inv a * a`)
1125 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1126 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(A*B)*C/\ &1 *A =A`]
1127 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= cos (angle (v,u,x:real^3)) \/ &0<= -- cos (angle (v,u,x))`);
1128 MRESAL1_TAC REAL_ABS_REFL`cos (angle (v,u,x:real^3))`[REAL_ARITH`A* &1=A`]
1129 THEN STRIP_TAC
1130 THEN ASSUME_TAC(PI_WORKS)
1131 THEN MP_TAC(REAL_ARITH`&0< pi==> &0<= pi`)
1132 THEN RESA_TAC
1133 THEN MRESAL_TAC COS_INJ_PI[`angle (v,u,x:real^3)`;`&0`][COS_0;ANGLE_RANGE;REAL_ARITH`&0<= &0`]
1134 THEN MRESA_TAC COLLINEAR_ANGLE[`v:real^3`;`u:real^3`;`x:real^3`]
1135 THEN POP_ASSUM MP_TAC
1136 THEN REWRITE_TAC[]
1137 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1138 THEN RESA_TAC;
1139 MRESAL1_TAC REAL_ABS_REFL`-- cos (angle (v,u,x:real^3))`[REAL_ARITH`--A=  &1<=> A= -- &1`;REAL_ABS_NEG]
1140 THEN STRIP_TAC
1141 THEN ASSUME_TAC(PI_WORKS)
1142 THEN MP_TAC(REAL_ARITH`&0< pi==> &0<= pi`)
1143 THEN RESA_TAC
1144 THEN MRESAL_TAC COS_INJ_PI[`angle (v,u,x:real^3)`;`pi`][COS_PI;ANGLE_RANGE;REAL_ARITH`pi<= pi`]
1145 THEN MRESA_TAC COLLINEAR_ANGLE[`v:real^3`;`u:real^3`;`x:real^3`]
1146 THEN POP_ASSUM MP_TAC
1147 THEN REWRITE_TAC[]
1148 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1149 THEN RESA_TAC;
1150 MRESAL_TAC Planarity.IMP_NORM_FAN[`v1:real^3`;`v:real^3`][REAL_EQ_MUL_LCANCEL]
1151 THEN SUBGOAL_THEN`angle(v,u,x)= angle(v,u,y1:real^3)`ASSUME_TAC;
1152 MRESA_TAC ANGLE_EQ[`v:real^3`;`u:real^3`;`x:real^3`;`v:real^3`;`u:real^3`;`y1:real^3`]
1153 THEN EXPAND_TAC"y1"
1154 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % ( x - u)`;NORM_MUL;REAL_ARITH`abs(&1/ &2) *A=A/ &2`;REAL_ARITH`(A+B)- &2 * C= A-B<=> B=C`;DOT_RMUL]
1155 THEN REAL_ARITH_TAC;
1156 SUBGOAL_THEN`~(v=w1:real^3)` ASSUME_TAC;
1157 EXPAND_TAC"w1"
1158 THEN REWRITE_TAC[VECTOR_ARITH`v = (b1 * inv (norm (v1 - v))) % (v1 - v) + y1
1159 <=> v- y1 = (b1 * inv (norm (v1 - v))) % (v1 - v) `]
1160 THEN STRIP_TAC
1161 THEN MP_TAC(SET_RULE`v - y1 = (b1 * inv (norm (v1 - v))) % (v1 - v):real^3
1162 ==> norm(v - y1) = norm( (b1 * inv (norm (v1 - v))) % (v1 - v))`)
1163 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC (SYM th))
1164 THEN REWRITE_TAC[NORM_MUL]
1165 THEN MRESA1_TAC REAL_ABS_REFL`b1 * inv (norm(v1- v:real^3))`
1166 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ A* &1= A`]
1167 THEN STRIP_TAC
1168 THEN MP_TAC(SET_RULE`norm (v - y1:real^3) = b1
1169 ==> norm (v - y1) pow 2= b1 pow 2`)
1170 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC (SYM th))
1171 THEN ASM_REWRITE_TAC[]
1172 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`y1:real^3`][dist]
1173 THEN ONCE_REWRITE_TAC[NORM_SUB]
1174 THEN ASM_REWRITE_TAC[]
1175 THEN EXPAND_TAC"y1"
1176 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % ( x - u)`;NORM_MUL;REAL_ARITH`abs(&1/ &2) *A=A/ &2`;REAL_ARITH`(A+B)- &2 * C= A-B<=> B=C`]
1177 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
1178 THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th] THEN MP_TAC th)
1179 THEN ONCE_REWRITE_TAC[NORM_SUB]
1180 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,y1))
1181 <=>  a * b / &2* cos (angle (v,u,y1))= (a pow 2 + b pow 2- t pow 2  )/ &4`]
1182 THEN RESA_TAC
1183 THEN REWRITE_TAC[REAL_ARITH`(a pow 2 + (b / &2) pow 2) - &2 * (a pow 2 + b pow 2 - t pow 2) / &4=t pow 2 - (b / &2) pow 2 <=> a pow 2 = t pow 2`]
1184 THEN STRIP_TAC
1185 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1186 THEN ASM_TAC
1187 THEN REWRITE_TAC[REAL_ARITH`A+B-A=B`]
1188 THEN REPEAT STRIP_TAC
1189 THEN MP_TAC(REAL_ARITH`inv b * b pow 2 / &2 = (inv b * b) * b / &2`)
1190 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *A=A`]
1191 THEN STRIP_TAC
1192 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1193 THEN MP_TAC(VECTOR_ARITH`(b / &2 * inv b) % (x-u) + u= (inv b *b )/ &2 % (x-u) + u:real^3`)
1194 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (x-u) + u= &1/ &2 %(u+x)`]
1195 THEN STRIP_TAC
1196 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1197 THEN REMOVE_ASSUM_TAC
1198 THEN REMOVE_ASSUM_TAC
1199 THEN POP_ASSUM MP_TAC
1200 THEN REWRITE_TAC[]
1201 THEN ONCE_REWRITE_TAC[NORM_SUB]
1202 THEN STRIP_TAC
1203 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1204 THEN REMOVE_ASSUM_TAC
1205 THEN POP_ASSUM MP_TAC
1206 THEN REWRITE_TAC[]
1207 THEN ONCE_REWRITE_TAC[REAL_ARITH`norm (y1 - v) * inv (norm (y1 - v)) =  inv (norm (y1 - v))* norm (y1 - v) `]
1208 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 % (y1 - v) = v - y1<=> y1=v`];
1209 SUBGOAL_THEN`norm(v1-u:real^3) pow 2+ norm(v1- v) pow 2= norm(v-u:real^3) pow 2`ASSUME_TAC;
1210 DISJ_CASES_TAC(SET_RULE`v1=u \/ ~(v1=u:real^3)`);
1211 ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0 pow 2+A= A`]
1212 THEN ONCE_REWRITE_TAC[NORM_SUB]
1213 THEN ASM_REWRITE_TAC[];
1214 MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`v1:real^3`][dist]
1215 THEN ONCE_REWRITE_TAC[NORM_SUB]
1216 THEN ASM_REWRITE_TAC[]
1217 THEN ONCE_REWRITE_TAC[NORM_SUB]
1218 THEN EXPAND_TAC"v1"
1219 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u= (a1 * inv b) % (x - u) `]
1220 THEN ASM_REWRITE_TAC[]
1221 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist]
1222 THEN POP_ASSUM MP_TAC
1223 THEN ONCE_REWRITE_TAC[NORM_SUB]
1224 THEN ASM_REWRITE_TAC[REAL_ARITH`t pow 2 = (a pow 2 + b pow 2) - &2 * a * b * cos (angle (v,u,y1))
1225 <=> a * b * cos (angle (v,u,y1))= (a pow 2 + b pow 2- t pow 2) / &2 `]
1226 THEN STRIP_TAC
1227 THEN MP_TAC(SET_RULE`a * b * cos (angle (v,u,y1:real^3))= (a pow 2 + b pow 2- t pow 2) / &2
1228 ==> inv b*(a * b * cos (angle (v,u,y1)))= inv b*((a pow 2 + b pow 2- t pow 2) / &2 )`)
1229 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
1230 THEN REWRITE_TAC[REAL_ARITH`inv b * a * b * cos (angle (v,u,y1))= (inv b * b) * a * cos (angle (v,u,y1))`]
1231 THEN ASM_REWRITE_TAC[NORM_MUL;REAL_ARITH`&1*A=A`;REAL_ABS_MUL;REAL_ABS_INV]
1232 THEN MRESA1_TAC REAL_ABS_NORM`x-u:real^3`
1233 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &1=A /\ (A*B)*C=A*(B*C)/\ abs a pow 2= a pow 2`]
1234 THEN STRIP_TAC
1235 THEN SUBGOAL_THEN`abs a1= a *cos(angle(v, u, v1:real^3))` ASSUME_TAC;
1236 POP_ASSUM MP_TAC
1237 THEN DISJ_CASES_TAC(REAL_ARITH`&0 <= a1 \/ &0 <=(-- a1)`);
1238 MRESA1_TAC REAL_ABS_REFL`a1:real`
1239 THEN STRIP_TAC
1240 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1241 THEN MATCH_MP_TAC(SET_RULE`angle (v,u,x) = angle (v,u,v1)
1242 ==> a * cos (angle (v,u,x)) = a * cos (angle (v,u,v1:real^3))`)
1243 THEN MRESA_TAC ANGLE_EQ[`v:real^3`;`u:real^3`;`x:real^3`;`v:real^3`;`u:real^3`;`v1:real^3`]
1244 THEN EXPAND_TAC"v1"
1245 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u
1246 =(a1 * inv b) % (x - u)`;NORM_MUL;DOT_RMUL]
1247 THEN ASM_REWRITE_TAC[NORM_MUL;REAL_ARITH`&1*A=A`;REAL_ABS_MUL;REAL_ABS_INV]
1248 THEN REAL_ARITH_TAC;
1249 MRESAL1_TAC REAL_ABS_REFL`--a1:real`[REAL_ABS_NEG]
1250 THEN STRIP_TAC
1251 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`--(A*B)=A*(-- B)`])
1252 THEN MRESAL1_TAC COS_PERIODIC_PI`-- angle(v,u,y1:real^3)`[COS_NEG]
1253 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`--A+B=B-A`])
1254 THEN MATCH_MP_TAC(SET_RULE` angle (v,u,v1) =(pi -angle (v,u,y1) )
1255 ==> a * cos (pi-angle (v,u,y1) ) = a * cos (angle (v,u,v1:real^3))`)
1256 THEN MRESA_TAC (GEN_ALL ANGLE_EQ_PI_LEFT)[`v:real^3`;`v1:real^3`;`u:real^3`;`x:real^3`]
1257 THEN POP_ASSUM MP_TAC
1258 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1259 THEN ASM_REWRITE_TAC[]
1260 THEN STRIP_TAC
1261 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1262 THEN POP_ASSUM MATCH_MP_TAC
1263 THEN ASM_REWRITE_TAC[ANGLE_BETWEEN;BETWEEN_IN_SEGMENT;IN_SEGMENT]
1264 THEN EXPAND_TAC"v1"
1265 THEN REWRITE_TAC[VECTOR_ARITH`( &1 - u1) % x + u1 % ((a1 * inv b) % (x - u) + u)
1266 = ( &1 -  u1 *( &1-a1 * inv b)) % x + (u1 * ( &1- a1 * inv b)) % u`]
1267 THEN EXISTS_TAC`inv (&1 - a1 * inv b)`
1268 THEN STRIP_TAC;
1269 REWRITE_TAC[REAL_LE_INV_EQ]
1270 THEN MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> &0<= &1- a*b`)
1271 THEN MATCH_MP_TAC REAL_LE_MUL
1272 THEN ASM_REWRITE_TAC[];
1273 STRIP_TAC;
1274 MATCH_MP_TAC REAL_INV_LE_1
1275 THEN MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> &1<= &1- a*b`)
1276 THEN MATCH_MP_TAC REAL_LE_MUL
1277 THEN ASM_REWRITE_TAC[];
1278 SUBGOAL_THEN`~( &1 - a1 * inv b = &0)`ASSUME_TAC;
1279 MATCH_MP_TAC(REAL_ARITH`&0<= (-- a) *b ==> ~( &1- a*b= &0)`)
1280 THEN MATCH_MP_TAC REAL_LE_MUL
1281 THEN ASM_REWRITE_TAC[];
1282 MRESA1_TAC REAL_MUL_LINV`&1 - a1 * inv b`
1283 THEN VECTOR_ARITH_TAC;
1284 REWRITE_TAC[REAL_ARITH`&2 * a * abs a1 * inv b * b * cos (angle (v,u,v1))
1285 = &2 *  abs a1 * (inv b * b) *( a* cos (angle (v,u,v1)))`]
1286 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1287 THEN REAL_ARITH_TAC;
1288 POP_ASSUM (fun th-> MP_TAC th
1289 THEN ASM_REWRITE_TAC[]
1290 THEN EXPAND_TAC"v1"
1291 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - u=(a1 * inv b) % (x - u) `;NORM_MUL]
1292 THEN ASM_REWRITE_TAC[REAL_ARITH`(abs (a1 * inv b) * b) pow 2= (a1 * inv b * b) pow 2/\ a* &1=a`;REAL_ARITH`A+B=C<=> B=C-A`]
1293 THEN STRIP_TAC
1294 THEN ASSUME_TAC th)
1295 THEN SUBGOAL_THEN`~(w1=y1:real^3)`ASSUME_TAC;
1296 EXPAND_TAC"w1"
1297 THEN REWRITE_TAC[VECTOR_ARITH`(b1 * inv (norm (v1 - v))) % (v1 - v) + y1 = y1<=> (b1 * inv (norm (v1 - v))) % (v1 - v)  = vec 0`;GSYM NORM_EQ_0;NORM_MUL;REAL_ABS_MUL]
1298 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
1299 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
1300 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)`]
1301 THEN MP_TAC(REAL_ARITH`&0< b1==> ~(b1 * &1= &0)`)
1302 THEN RESA_TAC;
1303 SUBGOAL_THEN`(u-x) dot (v1- v:real^3)= &0` ASSUME_TAC;
1304 DISJ_CASES_TAC(SET_RULE`v1=u\/ ~(u=v1:real^3)`);
1305 ASM_REWRITE_TAC[]
1306 THEN POP_ASSUM MP_TAC
1307 THEN EXPAND_TAC"v1"
1308 THEN REWRITE_TAC[VECTOR_ARITH`(a1 * inv b) % (x - u) + u=u<=> (a1 * inv b) % (x - u) = vec 0`;GSYM NORM_EQ_0;NORM_MUL;REAL_ENTIRE;REAL_ABS_MUL]
1309 THEN ASM_REWRITE_TAC[]
1310 THEN MRESA1_TAC REAL_ABS_REFL`inv b:real`
1311 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
1312 THEN RESA_TAC
1313 THEN REWRITE_TAC[REAL_ABS_ZERO]
1314 THEN EXPAND_TAC"a1"
1315 THEN REWRITE_TAC[REAL_ENTIRE;REAL_ABS_MUL]
1316 THEN ASM_REWRITE_TAC[REAL_ARITH`(A+B-C) / &2= &0<=> A+B=C`]
1317 THEN STRIP_TAC
1318 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`x:real^3`][dist;COS_ANGLE]
1319 THEN POP_ASSUM MP_TAC
1320 THEN ONCE_REWRITE_TAC[NORM_SUB]
1321 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`t pow 2 = t pow 2 - &2 * a * b * ((v - u) dot (x - u)) * inv (a * b)<=> a * b * ((v - u) dot (x - u)) * inv (a * b)= &0`;REAL_ENTIRE;]
1322 THEN ASM_REWRITE_TAC[REAL_ENTIRE;REAL_INV_MUL]
1323 THEN STRIP_TAC
1324 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1325 THEN ASM_REWRITE_TAC[DOT_LNEG;DOT_RNEG;DOT_SYM]
1326 THEN REAL_ARITH_TAC;
1327 POP_ASSUM MP_TAC
1328 THEN POP_ASSUM MP_TAC
1329 THEN POP_ASSUM MP_TAC
1330 THEN REMOVE_ASSUM_TAC
1331 THEN REPEAT STRIP_TAC
1332 THEN MRESAL_TAC LAW_OF_COSINES[`v1:real^3`;`u:real^3`;`v:real^3`][dist;COS_ANGLE]
1333 THEN POP_ASSUM MP_TAC
1334 THEN ONCE_REWRITE_TAC[NORM_SUB]
1335 THEN ASM_REWRITE_TAC[real_div;REAL_INV_MUL;REAL_ARITH`a pow 2 =
1336  a pow 2 -
1337  &2 *
1338  norm (u - v1) *
1339  norm (v - v1) *
1340  ((u - v1) dot (v - v1)) *
1341  inv (norm (v1 - u)) *
1342  inv (norm (v1 - v))
1343 <=> norm (u - v1) *
1344  norm (v - v1) *
1345  ((u - v1) dot (v - v1)) *
1346  inv (norm (v1 - u)) *
1347  inv (norm (v1 - v))= &0`;REAL_ENTIRE]
1348 THEN MP_TAC(REAL_ARITH` &0 < norm (v1 - v)/\ &0< inv (norm (v1 - v))==> ~( norm (v1 - v:real^3)= &0)/\ ~(inv (norm (v1 - v))= &0)`)
1349 THEN RESA_TAC
1350 THEN ONCE_REWRITE_TAC[NORM_SUB]
1351 THEN ASM_REWRITE_TAC[]
1352 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v1:real^3`;`u:real^3`][REAL_EQ_MUL_LCANCEL]
1353 THEN ONCE_REWRITE_TAC[NORM_SUB]
1354 THEN MP_TAC(REAL_ARITH` &0< inv (norm (v1 - u:real^3))==>  ~(inv (norm (v1 - u))= &0)`)
1355 THEN RESA_TAC
1356 THEN EXPAND_TAC"v1"
1357 THEN REWRITE_TAC[VECTOR_ARITH`u - ((a1 * inv b) % (x - u) + u)= (a1 * inv b) % (--(x-u)) `;DOT_LMUL]
1358 THEN ASM_REWRITE_TAC[REAL_ENTIRE]
1359 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
1360 THEN RESA_TAC
1361 THEN REMOVE_ASSUM_TAC
1362 THEN REMOVE_ASSUM_TAC
1363 THEN REMOVE_ASSUM_TAC
1364 THEN REMOVE_ASSUM_TAC
1365 THEN REMOVE_ASSUM_TAC
1366 THEN REMOVE_ASSUM_TAC
1367 THEN REMOVE_ASSUM_TAC
1368 THEN REMOVE_ASSUM_TAC
1369 THEN POP_ASSUM MP_TAC
1370 THEN EXPAND_TAC"v1"
1371 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u)-u= (a1 * inv b) % ((x-u)) `;NORM_MUL]
1372 THEN ASM_REWRITE_TAC[REAL_ENTIRE;REAL_ABS_ZERO]
1373 THEN MP_TAC(REAL_ARITH`&0 < inv b /\ &0< inv a==> ~(inv b= &0)/\ ~(inv a= &0)`)
1374 THEN RESA_TAC
1375 THEN RESA_TAC
1376 THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`--A = &0<=> A= &0`]
1377 THEN STRIP_TAC
1378 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1379 THEN ASM_REWRITE_TAC[DOT_LNEG;DOT_RNEG;DOT_SYM]
1380 THEN REAL_ARITH_TAC;
1381 SUBGOAL_THEN`norm(x- w1:real^3)=a2`ASSUME_TAC;
1382 MRESAL_TAC DIST_EQ[`x:real^3`;`w1:real^3`;`x:real^3`;`w:real^3`][dist]
1383 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`x:real^3`;`w1:real^3`][dist;COS_ANGLE]
1384 THEN EXPAND_TAC"w1"
1385 THEN REWRITE_TAC[VECTOR_ARITH`(y1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1))=  -- ((b1 * inv (norm (v1 - v))) % (v1 - v)) /\
1386 (((b1 * inv (norm (v1 - v))) % (v1 - v) + y1) - y1)=(b1 * inv (norm (v1 - v))) % (v1 - v) `;NORM_NEG;NORM_MUL;REAL_ABS_MUL]
1387 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
1388 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
1389 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ a* &1=a`;DOT_RMUL;]
1390 THEN EXPAND_TAC"y1"
1391 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - x= &1 / &2 % (u - x) `;NORM_MUL;VECTOR_ARITH`x - &1 / &2 % (u + x)= (-- &1 / &2) % (u - x)`;DOT_LMUL]
1392 THEN ONCE_REWRITE_TAC[NORM_SUB]
1393 THEN ASM_REWRITE_TAC[]
1394 THEN REAL_ARITH_TAC;
1395 SUBGOAL_THEN`norm(u- w1:real^3)=a2`ASSUME_TAC;
1396 MRESAL_TAC DIST_EQ[`u:real^3`;`w1:real^3`;`u:real^3`;`w:real^3`][dist]
1397 THEN MRESAL_TAC LAW_OF_COSINES[`y1:real^3`;`u:real^3`;`w1:real^3`][dist;COS_ANGLE]
1398 THEN EXPAND_TAC"w1"
1399 THEN REWRITE_TAC[VECTOR_ARITH`(y1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1))=  -- ((b1 * inv (norm (v1 - v))) % (v1 - v)) /\
1400 (((b1 * inv (norm (v1 - v))) % (v1 - v) + y1) - y1)=(b1 * inv (norm (v1 - v))) % (v1 - v) `;NORM_NEG;NORM_MUL;REAL_ABS_MUL]
1401 THEN MRESA1_TAC REAL_ABS_REFL`b1:real`
1402 THEN MRESA1_TAC REAL_ABS_REFL`inv (norm (v1 - v:real^3)):real`
1403 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ a* &1=a`;DOT_RMUL;]
1404 THEN EXPAND_TAC"y1"
1405 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - u= &1 / &2 % (x - u) `;NORM_MUL;VECTOR_ARITH`u - &1 / &2 % (u + x)= (&1 / &2) % (u - x)`;DOT_LMUL]
1406 THEN ASM_REWRITE_TAC[]
1407 THEN REAL_ARITH_TAC;
1408 SUBGOAL_THEN`a1 * inv b<= &1/ &2`ASSUME_TAC;
1409 MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`x:real^3`][REAL_EQ_MUL_LCANCEL]
1410 THEN
1411 MRESA_TAC Trigonometry2.POW2_COND[`a:real`;`t:real`]
1412 THEN MP_TAC(REAL_ARITH`a pow 2 <= t pow 2 ==> (a pow 2 +b pow 2 - t pow 2)/ &2<= b pow 2 / &2`)
1413 THEN RESA_TAC
1414 THEN MRESA_TAC REAL_LE_LMUL[`inv b`;`(a pow 2 +b pow 2 - t pow 2)/ &2`;`b pow 2 / &2`]
1415 THEN MRESAL_TAC REAL_LE_RMUL[`a1:real`;`inv b * b pow 2 / &2`;`inv b`][REAL_ARITH`(inv b * b pow 2 / &2) * inv b= (inv b * b) pow 2 / &2/\ &1 pow 2 = &1`];
1416 EXISTS_TAC`w1:real^3`
1417 THEN EXISTS_TAC`y:real^3`
1418 THEN STRIP_TAC;
1419 ASM_REWRITE_TAC[INTER;IN_ELIM_THM;IN_SEGMENT]
1420 THEN STRIP_TAC;
1421 EXISTS_TAC`norm (v1 - v:real^3) * inv (norm (v1 - v) + b1)`
1422 THEN ASM_REWRITE_TAC[]
1423 THEN STRIP_TAC;
1424 MATCH_MP_TAC REAL_LT_MUL
1425 THEN ASM_REWRITE_TAC[]
1426 THEN MATCH_MP_TAC REAL_LT_INV
1427 THEN MATCH_MP_TAC(REAL_ARITH`&0< A /\ &0< B==> &0< A+B`)
1428 THEN ASM_REWRITE_TAC[];
1429 MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
1430 THEN RESA_TAC
1431 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
1432 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
1433 THEN MRESA_TAC REAL_LT_LMUL[`inv(norm(v1-v:real^3)+b1)`;`norm(v1-v:real^3)`;`norm(v1-v:real^3)+b1`]
1434 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1435 THEN RESA_TAC;
1436 SUBGOAL_THEN`~(y=v1:real^3)<=> ~(v1= y1)`ASSUME_TAC;
1437 EXPAND_TAC"y"
1438 THEN REWRITE_TAC[VECTOR_ARITH`(&1-a) %u+ a%v= x<=> (&1-a) %(u-x)=  a%(x-v)`]
1439 THEN EXPAND_TAC"w1"
1440 THEN REWRITE_TAC[VECTOR_ARITH`v1 - ((b1 * inv (norm (v1 - v))) % (v1 - v) + y1)
1441 = (v1-y1) - ((b1 * inv (norm (v1 - v))) % (v1 - v))`;]
1442 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A%(B-C)= A%B-A%C`]
1443 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`;REAL_ARITH`(norm (v1 - v) * inv (norm (v1 - v) + b1)) * b1 * inv (norm (v1 - v))
1444 = inv (norm (v1 - v) + b1) * b1 * inv (norm (v1 - v)) *norm (v1 - v) /\ A * &1=A`]
1445 THEN ONCE_REWRITE_TAC[ VECTOR_ARITH` A%B-A%C=A%(B-C)`]
1446 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
1447 THEN RESA_TAC
1448 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
1449 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
1450 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
1451 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
1452  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
1453 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
1454  &1 `];
1455 ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v - v1) =
1456    (norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - y1) -
1457    (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - v)
1458 <=>
1459    (norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - y1) = vec 0`;VECTOR_MUL_EQ_0]
1460 THEN MRESA_TAC REAL_LT_MUL[`norm(v1-v:real^3)`;`inv (norm (v1 - v:real^3) + b1)`]
1461 THEN MP_TAC(REAL_ARITH`
1462 &0< norm (v1 - v) * inv (norm (v1 - v) + b1)
1463 ==>
1464 ~(norm (v1 - v) * inv (norm (v1 - v:real^3) + b1) = &0)`)
1465 THEN RESA_TAC
1466 THEN REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> A=B`];
1467 POP_ASSUM MP_TAC
1468 THEN DISJ_CASES_TAC(SET_RULE`(v1 = y1) \/ ~(v1 = y1:real^3)`);
1469 ASM_REWRITE_TAC[]
1470 THEN RESA_TAC
1471 THEN EXISTS_TAC`&1/ &2`
1472 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1/ &2/\ &1/ &2< &1`;VECTOR_ARITH`(&1 - &1 / &2) % x + &1 / &2 % u= &1/ &2 %(u+x)`];
1473 RESA_TAC
1474 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`y:real^3`;`v1:real^3`][REAL_EQ_MUL_LCANCEL]
1475 THEN EXISTS_TAC`(&1 - norm (v1 - v) * inv (norm (v1 - v:real^3) + b1)) * (&1 / &2 - a1 * inv b) + &1/ &2`
1476 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B/\C<=> C/\A/\B`]
1477 THEN STRIP_TAC;
1478 REWRITE_TAC[VECTOR_ARITH`y= (&1-u) %A+u%B<=> y-A= u%(B-A)`]
1479 THEN EXPAND_TAC"y"
1480 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[VECTOR_ARITH`((&1-u) %A+u%B)-y=  (&1-u) %(A-y)+u%(B-y)`;NORM_MUL]
1481 THEN ASM_REWRITE_TAC[]
1482 THEN EXPAND_TAC"w1"
1483 THEN REWRITE_TAC[VECTOR_ARITH`A%((B+C)-D)=A%B+A%(C-D)/\ A%E%B=(A*E)%B`;REAL_ARITH`(norm (v1 - v) * inv (norm (v1 - v) + b1)) * b1 * inv (norm (v1 - v))
1484 =inv (norm (v1 - v) + b1) * b1 * inv (norm (v1 - v)) *norm (v1 - v) `]
1485 THEN ASM_REWRITE_TAC[REAL_ARITH`a* &1= a`]
1486 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1`)
1487 THEN RESA_TAC
1488 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
1489 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
1490 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
1491 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
1492  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
1493 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
1494  &1 `;];
1495 ASM_REWRITE_TAC[VECTOR_ARITH`A%(v-x)+ A%(y-v)+c= A%(y-x)+c`]
1496 THEN EXPAND_TAC"y1"
1497 THEN REWRITE_TAC[VECTOR_ARITH`&1 / &2 % (u + x) - x= &1/ &2 %(u-x)`]
1498 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - x) +
1499  (norm (v1 - v) * inv (norm (v1 - v) + b1)) % &1 / &2 % (u - x) =
1500  ((&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) * (&1 / &2 - a1 * inv b) + &1 / &2) % (u - x)
1501 <=> (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) % (v1 - &1/ &2 %(x+u)) =
1502  ((&1 - norm (v1 - v) * inv (norm (v1 - v) + b1)) * (&1 / &2 - a1 * inv b)) % (u - x)
1503 `]
1504 THEN EXPAND_TAC"v1"
1505 THEN REWRITE_TAC[VECTOR_ARITH`((a1 * inv b) % (x - u) + u) - &1 / &2 % (x + u)
1506 = (&1/ &2- a1 * inv b) % (u-x) `]
1507 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`];
1508 STRIP_TAC;
1509 MATCH_MP_TAC(REAL_ARITH`&0<=A ==> &0< A+ &1/ &2`)
1510 THEN MATCH_MP_TAC REAL_LE_MUL
1511 THEN ASM_REWRITE_TAC[]
1512 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v)==>norm(v1-v:real^3) < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0<= norm (v1-v) +b1`)
1513 THEN RESA_TAC
1514 THEN MRESA1_TAC REAL_LE_INV`(norm(v1-v:real^3)+b1)`
1515 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
1516 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
1517 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
1518  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
1519 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
1520  &1 `;];
1521 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1522 THEN STRIP_TAC;
1523 MATCH_MP_TAC REAL_LE_MUL
1524 THEN ASM_REWRITE_TAC[];
1525 ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`];
1526 SUBGOAL_THEN`&0< a1 * inv b`ASSUME_TAC;
1527 MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`x:real^3`][REAL_EQ_MUL_LCANCEL]
1528 THEN
1529 MRESA_TAC Trigonometry2.POW2_COND[`t:real`;`b:real`]
1530 THEN MP_TAC(REAL_ARITH`t pow 2 <= b pow 2 /\ &0< a pow 2 ==> &0< (a pow 2 +b pow 2 - t pow 2)/ &2`)
1531 THEN ASM_REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]
1532 THEN STRIP_TAC
1533 THEN MRESA_TAC REAL_LT_MUL[`inv b`;`(a pow 2 +b pow 2 - t pow 2)/ &2`]
1534 THEN MRESA_TAC REAL_LT_MUL[`a1:real`;`inv b`];
1535 MP_TAC(REAL_ARITH`&0< a1 * inv b==>(&1 / &2 - a1 * inv b)< &1/ &2`)
1536 THEN RESA_TAC
1537 THEN MP_TAC(REAL_ARITH`&0< b1 /\ &0< norm (v1-v:real^3)==>b1 < norm (v1-v) +b1/\  ~(norm (v1-v) +b1= &0)/\ &0< norm (v1-v) +b1 /\ &0<= norm (v1-v) +b1`)
1538 THEN RESA_TAC
1539 THEN MRESA1_TAC REAL_LT_INV`(norm(v1-v:real^3)+b1)`
1540 THEN MRESA1_TAC REAL_LE_INV`(norm(v1-v:real^3)+b1)`
1541 THEN MRESA1_TAC REAL_MUL_LINV`(norm(v1-v:real^3)+b1)`
1542 THEN SUBGOAL_THEN`inv (norm (v1 - v:real^3) + b1) * b1 = (&1 - norm (v1 - v) * inv (norm (v1 - v) + b1))`ASSUME_TAC;
1543 ASM_REWRITE_TAC[REAL_ARITH`inv (norm (v1 - v) + b1) * b1 =
1544  &1 - norm (v1 - v) * inv (norm (v1 - v) + b1)
1545 <=> inv (norm (v1 - v) + b1) *(norm(v1-v)+ b1) =
1546  &1 `;];
1547 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1548 THEN MRESA_TAC REAL_LT_LMUL[`inv (norm (v1 - v:real^3) + b1)`;`b1:real`;`norm (v1 - v:real^3) + b1`]
1549 THEN MRESA_TAC REAL_LE_MUL[`inv (norm (v1 - v:real^3) + b1)`;`b1:real`]
1550 THEN MRESAL_TAC Real_ext.REAL_PROP_LT_LRMUL[`(inv (norm (v1 - v:real^3) + b1) * b1)`;`&1`;`(&1 / &2 - a1 * inv b)`;`&1/ &2`][REAL_ARITH`&0<= A-B<=> B<=A`]
1551 THEN POP_ASSUM MP_TAC
1552 THEN REAL_ARITH_TAC;
1553 ASM_REWRITE_TAC[]]);;
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572 let TWO_DIAGONAL_AT_MOST1=prove_by_refinement(` t<= &2 /\ &0< t
1573 ==>
1574 ?u w:real^3 v x y.
1575 ~(v=x)/\ ~(v=u) /\ ~(v=w) /\ ~(x=u)/\ ~(x=w) /\ ~(u=w)
1576 /\ norm(v-x)=t
1577 /\ norm(v-u)= &2
1578 /\ norm(x-w)= &2
1579 /\ norm(u-w)= &2
1580 /\ y IN segment(v,w) INTER segment (x,u)
1581 /\ norm(v-w)= norm(x-u)
1582 /\ (t<= norm(v-w) ==> norm(v-w)<= &1 + sqrt( &5) /\ t<= &1 + sqrt( &5))`,
1583 [REPEAT STRIP_TAC
1584 THEN ABBREV_TAC`b=(&1- t/ &2)`
1585 THEN ABBREV_TAC`c=(&1+ t/ &2)`
1586 THEN ABBREV_TAC`d=(sqrt(&4- (&1- t/ &2) pow 2))`
1587 THEN ABBREV_TAC`e= &2* inv(t+ &2) * d`
1588 THEN MP_TAC(REAL_ARITH`t<= &2 /\ &0< t==> &0<= (&1- t/ &2) /\ (&1- t/ &2)<= &2/\ ~((&1- t/ &2)= &2) /\ ~(t+ &2= &0)/\ &0<= t/\ (&1- t/ &2) -(&1+ t/ &2) = -- t
1589 /\ (&1+ t/ &2) - &2 = -- (&1- t/ &2) /\ &0< t+ &2 /\ (&1- t/ &2) - &2 = -- (&1+ t/ &2)`)
1590 THEN RESA_TAC
1591 THEN SUBGOAL_THEN`&0<= &4- (&1- t/ &2) pow 2` ASSUME_TAC;
1592 REWRITE_TAC[REAL_ARITH`&0<= A- B<=> B<=A`]
1593 THEN MATCH_MP_TAC REAL_RSQRT_LE
1594 THEN MRESAL_TAC SQRT_UNIQUE[`&4`;`&2`][REAL_ARITH`&0<= &2 /\ &2 pow 2= &4`]
1595 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 <= &1- t/ &2 <=> t<= &2`; REAL_ARITH`t / &2 - &1 <= &2 <=>  t<= &6`; REAL_ARITH`&0 <= &4`]
1596 THEN MP_TAC(REAL_ARITH`t<= &2==> t <= &6`)
1597 THEN RESA_TAC;
1598 SUBGOAL_THEN`~(&4- (&1- t/ &2) pow 2= &0)` ASSUME_TAC;
1599 REWRITE_TAC[REAL_ARITH`A-B= &0 <=> B=A`]
1600 THEN STRIP_TAC
1601 THEN MRESAL_TAC Collect_geom.EQ_POW2_COND[` &1- t/ &2`;`&2`][REAL_ARITH`&2 pow 2= &4/\ &0<= &2`;REAL_ARITH`&0 <= t / &2 - &1<=> &2<= t`;REAL_ARITH`t / &2 - &1 = &2<=> t= &6`]
1602 THEN POP_ASSUM MP_TAC
1603 THEN MP_TAC(REAL_ARITH`t<= &4==> ~(t = &6)`)
1604 THEN RESA_TAC;
1605 SUBGOAL_THEN`b pow 2 + d pow 2= &4`ASSUME_TAC;
1606 MRESA1_TAC SQRT_POW_2`&4- (&1- t/ &2) pow 2`
1607 THEN EXPAND_TAC"b"
1608 THEN REAL_ARITH_TAC;
1609 MRESA1_TAC SQRT_EQ_0`&4- (&1- t/ &2) pow 2`
1610 THEN SUBGOAL_THEN`&1 - t * inv (t + &2) = &2 * inv (t + &2)` ASSUME_TAC;
1611 REWRITE_TAC[REAL_ARITH`A-B *D=C *D<=> D *(B+C)= A`]
1612 THEN MATCH_MP_TAC REAL_MUL_LINV
1613 THEN ASM_REWRITE_TAC[];
1614 EXISTS_TAC`vec 0:real^3`
1615 THEN EXISTS_TAC`(vector[&2; &0; &0]):real^3`
1616 THEN EXISTS_TAC`(vector[b; d; &0]):real^3`
1617 THEN EXISTS_TAC`(vector[c; d; &0]):real^3`
1618 THEN EXISTS_TAC`(vector[&1;e; &0]):real^3`
1619 THEN STRIP_TAC;
1620 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1621 THEN EXPAND_TAC"b"
1622 THEN EXPAND_TAC"c"
1623 THEN REWRITE_TAC[REAL_ARITH`&1 - t / &2 = &1 + t / &2 <=> t= &0`]
1624 THEN MP_TAC(REAL_ARITH`&0<t==> ~(t= &0)`)
1625 THEN RESA_TAC;
1626 STRIP_TAC;
1627 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1628 THEN EXPAND_TAC"b"
1629 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - t / &2= &0 <=> t= &2`;REAL_ARITH`&1 + t / &2= &0 <=> t= -- &2`;DE_MORGAN_THM];
1630 STRIP_TAC;
1631 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
1632 STRIP_TAC;
1633 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
1634 STRIP_TAC;
1635 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
1636 STRIP_TAC;
1637 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM;REAL_ARITH`~(&0= &2)`];
1638 STRIP_TAC;
1639 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1640            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1641            vector_neg; vector_sub; vector_mul; ARITH;]
1642 THEN REAL_ARITH_TAC;
1643 STRIP_TAC;
1644 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1645            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1646            vector_neg; vector_sub; vector_mul; ARITH;VECTOR_ARITH`A- vec 0=A`;
1647 REAL_ARITH`&0<= &2 /\ a * a= a pow 2/\ A+ &0 pow 2=A/\ &2 pow 2= &4`];
1648 STRIP_TAC;
1649 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1650            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1651            vector_neg; vector_sub; vector_mul; ARITH;
1652 REAL_ARITH`&0<= &2  /\ --a * --a= a pow 2/\ A- &0 =A/\ A+ &0 * &0=A/\ &2 pow 2= &4`]
1653 THEN ASM_REWRITE_TAC[REAL_ARITH`b * b= b pow 2`];
1654 STRIP_TAC;
1655 ONCE_REWRITE_TAC[NORM_SUB]
1656 THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1657            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1658            vector_neg; vector_sub; vector_mul; ARITH;VECTOR_ARITH`A- vec 0=A`;
1659 REAL_ARITH`&0<= &2 /\ a * a= a pow 2/\ A+ &0 pow 2=A/\ &2 pow 2= &4`];
1660 STRIP_TAC;
1661 REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
1662 THEN STRIP_TAC;
1663 STRIP_TAC;
1664 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
1665 EXISTS_TAC`t * inv(t+ &2)`
1666 THEN STRIP_TAC;
1667 MATCH_MP_TAC REAL_LT_MUL
1668 THEN ASM_REWRITE_TAC[]
1669 THEN MATCH_MP_TAC REAL_LT_INV
1670 THEN ASM_REWRITE_TAC[];
1671 STRIP_TAC;
1672 MATCH_MP_TAC REAL_LT_RCANCEL_IMP
1673 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`
1674 THEN EXISTS_TAC`t+ &2`
1675 THEN ASM_REWRITE_TAC[REAL_ARITH`(A *B) * C= A *(B*C)`]
1676 THEN REAL_ARITH_TAC;
1677 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1678            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1679            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`&2 * inv (t + &2) * b + t * inv (t + &2) * &2= &2 * inv (t + &2) * (b+t)`]
1680 THEN EXPAND_TAC"b"
1681 THEN REWRITE_TAC[REAL_ARITH`&1 = &2 * inv (t + &2) * (&1 - t / &2 + t)
1682 <=> inv (t + &2) * (t + &2)= &1`]
1683 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`;
1684 STRIP_TAC;
1685 ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;DE_MORGAN_THM];
1686 EXISTS_TAC`t * inv(t+ &2)`
1687 THEN STRIP_TAC;
1688 MATCH_MP_TAC REAL_LT_MUL
1689 THEN ASM_REWRITE_TAC[]
1690 THEN MATCH_MP_TAC REAL_LT_INV
1691 THEN ASM_REWRITE_TAC[];
1692 STRIP_TAC;
1693 MATCH_MP_TAC REAL_LT_RCANCEL_IMP
1694 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`
1695 THEN EXISTS_TAC`t+ &2`
1696 THEN ASM_REWRITE_TAC[REAL_ARITH`(A *B) * C= A *(B*C)`]
1697 THEN REAL_ARITH_TAC;
1698 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1699            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ_SQUARE;
1700            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`&2 * inv (t + &2) * b + t * inv (t + &2) * &2= &2 * inv (t + &2) * (b+t)`]
1701 THEN EXPAND_TAC"c"
1702 THEN REWRITE_TAC[REAL_ARITH`&1 = &2 * inv (t + &2) * (&1 + t / &2)
1703 <=> inv (t + &2) * (t + &2)= &1`]
1704 THEN MRESA1_TAC REAL_MUL_LINV`t + &2`;
1705 STRIP_TAC;
1706 ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1707            vector_add; vec; dot; cross; orthogonal; basis; NORM_EQ;
1708            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c`;REAL_ARITH`a- &0=a `;VECTOR_ARITH`A- vec 0=A`]
1709 THEN REAL_ARITH_TAC;
1710 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a<=b <=> b>=a`]
1711 THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1712            vector_add; vec; dot; cross; orthogonal; basis; NORM_LE_SQUARE;NORM_GE_SQUARE;
1713            vector_neg; vector_sub; vector_mul; ARITH;REAL_ARITH`A * &0= &0 /\ a+ &0 = a/\ (a*b)*c=a *b*c/\ --c * --c + d * d= c pow 2 + d pow 2`;REAL_ARITH`a- &0=a `;VECTOR_ARITH`A- vec 0=A`]
1714 THEN MRESA1_TAC SQRT_POW_2`&4 - (&1- t/ &2) pow 2`
1715 THEN MRESAL1_TAC SQRT_POW_2`(&5)`[REAL_ARITH`&0<= &5`;REAL_ARITH`(&1 + sqrt (&5)) pow 2= &1 + &2 * sqrt(&5) + sqrt(&5) pow 2`]
1716 THEN MP_TAC(REAL_ARITH`&0< t==> ~(t<= &0)`)
1717 THEN RESA_TAC
1718 THEN EXPAND_TAC"b"
1719 THEN EXPAND_TAC"c"
1720 THEN REWRITE_TAC[REAL_ARITH`(&1 + t / &2) pow 2 + &4 - (&1- t/ &2) pow 2
1721 =  &4 + &2 * t`;REAL_ARITH`&4 + &2 * t <= &1 + &2 * sqrt (&5) + &5<=>  t <= &1 + sqrt( &5) `; REAL_ARITH`&4 + &2 * t >= t pow 2<=> (t- &1) pow 2<= &5`]
1722 THEN STRIP_TAC
1723 THEN MRESAL_TAC REAL_LE_RSQRT[`t- &1`;`&5`][REAL_ARITH`A-B<= C<=> A<= B+C`]
1724 THEN MRESAL1_TAC SQRT_POS_LE`&5`[REAL_ARITH`&0<= &5`]
1725 THEN POP_ASSUM MP_TAC
1726 THEN REAL_ARITH_TAC]);;
1727
1728
1729
1730
1731
1732
1733
1734
1735 let VPWSHTO1=prove_by_refinement(`!v x:real^3  u w:real^3.
1736 t<= &4 /\ ~(collinear{v,x,u})
1737 /\ ~(collinear{w,x,u})
1738 /\ ~(v=w)
1739 /\ norm(v-x)=t
1740 /\ norm(v-u)= &2
1741 /\ norm(x-w)= &2
1742 /\ norm(u-w)= &2
1743 /\ t<= norm(x-u)
1744 /\ t<= norm(v-w)
1745 ==> min  (norm(v-w)) (norm(x-u))<= &1 + sqrt(&5)/\ t<= &1 + sqrt(&5)`,
1746 [REPEAT GEN_TAC
1747 THEN STRIP_TAC
1748 THEN MRESA_TAC th3[`v:real^3`;`x:real^3`;`u:real^3`]
1749 THEN MRESA_TAC th3[`w:real^3`;`x:real^3`;`u:real^3`]
1750 THEN MRESA_TAC th3[`x:real^3`;`w:real^3`;`u:real^3`]
1751 THEN POP_ASSUM MP_TAC
1752 THEN ONCE_REWRITE_TAC[SET_RULE`{x,w,u}={w,x,u}`]
1753 THEN RESA_TAC
1754 THEN DISJ_CASES_TAC(REAL_ARITH`&2<= t \/ t<= &2`);
1755 MRESA_TAC MAX_IF_COPLANAR[`v:real^3`;`x:real^3`;`u:real^3`;`w:real^3`;`&2`;`t:real`]
1756 THEN SUBGOAL_THEN`~(x =w1:real^3)` ASSUME_TAC;
1757 STRIP_TAC
1758 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1759 THEN POP_ASSUM MP_TAC
1760 THEN POP_ASSUM MP_TAC
1761 THEN POP_ASSUM MP_TAC
1762 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
1763 THEN REAL_ARITH_TAC;
1764 SUBGOAL_THEN`~(u =w1:real^3)` ASSUME_TAC;
1765 STRIP_TAC
1766 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1767 THEN POP_ASSUM MP_TAC
1768 THEN POP_ASSUM MP_TAC
1769 THEN POP_ASSUM MP_TAC
1770 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
1771 THEN REAL_ARITH_TAC;
1772 MRESA_TAC (GEN_ALL MAX_COPLANAR_4POINT)[`t:real`;`y:real^3`;`&2`;`v:real^3`;`x:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
1773 THEN MRESA1_TAC (GEN_ALL TWO_DIAGONAL_AT_MOST)`t:real`
1774 THEN POP_ASSUM MP_TAC
1775 THEN MRESA_TAC (GEN_ALL EQ_DIAGONAL_MIN)[`y':real^3`;`t:real`;`&2`;`y:real^3`;`v':real^3`;`v:real^3`;`x':real^3`;`x:real^3`;`u':real^3`;`w':real^3`;`u:real^3`;`w1:real^3`]
1776 THEN MP_TAC(REAL_ARITH`min (norm (v - w1)) (norm (x - u)) <= norm (x' - u')
1777 /\ min (norm (v - w:real^3)) (norm (x - u)) <= min (norm (v - w1)) (norm (x - u:real^3))
1778 /\ t<= norm (v - w) /\ t <= norm (x - u)
1779 ==> min (norm (v - w)) (norm (x - u)) <= norm (x' - u':real^3)/\ t<= norm (x' - u':real^3) `)
1780 THEN RESA_TAC
1781 THEN REMOVE_ASSUM_TAC
1782 THEN POP_ASSUM MP_TAC
1783 THEN REAL_ARITH_TAC;
1784 MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`x:real^3`][REAL_EQ_MUL_LCANCEL]
1785 THEN DISJ_CASES_TAC (REAL_ARITH`norm (u - x:real^3)< &2\/(&2 <= norm (u - x))`);
1786 SUBGOAL_THEN`&2<= &1+ sqrt(&5)` ASSUME_TAC;
1787 REWRITE_TAC[REAL_ARITH`&2<= &1+ sqrt(&5)<=> &1<= sqrt(&5)`]
1788 THEN MATCH_MP_TAC REAL_LE_RSQRT
1789 THEN REAL_ARITH_TAC;
1790 POP_ASSUM MP_TAC
1791 THEN ONCE_REWRITE_TAC[NORM_SUB]
1792 THEN POP_ASSUM MP_TAC
1793 THEN REMOVE_ASSUM_TAC
1794 THEN REMOVE_ASSUM_TAC
1795 THEN REMOVE_ASSUM_TAC
1796 THEN REMOVE_ASSUM_TAC
1797 THEN REMOVE_ASSUM_TAC
1798 THEN REMOVE_ASSUM_TAC
1799 THEN POP_ASSUM MP_TAC
1800 THEN REAL_ARITH_TAC;
1801 MRESA_TAC MAX_IF_COPLANAR1[`v:real^3`;`u:real^3`;`x:real^3`;`w:real^3`;`t:real`;`&2:real`;`&2`]
1802 THEN POP_ASSUM MP_TAC
1803 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1804 THEN RESA_TAC
1805 THEN SUBGOAL_THEN`~(x =w1:real^3)` ASSUME_TAC;
1806 STRIP_TAC
1807 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1808 THEN POP_ASSUM MP_TAC
1809 THEN POP_ASSUM MP_TAC
1810 THEN POP_ASSUM MP_TAC
1811 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
1812 THEN REAL_ARITH_TAC;
1813 SUBGOAL_THEN`~(u =w1:real^3)` ASSUME_TAC;
1814 STRIP_TAC
1815 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1816 THEN POP_ASSUM MP_TAC
1817 THEN POP_ASSUM MP_TAC
1818 THEN POP_ASSUM MP_TAC
1819 THEN POP_ASSUM MP_TAC
1820 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
1821 THEN REAL_ARITH_TAC;
1822 SUBGOAL_THEN`y IN segment (v,w1) INTER segment (x,u:real^3)` ASSUME_TAC;
1823 ASM_TAC
1824 THEN REWRITE_TAC[INTER;IN_ELIM_THM]
1825 THEN REPEAT STRIP_TAC
1826 THEN ASM_REWRITE_TAC[]
1827 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
1828 THEN ASM_REWRITE_TAC[];
1829 MRESA_TAC (GEN_ALL MAX_COPLANAR_4POINT)[`t:real`;`y:real^3`;`&2`;`v:real^3`;`x:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
1830 THEN MRESA1_TAC (GEN_ALL TWO_DIAGONAL_AT_MOST1)`t:real`
1831 THEN POP_ASSUM MP_TAC
1832 THEN MRESA_TAC (GEN_ALL EQ_DIAGONAL_MIN)[`y':real^3`;`t:real`;`&2`;`y:real^3`;`v':real^3`;`v:real^3`;`x':real^3`;`x:real^3`;`u':real^3`;`w':real^3`;`u:real^3`;`w1:real^3`]
1833 THEN MP_TAC(REAL_ARITH`min (norm (v - w1)) (norm (x - u)) <= norm (x' - u')
1834 /\ min (norm (v - w:real^3)) (norm (x - u)) <= min (norm (v - w1)) (norm (x - u:real^3))
1835 /\ t<= norm (v - w) /\ t <= norm (x - u)
1836 ==> min (norm (v - w)) (norm (x - u)) <= norm (x' - u':real^3)/\ t<= norm (x' - u':real^3) `)
1837 THEN RESA_TAC
1838 THEN REMOVE_ASSUM_TAC
1839 THEN POP_ASSUM MP_TAC
1840 THEN REAL_ARITH_TAC]);;
1841
1842
1843
1844
1845
1846
1847 let VPWSHTO200=prove_by_refinement(
1848 `!v x:real^3  u w:real^3 w1.
1849 ~(collinear{v,x,u})
1850 /\ ~(collinear{w,x,u})
1851 /\ ~(collinear{w1,x,u})
1852 /\ ~(collinear{w,v,u})
1853 /\ ~(collinear{w1,v,u})
1854 /\ ~(collinear{w1,w,u})
1855 /\ ~(collinear{w,v,x})
1856 /\ ~(collinear{w1,v,x})
1857 /\ ~(collinear{w1,w,x})
1858 /\ ~(collinear{w1,w,v})
1859 /\ norm(v-x)= &2
1860 /\ norm(x-u)= &2
1861 /\ norm(u-w)= &2
1862 /\ norm(w-w1)= &2
1863 /\ norm(w1-v)= &2
1864 /\ norm(v-u)<= norm(v-w)
1865 /\ norm(v-u)<= norm(u-w1)
1866 /\ norm(v-u)<= norm(w1-x)
1867 /\ norm(v-u)<= norm(x-w)
1868 ==> ?w2.  w2 IN {v,x,u,w,w1}/\ ~(x=w2)
1869 /\ norm(v-u) <= &1 + sqrt(&5)/\
1870  ((~(w1=w2) /\ norm(v-w2)<= &1 + sqrt(&5)) \/ (~(w=w2) /\ norm(u-w2)<= &1 + sqrt(&5)))`,
1871 [REPEAT STRIP_TAC
1872 THEN MRESAL_TAC NORM_TRIANGLE[`v-x:real^3`;`x-u:real^3`][VECTOR_ARITH`v-x+x-u=v-u:real^3`;REAL_ARITH`&2+ &2= &4`]
1873 THEN MRESA_TAC (GEN_ALL VPWSHTO1)[`norm(v-u:real^3)`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
1874 THEN POP_ASSUM MP_TAC
1875 THEN ONCE_REWRITE_TAC[NORM_SUB]
1876 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1877 THEN ASM_REWRITE_TAC[]
1878 THEN MRESA_TAC th3[`w:real^3`;`v:real^3`;`u:real^3`]
1879 THEN STRIP_TAC
1880 THEN DISJ_CASES_TAC(REAL_ARITH`norm(w1-u) <= norm(w-v:real^3)\/ norm(w-v) <= norm(w1-u:real^3)`);
1881 MP_TAC(REAL_ARITH`norm (w1 - u) <= norm (w - v:real^3) /\ min (norm (w - v)) (norm (w1 - u)) <= &1 + sqrt (&5)
1882 ==> norm(w1-u:real^3)<= &1 + sqrt (&5)`)
1883 THEN RESA_TAC
1884 THEN EXISTS_TAC`w1:real^3`
1885 THEN ASM_REWRITE_TAC[]
1886 THEN ONCE_REWRITE_TAC[NORM_SUB]
1887 THEN ASM_REWRITE_TAC[]
1888 THEN MRESA_TAC th3[`w1:real^3`;`w:real^3`;`u:real^3`]
1889 THEN MRESA_TAC th3[`w1:real^3`;`v:real^3`;`x:real^3`]
1890 THEN SET_TAC[];
1891 MP_TAC(REAL_ARITH`norm (w - v) <= norm (w1 - u:real^3) /\ min (norm (w - v)) (norm (w1 - u)) <= &1 + sqrt (&5)
1892 ==> norm(w-v:real^3)<= &1 + sqrt (&5)`)
1893 THEN RESA_TAC
1894 THEN EXISTS_TAC`w:real^3`
1895 THEN ASM_REWRITE_TAC[]
1896 THEN MRESA_TAC th3[`w1:real^3`;`w:real^3`;`u:real^3`]
1897 THEN MRESA_TAC th3[`w:real^3`;`v:real^3`;`x:real^3`]
1898 THEN SET_TAC[]]);;
1899
1900
1901 let VPWSHTO2=prove(`!vv:num->real^3.
1902 ~(collinear{vv 0, vv 1 ,vv 2})
1903 /\ ~(collinear{vv 3,vv 1,vv 2})
1904 /\ ~(collinear{vv 4,vv 1,vv 2})
1905 /\ ~(collinear{vv 3,vv 0,vv 2})
1906 /\ ~(collinear{vv 4, vv 0,vv 2})
1907 /\ ~(collinear{vv 4, vv 3,vv 2})
1908 /\ ~(collinear{vv 3,vv 0,vv 1})
1909 /\ ~(collinear{vv 4,vv 0,vv 1})
1910 /\ ~(collinear{vv 4,vv 3,vv 1})
1911 /\ ~(collinear{vv 4,vv 3,vv 0})
1912 /\ norm(vv 0-vv 1)= &2
1913 /\ norm(vv 1-vv 2)= &2
1914 /\ norm(vv 2-vv 3)= &2
1915 /\ norm(vv 3-vv 4)= &2
1916 /\ norm(vv 4-vv 0)= &2
1917 /\ norm(vv 0-vv 2)<= norm(vv 0-vv 3)
1918 /\ norm(vv 0-vv 2)<= norm(vv 2-vv 4)
1919 /\ norm(vv 0-vv 2)<= norm(vv 4-vv 1)
1920 /\ norm(vv 0-vv 2)<= norm(vv 1-vv 3)
1921 ==>
1922 ?i. i IN 0..4/\ norm(vv i - vv ((i +2) MOD 5) ) <= &1 + sqrt(&5)/\ norm(vv i - vv ((i +3) MOD 5))<= &1 + sqrt(&5)`,
1923 REPEAT STRIP_TAC
1924 THEN ABBREV_TAC `v= (vv:num->real^3) 0`
1925 THEN ABBREV_TAC `x= (vv:num->real^3) 1`
1926 THEN ABBREV_TAC `u= (vv:num->real^3) 2`
1927 THEN ABBREV_TAC `w= (vv:num->real^3) 3`
1928 THEN ABBREV_TAC `w1= (vv:num->real^3) 4`
1929 THEN MRESAL_TAC NORM_TRIANGLE[`v-x:real^3`;`x-u:real^3`][VECTOR_ARITH`v-x+x-u=v-u:real^3`;REAL_ARITH`&2+ &2= &4`]
1930 THEN MRESA_TAC (GEN_ALL VPWSHTO1)[`norm(v-u:real^3)`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
1931 THEN POP_ASSUM MP_TAC
1932 THEN ONCE_REWRITE_TAC[NORM_SUB]
1933 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1934 THEN ASM_REWRITE_TAC[]
1935 THEN MRESA_TAC th3[`w:real^3`;`v:real^3`;`u:real^3`]
1936 THEN STRIP_TAC
1937 THEN DISJ_CASES_TAC(REAL_ARITH`norm(w1-u) <= norm(w-v:real^3)\/ norm(w-v) <= norm(w1-u:real^3)`)
1938 THENL[
1939 MP_TAC(REAL_ARITH`norm (w1 - u) <= norm (w - v:real^3) /\ min (norm (w - v)) (norm (w1 - u)) <= &1 + sqrt (&5)
1940 ==> norm(w1-u:real^3)<= &1 + sqrt (&5)`)
1941 THEN RESA_TAC
1942 THEN EXISTS_TAC`2`
1943 THEN ASM_REWRITE_TAC[ARITH_RULE`(2+2) MOD 5=4/\(2+3) MOD 5=0/\ 0<=2/\2<=4`;IN_NUMSEG]
1944 THEN ONCE_REWRITE_TAC[NORM_SUB]
1945 THEN ASM_REWRITE_TAC[];
1946 MP_TAC(REAL_ARITH`norm (w - v) <= norm (w1 - u:real^3) /\ min (norm (w - v)) (norm (w1 - u)) <= &1 + sqrt (&5)
1947 ==> norm(w-v:real^3)<= &1 + sqrt (&5)`)
1948 THEN RESA_TAC
1949 THEN EXISTS_TAC`0`
1950 THEN ASM_REWRITE_TAC[ARITH_RULE`(0+2) MOD 5=2/\(0+3) MOD 5=3/\
1951 0<=0/\0<=4`;IN_NUMSEG]]);;
1952
1953
1954
1955
1956 let MOD_ADD_235=prove(`((i + 2) MOD 5 + 3) MOD 5 =i MOD 5`,
1957 MRESAL_TAC MOD_ADD_MOD[`i+2`;`3`;`5`][ARITH_RULE`~(5=0)/\ 3 MOD 5=3/\ (i + 2) + 3=1*5+i`]
1958 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i:num`]);;
1959
1960
1961 let MOD_ADD_325=prove(`((i + 3) MOD 5 + 2) MOD 5 =i MOD 5`,
1962 MRESAL_TAC MOD_ADD_MOD[`i+3`;`2`;`5`][ARITH_RULE`~(5=0)/\ 2 MOD 5=2/\ (i + 3) + 2=1*5+i`]
1963 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i:num`]);;
1964
1965 let MOD_ADD_225=prove(`((i + 2) MOD 5 + 2) MOD 5 =(i+4) MOD 5`,
1966 MRESAL_TAC MOD_ADD_MOD[`i+2`;`2`;`5`][ARITH_RULE`~(5=0)/\ 2 MOD 5=2/\ (i + 2) + 2=i+4`]
1967 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i:num`]);;
1968
1969 let MOD_ADD_335=prove(`((i + 3) MOD 5 + 3) MOD 5 =(i+1) MOD 5`,
1970 MRESAL_TAC MOD_ADD_MOD[`i+3`;`3`;`5`][ARITH_RULE`~(5=0)/\ 3 MOD 5=3/\ (i + 3) + 3=1*5+(i+1)`]
1971 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+1:num`]);;
1972
1973
1974 let MOD_ADD_345=prove(`((i + 3) MOD 5 + 4) MOD 5 =(i+2) MOD 5`,
1975 MRESAL_TAC MOD_ADD_MOD[`i+3`;`4`;`5`][ARITH_RULE`~(5=0)/\ 4 MOD 5=4/\ (i + 3) + 4=1*5+(i+2)`]
1976 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+2:num`]);;
1977
1978 let MOD_ADD_245=prove(`((i + 2) MOD 5 + 4) MOD 5 =(i+1) MOD 5`,
1979 MRESAL_TAC MOD_ADD_MOD[`i+2`;`4`;`5`][ARITH_RULE`~(5=0)/\ 4 MOD 5=4/\ (i + 2) + 4=1*5+(i+1)`]
1980 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+1:num`]);;
1981
1982 let MOD_ADD_425=prove(`((i + 4) MOD 5 + 2) MOD 5 =(i+1) MOD 5`,
1983 MRESAL_TAC MOD_ADD_MOD[`i+4`;`2`;`5`][ARITH_RULE`~(5=0)/\ 2 MOD 5=2/\ (i + 4) + 2=1*5+(i+1)`]
1984 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+1:num`]);;
1985
1986 let MOD_ADD_435=prove(`((i + 4) MOD 5 + 3) MOD 5 =(i+2) MOD 5`,
1987 MRESAL_TAC MOD_ADD_MOD[`i+4`;`3`;`5`][ARITH_RULE`~(5=0)/\ 3 MOD 5=3/\ (i + 4) + 3=1*5+(i+2)`]
1988 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+2:num`]);;
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999 let MOD_ADD_215=prove(`((i + 2) MOD 5 + 1) MOD 5 =(i+3) MOD 5`,
2000 MRESAL_TAC MOD_ADD_MOD[`i+2`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ (i + 2) + 1=(i+3)`]
2001 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+1:num`]);;
2002
2003 let MOD_ADD_125=prove(`((i + 1) MOD 5 + 2) MOD 5 =(i+3) MOD 5`,
2004 MRESAL_TAC MOD_ADD_MOD[`i+1`;`2`;`5`][ARITH_RULE`~(5=0)/\ 2 MOD 5=2/\ (i + 1) + 2=(i+3)`]
2005 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+1:num`]);;
2006
2007 let MOD_ADD_135=prove(`((i + 1) MOD 5 + 3) MOD 5 =(i+4) MOD 5`,
2008 MRESAL_TAC MOD_ADD_MOD[`i+1`;`3`;`5`][ARITH_RULE`~(5=0)/\ 3 MOD 5=3/\ (i + 1) + 3=(i+4)`]
2009 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+2:num`]);;
2010
2011 let MOD_ADD_315=prove(`((i + 3) MOD 5 + 1) MOD 5 =(i+4) MOD 5`,
2012 MRESAL_TAC MOD_ADD_MOD[`i+3`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ (i + 3) + 1=(i+4)`]
2013 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i+2:num`]);;
2014
2015 let VPWSHTO=prove_by_refinement(`!vv:num->real^3.
2016 ~(collinear{vv 0, vv 1 ,vv 2})
2017 /\ ~(collinear{vv 3,vv 1,vv 2})
2018 /\ ~(collinear{vv 4,vv 1,vv 2})
2019 /\ ~(collinear{vv 3,vv 0,vv 2})
2020 /\ ~(collinear{vv 4, vv 0,vv 2})
2021 /\ ~(collinear{vv 4, vv 3,vv 2})
2022 /\ ~(collinear{vv 3,vv 0,vv 1})
2023 /\ ~(collinear{vv 4,vv 0,vv 1})
2024 /\ ~(collinear{vv 4,vv 3,vv 1})
2025 /\ ~(collinear{vv 4,vv 3,vv 0})
2026 /\ norm(vv 0-vv 1)= &2
2027 /\ norm(vv 1-vv 2)= &2
2028 /\ norm(vv 2-vv 3)= &2
2029 /\ norm(vv 3-vv 4)= &2
2030 /\ norm(vv 4-vv 0)= &2
2031 ==>
2032 ?i. i IN 0..4/\ norm(vv i - vv ((i +2) MOD 5) ) <= &1 + sqrt(&5)/\ norm(vv i - vv ((i +3) MOD 5))<= &1 + sqrt(&5)`,
2033 [
2034 REPEAT STRIP_TAC
2035 THEN ABBREV_TAC `v= (vv:num->real^3) 0`
2036 THEN ABBREV_TAC `x= (vv:num->real^3) 1`
2037 THEN ABBREV_TAC `u= (vv:num->real^3) 2`
2038 THEN ABBREV_TAC `w= (vv:num->real^3) 3`
2039 THEN ABBREV_TAC `w1= (vv:num->real^3) 4`
2040 THEN DISJ_CASES_TAC(REAL_ARITH`(norm(v-u)<= norm(v-w)
2041 /\ norm(v-u)<= norm(u-w1)
2042 /\ norm(v-u)<= norm(w1-x)
2043 /\ norm(v-u)<= norm(x-w:real^3))
2044 \/
2045 (norm(v-w)<= norm(v-u)
2046 /\ norm(v-w)<= norm(u-w1)
2047 /\ norm(v-w)<= norm(w1-x)
2048 /\ norm(v-w)<= norm(x-w))
2049 \/
2050 (norm(u-w1)<= norm(v-w)
2051 /\ norm(u-w1)<= norm(v-u)
2052 /\ norm(u-w1)<= norm(w1-x)
2053 /\ norm(u-w1)<= norm(x-w))
2054 \/
2055 (norm(w1-x)<= norm(v-w)
2056 /\ norm(w1-x)<= norm(u-w1)
2057 /\ norm(w1-x)<= norm(v-u)
2058 /\ norm(w1-x)<= norm(x-w))
2059 \/
2060 (norm(x-w)<= norm(v-w)
2061 /\ norm(x-w)<= norm(u-w1)
2062 /\ norm(x-w)<= norm(w1-x)
2063 /\ norm(x-w)<= norm(v-u))`);
2064 MRESA_TAC VPWSHTO2[`vv:num->real^3`];
2065 POP_ASSUM MP_TAC
2066 THEN STRIP_TAC;
2067 MRESAL_TAC VPWSHTO2[`(\i. (vv:num->real^3) ((i+3) MOD 5))`;]
2068 [ARITH_RULE`0+3=3/\ 1+3=4/\ 2+3=5/\ 3+3=6/\ 4+3=7/\ 0 MOD 5=0
2069 /\ 1 MOD 5=1 /\ 2 MOD 5=2/\ 3  MOD 5=3/\ 4 MOD 5=4/\ 5 MOD 5=0/\ 6 MOD 5=1/\ 7 MOD 5=2`]
2070 THEN POP_ASSUM MP_TAC
2071 THEN MRESA_TAC NORM_SUB[`w:real^3`;`v:real^3`]
2072 THEN MRESA_TAC NORM_SUB[`w:real^3`;`x:real^3`]
2073 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2074 THEN ASM_REWRITE_TAC[]
2075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2076 THEN ASM_REWRITE_TAC[]
2077 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]
2078 THEN ASM_REWRITE_TAC[]
2079 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2080 THEN ASM_REWRITE_TAC[]
2081 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2082 THEN ASM_REWRITE_TAC[MOD_ADD_235;MOD_ADD_335]
2083 THEN STRIP_TAC
2084 THEN EXISTS_TAC`(i+3) MOD 5`
2085 THEN MRESAL_TAC DIVISION[`i+3`;`5`][ARITH_RULE`~(5=0)`;IN_NUMSEG;MOD_ADD_325;MOD_ADD_335]
2086 THEN POP_ASSUM MP_TAC
2087 THEN ARITH_TAC;
2088 MRESAL_TAC VPWSHTO2[`(\i. (vv:num->real^3) ((i+2) MOD 5))`;]
2089 [ARITH_RULE`0+2=2/\ 1+2=3/\ 2+2=4/\ 3+2=5/\ 4+2=6/\ 0 MOD 5=0
2090 /\ 1 MOD 5=1 /\ 2 MOD 5=2/\ 3  MOD 5=3/\ 4 MOD 5=4/\ 5 MOD 5=0/\ 6 MOD 5=1/\ 7 MOD 5=2`]
2091 THEN POP_ASSUM MP_TAC
2092 THEN MRESA_TAC NORM_SUB[`w:real^3`;`v:real^3`]
2093 THEN MRESA_TAC NORM_SUB[`u:real^3`;`v:real^3`]
2094 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2095 THEN ASM_REWRITE_TAC[]
2096 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2097 THEN ASM_REWRITE_TAC[]
2098 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]
2099 THEN ASM_REWRITE_TAC[]
2100 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2101 THEN ASM_REWRITE_TAC[]
2102 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2103 THEN ASM_REWRITE_TAC[MOD_ADD_225;MOD_ADD_325]
2104 THEN STRIP_TAC
2105 THEN EXISTS_TAC`(i+2) MOD 5`
2106 THEN MRESAL_TAC DIVISION[`i+2`;`5`][ARITH_RULE`~(5=0)`;IN_NUMSEG;MOD_ADD_225;MOD_ADD_235]
2107 THEN POP_ASSUM MP_TAC
2108 THEN ARITH_TAC;
2109 MRESAL_TAC VPWSHTO2[`(\i. (vv:num->real^3) ((i+4) MOD 5))`;]
2110 [ARITH_RULE`0+4=4/\ 1+4=5/\ 2+4=6/\ 3+4=7/\ 4+4=8/\ 0 MOD 5=0
2111 /\ 1 MOD 5=1 /\ 2 MOD 5=2/\ 3  MOD 5=3/\ 4 MOD 5=4/\ 5 MOD 5=0/\ 6 MOD 5=1/\ 7 MOD 5=2/\ 8 MOD 5=3`]
2112 THEN POP_ASSUM MP_TAC
2113 THEN MRESA_TAC NORM_SUB[`w:real^3`;`v:real^3`]
2114 THEN MRESA_TAC NORM_SUB[`w1:real^3`;`u:real^3`]
2115 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2116 THEN ASM_REWRITE_TAC[]
2117 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2118 THEN ASM_REWRITE_TAC[]
2119 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]
2120 THEN ASM_REWRITE_TAC[]
2121 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2122 THEN ASM_REWRITE_TAC[]
2123 THEN ASM_REWRITE_TAC[MOD_ADD_245;MOD_ADD_345]
2124 THEN STRIP_TAC
2125 THEN EXISTS_TAC`(i+4) MOD 5`
2126 THEN MRESAL_TAC DIVISION[`i+4`;`5`][ARITH_RULE`~(5=0)`;IN_NUMSEG;MOD_ADD_425;MOD_ADD_435]
2127 THEN POP_ASSUM MP_TAC
2128 THEN ARITH_TAC;
2129 MRESAL_TAC VPWSHTO2[`(\i. (vv:num->real^3) ((i+1) MOD 5))`;]
2130 [ARITH_RULE`0+1=1/\ 1+1=2/\ 2+1=3/\ 3+1=4/\ 4+1=5/\ 0 MOD 5=0
2131 /\ 1 MOD 5=1 /\ 2 MOD 5=2/\ 3  MOD 5=3/\ 4 MOD 5=4/\ 5 MOD 5=0/\ 6 MOD 5=1/\ 7 MOD 5=2/\ 8 MOD 5=3`]
2132 THEN POP_ASSUM MP_TAC
2133 THEN MRESA_TAC NORM_SUB[`w:real^3`;`v:real^3`]
2134 THEN MRESA_TAC NORM_SUB[`x:real^3`;`w1:real^3`]
2135 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2136 THEN ASM_REWRITE_TAC[]
2137 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
2138 THEN ASM_REWRITE_TAC[]
2139 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]
2140 THEN ASM_REWRITE_TAC[]
2141 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2142 THEN ASM_REWRITE_TAC[MOD_ADD_215;MOD_ADD_315]
2143 THEN STRIP_TAC
2144 THEN EXISTS_TAC`(i+1) MOD 5`
2145 THEN MRESAL_TAC DIVISION[`i+1`;`5`][ARITH_RULE`~(5=0)`;IN_NUMSEG;MOD_ADD_125;MOD_ADD_135]
2146 THEN POP_ASSUM MP_TAC
2147 THEN ARITH_TAC]);;
2148
2149
2150
2151 let POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR=prove_by_refinement(`{u,v,w} SUBSET ball_annulus /\  packing {u,v,w} /\ ~(u=v)/\ ~(u=w)/\ ~(v=w)
2152 ==> ~(v IN segment [u,w])`,
2153 [REPEAT STRIP_TAC
2154 THEN ABBREV_TAC`t= (inv (norm(u-w))) pow 2 * (w dot (w-u:real^3))`
2155 THEN ABBREV_TAC`p=t %(u-w)+w:real^3`
2156 THEN SUBGOAL_THEN`collinear{u,p,w:real^3}` ASSUME_TAC;
2157 REWRITE_TAC[COLLINEAR_3_EXPAND]
2158 THEN MATCH_MP_TAC(SET_RULE`A==> B\/ A`)
2159 THEN EXISTS_TAC`t:real`
2160 THEN EXPAND_TAC"p"
2161 THEN VECTOR_ARITH_TAC;
2162 POP_ASSUM MP_TAC
2163 THEN REWRITE_TAC[COLLINEAR_BETWEEN_CASES;BETWEEN_IN_SEGMENT]
2164 THEN SUBGOAL_THEN`norm(p:real^3) pow 2+ norm(p-w:real^3) pow 2= norm(w) pow 2` ASSUME_TAC;
2165 MRESAL_TAC LAW_OF_COSINES[`p:real^3`;`w:real^3`;`vec 0:real^3`][dist;VECTOR_ARITH`A- vec 0=A`;REAL_ARITH`A+B=(B+A)- &2* C<=> C= &0`;COS_ANGLE]
2166 THEN EXPAND_TAC"p"
2167 THEN REWRITE_TAC[VECTOR_ARITH`w - (t % (u - w) + w)= (-- t) % (u - w)/\ vec 0-A= --A`;DOT_RNEG;DOT_LMUL;DOT_RMUL;DOT_RADD]
2168 THEN EXPAND_TAC"t"
2169 THEN REWRITE_TAC[DOT_SQUARE_NORM;VECTOR_ARITH`(inv (norm (u - w)) pow 2 * (w dot (w - u))) * norm (u - w) pow 2 +
2170            (u - w) dot w
2171 =(inv (norm (u - w)) * norm (u - w)) pow 2 * (w dot (w-u)) -
2172            (w-u) dot w`]
2173 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`u:real^3`;`w:real^3`]
2174 THEN MRESA_TAC DOT_SYM[`w:real^3`;`w-u:real^3`]
2175 THEN REWRITE_TAC[REAL_ARITH`(--t * --(&1 pow 2 * ((w - u) dot w) - (w - u) dot w)) /
2176        (norm (--t % (u - w)) * norm (--p))= &0`]
2177 THEN REAL_ARITH_TAC;
2178 SUBGOAL_THEN`norm(p:real^3) pow 2+ norm(p-u:real^3) pow 2= norm(u) pow 2` ASSUME_TAC;
2179 MRESAL_TAC LAW_OF_COSINES[`p:real^3`;`u:real^3`;`vec 0:real^3`][dist;VECTOR_ARITH`A- vec 0=A`;REAL_ARITH`A+B=(B+A)- &2* C<=> C= &0`;COS_ANGLE]
2180 THEN EXPAND_TAC"p"
2181 THEN REWRITE_TAC[VECTOR_ARITH`u - (t % (u - w) + w)= (&1- t) % (u - w)/\ vec 0-A= --A`;DOT_RNEG;DOT_LMUL;DOT_RMUL;DOT_RADD]
2182 THEN EXPAND_TAC"t"
2183 THEN REWRITE_TAC[DOT_SQUARE_NORM;VECTOR_ARITH`(inv (norm (u - w)) pow 2 * (w dot (w - u))) * norm (u - w) pow 2 +
2184            (u - w) dot w
2185 =(inv (norm (u - w)) * norm (u - w)) pow 2 * (w dot (w-u)) -
2186            (w-u) dot w`]
2187 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`u:real^3`;`w:real^3`]
2188 THEN MRESA_TAC DOT_SYM[`w:real^3`;`w-u:real^3`]
2189 THEN REWRITE_TAC[REAL_ARITH`(--t * --(&1 pow 2 * ((w - u) dot w) - (w - u) dot w)) /
2190        (norm (--t % (u - w)) * norm (--p))= &0`]
2191 THEN REAL_ARITH_TAC;
2192 SUBGOAL_THEN`norm(p:real^3) pow 2+ norm(p-v:real^3) pow 2= norm(v) pow 2` ASSUME_TAC;
2193 MRESAL_TAC LAW_OF_COSINES[`p:real^3`;`v:real^3`;`vec 0:real^3`][dist;VECTOR_ARITH`A- vec 0=A`;REAL_ARITH`A+B=(B+A)- &2* C<=> C= &0`;COS_ANGLE]
2194 THEN FIND_ASSUM MP_TAC`v IN segment [u,w:real^3]`
2195 THEN REWRITE_TAC[IN_SEGMENT]
2196 THEN RESA_TAC
2197 THEN EXPAND_TAC"p"
2198 THEN REWRITE_TAC[VECTOR_ARITH`((&1 - u') % u + u' % w) - (t % (u - w) + w)
2199 = (&1 - u'-t) % (u - w) /\ vec 0-A= --A`;DOT_RNEG;DOT_LMUL;DOT_RMUL;DOT_RADD]
2200 THEN EXPAND_TAC"t"
2201 THEN REWRITE_TAC[DOT_SQUARE_NORM;VECTOR_ARITH`(inv (norm (u - w)) pow 2 * (w dot (w - u))) * norm (u - w) pow 2 +
2202            (u - w) dot w
2203 =(inv (norm (u - w)) * norm (u - w)) pow 2 * (w dot (w-u)) -
2204            (w-u) dot w`]
2205 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`u:real^3`;`w:real^3`]
2206 THEN MRESA_TAC DOT_SYM[`w:real^3`;`w-u:real^3`]
2207 THEN REWRITE_TAC[REAL_ARITH`(--t * --(&1 pow 2 * ((w - u) dot w) - (w - u) dot w)) /
2208        (norm (--t % (u - w)) * norm (--p))= &0`]
2209 THEN REAL_ARITH_TAC;
2210 STRIP_TAC;
2211 SUBGOAL_THEN`&2<= norm(p-w:real^3)`ASSUME_TAC;
2212 MRESAL_TAC DIST_IN_CLOSED_SEGMENT[`p:real^3`;`w:real^3`;`u:real^3`][dist]
2213 THEN MRESA1_TAC packing`{u,v,w:real^3}`
2214 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`u:real^3`;`w:real^3`][SET_RULE`{u, v, w} u /\ {u, v, w} w`;dist])
2215 THEN POP_ASSUM MP_TAC
2216 THEN POP_ASSUM MP_TAC
2217 THEN REAL_ARITH_TAC;
2218 SUBGOAL_THEN`norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`ASSUME_TAC;
2219 MATCH_MP_TAC(REAL_ARITH`&4 <= norm (p - w:real^3) pow 2/\ norm p pow 2 + norm (p - w:real^3) pow 2 = norm w pow 2 /\ norm w pow 2 <= (&2 * h0) pow 2 ==> norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`)
2220 THEN ASM_REWRITE_TAC[]
2221 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(p-w:real^3)`][REAL_ARITH`&0<= &2/\ &2 pow 2= &4`;NORM_POS_LE]
2222 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm (w:real^3)`;`&2 * h0`][REAL_ARITH`&0 <= &2 * #1.26/\ &2 pow 2= &4`;NORM_POS_LE; h0]
2223 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2224 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2225 ==> w IN ball_annulus`)
2226 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;h0]
2227 THEN RESA_TAC;
2228 SUBGOAL_THEN`&0<=  &2 pow 2 -norm (p:real^3) pow 2` ASSUME_TAC;
2229 MATCH_MP_TAC(REAL_ARITH`A<=(&2 * h0) pow 2 - &4/\  (&2 * h0) pow 2 - &4<=  &2 pow 2 ==> &0<= &2 pow 2 -A`)
2230 THEN ASM_REWRITE_TAC[h0]
2231 THEN REAL_ARITH_TAC;
2232 MRESAL_TAC between[`p:real^3`;`u:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT;dist]
2233 THEN POP_ASSUM MP_TAC
2234 THEN MRESAL_TAC SQRT_UNIQUE[`norm (w:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-w:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2235 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2236 THEN MRESAL_TAC SQRT_UNIQUE[`norm (u:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-u:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2237 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2238 THEN REWRITE_TAC[REAL_ARITH`A=B+C<=> C= A-B`]
2239 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2240 ==> w IN ball_annulus/\ u IN ball_annulus /\ v IN ball_annulus`)
2241 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;ball;REAL_ARITH`~(a< &2)<=> &2<= a`]
2242 THEN STRIP_TAC
2243 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm(w:real^3)`;`&2 * h0`][NORM_POS_LE;h0;REAL_ARITH`&0 <= &2 * #1.26`]
2244 THEN POP_ASSUM MP_TAC
2245 THEN REWRITE_TAC[SYM h0]
2246 THEN STRIP_TAC
2247 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(u:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
2248 THEN MP_TAC(REAL_ARITH`
2249 norm (w:real^3) pow 2<= (&2 * h0) pow 2
2250 /\ &2 pow 2 <= norm (u:real^3) pow 2
2251 ==>
2252 norm w pow 2 - norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - norm p pow 2
2253 /\ &2 pow 2 - norm p pow 2<= norm u pow 2 - norm p pow 2 `)
2254 THEN RESA_TAC
2255 THEN MRESAL_TAC SQRT_MONO_LE[`norm (w:real^3) pow 2 - norm (p:real^3) pow 2`;`(&2 * h0) pow 2 - norm (p:real^3) pow 2`][REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2256 THEN MRESAL_TAC SQRT_MONO_LE[`&2 pow 2 - norm (p:real^3) pow 2 `;`norm (u:real^3) pow 2 -  norm (p:real^3) pow 2`][]
2257 THEN STRIP_TAC
2258 THEN MP_TAC(REAL_ARITH`norm (u - w:real^3) =
2259    sqrt (norm w pow 2 - norm p pow 2) - sqrt (norm u pow 2 - norm p pow 2)
2260 /\ sqrt (norm w pow 2 - norm (p:real^3) pow 2) <=
2261       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2262 /\ sqrt (&2 pow 2 - norm p pow 2) <= sqrt (norm u pow 2 - norm p pow 2)
2263 ==> norm (u - w:real^3) <= sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)`)
2264 THEN RESA_TAC
2265 THEN POP_ASSUM MP_TAC
2266 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2267 THEN SUBGOAL_THEN`~(sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) + sqrt (&2 pow 2 - norm p pow 2)= &0)` ASSUME_TAC;
2268 MRESAL_TAC SQRT_UNIQUE[`norm (w:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-w:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2269 THEN MATCH_MP_TAC(REAL_ARITH`~(A= &0/\B= &0) /\ &0<= A /\ &0<= B ==> ~(A+B= &0)`)
2270 THEN MRESA1_TAC SQRT_POS_LE`&2 pow 2 - norm (p:real^3) pow 2`
2271 THEN MP_TAC(REAL_ARITH`sqrt (norm w pow 2 - norm p pow 2) <=
2272       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2273 /\ sqrt (norm w pow 2 - norm p pow 2) = norm (p - w:real^3)
2274 /\ &0 <= norm (p - w)
2275 ==> &0 <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2276 `)
2277 THEN ASM_REWRITE_TAC[NORM_POS_LE]
2278 THEN RESA_TAC
2279 THEN MP_TAC(REAL_ARITH` (norm w pow 2 - norm p pow 2) <=
2280        ((&2 * h0) pow 2 - norm p pow 2)
2281 /\   norm p pow 2 +norm (p - w:real^3) pow 2 =norm w pow 2
2282 /\  &0<= norm (p-w) pow 2
2283 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2284 `)
2285 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2286 THEN RESA_TAC
2287 THEN MRESA1_TAC SQRT_EQ_0`(&2 * h0) pow 2 - norm (p:real^3) pow 2`
2288 THEN MRESA1_TAC SQRT_EQ_0`(&2 ) pow 2 - norm (p:real^3) pow 2`
2289 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> B=A`]
2290 THEN STRIP_TAC
2291 THEN POP_ASSUM MP_TAC
2292 THEN ASM_REWRITE_TAC[h0]
2293 THEN REAL_ARITH_TAC;
2294 MRESA1_TAC REAL_MUL_LINV`sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) +
2295         sqrt (&2 pow 2 - norm p pow 2)`
2296 THEN ONCE_REWRITE_TAC[REAL_ARITH`sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)= &1 *(sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2))`]
2297 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`(A*(B+C))*(B-C)=A* (B pow 2- C pow 2)`])
2298 THEN MP_TAC(REAL_ARITH` (norm w pow 2 - norm p pow 2) <=
2299        ((&2 * h0) pow 2 - norm p pow 2)
2300 /\   norm p pow 2 +norm (p - w:real^3) pow 2 =norm w pow 2
2301 /\  &0<= norm (p-w) pow 2
2302 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2303 `)
2304 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2305 THEN RESA_TAC
2306 THEN MRESAL1_TAC  SQRT_POW_2`(&2 * h0) pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2307 THEN MRESAL1_TAC  SQRT_POW_2`&2 pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (u:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm u pow 2 - (norm p pow 2+ norm(p-u:real^3) pow 2) + norm(p-u:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2308 THEN REWRITE_TAC[REAL_ARITH`A-B-(C-B)=A-C`]
2309 THEN MP_TAC( REAL_ARITH`
2310 norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - &4
2311 ==>
2312 &4<= (&2 * h0) pow 2 - norm p pow 2 /\ &8 - (&2 * h0) pow 2<= &2 pow 2 - norm p pow 2`)
2313 THEN RESA_TAC
2314 THEN MRESAL_TAC SQRT_MONO_LE[`&4`;`(&2 *h0) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2315 THEN SUBGOAL_THEN`&0 <= &8 - (&2 * h0) pow 2`ASSUME_TAC;
2316 REWRITE_TAC[h0]
2317 THEN REAL_ARITH_TAC;
2318 MRESAL_TAC SQRT_MONO_LE[`&8 - (&2 * h0) pow 2`;`(&2 ) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2319 THEN MP_TAC(REAL_ARITH`sqrt (&8 - (&2 * h0) pow 2) <= sqrt (&2 pow 2 - norm p pow 2)/\ sqrt (&4) <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2320 ==> sqrt (&8 - (&2 * h0) pow 2)+ sqrt (&4) <= sqrt (&2 pow 2 - norm p pow 2)+ sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`)
2321 THEN RESA_TAC
2322 THEN SUBGOAL_THEN`&0 < sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)` ASSUME_TAC;
2323 MATCH_MP_TAC(REAL_ARITH`&0< A/\ &0<B ==> &0< A+B`)
2324 THEN STRIP_TAC
2325 THEN MATCH_MP_TAC SQRT_POS_LT
2326 THEN REWRITE_TAC[h0]
2327 THEN REAL_ARITH_TAC;
2328 SUBGOAL_THEN`&0 <= (&2 * h0) pow 2 - &2 pow 2`ASSUME_TAC;
2329 REWRITE_TAC[h0]
2330 THEN REAL_ARITH_TAC;
2331 MRESA_TAC REAL_LE_INV2[`sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)`;`sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`]
2332 THEN MRESA_TAC REAL_LE_RMUL[`inv(sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2))`;`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`]
2333 THEN SUBGOAL_THEN`inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2334       ((&2 * h0) pow 2 - &2 pow 2)< &2` ASSUME_TAC;
2335 MP_TAC(REAL_ARITH` &0< sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) ==> ~(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) = &0)`)
2336 THEN RESA_TAC
2337 THEN MRESA1_TAC REAL_MUL_LINV`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`
2338 THEN MRESAL_TAC REAL_LT_LMUL[`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`;`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) * &2`][REAL_ARITH`A*(B*C)=(A*B)*C/\ &1 *A=A`]
2339 THEN POP_ASSUM MATCH_MP_TAC
2340 THEN STRIP_TAC;
2341 MATCH_MP_TAC REAL_LT_INV
2342 THEN ASM_REWRITE_TAC[];
2343 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2/\ abs(&2)= &2`;POW_2_SQRT_ABS;]
2344 THEN MATCH_MP_TAC(REAL_ARITH`
2345  h0 pow 2 <  &2/\ &0< sqrt (&8 - (&2 * h0) pow 2)
2346 ==>
2347 (&2 * h0) pow 2 - &2 pow 2 < (sqrt (&8 - (&2 * h0) pow 2) + &2) * &2
2348 `)
2349 THEN STRIP_TAC;
2350 REWRITE_TAC[h0]
2351 THEN REAL_ARITH_TAC;
2352 MATCH_MP_TAC SQRT_POS_LT
2353 THEN REWRITE_TAC[h0]
2354 THEN REAL_ARITH_TAC;
2355 STRIP_TAC
2356 THEN MP_TAC(REAL_ARITH`inv
2357       (sqrt (&2 pow 2 - norm (p:real^3) pow 2) +
2358        sqrt ((&2 * h0) pow 2 - norm p pow 2)) *
2359       ((&2 * h0) pow 2 - &2 pow 2) <=
2360       inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2361       ((&2 * h0) pow 2 - &2 pow 2)
2362 /\ inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2363       ((&2 * h0) pow 2 - &2 pow 2) <
2364       &2
2365 /\ norm (u - w) <=
2366    inv
2367    (sqrt ((&2 * h0) pow 2 - norm p pow 2) + sqrt (&2 pow 2 - norm p pow 2)) *
2368    ((&2 * h0) pow 2 - &2 pow 2)
2369 ==> norm(u-w:real^3)< &2`)
2370 THEN RESA_TAC;
2371 MRESA1_TAC( GEN_ALL packing_lt)`{u,v,w:real^3}`
2372 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`u:real^3`;`w:real^3`][SET_RULE`u IN {u, v, w}`;]);
2373 SET_TAC[];
2374 ASM_REWRITE_TAC[dist];
2375 MRESA_TAC UNION_SEGMENT[`w:real^3`;`p:real^3`;`u:real^3`]
2376 THEN FIND_ASSUM MP_TAC`v IN segment [u,w:real^3]`
2377 THEN REWRITE_TAC[]
2378 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2379 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;UNION;IN_ELIM_THM])
2380 THEN STRIP_TAC;
2381 POP_ASSUM MP_TAC
2382 THEN REWRITE_TAC[]
2383 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2384 THEN STRIP_TAC
2385 THEN SUBGOAL_THEN`&2<= norm(p-w:real^3)`ASSUME_TAC;
2386 MRESAL_TAC DIST_IN_CLOSED_SEGMENT[`p:real^3`;`w:real^3`;`v:real^3`][dist]
2387 THEN MRESA1_TAC packing`{u,v,w:real^3}`
2388 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`v:real^3`;`w:real^3`][SET_RULE`{u, v, w} v /\ {u, v, w} w`;dist])
2389 THEN POP_ASSUM MP_TAC
2390 THEN POP_ASSUM MP_TAC
2391 THEN REAL_ARITH_TAC;
2392 SUBGOAL_THEN`norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`ASSUME_TAC;
2393 MATCH_MP_TAC(REAL_ARITH`&4 <= norm (p - w:real^3) pow 2/\ norm p pow 2 + norm (p - w:real^3) pow 2 = norm w pow 2 /\ norm w pow 2 <= (&2 * h0) pow 2 ==> norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`)
2394 THEN ASM_REWRITE_TAC[]
2395 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(p-w:real^3)`][REAL_ARITH`&0<= &2/\ &2 pow 2= &4`;NORM_POS_LE]
2396 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm (w:real^3)`;`&2 * h0`][REAL_ARITH`&0 <= &2 * #1.26/\ &2 pow 2= &4`;NORM_POS_LE; h0]
2397 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2398 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2399 ==> w IN ball_annulus`)
2400 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;h0]
2401 THEN RESA_TAC;
2402 SUBGOAL_THEN`&0<=  &2 pow 2 -norm (p:real^3) pow 2` ASSUME_TAC;
2403 MATCH_MP_TAC(REAL_ARITH`A<=(&2 * h0) pow 2 - &4/\  (&2 * h0) pow 2 - &4<=  &2 pow 2 ==> &0<= &2 pow 2 -A`)
2404 THEN ASM_REWRITE_TAC[h0]
2405 THEN REAL_ARITH_TAC;
2406 MRESAL_TAC between[`p:real^3`;`v:real^3`;`w:real^3`][BETWEEN_IN_SEGMENT;dist]
2407 THEN POP_ASSUM MP_TAC
2408 THEN MRESAL_TAC SQRT_UNIQUE[`norm (w:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-w:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2409 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2410 THEN MRESAL_TAC SQRT_UNIQUE[`norm (v:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-v:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2411 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2412 THEN REWRITE_TAC[REAL_ARITH`A=B+C<=> C= A-B`]
2413 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2414 ==> w IN ball_annulus/\ u IN ball_annulus /\ v IN ball_annulus`)
2415 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;ball;REAL_ARITH`~(a< &2)<=> &2<= a`]
2416 THEN STRIP_TAC
2417 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm(w:real^3)`;`&2 * h0`][NORM_POS_LE;h0;REAL_ARITH`&0 <= &2 * #1.26`]
2418 THEN POP_ASSUM MP_TAC
2419 THEN REWRITE_TAC[SYM h0]
2420 THEN STRIP_TAC
2421 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(v:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
2422 THEN MP_TAC(REAL_ARITH`
2423 norm (w:real^3) pow 2<= (&2 * h0) pow 2
2424 /\ &2 pow 2 <= norm (v:real^3) pow 2
2425 ==>
2426 norm w pow 2 - norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - norm p pow 2
2427 /\ &2 pow 2 - norm p pow 2<= norm v pow 2 - norm p pow 2 `)
2428 THEN RESA_TAC
2429 THEN MRESAL_TAC SQRT_MONO_LE[`norm (w:real^3) pow 2 - norm (p:real^3) pow 2`;`(&2 * h0) pow 2 - norm (p:real^3) pow 2`][REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2430 THEN MRESAL_TAC SQRT_MONO_LE[`&2 pow 2 - norm (p:real^3) pow 2 `;`norm (v:real^3) pow 2 -  norm (p:real^3) pow 2`][]
2431 THEN STRIP_TAC
2432 THEN MP_TAC(REAL_ARITH`norm (v - w:real^3) =
2433    sqrt (norm w pow 2 - norm p pow 2) - sqrt (norm v pow 2 - norm p pow 2)
2434 /\ sqrt (norm w pow 2 - norm (p:real^3) pow 2) <=
2435       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2436 /\ sqrt (&2 pow 2 - norm p pow 2) <= sqrt (norm v pow 2 - norm p pow 2)
2437 ==> norm (v - w:real^3) <= sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)`)
2438 THEN RESA_TAC
2439 THEN POP_ASSUM MP_TAC
2440 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2441 THEN SUBGOAL_THEN`~(sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) + sqrt (&2 pow 2 - norm p pow 2)= &0)` ASSUME_TAC;
2442 MRESAL_TAC SQRT_UNIQUE[`norm (w:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-w:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2443 THEN MATCH_MP_TAC(REAL_ARITH`~(A= &0/\B= &0) /\ &0<= A /\ &0<= B ==> ~(A+B= &0)`)
2444 THEN MRESA1_TAC SQRT_POS_LE`&2 pow 2 - norm (p:real^3) pow 2`
2445 THEN MP_TAC(REAL_ARITH`sqrt (norm w pow 2 - norm p pow 2) <=
2446       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2447 /\ sqrt (norm w pow 2 - norm p pow 2) = norm (p - w:real^3)
2448 /\ &0 <= norm (p - w)
2449 ==> &0 <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2450 `)
2451 THEN ASM_REWRITE_TAC[NORM_POS_LE]
2452 THEN RESA_TAC
2453 THEN MP_TAC(REAL_ARITH` (norm w pow 2 - norm p pow 2) <=
2454        ((&2 * h0) pow 2 - norm p pow 2)
2455 /\   norm p pow 2 +norm (p - w:real^3) pow 2 =norm w pow 2
2456 /\  &0<= norm (p-w) pow 2
2457 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2458 `)
2459 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2460 THEN RESA_TAC
2461 THEN MRESA1_TAC SQRT_EQ_0`(&2 * h0) pow 2 - norm (p:real^3) pow 2`
2462 THEN MRESA1_TAC SQRT_EQ_0`(&2 ) pow 2 - norm (p:real^3) pow 2`
2463 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> B=A`]
2464 THEN STRIP_TAC
2465 THEN POP_ASSUM MP_TAC
2466 THEN ASM_REWRITE_TAC[h0]
2467 THEN REAL_ARITH_TAC;
2468 MRESA1_TAC REAL_MUL_LINV`sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) +
2469         sqrt (&2 pow 2 - norm p pow 2)`
2470 THEN ONCE_REWRITE_TAC[REAL_ARITH`sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)= &1 *(sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2))`]
2471 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`(A*(B+C))*(B-C)=A* (B pow 2- C pow 2)`])
2472 THEN MP_TAC(REAL_ARITH` (norm w pow 2 - norm p pow 2) <=
2473        ((&2 * h0) pow 2 - norm p pow 2)
2474 /\   norm p pow 2 +norm (p - w:real^3) pow 2 =norm w pow 2
2475 /\  &0<= norm (p-w) pow 2
2476 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2477 `)
2478 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2479 THEN RESA_TAC
2480 THEN MRESAL1_TAC  SQRT_POW_2`(&2 * h0) pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2481 THEN MRESAL1_TAC  SQRT_POW_2`&2 pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (u:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm u pow 2 - (norm p pow 2+ norm(p-u:real^3) pow 2) + norm(p-u:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2482 THEN REWRITE_TAC[REAL_ARITH`A-B-(C-B)=A-C`]
2483 THEN MP_TAC( REAL_ARITH`
2484 norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - &4
2485 ==>
2486 &4<= (&2 * h0) pow 2 - norm p pow 2 /\ &8 - (&2 * h0) pow 2<= &2 pow 2 - norm p pow 2`)
2487 THEN RESA_TAC
2488 THEN MRESAL_TAC SQRT_MONO_LE[`&4`;`(&2 *h0) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2489 THEN SUBGOAL_THEN`&0 <= &8 - (&2 * h0) pow 2`ASSUME_TAC;
2490 REWRITE_TAC[h0]
2491 THEN REAL_ARITH_TAC;
2492 MRESAL_TAC SQRT_MONO_LE[`&8 - (&2 * h0) pow 2`;`(&2 ) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2493 THEN MP_TAC(REAL_ARITH`sqrt (&8 - (&2 * h0) pow 2) <= sqrt (&2 pow 2 - norm p pow 2)/\ sqrt (&4) <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2494 ==> sqrt (&8 - (&2 * h0) pow 2)+ sqrt (&4) <= sqrt (&2 pow 2 - norm p pow 2)+ sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`)
2495 THEN RESA_TAC
2496 THEN SUBGOAL_THEN`&0 < sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)` ASSUME_TAC;
2497 MATCH_MP_TAC(REAL_ARITH`&0< A/\ &0<B ==> &0< A+B`)
2498 THEN STRIP_TAC
2499 THEN MATCH_MP_TAC SQRT_POS_LT
2500 THEN REWRITE_TAC[h0]
2501 THEN REAL_ARITH_TAC;
2502 SUBGOAL_THEN`&0 <= (&2 * h0) pow 2 - &2 pow 2`ASSUME_TAC;
2503 REWRITE_TAC[h0]
2504 THEN REAL_ARITH_TAC;
2505 MRESA_TAC REAL_LE_INV2[`sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)`;`sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`]
2506 THEN MRESA_TAC REAL_LE_RMUL[`inv(sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2))`;`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`]
2507 THEN SUBGOAL_THEN`inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2508       ((&2 * h0) pow 2 - &2 pow 2)< &2` ASSUME_TAC;
2509 MP_TAC(REAL_ARITH` &0< sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) ==> ~(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) = &0)`)
2510 THEN RESA_TAC
2511 THEN MRESA1_TAC REAL_MUL_LINV`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`
2512 THEN MRESAL_TAC REAL_LT_LMUL[`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`;`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) * &2`][REAL_ARITH`A*(B*C)=(A*B)*C/\ &1 *A=A`]
2513 THEN POP_ASSUM MATCH_MP_TAC
2514 THEN STRIP_TAC;
2515 MATCH_MP_TAC REAL_LT_INV
2516 THEN ASM_REWRITE_TAC[];
2517 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2/\ abs(&2)= &2`;POW_2_SQRT_ABS;]
2518 THEN MATCH_MP_TAC(REAL_ARITH`
2519  h0 pow 2 <  &2/\ &0< sqrt (&8 - (&2 * h0) pow 2)
2520 ==>
2521 (&2 * h0) pow 2 - &2 pow 2 < (sqrt (&8 - (&2 * h0) pow 2) + &2) * &2
2522 `)
2523 THEN STRIP_TAC;
2524 REWRITE_TAC[h0]
2525 THEN REAL_ARITH_TAC;
2526 MATCH_MP_TAC SQRT_POS_LT
2527 THEN REWRITE_TAC[h0]
2528 THEN REAL_ARITH_TAC;
2529 STRIP_TAC
2530 THEN MP_TAC(REAL_ARITH`inv
2531       (sqrt (&2 pow 2 - norm (p:real^3) pow 2) +
2532        sqrt ((&2 * h0) pow 2 - norm p pow 2)) *
2533       ((&2 * h0) pow 2 - &2 pow 2) <=
2534       inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2535       ((&2 * h0) pow 2 - &2 pow 2)
2536 /\ inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2537       ((&2 * h0) pow 2 - &2 pow 2) <
2538       &2
2539 /\ norm (v - w) <=
2540    inv
2541    (sqrt ((&2 * h0) pow 2 - norm p pow 2) + sqrt (&2 pow 2 - norm p pow 2)) *
2542    ((&2 * h0) pow 2 - &2 pow 2)
2543 ==> norm(v-w:real^3)< &2`)
2544 THEN RESA_TAC;
2545 MRESA1_TAC( GEN_ALL packing_lt)`{u,v,w:real^3}`
2546 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`v:real^3`;`w:real^3`][SET_RULE`v IN {u, v, w}`;]);
2547 SET_TAC[];
2548 ASM_REWRITE_TAC[dist];
2549 SUBGOAL_THEN`&2<= norm(p-u:real^3)`ASSUME_TAC;
2550 MRESAL_TAC DIST_IN_CLOSED_SEGMENT[`p:real^3`;`u:real^3`;`v:real^3`][dist]
2551 THEN MRESA1_TAC packing`{u,v,w:real^3}`
2552 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`v:real^3`;`u:real^3`][SET_RULE`{u, v, w} v /\ {u, v, w} u`;dist])
2553 THEN POP_ASSUM MP_TAC
2554 THEN POP_ASSUM MP_TAC
2555 THEN REAL_ARITH_TAC;
2556 SUBGOAL_THEN`norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`ASSUME_TAC;
2557 MATCH_MP_TAC(REAL_ARITH`&4 <= norm (p - u:real^3) pow 2/\ norm p pow 2 + norm (p - u:real^3) pow 2 = norm u pow 2 /\ norm u pow 2 <= (&2 * h0) pow 2 ==> norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`)
2558 THEN ASM_REWRITE_TAC[]
2559 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(p-u:real^3)`][REAL_ARITH`&0<= &2/\ &2 pow 2= &4`;NORM_POS_LE]
2560 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm (u:real^3)`;`&2 * h0`][REAL_ARITH`&0 <= &2 * #1.26/\ &2 pow 2= &4`;NORM_POS_LE; h0]
2561 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2562 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2563 ==> u IN ball_annulus`)
2564 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;h0]
2565 THEN RESA_TAC;
2566 SUBGOAL_THEN`&0<=  &2 pow 2 -norm (p:real^3) pow 2` ASSUME_TAC;
2567 MATCH_MP_TAC(REAL_ARITH`A<=(&2 * h0) pow 2 - &4/\  (&2 * h0) pow 2 - &4<=  &2 pow 2 ==> &0<= &2 pow 2 -A`)
2568 THEN ASM_REWRITE_TAC[h0]
2569 THEN REAL_ARITH_TAC;
2570 MRESAL_TAC between[`p:real^3`;`v:real^3`;`u:real^3`][BETWEEN_IN_SEGMENT;dist]
2571 THEN POP_ASSUM MP_TAC
2572 THEN MRESAL_TAC SQRT_UNIQUE[`norm (u:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-u:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2573 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2574 THEN MRESAL_TAC SQRT_UNIQUE[`norm (v:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-v:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2575 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2576 THEN REWRITE_TAC[REAL_ARITH`A=B+C<=> C= A-B`]
2577 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2578 ==> w IN ball_annulus/\ u IN ball_annulus /\ v IN ball_annulus`)
2579 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;ball;REAL_ARITH`~(a< &2)<=> &2<= a`]
2580 THEN STRIP_TAC
2581 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm(u:real^3)`;`&2 * h0`][NORM_POS_LE;h0;REAL_ARITH`&0 <= &2 * #1.26`]
2582 THEN POP_ASSUM MP_TAC
2583 THEN REWRITE_TAC[SYM h0]
2584 THEN STRIP_TAC
2585 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(v:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
2586 THEN MP_TAC(REAL_ARITH`
2587 norm (u:real^3) pow 2<= (&2 * h0) pow 2
2588 /\ &2 pow 2 <= norm (v:real^3) pow 2
2589 ==>
2590 norm u pow 2 - norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - norm p pow 2
2591 /\ &2 pow 2 - norm p pow 2<= norm v pow 2 - norm p pow 2 `)
2592 THEN RESA_TAC
2593 THEN MRESAL_TAC SQRT_MONO_LE[`norm (u:real^3) pow 2 - norm (p:real^3) pow 2`;`(&2 * h0) pow 2 - norm (p:real^3) pow 2`][REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2594 THEN MRESAL_TAC SQRT_MONO_LE[`&2 pow 2 - norm (p:real^3) pow 2 `;`norm (v:real^3) pow 2 -  norm (p:real^3) pow 2`][]
2595 THEN STRIP_TAC
2596 THEN MP_TAC(REAL_ARITH`norm (v - u:real^3) =
2597    sqrt (norm u pow 2 - norm p pow 2) - sqrt (norm v pow 2 - norm p pow 2)
2598 /\ sqrt (norm u pow 2 - norm (p:real^3) pow 2) <=
2599       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2600 /\ sqrt (&2 pow 2 - norm p pow 2) <= sqrt (norm v pow 2 - norm p pow 2)
2601 ==> norm (v - u:real^3) <= sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)`)
2602 THEN RESA_TAC
2603 THEN POP_ASSUM MP_TAC
2604 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2605 THEN SUBGOAL_THEN`~(sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) + sqrt (&2 pow 2 - norm p pow 2)= &0)` ASSUME_TAC;
2606 MRESAL_TAC SQRT_UNIQUE[`norm (u:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-u:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2607 THEN MATCH_MP_TAC(REAL_ARITH`~(A= &0/\B= &0) /\ &0<= A /\ &0<= B ==> ~(A+B= &0)`)
2608 THEN MRESA1_TAC SQRT_POS_LE`&2 pow 2 - norm (p:real^3) pow 2`
2609 THEN MP_TAC(REAL_ARITH`sqrt (norm u pow 2 - norm p pow 2) <=
2610       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2611 /\ sqrt (norm u pow 2 - norm p pow 2) = norm (p - u:real^3)
2612 /\ &0 <= norm (p - u)
2613 ==> &0 <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2614 `)
2615 THEN ASM_REWRITE_TAC[NORM_POS_LE]
2616 THEN RESA_TAC
2617 THEN MP_TAC(REAL_ARITH` (norm u pow 2 - norm p pow 2) <=
2618        ((&2 * h0) pow 2 - norm p pow 2)
2619 /\   norm p pow 2 +norm (p - u:real^3) pow 2 =norm u pow 2
2620 /\  &0<= norm (p-u) pow 2
2621 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2622 `)
2623 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2624 THEN RESA_TAC
2625 THEN MRESA1_TAC SQRT_EQ_0`(&2 * h0) pow 2 - norm (p:real^3) pow 2`
2626 THEN MRESA1_TAC SQRT_EQ_0`(&2 ) pow 2 - norm (p:real^3) pow 2`
2627 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> B=A`]
2628 THEN STRIP_TAC
2629 THEN POP_ASSUM MP_TAC
2630 THEN ASM_REWRITE_TAC[h0]
2631 THEN REAL_ARITH_TAC;
2632 MRESA1_TAC REAL_MUL_LINV`sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) +
2633         sqrt (&2 pow 2 - norm p pow 2)`
2634 THEN ONCE_REWRITE_TAC[REAL_ARITH`sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)= &1 *(sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2))`]
2635 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`(A*(B+C))*(B-C)=A* (B pow 2- C pow 2)`])
2636 THEN MP_TAC(REAL_ARITH` (norm u pow 2 - norm p pow 2) <=
2637        ((&2 * h0) pow 2 - norm p pow 2)
2638 /\   norm p pow 2 +norm (p - u:real^3) pow 2 =norm u pow 2
2639 /\  &0<= norm (p-u) pow 2
2640 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2641 `)
2642 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2643 THEN RESA_TAC
2644 THEN MRESAL1_TAC  SQRT_POW_2`(&2 * h0) pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2645 THEN MRESAL1_TAC  SQRT_POW_2`&2 pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (u:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm u pow 2 - (norm p pow 2+ norm(p-u:real^3) pow 2) + norm(p-u:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2646 THEN REWRITE_TAC[REAL_ARITH`A-B-(C-B)=A-C`]
2647 THEN MP_TAC( REAL_ARITH`
2648 norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - &4
2649 ==>
2650 &4<= (&2 * h0) pow 2 - norm p pow 2 /\ &8 - (&2 * h0) pow 2<= &2 pow 2 - norm p pow 2`)
2651 THEN RESA_TAC
2652 THEN MRESAL_TAC SQRT_MONO_LE[`&4`;`(&2 *h0) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2653 THEN SUBGOAL_THEN`&0 <= &8 - (&2 * h0) pow 2`ASSUME_TAC;
2654 REWRITE_TAC[h0]
2655 THEN REAL_ARITH_TAC;
2656 MRESAL_TAC SQRT_MONO_LE[`&8 - (&2 * h0) pow 2`;`(&2 ) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2657 THEN MP_TAC(REAL_ARITH`sqrt (&8 - (&2 * h0) pow 2) <= sqrt (&2 pow 2 - norm p pow 2)/\ sqrt (&4) <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2658 ==> sqrt (&8 - (&2 * h0) pow 2)+ sqrt (&4) <= sqrt (&2 pow 2 - norm p pow 2)+ sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`)
2659 THEN RESA_TAC
2660 THEN SUBGOAL_THEN`&0 < sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)` ASSUME_TAC;
2661 MATCH_MP_TAC(REAL_ARITH`&0< A/\ &0<B ==> &0< A+B`)
2662 THEN STRIP_TAC
2663 THEN MATCH_MP_TAC SQRT_POS_LT
2664 THEN REWRITE_TAC[h0]
2665 THEN REAL_ARITH_TAC;
2666 SUBGOAL_THEN`&0 <= (&2 * h0) pow 2 - &2 pow 2`ASSUME_TAC;
2667 REWRITE_TAC[h0]
2668 THEN REAL_ARITH_TAC;
2669 MRESA_TAC REAL_LE_INV2[`sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)`;`sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`]
2670 THEN MRESA_TAC REAL_LE_RMUL[`inv(sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2))`;`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`]
2671 THEN SUBGOAL_THEN`inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2672       ((&2 * h0) pow 2 - &2 pow 2)< &2` ASSUME_TAC;
2673 MP_TAC(REAL_ARITH` &0< sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) ==> ~(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) = &0)`)
2674 THEN RESA_TAC
2675 THEN MRESA1_TAC REAL_MUL_LINV`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`
2676 THEN MRESAL_TAC REAL_LT_LMUL[`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`;`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) * &2`][REAL_ARITH`A*(B*C)=(A*B)*C/\ &1 *A=A`]
2677 THEN POP_ASSUM MATCH_MP_TAC
2678 THEN STRIP_TAC;
2679 MATCH_MP_TAC REAL_LT_INV
2680 THEN ASM_REWRITE_TAC[];
2681 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2/\ abs(&2)= &2`;POW_2_SQRT_ABS;]
2682 THEN MATCH_MP_TAC(REAL_ARITH`
2683  h0 pow 2 <  &2/\ &0< sqrt (&8 - (&2 * h0) pow 2)
2684 ==>
2685 (&2 * h0) pow 2 - &2 pow 2 < (sqrt (&8 - (&2 * h0) pow 2) + &2) * &2
2686 `)
2687 THEN STRIP_TAC;
2688 REWRITE_TAC[h0]
2689 THEN REAL_ARITH_TAC;
2690 MATCH_MP_TAC SQRT_POS_LT
2691 THEN REWRITE_TAC[h0]
2692 THEN REAL_ARITH_TAC;
2693 STRIP_TAC
2694 THEN MP_TAC(REAL_ARITH`inv
2695       (sqrt (&2 pow 2 - norm (p:real^3) pow 2) +
2696        sqrt ((&2 * h0) pow 2 - norm p pow 2)) *
2697       ((&2 * h0) pow 2 - &2 pow 2) <=
2698       inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2699       ((&2 * h0) pow 2 - &2 pow 2)
2700 /\ inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2701       ((&2 * h0) pow 2 - &2 pow 2) <
2702       &2
2703 /\ norm (v - u) <=
2704    inv
2705    (sqrt ((&2 * h0) pow 2 - norm p pow 2) + sqrt (&2 pow 2 - norm p pow 2)) *
2706    ((&2 * h0) pow 2 - &2 pow 2)
2707 ==> norm(v-u:real^3)< &2`)
2708 THEN RESA_TAC;
2709 MRESA1_TAC( GEN_ALL packing_lt)`{u,v,w:real^3}`
2710 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`v:real^3`;`u:real^3`][SET_RULE`v IN {u, v, w}`;]);
2711 SET_TAC[];
2712 ASM_REWRITE_TAC[dist];
2713 POP_ASSUM MP_TAC
2714 THEN REWRITE_TAC[]
2715 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2716 THEN STRIP_TAC
2717 THEN SUBGOAL_THEN`&2<= norm(p-u:real^3)`ASSUME_TAC;
2718 MRESAL_TAC DIST_IN_CLOSED_SEGMENT[`p:real^3`;`u:real^3`;`w:real^3`][dist]
2719 THEN MRESA1_TAC packing`{u,v,w:real^3}`
2720 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`w:real^3`;`u:real^3`][SET_RULE`{u, v, w} w /\ {u, v, w} u`;dist])
2721 THEN POP_ASSUM MP_TAC
2722 THEN POP_ASSUM MP_TAC
2723 THEN REAL_ARITH_TAC;
2724 SUBGOAL_THEN`norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`ASSUME_TAC;
2725 MATCH_MP_TAC(REAL_ARITH`&4 <= norm (p - u:real^3) pow 2/\ norm p pow 2 + norm (p - u:real^3) pow 2 = norm u pow 2 /\ norm u pow 2 <= (&2 * h0) pow 2 ==> norm (p:real^3) pow 2<= (&2 * h0) pow 2- &4`)
2726 THEN ASM_REWRITE_TAC[]
2727 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(p-u:real^3)`][REAL_ARITH`&0<= &2/\ &2 pow 2= &4`;NORM_POS_LE]
2728 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm (u:real^3)`;`&2 * h0`][REAL_ARITH`&0 <= &2 * #1.26/\ &2 pow 2= &4`;NORM_POS_LE; h0]
2729 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2730 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2731 ==> u IN ball_annulus`)
2732 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;h0]
2733 THEN RESA_TAC;
2734 SUBGOAL_THEN`&0<=  &2 pow 2 -norm (p:real^3) pow 2` ASSUME_TAC;
2735 MATCH_MP_TAC(REAL_ARITH`A<=(&2 * h0) pow 2 - &4/\  (&2 * h0) pow 2 - &4<=  &2 pow 2 ==> &0<= &2 pow 2 -A`)
2736 THEN ASM_REWRITE_TAC[h0]
2737 THEN REAL_ARITH_TAC;
2738 MRESAL_TAC between[`p:real^3`;`w:real^3`;`u:real^3`][BETWEEN_IN_SEGMENT;dist]
2739 THEN POP_ASSUM MP_TAC
2740 THEN MRESAL_TAC SQRT_UNIQUE[`norm (u:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-u:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2741 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2742 THEN MRESAL_TAC SQRT_UNIQUE[`norm (w:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-w:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2743 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2744 THEN REWRITE_TAC[REAL_ARITH`A=B+C<=> C= A-B`]
2745 THEN MP_TAC(SET_RULE`{u, v, w} SUBSET ball_annulus
2746 ==> w IN ball_annulus/\ u IN ball_annulus /\ v IN ball_annulus`)
2747 THEN ASM_REWRITE_TAC[ball_annulus; cball;IN_ELIM_THM;DIFF;dist;VECTOR_ARITH`vec 0- w= -- w`;NORM_NEG;ball;REAL_ARITH`~(a< &2)<=> &2<= a`]
2748 THEN STRIP_TAC
2749 THEN MRESAL_TAC Trigonometry2.POW2_COND[`norm(u:real^3)`;`&2 * h0`][NORM_POS_LE;h0;REAL_ARITH`&0 <= &2 * #1.26`]
2750 THEN POP_ASSUM MP_TAC
2751 THEN REWRITE_TAC[SYM h0]
2752 THEN STRIP_TAC
2753 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2`;`norm(w:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
2754 THEN MP_TAC(REAL_ARITH`
2755 norm (u:real^3) pow 2<= (&2 * h0) pow 2
2756 /\ &2 pow 2 <= norm (w:real^3) pow 2
2757 ==>
2758 norm u pow 2 - norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - norm p pow 2
2759 /\ &2 pow 2 - norm p pow 2<= norm w pow 2 - norm p pow 2 `)
2760 THEN RESA_TAC
2761 THEN MRESAL_TAC SQRT_MONO_LE[`norm (u:real^3) pow 2 - norm (p:real^3) pow 2`;`(&2 * h0) pow 2 - norm (p:real^3) pow 2`][REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2762 THEN MRESAL_TAC SQRT_MONO_LE[`&2 pow 2 - norm (p:real^3) pow 2 `;`norm (w:real^3) pow 2 -  norm (p:real^3) pow 2`][]
2763 THEN STRIP_TAC
2764 THEN MP_TAC(REAL_ARITH`norm (w - u:real^3) =
2765    sqrt (norm u pow 2 - norm p pow 2) - sqrt (norm w pow 2 - norm p pow 2)
2766 /\ sqrt (norm u pow 2 - norm (p:real^3) pow 2) <=
2767       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2768 /\ sqrt (&2 pow 2 - norm p pow 2) <= sqrt (norm w pow 2 - norm p pow 2)
2769 ==> norm (w - u:real^3) <= sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)`)
2770 THEN RESA_TAC
2771 THEN POP_ASSUM MP_TAC
2772 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2773 THEN SUBGOAL_THEN`~(sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) + sqrt (&2 pow 2 - norm p pow 2)= &0)` ASSUME_TAC;
2774 MRESAL_TAC SQRT_UNIQUE[`norm (u:real^3) pow 2- norm (p:real^3) pow 2`;`norm (p-u:real^3)`][NORM_POS_LE;REAL_ARITH`A=B-C<=> C+A=B`]
2775 THEN MATCH_MP_TAC(REAL_ARITH`~(A= &0/\B= &0) /\ &0<= A /\ &0<= B ==> ~(A+B= &0)`)
2776 THEN MRESA1_TAC SQRT_POS_LE`&2 pow 2 - norm (p:real^3) pow 2`
2777 THEN MP_TAC(REAL_ARITH`sqrt (norm u pow 2 - norm p pow 2) <=
2778       sqrt ((&2 * h0) pow 2 - norm p pow 2)
2779 /\ sqrt (norm u pow 2 - norm p pow 2) = norm (p - u:real^3)
2780 /\ &0 <= norm (p - u)
2781 ==> &0 <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2782 `)
2783 THEN ASM_REWRITE_TAC[NORM_POS_LE]
2784 THEN RESA_TAC
2785 THEN MP_TAC(REAL_ARITH` (norm u pow 2 - norm p pow 2) <=
2786        ((&2 * h0) pow 2 - norm p pow 2)
2787 /\   norm p pow 2 +norm (p - u:real^3) pow 2 =norm u pow 2
2788 /\  &0<= norm (p-u) pow 2
2789 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2790 `)
2791 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2792 THEN RESA_TAC
2793 THEN MRESA1_TAC SQRT_EQ_0`(&2 * h0) pow 2 - norm (p:real^3) pow 2`
2794 THEN MRESA1_TAC SQRT_EQ_0`(&2 ) pow 2 - norm (p:real^3) pow 2`
2795 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> B=A`]
2796 THEN STRIP_TAC
2797 THEN POP_ASSUM MP_TAC
2798 THEN ASM_REWRITE_TAC[h0]
2799 THEN REAL_ARITH_TAC;
2800 MRESA1_TAC REAL_MUL_LINV`sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2) +
2801         sqrt (&2 pow 2 - norm p pow 2)`
2802 THEN ONCE_REWRITE_TAC[REAL_ARITH`sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2)= &1 *(sqrt ((&2 * h0) pow 2 - norm p pow 2) - sqrt (&2 pow 2 - norm p pow 2))`]
2803 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;REAL_ARITH`(A*(B+C))*(B-C)=A* (B pow 2- C pow 2)`])
2804 THEN MP_TAC(REAL_ARITH` (norm u pow 2 - norm p pow 2) <=
2805        ((&2 * h0) pow 2 - norm p pow 2)
2806 /\   norm p pow 2 +norm (p - u:real^3) pow 2 =norm u pow 2
2807 /\  &0<= norm (p-u) pow 2
2808 ==> &0 <= ((&2 * h0) pow 2 - norm p pow 2)
2809 `)
2810 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
2811 THEN RESA_TAC
2812 THEN MRESAL1_TAC  SQRT_POW_2`(&2 * h0) pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (w:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm w pow 2 - (norm p pow 2+ norm(p-w:real^3) pow 2) + norm(p-w:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2813 THEN MRESAL1_TAC  SQRT_POW_2`&2 pow 2 - norm (p:real^3) pow 2`[REAL_ARITH`&0 <= norm (u:real^3) pow 2 - norm (p:real^3) pow 2 <=> &0 <= norm u pow 2 - (norm p pow 2+ norm(p-u:real^3) pow 2) + norm(p-u:real^3) pow 2`;REAL_ARITH`A-A+B=B`;REAL_LE_POW_2]
2814 THEN REWRITE_TAC[REAL_ARITH`A-B-(C-B)=A-C`]
2815 THEN MP_TAC( REAL_ARITH`
2816 norm (p:real^3) pow 2 <= (&2 * h0) pow 2 - &4
2817 ==>
2818 &4<= (&2 * h0) pow 2 - norm p pow 2 /\ &8 - (&2 * h0) pow 2<= &2 pow 2 - norm p pow 2`)
2819 THEN RESA_TAC
2820 THEN MRESAL_TAC SQRT_MONO_LE[`&4`;`(&2 *h0) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2821 THEN SUBGOAL_THEN`&0 <= &8 - (&2 * h0) pow 2`ASSUME_TAC;
2822 REWRITE_TAC[h0]
2823 THEN REAL_ARITH_TAC;
2824 MRESAL_TAC SQRT_MONO_LE[`&8 - (&2 * h0) pow 2`;`(&2 ) pow 2 - norm (p:real^3) pow 2 `][REAL_ARITH`&0<= &4`]
2825 THEN MP_TAC(REAL_ARITH`sqrt (&8 - (&2 * h0) pow 2) <= sqrt (&2 pow 2 - norm p pow 2)/\ sqrt (&4) <= sqrt ((&2 * h0) pow 2 - norm p pow 2)
2826 ==> sqrt (&8 - (&2 * h0) pow 2)+ sqrt (&4) <= sqrt (&2 pow 2 - norm p pow 2)+ sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`)
2827 THEN RESA_TAC
2828 THEN SUBGOAL_THEN`&0 < sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)` ASSUME_TAC;
2829 MATCH_MP_TAC(REAL_ARITH`&0< A/\ &0<B ==> &0< A+B`)
2830 THEN STRIP_TAC
2831 THEN MATCH_MP_TAC SQRT_POS_LT
2832 THEN REWRITE_TAC[h0]
2833 THEN REAL_ARITH_TAC;
2834 SUBGOAL_THEN`&0 <= (&2 * h0) pow 2 - &2 pow 2`ASSUME_TAC;
2835 REWRITE_TAC[h0]
2836 THEN REAL_ARITH_TAC;
2837 MRESA_TAC REAL_LE_INV2[`sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)`;`sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2)`]
2838 THEN MRESA_TAC REAL_LE_RMUL[`inv(sqrt (&2 pow 2 - norm p pow 2) + sqrt ((&2 * h0) pow 2 - norm (p:real^3) pow 2))`;`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`]
2839 THEN SUBGOAL_THEN`inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2840       ((&2 * h0) pow 2 - &2 pow 2)< &2` ASSUME_TAC;
2841 MP_TAC(REAL_ARITH` &0< sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) ==> ~(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4) = &0)`)
2842 THEN RESA_TAC
2843 THEN MRESA1_TAC REAL_MUL_LINV`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`
2844 THEN MRESAL_TAC REAL_LT_LMUL[`inv(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4))`;`((&2 * h0) pow 2 - &2 pow 2)`;`(sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) * &2`][REAL_ARITH`A*(B*C)=(A*B)*C/\ &1 *A=A`]
2845 THEN POP_ASSUM MATCH_MP_TAC
2846 THEN STRIP_TAC;
2847 MATCH_MP_TAC REAL_LT_INV
2848 THEN ASM_REWRITE_TAC[];
2849 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2/\ abs(&2)= &2`;POW_2_SQRT_ABS;]
2850 THEN MATCH_MP_TAC(REAL_ARITH`
2851  h0 pow 2 <  &2/\ &0< sqrt (&8 - (&2 * h0) pow 2)
2852 ==>
2853 (&2 * h0) pow 2 - &2 pow 2 < (sqrt (&8 - (&2 * h0) pow 2) + &2) * &2
2854 `)
2855 THEN STRIP_TAC;
2856 REWRITE_TAC[h0]
2857 THEN REAL_ARITH_TAC;
2858 MATCH_MP_TAC SQRT_POS_LT
2859 THEN REWRITE_TAC[h0]
2860 THEN REAL_ARITH_TAC;
2861 STRIP_TAC
2862 THEN MP_TAC(REAL_ARITH`inv
2863       (sqrt (&2 pow 2 - norm (p:real^3) pow 2) +
2864        sqrt ((&2 * h0) pow 2 - norm p pow 2)) *
2865       ((&2 * h0) pow 2 - &2 pow 2) <=
2866       inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2867       ((&2 * h0) pow 2 - &2 pow 2)
2868 /\ inv (sqrt (&8 - (&2 * h0) pow 2) + sqrt (&4)) *
2869       ((&2 * h0) pow 2 - &2 pow 2) <
2870       &2
2871 /\ norm (w - u) <=
2872    inv
2873    (sqrt ((&2 * h0) pow 2 - norm p pow 2) + sqrt (&2 pow 2 - norm p pow 2)) *
2874    ((&2 * h0) pow 2 - &2 pow 2)
2875 ==> norm(w-u:real^3)< &2`)
2876 THEN RESA_TAC;
2877 MRESA1_TAC( GEN_ALL packing_lt)`{u,v,w:real^3}`
2878 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`w:real^3`;`u:real^3`][SET_RULE`w IN {u, v, w}`;]);
2879 SET_TAC[];
2880 ASM_REWRITE_TAC[dist]]);;
2881
2882
2883 let POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2 =prove(`{u,v,w} SUBSET ball_annulus /\  packing {u,v,w} /\ ~(v = u) /\ ~(v = w) /\ ~(u = w)
2884 ==> ~(collinear{u,v,w})`,
2885 REWRITE_TAC[COLLINEAR_BETWEEN_CASES;BETWEEN_IN_SEGMENT]
2886 THEN REPEAT STRIP_TAC
2887 THENL[MRESA_TAC(GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR)[`u:real^3`;`v:real^3`;`w:real^3`]
2888 THEN ONCE_REWRITE_TAC[SET_RULE`{v,u,w}={u,v,w}`]
2889 THEN ASM_REWRITE_TAC[];
2890 MRESA_TAC(GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR)[`v:real^3`;`w:real^3`;`u:real^3`]
2891 THEN ONCE_REWRITE_TAC[SET_RULE`{w,v,u}={u,v,w}`]
2892 THEN ASM_REWRITE_TAC[];
2893 MRESA_TAC(GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR)[`w:real^3`;`u:real^3`;`v:real^3`]
2894 THEN ONCE_REWRITE_TAC[SET_RULE`{u,w,v}={u,v,w}`]
2895 THEN ASM_REWRITE_TAC[]]);;
2896
2897 let SUBSET_PACKING=prove(`!sub s.
2898          packing s /\ sub SUBSET s
2899          ==> packing sub`,
2900 REPEAT STRIP_TAC
2901 THEN REWRITE_TAC[packing;GSYM dist3]
2902 THEN MRESAL_TAC Geomdetail.SUB_PACKING[`sub:real^3->bool`;`s:real^3->bool`][IN]);;
2903
2904
2905
2906
2907
2908
2909
2910
2911 let VPWSHTO_PRIME=prove(`!vv:num->real^3.
2912 {vv 0,vv 1,vv 2,vv 3,vv 4} SUBSET ball_annulus /\  packing {vv 0,vv 1,vv 2,vv 3,vv 4} /\ ~(vv 0 = vv 1) /\ ~(vv 0 = vv 1) /\ ~(vv 0 = vv 2)/\ ~(vv 0 = vv 3)
2913 /\ ~(vv 0 = vv 4)  /\ ~(vv 1 = vv 2)/\ ~(vv 1 = vv 3)
2914 /\ ~(vv 1 = vv 4) /\ ~(vv 2 = vv 3)
2915 /\ ~(vv 2 = vv 4)/\  ~(vv 3 = vv 4)
2916 /\ norm(vv 0-vv 1)= &2
2917 /\ norm(vv 1-vv 2)= &2
2918 /\ norm(vv 2-vv 3)= &2
2919 /\ norm(vv 3-vv 4)= &2
2920 /\ norm(vv 4-vv 0)= &2
2921 ==>
2922 ?i. i IN 0..4/\ norm(vv i - vv ((i +2) MOD 5) ) <= &1 + sqrt(&5)/\ norm(vv i - vv ((i +3) MOD 5))<= &1 + sqrt(&5)`,
2923 REPEAT STRIP_TAC
2924 THEN MATCH_MP_TAC VPWSHTO
2925 THEN ASM_REWRITE_TAC[]
2926 THEN ABBREV_TAC `v= (vv:num->real^3) 0`
2927 THEN ABBREV_TAC `x= (vv:num->real^3) 1`
2928 THEN ABBREV_TAC `u= (vv:num->real^3) 2`
2929 THEN ABBREV_TAC `w= (vv:num->real^3) 3`
2930 THEN ABBREV_TAC `w1= (vv:num->real^3) 4`
2931 THEN MP_TAC(SET_RULE`{v,x,u,w,w1} SUBSET ball_annulus
2932 ==> {v, x, u} SUBSET ball_annulus /\
2933 {w, x, u} SUBSET ball_annulus /\
2934  {w1, x, u} SUBSET ball_annulus /\
2935  {w, v, u} SUBSET ball_annulus /\
2936  {w1, v, u} SUBSET ball_annulus /\
2937  {w1, w, u} SUBSET ball_annulus /\
2938  {w, v, x} SUBSET ball_annulus /\
2939  {w1, v, x} SUBSET ball_annulus /\
2940  {w1, w, x} SUBSET ball_annulus /\
2941  {w1, w, v} SUBSET ball_annulus `)
2942 THEN RESA_TAC
2943 THEN MRESAL_TAC SUBSET_PACKING[`{v, x, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{v, x, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2944 THEN MRESAL_TAC SUBSET_PACKING[`{w, x, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w, x, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2945 THEN MRESAL_TAC SUBSET_PACKING[`{w1, x, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, x, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2946 THEN MRESAL_TAC SUBSET_PACKING[`{w, v, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w, v, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2947 THEN MRESAL_TAC SUBSET_PACKING[`{w1, v, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, v, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2948 THEN MRESAL_TAC SUBSET_PACKING[`{w1, w, u:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, w, u:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2949 THEN MRESAL_TAC SUBSET_PACKING[`{w, v, x:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w, v, x:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2950 THEN MRESAL_TAC SUBSET_PACKING[`{w1, v, x:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, v, x:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2951 THEN MRESAL_TAC SUBSET_PACKING[`{w1, w, x:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, w, x:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2952 THEN MRESAL_TAC SUBSET_PACKING[`{w1, w, v:real^3}`;`{v,x,u,w,w1:real^3}`][SET_RULE`{w1, w, v:real^3} SUBSET {v,x,u,w,w1:real^3}`]
2953 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`v:real^3`; `x:real^3`; `u:real^3`]
2954 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `x:real^3`; `u:real^3`]
2955 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w:real^3`; `v:real^3`; `u:real^3`]
2956 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `v:real^3`; `u:real^3`]
2957 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w:real^3`; `x:real^3`; `u:real^3`]
2958 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `w:real^3`; `u:real^3`]
2959 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w:real^3`; `v:real^3`; `x:real^3`]
2960 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `v:real^3`; `x:real^3`]
2961 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `w:real^3`; `x:real^3`]
2962 THEN MRESA_TAC (GEN_ALL POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2)[`w1:real^3`; `w:real^3`; `v:real^3`]);;
2963
2964
2965
2966
2967 end;;
2968
2969