(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: URRPHBZ3                                                 *)
(*      Chaper    : Packing (Marchal cells)                                  *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
     
(*  flyspeck_needs "packing/marchal_cells_2.hl";;                            *)
(*  flyspeck_needs "packing/HDTFNFZ.hl";;                                    *)
(* ========================================================================= *)

module Urrphbz3 = struct

open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;
open Hdtfnfz;;

 
let URRPHBZ3 = prove_by_refinement (URRPHBZ3_concl,
[(REPEAT STRIP_TAC);
 (ABBREV_TAC `X = mcell k V ul`);
 (SWITCH_TAC);
 (UP_ASM_TAC THEN REWRITE_WITH `VX V X = V INTER X`);
 (MATCH_MP_TAC HDTFNFZ);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `k:num`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SET_RULE `A DIFF A INTER B = A DIFF B`; IN_DIFF]);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `open ((:real^3) DIFF X)`);
 (REWRITE_TAC[GSYM closed]);
 (EXPAND_TAC "X" THEN ASM_SIMP_TAC[CLOSED_MCELL]);
 (UP_ASM_TAC THEN REWRITE_TAC[OPEN_CONTAINS_CBALL]);
 (STRIP_TAC);
 (NEW_GOAL `?e. &0 < e /\ cball (v:real^3,e) SUBSET (:real^3) DIFF X`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[cball; SUBSET; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e:real`);
 (REPEAT STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `e < dist (p, v:real^3) <=> ~(dist (v, p) <= e)`);
 (REWRITE_TAC[DIST_SYM]);
 (REAL_ARITH_TAC);
 (STRIP_TAC);

 (NEW_GOAL `((:real^3) DIFF X) (p:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `~(X (p:real^3))`);
 (UP_ASM_TAC);
 (REWRITE_WITH `((:real^3) DIFF X) p ==> ~X p <=>  p IN ((:real^3) DIFF X) ==> ~(p IN X)`);
 (ASM_REWRITE_TAC[IN]);
 (SET_TAC[]);
 (ASM_MESON_TAC[])]);;

end;;