(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Zithlqn = struct open Hypermap;; open Fan;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Flyspeck_constants;; open Pack_defs;; open Hales_tactic;; open Appendix;; let s_init_J_empty= prove_by_refinement( `!s. MEM s s_init_list_v39 ==> scs_J_v39 s = (\i j. F)`, (* {{{ proof *) [ 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; scs_J_v39_explicit;mk_unadorned_v39] ]);; (* }}} *) let dsv_scs_init= prove_by_refinement( ` MEM s s_init_list_v39 ==> dsv_v39 s vv = scs_d_v39 s`, (* {{{ proof *) [ SIMP_TAC[s_init_J_empty;dsv_J_empty] ]);; (* }}} *) let exists_point_in_V= prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ 3 <= CARD V /\ CARD V <= 6 ==> ?v. v IN V`, (* {{{ proof *) [ ONCE_REWRITE_TAC[SET_RULE`(?v. v IN V)<=> ~(V={})`] THEN REPEAT STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;CARD_CLAUSES]) THEN ARITH_TAC ]);; (* }}} *) let exists_vv_FF= prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ 3 <= CARD V /\ CARD V <= 6 /\ v, w IN FF ==> ?vv. vv 0=v /\ vv 1= w /\ (!i. vv i= vv (i MOD (CARD V))) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)` THEN REWRITE_TAC[IMAGE;] THEN STRIP_TAC; REWRITE_TAC[ITER]; STRIP_TAC; REWRITE_TAC[ARITH_RULE`1= SUC 0`; ITER] THEN MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]; MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN 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)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC; GEN_TAC THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th]) THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN RESA_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`) 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`] 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]; STRIP_TAC; POP_ASSUM MP_TAC THEN SET_TAC[]; STRIP_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA) [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`] THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`]) THEN POP_ASSUM MATCH_MP_TAC THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`] THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`]; REMOVE_ASSUM_TAC THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC; REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; REWRITE_TAC[IN_ELIM_THM] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]); ASM_REWRITE_TAC[] THEN STRIP_TAC; ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] 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] 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`] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) 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)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM]; POP_ASSUM MP_TAC 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)`] THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND) [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;] THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`] THEN STRIP_TAC; EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[ITER]; MP_TAC(ARITH_RULE`x =0 \/ 0 ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC) THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`) THEN EXISTS_TAC`CARD (V:real^3->bool) -1` THEN ASM_REWRITE_TAC[] THEN MP_TAC Tecoxbm.RHO_IVS_IDD THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[]; SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC); EXISTS_TAC`x-1` THEN POP_ASSUM MP_TAC THEN ARITH_TAC; EXISTS_TAC`x'':num` THEN ASM_REWRITE_TAC[ITER] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`) THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD) [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;] THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`) THEN REWRITE_TAC[ITER] THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`; ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`) THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) 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)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[ITER] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) ]);; (* }}} *) let exists_vv= prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ 3 <= CARD V /\ CARD V <= 6 ==> ?vv. (!i. vv i= vv (i MOD (CARD V))) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN MP_TAC exists_point_in_V THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)` THEN REWRITE_TAC[IMAGE;] THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC; GEN_TAC THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th]) THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN RESA_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`) 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`] 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]; STRIP_TAC; POP_ASSUM MP_TAC THEN SET_TAC[]; STRIP_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA) [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`] THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`]) THEN POP_ASSUM MATCH_MP_TAC THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`] THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`]; REMOVE_ASSUM_TAC THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC; REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; REWRITE_TAC[IN_ELIM_THM] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]); ASM_REWRITE_TAC[] THEN STRIP_TAC; ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] 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] 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`] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) 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)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM]; POP_ASSUM MP_TAC 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)`] THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND) [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;] THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`] THEN STRIP_TAC; EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[ITER]; MP_TAC(ARITH_RULE`x =0 \/ 0 ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC) THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`) THEN EXISTS_TAC`CARD (V:real^3->bool) -1` THEN ASM_REWRITE_TAC[] THEN MP_TAC Tecoxbm.RHO_IVS_IDD THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[]; SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC); EXISTS_TAC`x-1` THEN POP_ASSUM MP_TAC THEN ARITH_TAC; EXISTS_TAC`x'':num` THEN ASM_REWRITE_TAC[ITER] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`) THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD) [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;] THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`) THEN REWRITE_TAC[ITER] THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`; ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC; STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`) THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) 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)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[ITER] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) ]);; (* }}} *) let SUC_MOD_NOT_EQ=prove_by_refinement( `~(i MOD 3 = SUC i MOD 3)`, (* {{{ proof *) [ REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN DISCH_THEN(LABEL_TAC"EM") THEN MRESAL_TAC DIV_MONO[`i:num`;`i+1`;`3`][ARITH_RULE`~(3=0)/\ i<= i+1`] THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`] THEN POP_ASSUM MP_TAC 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`) THEN RESA_TAC; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th]) THEN ARITH_TAC; STRIP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_THEN "YEU"(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th]) THEN REWRITE_TAC[ARITH_RULE`(i DIV 3 * 3 + (i + 1) MOD 3) + 1 = (i + 1) DIV 3 * 3 + (i + 1) MOD 3 <=> 1 = ((i + 1) DIV 3 - i DIV 3) * 3`] THEN MP_TAC(ARITH_RULE`i DIV 3 < (i + 1) DIV 3 ==> 1<= ( (i + 1) DIV 3 -i DIV 3 )`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE` 1<= ( (i + 1) DIV 3 -i DIV 3 )==> 3<= ( (i + 1) DIV 3 -i DIV 3 ) *3`) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC ]);; (* }}} *) let SUC_MOD_EQ1=prove_by_refinement( `(SUC i MOD 3 = SUC j MOD 3) /\ i<=j ==> (i MOD 3 = j MOD 3) `, (* {{{ proof *) [ REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`i + 1 = (i + 1) DIV 3 * 3 + (j + 1) MOD 3 <=> (j + 1) MOD 3= (i + 1) - ((i + 1) DIV 3 * 3) `] THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`j+1:num`;`3`][ARITH_RULE`~(3=0)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC 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 `] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`) THEN RESA_TAC THEN MRESAL_TAC DIV_MONO[`i+1`;`j+1`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`j + (i + 1) DIV 3 * 3 = (j + 1) DIV 3 * 3 + i /\ i<= j /\ (i + 1) DIV 3 <= (j + 1) DIV 3 ==> j -i = 3*((j + 1) DIV 3 - (i + 1) DIV 3) `) THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`j = j DIV 3 * 3 + j MOD 3 /\ i = i DIV 3 * 3 + i MOD 3 /\ i<= j/\ i DIV 3<= j DIV 3 ==> j-i = ((j DIV 3 - i DIV 3) * 3 + j MOD 3) -i MOD 3 `) THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th]) THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th]) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN STRIP_TAC THEN MRESAL_TAC MOD_MULT[`3`;`(j + 1) DIV 3 - (i + 1) DIV 3`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE`a*b=b*a`] THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MP_TAC(ARITH_RULE`i MOD 3 <=j MOD 3 \/ j MOD 3 < i MOD 3:num`) THEN STRIP_TAC; MP_TAC(ARITH_RULE` i MOD 3 <=j MOD 3 ==> ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3 = (j DIV 3 - i DIV 3) * 3 + j MOD 3 - i MOD 3 `) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3)`;`3`;`j MOD 3 - i MOD 3`] THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`j MOD 3 < 3 /\ i MOD 3 <=j MOD 3 ==> j MOD 3 - i MOD 3 < 3 `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MRESA_TAC MOD_LT[`j MOD 3 - i MOD 3`;`3`] THEN ASM_TAC THEN ARITH_TAC; MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`i MOD 3 < 3/\ j MOD 3< i MOD 3 ==> (3+ j MOD 3) - i MOD 3 < 3 /\ 0< (3+ j MOD 3) - i MOD 3`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`j DIV 3 - i DIV 3 =0 \/ 1<= j DIV 3 - i DIV 3:num`) THEN STRIP_TAC; 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`]) THEN REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`j MOD 3 < i MOD 3 /\ j - i = j MOD 3 - i MOD 3 /\ i<= j ==> j=i `) THEN ASM_REWRITE_TAC[] THEN RESA_TAC; STRIP_TAC THEN MP_TAC(ARITH_RULE`1 <= j DIV 3 - i DIV 3 /\ 0 < (3 + j MOD 3) - i MOD 3 ==> ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3 =((j DIV 3 - i DIV 3)-1) * 3 +(3+ j MOD 3) - i MOD 3`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3 -1)`;`3`;`(3+ j MOD 3) - i MOD 3`] THEN MRESA_TAC MOD_LT[`(3+j MOD 3) - i MOD 3`;`3`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC ]);; (* }}} *) let SUC_MOD_EQ=prove_by_refinement( `(SUC i MOD 3 = SUC j MOD 3) ==> (i MOD 3 = j MOD 3) `, (* {{{ proof *) [ REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`) THEN STRIP_TAC; MATCH_MP_TAC SUC_MOD_EQ1 THEN ASM_REWRITE_TAC[]; MRESA_TAC (GEN_ALL SUC_MOD_EQ1)[`j:num`;`i:num`] THEN ASM_REWRITE_TAC[] ]);; (* }}} *) let NOT_IMP_SUC_MOD_EQ=prove_by_refinement( `~(i MOD 3 = j MOD 3) ==> ~(SUC i MOD 3 = SUC j MOD 3)`, [SIMP_TAC[CONTRAPOS_THM;] THEN REWRITE_TAC[SUC_MOD_EQ]]);; let IMP_SUC_MOD_EQ1=prove_by_refinement( ` ~(k=0) /\ (i MOD k = j MOD k) /\ i<= j ==> (SUC i MOD k = SUC j MOD k)`, (* {{{ proof *) [ REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN REMOVE_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i:num = i DIV k * k + j MOD k ==> j MOD k = i - (i DIV k * k) `) 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) THEN RESA_TAC THEN MRESAL_TAC DIVISION[`j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`) THEN RESA_TAC THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`j = (j DIV k) * k + i - (i DIV k) * k /\ i +1 <= j+1 /\ i DIV k <= j DIV k /\ ~(k=0) ==> j -i = (j DIV k) *k - (i DIV k) *k `) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th]) THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN ONCE_REWRITE_TAC[MULT_AC] THEN MRESAL_TAC DIV_MONO[`i+1:num`;`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESA_TAC LE_MULT_RCANCEL[`((i+1) DIV k)`;`((j+1) DIV k)`;`k:num`] THEN MP_TAC(ARITH_RULE`i + 1 = (i + 1) DIV k * k + (i + 1) MOD k /\ j + 1 = (j + 1) DIV k * k + (j + 1) MOD k /\ i<= j/\ ((i+1) DIV k)*k<= ((j+1) DIV k)*k ==> j-i = (((j + 1) DIV k * k - (i + 1) DIV k * k) + (j + 1) MOD k) - (i + 1) MOD k`) THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th]) THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th]) THEN ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN STRIP_TAC THEN STRIP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`j DIV k - i DIV k`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MP_TAC(ARITH_RULE`(i+1) MOD k <=(j+1) MOD k \/ (j+1) MOD k < (i+1) MOD k:num`) THEN STRIP_TAC; MP_TAC(ARITH_RULE` (i+1) MOD k <=(j+1) MOD k ==> ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)= (((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k - (i + 1) MOD k)`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`;`(j + 1) MOD k - (i + 1) MOD k`] THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < k /\ (i + 1) MOD k <=(j + 1) MOD k ==> (j + 1) MOD k - (i + 1) MOD k < k `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MRESA_TAC MOD_LT[`(j + 1) MOD k - (i + 1) MOD k`;` k:num`] THEN REPLICATE_TAC 8 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`(i+1) MOD k < k/\ (j+1) MOD k< (i+1) MOD k ==> (k+ (j+1) MOD k) - (i+1) MOD k < k /\ 0< (k+ (j+1) MOD k) - (i+1) MOD k`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`(j+1) DIV k - (i+1) DIV k =0 \/ 1<= (j+1) DIV k - (i+1) DIV k`) THEN STRIP_TAC; 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`]) THEN REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < (i + 1) MOD k /\ j - i = (j + 1) MOD k - (i + 1) MOD k /\ i<= j ==> j=i `) THEN ASM_REWRITE_TAC[] THEN RESA_TAC; STRIP_TAC THEN MRESAL_TAC LE_MULT_RCANCEL[`1`;`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`][ARITH_RULE`1*k=k`] 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 ==> ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k) = ((((j + 1) DIV k - (i + 1) DIV k) * k- 1*k)+(k+ (j + 1) MOD k) - (i + 1) MOD k) `) THEN RESA_TAC THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] 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`] THEN MRESA_TAC MOD_LT[`(k + (j + 1) MOD k) - (i + 1) MOD k`;`k:num`] THEN REPLICATE_TAC 4 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC ]);; (* }}} *) let IMP_SUC_MOD_EQ=prove_by_refinement( ` ~(k=0) /\ (i MOD k = j MOD k) ==> (SUC i MOD k = SUC j MOD k)`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`) THEN STRIP_TAC; MATCH_MP_TAC IMP_SUC_MOD_EQ1 THEN ASM_REWRITE_TAC[]; MRESA_TAC (GEN_ALL IMP_SUC_MOD_EQ1)[`j:num`;`i:num`;`k:num`] THEN ASM_REWRITE_TAC[] ]);; (* }}} *) let CHOOSE_MOD_3=prove_by_refinement( `~(i MOD 3 = j MOD 3) /\ ~(SUC j MOD 3 = i MOD 3) ==> j MOD 3 = SUC i MOD 3`, (* {{{ proof *) [ MP_TAC(ARITH_RULE`i MOD 3= 0 \/ i MOD 3= 1 \/ i MOD 3= 2`) THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`] THEN MP_TAC(ARITH_RULE`j MOD 3= 0 \/ j MOD 3= 1 \/ j MOD 3= 2`) THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`] THEN MP_TAC(ARITH_RULE`SUC j MOD 3= 0 \/ SUC j MOD 3= 1 \/ SUC j MOD 3= 2`) THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`] THEN REPEAT STRIP_TAC THEN MP_TAC(SET_RULE`SUC j MOD 3 IN {0, 1, 2} /\ j MOD 3 IN {0, 1, 2} /\ i MOD 3 IN {0, 1, 2} ==> {SUC j MOD 3, j MOD 3, i MOD 3 }SUBSET {0, 1, 2}`) THEN RESA_TAC THEN SUBGOAL_THEN`CARD {SUC j MOD 3, j MOD 3, i MOD 3 }=3` ASSUME_TAC; ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY;] THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`j:num` THEN ARITH_TAC; SUBGOAL_THEN`CARD {0, 1, 2 }=3` ASSUME_TAC; ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY;] THEN ARITH_TAC; SUBGOAL_THEN`FINITE {0, 1, 2 }` ASSUME_TAC; ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY;]; MRESA_TAC CARD_SUBSET_EQ[`{SUC j MOD 3, j MOD 3, i MOD 3 }`;`{0, 1, 2}`] THEN MP_TAC(ARITH_RULE`SUC i MOD 3= 0 \/ SUC i MOD 3= 1 \/ SUC i MOD 3= 2`) THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ONCE_REWRITE_TAC[SET_RULE` A IN {B,C,D}<=> (A=B\/ A=C\/A=D)`] THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`i:num` THEN MRESA_TAC(GEN_ALL NOT_IMP_SUC_MOD_EQ)[`i:num`;`j:num`] THEN RESA_TAC ]);; (* }}} *) let SMALL_BALL_ANNULUS_6=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) /\ dist(v,w)<= &6 )`, (* {{{ proof *) [ REPEAT STRIP_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`]) THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus ==> v IN ball_annulus /\ w IN ball_annulus`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0] THEN REAL_ARITH_TAC ]);; (* }}} *) let SMALL_BALL_ANNULUS_6_sqrt8=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) /\ dist(v,w)<= &6 )`, (* {{{ proof *) [ REPEAT STRIP_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`]) THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus ==> v IN ball_annulus /\ w IN ball_annulus`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0] THEN REAL_ARITH_TAC ]);; (* }}} *) let SMALL_BALL_ANNULUS_6_3=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w)) ==> (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) /\ dist(v,w)<= &6 )`, (* {{{ proof *) [ REPEAT STRIP_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`]) THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus ==> v IN ball_annulus /\ w IN ball_annulus`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0] THEN REAL_ARITH_TAC ]);; (* }}} *) let CS_ADJ=prove(`cs_adj = (\k a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))`, MP_TAC( GENL [`k:num`;`a1:real`;`a2:real`;`i:num`;`j:num`] (SPEC_ALL cs_adj)) THEN REWRITE_TAC[GSYM FUN_EQ_THM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN SIMP_TAC[FUN_EQ_THM]);; let ZITHLQN_CASE_3=prove_by_refinement( ` V SUBSET ball_annulus /\ CARD V =3 /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;Oxl_def.periodic;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 3 = j MOD 3 \/ ~(i MOD 3 = j MOD 3)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 3 = i MOD 3 \/ ~(SUC j MOD 3 = i MOD 3)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 7 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); MP_TAC CHOOSE_MOD_3 THEN ASM_REWRITE_TAC[] THEN RESA_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;] THEN ARITH_TAC ]);; (* }}} *) let ZITHLQN_CASE_4=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =4 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_5=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =5 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_6=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =6 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 6 = j MOD 6 \/ ~(i MOD 6 = j MOD 6)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 6 = i MOD 6 \/ ~(SUC j MOD 6 = i MOD 6)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 6 = j MOD 6 \/ ~(SUC i MOD 6 = j MOD 6)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_5_pro_cs=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =5 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\ (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ {v0,w0} IN E /\ &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8 /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k ,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ vv 0= v0 /\ vv 1= w0 ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(SET_RULE`{i MOD 5,j MOD 5}={0,1} \/ ~({i MOD 5,j MOD 5}={0,1})`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC; STRIP_TAC THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]); 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)`) THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC; REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`]) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC; STRIP_TAC 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) `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`] THEN SET_TAC[]; POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC; REPLICATE_TAC 10 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`]) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC; STRIP_TAC 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) `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REPLICATE_TAC 14 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REPLICATE_TAC 14 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`] THEN SET_TAC[]; POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 10 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 18 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 18 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_4_3=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =4 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) ) /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6_3 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_5_sqrt8=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =5 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) ) /\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 12 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let ZITHLQN_CASE_4_pro_cs=prove_by_refinement( ` convex_local_fan (V,E,FF) /\ packing V /\ V SUBSET ball_annulus /\ CARD V =4 /\ (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\ (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\ {v0,w0} IN E /\ &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8 /\ (s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k ,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)) /\ (!i. vv (i MOD (CARD V))= vv i) /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V) /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ vv 0= v0 /\ vv 1= w0 ==> vv IN BBs_v39 s`, (* {{{ proof *) [ REPEAT STRIP_TAC THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8 THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ] THEN STRIP_TAC; ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic] THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`]; STRIP_TAC THEN REPEAT GEN_TAC; ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF] THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[DIST_POS_LE] THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`) THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN REPEAT RESA_TAC THEN REWRITE_TAC[DIST_REFL] THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[] THEN MP_TAC(SET_RULE`{i MOD 4,j MOD 4}={0,1} \/ ~({i MOD 4,j MOD 4}={0,1})`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC; STRIP_TAC THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]); 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)`) THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`] THEN STRIP_TAC THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC; REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`]) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC; STRIP_TAC 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) `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`] THEN SET_TAC[]; POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`) THEN STRIP_TAC; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC; REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`]) THEN REPEAT RESA_TAC THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`]; SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC; REPLICATE_TAC 10 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`]) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC; STRIP_TAC 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) `) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REPLICATE_TAC 14 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REPLICATE_TAC 14 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`]) THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`] THEN SET_TAC[]; POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]); ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC; STRIP_TAC THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(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`;] THEN POP_ASSUM MP_TAC THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[th]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC); POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`]) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`]; SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC; REPLICATE_TAC 10 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]); REPLICATE_TAC 18 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> REPLICATE_TAC 18 STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]) THEN POP_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM]) THEN STRIP_TAC; EXISTS_TAC`i:num` THEN SET_TAC[]; EXISTS_TAC`j:num` THEN SET_TAC[]; ]);; (* }}} *) let exists_vv3=prove_by_refinement( `&2 <= norm v1 /\ &2 <= norm v2 /\ &2 <= norm v3 /\ norm v1 <= &2 * h0 /\ norm v2 <= &2 * h0 /\ norm v3 <= &2 * h0 /\ &2 <= dist(v1,v2) /\ &2 <= dist(v1,v3) /\ &2 <= dist(v2,v3) /\ dist(v1,v2) <= &2 * h0 /\ dist(v1,v3) <= &2 * h0 /\ dist(v2,v3) <= &2 * h0 /\ (!i. vv i = if i MOD 3 = 0 then v1 else if i MOD 3 = 1 then v2 else v3) /\ V= IMAGE vv (:num) /\ E= IMAGE (\i. {vv i, vv (SUC i)}) (:num) /\ FF= IMAGE (\i. vv i,vv (SUC i)) (:num) ==> (!i. vv (i MOD (CARD V))= vv i) /\ V SUBSET ball_annulus /\ CARD V =3/\ (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)`, (* {{{ proof *) [ STRIP_TAC THEN SUBGOAL_THEN`(!i. (vv:num->real^3) (i MOD 3)= vv i)`ASSUME_TAC; ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]; SUBGOAL_THEN`(V:real^3->bool)={v1,v2,v3}`ASSUME_TAC; ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`x' MOD 3= 0 \/ x' MOD 3= 1\/ x' MOD 3=2`) THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; STRIP_TAC THEN MP_TAC(SET_RULE`x IN {v1, v2, v3:real^3} ==> x = v1 \/ x= v2 \/ x= v3`) THEN RESA_TAC; EXISTS_TAC`0:num` THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 3 = 0`] THEN SET_TAC[]; EXISTS_TAC`1:num` THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3 = 1/\ ~(1 MOD 3 = 0)`] THEN SET_TAC[]; EXISTS_TAC`2:num` THEN ASM_REWRITE_TAC[ARITH_RULE`~(2 MOD 3 = 1) /\ ~(2 MOD 3 = 0)`] THEN SET_TAC[]; SUBGOAL_THEN(`~(v1=v2:real^3) /\ ~(v1=v3:real^3) /\ ~(v3=v2:real^3)`)ASSUME_TAC; STRIP_TAC; STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL]) THEN REAL_ARITH_TAC; STRIP_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL]) THEN REAL_ARITH_TAC; SUBGOAL_THEN`CARD (V:real^3->bool)=3` ASSUME_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY;] THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN ARITH_TAC; POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN POP_ASSUM(fun th-> POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th]) THEN ASSUME_TAC th) THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`(v1 IN ball_annulus /\ v2 IN ball_annulus /\ v3 IN ball_annulus)==> {v1, v2, v3} SUBSET ball_annulus `) THEN RESA_TAC THEN ASM_REWRITE_TAC[ball_annulus;DIFF;cball;ball;IN_ELIM_THM; REAL_ARITH`~(a< &2)<=> &2<=a`;DIST_0]; REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`x MOD 3= 0 \/ x MOD 3= 1\/ x MOD 3=2`) THEN STRIP_TAC THEN ASM_REWRITE_TAC[]; 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)`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`{v, w} = {v1, v2} /\ ~(v1=v2) ==>(v=v1 /\ w=v2)\/ (v=v2 /\ w=v1:real^3)`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; 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)`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`{v, w} = {v2, v3} /\ ~(v3=v2) ==>(v=v2 /\ w=v3)\/ (v=v3 /\ w=v2:real^3)`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; 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)`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`{v, w} = {v3, v1} /\ ~(v1=v3) ==>(v=v1 /\ w=v3)\/ (v=v3 /\ w=v1:real^3)`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] ]);; (* }}} *) let ZITHLQN=prove_by_refinement(`(!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s ==> &0 <= taustar_v39 s vv) ==> JEJTVGB_assume_v39`, (* {{{ proof *) [ REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN REPEAT STRIP_TAC; MP_TAC(ARITH_RULE`4<= CARD(V:real^3->bool) /\ CARD(V:real^3->bool)<= 6 ==> CARD V= 4\/ CARD V=5 \/ CARD V=6 `) THEN RESA_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;] THEN SET_TAC[]; MP_TAC exists_vv THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_4 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN STRIP_TAC THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd) )` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MP_TAC exists_vv THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_5 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN STRIP_TAC THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd) )` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MP_TAC exists_vv THEN ASM_REWRITE_TAC[ARITH_RULE`3<=6`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_6 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN STRIP_TAC THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(6<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC `(vv i = if i MOD 3 = 0 then v1 else if i MOD 3 = 1 then v2 else v3:real^3)` THEN ABBREV_TAC`V = IMAGE (vv:num->real^3) (:num)` THEN ABBREV_TAC` E= IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num) ` THEN ABBREV_TAC` FF= IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num) ` THEN ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MP_TAC exists_vv3 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_3 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`] THEN STRIP_TAC THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`(3<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th;]) THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`0 MOD 3=0/\ 1 MOD 3=1 /\ 2 MOD 3=2/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)`] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd) )` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MP_TAC exists_vv THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5/\ 5<=6`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_5_sqrt8 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN STRIP_TAC THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd) )` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;]; MRESA_TAC(GEN_ALL exists_vv_FF) [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_5_pro_cs THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] ) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; MRESA_TAC(GEN_ALL exists_vv_FF) [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`] THEN STRIP_TAC 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`] (GEN_ALL ZITHLQN_CASE_5_pro_cs)) THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] ) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC th) THEN STRIP_TAC THEN STRIP_TAC THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) )` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF) [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;]; MRESA_TAC(GEN_ALL exists_vv_FF) [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_4_pro_cs THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] ) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; MRESA_TAC(GEN_ALL exists_vv_FF) [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`] THEN STRIP_TAC 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`] (GEN_ALL ZITHLQN_CASE_4_pro_cs)) THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[DIST_SYM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] ) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC th) THEN STRIP_TAC THEN STRIP_TAC THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ABBREV_TAC`(s=let upperbd = &6 in let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0 else (if {i MOD k,j MOD k}={0,1} then p else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))` THEN SUBGOAL_THEN `s IN set_of_list (let upperbd = &6 in let a_pro = (\k p a1 a2 i j. if i MOD k = j MOD k then &0 else if {i MOD k, j MOD k} = {0, 1} then p else if j MOD k = SUC i MOD k \/ SUC j MOD k = i MOD k then a1 else a2) in [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8) (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477 (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd)])` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39] THEN SET_TAC[]; MP_TAC exists_vv THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4/\ 4<=6`] THEN STRIP_TAC THEN MP_TAC ZITHLQN_CASE_4_3 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[GSYM th] THEN ASM_REWRITE_TAC[]) THEN STRIP_TAC THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM] THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC; EXPAND_TAC"s" THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ]; ASM_REWRITE_TAC[d_tame] THEN MP_TAC dsv_scs_init THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"s" THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ] THEN REAL_ARITH_TAC; ]);; (* }}} *) end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)