text_formalization/local/JCYFMRP.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Jcyfmrp = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89
  90
  91
  92
  93 let J_EMPY_CASES_A_EQ_2=prove(`(!i. scs_a_v39 s i (SUC i) = &2)
  94   /\ is_scs_v39 s
  95 ==>  scs_J_v39 s i= {}`,
  96 STRIP_TAC
  97 THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s i x) \/ (scs_J_v39 s i= {})`)
  98 THEN RESA_TAC
  99 THEN ASM_TAC
 100 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 101 THEN REPEAT RESA_TAC
 102 THEN THAYTHEL_ASM_TAC(21-19)[`i`;`x`][]
 103 THEN THAYTHEL_ASM_TAC (23-18)[`i`;`x`][]
 104 THENL[
 105 DICH_TAC 4
 106 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`x`;`s`;`i`;`SUC i`][is_scs_v39]
 107 THEN POP_ASSUM MP_TAC
 108 THEN MP_TAC Geomdetail.db_t0_sq8
 109 THEN REWRITE_TAC[sqrt8]
 110 THEN REAL_ARITH_TAC;
 111
 112 DICH_TAC 4
 113 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`x`;`s`;`SUC x`;`x`][is_scs_v39]
 114 THEN POP_ASSUM MP_TAC
 115 THEN MP_TAC Geomdetail.db_t0_sq8
 116 THEN REWRITE_TAC[sqrt8]
 117 THEN REAL_ARITH_TAC]);;
 118
 119 let DIST_EDGE_LE_CSTAB_CASE_LE3=prove(`3< scs_k_v39 s /\ BBs_v39 s v /\ is_scs_v39 s ==> dist(v i, v (SUC i))<= cstab`,
 120 REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
 121 THEN REPEAT RESA_TAC
 122 THEN THAYTHE_TAC (24-21)[`i`]
 123 THEN THAYTHE_TAC (24-3)[`i`;`SUC i`]
 124 THEN DICH_TAC 0
 125 THEN DICH_TAC 1
 126 THEN REAL_ARITH_TAC);;
 127
 128
 129 let J_EMPY_CASES_A_EQ_2_V1=prove(
 130 `scs_a_v39 s i (SUC i) = &2/\ scs_a_v39 s (SUC i) (SUC(SUC i)) = &2
 131   /\ is_scs_v39 s
 132 ==>  scs_J_v39 s (SUC i)= {}`,
 133 STRIP_TAC
 134 THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s (SUC i) x) \/ (scs_J_v39 s (SUC i)= {})`)
 135 THEN RESA_TAC
 136 THEN ASM_TAC
 137 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 138 THEN REPEAT RESA_TAC
 139 THEN THAYTHEL_ASM_TAC(21-19)[`SUC i`;`x`][]
 140 THEN THAYTHEL_ASM_TAC (23-18)[`SUC i`;`x`][]
 141 THENL[
 142 DICH_TAC 4
 143 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC i`;`x`;`s`;`SUC i`;`SUC (SUC i)`][is_scs_v39]
 144 THEN POP_ASSUM MP_TAC
 145 THEN MP_TAC Geomdetail.db_t0_sq8
 146 THEN REWRITE_TAC[sqrt8]
 147 THEN REAL_ARITH_TAC;
 148
 149 DICH_TAC 4
 150 THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s==> ~(scs_k_v39 s= 0)`)
 151 THEN RESA_TAC
 152 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`scs_k_v39 s`;`i`;`x`;`1`][ARITH_RULE`1+x= SUC x`]
 153 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(SUC i)`;`x`;`s`;`SUC i`;`i`][is_scs_v39]
 154 THEN POP_ASSUM MP_TAC
 155 THEN MP_TAC Geomdetail.db_t0_sq8
 156 THEN REWRITE_TAC[sqrt8]
 157 THEN REAL_ARITH_TAC]);;
 158
 159
 160
 161
 162 let SCS_M_LE_1= prove_by_refinement(` CARD (scs_M s) <= 1 /\ is_scs_v39 s
 163 ==> ?p. (!i. ~(i MOD scs_k_v39 s=p MOD scs_k_v39 s)==> scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
 164 [
 165 STRIP_TAC
 166 THEN POP_ASSUM (fun th-> MP_TAC th
 167 THEN ASSUME_TAC th)
 168 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 169 THEN RESA_TAC
 170 THEN DICH_TAC (21)
 171 THEN REWRITE_TAC[scs_M]
 172 THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
 173 THEN SUBGOAL_THEN`FINITE
 174       {i | i < scs_k_v39 s /\
 175            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 176
 177 MATCH_MP_TAC FINITE_SUBSET
 178 THEN EXISTS_TAC`0..6`
 179 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 180 THEN GEN_TAC
 181 THEN DICH_TAC(20-3)
 182 THEN ARITH_TAC;
 183
 184
 185 ABBREV_TAC`k=scs_k_v39 s`
 186 THEN RESA_TAC;
 187
 188 MRESA_TAC CARD_EQ_0[`{i | i < scs_k_v39 s /\
 189         (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 190 THEN POP_ASSUM MP_TAC
 191 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
 192 THEN STRIP_TAC
 193 THEN EXISTS_TAC `0`
 194 THEN REPEAT GEN_TAC
 195 THEN STRIP_TAC
 196 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 197 THEN RESA_TAC
 198 THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
 199 THEN DICH_TAC 0
 200 THEN DICH_TAC 0
 201 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 202 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 203 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 204 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 205 THEN THAYTHES_TAC (30-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
 206 THEN POP_ASSUM MP_TAC
 207 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 208 THEN REAL_ARITH_TAC;
 209
 210
 211 MRESA_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`{i | i < k /\
 212            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 213 THEN POP_ASSUM MP_TAC
 214 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
 215 THEN STRIP_TAC
 216 THEN EXISTS_TAC`x:num`
 217 THEN GEN_TAC
 218 THEN STRIP_TAC
 219 THEN THAYTHEL_ASM_TAC 1[`x`][]
 220 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 221 THEN RESA_TAC
 222 THEN DICH_TAC 5
 223 THEN ASM_SIMP_TAC[MOD_LT]
 224 THEN STRIP_TAC
 225 THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
 226 THEN DICH_TAC 0
 227 THEN DICH_TAC 0
 228 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 229 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 230 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 231 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 232 THEN THAYTHES_TAC (32-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
 233 THEN POP_ASSUM MP_TAC
 234 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 235 THEN REAL_ARITH_TAC]);;
 236
 237
 238
 239
 240 let JCYFMRP_concl = `
 241 main_nonlinear_terminal_v11
 242 ==>
 243 (!s (v:num->real^3).
 244   3< scs_k_v39 s/\
 245   is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
 246   (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
 247   CARD (scs_M s) <= 1 /\
 248   (!i. scs_a_v39 s i (SUC i) = &2) /\
 249   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
 250   (?i. dist(v i, v (i+1)) = &2))`;;
 251
 252
 253
 254
 255
 256 let JCYFMRP=prove_by_refinement(  JCYFMRP_concl,
 257 [
 258 MP_TAC Cuxvzoz.CUXVZOZ
 259 THEN STRIP_TAC
 260 THEN STRIP_TAC
 261 THEN REWRITE_TAC[IN;scs_generic]
 262 THEN REPEAT GEN_TAC
 263 THEN ABBREV_TAC`k=scs_k_v39 s`
 264 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
 265 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
 266 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 267 THEN STRIP_TAC
 268 THEN MP_TAC(SET_RULE`?i. dist (v i,v (i + 1)) = &2\/ ~(?i. dist ((v:num->real^3) i,v (i + 1)) = &2)`)
 269 THEN STRIP_TAC
 270 THEN ASM_REWRITE_TAC[]
 271 ;
 272
 273
 274 EXISTS_TAC`i:num`
 275 THEN ASM_REWRITE_TAC[]
 276 ;
 277
 278 DICH_TAC 1
 279 THEN DICH_TAC 0
 280 THEN REWRITE_TAC[NOT_EXISTS_THM]
 281 THEN REPEAT STRIP_TAC
 282 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 283 THEN SUBGOAL_THEN`!i. &2< dist((v:num->real^3) i, v (SUC i))`ASSUME_TAC
 284 ;
 285
 286
 287 GEN_TAC
 288 THEN MATCH_MP_TAC(REAL_ARITH`a<=b /\ ~(b= a)==> a<b`)
 289 THEN MP_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2
 290 THEN REWRITE_TAC[GSYM dist]
 291 THEN RESA_TAC
 292 THEN ASM_REWRITE_TAC[ADD1];
 293
 294
 295
 296 SUBGOAL_THEN`!i. norm ((v:num->real^3) i)= &2` ASSUME_TAC
 297 ;
 298
 299
 300
 301 GEN_TAC
 302 THEN MP_TAC(REAL_ARITH`norm ((v:num->real^3) i)= &2\/ ~(norm ((v:num->real^3) i)= &2)`)
 303 THEN RESA_TAC
 304 THEN DICH_TAC 2
 305 THEN MRESA_TAC J_EMPY_CASES_A_EQ_2[`s`;`i`]
 306 THEN DICH_TAC 0
 307 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 308 THEN STRIP_TAC
 309 THEN STRIP_TAC
 310 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
 311 THEN MP_TAC Local_lemmas.CVLF_LF_F
 312 THEN RESA_TAC
 313 THEN DICH_TAC 0
 314 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 315 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
 316 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
 317 THEN RESA_TAC
 318 THEN POP_ASSUM MP_TAC
 319 THEN REWRITE_TAC[NOT_EXISTS_THM]
 320 THEN STRIP_TAC
 321 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) i) V' E')` ASSUME_TAC;
 322
 323
 324
 325 REPEAT RESA_TAC
 326 ;
 327
 328 SUBGOAL_THEN`!i'. ~(i' MOD k = i MOD k) ==> scs_a_v39 s i i' < dist ((v:num->real^3) i,v i')`ASSUME_TAC;
 329
 330
 331
 332 REPEAT STRIP_TAC
 333 THEN MP_TAC(SET_RULE`i' MOD k= SUC i MOD k\/ ~(i' MOD k= SUC i MOD k)`)
 334 THEN RESA_TAC
 335 ;
 336
 337
 338 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC i:num`]
 339 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`i' `;`s:scs_v39`;`i`;`SUC i`][]
 340 ;
 341
 342
 343
 344 MP_TAC(SET_RULE`SUC i' MOD k= i MOD k\/ ~(SUC i' MOD k= i MOD k)`)
 345 THEN RESA_TAC
 346 ;
 347
 348
 349 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`SUC i':num`]
 350 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i`;`i' `;`s:scs_v39`;`SUC i'`;`i'`][]
 351 THEN ASM_TAC
 352 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 353 THEN REPEAT RESA_TAC
 354 THEN ONCE_REWRITE_TAC[DIST_SYM]
 355 THEN ASM_REWRITE_TAC[];
 356
 357
 358
 359 THAYTHEL_TAC (27-13)[`i`;`i'`][scs_diag]
 360 THEN DICH_TAC 0
 361 THEN DICH_TAC 0
 362 THEN REAL_ARITH_TAC;
 363
 364
 365
 366 MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`i:num`][]
 367 ;
 368
 369
 370
 371 MP_TAC SCS_M_LE_1
 372 THEN RESA_TAC
 373 THEN SUBGOAL_THEN`!i. ~(i MOD k= p MOD k )/\ ~(i MOD k= SUC p MOD k )
 374 ==> pi / &2 < azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1))`
 375 ASSUME_TAC
 376 ;
 377
 378
 379 GEN_TAC
 380 THEN STRIP_TAC
 381 THEN MP_TAC SYNQIWN
 382 THEN RESA_TAC
 383 THEN POP_ASSUM MATCH_MP_TAC
 384 THEN EXISTS_TAC`s:scs_v39`
 385 THEN ASM_REWRITE_TAC[]
 386 THEN REPEAT STRIP_TAC;
 387
 388
 389
 390 MATCH_MP_TAC(GEN_ALL(REAL_ARITH`a<=b/\ b<=c ==> a<=c`))
 391 THEN EXISTS_TAC`scs_b_v39 s i (SUC i)`
 392 THEN ASM_TAC
 393 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
 394 THEN REPEAT RESA_TAC
 395 THEN MATCH_DICH_TAC 2
 396 THEN ASM_REWRITE_TAC[];
 397
 398
 399
 400 MATCH_MP_TAC(GEN_ALL(REAL_ARITH`a<=b/\ b<=c ==> a<=c`))
 401 THEN EXISTS_TAC`scs_b_v39 s (i+k-1) (SUC (i+k-1))`
 402 THEN MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= 1*k+i/\ ~(k<=3)/\ ~(k=0)`)
 403 THEN RESA_TAC
 404 THEN ASM_TAC
 405 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
 406 THEN REPEAT RESA_TAC
 407 ;
 408
 409
 410
 411 MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`1*k+i `;`s:scs_v39`;`i+k-1`;`(1*k+i)MOD k`][MOD_REFL;MOD_MULT_ADD]
 412 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`i MOD k `;`s:scs_v39`;`i+k-1`;`i`][MOD_REFL;MOD_MULT_ADD]
 413 THEN ONCE_REWRITE_TAC[DIST_SYM]
 414 THEN ASM_REWRITE_TAC[];
 415
 416
 417
 418 MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`1*k+i `;`s:scs_v39`;`i+k-1`;`(1*k+i)MOD k`][MOD_REFL;MOD_MULT_ADD]
 419 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i+k-1`;`i MOD k `;`s:scs_v39`;`i+k-1`;`i`][MOD_REFL;MOD_MULT_ADD]
 420 THEN THAYTHE_TAC (28-21)[`i+k-1`]
 421 THEN MATCH_DICH_TAC 0
 422 THEN DICH_TAC (27-22)
 423 THEN ASM_REWRITE_TAC[CONTRAPOS_THM]
 424 THEN STRIP_TAC
 425 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`i+k-1`;`p`;`k`][MOD_MULT_ADD];
 426
 427
 428
 429 MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= i+ 1*k+0/\ ~(k<=3)/\ ~(k=0)/\ k-1<k
 430 /\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(1=k-1)/\ ~(2=k-1)/\ ~(1=0)`)
 431 THEN RESA_TAC
 432 THEN THAYTHES_TAC (31-14)[`SUC i`;`i+k-1`;][scs_diag;ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT;MOD_MULT_ADD]
 433 THEN POP_ASSUM MP_TAC
 434 THEN REAL_ARITH_TAC;
 435
 436
 437
 438 MP_TAC(SET_RULE` (!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
 439           ==> pi<= azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1))) \/ ~(!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
 440           ==> pi<= azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1))) `)
 441 THEN RESA_TAC
 442 ;
 443
 444
 445
 446
 447
 448 SUBGOAL_THEN`!i. ~(i MOD k = p MOD k) /\ ~(i MOD k = SUC p MOD k)
 449           ==>  azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1))= pi`ASSUME_TAC
 450 ;
 451
 452
 453
 454 REPEAT STRIP_TAC
 455 THEN THAYTHE_TAC 2[`i`]
 456 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`]
 457 THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`]
 458 THEN MRESA_TAC WL_IN_V[`i+k-1`;`v:num->real^3`]
 459 THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (i)`;`v`;`i`;`k`]
 460 THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`]
 461 THEN THAYTHE_TAC 0[`v (i+k-1)`]
 462 THEN DICH_TAC 0
 463 THEN DICH_TAC (27-22)
 464 THEN REWRITE_TAC[ADD1]
 465 THEN REAL_ARITH_TAC;
 466
 467
 468 SUBGOAL_THEN`(0..(k-1)) DELETE p MOD k DELETE SUC p MOD k SUBSET{i | i < k /\ azim (vec 0) (v i) (v (SUC i)) ((v:num->real^3) (i + k - 1)) = pi}`
 469 ASSUME_TAC
 470 ;
 471
 472
 473 REWRITE_TAC[SUBSET;IN_ELIM_THM;DELETE;IN_NUMSEG;]
 474 THEN REPEAT RESA_TAC
 475 THEN MP_TAC(ARITH_RULE`3<k==> (x<=k-1<=> x<k )`)
 476 THEN RESA_TAC
 477 THEN THAYTHES_TAC 5[`x:num`][MOD_LT;];
 478
 479
 480 MP_TAC(ARITH_RULE`3<k==> ~(k=0 )/\ 1<k`)
 481 THEN RESA_TAC
 482 THEN MRESA_TAC DIVISION[`p`;`k`]
 483 THEN MP_TAC(ARITH_RULE`3<k/\ p MOD k< k ==> p MOD k<=k-1/\ (k-1+1)-0=k`)
 484 THEN RESA_TAC
 485 THEN MRESAS_TAC Hypermap.CARD_MINUS_ONE[`0..(k-1)`;`p MOD k`][FINITE_NUMSEG;IN_NUMSEG;ARITH_RULE`0<=a`;CARD_NUMSEG]
 486 THEN MP_TAC(ARITH_RULE`3<k/\ k = CARD ((0..k - 1) DELETE p MOD k) + 1 ==>  CARD ((0..k - 1) DELETE p MOD k) =k-1`)
 487 THEN RESA_TAC
 488 THEN POP_ASSUM MP_TAC
 489 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 490 THEN RESA_TAC
 491 THEN SUBGOAL_THEN`SUC p MOD k IN (0..k - 1) DELETE p MOD k`ASSUME_TAC
 492 ;
 493
 494
 495 ASM_REWRITE_TAC[DELETE;IN_ELIM_THM;IN_NUMSEG]
 496 THEN MRESA_TAC DIVISION[`SUC p`;`k`]
 497 THEN MP_TAC(ARITH_RULE`3<k/\ SUC p MOD k< k ==> SUC p MOD k<=k-1/\ 0<= SUC p MOD k/\ 1<k`)
 498 THEN RESA_TAC
 499 THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ];
 500
 501
 502
 503
 504 MRESAS_TAC Hypermap.CARD_MINUS_ONE[`(0..(k-1)) DELETE p MOD k`;`SUC p MOD k`][FINITE_NUMSEG;IN_NUMSEG;ARITH_RULE`0<=a`;CARD_NUMSEG;FINITE_DELETE]
 505 THEN MP_TAC(ARITH_RULE`3<k/\ k - 1 = CARD ((0..k - 1) DELETE p MOD k DELETE SUC p MOD k) + 1 ==>  CARD ((0..k - 1) DELETE p MOD k DELETE SUC p MOD k) =k-2`)
 506 THEN RESA_TAC
 507 THEN POP_ASSUM MP_TAC
 508 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 509 THEN RESA_TAC
 510 ;
 511
 512
 513 SUBGOAL_THEN`FINITE
 514       {i | i < k /\ azim (vec 0) ((v:num->real^3) i) (v (SUC i)) (v (i + k - 1)) = pi}`ASSUME_TAC
 515 ;
 516
 517
 518 MATCH_MP_TAC FINITE_SUBSET
 519 THEN EXISTS_TAC`0..k`
 520 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 521 THEN ARITH_TAC;
 522
 523
 524 MRESA_TAC CARD_SUBSET[`(0..k - 1) DELETE p MOD k DELETE SUC p MOD k`;`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`]
 525 THEN MRESAL_TAC Aursipd.AURSIPD[`s`;`v`][scs_generic;IN;scs_is_str]
 526 THEN POP_ASSUM MP_TAC
 527 THEN POP_ASSUM MP_TAC
 528 THEN DICH_TAC (32-5)
 529 THEN ABBREV_TAC`a= CARD {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}`
 530 THEN ARITH_TAC;
 531
 532
 533
 534 DICH_TAC 5
 535 THEN POP_ASSUM MP_TAC
 536 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<=b)<=> b<a`]
 537 THEN STRIP_TAC
 538 THEN STRIP_TAC;
 539
 540
 541
 542 DICH_TAC 23
 543 THEN RESA_TAC
 544 THEN THAYTHEL_TAC 0[`s`;`FF`;`k`;`i`;`v`][scs_generic;GSYM ADD1];
 545
 546
 547
 548 THAYTHES_TAC (22-14)[`SUC i`;`i+k-1`][Ocbicby.scs_diag_2]
 549 THEN ONCE_REWRITE_TAC[DIST_SYM]
 550 THEN POP_ASSUM MP_TAC
 551 THEN REWRITE_TAC[cstab]
 552 THEN REAL_ARITH_TAC;
 553
 554
 555 STRIP_TAC
 556 ;
 557
 558
 559
 560 REPEAT RESA_TAC
 561 THEN THAYTHES_TAC (24-14)[`i'`;`j`][Ocbicby.scs_diag_2]
 562 THEN POP_ASSUM MP_TAC
 563 THEN POP_ASSUM MP_TAC
 564 THEN REAL_ARITH_TAC;
 565
 566
 567
 568 STRIP_TAC;
 569
 570
 571
 572 ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
 573 THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v i`;`v`;`i`;`k`][GSYM ADD1];
 574
 575
 576
 577 STRIP_TAC;
 578
 579
 580
 581 ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
 582 THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v i`;`v`;`i`;`k`][GSYM ADD1]
 583 THEN THAYTHE_TAC (24-18)[`i`];
 584
 585 STRIP_TAC
 586 ;
 587
 588
 589 MATCH_DICH_TAC (22-17)
 590 THEN ASM_REWRITE_TAC[]
 591 ;
 592
 593
 594 STRIP_TAC
 595 ;
 596
 597 MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
 598 THEN MRESAS_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i+k-1`][Imjxphr.EQ_W_L_IN_BBS;GSYM dist]
 599 ;
 600
 601
 602
 603 MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
 604 THEN MRESAL_TAC DIST_EDGE_LE_CSTAB_CASE_LE3[`s`;`v`;`i+k-1`][Imjxphr.EQ_W_L_IN_BBS;GSYM dist]
 605 ;
 606
 607
 608 ]);;
 609
 610
 611
 612
 613
 614
 615  end;;
 616
 617
 618 (*
 619 let check_completeness_claimA_concl =
 620   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 621 *)
 622
 623
 624
 625