1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Rrcwnsj = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
92 let BB_VV_FUN_EQ=prove(`is_scs_v39 s /\ BBs_v39 s vv
93 ==> (!i j. vv i = vv j <=> i MOD (scs_k_v39 s) = j MOD (scs_k_v39 s))`,
97 MRESA_TAC W_IN_BB_FUN_EQ[`vv`;`i`;`j`;`s`];
98 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`vv`;`j`]]);;
100 let WL_IN_E=prove(`{(w:num->real^3) l,w (SUC l)} IN IMAGE (\i. {w i,w (SUC i)}) (:num)`,
101 REWRITE_TAC[IMAGE;IN_ELIM_THM]
102 THEN EXISTS_TAC`l:num`
103 THEN ASM_REWRITE_TAC[]
108 let LUNAR_IN_V=prove(`lunar (v,w) V E==> v IN V/\ w IN V`,
114 let B_LE_2h0_A_EQ2_IN_CASES_6=prove(
115 `scs_k_v39 s=6 /\ is_scs_v39 s
116 ==> !i. scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 `,
118 THEN POP_ASSUM (fun th-> MP_TAC th
120 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
124 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
125 THEN SUBGOAL_THEN`FINITE
127 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC
130 MATCH_MP_TAC FINITE_SUBSET
131 THEN EXISTS_TAC`0..6`
132 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
135 MRESA_TAC CARD_EQ_0[`{i | i < 6 /\
136 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
137 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
138 THEN MRESAL_TAC DIVISION[`i`;`6`][ARITH_RULE`~(6=0)`]
140 THEN THAYTHEL_TAC 0[`i MOD 6`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
141 THEN POP_ASSUM MP_TAC
142 THEN POP_ASSUM MP_TAC
143 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC(i MOD 6) MOD 6:num`;`s:scs_v39`;`i MOD 6:num`;`SUC(i MOD 6):num`][MOD_REFL;ARITH_RULE`~(6=0)`]
145 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`]
146 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`]
147 THEN THAYTHES_TAC (26-17)[`i MOD 6`;`SUC i MOD 6`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ]
149 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i:num`;`SUC(i MOD 6) MOD 6:num`;`s:scs_v39`;`i MOD 6:num`;`SUC(i MOD 6):num`][MOD_REFL;ARITH_RULE`~(6=0)`]
151 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`]
152 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ]
153 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD 6:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`]
154 THEN REAL_ARITH_TAC]);;
158 let J_EMPY_CASES_6=prove(`scs_k_v39 s=6 /\ is_scs_v39 s
159 ==> scs_J_v39 s i= {}`,
161 THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s i x) \/ (scs_J_v39 s i= {})`)
163 THEN MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
166 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
168 THEN THAYTHEL_ASM_TAC(22-19)[`i`;`x`][]
169 THEN THAYTHEL_ASM_TAC (24-18)[`i`;`x`][]
175 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`i`;`SUC i`][is_scs_v39]
176 THEN THAYTHE_TAC (25-19)[`i`]
177 THEN REMOVE_ASSUM_TAC
178 THEN POP_ASSUM MP_TAC
180 THEN REWRITE_TAC[h0;cstab]
186 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`SUC x`;`x`][is_scs_v39]
187 THEN THAYTHE_TAC (25-19)[`x`]
188 THEN REMOVE_ASSUM_TAC
189 THEN POP_ASSUM MP_TAC
191 THEN REWRITE_TAC[h0;cstab]
192 THEN REAL_ARITH_TAC]);;
195 let BB_RHO_NODE_IVS=prove(`scs_k_v39 s = k /\
197 IMAGE vv (:num) = V /\
198 IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
199 IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\
203 ==> rho_node1 FF u = vv (p1+1) /\ ivs_rho_node1 FF u = vv (p1+k-1)`,
205 THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
207 THEN MP_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME
209 THEN THAYTHEL_ASM_TAC 0[`SUC 0`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
210 THEN THAYTHEL_ASM_TAC 0[`k-1`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
211 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`vv`]
212 THEN MP_TAC Local_lemmas.CVLF_LF_F
214 THEN MRESA_TAC WL_IN_V[`p1`;`vv`]
215 THEN MP_TAC Odxlstcv2.CARD_V_EQ_SCS_K1
217 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
219 THEN THAYTHES_TAC 0[`vv p1`][WL_IN_V;ARITH_RULE`k-1+a=a+k-1`]);;
223 let BB_F_SUC_PRE=prove(`is_scs_v39 s /\ BBs_v39 s f ==> f (SUC (i + (scs_k_v39 s) - 1)) = f i`,
225 THEN MATCH_MP_TAC Oxlzlez.F_SUC_PRE
226 THEN POP_ASSUM MP_TAC
227 THEN POP_ASSUM MP_TAC
228 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
230 THEN POP_ASSUM MP_TAC
235 let RRCWNSJ_concl = `
236 main_nonlinear_terminal_v11
237 ==>(!s (v:num->real^3).
238 is_scs_v39 s /\ scs_basic_v39 s /\ MMs_v39 s v/\
240 (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
241 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) /\
242 (!i. scs_b_v39 s i (SUC i) <= cstab) ==>
248 let RRCWNSJ = prove_by_refinement(
253 THEN ABBREV_TAC`k= scs_k_v39 s`
254 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
255 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
256 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
258 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
259 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
260 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
261 THEN MP_TAC Local_lemmas.CVLF_LF_F
263 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
265 THEN MRESA_TAC LUNAR_IN_V[`E`;`v'`;`w`;`V`]
266 THEN POP_ASSUM MP_TAC
267 THEN POP_ASSUM MP_TAC
269 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
273 THEN MRESA_TAC Axjrpnc.AXJRPNC[`s`;`v`;`x`;`x'`]
276 THEN POP_ASSUM(fun th->ASSUME_TAC (SYM th))
277 THEN MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
279 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
280 THEN THAYTHEL_ASM_TAC 0[`x`][]
281 THEN THAYTHE_TAC 0[`SUC x`]
282 THEN SUBGOAL_THEN`norm((v:num->real^3) (SUC x))= &2 \/ norm (v x- v (SUC x))= &2` ASSUME_TAC;
284 MP_TAC(REAL_ARITH`&2 <= norm (v x - v (SUC x))
285 /\ &2 <= norm (v (SUC x) - v (SUC (SUC x)))
286 ==> (&2 < norm (v x - v (SUC x))
287 /\ &2 < norm (v (SUC x) - v (SUC (SUC x))))\/ norm (v x - v (SUC x))= &2
288 \/ (norm ((v:num->real^3) (SUC x) - v (SUC (SUC x)))= &2) `)
291 SUBGOAL_THEN`!i. ~(i MOD k = (SUC x) MOD k) ==> scs_a_v39 s (SUC x) i < dist (v (SUC x),(v:num->real^3) i)`ASSUME_TAC
296 THEN MP_TAC(SET_RULE`i MOD k= x MOD k\/ ~(i MOD k= x MOD k)`)
300 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
301 THEN ONCE_REWRITE_TAC[DIST_SYM]
302 THEN ASM_REWRITE_TAC[dist]
303 THEN THAYTHE_TAC (33-26)[`x`]
304 THEN DICH_TAC (34-28)
306 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i `;`s:scs_v39`;`SUC x`;`x`][is_scs_v39]
308 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
309 THEN REPEAT RESA_TAC;
313 MP_TAC(SET_RULE`i MOD k= SUC (SUC x) MOD k\/ ~(i MOD k= SUC (SUC x) MOD k)`)
318 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`SUC(SUC x):num`]
319 THEN THAYTHEL_TAC (34-26)[`SUC(x)`][dist]
320 THEN DICH_TAC (35-29)
322 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i`;`s:scs_v39`;`SUC x`;`SUC(SUC x)`][is_scs_v39]
324 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
325 THEN REPEAT RESA_TAC;
329 MP_TAC(ARITH_RULE`~(6=0)`)
331 THEN THAYTHES_TAC (34-9)[`i`;`SUC x`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT]
332 THEN ONCE_REWRITE_TAC[DIST_SYM]
334 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
336 THEN POP_ASSUM MP_TAC
341 MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
343 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
345 THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`SUC x`][DE_MORGAN_THM;]
346 THEN POP_ASSUM MP_TAC
347 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
353 THEN DICH_TAC (35-23)
355 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
356 THEN REPLICATE_TAC (49-36) (REMOVE_ASSUM_TAC)
357 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
358 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
360 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
361 THEN POP_ASSUM MP_TAC
362 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
363 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
365 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
366 THEN ASM_REWRITE_TAC[ADD1]
374 MP_TAC(REAL_ARITH`norm (v (SUC x)) = &2 \/ ~(norm ((v:num->real^3) (SUC x)) = &2)`)
376 THEN MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
378 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
380 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
386 THEN DICH_TAC (34-23)
388 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
389 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
390 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
391 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
393 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
394 THEN POP_ASSUM MP_TAC
395 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
396 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
398 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
399 THEN ASM_REWRITE_TAC[ADD1]
404 SUBGOAL_THEN`(!i. scs_diag k (SUC x) i
405 ==> scs_a_v39 s (SUC x) i < dist (v (SUC x),(v:num->real^3) i))`ASSUME_TAC
410 THEN THAYTHE_TAC (33-9)[`SUC x`;`i`]
411 THEN POP_ASSUM MP_TAC
412 THEN POP_ASSUM MP_TAC
419 SUBGOAL_THEN`azim (vec 0) (v (SUC x)) (v (SUC (SUC x))) ((v:num->real^3) (SUC x + k - 1)) = pi`ASSUME_TAC
425 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
426 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
427 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
428 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
430 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
431 THEN POP_ASSUM MP_TAC
432 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
433 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+1)`;`v`;`x+1`;`k`];
436 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC x)), v (SUC x + k - 1)}`
443 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 3 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)`)
445 THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
446 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
447 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)`]
448 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
449 THEN MATCH_DICH_TAC 1
450 THEN MRESAS_TAC WL_IN_V[`SUC (SUC x)`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
451 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
452 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
454 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];
460 SUBGOAL_THEN`(v:num->real^3) (SUC x) IN aff_gt {vec 0} {v (SUC (SUC x)), v (SUC x + k - 1)}`
466 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 1 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)/\ ~(6<=3)/\ 3 MOD 6=3`)
468 THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
469 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;`x`]
470 THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`w`;`FF`;`v'`][BB_VV_FUN_EQ]
472 THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
473 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x=x+i:num`]
474 THEN REWRITE_TAC[ARITH_RULE`3+x=x+3`]
475 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
477 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
479 THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;` FF`;`v x`;`v`;`x`;`k`][ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (l + x) | l = 1 \/ l = 2} = {v (1+x), v(2+x)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE`2+x=x+2`]
481 THEN MP_TAC(SET_RULE`v (x + 2) IN aff_gt {vec 0, v x} {v (x + 1)}
482 /\ aff_gt {vec 0, v x} {v (x + 1)} SUBSET aff_ge {vec 0, v x} {v (x + 1)}
483 ==> v (x + 2) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + 1)}`)
484 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
486 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
487 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`k-1+ SUC i=SUC(i+k-1)`]
489 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)/\ SUC (SUC x)= x+2`]
490 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
492 THEN MRESA_TAC WL_IN_V[`x`;`v:num->real^3`]
493 THEN MRESA_TAC WL_IN_V[`x+2`;`v:num->real^3`]
494 THEN MRESAL_TAC WL_IN_E[`x`;`v:num->real^3`][ADD1]
495 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v x`]
496 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
497 THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+1)`;`v (x+2)`][ADD1]
498 THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+2)`]
499 THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+1)`;`v (x+2)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ]
503 MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
504 THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x:num`]
507 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
511 MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`SUC x`][dist]
512 THEN POP_ASSUM MP_TAC
513 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
514 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE` SUC i+k-1=SUC(i+k-1)`]
515 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
517 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`1*k+x `;`s:scs_v39`;`SUC x:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
518 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`x MOD k `;`s:scs_v39`;`SUC x:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
520 THEN REWRITE_TAC[GSYM dist]
521 THEN ONCE_REWRITE_TAC[DIST_SYM]
522 THEN REWRITE_TAC[dist]
525 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
530 (********CASES 2*****)
534 SUBGOAL_THEN`norm((v:num->real^3) (x+k-1))= &2 \/ norm (v (x+k-1)- v (x))= &2` ASSUME_TAC;
536 REPLICATE_TAC 3 REMOVE_ASSUM_TAC
537 THEN ASSUME_TAC(ARITH_RULE`(x + k - 1) + k - 1=x + k - 1 + k - 1`)
538 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
539 THEN MRESAL_TAC BB_F_SUC_PRE[`s`;`v`;`x+k-1`][]
540 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
541 THEN THAYTHEL_ASM_TAC 0[`x+k-1`][]
542 THEN THAYTHE_TAC 0[`x+ k-1+k-1`]
543 THEN MP_TAC(REAL_ARITH`&2 <= norm (v (x+k-1) - v (x))
544 /\ &2 <= norm (v (x+k-1+k-1) - v (x+k-1))
545 ==> (&2 < norm (v (x+k-1) - v (x))
546 /\ &2 < norm (v (x+k-1+k-1) - v (x+k-1)))\/ norm (v (x+k-1) - v (x))= &2
547 \/ (norm ((v:num->real^3) (x+k-1+k-1) - v (x+k-1))= &2) `)
550 SUBGOAL_THEN`!i. ~(i MOD k = (x+k-1) MOD k) ==> scs_a_v39 s (x+k-1) i < dist (v (x+k-1),(v:num->real^3) i)`ASSUME_TAC
555 THEN MP_TAC(SET_RULE`i MOD k= x MOD k\/ ~(i MOD k= x MOD k)`)
559 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
560 THEN THAYTHE_TAC (36-26)[`x+k-1`]
561 THEN POP_ASSUM MP_TAC
562 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
564 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`1*k+x `;`s:scs_v39`;` x+k-1:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
565 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`x MOD k `;`s:scs_v39`;` x+k-1:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
566 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x`][is_scs_v39;dist]
568 THEN DICH_TAC (42-31)
571 MP_TAC(SET_RULE`i MOD k= (x+k-1+k-1) MOD k\/ ~(i MOD k= (x+k-1+k-1) MOD k)`)
576 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`(x+k-1+k-1):num`]
577 THEN ONCE_REWRITE_TAC[DIST_SYM]
578 THEN THAYTHEL_TAC (37-26)[`x+k-1+k-1`][dist]
580 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1+ 6 - 1)= 1*6+(x+ 6 - 1)/\ ~(6=0)`)
582 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`1*k+(x+k-1) `;`s:scs_v39`;` x+k-1+k-1:num`;`(1*k+(x+k-1)) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
583 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`(x+k-1) MOD k `;`s:scs_v39`;` x+k-1+k-1:num`;`x+k-1:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
584 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x+k-1+k-1`][is_scs_v39;dist]
586 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
587 THEN REPEAT RESA_TAC;
591 MP_TAC(ARITH_RULE`~(6=0)/\ 1+(x + 6- 1)= 1*6+x`)
593 THEN THAYTHES_TAC (38-9)[`i`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_MULT_ADD]
594 THEN ONCE_REWRITE_TAC[DIST_SYM]
596 THEN MP_TAC(ARITH_RULE`x+6-1=1+(x+6-2)`)
598 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
600 THEN MP_TAC(ARITH_RULE`x+6-1+6-1=1*6+(x+6-2)`)
602 THEN ASM_SIMP_TAC[MOD_MULT_ADD]
604 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
606 THEN POP_ASSUM MP_TAC
611 MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
613 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
615 THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`x+k-1`][DE_MORGAN_THM;]
616 THEN POP_ASSUM MP_TAC
617 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
623 THEN DICH_TAC (38-23)
625 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
626 THEN REPLICATE_TAC (52-39) (REMOVE_ASSUM_TAC)
627 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
628 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
630 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
631 THEN POP_ASSUM MP_TAC
632 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
633 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
634 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
636 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
637 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
639 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
640 THEN ASM_REWRITE_TAC[ADD1]
648 MP_TAC(REAL_ARITH`norm (v (x+k-1)) = &2 \/ ~(norm ((v:num->real^3) (x+k-1)) = &2)`)
650 THEN MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
652 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
654 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
660 THEN DICH_TAC (37-23)
662 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
663 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
664 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
665 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
667 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
668 THEN POP_ASSUM MP_TAC
669 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
670 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
671 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
673 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
674 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
676 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
677 THEN ASM_REWRITE_TAC[ADD1]
682 SUBGOAL_THEN`(!i. scs_diag k (x+k-1) i
683 ==> scs_a_v39 s (x+k-1) i < dist (v (x+k-1),(v:num->real^3) i))`ASSUME_TAC
688 THEN THAYTHE_TAC (36-9)[`x+k-1`;`i`]
689 THEN POP_ASSUM MP_TAC
690 THEN POP_ASSUM MP_TAC
697 SUBGOAL_THEN`azim (vec 0) ((v:num->real^3) (x + k - 1)) (v x) (v (x + k - 1+k-1)) = pi`ASSUME_TAC
702 THEN REMOVE_ASSUM_TAC
703 THEN REMOVE_ASSUM_TAC
704 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
707 THEN ASM_REWRITE_TAC[]
709 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]
713 THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
714 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
715 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
717 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
718 THEN POP_ASSUM MP_TAC
719 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
720 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
721 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
723 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
724 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
725 THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`][ARITH_RULE`(x + k - 1) + 1= SUC (x + k - 1)`];
729 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) x, v (x + k - 1 + k - 1)}`
736 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1+6-1) MOD 6= 3 MOD 6)/\ ~((6-1+6-1) MOD 6= 0 MOD 6)`)
738 THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
739 THEN MATCH_DICH_TAC 0
740 THEN MRESAS_TAC WL_IN_V[`x+k-1+k-1`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
741 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
742 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
744 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];
749 SUBGOAL_THEN`(v:num->real^3) (x + k - 1) IN aff_gt {vec 0} {v x, v (x + k - 1 + k - 1)}`
755 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ (0 MOD 6= (3+3) MOD 6)/\ ~(1 MOD 6= 3 MOD 6)/\ ~(6<=3)/\ ~((3+1) MOD 6= (6-1) MOD 6)`)
757 THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
758 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v (x+3)`;`v`;`x+3`]
759 THEN MRESA_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ[`V`;`E`;`w`;`FF`;`v'`]
760 THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`v'`;`FF`;`w`][BB_VV_FUN_EQ;Local_lemmas.LUNAR_COMM;]
761 THEN POP_ASSUM MP_TAC
762 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
763 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v x`;`v`;`x`;`k`]
765 THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
766 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x+3=x+i+3:num`]
767 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
768 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
770 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
771 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+3=3+i:num`]
772 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
774 THEN ASM_REWRITE_TAC[ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (x + 3 + l) | l = 1 \/ l = 2} = {v (x+3+1), v(x+3+2)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE` 3+2=6-1`]
775 THEN MP_TAC(ARITH_RULE`x+6-1+6-1= 1*6+(x+3+1)`)
777 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + x + 3 + 1`;`v:num->real^3`;`(1 * k + x + 3 + 1) MOD k:num`][MOD_REFL;MOD_MULT_ADD]
778 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(x + 3 + 1) MOD k`;`v:num->real^3`;`(x + 3 + 1):num`][MOD_REFL;MOD_MULT_ADD]
780 THEN MP_TAC(SET_RULE`v (x + 3+1) IN aff_gt {vec 0, v x} {v (x +k- 1)}
781 /\ aff_gt {vec 0, v x} {v (x +k- 1)} SUBSET aff_ge {vec 0, v x} {v (x + k-1)}
782 ==> v (x + 3+1) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + k-1)}`)
783 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
785 THEN DICH_TAC (59-37)
787 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
788 THEN MRESA_TAC WL_IN_V[`x+3+1`;`v:num->real^3`]
789 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`]
790 THEN MRESAL_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v (x+k-1)`][GSYM ADD1]
792 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
794 THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+k-1)`;`v (x+3+1)`][ADD1]
795 THEN MRESAL_TAC WL_IN_E[`x+k-1`;`v:num->real^3`][]
797 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
799 THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+3+1)`]
800 THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+k-1)`;`v (x+3+1)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ];
802 MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`x+k-1`][dist]
807 THEN POP_ASSUM MP_TAC
808 THEN REWRITE_TAC[GSYM dist]
810 THEN ONCE_REWRITE_TAC[DIST_SYM]
816 MRESA_TAC BB_F_SUC_PRE[`s`;`v:num->real^3`;`x`]
817 THEN MP_TAC Axjrpnc.DIST_LE_2h0_IN_CASES_6
819 THEN THAYTHEL_ASM_TAC 0[`x`][GSYM dist]
820 THEN THAYTHEL_TAC 0[`x+k-1`][GSYM dist]
821 THEN POP_ASSUM MP_TAC
823 THEN ONCE_REWRITE_TAC[DIST_SYM]
826 SUBGOAL_THEN` cstab <= dist (v (SUC x),(v:num->real^3) (x + k - 1))`ASSUME_TAC
829 MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(1 MOD 6=6 MOD 6)/\ (x+6-1)+1=x+6/\ ~(1 MOD 6= (6-1) MOD 6)/\ ~(6=0)/\ ~((2) MOD 6= (6-1) MOD 6)`)
831 THEN THAYTHES_TAC (41-10)[`SUC x`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`(i+1)+1= i+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
832 THEN POP_ASSUM MP_TAC
838 THEN MRESAL_TAC JKQEWGV3[`s`;`v`;`v'`;`w`][LET_DEF;LET_END_DEF;];
843 THEN REMOVE_ASSUM_TAC
846 THEN THAYTHE_TAC 0[`s`;`v`;`x`;`k`]
848 THEN DICH_TAC (35-30)
849 THEN DICH_TAC (34-29)
853 THEN REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;ADD1]
854 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x)`;`v`;`x`;`k`]
872 let check_completeness_claimA_concl =
873 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)