text_formalization/packing/URRPHBZ3.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma: URRPHBZ3                                                 *)\r
   6 (*      Chaper    : Packing (Marchal cells)                                  *)\r
   7 (*                                                                           *)\r
   8 (* ========================================================================= *)\r
   9 \r
  10 (* ========================================================================= *)\r
  11 (*                     FILES NEED TO BE LOADED                               *)\r
  12      \r
  13 (*  flyspeck_needs "packing/marchal_cells_2.hl";;                            *)\r
  14 (*  flyspeck_needs "packing/HDTFNFZ.hl";;                                    *)\r
  15 (* ========================================================================= *)\r
  16 \r
  17 module Urrphbz3 = struct\r
  18 \r
  19 open Rogers;;\r
  20 open Vukhacky_tactics;;\r
  21 open Pack_defs;;\r
  22 open Pack_concl;; \r
  23 open Pack1;;\r
  24 open Sphere;; \r
  25 open Marchal_cells;;\r
  26 open Emnwuus;;\r
  27 open Marchal_cells_2_new;;\r
  28 open Lepjbdj;;\r
  29 open Hdtfnfz;;\r
  30 \r
  31  let URRPHBZ3 = prove_by_refinement (URRPHBZ3_concl,\r
  32 [(REPEAT STRIP_TAC);\r
  33  (ABBREV_TAC `X = mcell k V ul`);\r
  34  (SWITCH_TAC);\r
  35  (UP_ASM_TAC THEN REWRITE_WITH `VX V X = V INTER X`);\r
  36  (MATCH_MP_TAC HDTFNFZ);\r
  37  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `k:num`);\r
  38  (ASM_REWRITE_TAC[]);\r
  39  (REWRITE_TAC[SET_RULE `A DIFF A INTER B = A DIFF B`; IN_DIFF]);\r
  40  (REPEAT STRIP_TAC);\r
  41 \r
  42  (NEW_GOAL `open ((:real^3) DIFF X)`);\r
  43  (REWRITE_TAC[GSYM closed]);\r
  44  (EXPAND_TAC "X" THEN ASM_SIMP_TAC[CLOSED_MCELL]);\r
  45  (UP_ASM_TAC THEN REWRITE_TAC[OPEN_CONTAINS_CBALL]);\r
  46  (STRIP_TAC);\r
  47  (NEW_GOAL `?e. &0 < e /\ cball (v:real^3,e) SUBSET (:real^3) DIFF X`);\r
  48  (FIRST_ASSUM MATCH_MP_TAC);\r
  49  (ASM_SET_TAC[]);\r
  50  (UP_ASM_TAC THEN REWRITE_TAC[cball; SUBSET; IN; IN_ELIM_THM]);\r
  51  (REPEAT STRIP_TAC);\r
  52  (EXISTS_TAC `e:real`);\r
  53  (REPEAT STRIP_TAC);\r
  54  (ASM_REAL_ARITH_TAC);\r
  55  (REWRITE_WITH `e < dist (p, v:real^3) <=> ~(dist (v, p) <= e)`);\r
  56  (REWRITE_TAC[DIST_SYM]);\r
  57  (REAL_ARITH_TAC);\r
  58  (STRIP_TAC);\r
  59 \r
  60  (NEW_GOAL `((:real^3) DIFF X) (p:real^3)`);\r
  61  (FIRST_ASSUM MATCH_MP_TAC);\r
  62  (ASM_SIMP_TAC[]);\r
  63  (NEW_GOAL `~(X (p:real^3))`);\r
  64  (UP_ASM_TAC);\r
  65  (REWRITE_WITH `((:real^3) DIFF X) p ==> ~X p <=>  p IN ((:real^3) DIFF X) ==> ~(p IN X)`);\r
  66  (ASM_REWRITE_TAC[IN]);\r
  67  (SET_TAC[]);\r
  68  (ASM_MESON_TAC[])]);;\r
  69 \r
  70 end;;\r
  71 \r