legacy/oldfan/JGIYDLE.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11
  12 module  Lead_fan = struct
  13
  14
  15
  16 open Sphere;;
  17 open Fan_defs;;
  18 open Hypermap_of_fan;;
  19 open Tactic_fan;;
  20 open Lemma_fan;;
  21 open Fan;;
  22 open Hypermap_of_fan;;
  23 open Node_fan;;
  24 open Azim_node;;
  25 open Sum_azim_node;;
  26 open Disjoint_fan;;
  27
  28 (* ========================================================================== *)
  29 (*                   DISJOINT IN   FAN                        *)
  30 (* ========================================================================== *)
  31
  32
  33
  34
  35 let exist_fan=prove(`(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
  36
  37 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
  38 ==>
  39 ?h:real.
  40 (&0 < h)
  41 /\
  42 (!y1:real^3 y2:real^3. (y1 IN aff_ge {x} {v} INTER ballnorm_fan x) /\ y2 IN (aff_ge {x} {v1, w1} INTER ballnorm_fan x)
  43 ==> h  <= dist(y1,y2) ))`,
  44 REPEAT STRIP_TAC
  45 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
  46 ` (v:real^3)`] remark1_fan)
  47 THEN RES_TAC
  48 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
  49 ` (v1:real^3)`] remark1_fan)
  50 THEN RES_TAC
  51 THEN MATCH_MP_TAC( ISPECL [`aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x`;
  52  `aff_ge {(x:real^3)} {(v1:real^3), (w1:real^3)} INTER ballnorm_fan x`] SEPARATE_CLOSED_COMPACT)
  53   THEN MP_TAC(ISPECL[`(x:real^3) `;` (v:real^3)`;` (w:real^3)`]closed_point_fan)
  54 THEN RESA_TAC
  55   THEN MP_TAC(ISPECL[`(x:real^3) `;` (v1:real^3)`;` (w1:real^3)`]compact_aff_ge_ballnorm_fan) THEN RESA_TAC
  56   THEN FIND_ASSUM(MP_TAC)`FAN(x:real^3,V,E)`
  57   THEN REWRITE_TAC[FAN;fan7] THEN STRIP_TAC
  58   THEN POP_ASSUM(fun th-> MP_TAC(ISPECL[`{(v:real^3)}`;`{(v1:real^3),(w1:real^3)}`]th))
  59                    THEN ASM_REWRITE_TAC[UNION; IN_ELIM_THM;]
  60   THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[EXTENSION;]
  61   THEN ASM_REWRITE_TAC[IN_SING; SET_RULE`(!x. x = v <=> x = v') <=> v =v'`;SET_RULE`(?v'. v' IN V /\ v = v')<=> v IN V`]
  62   THEN SUBGOAL_THEN `{v:real^3} INTER {v1,w1} ={}` ASSUME_TAC
  63 THENL[
  64 REWRITE_TAC[INTER;IN_SING; EXTENSION; EMPTY; IN_ELIM_THM] THEN ASM_SET_TAC[];
  65
  66 ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; SET_RULE`(A INTER C) INTER (B INTER C)= (A INTER B) INTER C`;]
  67 THEN ASSUME_TAC(AFFINE_SING) THEN MP_TAC(ISPEC`{ (x:real^3) }` AFFINE_HULL_EQ )
  68   THEN RESA_TAC THEN RESA_TAC THEN REWRITE_TAC[ballnorm_fan;INTER; IN_SING; EXTENSION;EMPTY;IN_ELIM_THM;
  69 ] THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[DIST_REFL ] THEN REAL_ARITH_TAC]);;
  70
  71
  72
  73
  74 let ballsets_fan=new_definition`ballsets_fan (s:real^3->bool) (h:real)= {y:real^3| ?x:real^3. dist(x,y) < h /\ x IN s} `;;
  75
  76
  77 let exists_ballsets_fan =prove(
  78 `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
  79 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
  80 ==>
  81 ?h:real.
  82 (&0 < h)
  83 /\ (ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h INTER (aff_ge {x} {v1, w1} INTER ballnorm_fan x) = {})
  84 )`,
  85  REPEAT GEN_TAC THEN DISCH_TAC THEN
  86    MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exist_fan)  THEN RES_TAC
  87    THEN POP_ASSUM MP_TAC  THEN REWRITE_TAC[ballsets_fan; INTER; IN_ELIM_THM]
  88    THEN DISCH_TAC THEN EXISTS_TAC`h:real`
  89    THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;] THEN GEN_TAC THEN EQ_TAC
  90 THENL[
  91  POP_ASSUM MP_TAC
  92    THEN DISCH_THEN(LABEL_TAC"a")
  93    THEN STRIP_TAC THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPECL[`x'':real^3`;`x':real^3`]th))
  94 THEN ASM_REWRITE_TAC[EMPTY;IN_ELIM_THM] THEN REPEAT (POP_ASSUM MP_TAC)
  95    THEN REAL_ARITH_TAC;
  96 REWRITE_TAC[EMPTY;IN_ELIM_THM]]);;
  97
  98
  99
 100
 101 (*-------------------------------------------------------------------------------------------*)
 102 (* cone_ge_fan_inter_aff_ge_is_empty                                                         *)
 103 (*-------------------------------------------------------------------------------------------*)
 104
 105
 106
 107 let cone_ge_fan=new_definition`cone_ge_fan (x:real^3) (s:real^3->bool)= {y:real^3| ?a:real z:real^3. (&0 <= a)/\(z IN s) /\ (y =a % (z - x) + x)}`;;
 108
 109
 110
 111
 112
 113 let cone_ge_fan_inter_aff_ge_is_empty=prove(
 114 `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
 115 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
 116 ==>
 117
 118 ?h:real.
 119 (h > &0)
 120 /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} = {x})
 121 )`,
 122
 123 REPEAT STRIP_TAC
 124 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 125 `(v:real^3)`] remark1_fan)
 126   THEN RES_TAC
 127 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
 128 `(v1:real^3)`] remark1_fan)
 129   THEN RES_TAC
 130 THEN  MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;
 131 `(w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exists_ballsets_fan)
 132 THEN ASM_REWRITE_TAC[]
 133    THEN MATCH_MP_TAC MONO_EXISTS
 134 THEN GEN_TAC THEN STRIP_TAC THEN STRIP_TAC
 135 THENL(*1*)[
 136
 137 ASM_REWRITE_TAC[REAL_ARITH`a> &0 <=> &0< a`];(*1*)
 138  REWRITE_TAC [cone_ge_fan; EXTENSION; IN_SING; INTER; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
 139 THENL(*2*)[
 140  ASM_CASES_TAC `(x':real^3)=(x:real^3)`
 141 THENL(*3*)[ASM_REWRITE_TAC[];(*3*)
 142                        MP_TAC (ISPECL [`x':real^3`; `x:real^3`] imp_norm_not_zero_fan)
 143                                    THEN RES_TAC THEN STRIP_TAC THEN
 144                                            POP_ASSUM MP_TAC THEN  DISCH_THEN(LABEL_TAC "a")
 145                                               THEN REPEAT STRIP_TAC
 146                                               THEN ASM_REWRITE_TAC[]
 147                                               THEN ABBREV_TAC `(x1:real^3)= inv (norm ((x':real^3)-(x:real^3))) % (x'-x) + x`
 148                                               THEN SUBGOAL_THEN `(x1:real^3) IN ballnorm_fan (x:real^3)` ASSUME_TAC
 149 THENL(*4*)[                     REWRITE_TAC[ballnorm_fan; IN_ELIM_THM]
 150                                                         THEN EXPAND_TAC "x1"
 151                                                         THEN REWRITE_TAC[dist]
 152                                                         THEN REWRITE_TAC[VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --(a)`; VECTOR_ARITH `-- ((a:real)% (v:real^3))=(-- a) % v`; NORM_MUL;REAL_ABS_NEG; REAL_ABS_INV; REAL_ABS_NORM]
 153                                                         THEN USE_THEN "a"  MP_TAC
 154                                                         THEN MP_TAC(ISPEC `norm ((x':real^3)-(x:real^3))` REAL_MUL_LINV)
 155                                                         THEN ASM_MESON_TAC[];(*4*)
 156               SUBGOAL_THEN `(x1:real^3) IN aff_ge {(x:real^3)} {(v1:real^3),(w1:real^3)}` ASSUME_TAC
 157 THENL(*5*)[REMOVE_THEN "a" MP_TAC THEN
 158 MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC
 159                                                         THEN REWRITE_TAC[IN_ELIM_THM]
 160   THEN STRIP_TAC THEN
 161                                                         EXISTS_TAC `&1 - inv (norm((x':real^3)-(x:real^3))) + inv (norm (x' - x)) * (t1:real) `
 162                                                         THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t2:real) `
 163                                                         THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t3:real) `
 164                                                         THEN EXPAND_TAC "x1"
 165                                                         THEN REWRITE_TAC[VECTOR_ARITH`((a:real)-(b:real)+(c:real))%(v:real^3)=(a:real) % v -(b:real)% v+(c:real) %(v:real^3)`;
 166 VECTOR_ARITH `&1 % (x:real^3)=x`; VECTOR_ARITH `((a:real)*(b:real)) % (v:real^3)= (a % (b % v))`;
 167 VECTOR_ARITH `(x - inv (norm (x' - x)) % x + inv (norm (x' - x)) % t1 % x) +
 168  inv (norm (x' - x)) % t2 % v1 +
 169  inv (norm (x' - x)) % t3 % w1 =(inv (norm ((x':real^3)- x))) % ( t1 % x + t2 % v1+ t3% w1 -x)+ (x:real^3)`
 170
 171 ]
 172                                                         THEN STRIP_TAC
 173 THENL(*6*)[SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC
 174 THENL(*7*)[                                                                MATCH_MP_TAC REAL_LE_INV
 175                                                                                  THEN MESON_TAC[NORM_POS_LE];(*7*)
 176                                                                                ASM_MESON_TAC[REAL_LE_MUL]](*7*);(*6*)
 177
 178 STRIP_TAC
 179 THENL(*7*)[ SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC
 180 THENL(*8*)[                                                                 MATCH_MP_TAC REAL_LE_INV
 181                                                                           THEN MESON_TAC[NORM_POS_LE];(*8*)
 182    ASM_MESON_TAC[REAL_LE_MUL; REAL_ARITH `(a:real)>= &0 <=> &0 <= a`]](*8*);(*7*)
 183
 184 REWRITE_TAC[REAL_ARITH `(&1 - inv (norm (x' - x)) + inv (norm (x' - x)) * t1) +
 185  inv (norm (x' - x)) * t2 +
 186  inv (norm (x' - x)) * t3= &1 - inv (norm (x' - x)) + inv (norm (x' - x)) * (t1 + t2 + t3)`]
 187     THEN STRIP_TAC
 188 THENL(*8*)[
 189 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `(a:real) * &1 = a`; REAL_ARITH `&1 - (a:real) +(a:real) = &1`];(*8*)
 190
 191 SUBGOAL_THEN `(x':real^3) -(x:real^3)= (t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3)` ASSUME_TAC
 192 THENL(*9*)[ ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;(*9*)
 193     SUBGOAL_THEN `inv (norm   ((x':real^3) -(x:real^3)) )  % ((x':real^3) -(x:real^3)) = inv (norm   ((x':real^3) -(x:real^3)) ) % ((t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3))` ASSUME_TAC
 194 THENL(*10*)[ASM_MESON_TAC[ VECTOR_MUL_LCANCEL ];(*10*)
 195 ASM_MESON_TAC[]](*10*)](*9*)](*8*)](*7*)](*6*); (*5*)
 196
 197 SUBGOAL_THEN `(x1:real^3) IN ballsets_fan (aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x) (h:real)` ASSUME_TAC
 198 THENL(*6*)[
 199  SUBGOAL_THEN `norm ((z:real^3)-(x:real^3))= &1` ASSUME_TAC
 200 THENL(*7*)[FIND_ASSUM(MP_TAC)`z IN ballnorm_fan (x:real^3)`
 201     THEN REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; NORM_SUB];(*7*)
 202     POP_ASSUM MP_TAC
 203     THEN DISCH_THEN (LABEL_TAC "k")
 204     THEN SUBGOAL_THEN `(x':real^3)- (x:real^3)= (a:real) % ((z:real^3)-x )` ASSUME_TAC
 205 THENL(*8*)[ FIND_ASSUM(MP_TAC)`x'=a %(z-x) +x:real^3`  THEN VECTOR_ARITH_TAC;(*8*)
 206
 207 SUBGOAL_THEN `norm((x':real^3)- (x:real^3))= norm((a:real) % ((z:real^3)-x ))` ASSUME_TAC
 208 THENL(*9*)[ASM_SET_TAC[];(*9*)
 209
 210 POP_ASSUM MP_TAC
 211 THEN REWRITE_TAC[NORM_MUL]
 212 THEN     POP_ASSUM MP_TAC
 213          THEN USE_THEN "k" (fun th -> REWRITE_TAC[th])
 214   THEN REDUCE_ARITH_TAC
 215          THEN SUBGOAL_THEN `abs (a:real)=a`ASSUME_TAC
 216     THENL(*10*)[FIND_ASSUM(MP_TAC)`&0 <= a:real` THEN REAL_ARITH_TAC;(*10*)
 217 POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN DISCH_THEN(LABEL_TAC"l")
 218     THEN DISCH_THEN (LABEL_TAC "n")
 219      THEN REMOVE_THEN "l" MP_TAC                                                                                                                     THEN USE_THEN "n" (fun th-> REWRITE_TAC[SYM th])
 220                             THEN DISCH_THEN (LABEL_TAC "l")
 221                                                                              THEN SUBGOAL_THEN `(inv (norm (x'- x))) % ((x':real^3)- (x:real^3)) = (inv (norm (x' - x))) % (norm (x' - x) % ((z:real^3)- x ))` ASSUME_TAC
 222 THENL(*11*)[POP_ASSUM MP_TAC THEN MESON_TAC[];(*11*)
 223                 POP_ASSUM MP_TAC
 224                  THEN REWRITE_TAC[VECTOR_ARITH `(a:real)%(b:real)%(v:real^3)=(a*b)%v`]
 225                   THEN MP_TAC(ISPEC`norm((x':real^3)-(x:real^3))`REAL_MUL_LINV)
 226                   THEN FIND_ASSUM(fun th ->REWRITE_TAC[th]) `~(norm((x':real^3)-(x:real^3))= &0)`
 227                   THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN REDUCE_VECTOR_TAC
 228                  THEN REWRITE_TAC[VECTOR_ARITH `((a:real^3)=(z:real^3)-(x:real^3))<=>(a+x=z)`]
 229                   THEN FIND_ASSUM(fun th-> REWRITE_TAC[th])`inv (norm (x' - x)) % (x' - x) + x = x1:real^3`
 230     THEN DISCH_TAC THEN ASM_REWRITE_TAC[INTER]](*11*)](*10*)](*9*)](*8*)](*7*);(*6*)
 231 ASM_SET_TAC[]](*6*)](*5*)](*4*)](*3*);(*2*)
 232
 233 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 234 THENL(*2*)[ EXISTS_TAC `&0`  THEN EXISTS_TAC`inv (norm ((v:real^3)-(x:real^3))) % (v-x) + x` THEN REDUCE_VECTOR_TAC
 235   THEN STRIP_TAC
 236 THENL(*3*)[ REAL_ARITH_TAC;(*3*)
 237               STRIP_TAC
 238 THENL(*4*)[            REWRITE_TAC[ballsets_fan; IN_ELIM_THM]
 239                      THEN EXISTS_TAC `inv(norm((v:real^3)-(x:real^3))) % (v-x)+x`
 240                      THEN REWRITE_TAC[dist; VECTOR_ARITH `(a)-a= vec 0`; NORM_0]
 241                      THEN STRIP_TAC
 242 THENL(*5*)[    ASM_SET_TAC[];(*5*)
 243
 244 STRIP_TAC
 245 THENL(*6*)[
 246 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC
 247  THEN REWRITE_TAC[IN_ELIM_THM]
 248   THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))`
 249   THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))`
 250  THEN STRIP_TAC
 251 THENL(*7*)[
 252  MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*7*)
 253 STRIP_TAC
 254 THENL(*8*)[ REAL_ARITH_TAC;(*8*)
 255 VECTOR_ARITH_TAC](*8*)](*7*);(*6*)
 256
 257   REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
 258          THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC
 259 THENL(*7*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*7*)
 260
 261 SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC
 262 THENL(*8*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*8*)
 263
 264 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
 265 THENL(*9*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*9*)
 266  POP_ASSUM MP_TAC THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*9*)](*8*)](*7*)](*6*)](*5*);(*4*)
 267 REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
 268              THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC
 269 THENL(*5*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*5*)
 270  SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC
 271 THENL(*6*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*)
 272 POP_ASSUM (fun th -> REWRITE_TAC[th])
 273       THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
 274 THENL(*7*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*7*)
 275         POP_ASSUM MP_TAC  THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*7*)](*6*)](*5*)](*4*)](*3*);(*2*)
 276
 277 MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM]
 278 THEN
 279 EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`
 280   THEN STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]]]]);;
 281
 282
 283 let subset_by_inequality_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3) (h:real) (h1:real).
 284 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E /\ h < h1
 285 ==>
 286  cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET  cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1}
 287 `,
 288 REPEAT STRIP_TAC
 289 THEN  SUBGOAL_THEN` cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x) SUBSET  cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) ` ASSUME_TAC
 290 THENL[
 291 REWRITE_TAC[cone_ge_fan; SUBSET;IN_ELIM_THM]
 292 THEN GEN_TAC
 293 THEN STRIP_TAC
 294 THEN EXISTS_TAC`a:real`
 295 THEN EXISTS_TAC`z:real^3`
 296 THEN ASM_REWRITE_TAC[]
 297 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 298 THEN POP_ASSUM MP_TAC
 299 THEN REWRITE_TAC[ballsets_fan;INTER; IN_ELIM_THM]
 300 THEN RESA_TAC
 301 THEN EXISTS_TAC`x'':real^3`
 302 THEN ASM_REWRITE_TAC[]
 303 THEN REPEAT (POP_ASSUM MP_TAC)
 304 THEN REAL_ARITH_TAC;
 305 ASM_SET_TAC[]]);;
 306
 307
 308
 309 let cone_ge_fan_inter_aff_ge_is_empty_fan=prove( `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
 310 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
 311 ==>
 312
 313 ?h:real.
 314 (&1> h)
 315 /\ (h > &0)
 316 /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET {x})
 317 )`,
 318
 319 REPEAT STRIP_TAC
 320 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;
 321 `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty)
 322 THEN RESA_TAC
 323 THEN DISJ_CASES_TAC(REAL_ARITH `(h >= &1) \/ (&1 > h)` )
 324 THENL[
 325 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;
 326 `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`; `&1/ &2`; `(h:real)`]subset_by_inequality_fan)
 327 THEN RESA_TAC
 328 THEN POP_ASSUM MP_TAC
 329 THEN MP_TAC(REAL_ARITH`h>= &1==> &1 / &2 <h`)
 330 THEN ASM_REWRITE_TAC[]
 331 THEN DISCH_TAC
 332 THEN ASM_REWRITE_TAC[]
 333 THEN DISCH_TAC
 334 THEN EXISTS_TAC `&1/ &2`
 335 THEN ASM_REWRITE_TAC[]
 336 THEN REAL_ARITH_TAC;
 337
 338 EXISTS_TAC      `h:real`
 339 THEN ASM_REWRITE_TAC[]
 340 THEN ASM_SET_TAC[]]);;
 341
 342
 343
 344
 345 let rcone_subset_cone=prove(
 346 `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) h:real.
 347 FAN(x,V,E) /\ {v,w} IN E /\(&0< h) /\ (h< &1)
 348 ==>
 349 ?h1:real.
 350 &1 > h1 /\
 351 h1> &0 /\
 352 (rcone_fan x v h1) SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x )`,
 353
 354 REWRITE_TAC[rcone_fan;cone_ge_fan; SUBSET;IN_ELIM_THM;dist]
 355   THEN REPEAT STRIP_TAC
 356   THEN EXISTS_TAC`(&2 -(h:real) pow 2)/ &2`
 357 THEN STRIP_TAC
 358 THENL[
 359 REWRITE_TAC[REAL_ARITH`&1 > (&2 -(h:real) pow 2)/ &2 <=> h pow 2> &0`]
 360 THEN MP_TAC (ISPECL[`h:real`;`2`]REAL_POW_LT)
 361 THEN REPEAT(POP_ASSUM MP_TAC)
 362 THEN REAL_ARITH_TAC;
 363
 364 STRIP_TAC
 365 THENL[
 366 REWRITE_TAC[REAL_ARITH`(&2 -h pow 2)/ &2> &0<=> &2 > h pow 2`]
 367 THEN MATCH_MP_TAC(REAL_ARITH` h pow 2<= &1 ==> &2 > h pow 2`)
 368 THEN MATCH_MP_TAC (ISPECL[`2`;`h:real`;]REAL_POW_1_LE)
 369 THEN POP_ASSUM MP_TAC
 370 THEN POP_ASSUM MP_TAC
 371 THEN REAL_ARITH_TAC;
 372
 373  REPEAT STRIP_TAC
 374   THEN EXISTS_TAC `norm ((x':real^3)-(x:real^3))`
 375   THEN EXISTS_TAC `inv(norm ((x':real^3)-(x:real^3)))%(x'-x)+x`
 376   THEN REWRITE_TAC[NORM_POS_LE]
 377   THEN POP_ASSUM MP_TAC
 378   THEN DISJ_CASES_TAC(SET_RULE`((x':real^3)-(x:real^3)= vec 0) \/ ~((x':real^3)-(x:real^3)= vec 0)`)
 379 THENL(*1*)[
 380
 381 ASM_REWRITE_TAC[NORM_0;DOT_LZERO;] THEN REDUCE_ARITH_TAC THEN REAL_ARITH_TAC;(*1*)
 382
 383 REWRITE_TAC[VECTOR_ARITH`(A+B)-B=A:real^3`;VECTOR_MUL_ASSOC]
 384   THEN MP_TAC(ISPEC`x':real^3- x`NORM_EQ_0)
 385   THEN RESA_TAC
 386   THEN MP_TAC(ISPEC`norm(x':real^3- x)`REAL_MUL_LINV)
 387   THEN ASM_REWRITE_TAC[REAL_MUL_SYM]
 388   THEN RESA_TAC
 389   THEN REDUCE_VECTOR_TAC
 390   THEN REWRITE_TAC[VECTOR_ARITH`A-B+B=A:real^3`]
 391   THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC
 392 THENL(*2*)[
 393   REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
 394     THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]imp_norm_ge_zero_fan)
 395     THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`]
 396     THEN RESA_TAC
 397     THEN MP_TAC(ISPEC`inv(norm((x':real^3)-(x:real^3)))`REAL_ABS_REFL)
 398     THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`]
 399    THEN RESA_TAC;(*2*)
 400
 401 STRIP_TAC
 402   THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan (x:real^3)) (h:real)` ASSUME_TAC
 403 THENL(*3*)[
 404
 405 REWRITE_TAC[ballsets_fan;IN_ELIM_THM;dist]
 406   THEN EXISTS_TAC`inv (norm (v - x)) % (v - x) + (x:real^3)`
 407   THEN STRIP_TAC
 408 THENL(*4*)[
 409
 410 REWRITE_TAC[VECTOR_ARITH`((v:real^3)+b)-(u+b)= (v-u)`;]
 411  THEN SUBGOAL_THEN`norm(inv(norm(v-x))%(v:real^3-x)-inv(norm(x'-x))%(x'-x)) pow 2< h pow 2` ASSUME_TAC
 412 THENL(*5*)[
 413 REWRITE_TAC[NORM_POW_2;DOT_LSUB;DOT_RSUB]
 414 THEN REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_SQUARE_NORM; REAL_ARITH`a-b-(c-d)=a+d-b-c`;
 415 REAL_ARITH`a*a*b pow 2=(a*b) pow 2`;DOT_SYM;REAL_ARITH`a+b-e*d*c-d*e*c=a+b- &2 * d*e *c`]
 416 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`;
 417 `(v:real^3)`;] remark1_fan)
 418 THEN RES_TAC
 419 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan)
 420 THEN REWRITE_TAC[NORM_SUB]
 421  THEN RES_TAC
 422   THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV)
 423 THEN RES_TAC
 424 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 pow 2= &1`;
 425 REAL_ARITH`&1+ &1 - &2 * a< h pow 2 <=> a > (&2- h pow 2)/ &2`]
 426 THEN MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE)
 427  THEN DISCH_TAC
 428 THEN SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC
 429 THENL(*6*)[
 430
 431 REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
 432
 433  MP_TAC (ISPEC `(x':real^3)-(x:real^3)` NORM_POS_LE)
 434  THEN DISCH_TAC
 435 THEN SUBGOAL_THEN ` norm((x:real^3)-(x':real^3))> &0 ` ASSUME_TAC
 436 THENL(*7*)[
 437
 438 ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')> &0 <=> norm(x'-x)> &0`]
 439 THEN REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*7*)
 440
 441 MP_TAC(ISPECL[`(&2 - (h:real) pow 2) / &2`;
 442 `inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`;
 443 `norm (x:real^3 - x')`]REAL_LT_LMUL_EQ)
 444 THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`]
 445 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 446 THEN POP_ASSUM(fun th->REWRITE_TAC[])
 447 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`]
 448 THEN DISCH_TAC
 449 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 450 THEN MP_TAC(ISPECL[`norm (x:real^3 - x') * (&2 - (h:real) pow 2) / &2`;
 451 `norm (x:real^3 - x')*inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`;
 452 `norm (v:real^3 - x)`]REAL_LT_LMUL_EQ)
 453 THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`]
 454 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 455 THEN POP_ASSUM(fun th->REWRITE_TAC[])
 456 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`]
 457 THEN DISCH_TAC
 458 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
 459 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C*D*E>a*b*c<=>(C*B)*(D*A)*E>b*c*a`]
 460 THEN ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')= norm(x'-x)`]
 461 THEN ASM_REWRITE_TAC[]
 462 THEN REDUCE_ARITH_TAC
 463 THEN GEN_REWRITE_TAC(RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[NORM_SUB]
 464 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DOT_SYM]
 465 THEN ASM_REWRITE_TAC[]](*7*)](*6*)(*5*);
 466
 467 ASM_REWRITE_TAC[NORM_LT_SQUARE;DOT_SQUARE_NORM]](*5*);(*4*)
 468
 469
 470 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`;
 471 `(v:real^3)`;] remark1_fan)
 472 THEN RES_TAC
 473 THEN
 474 SUBGOAL_THEN`inv(norm(v-x:real^3)) % (v-x) +x IN aff_ge {x} {v}` ASSUME_TAC
 475 THENL(*5*)[
 476 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC
 477  THEN REWRITE_TAC[IN_ELIM_THM]
 478   THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))`
 479   THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))`
 480  THEN STRIP_TAC
 481 THENL(*6*)[
 482
 483
 484  MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*)
 485 STRIP_TAC
 486 THENL(*7*)[
 487  REAL_ARITH_TAC;
 488 VECTOR_ARITH_TAC]](*6*);(*5*)
 489
 490 SUBGOAL_THEN` inv (norm (v- x)) % (v - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC
 491 THENL(*6*)[
 492   REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
 493     THEN MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan)
 494 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> v=x`]
 495
 496     THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`]
 497     THEN RESA_TAC
 498     THEN MP_TAC(ISPEC`inv(norm((v:real^3)-(x:real^3)))`REAL_ABS_REFL)
 499     THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`]
 500    THEN RESA_TAC
 501 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan)
 502 THEN REWRITE_TAC[NORM_SUB]
 503  THEN RES_TAC
 504   THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV)
 505 THEN RES_TAC
 506 THEN ASM_REWRITE_TAC[];(*6*)
 507 ASM_SET_TAC[]](*6*)](*5*)](*4*);(*3*)
 508 ASM_SET_TAC[]]]]]]);;
 509
 510
 511
 512
 513
 514
 515
 516
 517
 518
 519
 520
 521
 522
 523 let inter_is_empty=prove(`
 524 !(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
 525 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
 526 ==>
 527 ?h1:real.
 528 &1 > h1 /\
 529 h1> &0 /\
 530 rcone_fan x v h1 INTER aff_ge {x} {v1, w1} = {}
 531 `,
 532 REPEAT STRIP_TAC
 533 THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3) `
 534 ;`(w:real^3)`;` (v1:real^3) `;`(w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty_fan)
 535 THEN RESA_TAC
 536 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`(v:real^3)`;
 537 `(w:real^3)`;` h:real`]rcone_subset_cone)
 538 THEN RESA_TAC
 539 THEN POP_ASSUM MP_TAC
 540 THEN REWRITE_TAC[REAL_ARITH`&0<h<=> h> &0`; REAL_ARITH`h< &1 <=> &1 >h`]
 541 THEN RES_TAC
 542 THEN SUBGOAL_THEN`(rcone_fan x v h1 INTER aff_ge {x} {v1, w1}) SUBSET
 543       {x:real^3}` ASSUME_TAC
 544 THENL[
 545 ASM_SET_TAC[];
 546 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (h1:real)`]origin_not_in_rcone_fan)
 547 THEN REPEAT STRIP_TAC
 548 THEN EXISTS_TAC`h1:real`
 549 THEN ASM_REWRITE_TAC[]
 550 THEN POP_ASSUM MP_TAC
 551 THEN POP_ASSUM MP_TAC
 552 THEN REWRITE_TAC[SUBSET; IN_SING;EXTENSION;EMPTY]
 553 THEN REPEAT STRIP_TAC
 554 THEN EQ_TAC
 555 THENL[
 556  POP_ASSUM MP_TAC
 557 THEN POP_ASSUM MP_TAC
 558 THEN DISCH_THEN(LABEL_TAC"a")
 559 THEN DISCH_TAC
 560 THEN DISCH_TAC
 561 THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC`x':real^3`th))
 562 THEN ASM_REWRITE_TAC[]
 563 THEN POP_ASSUM MP_TAC
 564 THEN DISCH_THEN(LABEL_TAC"a")
 565 THEN DISCH_TAC
 566 THEN REMOVE_THEN "a" MP_TAC
 567 THEN ASM_REWRITE_TAC[]
 568 THEN DISCH_TAC
 569 THEN SUBGOAL_THEN`x:real^3 IN rcone_fan x v h1` ASSUME_TAC
 570 THENL[ASM_SET_TAC[];
 571 ASM_SET_TAC[]];
 572 ASM_SET_TAC[]]]);;
 573
 574 let avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3)(w2:real^3).
 575 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
 576 ==>
 577 ?h:real.
 578 &1 >h /\
 579 h> &0
 580 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),(w2:real^3)) h INTER aff_ge {x} {v1, w1} = {}
 581 `,
 582
 583 REPEAT STRIP_TAC
 584 THEN REWRITE_TAC[rw_dart_fan]
 585 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)` ;`(w1:real^3)`]inter_is_empty)
 586 THEN RESA_TAC
 587 THEN EXISTS_TAC`h1:real`
 588 THEN ASM_SET_TAC[]
 589
 590 );;
 591
 592
 593 let avoids1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)  (w1:real^3).
 594 FAN(x,V,E) /\ {v,w} IN E /\ {v,w1} IN E
 595 ==>
 596 ?h:real.
 597 &1 > h /\
 598 h > &0 /\
 599  rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v, w1} = {}`,
 600 REPEAT STRIP_TAC
 601 THEN REWRITE_TAC[rw_dart_fan]
 602 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;
 603 ` (w:real^3)`;`(w1:real^3)`]IBZWFFH)
 604 THEN RESA_TAC
 605 THEN EXISTS_TAC`&1/ &2`
 606 THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`]
 607 THEN ASM_SET_TAC[]);;
 608
 609
 610 let finish_avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
 611 FAN(x,V,E) /\ {v,w} IN E /\ {v1,w1} IN E
 612 ==>
 613 ?h:real.
 614 &1 >h /\
 615 h> &0/\
 616 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v1, w1} = {}`,
 617
 618 REPEAT STRIP_TAC
 619 THEN DISJ_CASES_TAC(SET_RULE`~(v:real^3 IN {v1,w1})\/ (v=v1\/ v=w1)`)
 620 THENL[
 621 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`(v1:real^3)`;`w1:real^3`;` (sigma_fan x V E v w:real^3)`]avoids_fan)
 622 THEN RESA_TAC
 623 THEN ASM_SET_TAC[];
 624
 625 POP_ASSUM MP_TAC
 626 THEN STRIP_TAC
 627 THENL[
 628 POP_ASSUM MP_TAC
 629 THEN POP_ASSUM MP_TAC
 630 THEN DISCH_THEN(LABEL_TAC"A")
 631 THEN DISCH_TAC
 632 THEN REMOVE_THEN "A" MP_TAC
 633 THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)])
 634 THEN DISCH_TAC
 635 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`w1:real^3`]avoids1_fan)
 636 THEN RESA_TAC;
 637
 638 POP_ASSUM MP_TAC
 639 THEN POP_ASSUM MP_TAC
 640 THEN DISCH_THEN(LABEL_TAC"A")
 641 THEN DISCH_TAC
 642 THEN REMOVE_THEN "A" MP_TAC
 643 THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)])
 644 THEN ONCE_REWRITE_TAC[SET_RULE`{X,Y}={Y,X}`]
 645 THEN DISCH_TAC
 646 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`v1:real^3`]avoids1_fan)
 647 THEN RESA_TAC]]);;
 648
 649 let continuous_set_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (h:real) (h1:real).
 650 FAN(x,V,E) /\ {v,w} IN E /\ h1 <= h
 651 ==>
 652 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h1`,
 653
 654 REPEAT STRIP_TAC
 655 THEN REWRITE_TAC[rw_dart_fan]
 656 THEN SUBGOAL_THEN `rcone_fan x v h SUBSET rcone_fan x v h1` ASSUME_TAC
 657 THENL[
 658 REWRITE_TAC[rcone_fan;SUBSET; IN_ELIM_THM]
 659 THEN REPEAT STRIP_TAC
 660 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
 661 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
 662 THEN MP_TAC(ISPECL[`dist((v:real^3),x)`;`h1:real`;`h:real`] REAL_LE_LMUL)
 663 THEN RESA_TAC
 664 THEN MP_TAC(ISPECL[`dist((x':real^3),x)`;`dist((v:real^3),x)* (h1:real)`;`dist((v:real^3),x)* (h:real)`] REAL_LE_LMUL)
 665 THEN RESA_TAC
 666 THEN REPEAT (POP_ASSUM MP_TAC)
 667 THEN REAL_ARITH_TAC;
 668 ASM_SET_TAC[]]);;
 669
 670
 671
 672
 673
 674
 675 let finish_avoids1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E':(real^3->bool)->bool) (v:real^3) (w:real^3).
 676 FAN(x,V,E) /\ {v,w} IN E /\ E' SUBSET E
 677 ==>
 678 ?h:real.
 679 &1> h /\
 680 h> &0 /\
 681 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER {v | ?e. e IN E' /\ v IN aff_ge {x} e}={}`,
 682
 683 REPEAT STRIP_TAC
 684 THEN REWRITE_TAC[xfan; IN_ELIM_THM]
 685 THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]set_edges_is_finite_fan)
 686 THEN RESA_TAC
 687 THEN MP_TAC(ISPECL [`(E':(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`] FINITE_SUBSET)
 688 THEN RESA_TAC
 689 THEN ABBREV_TAC`n=CARD (E':(real^3->bool)->bool)`
 690 THEN REPEAT(POP_ASSUM MP_TAC)
 691 THEN SPEC_TAC (`(E':(real^3->bool)->bool)`,`(E':(real^3->bool)->bool)`)
 692 THEN SPEC_TAC (`n:num`,`n:num`)
 693 THEN INDUCT_TAC
 694 THENL(*1*)[
 695 REPEAT STRIP_TAC
 696 THEN MP_TAC(ISPECL[`E':(real^3->bool)->bool`]CARD_EQ_0)
 697 THEN RESA_TAC
 698 THEN EXISTS_TAC`&1 / &2`
 699 THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`]
 700 THEN ASM_SET_TAC[];(*1*)
 701
 702 REPEAT GEN_TAC
 703 THEN POP_ASSUM MP_TAC
 704 THEN DISCH_THEN (LABEL_TAC "A")
 705 THEN REPEAT STRIP_TAC
 706 THEN MP_TAC(ISPEC`(E':(real^3->bool)->bool)` CHOOSE_SUBSET)
 707 THEN RESA_TAC
 708 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`n:num `th))
 709 THEN REWRITE_TAC[ARITH_RULE `n:num <= SUC n`; HAS_SIZE]
 710 THEN STRIP_TAC
 711 THEN MP_TAC(SET_RULE` t SUBSET E' /\ E' SUBSET E ==> (t:(real^3->bool)->bool) SUBSET E`)
 712 THEN RESA_TAC
 713 THEN REMOVE_THEN "A" (fun th-> MP_TAC(ISPEC`(t:(real^3->bool)->bool)`th))
 714 THEN RESA_TAC
 715 THEN SUBGOAL_THEN `~((E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)= {})` ASSUME_TAC
 716 THENL(*2*)[
 717 STRIP_TAC
 718 THEN MP_TAC(SET_RULE`(E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)={} /\ t SUBSET E' ==>  t= E'`)
 719 THEN RESA_TAC
 720 THEN FIND_ASSUM MP_TAC`CARD (t:(real^3->bool)->bool)=n`
 721 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
 722 THEN ASM_REWRITE_TAC[]
 723 THEN ARITH_TAC;(*2*)
 724
 725 SUBGOAL_THEN`?e. e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)`
 726 ASSUME_TAC
 727 THENL(*3*)[
 728 ASM_SET_TAC[];(*3*)
 729
 730 POP_ASSUM MP_TAC
 731 THEN STRIP_TAC
 732 THEN MP_TAC(SET_RULE`e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)/\
 733 (E':(real^3->bool)->bool) SUBSET (E:(real^3->bool)->bool) /\ t SUBSET E' ==> e IN E'/\ e IN E/\ ~(e IN t) /\ {e} UNION t SUBSET E'`)
 734 THEN RESA_TAC
 735 THEN MP_TAC(ISPECL [`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`(E':(real^3->bool)->bool)`] FINITE_SUBSET)
 736 THEN RESA_TAC
 737 THEN ASSUME_TAC(SET_RULE`e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`)
 738 THEN MP_TAC(ISPECL[`e:real^3->bool`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;]CARD_DELETE)
 739 THEN RESA_TAC
 740 THEN MP_TAC(SET_RULE `e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)
 741 ==> ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e PSUBSET {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`)
 742 THEN RESA_TAC
 743 THEN MP_TAC(ISPECL[`({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))DELETE e`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`]CARD_PSUBSET)
 744 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 745 THEN FIND_ASSUM MP_TAC`FINITE ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool))`
 746 THEN DISCH_TAC
 747 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 748 THEN DISCH_TAC
 749 THEN MP_TAC(ARITH_RULE`CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) < CARD ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool))
 750 /\ CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) = CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))-1
 751 <=>CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) +1= CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))`)
 752 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 753 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
 754 THEN REWRITE_TAC[ARITH_RULE`A=A`; ]
 755 THEN MP_TAC(SET_RULE`~(e IN t)==>({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e=t`)
 756 THEN RESA_TAC
 757 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 758 THEN FIND_ASSUM MP_TAC`(CARD (E':(real^3->bool)->bool)=SUC n)`
 759 THEN REWRITE_TAC[ARITH_RULE`SUC n=(n:num) +1`]
 760 THEN DISCH_TAC
 761 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
 762 THEN DISCH_TAC
 763 THEN MP_TAC(ISPECL[`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`E':(real^3->bool)->bool`]CARD_SUBSET_EQ)
 764 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
 765 THEN RESA_TAC
 766 THEN POP_ASSUM MP_TAC
 767 THEN DISCH_THEN(LABEL_TAC"MA")
 768 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]expand_edge_graph_fan)
 769 THEN RESA_TAC
 770 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;`(w:real^3)`; `(v':real^3)`;` (w':real^3)`]finish_avoids_fan)
 771 THEN RESA_TAC
 772 THEN POP_ASSUM MP_TAC
 773 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
 774 THEN POP_ASSUM MP_TAC
 775 THEN RESA_TAC
 776 THEN STRIP_TAC
 777 THEN ABBREV_TAC`h1= max (h:real) (h':real)`
 778 THEN EXISTS_TAC`h1:real`
 779 THEN STRIP_TAC
 780 THENL(*4*)[
 781 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 782 THEN REPEAT(POP_ASSUM MP_TAC)
 783 THEN REAL_ARITH_TAC;(*4*)
 784
 785 STRIP_TAC
 786 THENL(*5*)[
 787 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 788 THEN REPEAT(POP_ASSUM MP_TAC)
 789 THEN REAL_ARITH_TAC;(*5*)
 790
 791 REMOVE_THEN "MA" MP_TAC
 792 THEN DISCH_TAC
 793 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
 794 THEN REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION; INTER;]
 795 THEN GEN_TAC
 796 THEN EQ_TAC
 797 THENL(*6*)[
 798
 799 ASM_REWRITE_TAC[IN_SING]
 800 THEN STRIP_TAC
 801 THENL[
 802  POP_ASSUM MP_TAC
 803 THEN ASM_REWRITE_TAC[]
 804 THEN DISCH_TAC
 805 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h':real)`]continuous_set_fan)
 806 THEN RESA_TAC
 807 THEN POP_ASSUM MP_TAC
 808 THEN EXPAND_TAC"h1"
 809 THEN REWRITE_TAC[REAL_ARITH`h'<= max (h:real) (h':real)`]
 810 THEN RESA_TAC
 811 THEN ASM_SET_TAC[];
 812
 813  POP_ASSUM MP_TAC
 814 THEN ASM_REWRITE_TAC[]
 815 THEN DISCH_TAC
 816 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h:real)`]continuous_set_fan)
 817 THEN RESA_TAC
 818 THEN POP_ASSUM MP_TAC
 819 THEN EXPAND_TAC"h1"
 820 THEN REWRITE_TAC[REAL_ARITH`h<= max (h:real) (h':real)`]
 821 THEN RESA_TAC
 822 THEN ASM_SET_TAC[]];
 823
 824 ASM_SET_TAC[]]]]]]]);;
 825
 826
 827
 828
 829
 830
 831
 832 let rw_dart_avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3).
 833 FAN(x,V,E) /\ {v,w} IN E
 834 ==>
 835 ?h:real.
 836 &1> h /\
 837 h> &0 /\
 838 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h  SUBSET yfan(x,V,E) `,
 839
 840 REPEAT STRIP_TAC
 841 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]finish_avoids1_fan)
 842 THEN RESA_TAC
 843 THEN POP_ASSUM MP_TAC
 844 THEN REWRITE_TAC[SET_RULE`A SUBSET A`;yfan;xfan]
 845 THEN RESA_TAC
 846 THEN EXISTS_TAC`h:real`
 847 THEN ASM_REWRITE_TAC[]
 848 THEN ASM_SET_TAC[]);;
 849
 850
 851
 852
 853 (*------------------------------------------------------------------------*)
 854 (*------------------------------------------------------------------------*)
 855
 856
 857
 858 let r_fan=new_definition`r_fan (a:real) (b:real) (c:real) = { y:real^3 | y$1 > &0  /\  y$2 > a  /\ y$2 < b /\ y$3 > &0 /\ y$3 < c}`;;
 859
 860
 861
 862 let r1_le_fan=new_definition`r1_le_fan (a:real)={ y:real^3 | y$1 > a}`;;
 863
 864
 865 let r2_le_fan=new_definition`r2_le_fan (a:real)={ y:real^3 |  y$2 > a}`;;
 866
 867
 868
 869 let r3_le_fan=new_definition`r3_le_fan (a:real)={ y:real^3 | y$3 > a}`;;
 870
 871
 872
 873 let r1_ge_fan=new_definition`r1_ge_fan (a:real)={ y:real^3 |  y$1 < a}`;;
 874
 875
 876 let r2_ge_fan=new_definition`r2_ge_fan (a:real)={ y:real^3 |  y$2 < a}`;;
 877
 878 let r3_ge_fan=new_definition`r3_ge_fan (a:real)={ y:real^3 |  y$3 < a}`;;
 879
 880
 881
 882
 883 let r_fan_is_inter_halfspace=prove(`!a:real b:real c:real.
 884 r_fan a b c = r1_le_fan (&0) INTER r2_le_fan a INTER r2_ge_fan b INTER r3_le_fan (&0) INTER r3_ge_fan c`,
 885 REWRITE_TAC[r_fan; r1_le_fan; r2_le_fan; r2_ge_fan; r3_le_fan; r3_ge_fan; INTER; IN_ELIM_THM]);;
 886
 887
 888
 889
 890
 891 let r1_ge_is_convex_fan = prove(`!a:real. convex (r1_ge_fan a)/\ open (r1_ge_fan a) `,REWRITE_TAC[r1_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
 892
 893
 894 let r2_ge_is_convex_fan = prove(`!a:real. convex (r2_ge_fan a)/\ open (r2_ge_fan a)`,
 895 REWRITE_TAC[r2_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
 896
 897 let r3_ge_is_convex_fan = prove(`!a:real. convex (r3_ge_fan a) /\ open(r3_ge_fan a)`,
 898 REWRITE_TAC[r3_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
 899
 900 let r1_le_is_convex_fan = prove(`!a:real. convex (r1_le_fan a)/\  open (r1_le_fan a) `,
 901 REWRITE_TAC[r1_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
 902
 903 let r2_le_is_convex_fan = prove(`!a:real. convex (r2_le_fan a)/\ open (r2_le_fan a) `,
 904 REWRITE_TAC[r2_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
 905
 906 let r3_le_is_convex_fan = prove(`!a:real. convex (r3_le_fan a)/\ open (r3_le_fan a) `,
 907 REWRITE_TAC[r3_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
 908
 909 let r_is_connected_fan=prove(`!a:real b:real c:real. connected (r_fan a b c)/\convex (r_fan a b c) /\ open (r_fan a b c)`,
 910    (let lemma = prove(`!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c)`,
 911 ASSUME_TAC (r_fan_is_inter_halfspace) THEN ASM_REWRITE_TAC[] THEN
 912 ASSUME_TAC (r1_ge_is_convex_fan) THEN ASSUME_TAC ( r2_ge_is_convex_fan) THEN
 913 ASSUME_TAC (r3_ge_is_convex_fan) THEN ASSUME_TAC(r1_le_is_convex_fan) THEN
 914 ASSUME_TAC(r2_le_is_convex_fan) THEN ASSUME_TAC( r3_le_is_convex_fan) THEN
 915 ASM_MESON_TAC[CONVEX_INTER;OPEN_INTER])
 916     in
 917 SUBGOAL_THEN `!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c) ` ASSUME_TAC
 918 THENL [MESON_TAC[lemma];
 919        ASM_MESON_TAC[CONVEX_CONNECTED]]));;
 920
 921
 922
 923
 924
 925 let rw_dart_is_image_set_spherical_coordinate=prove(`(!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real.
 926 FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\  h< pi/ &2
 927 ==>
 928   IMAGE (change_spherical_coordinate_fan x v u)
 929 (r_fan (azim x v u u) (azim_fan x V E v u) h)=
 930       rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))) `,
 931 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,ASM_SET_TAC[]) in
 932 ( let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in
 933
 934 REWRITE_TAC[azim_fan;r_fan; rw_dart_fan; change_spherical_coordinate_fan;IMAGE;INTER;
 935 w_dart_fan;rcone_fan;EXTENSION;IN_ELIM_THM]
 936 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
 937 THEN REPEAT STRIP_TAC
 938 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;
 939 `(E:(real^3->bool)->bool)`;` u:real^3`;` v:real^3`]remark1_fan)
 940 THEN RESA_TAC
 941 THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
 942 THEN GEN_REWRITE_TAC( LAND_CONV  o ONCE_DEPTH_CONV)[lem1]
 943 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
 944 THEN RESA_TAC
 945 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
 946 THEN RESA_TAC
 947 THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
 948 THEN REWRITE_TAC[orthonormal]
 949 THEN STRIP_TAC
 950 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
 951 THEN RESA_TAC
 952 THEN EQ_TAC
 953 THENL(*1*)[
 954 STRIP_TAC
 955 THEN MP_TAC(ISPEC`(x'':real^3)$3`SIN_POS_PI2)
 956 THEN RESA_TAC
 957 THEN ONCE_REWRITE_TAC[SET_RULE`A /\ B <=> B /\ A`]
 958 THEN STRIP_TAC
 959 THENL(*2*)[
 960
 961
 962
 963
 964 REWRITE_TAC[dist;vector_norm;VECTOR_ARITH`(A+B)-A=(B:real^3)`; DOT_LADD;DOT_RADD;DOT_RMUL;DOT_LMUL;]
 965 THEN ONCE_REWRITE_TAC[DOT_SYM]
 966 THEN ASM_REWRITE_TAC[]
 967 THEN REDUCE_ARITH_TAC
 968 THEN ONCE_REWRITE_TAC[DOT_SYM]
 969 THEN ASM_REWRITE_TAC[]
 970 THEN REDUCE_ARITH_TAC
 971 THEN REWRITE_TAC[REAL_ARITH`((x'':real^3)$1 * cos (x''$2) * sin (x''$3)) * x''$1 * cos (x''$2) * sin (x''$3) +
 972   (x''$1 * sin (x''$2) * sin (x''$3)) * x''$1 * sin (x''$2) * sin (x''$3) +
 973   (x''$1 * cos (x''$3)) * x''$1 * cos (x''$3)=(x''$1 * x''$1)* (( sin (x''$2) pow 2 +(cos (x''$2) pow 2)) * (sin (x''$3) pow 2)+ cos (x''$3) pow 2)`]
 974 THEN ASSUME_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
 975 THEN ASM_REWRITE_TAC[]
 976 THEN REDUCE_ARITH_TAC
 977 THEN ASSUME_TAC(ISPEC`(x'':real^3)$3`SIN_CIRCLE)
 978 THEN ASM_REWRITE_TAC[]
 979 THEN REDUCE_ARITH_TAC
 980 THEN MP_TAC(ISPEC`(x'':real^3)$1`SQRT_POW_2)
 981 THEN MP_TAC(REAL_ARITH`(x'':real^3)$1> &0==> &0 <= (x'':real^3)$1`)
 982 THEN RESA_TAC
 983 THEN RESA_TAC
 984 THEN MP_TAC(ISPECL[`(x'':real^3)$1`;`(x'':real^3)$1`]SQRT_MUL)
 985 THEN RESA_TAC
 986 THEN REWRITE_TAC[REAL_ARITH`A*(A:real)=A pow 2`]
 987 THEN ASM_REWRITE_TAC[e3_fan;DOT_LMUL]
 988 THEN ONCE_REWRITE_TAC[GSYM vector_norm;]
 989 THEN ASSUME_TAC(ISPEC`(v:real^3)-(x:real^3)`DOT_SQUARE_NORM)
 990 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
 991 THEN REWRITE_TAC[REAL_ARITH`(A*B)*C *D pow 2=A*D*B *(C*D)`]
 992 THEN SUBGOAL_THEN`~(norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
 993 THENL(*3*)[
 994
 995 ASM_REWRITE_TAC[NORM_EQ_0;VECTOR_ARITH`v-x=vec 0<=> x=v`];(*3*)
 996
 997 MP_TAC(ISPEC`norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
 998 THEN RESA_TAC
 999 THEN ASM_REWRITE_TAC[]
1000 THEN REDUCE_ARITH_TAC
1001 THEN MP_TAC(ISPEC`((v:real^3)-(x:real^3))`NORM_POS_LT)
1002 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> x=v`;REAL_ARITH`A>B<=> B<A`]
1003 THEN DISCH_TAC
1004 THEN MATCH_MP_TAC REAL_LT_LMUL
1005 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 < A<=> A> &0`]
1006 THEN MATCH_MP_TAC REAL_LT_LMUL
1007 THEN ASM_REWRITE_TAC[]
1008 THEN MATCH_MP_TAC COS_MONO_LT
1009 THEN REPEAT(POP_ASSUM MP_TAC)
1010 THEN REAL_ARITH_TAC];(*2*)
1011
1012
1013
1014 SUBGOAL_THEN`azim (x:real^3) (v:real^3) (u:real^3)
1015  (x +
1016   (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1017   (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1018   (x''$1 * cos (x''$3)) % e3_fan x v u)= (x'':real^3)$2 ` ASSUME_TAC
1019 THENL(*3*)[
1020
1021 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
1022   (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1023   (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
1024   (x''$1 * cos (x''$3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
1025   `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1026   `(x''$1 * cos ((x'':real^3)$3)) * (inv (norm((v:real^3)-(x:real^3))))`;
1027 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
1028 `x''$1 * sin ((x'':real^3)$3)`;
1029 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`(x'':real^3)$2`]AZIM_UNIQUE)
1030 THEN DISCH_TAC
1031 THEN POP_ASSUM MATCH_MP_TAC
1032 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
1033 THEN STRIP_TAC
1034 THENL(*4*)[
1035
1036 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
1037 THEN REPEAT(POP_ASSUM MP_TAC)
1038 THEN REAL_ARITH_TAC;(*4*)
1039
1040 STRIP_TAC
1041 THENL(*5*)[
1042
1043 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`] azim)
1044 THEN REPEAT(POP_ASSUM MP_TAC)
1045 THEN REAL_ARITH_TAC;(*5*)
1046
1047 STRIP_TAC
1048 THENL(*6*)[
1049
1050 MATCH_MP_TAC REAL_LT_MUL
1051 THEN REPEAT(POP_ASSUM MP_TAC)
1052 THEN REAL_ARITH_TAC;(*6*)
1053
1054 STRIP_TAC
1055 THENL(*7*)[
1056
1057 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1058 THEN REDUCE_ARITH_TAC
1059 THEN REDUCE_VECTOR_TAC
1060 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1061 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1062 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1063  ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1064 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1065 THEN REDUCE_ARITH_TAC
1066 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1067 THEN REDUCE_VECTOR_TAC
1068 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1069 THEN RESA_TAC
1070 THEN ASM_REWRITE_TAC[]
1071 THEN REWRITE_TAC[e1_fan]
1072 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1073 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1074 THEN ONCE_REWRITE_TAC[DOT_SYM]
1075 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1076 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1077 THEN ASM_REWRITE_TAC[]
1078 THEN REDUCE_VECTOR_TAC
1079 THEN STRIP_TAC
1080 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1081 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1082 THEN REWRITE_TAC[DOT_RZERO]
1083 THEN REAL_ARITH_TAC;(*7*)
1084
1085 REWRITE_TAC[e3_fan]
1086 THEN VECTOR_ARITH_TAC](*7*)](*6*)](*5*)](*4*);(*3*)
1087
1088
1089
1090
1091 SUBGOAL_THEN`~collinear
1092   {(x:real^3), (v:real^3), x +
1093          (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v (u:real^3) +
1094          (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
1095          (x''$1 * cos (x''$3)) % e3_fan x v u}`ASSUME_TAC
1096 THENL(*4*)[
1097
1098 ONCE_REWRITE_TAC[lem]
1099 THEN REWRITE_TAC[collinear1_fan]
1100 THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2; IN_ELIM_THM; REAL_ARITH`A+B= &1<=>A= &1-B`]
1101 THEN STRIP_TAC
1102 THEN POP_ASSUM MP_TAC
1103 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1104 THEN REWRITE_TAC[VECTOR_ARITH`A+B=(&1-c) % A+ c % D<=>B=c%(D-A)`]
1105 THEN STRIP_TAC
1106 THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1107       (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1108       (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e1_fan x v u =
1109       ((v':real) % ((v:real^3) - (x:real^3))) dot e1_fan x v u` ASSUME_TAC
1110 THENL(*5*)[
1111 ASM_REWRITE_TAC[];(*5*)
1112
1113 POP_ASSUM MP_TAC
1114 THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1115 THEN ASM_REWRITE_TAC[DOT_SYM]
1116 THEN REDUCE_ARITH_TAC
1117 THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1118       (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1119       (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e2_fan x v u =
1120       ((v':real) % ((v:real^3) - (x:real^3))) dot e2_fan x v u` ASSUME_TAC
1121 THENL(*6*)[
1122 ASM_REWRITE_TAC[];(*6*)
1123
1124 POP_ASSUM MP_TAC
1125 THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1126 THEN ASM_REWRITE_TAC[DOT_SYM]
1127 THEN REDUCE_ARITH_TAC
1128 THEN REWRITE_TAC[REAL_ENTIRE]
1129 THEN STRIP_TAC
1130 THENL(*7*)[
1131
1132 REPEAT (POP_ASSUM MP_TAC)
1133 THEN REAL_ARITH_TAC;(*7*)
1134
1135 STRIP_TAC
1136 THENL(*8*)[
1137
1138 REPEAT (POP_ASSUM MP_TAC)
1139 THEN REAL_ARITH_TAC;(*8*)
1140
1141
1142 MP_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
1143 THEN ASM_REWRITE_TAC[]
1144 THEN REAL_ARITH_TAC;
1145
1146 REPEAT (POP_ASSUM MP_TAC)
1147 THEN REAL_ARITH_TAC];
1148
1149 REPEAT (POP_ASSUM MP_TAC)
1150 THEN REAL_ARITH_TAC](*7*)](*6*)](*5*);(*4*)
1151
1152
1153 REPEAT(POP_ASSUM MP_TAC)
1154 THEN DISJ_CASES_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1
1155 \/ ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) >1)`)
1156 THENL(*5*)[
1157 ASM_REWRITE_TAC[]
1158 THEN REPEAT STRIP_TAC
1159 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
1160 THEN ASM_REWRITE_TAC[]
1161 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1162 THEN ASM_REWRITE_TAC[]
1163 THEN FIND_ASSUM MP_TAC`(x'':real^3)$2 > azim (x:real^3) (v:real^3) u (u:real^3)`
1164 THEN REWRITE_TAC[AZIM_REFL]
1165 THEN REAL_ARITH_TAC;(*5*)
1166
1167
1168 ASM_REWRITE_TAC[]
1169 THEN REPEAT STRIP_TAC
1170 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1171 THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
1172 THEN RESA_TAC
1173 THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
1174 THEN STRIP_TAC
1175 THENL(*6*)[
1176
1177 ASM_SET_TAC[];(*6*)
1178
1179 STRIP_TAC
1180 THEN  MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x:real^3) +
1181   (x''$1 * cos (x''$2) * sin ((x'':real^3)$3)) % e1_fan x (v:real^3) (u:real^3) +
1182   (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1183   (x''$1 * cos (x''$3)) % e3_fan x v u`]AZIM_EQ_0_GE_ALT)
1184 THEN RESA_TAC
1185 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
1186 THEN REPEAT(POP_ASSUM MP_TAC)
1187 THEN REAL_ARITH_TAC](*6*)](*5*)](*4*)](*3*)](*2*);(*1*)
1188
1189
1190
1191 ONCE_REWRITE_TAC[GSYM EXTENSION]
1192 THEN DISJ_CASES_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1
1193 \/ ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) >1)`)
1194 THENL(*2*)[
1195 ASM_REWRITE_TAC[wedge;IN_ELIM_THM]
1196 THEN STRIP_TAC
1197 THEN POP_ASSUM MP_TAC
1198 THEN DISCH_THEN(LABEL_TAC"A")
1199 THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
1200 THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
1201 THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
1202 THENL(*3*)[
1203
1204
1205  STRIP_TAC
1206 THEN REMOVE_THEN "A" MP_TAC
1207 THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
1208 THEN REDUCE_ARITH_TAC
1209 THEN REAL_ARITH_TAC;(*3*)
1210
1211
1212 MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
1213 THEN RESA_TAC
1214 THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
1215 THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
1216 THEN RESA_TAC
1217 THEN ASM_REWRITE_TAC[]
1218 THEN STRIP_TAC
1219 THENL(*4*)[
1220 STRIP_TAC
1221 THENL(*5*)[
1222
1223 REWRITE_TAC[ARCV_ANGLE; angle;]
1224 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
1225 THEN STRIP_TAC
1226 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
1227 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
1228 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
1229 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
1230 THEN DISCH_TAC
1231 THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
1232 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1233 THEN REWRITE_TAC[DE_MORGAN_THM]
1234 THEN REPEAT(POP_ASSUM MP_TAC)
1235 THEN REAL_ARITH_TAC;(*5*)
1236
1237 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
1238 THEN RESA_TAC
1239 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
1240 THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
1241 THEN RESA_TAC
1242 THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
1243 THEN RESA_TAC
1244 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
1245 THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
1246 THEN RESA_TAC
1247 THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1248 THEN RESA_TAC
1249 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1250 THEN ASM_REWRITE_TAC[]
1251 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1252 THEN ASM_REWRITE_TAC[]
1253 THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
1254 THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
1255 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
1256 THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
1257 THEN ONCE_REWRITE_TAC[GSYM real_div;]
1258 THEN REWRITE_TAC[dist;arcV]
1259 THEN STRIP_TAC
1260 THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
1261 THEN RESA_TAC
1262 THEN MP_TAC(ISPEC`h:real`ACS_COS)
1263 THEN RESA_TAC
1264 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
1265 THEN RESA_TAC
1266 THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
1267 THEN POP_ASSUM MATCH_MP_TAC
1268 THEN REWRITE_TAC[COS_BOUNDS]
1269 THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
1270 THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
1271 THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
1272 THEN REAL_ARITH_TAC](*5*);(*4*)
1273
1274
1275 MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1276 `e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
1277 THEN ASM_REWRITE_TAC[]
1278 THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
1279 THENL(*5*)[
1280
1281 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1282   `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1283   `&0`;
1284 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
1285 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
1286 THEN DISCH_TAC
1287 THEN POP_ASSUM MATCH_MP_TAC
1288 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
1289 THEN STRIP_TAC
1290 THENL(*6*)[
1291 MP_TAC(PI_WORKS)
1292 THEN REAL_ARITH_TAC;(*6*)
1293
1294 STRIP_TAC
1295 THENL(*7*)[
1296
1297 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1298 THEN REDUCE_ARITH_TAC
1299 THEN REDUCE_VECTOR_TAC
1300 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1301 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1302 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1303  ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1304 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1305 THEN REDUCE_ARITH_TAC
1306 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1307 THEN REDUCE_VECTOR_TAC
1308 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1309 THEN RESA_TAC
1310 THEN ASM_REWRITE_TAC[]
1311 THEN REWRITE_TAC[e1_fan]
1312 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1313 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1314 THEN ONCE_REWRITE_TAC[DOT_SYM]
1315 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1316 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1317 THEN ASM_REWRITE_TAC[]
1318 THEN REDUCE_VECTOR_TAC
1319 THEN STRIP_TAC
1320 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1321 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1322 THEN REWRITE_TAC[DOT_RZERO]
1323 THEN REAL_ARITH_TAC;(*7*)
1324
1325 REWRITE_TAC[SIN_0;COS_0]
1326 THEN REDUCE_ARITH_TAC
1327 THEN REDUCE_VECTOR_TAC
1328 THEN VECTOR_ARITH_TAC](*7*)](*6*);(*5*)
1329
1330
1331 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
1332 THEN RESA_TAC
1333 THEN POP_ASSUM MATCH_MP_TAC
1334 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1335 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1336 THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
1337 THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
1338 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
1339 THEN REDUCE_ARITH_TAC
1340 THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*5*)](*4*)](*3*);(*2*)
1341
1342
1343
1344
1345
1346
1347
1348 ASM_REWRITE_TAC[]
1349 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1350 THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
1351 THEN RESA_TAC
1352 THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
1353 THEN STRIP_TAC
1354 THEN POP_ASSUM MP_TAC
1355 THEN DISCH_THEN(LABEL_TAC"A")
1356 THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
1357 THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
1358 THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
1359 THENL(*3*)[
1360
1361 STRIP_TAC
1362 THEN REMOVE_THEN "A" MP_TAC
1363 THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
1364 THEN REDUCE_ARITH_TAC
1365 THEN REAL_ARITH_TAC;(*3*)
1366
1367 MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
1368 THEN RESA_TAC
1369 THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
1370 THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
1371 THEN RESA_TAC
1372 THEN ASM_REWRITE_TAC[azim]
1373 THEN SUBGOAL_THEN`~collinear{(x:real^3),(v:real^3),(x':real^3)}` ASSUME_TAC
1374 THENL(*4*)[
1375
1376 POP_ASSUM (fun th-> REWRITE_TAC[])
1377 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1378 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1379 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1380 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1381 THEN POP_ASSUM MP_TAC
1382 THEN DISCH_THEN(LABEL_TAC"MA")
1383 THEN ONCE_REWRITE_TAC[lem1]
1384 THEN ASM_REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA;VECTOR_ARITH`v-x=vec 0<=> v=x`]
1385 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]AFF_GE_2_1)
1386 THEN RESA_TAC
1387 THEN STRIP_TAC
1388 THENL(*5*)[
1389
1390 REMOVE_THEN "MA" MP_TAC
1391 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1392 THEN EXISTS_TAC`&1`
1393 THEN EXISTS_TAC`&0`
1394 THEN EXISTS_TAC`&0`
1395 THEN REDUCE_ARITH_TAC
1396 THEN REDUCE_VECTOR_TAC
1397 THEN REAL_ARITH_TAC;(*5*)
1398
1399 REMOVE_THEN "MA" MP_TAC
1400 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1401 THEN EXISTS_TAC`&1- (c:real)`
1402 THEN EXISTS_TAC`c:real`
1403 THEN EXISTS_TAC`&0`
1404 THEN REDUCE_ARITH_TAC
1405 THEN REDUCE_VECTOR_TAC
1406 THEN ASM_REWRITE_TAC[VECTOR_ARITH`(x':real^3)=(&1 - (c:real)) % (x:real^3)+ c % (v:real^3)<=>x'-x=c%(v-x)`]
1407 THEN REAL_ARITH_TAC](*5*);(*4*)
1408
1409
1410
1411 STRIP_TAC
1412 THENL(*5*)[
1413 STRIP_TAC
1414 THENL(*6*)[
1415
1416 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]AZIM_EQ_0_GE_ALT)
1417 THEN ASM_REWRITE_TAC[]
1418 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]azim)
1419 THEN REAL_ARITH_TAC;(*6*)
1420
1421
1422 STRIP_TAC
1423 THENL(*7*)[
1424
1425 REWRITE_TAC[ARCV_ANGLE; angle;]
1426 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
1427 THEN STRIP_TAC
1428 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
1429 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
1430 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
1431 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
1432 THEN DISCH_TAC
1433 THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
1434 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1435 THEN REWRITE_TAC[DE_MORGAN_THM]
1436 THEN REPEAT(POP_ASSUM MP_TAC)
1437 THEN REAL_ARITH_TAC;(*7*)
1438
1439 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
1440 THEN RESA_TAC
1441 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
1442 THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
1443 THEN RESA_TAC
1444 THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
1445 THEN RESA_TAC
1446 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
1447 THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
1448 THEN RESA_TAC
1449 THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1450 THEN RESA_TAC
1451 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1452 THEN ASM_REWRITE_TAC[]
1453 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1454 THEN ASM_REWRITE_TAC[]
1455 THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
1456 THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
1457 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
1458 THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
1459 THEN ONCE_REWRITE_TAC[GSYM real_div;]
1460 THEN REWRITE_TAC[dist;arcV]
1461 THEN STRIP_TAC
1462 THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
1463 THEN RESA_TAC
1464 THEN MP_TAC(ISPEC`h:real`ACS_COS)
1465 THEN RESA_TAC
1466 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
1467 THEN RESA_TAC
1468 THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
1469 THEN POP_ASSUM MATCH_MP_TAC
1470 THEN REWRITE_TAC[COS_BOUNDS]
1471 THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
1472 THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
1473 THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
1474 THEN REAL_ARITH_TAC](*7*)](*6*);(*5*)
1475
1476 MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1477 `e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
1478 THEN ASM_REWRITE_TAC[]
1479 THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
1480 THENL(*6*)[
1481
1482 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1483   `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1484   `&0`;
1485 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
1486 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
1487 THEN DISCH_TAC
1488 THEN POP_ASSUM MATCH_MP_TAC
1489 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
1490 THEN STRIP_TAC
1491 THENL(*7*)[
1492 MP_TAC(PI_WORKS)
1493 THEN REAL_ARITH_TAC;(*7*)
1494
1495 STRIP_TAC
1496 THENL(*8*)[
1497
1498 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1499 THEN REDUCE_ARITH_TAC
1500 THEN REDUCE_VECTOR_TAC
1501 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1502 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1503 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1504  ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1505 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1506 THEN REDUCE_ARITH_TAC
1507 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1508 THEN REDUCE_VECTOR_TAC
1509 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1510 THEN RESA_TAC
1511 THEN ASM_REWRITE_TAC[]
1512 THEN REWRITE_TAC[e1_fan]
1513 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1514 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1515 THEN ONCE_REWRITE_TAC[DOT_SYM]
1516 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1517 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1518 THEN ASM_REWRITE_TAC[]
1519 THEN REDUCE_VECTOR_TAC
1520 THEN STRIP_TAC
1521 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1522 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1523 THEN REWRITE_TAC[DOT_RZERO]
1524 THEN REAL_ARITH_TAC;(*8*)
1525
1526 REWRITE_TAC[SIN_0;COS_0]
1527 THEN REDUCE_ARITH_TAC
1528 THEN REDUCE_VECTOR_TAC
1529 THEN VECTOR_ARITH_TAC](*8*)](*7*);(*6*)
1530
1531
1532 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
1533 THEN RESA_TAC
1534 THEN POP_ASSUM MATCH_MP_TAC
1535 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1536 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1537 THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
1538 THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
1539 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
1540 THEN REDUCE_ARITH_TAC
1541 THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*6*)](*5*)](*4*)](*3*)](*2*)](*1*))));;
1542
1543
1544
1545
1546 let connected_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real.
1547 FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\  h< pi/ &2
1548 ==>connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h)))`,
1549 REPEAT STRIP_TAC
1550 THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`v:real^3`;
1551 ` u:real^3` ;`h:real`]rw_dart_is_image_set_spherical_coordinate)
1552 THEN RESA_TAC
1553 THEN ASM_REWRITE_TAC[]
1554 THEN ASSUME_TAC(ISPECL[`(azim (x:real^3) (v:real^3) (u:real^3) u)`; `(azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) `;`h:real`] r_is_connected_fan)
1555 THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`]CONTINUOUS_ON_EQ_CONTINUOUS_AT)
1556 THEN RESA_TAC
1557 THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`] CONNECTED_CONTINUOUS_IMAGE)
1558 THEN RESA_TAC
1559 THEN POP_ASSUM MATCH_MP_TAC
1560 THEN GEN_TAC
1561 THEN STRIP_TAC
1562 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;
1563 `u:real^3`;`x':real^3`]continuous_change_spherical_coordinate_fan)
1564 THEN REWRITE_TAC[change_spherical_coordinate_fan]
1565 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1566 THEN DISCH_TAC
1567 THEN MATCH_MP_TAC CONTINUOUS_ADD
1568 THEN ASM_REWRITE_TAC[]
1569 THEN SIMP_TAC[CONTINUOUS_CONST]);;
1570
1571
1572 let not_empty_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1573 FAN(x,V,E)/\ {v,u} IN E
1574 ==>
1575 (!h:real. &0<h /\ h< pi/ &2
1576 ==>
1577 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={}))`,
1578 REPEAT STRIP_TAC
1579 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1580 THEN MRESA_TAC rw_dart_is_image_set_spherical_coordinate[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`h:real`]
1581 THEN POP_ASSUM MP_TAC
1582 THEN REWRITE_TAC[IMAGE_EQ_EMPTY;r_fan;EXTENSION;IN_ELIM_THM;IN;EMPTY;NOT_FORALL_THM;AZIM_REFL;azim_fan]
1583 THEN DISJ_CASES_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) V E) > 1)\/ CARD (set_of_edge v V E) > 1`)
1584 THENL[
1585 ASM_REWRITE_TAC[]
1586 THEN EXISTS_TAC`vector[&1; pi; h/ &2]:real^3`
1587 THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1588 THEN MP_TAC PI_WORKS
1589 THEN ASM_TAC
1590 THEN REAL_ARITH_TAC;
1591
1592 ASM_REWRITE_TAC[]
1593 THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge v V E = {u:real^3})\/  ~(set_of_edge v V E = {u})`)
1594 THENL[
1595 MRESA_TAC CARD_SING[`u:real^3`; `(set_of_edge v V E):real^3->bool`]
1596 THEN FIND_ASSUM MP_TAC `CARD ((set_of_edge v V E):real^3->bool) >1`
1597 THEN POP_ASSUM MP_TAC
1598 THEN POP_ASSUM (fun TH-> REWRITE_TAC[TH])
1599 THEN ARITH_TAC;
1600
1601 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))= &0) \/ ~(azim (x:real^3)  (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = &0)`)
1602 THENL[
1603 MRESA_TAC SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(v:real^3)`;`(u:real^3)`]
1604 THEN MRESA_TAC UNIQUE_AZIM_0_POINT_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`]
1605 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`v:real^3`];
1606
1607 MRESA_TAC azim[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`]
1608 THEN EXISTS_TAC`vector[&1; (azim x v u ((sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))))/ &2;h/ &2]:real^3`
1609 THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1610 THEN ASM_TAC
1611 THEN REAL_ARITH_TAC]]]);;
1612
1613
1614
1615 let JGIYDLE=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1616 FAN(x,V,E)/\ {v,u} IN E
1617 ==>
1618 (!h:real. &0<h /\ h< pi/ &2
1619 ==>
1620 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={}))
1621 /\(!h:real h1:real. h1 <= h
1622 ==>
1623 (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h1))
1624
1625 /\
1626 (?h:real.
1627 &1> h /\
1628 h> &0 /\
1629 rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h  SUBSET yfan(x,V,E))
1630 /\
1631 (!h:real. &0 <h /\  h< pi/ &2
1632 ==> connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))))`,
1633 MESON_TAC[not_empty_rw_dart_fan;continuous_set_fan;rw_dart_avoids_fan;connected_rw_dart_fan]);;
1634
1635
1636
1637
1638 end;;