text_formalization/tame/CKQOWSA.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Tame Hypermap                                                     *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2010-07-07                                                           *)\r
   7 (* (V,ESTD V) is a fan                                                        *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 flyspeck_needs "tame/CKQOWSA_4.hl";;\r
  11 flyspeck_needs "tame/tame_defs.hl";;\r
  12 flyspeck_needs "packing/pack2.hl";;\r
  13 \r
  14 \r
  15 module Ckqowsa = struct\r
  16 \r
  17 \r
  18 open Fan_defs;;\r
  19 open Ckqowsa_3_points;;\r
  20 open Ckqowsa_4_points;;\r
  21 \r
  22 \r
  23 let packing = prove(`!V. packing V <=> (!v w. v IN V /\ w IN V /\ ~(v = w) ==> &2 <= dist (v,w))`,\r
  24    REWRITE_TAC[Sphere.packing; IN]);;\r
  25 \r
  26 \r
  27 (* UNIONS (ESTD V) SUBSET V /\ graph (ESTD V) *)\r
  28 \r
  29 let ESTD_fan0 = prove(`!V. UNIONS (ESTD V) SUBSET V /\ graph (ESTD V)`,\r
  30    REPEAT STRIP_TAC THENL\r
  31      [\r
  32        REWRITE_TAC[SUBSET; IN_UNIONS; Tame_defs.ESTD; IN_ELIM_THM] THEN\r
  33          REPEAT STRIP_TAC THEN\r
  34          POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Collect_geom.IN_SET2] THEN\r
  35          DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[];\r
  36        ALL_TAC\r
  37      ] THEN\r
  38      REWRITE_TAC[graph; Tame_defs.ESTD; IN_ELIM_THM] THEN\r
  39      REPEAT STRIP_TAC THEN\r
  40      ASM_REWRITE_TAC[HAS_SIZE_2_EXISTS] THEN\r
  41      MAP_EVERY EXISTS_TAC [`v:real^3`; `w:real^3`] THEN\r
  42      ASM_REWRITE_TAC[Collect_geom.IN_SET2]);;\r
  43 \r
  44 \r
  45 (* fan1 (V,ESTD V) <=> FINITE V /\ ~(V = {}) *)\r
  46 \r
  47 let ESTD_fan1 = prove(`!V. V SUBSET ball_annulus /\ packing V /\ ~(V = {}) ==> fan1 (vec 0:real^3, V, ESTD V)`,\r
  48    SIMP_TAC[Pack_defs.ball_annulus; fan1; SUBSET_EMPTY] THEN\r
  49      REWRITE_TAC[SUBSET; cball; IN_DIFF; IN_ELIM_THM] THEN\r
  50      REPEAT STRIP_TAC THEN\r
  51      SUBGOAL_THEN `V = V INTER ball(vec 0:real^3, &4)` (fun th -> ONCE_REWRITE_TAC[th]) THENL\r
  52      [\r
  53        REWRITE_TAC[EXTENSION; IN_INTER; ball; IN_ELIM_THM] THEN\r
  54          GEN_TAC THEN\r
  55          EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
  56          MATCH_MP_TAC REAL_LET_TRANS THEN\r
  57          EXISTS_TAC `&2 * h0` THEN\r
  58          ASM_SIMP_TAC[Sphere.h0] THEN\r
  59          REAL_ARITH_TAC;\r
  60        ALL_TAC\r
  61      ] THEN\r
  62      ASM_SIMP_TAC[Pack2.KIUMVTC]);;\r
  63 \r
  64 \r
  65 \r
  66 (* fan2 (V,ESTD V) <=> ~(vec 0 IN V) *)\r
  67 \r
  68 let ESTD_fan2 = prove(`!V. V SUBSET ball_annulus ==> fan2 (vec 0, V, ESTD V)`,\r
  69    REWRITE_TAC[SUBSET] THEN\r
  70      REPEAT STRIP_TAC THEN\r
  71      REWRITE_TAC[fan2] THEN\r
  72      STRIP_TAC THEN\r
  73      FIRST_X_ASSUM (MP_TAC o SPEC `vec 0:real^3`) THEN\r
  74      ASM_REWRITE_TAC[in_ball_annulus]);;\r
  75 \r
  76 \r
  77 (* fan6 (V,ESTD V) <=> ~collinear {vec 0, e} *)\r
  78 \r
  79 let ESTD_fan6 = prove(`!V. V SUBSET ball_annulus /\ packing V ==> fan6 (vec 0, V, ESTD V)`,\r
  80    REWRITE_TAC[SUBSET; Sphere.packing; fan6; Tame_defs.ESTD; IN_ELIM_THM] THEN\r
  81      REPEAT STRIP_TAC THEN\r
  82      POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN\r
  83      ASM_REWRITE_TAC[SET_RULE `{vec 0:real^3} UNION {v,w} = {vec 0,v,w}`] THEN\r
  84      MATCH_MP_TAC estd_non_collinear_lemma THEN\r
  85      ASM_SIMP_TAC[] THEN\r
  86      FIRST_X_ASSUM MATCH_MP_TAC THEN\r
  87      REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binary "IN" o concl))) THEN\r
  88      ASM_SIMP_TAC[IN]);;\r
  89 \r
  90 \r
  91 (* fan7 *)\r
  92 \r
  93 (* 2 points *)\r
  94 \r
  95 let fan7_2 = prove(`!V v w. V SUBSET ball_annulus /\ packing V /\ v IN V /\ w IN V\r
  96                      ==> aff_ge {vec 0} {v} INTER aff_ge {vec 0} {w} = aff_ge {vec 0} ({v} INTER {w})`,\r
  97    REWRITE_TAC[SUBSET; packing] THEN\r
  98      REPEAT STRIP_TAC THEN\r
  99      ASM_CASES_TAC `v = w:real^3` THENL\r
 100      [\r
 101        ASM_REWRITE_TAC[INTER_ACI];\r
 102        ALL_TAC\r
 103      ] THEN\r
 104 \r
 105      SUBGOAL_THEN `{v} INTER {w:real^3} = {}` (fun th -> REWRITE_TAC[th]) THENL\r
 106      [\r
 107        REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_SING; IN_INTER] THEN\r
 108          GEN_TAC THEN POP_ASSUM MP_TAC THEN\r
 109          REWRITE_TAC[CONTRAPOS_THM] THEN\r
 110          STRIP_TAC THEN\r
 111          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);\r
 112        ALL_TAC\r
 113      ] THEN\r
 114 \r
 115      REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN\r
 116      REWRITE_TAC[EXTENSION; IN_SING; HALFLINE; IN_INTER; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN\r
 117      GEN_TAC THEN\r
 118      EQ_TAC THENL\r
 119      [\r
 120        REPEAT STRIP_TAC THEN\r
 121          ASM_CASES_TAC `t = &0` THENL [ ASM_REWRITE_TAC[VECTOR_MUL_LZERO]; ALL_TAC ] THEN\r
 122          UNDISCH_TAC `x = t % v:real^3` THEN\r
 123          DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv t % v`) THEN\r
 124          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 125          ABBREV_TAC `c = inv t * t'` THEN\r
 126          SUBGOAL_THEN `&0 <= c` ASSUME_TAC THENL [ EXPAND_TAC "c" THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN\r
 127          SUBGOAL_THEN `abs c = c` ASSUME_TAC THENL [ ASM_REWRITE_TAC[REAL_ABS_REFL]; ALL_TAC ] THEN\r
 128          DISCH_THEN (LABEL_TAC "v") THEN\r
 129          ASM_CASES_TAC `c <= &1` THENL\r
 130          [\r
 131            SUBGOAL_THEN `&2 + &2 <= norm (v:real^3) + dist (v,w)` MP_TAC THENL\r
 132              [\r
 133                MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 134                  ASM_SIMP_TAC[] THEN\r
 135                  REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`)) THEN\r
 136                  ASM_SIMP_TAC[in_ball_annulus];\r
 137                ALL_TAC\r
 138              ] THEN\r
 139 \r
 140              REMOVE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN\r
 141              ASM_REWRITE_TAC[dist; NORM_MUL; VECTOR_ARITH `c % w - w = --(&1 - c) % w:real^3`] THEN\r
 142              REWRITE_TAC[REAL_ABS_NEG] THEN\r
 143              SUBGOAL_THEN `abs (&1 - c) = &1 - c` (fun th -> REWRITE_TAC[th]) THENL [ ASM_REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &1 - c <=> c <= &1`]; ALL_TAC ] THEN\r
 144              REWRITE_TAC[REAL_ARITH `c * nw + (&1 - c) * nw = nw`] THEN\r
 145              REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`)) THEN\r
 146              ASM_REWRITE_TAC[in_ball_annulus; Sphere.h0] THEN\r
 147              REAL_ARITH_TAC;\r
 148            ALL_TAC\r
 149          ] THEN\r
 150 \r
 151          POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN\r
 152          SUBGOAL_THEN `&2 + &2 <= norm (w:real^3) + dist (v,w)` MP_TAC THENL\r
 153          [\r
 154            MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 155              ASM_SIMP_TAC[] THEN\r
 156              REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`)) THEN\r
 157              ASM_SIMP_TAC[in_ball_annulus];\r
 158            ALL_TAC\r
 159          ] THEN\r
 160 \r
 161          USE_THEN "v" (fun th -> REWRITE_TAC[SYM th]) THEN\r
 162          ASM_REWRITE_TAC[dist; NORM_MUL; VECTOR_ARITH `c % w - w = (c - &1) % w:real^3`] THEN\r
 163          SUBGOAL_THEN `abs (c - &1) = c - &1` (fun th -> REWRITE_TAC[th]) THENL [ ASM_SIMP_TAC[REAL_ABS_REFL; REAL_ARITH `&1 < c ==> &0 <= c - &1`]; ALL_TAC ] THEN\r
 164          REWRITE_TAC[REAL_ARITH `nw + (c - &1) * nw = c * nw`] THEN\r
 165          UNDISCH_TAC `abs c = c` THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN\r
 166          ASM_REWRITE_TAC[GSYM NORM_MUL] THEN\r
 167          REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`)) THEN\r
 168          ASM_REWRITE_TAC[in_ball_annulus; Sphere.h0] THEN\r
 169          REAL_ARITH_TAC;\r
 170        ALL_TAC\r
 171      ] THEN\r
 172 \r
 173      REPEAT STRIP_TAC THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL]);;\r
 174 \r
 175 \r
 176 (* 3 points *)\r
 177 \r
 178 let fan7_3 = prove(`!V e u. V SUBSET ball_annulus /\ packing V /\ u IN V /\ e IN ESTD V\r
 179                        ==> aff_ge {vec 0} {u} INTER aff_ge {vec 0} e = aff_ge {vec 0} ({u} INTER e)`,\r
 180    REWRITE_TAC[SUBSET; Tame_defs.ESTD; IN_ELIM_THM; packing] THEN\r
 181      REPEAT STRIP_TAC THEN\r
 182      SUBGOAL_THEN `~(v = vec 0:real^3) /\ ~(w = vec 0:real^3)` ASSUME_TAC THENL\r
 183      [\r
 184        FIRST_X_ASSUM (MP_TAC o SPEC `v:real^3`) THEN\r
 185          MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`v:real^3`; `w:real^3`] THEN\r
 186          ASM_SIMP_TAC[in_ball_annulus];\r
 187        ALL_TAC\r
 188      ] THEN\r
 189 \r
 190      ASM_CASES_TAC `u:real^3 IN e` THENL\r
 191      [\r
 192        SUBGOAL_THEN `{u:real^3} INTER e = {u}` (fun th -> REWRITE_TAC[th]) THENL\r
 193          [\r
 194            REWRITE_TAC[EXTENSION; IN_INTER; IN_SING] THEN\r
 195              GEN_TAC THEN\r
 196              EQ_TAC THENL\r
 197              [\r
 198                SIMP_TAC[];\r
 199                DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 200                  POP_ASSUM (fun th -> REWRITE_TAC[th])\r
 201              ];\r
 202            ALL_TAC\r
 203          ] THEN\r
 204 \r
 205          REWRITE_TAC[GSYM SUBSET_INTER_ABSORPTION] THEN\r
 206          ASM_SIMP_TAC[aff_ge_0_2; HALFLINE] THEN\r
 207          POP_ASSUM MP_TAC THEN\r
 208          ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; SUBSET; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN\r
 209          REPEAT STRIP_TAC THENL\r
 210          [\r
 211            MAP_EVERY EXISTS_TAC [`t:real`; `&0`];\r
 212            MAP_EVERY EXISTS_TAC [`&0`; `t:real`]\r
 213          ] THEN\r
 214          ASM_REWRITE_TAC[REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_ADD_RID];\r
 215        ALL_TAC\r
 216      ] THEN\r
 217 \r
 218      SUBGOAL_THEN `{u:real^3} INTER e = {}` (fun th -> REWRITE_TAC[th]) THENL\r
 219      [\r
 220        REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_SING] THEN\r
 221          GEN_TAC THEN STRIP_TAC THEN\r
 222          POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 223          POP_ASSUM (fun th -> REWRITE_TAC[th]);\r
 224        ALL_TAC\r
 225      ] THEN\r
 226 \r
 227      REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN\r
 228      ASM_CASES_TAC `aff_ge {vec 0} {u:real^3} INTER aff_ge {vec 0} e = {vec 0}` THEN ASM_REWRITE_TAC[] THEN\r
 229 \r
 230      SUBGOAL_THEN `?p. ~(p = vec 0:real^3) /\ p IN aff_ge {vec 0} {u} INTER aff_ge {vec 0} e` MP_TAC THENL\r
 231      [\r
 232        POP_ASSUM MP_TAC THEN\r
 233          REWRITE_TAC[EXTENSION; IN_SING; NOT_FORALL_THM] THEN\r
 234          DISCH_THEN (CHOOSE_THEN MP_TAC) THEN\r
 235          ASM_CASES_TAC `x = vec 0:real^3` THENL\r
 236          [\r
 237            ASM_REWRITE_TAC[IN_INTER; points_in_aff_ge_0_2; ENDS_IN_HALFLINE];\r
 238            ALL_TAC\r
 239          ] THEN\r
 240          ASM_REWRITE_TAC[] THEN\r
 241          DISCH_TAC THEN\r
 242          EXISTS_TAC `x:real^3` THEN\r
 243          ASM_REWRITE_TAC[];\r
 244        ALL_TAC\r
 245      ] THEN\r
 246 \r
 247      ASM_REWRITE_TAC[IN_INTER] THEN STRIP_TAC THEN\r
 248      UNDISCH_TAC `p IN aff_ge {vec 0} {u:real^3}` THEN\r
 249      ASM_SIMP_TAC[HALFLINE; VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN STRIP_TAC THEN\r
 250      POP_ASSUM MP_TAC THEN\r
 251      ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN\r
 252      DISCH_THEN (MP_TAC o AP_TERM `\v:real^3. inv t % v`) THEN\r
 253      ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 254      DISCH_TAC THEN\r
 255 \r
 256      SUBGOAL_THEN `u:real^3 IN aff_ge {vec 0} {v,w}` ASSUME_TAC THENL\r
 257      [\r
 258        POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 259          UNDISCH_TAC `p IN aff_ge {vec 0:real^3} {v,w}` THEN\r
 260          ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN\r
 261          STRIP_TAC THEN\r
 262          MAP_EVERY EXISTS_TAC [`inv t * t1`; `inv t * t2`] THEN\r
 263          SUBGOAL_THEN `&0 <= inv t` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN\r
 264          REWRITE_TAC[CONJ_ASSOC] THEN\r
 265          CONJ_TAC THENL [ CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN\r
 266          ASM_REWRITE_TAC[] THEN\r
 267          VECTOR_ARITH_TAC;\r
 268        ALL_TAC\r
 269      ] THEN\r
 270 \r
 271      MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN\r
 272      MAP_EVERY EXISTS_TAC [`v:real^3`; `w:real^3`; `u:real^3`] THEN\r
 273      ASM_SIMP_TAC[] THEN\r
 274      UNDISCH_TAC `~(u:real^3 IN e)` THEN\r
 275      ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN\r
 276      ASM_SIMP_TAC[]);;\r
 277 \r
 278 \r
 279 \r
 280 (* 4 points *)\r
 281 \r
 282 let fan7_4_0 = prove(`!V e1 e2. V SUBSET ball_annulus /\ packing V /\ e1 IN ESTD V /\ e2 IN ESTD V /\\r
 283                        (e1 INTER e2) HAS_SIZE 0\r
 284                        ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2 = aff_ge {vec 0} (e1 INTER e2)`,\r
 285    REWRITE_TAC[SUBSET; packing; HAS_SIZE_0; Tame_defs.ESTD; IN_ELIM_THM] THEN\r
 286      REPEAT STRIP_TAC THEN\r
 287      FIRST_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 288      ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN\r
 289      MATCH_MP_TAC LEMMA_4_POINTS_FINAL THEN\r
 290      ASM_SIMP_TAC[] THEN\r
 291      REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 292      POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 293      SET_TAC[]);;\r
 294 \r
 295 \r
 296 \r
 297 let fan7_4_1_one_case = prove(`!V v1 v2 v3 v4. V SUBSET ball_annulus /\ packing V /\ v1 IN V /\ v2 IN V /\ v3 IN V /\ v4 IN V /\\r
 298                                 ~(v1 = v3) /\ ~(v2 = v4) /\ v1 = v2 /\ ~(v3 = v4) /\\r
 299                                 dist (v1,v3) <= &2 * h0 /\ dist (v2,v4) <= &2 * h0\r
 300                                 ==> aff_ge {vec 0} {v1,v3} INTER aff_ge {vec 0} {v2,v4} = aff_ge {vec 0} ({v1,v3} INTER {v2,v4})`,\r
 301    REWRITE_TAC[SUBSET; packing] THEN REPEAT STRIP_TAC THEN\r
 302      ASM_REWRITE_TAC[] THEN\r
 303      SUBGOAL_THEN `{v2,v3} INTER {v2,v4} = {v2:real^3}` (fun th -> REWRITE_TAC[th]) THENL\r
 304      [\r
 305        REWRITE_TAC[EXTENSION; IN_INTER; IN_SING; IN_INSERT; NOT_IN_EMPTY] THEN\r
 306          GEN_TAC THEN\r
 307          ASM_CASES_TAC `x = v2:real^3` THEN ASM_REWRITE_TAC[] THEN\r
 308          STRIP_TAC THEN POP_ASSUM MP_TAC THEN\r
 309          POP_ASSUM (fun th -> ASM_REWRITE_TAC[th]);\r
 310        ALL_TAC\r
 311      ] THEN\r
 312 \r
 313      SUBGOAL_THEN `~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL\r
 314      [\r
 315        FIRST_X_ASSUM (MP_TAC o SPEC `x:real^3`) THEN\r
 316          MAP_EVERY (fun tm -> FIRST_ASSUM (MP_TAC o SPEC tm)) [`v2:real^3`; `v3:real^3`; `v4:real^3`] THEN\r
 317          ASM_SIMP_TAC[in_ball_annulus];\r
 318        ALL_TAC\r
 319      ] THEN\r
 320 \r
 321      ASM_SIMP_TAC[aff_ge_0_2] THEN\r
 322      REWRITE_TAC[EXTENSION; IN_INTER; HALFLINE; VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN\r
 323      GEN_TAC THEN EQ_TAC THENL\r
 324      [\r
 325        STRIP_TAC THEN\r
 326          POP_ASSUM (LABEL_TAC "x2" o SYM) THEN\r
 327          UNDISCH_TAC `x = t1 % v2 + t2 % v3:real^3` THEN\r
 328          DISCH_THEN (LABEL_TAC "x1" o SYM) THEN\r
 329 \r
 330          ASM_CASES_TAC `t1 <= t1'` THENL\r
 331          [\r
 332            ASM_CASES_TAC `t2 = &0` THENL\r
 333              [\r
 334                EXISTS_TAC `t1:real` THEN\r
 335                  REMOVE_THEN "x1" MP_TAC THEN\r
 336                  ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];\r
 337                ALL_TAC\r
 338              ] THEN\r
 339 \r
 340              REMOVE_THEN "x1" (MP_TAC o AP_TERM `\v:real^3. inv t2 % v`) THEN\r
 341              REMOVE_THEN "x2" (fun th -> REWRITE_TAC[SYM th]) THEN\r
 342              ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 343              REWRITE_TAC[VECTOR_ARITH `a % v2 + v3:real^3 = b % v2 + c % v4 <=> v3 = (b - a) % v2 + c % v4`] THEN\r
 344              REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN DISCH_TAC THEN\r
 345              SUBGOAL_THEN `v3:real^3 IN aff_ge {vec 0} {v2, v4}` ASSUME_TAC THENL\r
 346              [\r
 347                ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN\r
 348                  MAP_EVERY EXISTS_TAC [`inv t2 * (t1' - t1)`; `inv t2 * t2'`] THEN\r
 349                  SUBGOAL_THEN `&0 <= inv t2` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN\r
 350                  REWRITE_TAC[] THEN\r
 351                  CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= t1' - t1 <=> t1 <= t1'`];\r
 352                ALL_TAC\r
 353              ] THEN\r
 354 \r
 355              MATCH_MP_TAC (TAUT `F ==> A`) THEN\r
 356              MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN\r
 357              MAP_EVERY EXISTS_TAC [`v2:real^3`; `v4:real^3`; `v3:real^3`] THEN\r
 358              POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN REMOVE_ASSUM THEN\r
 359              ASM_SIMP_TAC[] THEN\r
 360              FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 361              ASM_REWRITE_TAC[] THEN\r
 362              UNDISCH_TAC `v1 = v2:real^3` THEN DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);\r
 363            ALL_TAC\r
 364          ] THEN\r
 365 \r
 366          POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN\r
 367          ASM_CASES_TAC `t2' = &0` THENL\r
 368          [\r
 369            EXISTS_TAC `t1':real` THEN\r
 370              REMOVE_THEN "x2" MP_TAC THEN\r
 371              ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID];\r
 372            ALL_TAC\r
 373          ] THEN\r
 374 \r
 375          REMOVE_THEN "x2" (MP_TAC o AP_TERM `\v:real^3. inv t2' % v`) THEN\r
 376          REMOVE_THEN "x1" (fun th -> REWRITE_TAC[SYM th]) THEN\r
 377          ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 378          REWRITE_TAC[VECTOR_ARITH `a % v2 + v4:real^3 = b % v2 + c % v3 <=> v4 = (b - a) % v2 + c % v3`] THEN\r
 379          REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN DISCH_TAC THEN\r
 380          SUBGOAL_THEN `v4:real^3 IN aff_ge {vec 0} {v2, v3}` ASSUME_TAC THENL\r
 381          [\r
 382            ASM_SIMP_TAC[aff_ge_0_2; IN_ELIM_THM] THEN\r
 383              MAP_EVERY EXISTS_TAC [`inv t2' * (t1 - t1')`; `inv t2' * t2`] THEN\r
 384              SUBGOAL_THEN `&0 <= inv t2'` ASSUME_TAC THENL [ MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN\r
 385              REWRITE_TAC[] THEN\r
 386              CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_ARITH `t1' < t1 ==> &0 <= t1 - t1'`];\r
 387            ALL_TAC\r
 388          ] THEN\r
 389 \r
 390          MATCH_MP_TAC (TAUT `F ==> A`) THEN\r
 391          MATCH_MP_TAC LEMMA_3_POINTS_FINAL THEN\r
 392          MAP_EVERY EXISTS_TAC [`v2:real^3`; `v3:real^3`; `v4:real^3`] THEN\r
 393          POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN REMOVE_ASSUM THEN\r
 394          ASM_SIMP_TAC[] THEN\r
 395          UNDISCH_TAC `v1 = v2:real^3` THEN DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);\r
 396        ALL_TAC\r
 397      ] THEN\r
 398 \r
 399      STRIP_TAC THEN\r
 400      CONJ_TAC THEN MAP_EVERY EXISTS_TAC [`t:real`; `&0`] THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; REAL_LE_REFL]);;\r
 401 \r
 402 \r
 403 \r
 404 let fan7_4_1_cases = prove(`!v w v' w':A. ~(v = w) /\ ~(v' = w') /\ ({v,w} INTER {v',w'}) HAS_SIZE 1\r
 405                              ==> (v = v' /\ ~(w = w')) \/ (v = w' /\ ~(w = v')) \/\r
 406                                  (w = v' /\ ~(v = w')) \/ (w = w' /\ ~(v = v'))`,\r
 407    REPEAT STRIP_TAC THEN\r
 408      POP_ASSUM (LABEL_TAC "A") THEN\r
 409      ASM_CASES_TAC `v = v':A` THEN ASM_REWRITE_TAC[] THENL\r
 410      [\r
 411        DISJ1_TAC THEN\r
 412          DISCH_TAC THEN\r
 413          REMOVE_THEN "A" MP_TAC THEN\r
 414          ASM_REWRITE_TAC[INTER_ACI] THEN\r
 415          REWRITE_TAC[HAS_SIZE_1_EXISTS; EXISTS_UNIQUE; NOT_EXISTS_THM; DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN\r
 416          ASM_MESON_TAC[];\r
 417        ALL_TAC\r
 418      ] THEN\r
 419 \r
 420      ASM_CASES_TAC `v = w':A` THEN ASM_REWRITE_TAC[] THENL\r
 421      [\r
 422        DISJ1_TAC THEN\r
 423          DISCH_TAC THEN\r
 424          REMOVE_THEN "A" MP_TAC THEN\r
 425          ASM_REWRITE_TAC[INTER_ACI; Collect_geom.PER_SET2] THEN\r
 426          REWRITE_TAC[HAS_SIZE_1_EXISTS; EXISTS_UNIQUE; NOT_EXISTS_THM; DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN\r
 427          ASM_MESON_TAC[];\r
 428        ALL_TAC\r
 429      ] THEN\r
 430 \r
 431      ASM_CASES_TAC `w = v':A` THEN ASM_REWRITE_TAC[] THEN\r
 432      REMOVE_THEN "A" MP_TAC THEN\r
 433      REWRITE_TAC[HAS_SIZE_1_EXISTS; EXISTS_UNIQUE; IN_INTER; IN_INSERT; NOT_IN_EMPTY] THEN\r
 434      ASM_MESON_TAC[]);;\r
 435 \r
 436 \r
 437 \r
 438 \r
 439 let fan7_4_1 = prove(`!V e1 e2. V SUBSET ball_annulus /\ packing V /\ e1 IN ESTD V /\ e2 IN ESTD V /\\r
 440                        (e1 INTER e2) HAS_SIZE 1\r
 441                        ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2 = aff_ge {vec 0} (e1 INTER e2)`,\r
 442    REWRITE_TAC[Tame_defs.ESTD; IN_ELIM_THM] THEN\r
 443      REPEAT STRIP_TAC THEN\r
 444      POP_ASSUM MP_TAC THEN\r
 445      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 446 \r
 447      MP_TAC (ISPECL [`v:real^3`; `w:real^3`; `v':real^3`; `w':real^3`] fan7_4_1_cases) THEN\r
 448      ASM_REWRITE_TAC[] THEN\r
 449      STRIP_TAC THENL\r
 450      [\r
 451        MATCH_MP_TAC fan7_4_1_one_case THEN\r
 452          EXISTS_TAC `V:real^3->bool` THEN\r
 453          ASM_REWRITE_TAC[];\r
 454 \r
 455        GEN_REWRITE_TAC (PAT_CONV `\x. s INTER aff_ge {vec 0:real^3} x = aff_ge {vec 0} (t INTER x)`) [Collect_geom.PER_SET2] THEN\r
 456          MATCH_MP_TAC fan7_4_1_one_case THEN\r
 457          EXISTS_TAC `V:real^3->bool` THEN\r
 458          ASM_REWRITE_TAC[DIST_SYM];\r
 459 \r
 460        GEN_REWRITE_TAC (PAT_CONV `\x. aff_ge {vec 0:real^3} x INTER s = aff_ge {vec 0} (x INTER t)`) [Collect_geom.PER_SET2] THEN\r
 461          MATCH_MP_TAC fan7_4_1_one_case THEN\r
 462          EXISTS_TAC `V:real^3->bool` THEN\r
 463          ASM_REWRITE_TAC[DIST_SYM] THEN\r
 464          UNDISCH_TAC `dist (v,w:real^3) <= &2 * h0` THEN\r
 465          ASM_SIMP_TAC[];\r
 466 \r
 467        ONCE_REWRITE_TAC[Collect_geom.PER_SET2] THEN\r
 468          MATCH_MP_TAC fan7_4_1_one_case THEN\r
 469          EXISTS_TAC `V:real^3->bool` THEN\r
 470          ASM_REWRITE_TAC[DIST_SYM] THEN\r
 471          UNDISCH_TAC `dist (v,w:real^3) <= &2 * h0` THEN\r
 472          ASM_SIMP_TAC[]\r
 473      ]);;\r
 474 \r
 475 \r
 476 \r
 477 let fan7_4_2 = prove(`!V e1 e2. e1 IN ESTD V /\ e2 IN ESTD V /\ (e1 INTER e2) HAS_SIZE 2\r
 478                        ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2 = aff_ge {vec 0} (e1 INTER e2)`,\r
 479    REPEAT STRIP_TAC THEN\r
 480      SUBGOAL_THEN `(e1:real^3->bool) HAS_SIZE 2 /\ (e2:real^3->bool) HAS_SIZE 2` STRIP_ASSUME_TAC THENL\r
 481      [\r
 482        MP_TAC (SPEC_ALL ESTD_fan0) THEN REWRITE_TAC[graph] THEN\r
 483          STRIP_TAC THEN\r
 484          CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[GSYM IN];\r
 485        ALL_TAC\r
 486      ] THEN\r
 487      REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN\r
 488      REWRITE_TAC[HAS_SIZE] THEN REPEAT DISCH_TAC THEN\r
 489 \r
 490      SUBGOAL_THEN `e1:real^3->bool = e2` MP_TAC THENL\r
 491      [\r
 492        MATCH_MP_TAC EQ_TRANS THEN\r
 493          EXISTS_TAC `e1 INTER e2:real^3->bool` THEN\r
 494          CONJ_TAC THENL\r
 495          [\r
 496            MATCH_MP_TAC EQ_SYM THEN\r
 497              MATCH_MP_TAC CARD_SUBSET_EQ THEN\r
 498              ASM_REWRITE_TAC[INTER_SUBSET];\r
 499            MATCH_MP_TAC CARD_SUBSET_EQ THEN\r
 500              ASM_REWRITE_TAC[INTER_SUBSET]\r
 501          ];\r
 502        ALL_TAC\r
 503      ] THEN\r
 504 \r
 505      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 506      REWRITE_TAC[INTER_ACI]);;\r
 507 \r
 508 \r
 509 \r
 510 \r
 511 let ESTD_fan7 = prove(`!V. V SUBSET ball_annulus /\ packing V ==> fan7 (vec 0, V, ESTD V)`,\r
 512    REWRITE_TAC[fan7; IN_UNION; IN_ELIM_THM] THEN\r
 513      REPEAT STRIP_TAC THENL\r
 514      [\r
 515        SUBGOAL_THEN `?n. n <= 2 /\ (e1:real^3->bool) INTER e2 HAS_SIZE n` MP_TAC THENL\r
 516          [\r
 517            SUBGOAL_THEN `e1:real^3->bool HAS_SIZE 2` MP_TAC THENL\r
 518            [\r
 519              MP_TAC (SPEC `V:real^3->bool` ESTD_fan0) THEN\r
 520                REWRITE_TAC[graph] THEN STRIP_TAC THEN\r
 521                FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 522                UNDISCH_TAC `e1 IN ESTD V` THEN\r
 523                SIMP_TAC[IN];\r
 524              ALL_TAC\r
 525            ] THEN\r
 526 \r
 527            REWRITE_TAC[HAS_SIZE] THEN\r
 528            STRIP_TAC THEN\r
 529            EXISTS_TAC `CARD (e1 INTER e2:real^3->bool)` THEN\r
 530            REWRITE_TAC[] THEN\r
 531            SUBGOAL_THEN `FINITE (e1 INTER e2:real^3->bool)` ASSUME_TAC THENL\r
 532            [\r
 533              MATCH_MP_TAC FINITE_SUBSET THEN\r
 534                EXISTS_TAC `e1:real^3->bool` THEN\r
 535                ASM_REWRITE_TAC[INTER_SUBSET];\r
 536              ALL_TAC\r
 537            ] THEN\r
 538 \r
 539            ASM_REWRITE_TAC[] THEN\r
 540            FIRST_X_ASSUM (fun th -> REWRITE_TAC [SYM th]) THEN\r
 541            MATCH_MP_TAC CARD_SUBSET THEN\r
 542            ASM_REWRITE_TAC[INTER_SUBSET];\r
 543            ALL_TAC\r
 544          ] THEN\r
 545 \r
 546          REWRITE_TAC[ARITH_RULE `n <= 2 <=> n = 0 \/ n = 1 \/ n = 2`] THEN\r
 547          REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THENL\r
 548          [\r
 549            MATCH_MP_TAC fan7_4_0 THEN\r
 550              EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[];\r
 551            MATCH_MP_TAC fan7_4_1 THEN\r
 552              EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[];\r
 553            MATCH_MP_TAC fan7_4_2 THEN\r
 554              EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]\r
 555          ];\r
 556 \r
 557        ASM_REWRITE_TAC[] THEN\r
 558          ONCE_REWRITE_TAC[INTER_ACI] THEN\r
 559          MATCH_MP_TAC fan7_3 THEN\r
 560          EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[];\r
 561 \r
 562        ASM_REWRITE_TAC[] THEN\r
 563          MATCH_MP_TAC fan7_3 THEN\r
 564          EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[];\r
 565 \r
 566        ASM_REWRITE_TAC[] THEN\r
 567          MATCH_MP_TAC fan7_2 THEN\r
 568          EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]\r
 569      ]);;\r
 570 \r
 571 \r
 572 (* CKQOWSA *)\r
 573 \r
 574 let CKQOWSA = prove(`!V. V SUBSET ball_annulus /\ packing V /\ ~(V = {}) ==> FAN (vec 0,V,ESTD V)`,\r
 575    REPEAT STRIP_TAC THEN\r
 576      REWRITE_TAC[Fan_defs.FAN] THEN\r
 577      ASM_SIMP_TAC[ESTD_fan0; ESTD_fan1; ESTD_fan2; ESTD_fan6; ESTD_fan7]);;\r
 578 \r
 579 \r
 580 end;;\r