1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Zithlqn = struct
20 open Wrgcvdr_cizmrrh;;
22 open Flyspeck_constants;;
32 let s_init_J_empty= prove_by_refinement(
33 `!s. MEM s s_init_list_v39 ==> scs_J_v39 s = (\i j. F)`,
36 REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;LET_DEF;LET_END_DEF;set_of_list; FORALL_IN_CLAUSES;
37 scs_J_v39_explicit;mk_unadorned_v39]
41 let dsv_scs_init= prove_by_refinement(
42 ` MEM s s_init_list_v39 ==> dsv_v39 s vv = scs_d_v39 s`,
45 SIMP_TAC[s_init_J_empty;dsv_J_empty]
50 let exists_point_in_V= prove_by_refinement(
51 ` convex_local_fan (V,E,FF) /\
53 V SUBSET ball_annulus /\
54 3 <= CARD V /\ CARD V <= 6
58 ONCE_REWRITE_TAC[SET_RULE`(?v. v IN V)<=> ~(V={})`]
60 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;CARD_CLAUSES])
70 let exists_vv_FF= prove_by_refinement(
71 ` convex_local_fan (V,E,FF) /\
73 V SUBSET ball_annulus /\
74 3 <= CARD V /\ CARD V <= 6
78 /\ (!i. vv i= vv (i MOD (CARD V)))
79 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
80 /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
81 /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,
85 THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
86 THEN REWRITE_TAC[IMAGE;]
93 REWRITE_TAC[ARITH_RULE`1= SUC 0`; ITER]
94 THEN MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE
95 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;];
97 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
99 MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`(V:real^3->bool)`]
100 THEN REMOVE_ASSUM_TAC
101 THEN POP_ASSUM MP_TAC
102 THEN REMOVE_ASSUM_TAC
103 THEN REMOVE_ASSUM_TAC
104 THEN REMOVE_ASSUM_TAC
105 THEN REMOVE_ASSUM_TAC
107 THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;
110 THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
111 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
113 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
114 THEN REMOVE_ASSUM_TAC
115 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
116 THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
117 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
118 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
120 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
121 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
122 THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];
131 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
134 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
135 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
136 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
137 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
138 THEN POP_ASSUM MATCH_MP_TAC
139 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
141 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
142 THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];
145 THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;
147 REWRITE_TAC[EXTENSION]
151 REWRITE_TAC[IN_ELIM_THM]
152 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
153 THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
155 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
156 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
157 THEN REWRITE_TAC[IN_ELIM_THM]
159 THEN EXISTS_TAC`n:num`
160 THEN ASM_REWRITE_TAC[]
163 REWRITE_TAC[IN_ELIM_THM]
165 THEN ASM_REWRITE_TAC[]
166 THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
167 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
169 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);
174 ONCE_REWRITE_TAC[EXTENSION]
179 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
180 THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
181 THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
182 THEN POP_ASSUM MP_TAC
183 THEN REMOVE_ASSUM_TAC
184 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
186 THEN REWRITE_TAC[IN_ELIM_THM]
187 THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
188 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
189 THEN REMOVE_ASSUM_TAC
190 THEN POP_ASSUM MP_TAC
191 THEN REWRITE_TAC[IN_ELIM_THM]
193 THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;
196 THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];
199 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
200 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
201 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
202 THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
206 THEN ASM_REWRITE_TAC[ITER];
208 MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
211 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
212 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
213 THEN ASM_REWRITE_TAC[]
215 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
216 THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
217 THEN ASM_REWRITE_TAC[]
218 THEN MP_TAC Tecoxbm.RHO_IVS_IDD
219 THEN ASM_REWRITE_TAC[]
221 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
224 SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);
227 THEN POP_ASSUM MP_TAC
231 THEN ASM_REWRITE_TAC[ITER]
232 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
233 THEN ASM_REWRITE_TAC[]
235 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
236 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
237 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
238 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
241 REWRITE_TAC[IN_ELIM_THM]
243 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
244 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
245 THEN ASM_REWRITE_TAC[]
247 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
248 THEN REWRITE_TAC[ITER]
249 THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;
251 ONCE_REWRITE_TAC[EXTENSION]
256 THEN REWRITE_TAC[IN_ELIM_THM]
257 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
258 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
259 THEN ASM_REWRITE_TAC[]
261 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
262 THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
263 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
264 THEN REMOVE_ASSUM_TAC
265 THEN POP_ASSUM MP_TAC
266 THEN REWRITE_TAC[IN_ELIM_THM]
268 THEN ASM_REWRITE_TAC[ITER]
269 THEN EXISTS_TAC`x':num`
270 THEN ASM_REWRITE_TAC[];
272 REWRITE_TAC[IN_ELIM_THM]
274 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
275 THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
276 THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
278 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
288 let exists_vv= prove_by_refinement(
289 ` convex_local_fan (V,E,FF) /\
291 V SUBSET ball_annulus /\
292 3 <= CARD V /\ CARD V <= 6
293 ==> ?vv. (!i. vv i= vv (i MOD (CARD V)))
294 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
295 /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
296 /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,
300 THEN MP_TAC exists_point_in_V
301 THEN ASM_REWRITE_TAC[]
303 THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
304 THEN REWRITE_TAC[IMAGE;]
305 THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;
308 THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
309 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
311 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
312 THEN REMOVE_ASSUM_TAC
313 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
314 THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
315 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
316 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
318 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
319 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
320 THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];
329 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
332 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
333 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
334 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
335 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
336 THEN POP_ASSUM MATCH_MP_TAC
337 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
339 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
340 THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];
343 THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;
345 REWRITE_TAC[EXTENSION]
349 REWRITE_TAC[IN_ELIM_THM]
350 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
351 THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
353 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
354 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
355 THEN REWRITE_TAC[IN_ELIM_THM]
357 THEN EXISTS_TAC`n:num`
358 THEN ASM_REWRITE_TAC[]
361 REWRITE_TAC[IN_ELIM_THM]
363 THEN ASM_REWRITE_TAC[]
364 THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
365 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
367 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);
372 ONCE_REWRITE_TAC[EXTENSION]
377 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
378 THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
379 THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
380 THEN POP_ASSUM MP_TAC
381 THEN REMOVE_ASSUM_TAC
382 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
384 THEN REWRITE_TAC[IN_ELIM_THM]
385 THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
386 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
387 THEN REMOVE_ASSUM_TAC
388 THEN POP_ASSUM MP_TAC
389 THEN REWRITE_TAC[IN_ELIM_THM]
391 THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;
394 THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];
397 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
398 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
399 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
400 THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
404 THEN ASM_REWRITE_TAC[ITER];
406 MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
409 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
410 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
411 THEN ASM_REWRITE_TAC[]
413 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
414 THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
415 THEN ASM_REWRITE_TAC[]
416 THEN MP_TAC Tecoxbm.RHO_IVS_IDD
417 THEN ASM_REWRITE_TAC[]
419 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
422 SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);
425 THEN POP_ASSUM MP_TAC
429 THEN ASM_REWRITE_TAC[ITER]
430 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
431 THEN ASM_REWRITE_TAC[]
433 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
434 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
435 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
436 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
439 REWRITE_TAC[IN_ELIM_THM]
441 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
442 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
443 THEN ASM_REWRITE_TAC[]
445 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
446 THEN REWRITE_TAC[ITER]
447 THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;
449 ONCE_REWRITE_TAC[EXTENSION]
454 THEN REWRITE_TAC[IN_ELIM_THM]
455 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
456 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
457 THEN ASM_REWRITE_TAC[]
459 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
460 THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
461 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
462 THEN REMOVE_ASSUM_TAC
463 THEN POP_ASSUM MP_TAC
464 THEN REWRITE_TAC[IN_ELIM_THM]
466 THEN ASM_REWRITE_TAC[ITER]
467 THEN EXISTS_TAC`x':num`
468 THEN ASM_REWRITE_TAC[];
470 REWRITE_TAC[IN_ELIM_THM]
472 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
473 THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
474 THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
476 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
483 let SUC_MOD_NOT_EQ=prove_by_refinement(
484 `~(i MOD 3 = SUC i MOD 3)`,
489 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
490 THEN POP_ASSUM MP_TAC
491 THEN POP_ASSUM MP_TAC
492 THEN DISCH_THEN(LABEL_TAC"YEU")
493 THEN DISCH_THEN(LABEL_TAC"EM")
494 THEN MRESAL_TAC DIV_MONO[`i:num`;`i+1`;`3`][ARITH_RULE`~(3=0)/\ i<= i+1`]
495 THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
496 THEN POP_ASSUM MP_TAC
497 THEN MP_TAC(ARITH_RULE`i DIV 3 <= (i + 1) DIV 3 ==> (i + 1) DIV 3 = i DIV 3 \/ i DIV 3 < (i + 1) DIV 3`)
501 THEN REMOVE_ASSUM_TAC
502 THEN REMOVE_ASSUM_TAC
503 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
507 THEN POP_ASSUM MP_TAC
508 THEN REMOVE_THEN "YEU"(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
509 THEN REWRITE_TAC[ARITH_RULE`(i DIV 3 * 3 + (i + 1) MOD 3) + 1 = (i + 1) DIV 3 * 3 + (i + 1) MOD 3
510 <=> 1 = ((i + 1) DIV 3 - i DIV 3) * 3`]
511 THEN MP_TAC(ARITH_RULE`i DIV 3 < (i + 1) DIV 3 ==> 1<= ( (i + 1) DIV 3 -i DIV 3 )`)
512 THEN ASM_REWRITE_TAC[]
514 THEN MP_TAC(ARITH_RULE` 1<= ( (i + 1) DIV 3 -i DIV 3 )==> 3<= ( (i + 1) DIV 3 -i DIV 3 ) *3`)
515 THEN ASM_REWRITE_TAC[]
523 let SUC_MOD_EQ1=prove_by_refinement(
524 `(SUC i MOD 3 = SUC j MOD 3)
527 (i MOD 3 = j MOD 3) `,
532 THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
533 THEN REMOVE_ASSUM_TAC
534 THEN POP_ASSUM MP_TAC
535 THEN REWRITE_TAC[ARITH_RULE`i + 1 = (i + 1) DIV 3 * 3 + (j + 1) MOD 3
536 <=> (j + 1) MOD 3= (i + 1) - ((i + 1) DIV 3 * 3) `]
538 THEN MRESAL_TAC DIVISION[`j+1:num`;`3`][ARITH_RULE`~(3=0)`]
539 THEN REMOVE_ASSUM_TAC
540 THEN POP_ASSUM MP_TAC
541 THEN REWRITE_TAC[ARITH_RULE`j + 1 = (j + 1) DIV 3 * 3 + (i + 1) - (i + 1) DIV 3 * 3 <=> j+ (i + 1) DIV 3 * 3 = (j + 1) DIV 3 * 3 +i `]
543 THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
545 THEN MRESAL_TAC DIV_MONO[`i+1`;`j+1`;`3`][ARITH_RULE`~(3=0)`]
546 THEN MP_TAC(ARITH_RULE`j + (i + 1) DIV 3 * 3 = (j + 1) DIV 3 * 3 + i
547 /\ i<= j /\ (i + 1) DIV 3 <= (j + 1) DIV 3
548 ==> j -i = 3*((j + 1) DIV 3 - (i + 1) DIV 3) `)
549 THEN ASM_REWRITE_TAC[]
550 THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`3`][ARITH_RULE`~(3=0)`]
551 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
552 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
553 THEN MP_TAC(ARITH_RULE`j = j DIV 3 * 3 + j MOD 3
554 /\ i = i DIV 3 * 3 + i MOD 3 /\ i<= j/\ i DIV 3<= j DIV 3
555 ==> j-i = ((j DIV 3 - i DIV 3) * 3 + j MOD 3) -i MOD 3 `)
556 THEN ASM_REWRITE_TAC[]
557 THEN REMOVE_ASSUM_TAC
558 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
559 THEN ASM_REWRITE_TAC[]
560 THEN REMOVE_ASSUM_TAC
561 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
562 THEN ASM_REWRITE_TAC[]
565 THEN MRESAL_TAC MOD_MULT[`3`;`(j + 1) DIV 3 - (i + 1) DIV 3`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
566 THEN POP_ASSUM MP_TAC
567 THEN ONCE_REWRITE_TAC[ARITH_RULE`a*b=b*a`]
568 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
569 THEN MP_TAC(ARITH_RULE`i MOD 3 <=j MOD 3 \/ j MOD 3 < i MOD 3:num`)
575 ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
576 = (j DIV 3 - i DIV 3) * 3 + j MOD 3 - i MOD 3
579 THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3)`;`3`;`j MOD 3 - i MOD 3`]
580 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
581 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
582 THEN MP_TAC(ARITH_RULE`j MOD 3 < 3 /\ i MOD 3 <=j MOD 3
583 ==> j MOD 3 - i MOD 3 < 3 `)
584 THEN ASM_REWRITE_TAC[]
586 THEN MRESA_TAC MOD_LT[`j MOD 3 - i MOD 3`;`3`]
590 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
591 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
592 THEN MP_TAC(ARITH_RULE`i MOD 3 < 3/\ j MOD 3< i MOD 3
593 ==> (3+ j MOD 3) - i MOD 3 < 3 /\ 0< (3+ j MOD 3) - i MOD 3`)
594 THEN ASM_REWRITE_TAC[]
595 THEN MP_TAC(ARITH_RULE`j DIV 3 - i DIV 3 =0 \/ 1<= j DIV 3 - i DIV 3:num`)
598 POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * 3 + j MOD 3) - i MOD 3= j MOD 3 - i MOD 3`])
599 THEN REPEAT STRIP_TAC
600 THEN MP_TAC(ARITH_RULE`j MOD 3 < i MOD 3
601 /\ j - i = j MOD 3 - i MOD 3 /\ i<= j ==> j=i `)
602 THEN ASM_REWRITE_TAC[]
606 THEN MP_TAC(ARITH_RULE`1 <= j DIV 3 - i DIV 3 /\ 0 < (3 + j MOD 3) - i MOD 3
607 ==> ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
608 =((j DIV 3 - i DIV 3)-1) * 3 +(3+ j MOD 3) - i MOD 3`)
610 THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3 -1)`;`3`;`(3+ j MOD 3) - i MOD 3`]
611 THEN MRESA_TAC MOD_LT[`(3+j MOD 3) - i MOD 3`;`3`]
612 THEN REMOVE_ASSUM_TAC
613 THEN REMOVE_ASSUM_TAC
614 THEN REMOVE_ASSUM_TAC
615 THEN POP_ASSUM MP_TAC
620 let SUC_MOD_EQ=prove_by_refinement(
621 `(SUC i MOD 3 = SUC j MOD 3)
623 (i MOD 3 = j MOD 3) `,
627 THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
630 MATCH_MP_TAC SUC_MOD_EQ1
631 THEN ASM_REWRITE_TAC[];
633 MRESA_TAC (GEN_ALL SUC_MOD_EQ1)[`j:num`;`i:num`]
634 THEN ASM_REWRITE_TAC[]
639 let NOT_IMP_SUC_MOD_EQ=prove_by_refinement(
640 `~(i MOD 3 = j MOD 3)
641 ==> ~(SUC i MOD 3 = SUC j MOD 3)`,
642 [SIMP_TAC[CONTRAPOS_THM;]
643 THEN REWRITE_TAC[SUC_MOD_EQ]]);;
647 let IMP_SUC_MOD_EQ1=prove_by_refinement(
648 ` ~(k=0) /\ (i MOD k = j MOD k)
650 ==> (SUC i MOD k = SUC j MOD k)`,
655 THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`]
656 THEN REMOVE_ASSUM_TAC
657 THEN MP_TAC(ARITH_RULE`i:num = i DIV k * k + j MOD k
658 ==> j MOD k = i - (i DIV k * k) `)
659 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC th)
661 THEN MRESAL_TAC DIVISION[`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
662 THEN REMOVE_ASSUM_TAC
663 THEN POP_ASSUM MP_TAC
664 THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
666 THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
668 THEN MP_TAC(ARITH_RULE`j = (j DIV k) * k + i - (i DIV k) * k
669 /\ i +1 <= j+1 /\ i DIV k <= j DIV k /\ ~(k=0)
670 ==> j -i = (j DIV k) *k - (i DIV k) *k `)
671 THEN ASM_REWRITE_TAC[]
672 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
673 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
674 THEN ONCE_REWRITE_TAC[MULT_AC]
675 THEN MRESAL_TAC DIV_MONO[`i+1:num`;`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
676 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
677 THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
678 THEN MRESA_TAC LE_MULT_RCANCEL[`((i+1) DIV k)`;`((j+1) DIV k)`;`k:num`]
679 THEN MP_TAC(ARITH_RULE`i + 1 = (i + 1) DIV k * k + (i + 1) MOD k
680 /\ j + 1 = (j + 1) DIV k * k + (j + 1) MOD k /\ i<= j/\ ((i+1) DIV k)*k<= ((j+1) DIV k)*k
681 ==> j-i = (((j + 1) DIV k * k - (i + 1) DIV k * k) + (j + 1) MOD k) - (i + 1) MOD k`)
682 THEN ASM_REWRITE_TAC[]
683 THEN REMOVE_ASSUM_TAC
684 THEN REMOVE_ASSUM_TAC
685 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
686 THEN ASM_REWRITE_TAC[]
687 THEN REMOVE_ASSUM_TAC
688 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
689 THEN ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
692 THEN MRESAL_TAC MOD_MULT[`k:num`;`j DIV k - i DIV k`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
693 THEN POP_ASSUM MP_TAC
694 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
695 THEN MP_TAC(ARITH_RULE`(i+1) MOD k <=(j+1) MOD k \/ (j+1) MOD k < (i+1) MOD k:num`)
699 (i+1) MOD k <=(j+1) MOD k
701 ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)=
702 (((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k - (i + 1) MOD k)`)
704 THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`;`(j + 1) MOD k - (i + 1) MOD k`]
705 THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
706 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
707 THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < k /\ (i + 1) MOD k <=(j + 1) MOD k
708 ==> (j + 1) MOD k - (i + 1) MOD k < k `)
709 THEN ASM_REWRITE_TAC[]
711 THEN MRESA_TAC MOD_LT[`(j + 1) MOD k - (i + 1) MOD k`;` k:num`]
712 THEN REPLICATE_TAC 8 (REMOVE_ASSUM_TAC)
713 THEN POP_ASSUM MP_TAC
716 MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
717 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
718 THEN MP_TAC(ARITH_RULE`(i+1) MOD k < k/\ (j+1) MOD k< (i+1) MOD k
719 ==> (k+ (j+1) MOD k) - (i+1) MOD k < k /\ 0< (k+ (j+1) MOD k) - (i+1) MOD k`)
720 THEN ASM_REWRITE_TAC[]
721 THEN MP_TAC(ARITH_RULE`(j+1) DIV k - (i+1) DIV k =0 \/ 1<= (j+1) DIV k - (i+1) DIV k`)
724 POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * k + (j + 1) MOD k) - (i + 1) MOD k= (j + 1) MOD k - (i + 1) MOD k`])
725 THEN REPEAT STRIP_TAC
726 THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < (i + 1) MOD k
727 /\ j - i = (j + 1) MOD k - (i + 1) MOD k /\ i<= j ==> j=i `)
728 THEN ASM_REWRITE_TAC[]
732 THEN MRESAL_TAC LE_MULT_RCANCEL[`1`;`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`][ARITH_RULE`1*k=k`]
733 THEN MP_TAC(ARITH_RULE`k <= ((j + 1) DIV k - (i + 1) DIV k)*k /\ 0 < (k + (j + 1) MOD k) - (i + 1) MOD k
734 ==> ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)
736 ((((j + 1) DIV k - (i + 1) DIV k) * k- 1*k)+(k+ (j + 1) MOD k) - (i + 1) MOD k)
739 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
740 THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k - 1)`;`k:num`;`(k + (j + 1) MOD k) - (i + 1) MOD k`]
741 THEN MRESA_TAC MOD_LT[`(k + (j + 1) MOD k) - (i + 1) MOD k`;`k:num`]
742 THEN REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
743 THEN POP_ASSUM MP_TAC
749 let IMP_SUC_MOD_EQ=prove_by_refinement(
750 ` ~(k=0) /\ (i MOD k = j MOD k)
751 ==> (SUC i MOD k = SUC j MOD k)`,
755 THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
757 MATCH_MP_TAC IMP_SUC_MOD_EQ1
758 THEN ASM_REWRITE_TAC[];
759 MRESA_TAC (GEN_ALL IMP_SUC_MOD_EQ1)[`j:num`;`i:num`;`k:num`]
760 THEN ASM_REWRITE_TAC[]
766 let CHOOSE_MOD_3=prove_by_refinement(
767 `~(i MOD 3 = j MOD 3) /\ ~(SUC j MOD 3 = i MOD 3)
768 ==> j MOD 3 = SUC i MOD 3`,
771 MP_TAC(ARITH_RULE`i MOD 3= 0 \/ i MOD 3= 1 \/ i MOD 3= 2`)
772 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
773 THEN MP_TAC(ARITH_RULE`j MOD 3= 0 \/ j MOD 3= 1 \/ j MOD 3= 2`)
774 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
775 THEN MP_TAC(ARITH_RULE`SUC j MOD 3= 0 \/ SUC j MOD 3= 1 \/ SUC j MOD 3= 2`)
776 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
777 THEN REPEAT STRIP_TAC
778 THEN MP_TAC(SET_RULE`SUC j MOD 3 IN {0, 1, 2} /\
779 j MOD 3 IN {0, 1, 2} /\ i MOD 3 IN {0, 1, 2}
780 ==> {SUC j MOD 3, j MOD 3, i MOD 3 }SUBSET {0, 1, 2}`)
782 THEN SUBGOAL_THEN`CARD {SUC j MOD 3, j MOD 3, i MOD 3 }=3` ASSUME_TAC;
784 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
785 IN_INSERT; NOT_IN_EMPTY;]
786 THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`j:num`
789 SUBGOAL_THEN`CARD {0, 1, 2 }=3` ASSUME_TAC;
791 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
792 IN_INSERT; NOT_IN_EMPTY;]
795 SUBGOAL_THEN`FINITE {0, 1, 2 }` ASSUME_TAC;
797 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
798 IN_INSERT; NOT_IN_EMPTY;];
800 MRESA_TAC CARD_SUBSET_EQ[`{SUC j MOD 3, j MOD 3, i MOD 3 }`;`{0, 1, 2}`]
801 THEN MP_TAC(ARITH_RULE`SUC i MOD 3= 0 \/ SUC i MOD 3= 1 \/ SUC i MOD 3= 2`)
802 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
803 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
804 THEN ONCE_REWRITE_TAC[SET_RULE` A IN {B,C,D}<=> (A=B\/ A=C\/A=D)`]
805 THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`i:num`
806 THEN MRESA_TAC(GEN_ALL NOT_IMP_SUC_MOD_EQ)[`i:num`;`j:num`]
814 let SMALL_BALL_ANNULUS_6=prove_by_refinement(
815 ` convex_local_fan (V,E,FF) /\
817 V SUBSET ball_annulus /\
818 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))
819 ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) /\ dist(v,w)<= &6 )`,
823 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
824 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
825 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
826 THEN ASM_REWRITE_TAC[];
827 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
828 ==> v IN ball_annulus /\ w IN ball_annulus`)
829 THEN ASM_REWRITE_TAC[]
830 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
832 THEN REMOVE_ASSUM_TAC
833 THEN POP_ASSUM MP_TAC
834 THEN ONCE_REWRITE_TAC[DIST_SYM]
836 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
837 THEN POP_ASSUM MP_TAC
838 THEN POP_ASSUM MP_TAC
839 THEN REMOVE_ASSUM_TAC
840 THEN POP_ASSUM MP_TAC
850 let SMALL_BALL_ANNULUS_6_sqrt8=prove_by_refinement(
851 ` convex_local_fan (V,E,FF) /\
853 V SUBSET ball_annulus /\
854 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w))
855 ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) /\ dist(v,w)<= &6 )`,
859 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
860 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
861 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
862 THEN ASM_REWRITE_TAC[];
863 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
864 ==> v IN ball_annulus /\ w IN ball_annulus`)
865 THEN ASM_REWRITE_TAC[]
866 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
868 THEN REMOVE_ASSUM_TAC
869 THEN POP_ASSUM MP_TAC
870 THEN ONCE_REWRITE_TAC[DIST_SYM]
872 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
873 THEN POP_ASSUM MP_TAC
874 THEN POP_ASSUM MP_TAC
875 THEN REMOVE_ASSUM_TAC
876 THEN POP_ASSUM MP_TAC
884 let SMALL_BALL_ANNULUS_6_3=prove_by_refinement(
885 ` convex_local_fan (V,E,FF) /\
887 V SUBSET ball_annulus /\
888 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w))
889 ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) /\ dist(v,w)<= &6 )`,
893 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
894 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
895 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
896 THEN ASM_REWRITE_TAC[];
897 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
898 ==> v IN ball_annulus /\ w IN ball_annulus`)
899 THEN ASM_REWRITE_TAC[]
900 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
902 THEN REMOVE_ASSUM_TAC
903 THEN POP_ASSUM MP_TAC
904 THEN ONCE_REWRITE_TAC[DIST_SYM]
906 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
907 THEN POP_ASSUM MP_TAC
908 THEN POP_ASSUM MP_TAC
909 THEN REMOVE_ASSUM_TAC
910 THEN POP_ASSUM MP_TAC
918 let CS_ADJ=prove(`cs_adj = (\k a1 a2 i j. (if (i MOD k = j MOD k) then &0
919 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))`,
920 MP_TAC( GENL [`k:num`;`a1:real`;`a2:real`;`i:num`;`j:num`] (SPEC_ALL cs_adj))
921 THEN REWRITE_TAC[GSYM FUN_EQ_THM]
923 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
924 THEN SIMP_TAC[FUN_EQ_THM]);;
929 let ZITHLQN_CASE_3=prove_by_refinement(
930 ` V SUBSET ball_annulus /\
932 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
933 /\ (s=let upperbd = &6 in
934 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
935 else (if {i MOD k,j MOD k}={0,1} then p
936 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
937 mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))
938 /\ (!i. vv (i MOD (CARD V))= vv i)
939 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
940 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
941 ==> vv IN BBs_v39 s`,
945 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;Oxl_def.periodic;mk_unadorned_v39;CS_ADJ]
948 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
949 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
950 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
951 THEN ASM_REWRITE_TAC[]
952 THEN REPEAT STRIP_TAC
953 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
958 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
959 THEN MP_TAC(ARITH_RULE`i MOD 3 = j MOD 3 \/ ~(i MOD 3 = j MOD 3)`)
962 ASM_REWRITE_TAC[DIST_POS_LE]
963 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
964 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
965 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
967 THEN REWRITE_TAC[DIST_REFL]
971 THEN MP_TAC(ARITH_RULE`SUC j MOD 3 = i MOD 3 \/ ~(SUC j MOD 3 = i MOD 3)`)
975 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
978 THEN POP_ASSUM MP_TAC
979 THEN POP_ASSUM MP_TAC
980 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
981 THEN REPEAT STRIP_TAC
982 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
983 THEN EXISTS_TAC`j:num`
984 THEN ASM_REWRITE_TAC[]
985 THEN POP_ASSUM MP_TAC
986 THEN POP_ASSUM MP_TAC
987 THEN POP_ASSUM MP_TAC
988 THEN POP_ASSUM MP_TAC
989 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
990 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
991 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
993 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
996 THEN REPLICATE_TAC 7 REMOVE_ASSUM_TAC
997 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1000 THEN ASM_REWRITE_TAC[]
1004 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1006 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1007 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1008 THEN REPEAT STRIP_TAC
1009 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1010 THEN EXISTS_TAC`i:num`
1011 THEN ASM_REWRITE_TAC[]
1012 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1013 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1014 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1015 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1016 THEN REPEAT RESA_TAC;
1019 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1020 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1022 ASM_REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;]
1029 let ZITHLQN_CASE_4=prove_by_refinement(
1030 ` convex_local_fan (V,E,FF) /\
1032 V SUBSET ball_annulus /\
1034 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
1035 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1036 /\ (s=let upperbd = &6 in
1037 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1038 else (if {i MOD k,j MOD k}={0,1} then p
1039 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1040 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))
1041 /\ (!i. vv (i MOD (CARD V))= vv i)
1042 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1043 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1044 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1045 ==> vv IN BBs_v39 s`,
1049 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1050 THEN MP_TAC SMALL_BALL_ANNULUS_6
1051 THEN ASM_REWRITE_TAC[]
1052 THEN REMOVE_ASSUM_TAC
1053 THEN REPEAT STRIP_TAC
1054 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1057 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1058 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1059 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1060 THEN ASM_REWRITE_TAC[]
1061 THEN REPEAT STRIP_TAC
1062 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1065 THEN REPEAT GEN_TAC;
1067 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1068 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
1071 ASM_REWRITE_TAC[DIST_POS_LE]
1072 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1073 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1074 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1075 THEN REPEAT RESA_TAC
1076 THEN REWRITE_TAC[DIST_REFL]
1077 THEN REAL_ARITH_TAC;
1080 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
1084 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1086 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1087 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1088 THEN REPEAT STRIP_TAC
1089 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1090 THEN EXISTS_TAC`j:num`
1091 THEN ASM_REWRITE_TAC[]
1092 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1093 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1094 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1095 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1096 THEN REPEAT RESA_TAC
1097 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1100 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1101 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1104 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
1108 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1110 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1111 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1112 THEN REPEAT STRIP_TAC
1113 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1114 THEN EXISTS_TAC`i:num`
1115 THEN ASM_REWRITE_TAC[]
1116 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1117 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1118 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1119 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1120 THEN REPEAT RESA_TAC
1121 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1124 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1125 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1128 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1131 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1132 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1133 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1134 THEN POP_ASSUM MP_TAC
1135 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1136 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1137 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1138 THEN REWRITE_TAC[th])
1139 THEN REPEAT STRIP_TAC
1140 THEN POP_ASSUM MP_TAC
1141 THEN REWRITE_TAC[PAIR_EQ]
1143 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1145 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1146 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1147 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1149 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1150 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1151 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1154 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1157 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1158 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1161 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1162 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1163 THEN POP_ASSUM MATCH_MP_TAC
1164 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1165 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1180 let ZITHLQN_CASE_5=prove_by_refinement(
1181 ` convex_local_fan (V,E,FF) /\
1183 V SUBSET ball_annulus /\
1185 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
1186 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1187 /\ (s=let upperbd = &6 in
1188 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1189 else (if {i MOD k,j MOD k}={0,1} then p
1190 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1191 mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd))
1192 /\ (!i. vv (i MOD (CARD V))= vv i)
1193 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1194 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1195 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1196 ==> vv IN BBs_v39 s`,
1200 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1201 THEN MP_TAC SMALL_BALL_ANNULUS_6
1202 THEN ASM_REWRITE_TAC[]
1203 THEN REMOVE_ASSUM_TAC
1204 THEN REPEAT STRIP_TAC
1205 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1208 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1209 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1210 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1211 THEN ASM_REWRITE_TAC[]
1212 THEN REPEAT STRIP_TAC
1213 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1216 THEN REPEAT GEN_TAC;
1218 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1219 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1222 ASM_REWRITE_TAC[DIST_POS_LE]
1223 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1224 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1225 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1226 THEN REPEAT RESA_TAC
1227 THEN REWRITE_TAC[DIST_REFL]
1228 THEN REAL_ARITH_TAC;
1231 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1235 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1237 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1239 THEN REPEAT STRIP_TAC
1240 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1241 THEN EXISTS_TAC`j:num`
1242 THEN ASM_REWRITE_TAC[]
1243 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1244 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1245 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1246 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1247 THEN REPEAT RESA_TAC
1248 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1251 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1252 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1255 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1259 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1261 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1262 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1263 THEN REPEAT STRIP_TAC
1264 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1265 THEN EXISTS_TAC`i:num`
1266 THEN ASM_REWRITE_TAC[]
1267 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1268 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1269 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1270 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1271 THEN REPEAT RESA_TAC
1272 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1275 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1276 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1279 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1282 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1283 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1284 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1285 THEN POP_ASSUM MP_TAC
1286 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1288 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1289 THEN REWRITE_TAC[th])
1290 THEN REPEAT STRIP_TAC
1291 THEN POP_ASSUM MP_TAC
1292 THEN REWRITE_TAC[PAIR_EQ]
1294 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1296 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1297 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1298 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1300 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1301 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1302 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1304 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1306 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1307 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1309 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1310 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1311 THEN POP_ASSUM MATCH_MP_TAC
1312 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1313 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1329 let ZITHLQN_CASE_6=prove_by_refinement(
1330 ` convex_local_fan (V,E,FF) /\
1332 V SUBSET ball_annulus /\
1334 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
1335 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1336 /\ (s=let upperbd = &6 in
1337 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1338 else (if {i MOD k,j MOD k}={0,1} then p
1339 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1340 mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd))
1341 /\ (!i. vv (i MOD (CARD V))= vv i)
1342 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1343 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1344 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1345 ==> vv IN BBs_v39 s`,
1349 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1350 THEN MP_TAC SMALL_BALL_ANNULUS_6
1351 THEN ASM_REWRITE_TAC[]
1352 THEN REMOVE_ASSUM_TAC
1353 THEN REPEAT STRIP_TAC
1354 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1357 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1358 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1359 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1360 THEN ASM_REWRITE_TAC[]
1361 THEN REPEAT STRIP_TAC
1362 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1365 THEN REPEAT GEN_TAC;
1367 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1368 THEN MP_TAC(ARITH_RULE`i MOD 6 = j MOD 6 \/ ~(i MOD 6 = j MOD 6)`)
1371 ASM_REWRITE_TAC[DIST_POS_LE]
1372 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1373 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1374 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1375 THEN REPEAT RESA_TAC
1376 THEN REWRITE_TAC[DIST_REFL]
1377 THEN REAL_ARITH_TAC;
1380 THEN MP_TAC(ARITH_RULE`SUC j MOD 6 = i MOD 6 \/ ~(SUC j MOD 6 = i MOD 6)`)
1384 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1386 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1387 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1388 THEN REPEAT STRIP_TAC
1389 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1390 THEN EXISTS_TAC`j:num`
1391 THEN ASM_REWRITE_TAC[]
1392 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1393 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1394 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1395 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1396 THEN REPEAT RESA_TAC
1397 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1400 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1401 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1404 THEN MP_TAC(ARITH_RULE`SUC i MOD 6 = j MOD 6 \/ ~(SUC i MOD 6 = j MOD 6)`)
1408 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1410 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1411 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1412 THEN REPEAT STRIP_TAC
1413 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1414 THEN EXISTS_TAC`i:num`
1415 THEN ASM_REWRITE_TAC[]
1416 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1417 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1418 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1419 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1420 THEN REPEAT RESA_TAC
1421 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1424 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1425 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1428 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1431 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1432 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1433 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1434 THEN POP_ASSUM MP_TAC
1435 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1436 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1437 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1438 THEN REWRITE_TAC[th])
1439 THEN REPEAT STRIP_TAC
1440 THEN POP_ASSUM MP_TAC
1441 THEN REWRITE_TAC[PAIR_EQ]
1443 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1445 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1446 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1447 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];
1449 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1450 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1451 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];
1453 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1455 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1456 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1458 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1459 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1460 THEN POP_ASSUM MATCH_MP_TAC
1461 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1462 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1478 let ZITHLQN_CASE_5_pro_cs=prove_by_refinement(
1479 ` convex_local_fan (V,E,FF) /\
1481 V SUBSET ball_annulus /\
1483 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
1484 (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
1486 &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
1487 /\ (s=let upperbd = &6 in
1488 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1489 else (if {i MOD k ,j MOD k}={0,1} then p
1490 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1491 mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd))
1492 /\ (!i. vv (i MOD (CARD V))= vv i)
1493 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1494 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1495 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1496 /\ vv 0= v0 /\ vv 1= w0
1497 ==> vv IN BBs_v39 s`,
1501 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1502 THEN MP_TAC SMALL_BALL_ANNULUS_6
1503 THEN ASM_REWRITE_TAC[]
1504 THEN REMOVE_ASSUM_TAC
1505 THEN REPEAT STRIP_TAC
1506 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1509 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1510 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1511 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1512 THEN ASM_REWRITE_TAC[]
1513 THEN REPEAT STRIP_TAC
1514 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1517 THEN REPEAT GEN_TAC;
1519 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1520 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1523 ASM_REWRITE_TAC[DIST_POS_LE]
1524 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1525 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1526 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1527 THEN REPEAT RESA_TAC
1528 THEN REWRITE_TAC[DIST_REFL]
1529 THEN REAL_ARITH_TAC;
1532 THEN MP_TAC(SET_RULE`{i MOD 5,j MOD 5}={0,1} \/ ~({i MOD 5,j MOD 5}={0,1})`)
1536 THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;
1539 THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);
1541 MP_TAC(SET_RULE`{i MOD 5,j MOD 5} = {0, 1} /\ ~(i MOD 5=j MOD 5)/\ ~(0=1)==> (i MOD 5=0 /\ j MOD 5=1)\/ (i MOD 5=1 /\ j MOD 5=0)`)
1542 THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
1544 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
1545 THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
1546 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
1548 THEN ASM_REWRITE_TAC[]
1550 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1552 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1553 THEN ONCE_REWRITE_TAC[DIST_SYM]
1554 THEN ASM_REWRITE_TAC[];
1557 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1561 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1563 REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1564 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1565 THEN REPEAT STRIP_TAC
1566 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1567 THEN EXISTS_TAC`j:num`
1568 THEN ASM_REWRITE_TAC[]
1569 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
1570 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1571 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1572 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1573 THEN REPEAT RESA_TAC
1574 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1576 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
1578 REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1579 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
1580 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1581 THEN ASM_REWRITE_TAC[];
1583 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
1586 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
1588 THEN ASM_REWRITE_TAC[]
1591 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1592 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
1593 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1595 THEN ASM_REWRITE_TAC[]
1597 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1598 THEN REPEAT STRIP_TAC
1599 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1600 THEN REPEAT STRIP_TAC
1601 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
1602 THEN POP_ASSUM MP_TAC
1605 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1606 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
1607 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1609 THEN ASM_REWRITE_TAC[]
1611 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1612 THEN REPEAT STRIP_TAC
1613 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1614 THEN REPEAT STRIP_TAC
1615 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
1616 THEN POP_ASSUM MP_TAC
1617 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
1621 THEN REMOVE_ASSUM_TAC
1622 THEN POP_ASSUM MP_TAC
1623 THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
1624 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1627 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1631 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1633 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1634 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1635 THEN REPEAT STRIP_TAC
1636 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1637 THEN EXISTS_TAC`i:num`
1638 THEN ASM_REWRITE_TAC[]
1639 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1640 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1641 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1642 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1643 THEN REPEAT RESA_TAC
1644 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1646 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
1648 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
1649 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
1650 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1651 THEN ASM_REWRITE_TAC[];
1653 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
1656 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
1658 THEN ASM_REWRITE_TAC[]
1661 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1662 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
1663 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1665 THEN ASM_REWRITE_TAC[]
1667 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1668 THEN REPEAT STRIP_TAC
1669 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1670 THEN REPEAT STRIP_TAC
1671 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1672 THEN POP_ASSUM MP_TAC
1675 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1676 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
1677 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1679 THEN ASM_REWRITE_TAC[]
1681 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1682 THEN REPEAT STRIP_TAC
1683 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1684 THEN REPEAT STRIP_TAC
1685 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1686 THEN POP_ASSUM MP_TAC
1687 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
1691 THEN REMOVE_ASSUM_TAC
1692 THEN POP_ASSUM MP_TAC
1693 THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
1694 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1697 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1700 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1701 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1702 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1703 THEN POP_ASSUM MP_TAC
1704 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1705 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1706 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1707 THEN REWRITE_TAC[th])
1708 THEN REPEAT STRIP_TAC
1709 THEN POP_ASSUM MP_TAC
1710 THEN REWRITE_TAC[PAIR_EQ]
1712 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);
1714 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1715 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1716 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1718 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1719 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1720 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1722 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1724 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
1725 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1727 REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
1728 THEN POP_ASSUM (fun th -> REPLICATE_TAC 18 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1729 THEN POP_ASSUM MATCH_MP_TAC
1730 THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
1731 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1750 let ZITHLQN_CASE_4_3=prove_by_refinement(
1751 ` convex_local_fan (V,E,FF) /\
1753 V SUBSET ball_annulus /\
1755 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) ) /\
1756 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1757 /\ (s=let upperbd = &6 in
1758 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1759 else (if {i MOD k,j MOD k}={0,1} then p
1760 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1761 mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))
1762 /\ (!i. vv (i MOD (CARD V))= vv i)
1763 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1764 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1765 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1766 ==> vv IN BBs_v39 s`,
1770 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1771 THEN MP_TAC SMALL_BALL_ANNULUS_6_3
1772 THEN ASM_REWRITE_TAC[]
1773 THEN REMOVE_ASSUM_TAC
1774 THEN REPEAT STRIP_TAC
1775 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1778 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1779 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1780 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1781 THEN ASM_REWRITE_TAC[]
1782 THEN REPEAT STRIP_TAC
1783 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1786 THEN REPEAT GEN_TAC;
1788 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1789 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
1792 ASM_REWRITE_TAC[DIST_POS_LE]
1793 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1794 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1795 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1796 THEN REPEAT RESA_TAC
1797 THEN REWRITE_TAC[DIST_REFL]
1798 THEN REAL_ARITH_TAC;
1801 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
1805 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1807 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1808 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1809 THEN REPEAT STRIP_TAC
1810 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1811 THEN EXISTS_TAC`j:num`
1812 THEN ASM_REWRITE_TAC[]
1813 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1814 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1815 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1816 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1817 THEN REPEAT RESA_TAC
1818 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1821 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1822 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1825 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
1829 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1831 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1832 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1833 THEN REPEAT STRIP_TAC
1834 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1835 THEN EXISTS_TAC`i:num`
1836 THEN ASM_REWRITE_TAC[]
1837 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1838 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1839 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1840 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1841 THEN REPEAT RESA_TAC
1842 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1845 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1846 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1849 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1852 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1853 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1854 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1855 THEN POP_ASSUM MP_TAC
1856 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1857 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1858 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1859 THEN REWRITE_TAC[th])
1860 THEN REPEAT STRIP_TAC
1861 THEN POP_ASSUM MP_TAC
1862 THEN REWRITE_TAC[PAIR_EQ]
1864 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1866 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1867 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1868 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1870 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1871 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1872 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1874 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1876 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1877 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1879 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1880 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1881 THEN POP_ASSUM MATCH_MP_TAC
1882 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1883 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1901 let ZITHLQN_CASE_5_sqrt8=prove_by_refinement(
1902 ` convex_local_fan (V,E,FF) /\
1904 V SUBSET ball_annulus /\
1906 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) ) /\
1907 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1908 /\ (s=let upperbd = &6 in
1909 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1910 else (if {i MOD k,j MOD k}={0,1} then p
1911 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1912 mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd))
1913 /\ (!i. vv (i MOD (CARD V))= vv i)
1914 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1915 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1916 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1917 ==> vv IN BBs_v39 s`,
1921 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1922 THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8
1923 THEN ASM_REWRITE_TAC[]
1924 THEN REMOVE_ASSUM_TAC
1925 THEN REPEAT STRIP_TAC
1926 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1929 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1930 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1931 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1932 THEN ASM_REWRITE_TAC[]
1933 THEN REPEAT STRIP_TAC
1934 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1937 THEN REPEAT GEN_TAC;
1939 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1940 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1943 ASM_REWRITE_TAC[DIST_POS_LE]
1944 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1945 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1946 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1947 THEN REPEAT RESA_TAC
1948 THEN REWRITE_TAC[DIST_REFL]
1949 THEN REAL_ARITH_TAC;
1952 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1956 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1958 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1959 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1960 THEN REPEAT STRIP_TAC
1961 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1962 THEN EXISTS_TAC`j:num`
1963 THEN ASM_REWRITE_TAC[]
1964 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1965 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1966 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1967 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1968 THEN REPEAT RESA_TAC
1969 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1972 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1973 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1976 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1980 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1982 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1983 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1984 THEN REPEAT STRIP_TAC
1985 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1986 THEN EXISTS_TAC`i:num`
1987 THEN ASM_REWRITE_TAC[]
1988 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1989 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1990 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1991 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1992 THEN REPEAT RESA_TAC
1993 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1996 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1997 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
2000 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
2003 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2004 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2005 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
2006 THEN POP_ASSUM MP_TAC
2007 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2008 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
2009 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2010 THEN REWRITE_TAC[th])
2011 THEN REPEAT STRIP_TAC
2012 THEN POP_ASSUM MP_TAC
2013 THEN REWRITE_TAC[PAIR_EQ]
2015 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
2017 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
2018 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2019 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
2021 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
2022 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2023 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
2025 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
2027 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2028 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
2030 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2031 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
2032 THEN POP_ASSUM MATCH_MP_TAC
2033 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2034 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
2057 let ZITHLQN_CASE_4_pro_cs=prove_by_refinement(
2058 ` convex_local_fan (V,E,FF) /\
2060 V SUBSET ball_annulus /\
2062 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
2063 (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
2065 &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
2066 /\ (s=let upperbd = &6 in
2067 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2068 else (if {i MOD k ,j MOD k}={0,1} then p
2069 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2070 mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd))
2071 /\ (!i. vv (i MOD (CARD V))= vv i)
2072 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
2073 /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
2074 /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
2075 /\ vv 0= v0 /\ vv 1= w0
2076 ==> vv IN BBs_v39 s`,
2080 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2081 THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8
2082 THEN ASM_REWRITE_TAC[]
2083 THEN REMOVE_ASSUM_TAC
2084 THEN REPEAT STRIP_TAC
2085 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
2088 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
2089 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2090 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
2091 THEN ASM_REWRITE_TAC[]
2092 THEN REPEAT STRIP_TAC
2093 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
2096 THEN REPEAT GEN_TAC;
2098 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
2099 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
2102 ASM_REWRITE_TAC[DIST_POS_LE]
2103 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2104 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
2105 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
2106 THEN REPEAT RESA_TAC
2107 THEN REWRITE_TAC[DIST_REFL]
2108 THEN REAL_ARITH_TAC;
2111 THEN MP_TAC(SET_RULE`{i MOD 4,j MOD 4}={0,1} \/ ~({i MOD 4,j MOD 4}={0,1})`)
2115 THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;
2118 THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);
2120 MP_TAC(SET_RULE`{i MOD 4,j MOD 4} = {0, 1} /\ ~(i MOD 4=j MOD 4)/\ ~(0=1)==> (i MOD 4=0 /\ j MOD 4=1)\/ (i MOD 4=1 /\ j MOD 4=0)`)
2121 THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
2123 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
2124 THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
2125 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
2127 THEN ASM_REWRITE_TAC[]
2129 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2131 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
2132 THEN ONCE_REWRITE_TAC[DIST_SYM]
2133 THEN ASM_REWRITE_TAC[];
2136 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
2140 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
2142 REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2143 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2144 THEN REPEAT STRIP_TAC
2145 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2146 THEN EXISTS_TAC`j:num`
2147 THEN ASM_REWRITE_TAC[]
2148 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
2149 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
2150 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
2151 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
2152 THEN REPEAT RESA_TAC
2153 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
2155 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
2157 REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2158 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
2159 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2160 THEN ASM_REWRITE_TAC[];
2162 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
2165 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
2167 THEN ASM_REWRITE_TAC[]
2170 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2171 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
2172 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2174 THEN ASM_REWRITE_TAC[]
2176 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2177 THEN REPEAT STRIP_TAC
2178 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2179 THEN REPEAT STRIP_TAC
2180 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
2181 THEN POP_ASSUM MP_TAC
2184 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2185 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
2186 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2188 THEN ASM_REWRITE_TAC[]
2190 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2191 THEN REPEAT STRIP_TAC
2192 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2193 THEN REPEAT STRIP_TAC
2194 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
2195 THEN POP_ASSUM MP_TAC
2196 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
2200 THEN REMOVE_ASSUM_TAC
2201 THEN POP_ASSUM MP_TAC
2202 THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
2203 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
2206 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
2210 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
2212 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2213 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2214 THEN REPEAT STRIP_TAC
2215 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2216 THEN EXISTS_TAC`i:num`
2217 THEN ASM_REWRITE_TAC[]
2218 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2219 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
2220 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
2221 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
2222 THEN REPEAT RESA_TAC
2223 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
2225 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
2227 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
2228 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
2229 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2230 THEN ASM_REWRITE_TAC[];
2232 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
2235 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
2237 THEN ASM_REWRITE_TAC[]
2240 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2241 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
2242 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2244 THEN ASM_REWRITE_TAC[]
2246 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2247 THEN REPEAT STRIP_TAC
2248 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2249 THEN REPEAT STRIP_TAC
2250 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2251 THEN POP_ASSUM MP_TAC
2254 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2255 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
2256 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2258 THEN ASM_REWRITE_TAC[]
2260 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2261 THEN REPEAT STRIP_TAC
2262 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2263 THEN REPEAT STRIP_TAC
2264 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2265 THEN POP_ASSUM MP_TAC
2266 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
2270 THEN REMOVE_ASSUM_TAC
2271 THEN POP_ASSUM MP_TAC
2272 THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
2273 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
2276 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
2279 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2280 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2281 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
2282 THEN POP_ASSUM MP_TAC
2283 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2284 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
2285 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2286 THEN REWRITE_TAC[th])
2287 THEN REPEAT STRIP_TAC
2288 THEN POP_ASSUM MP_TAC
2289 THEN REWRITE_TAC[PAIR_EQ]
2291 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);
2293 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
2294 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2295 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
2297 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
2298 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2299 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
2301 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
2303 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
2304 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
2306 REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
2307 THEN POP_ASSUM (fun th -> REPLICATE_TAC 18 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
2308 THEN POP_ASSUM MATCH_MP_TAC
2309 THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
2310 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
2325 let exists_vv3=prove_by_refinement(
2329 norm v1 <= &2 * h0 /\
2330 norm v2 <= &2 * h0 /\
2331 norm v3 <= &2 * h0 /\
2332 &2 <= dist(v1,v2) /\
2333 &2 <= dist(v1,v3) /\
2334 &2 <= dist(v2,v3) /\
2335 dist(v1,v2) <= &2 * h0 /\
2336 dist(v1,v3) <= &2 * h0 /\
2337 dist(v2,v3) <= &2 * h0
2339 if i MOD 3 = 0 then v1 else
2340 if i MOD 3 = 1 then v2 else v3)
2341 /\ V= IMAGE vv (:num) /\ E= IMAGE (\i. {vv i, vv (SUC i)}) (:num)
2342 /\ FF= IMAGE (\i. vv i,vv (SUC i)) (:num)
2344 (!i. vv (i MOD (CARD V))= vv i)
2345 /\ V SUBSET ball_annulus /\
2347 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)`,
2351 THEN SUBGOAL_THEN`(!i. (vv:num->real^3) (i MOD 3)= vv i)`ASSUME_TAC;
2353 ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
2355 SUBGOAL_THEN`(V:real^3->bool)={v1,v2,v3}`ASSUME_TAC;
2357 ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
2362 THEN ASM_REWRITE_TAC[]
2363 THEN MP_TAC(ARITH_RULE`x' MOD 3= 0 \/ x' MOD 3= 1\/ x' MOD 3=2`)
2365 THEN ASM_REWRITE_TAC[]
2369 THEN MP_TAC(SET_RULE`x IN {v1, v2, v3:real^3} ==> x = v1 \/ x= v2 \/ x= v3`)
2373 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 3 = 0`]
2377 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3 = 1/\ ~(1 MOD 3 = 0)`]
2381 THEN ASM_REWRITE_TAC[ARITH_RULE`~(2 MOD 3 = 1) /\ ~(2 MOD 3 = 0)`]
2384 SUBGOAL_THEN(`~(v1=v2:real^3) /\ ~(v1=v3:real^3) /\ ~(v3=v2:real^3)`)ASSUME_TAC;
2389 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
2390 THEN REAL_ARITH_TAC;
2394 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
2395 THEN REAL_ARITH_TAC;
2397 SUBGOAL_THEN`CARD (V:real^3->bool)=3` ASSUME_TAC;
2400 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2401 THEN ASM_REWRITE_TAC[]
2403 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
2404 IN_INSERT; NOT_IN_EMPTY;]
2405 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2406 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2407 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2410 POP_ASSUM(fun th-> REWRITE_TAC[th])
2411 THEN POP_ASSUM(fun th->
2412 POP_ASSUM(fun th-> REWRITE_TAC[th])
2413 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
2415 THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
2418 MATCH_MP_TAC(SET_RULE`(v1 IN ball_annulus
2419 /\ v2 IN ball_annulus /\ v3 IN ball_annulus)==> {v1, v2, v3} SUBSET ball_annulus `)
2421 THEN ASM_REWRITE_TAC[ball_annulus;DIFF;cball;ball;IN_ELIM_THM; REAL_ARITH`~(a< &2)<=> &2<=a`;DIST_0];
2423 REWRITE_TAC[IMAGE;IN_ELIM_THM]
2426 THEN POP_ASSUM MP_TAC
2427 THEN MP_TAC(ARITH_RULE`x MOD 3= 0 \/ x MOD 3= 1\/ x MOD 3=2`)
2429 THEN ASM_REWRITE_TAC[];
2431 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`0`;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0 MOD 3=1/\ ~(1=0)`]
2433 THEN MP_TAC(SET_RULE`{v, w} = {v1, v2} /\ ~(v1=v2) ==>(v=v1 /\ w=v2)\/ (v=v2 /\
2435 THEN ASM_REWRITE_TAC[]
2437 THEN ASM_REWRITE_TAC[]
2438 THEN ONCE_REWRITE_TAC[DIST_SYM]
2439 THEN ASM_REWRITE_TAC[];
2441 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`1`;`3`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ SUC 1 MOD 3=2/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
2443 THEN MP_TAC(SET_RULE`{v, w} = {v2, v3} /\ ~(v3=v2) ==>(v=v2 /\ w=v3)\/ (v=v3 /\
2445 THEN ASM_REWRITE_TAC[]
2447 THEN ASM_REWRITE_TAC[]
2448 THEN ONCE_REWRITE_TAC[DIST_SYM]
2449 THEN ASM_REWRITE_TAC[];
2451 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`2`;`3`][ARITH_RULE`~(3=0)/\ 2 MOD 3=2/\ SUC 2 MOD 3=0/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
2453 THEN MP_TAC(SET_RULE`{v, w} = {v3, v1} /\ ~(v1=v3) ==>(v=v1 /\ w=v3)\/ (v=v3 /\
2455 THEN ASM_REWRITE_TAC[]
2457 THEN ASM_REWRITE_TAC[]
2458 THEN ONCE_REWRITE_TAC[DIST_SYM]
2459 THEN ASM_REWRITE_TAC[]
2465 let ZITHLQN=prove_by_refinement(`(!s vv. MEM s s_init_list_v39 /\ vv IN
2467 &0 <= taustar_v39 s vv) ==> JEJTVGB_assume_v39`,
2470 REWRITE_TAC[IMP_CONJ]
2471 THEN REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2472 THEN REPEAT STRIP_TAC;
2474 MP_TAC(ARITH_RULE`4<= CARD(V:real^3->bool) /\ CARD(V:real^3->bool)<= 6
2475 ==> CARD V= 4\/ CARD V=5 \/ CARD V=6 `)
2478 ABBREV_TAC`(s=let upperbd = &6 in
2479 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2480 else (if {i MOD k,j MOD k}={0,1} then p
2481 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2482 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))`
2486 (let upperbd = &6 in
2489 if i MOD k = j MOD k
2491 else if {i MOD k, j MOD k} = {0, 1}
2493 else if j MOD k = SUC i MOD k \/
2494 SUC j MOD k = i MOD k
2497 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2498 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2499 (cs_adj 5 (&2) (&2 * h0))
2500 (cs_adj 5 (&2 * h0) upperbd);
2501 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2502 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2503 (cs_adj 3 (&2) (&2 * h0))
2504 (cs_adj 3 (&2 * h0) upperbd);
2505 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2506 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2507 (cs_adj 4 (&2) (&3))
2508 (cs_adj 4 (&2 * h0) upperbd);
2509 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2510 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2511 (a_pro 4 (&2 * h0) (&2) sqrt8)
2512 (a_pro 4 sqrt8 (&2 * h0)
2513 upperbd)])` ASSUME_TAC;
2516 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;]
2520 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4`]
2522 THEN MP_TAC ZITHLQN_CASE_4
2523 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2524 THEN ASM_REWRITE_TAC[]
2526 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2527 THEN POP_ASSUM MP_TAC
2528 THEN ASM_REWRITE_TAC[]
2529 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2530 THEN ASM_REWRITE_TAC[])
2532 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2533 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2534 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2535 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2536 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2539 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2540 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
2542 ASM_REWRITE_TAC[d_tame]
2543 THEN MP_TAC dsv_scs_init
2544 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2546 THEN ASM_REWRITE_TAC[]
2548 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2549 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2550 THEN REAL_ARITH_TAC;
2552 ABBREV_TAC`(s=let upperbd = &6 in
2553 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2554 else (if {i MOD k,j MOD k}={0,1} then p
2555 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2556 mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd) )`
2560 (let upperbd = &6 in
2563 if i MOD k = j MOD k
2565 else if {i MOD k, j MOD k} = {0, 1}
2567 else if j MOD k = SUC i MOD k \/
2568 SUC j MOD k = i MOD k
2571 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2572 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2573 (cs_adj 5 (&2) (&2 * h0))
2574 (cs_adj 5 (&2 * h0) upperbd);
2575 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2576 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2577 (cs_adj 3 (&2) (&2 * h0))
2578 (cs_adj 3 (&2 * h0) upperbd);
2579 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2580 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2581 (cs_adj 4 (&2) (&3))
2582 (cs_adj 4 (&2 * h0) upperbd);
2583 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2584 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2585 (a_pro 4 (&2 * h0) (&2) sqrt8)
2586 (a_pro 4 sqrt8 (&2 * h0)
2587 upperbd)])` ASSUME_TAC;
2590 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2594 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5`]
2596 THEN MP_TAC ZITHLQN_CASE_5
2597 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2598 THEN ASM_REWRITE_TAC[]
2600 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2601 THEN POP_ASSUM MP_TAC
2602 THEN ASM_REWRITE_TAC[]
2603 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2604 THEN ASM_REWRITE_TAC[])
2606 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2607 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2608 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2609 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2610 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2613 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2614 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2616 ASM_REWRITE_TAC[d_tame]
2617 THEN MP_TAC dsv_scs_init
2618 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2620 THEN ASM_REWRITE_TAC[]
2622 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2623 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2624 THEN REAL_ARITH_TAC;
2626 ABBREV_TAC`(s=let upperbd = &6 in
2627 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2628 else (if {i MOD k,j MOD k}={0,1} then p
2629 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2630 mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd) )`
2634 (let upperbd = &6 in
2637 if i MOD k = j MOD k
2639 else if {i MOD k, j MOD k} = {0, 1}
2641 else if j MOD k = SUC i MOD k \/
2642 SUC j MOD k = i MOD k
2645 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2646 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2647 (cs_adj 5 (&2) (&2 * h0))
2648 (cs_adj 5 (&2 * h0) upperbd);
2649 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2650 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2651 (cs_adj 3 (&2) (&2 * h0))
2652 (cs_adj 3 (&2 * h0) upperbd);
2653 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2654 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2655 (cs_adj 4 (&2) (&3))
2656 (cs_adj 4 (&2 * h0) upperbd);
2657 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2658 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2659 (a_pro 4 (&2 * h0) (&2) sqrt8)
2660 (a_pro 4 sqrt8 (&2 * h0)
2661 upperbd)])` ASSUME_TAC;
2664 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2668 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=6`]
2670 THEN MP_TAC ZITHLQN_CASE_6
2671 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2672 THEN ASM_REWRITE_TAC[]
2674 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2675 THEN POP_ASSUM MP_TAC
2676 THEN ASM_REWRITE_TAC[]
2677 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2678 THEN ASM_REWRITE_TAC[])
2680 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2681 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2682 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2683 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2684 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2687 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2688 ;ARITH_RULE`~(6<=3)`;mk_unadorned_v39;CS_ADJ];
2690 ASM_REWRITE_TAC[d_tame]
2691 THEN MP_TAC dsv_scs_init
2692 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2694 THEN ASM_REWRITE_TAC[]
2696 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2697 ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2698 THEN REAL_ARITH_TAC;
2701 if i MOD 3 = 0 then v1 else
2702 if i MOD 3 = 1 then v2 else v3:real^3)`
2703 THEN ABBREV_TAC`V = IMAGE (vv:num->real^3) (:num)`
2704 THEN ABBREV_TAC` E= IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num) `
2705 THEN ABBREV_TAC` FF= IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num) `
2706 THEN ABBREV_TAC`(s=let upperbd = &6 in
2707 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2708 else (if {i MOD k,j MOD k}={0,1} then p
2709 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2710 mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))`
2714 (let upperbd = &6 in
2717 if i MOD k = j MOD k
2719 else if {i MOD k, j MOD k} = {0, 1}
2721 else if j MOD k = SUC i MOD k \/
2722 SUC j MOD k = i MOD k
2725 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2726 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2727 (cs_adj 5 (&2) (&2 * h0))
2728 (cs_adj 5 (&2 * h0) upperbd);
2729 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2730 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2731 (cs_adj 3 (&2) (&2 * h0))
2732 (cs_adj 3 (&2 * h0) upperbd);
2733 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2734 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2735 (cs_adj 4 (&2) (&3))
2736 (cs_adj 4 (&2 * h0) upperbd);
2737 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2738 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2739 (a_pro 4 (&2 * h0) (&2) sqrt8)
2740 (a_pro 4 sqrt8 (&2 * h0)
2741 upperbd)])` ASSUME_TAC;
2744 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2748 THEN ASM_REWRITE_TAC[]
2750 THEN MP_TAC ZITHLQN_CASE_3
2751 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
2752 THEN ASM_REWRITE_TAC[]
2754 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2755 THEN POP_ASSUM MP_TAC
2756 THEN ASM_REWRITE_TAC[]
2757 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2758 THEN ASM_REWRITE_TAC[])
2759 THEN SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
2761 THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
2762 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2763 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2764 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2765 THEN SUBGOAL_THEN`(scs_k_v39 s <= 3)` ASSUME_TAC;
2768 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2769 ;ARITH_RULE`(3<=3)`;mk_unadorned_v39;CS_ADJ];
2771 ASM_REWRITE_TAC[d_tame]
2772 THEN MP_TAC dsv_scs_init
2773 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2775 THEN ASM_REWRITE_TAC[]
2777 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2778 ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2779 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
2780 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th;])
2781 THEN REPEAT STRIP_TAC
2782 THEN POP_ASSUM MP_TAC
2783 THEN REWRITE_TAC[ARITH_RULE`0 MOD 3=0/\ 1 MOD 3=1 /\ 2 MOD 3=2/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)`]
2784 THEN REAL_ARITH_TAC;
2786 ABBREV_TAC`(s=let upperbd = &6 in
2787 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2788 else (if {i MOD k,j MOD k}={0,1} then p
2789 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2790 mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd) )`
2794 (let upperbd = &6 in
2797 if i MOD k = j MOD k
2799 else if {i MOD k, j MOD k} = {0, 1}
2801 else if j MOD k = SUC i MOD k \/
2802 SUC j MOD k = i MOD k
2805 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2806 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2807 (cs_adj 5 (&2) (&2 * h0))
2808 (cs_adj 5 (&2 * h0) upperbd);
2809 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2810 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2811 (cs_adj 3 (&2) (&2 * h0))
2812 (cs_adj 3 (&2 * h0) upperbd);
2813 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2814 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2815 (cs_adj 4 (&2) (&3))
2816 (cs_adj 4 (&2 * h0) upperbd);
2817 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2818 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2819 (a_pro 4 (&2 * h0) (&2) sqrt8)
2820 (a_pro 4 sqrt8 (&2 * h0)
2821 upperbd)])` ASSUME_TAC;
2824 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2828 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5/\ 5<=6`]
2830 THEN MP_TAC ZITHLQN_CASE_5_sqrt8
2831 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2832 THEN ASM_REWRITE_TAC[]
2834 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2835 THEN POP_ASSUM MP_TAC
2836 THEN ASM_REWRITE_TAC[]
2837 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2838 THEN ASM_REWRITE_TAC[])
2840 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2841 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2842 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2843 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2844 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2847 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2848 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2850 ASM_REWRITE_TAC[d_tame]
2851 THEN MP_TAC dsv_scs_init
2852 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2854 THEN ASM_REWRITE_TAC[]
2856 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2857 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2858 THEN REAL_ARITH_TAC;
2860 ABBREV_TAC`(s=let upperbd = &6 in
2861 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2862 else (if {i MOD k,j MOD k}={0,1} then p
2863 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2864 mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd) )`
2868 (let upperbd = &6 in
2871 if i MOD k = j MOD k
2873 else if {i MOD k, j MOD k} = {0, 1}
2875 else if j MOD k = SUC i MOD k \/
2876 SUC j MOD k = i MOD k
2879 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2880 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2881 (cs_adj 5 (&2) (&2 * h0))
2882 (cs_adj 5 (&2 * h0) upperbd);
2883 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2884 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2885 (cs_adj 3 (&2) (&2 * h0))
2886 (cs_adj 3 (&2 * h0) upperbd);
2887 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2888 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2889 (cs_adj 4 (&2) (&3))
2890 (cs_adj 4 (&2 * h0) upperbd);
2891 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2892 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2893 (a_pro 4 (&2 * h0) (&2) sqrt8)
2894 (a_pro 4 sqrt8 (&2 * h0)
2895 upperbd)])` ASSUME_TAC;
2898 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2901 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2902 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2903 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];
2905 MRESA_TAC(GEN_ALL exists_vv_FF)
2906 [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
2907 THEN POP_ASSUM MP_TAC
2908 THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
2910 THEN MP_TAC ZITHLQN_CASE_5_pro_cs
2911 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2912 THEN ASM_REWRITE_TAC[]
2914 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2915 THEN POP_ASSUM MP_TAC
2916 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2918 THEN ASM_REWRITE_TAC[]
2920 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
2921 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2922 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2923 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2924 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2927 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2928 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2930 ASM_REWRITE_TAC[d_tame]
2931 THEN MP_TAC dsv_scs_init
2932 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2934 THEN ASM_REWRITE_TAC[]
2936 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2937 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2938 THEN REAL_ARITH_TAC;
2940 MRESA_TAC(GEN_ALL exists_vv_FF)
2941 [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
2942 THEN POP_ASSUM MP_TAC
2943 THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
2945 THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
2946 (GEN_ALL ZITHLQN_CASE_5_pro_cs))
2947 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2948 THEN ASM_REWRITE_TAC[]
2949 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2950 THEN ASM_REWRITE_TAC[DIST_SYM]
2952 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2953 THEN POP_ASSUM MP_TAC
2954 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
2956 THEN ASM_REWRITE_TAC[]
2957 THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
2958 THEN POP_ASSUM MP_TAC
2959 THEN POP_ASSUM MP_TAC
2960 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2962 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
2966 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
2967 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2968 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2969 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2970 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2973 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2974 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2976 ASM_REWRITE_TAC[d_tame]
2977 THEN MP_TAC dsv_scs_init
2978 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2980 THEN ASM_REWRITE_TAC[]
2982 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2983 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2984 THEN REAL_ARITH_TAC;
2986 ABBREV_TAC`(s=let upperbd = &6 in
2987 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2988 else (if {i MOD k,j MOD k}={0,1} then p
2989 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2990 mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) )`
2994 (let upperbd = &6 in
2997 if i MOD k = j MOD k
2999 else if {i MOD k, j MOD k} = {0, 1}
3001 else if j MOD k = SUC i MOD k \/
3002 SUC j MOD k = i MOD k
3005 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
3006 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
3007 (cs_adj 5 (&2) (&2 * h0))
3008 (cs_adj 5 (&2 * h0) upperbd);
3009 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
3010 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
3011 (cs_adj 3 (&2) (&2 * h0))
3012 (cs_adj 3 (&2 * h0) upperbd);
3013 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
3014 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
3015 (cs_adj 4 (&2) (&3))
3016 (cs_adj 4 (&2 * h0) upperbd);
3017 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
3018 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
3019 (a_pro 4 (&2 * h0) (&2) sqrt8)
3020 (a_pro 4 sqrt8 (&2 * h0)
3021 upperbd)])` ASSUME_TAC;
3024 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
3027 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
3028 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
3029 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];
3031 MRESA_TAC(GEN_ALL exists_vv_FF)
3032 [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
3033 THEN POP_ASSUM MP_TAC
3034 THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
3036 THEN MP_TAC ZITHLQN_CASE_4_pro_cs
3037 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3038 THEN ASM_REWRITE_TAC[]
3040 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3041 THEN POP_ASSUM MP_TAC
3042 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
3044 THEN ASM_REWRITE_TAC[]
3046 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
3047 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3048 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3049 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3050 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3053 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3054 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3056 ASM_REWRITE_TAC[d_tame]
3057 THEN MP_TAC dsv_scs_init
3058 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3060 THEN ASM_REWRITE_TAC[]
3062 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3063 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3064 THEN REAL_ARITH_TAC;
3066 MRESA_TAC(GEN_ALL exists_vv_FF)
3067 [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
3068 THEN POP_ASSUM MP_TAC
3069 THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
3071 THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
3072 (GEN_ALL ZITHLQN_CASE_4_pro_cs))
3073 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3074 THEN ASM_REWRITE_TAC[]
3075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3076 THEN ASM_REWRITE_TAC[DIST_SYM]
3078 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3079 THEN POP_ASSUM MP_TAC
3080 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
3082 THEN ASM_REWRITE_TAC[]
3083 THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
3084 THEN POP_ASSUM MP_TAC
3085 THEN POP_ASSUM MP_TAC
3086 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3088 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
3092 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
3093 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3094 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3095 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3096 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3099 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3100 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3102 ASM_REWRITE_TAC[d_tame]
3103 THEN MP_TAC dsv_scs_init
3104 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3106 THEN ASM_REWRITE_TAC[]
3108 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3109 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3110 THEN REAL_ARITH_TAC;
3112 ABBREV_TAC`(s=let upperbd = &6 in
3113 let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
3114 else (if {i MOD k,j MOD k}={0,1} then p
3115 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
3116 mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))`
3120 (let upperbd = &6 in
3123 if i MOD k = j MOD k
3125 else if {i MOD k, j MOD k} = {0, 1}
3127 else if j MOD k = SUC i MOD k \/
3128 SUC j MOD k = i MOD k
3131 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
3132 (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
3133 (cs_adj 5 (&2) (&2 * h0))
3134 (cs_adj 5 (&2 * h0) upperbd);
3135 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
3136 (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
3137 (cs_adj 3 (&2) (&2 * h0))
3138 (cs_adj 3 (&2 * h0) upperbd);
3139 mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
3140 (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
3141 (cs_adj 4 (&2) (&3))
3142 (cs_adj 4 (&2 * h0) upperbd);
3143 mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
3144 (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
3145 (a_pro 4 (&2 * h0) (&2) sqrt8)
3146 (a_pro 4 sqrt8 (&2 * h0)
3147 upperbd)])` ASSUME_TAC;
3150 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
3154 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4/\ 4<=6`]
3156 THEN MP_TAC ZITHLQN_CASE_4_3
3157 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3158 THEN ASM_REWRITE_TAC[]
3160 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3161 THEN POP_ASSUM MP_TAC
3162 THEN ASM_REWRITE_TAC[]
3163 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th]
3164 THEN ASM_REWRITE_TAC[])
3166 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
3167 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3168 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3169 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3170 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3173 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3174 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3176 ASM_REWRITE_TAC[d_tame]
3177 THEN MP_TAC dsv_scs_init
3178 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3180 THEN ASM_REWRITE_TAC[]
3182 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3183 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3184 THEN REAL_ARITH_TAC;
3196 let check_completeness_claimA_concl =
3197 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)