1 (* ========================================================================= *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Authour : VU KHAC KY *)
\r
5 (* Book lemma: HDTFNFZ *)
\r
6 (* Chaper : Packing (Marchal cells) *)
\r
8 (* ========================================================================= *)
\r
10 (* ========================================================================= *)
\r
11 (* FILES NEED TO BE LOADED *)
\r
13 (* flyspeck_needs "packing/marchal_cells_2_new.hl";; *)
\r
14 (* flyspeck_needs "packing/LEPJBDJ.hl";; *)
\r
15 (* ========================================================================= *)
\r
17 module Hdtfnfz = struct
\r
21 open Vukhacky_tactics;;
\r
26 open Marchal_cells;;
\r
28 open Marchal_cells_2_new;;
\r
32 let HDTFNFZ_concl =
\r
37 X = mcell k V ul /\ ~(NULLSET X)
\r
38 ==> VX V X = V INTER X`;;
\r
40 let HDTFNFZ = prove_by_refinement (HDTFNFZ_concl,
\r
41 [(REPEAT STRIP_TAC);
\r
48 (COND_CASES_TAC); (* break into 2 subgoals k' = 0 and k' > 0 *)
\r
50 (UNDISCH_TAC `cell_params V X = k',ul'`);
\r
51 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
52 (REWRITE_TAC[cell_params]);
\r
53 (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);
\r
55 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);
\r
56 (ASM_REWRITE_TAC[]);
\r
57 (MATCH_MP_TAC SELECT_AX);
\r
58 (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);
\r
61 (REWRITE_TAC[BETA_THM]);
\r
62 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
\r
64 (REWRITE_TAC[BETA_THM]);
\r
65 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
\r
66 (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
\r
67 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);
\r
68 (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);
\r
69 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);
\r
70 (UP_ASM_TAC THEN EXPAND_TAC "P");
\r
71 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
\r
72 (REWRITE_TAC[ASSUME `X = mcell k' V ul'`; ASSUME `k' = 0` ]);
\r
73 (MATCH_MP_TAC LEPJBDJ_0);
\r
74 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
\r
75 (* Finish the case k' = 0 *)
\r
77 (* Continue with the case k' > 0 *)
\r
79 (UNDISCH_TAC `cell_params V X = k',ul'`);
\r
80 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
81 (REWRITE_TAC[cell_params]);
\r
82 (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);
\r
84 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);
\r
85 (ASM_REWRITE_TAC[]);
\r
86 (MATCH_MP_TAC SELECT_AX);
\r
87 (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);
\r
90 (REWRITE_TAC[BETA_THM]);
\r
91 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
\r
93 (REWRITE_TAC[BETA_THM]);
\r
94 (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
\r
95 (REWRITE_WITH `mcell k V ul = mcell4 V ul`);
\r
96 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);
\r
97 (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);
\r
98 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);
\r
99 (UP_ASM_TAC THEN EXPAND_TAC "P");
\r
100 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
\r
101 (REWRITE_TAC[ASSUME `X = mcell k' V ul'`]);
\r
102 (MATCH_MP_TAC LEPJBDJ);
\r
103 (ASM_REWRITE_TAC[]);
\r
104 (REPEAT STRIP_TAC);
\r
107 (NEW_GOAL `X:real^3->bool = {}`);
\r
109 (NEW_GOAL `NULLSET (X:real^3->bool)`);
\r
110 (ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
\r
111 (ASM_MESON_TAC[])]);;
\r