1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\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
10 flyspeck_needs "tame/CKQOWSA_4.hl";;
\r
11 flyspeck_needs "tame/tame_defs.hl";;
\r
12 flyspeck_needs "packing/pack2.hl";;
\r
15 module Ckqowsa = struct
\r
19 open Ckqowsa_3_points;;
\r
20 open Ckqowsa_4_points;;
\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
27 (* UNIONS (ESTD V) SUBSET V /\ graph (ESTD V) *)
\r
29 let ESTD_fan0 = prove(`!V. UNIONS (ESTD V) SUBSET V /\ graph (ESTD V)`,
\r
30 REPEAT STRIP_TAC THENL
\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
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
45 (* fan1 (V,ESTD V) <=> FINITE V /\ ~(V = {}) *)
\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
53 REWRITE_TAC[EXTENSION; IN_INTER; ball; IN_ELIM_THM] 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
62 ASM_SIMP_TAC[Pack2.KIUMVTC]);;
\r
66 (* fan2 (V,ESTD V) <=> ~(vec 0 IN V) *)
\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
73 FIRST_X_ASSUM (MP_TAC o SPEC `vec 0:real^3`) THEN
\r
74 ASM_REWRITE_TAC[in_ball_annulus]);;
\r
77 (* fan6 (V,ESTD V) <=> ~collinear {vec 0, e} *)
\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
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
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
101 ASM_REWRITE_TAC[INTER_ACI];
\r
105 SUBGOAL_THEN `{v} INTER {w:real^3} = {}` (fun th -> REWRITE_TAC[th]) THENL
\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
111 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
\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
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
131 SUBGOAL_THEN `&2 + &2 <= norm (v:real^3) + dist (v,w)` MP_TAC THENL
\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
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
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
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
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
173 REPEAT STRIP_TAC THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL]);;
\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
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
190 ASM_CASES_TAC `u:real^3 IN e` THENL
\r
192 SUBGOAL_THEN `{u:real^3} INTER e = {u}` (fun th -> REWRITE_TAC[th]) THENL
\r
194 REWRITE_TAC[EXTENSION; IN_INTER; IN_SING] THEN
\r
199 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
200 POP_ASSUM (fun th -> REWRITE_TAC[th])
\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
211 MAP_EVERY EXISTS_TAC [`t:real`; `&0`];
\r
212 MAP_EVERY EXISTS_TAC [`&0`; `t:real`]
\r
214 ASM_REWRITE_TAC[REAL_LE_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_ADD_RID];
\r
218 SUBGOAL_THEN `{u:real^3} INTER e = {}` (fun th -> REWRITE_TAC[th]) THENL
\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
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
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
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
237 ASM_REWRITE_TAC[IN_INTER; points_in_aff_ge_0_2; ENDS_IN_HALFLINE];
\r
240 ASM_REWRITE_TAC[] THEN
\r
242 EXISTS_TAC `x:real^3` THEN
\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
256 SUBGOAL_THEN `u:real^3 IN aff_ge {vec 0} {v,w}` ASSUME_TAC THENL
\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
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
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
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
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
305 REWRITE_TAC[EXTENSION; IN_INTER; IN_SING; IN_INSERT; NOT_IN_EMPTY] 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
313 SUBGOAL_THEN `~(v2 = vec 0:real^3) /\ ~(v3 = vec 0:real^3) /\ ~(v4 = vec 0:real^3)` ASSUME_TAC THENL
\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
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
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
330 ASM_CASES_TAC `t1 <= t1'` THENL
\r
332 ASM_CASES_TAC `t2 = &0` THENL
\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
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
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
351 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= t1' - t1 <=> t1 <= t1'`];
\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
366 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
\r
367 ASM_CASES_TAC `t2' = &0` THENL
\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
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
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
386 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_ARITH `t1' < t1 ==> &0 <= t1 - t1'`];
\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
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
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
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
420 ASM_CASES_TAC `v = w':A` THEN ASM_REWRITE_TAC[] THENL
\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
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
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
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
451 MATCH_MP_TAC fan7_4_1_one_case THEN
\r
452 EXISTS_TAC `V:real^3->bool` THEN
\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
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
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
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
482 MP_TAC (SPEC_ALL ESTD_fan0) THEN REWRITE_TAC[graph] THEN
\r
484 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[GSYM IN];
\r
487 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
\r
488 REWRITE_TAC[HAS_SIZE] THEN REPEAT DISCH_TAC THEN
\r
490 SUBGOAL_THEN `e1:real^3->bool = e2` MP_TAC THENL
\r
492 MATCH_MP_TAC EQ_TRANS THEN
\r
493 EXISTS_TAC `e1 INTER e2:real^3->bool` THEN
\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
505 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
506 REWRITE_TAC[INTER_ACI]);;
\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
515 SUBGOAL_THEN `?n. n <= 2 /\ (e1:real^3->bool) INTER e2 HAS_SIZE n` MP_TAC THENL
\r
517 SUBGOAL_THEN `e1:real^3->bool HAS_SIZE 2` MP_TAC THENL
\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
527 REWRITE_TAC[HAS_SIZE] THEN
\r
529 EXISTS_TAC `CARD (e1 INTER e2:real^3->bool)` THEN
\r
531 SUBGOAL_THEN `FINITE (e1 INTER e2:real^3->bool)` ASSUME_TAC THENL
\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
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
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
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
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
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
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
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