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

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

module Hdtfnfz = 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;;


let HDTFNFZ_concl = 
`!V ul k v X.
     saturated V /\
     packing V /\
     barV V 3 ul /\
     X = mcell k V ul /\ ~(NULLSET X)
     ==> VX V X = V INTER X`;;

let HDTFNFZ = prove_by_refinement (HDTFNFZ_concl,
[(REPEAT STRIP_TAC);
 (REWRITE_TAC[VX]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (LET_TAC);
 (COND_CASES_TAC);  (* break into 2 subgoals k' = 0 and k' > 0 *)

 (UNDISCH_TAC `cell_params V X = k',ul'`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[cell_params]);
 (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);
 (DISCH_TAC);
 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SELECT_AX);
 (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);
 (EXPAND_TAC "P");
 (COND_CASES_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
 (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);
 (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);
 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);
 (UP_ASM_TAC THEN EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `X = mcell k' V ul'`; ASSUME `k' = 0` ]);
 (MATCH_MP_TAC LEPJBDJ_0);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
   (* Finish the case k' = 0  *)

   (* Continue with the case k' > 0  *)

 (UNDISCH_TAC `cell_params V X = k',ul'`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[cell_params]);
 (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);
 (DISCH_TAC);
 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SELECT_AX);
 (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);
 (EXPAND_TAC "P");
 (COND_CASES_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
 (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);
 (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);
 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);
 (UP_ASM_TAC THEN EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 (REWRITE_TAC[ASSUME `X = mcell k' V ul'`]);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_SET_TAC[]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `X:real^3->bool = {}`);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `NULLSET (X:real^3->bool)`);
 (ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
 (ASM_MESON_TAC[])]);;

end;;