text_formalization/local/TFITSKC.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 Tfitskc = 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 Aursipd;;
  89 open Cuxvzoz;;
  90 open Rrcwnsj;;
  91
  92
  93
  94 let SCS_DIAG_A_LE_DIST=prove(`(!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j))
  95 ==>  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j < dist(v i, (v:num->real^3) j)))`,
  96 REPEAT RESA_TAC
  97 THEN THAYTHE_TAC 1[`i`;`j`]
  98 THEN ASM_TAC
  99 THEN REAL_ARITH_TAC);;
 100
 101
 102 let DIST_EQ_2_IMP_A_EQ_2=prove(`is_scs_v39 s/\ BBs_v39 s v /\ dist (v i,v (SUC i)) = &2
 103 ==> scs_a_v39 s i (SUC i) = &2`,
 104 REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
 105 THEN RESA_TAC
 106 THEN ABBREV_TAC`k= scs_k_v39 s`
 107 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k`;`SUC i MOD k `;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;MOD_MULT_ADD;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;is_scs_v39]
 108 THEN THAYTHES_TAC (26-14)[`i MOD k`;`SUC i MOD k`][DIVISION;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;Qknvmlb.SUC_MOD_NOT_EQ]
 109 THEN DICH_TAC 0
 110 THEN THAYTHE_TAC 4[`i`;`SUC i`]
 111 THEN DICH_TAC 1
 112 THEN REAL_ARITH_TAC);;
 113
 114
 115 let SCS_DIAG_2=prove(`3<k==> scs_diag k i (SUC (SUC i))`,
 116 STRIP_TAC
 117 THEN REWRITE_TAC[scs_diag;ADD1]
 118 THEN MP_TAC(ARITH_RULE`3<k==> (i+1)+1=i+2/\ (i+2)+1=i+3/\ ~(k=0)/\ k-1<k
 119 /\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)`)
 120 THEN RESA_TAC
 121 THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
 122 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 123 THEN RESA_TAC
 124 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]);;
 125
 126
 127 let TFITSKCv1_concl = `
 128 main_nonlinear_terminal_v11
 129 ==> (!s (v:num->real^3) i.
 130 (!i'. ~scs_J_v39 s (SUC (SUC i)) i')/\
 131  scs_a_v39 s (SUC (SUC i)) (SUC(SUC(SUC i)))< scs_b_v39 s (SUC (SUC i)) (SUC(SUC(SUC i))) /\
 132 3< scs_k_v39 s  /\
 133 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
 134   scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0 /\
 135   dist(v i,v (i+1)) = &2 /\ dist(v i,v (i+1))< scs_b_v39 s i (i+1) /\
 136   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) ==>
 137   dist(v (i+1),v(i+2)) = &2)`;;
 138
 139
 140
 141
 142
 143
 144 let TFITSKCv1=prove_by_refinement(  TFITSKCv1_concl,
 145 [
 146 STRIP_TAC
 147 THEN REWRITE_TAC[IN;GSYM ADD1;ARITH_RULE`i+2=SUC(SUC i)`;scs_generic]
 148 THEN REPEAT GEN_TAC
 149 THEN STRIP_TAC
 150 THEN ABBREV_TAC`k=scs_k_v39 s`
 151 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
 152 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
 153 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 154 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 155 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`]
 156 THEN MP_TAC Local_lemmas.CVLF_LF_F
 157 THEN RESA_TAC
 158 THEN MP_TAC SCS_DIAG_A_LE_DIST
 159 THEN RESA_TAC
 160 THEN MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`][ARITH_RULE`SUC(i+1)=i+2`;GSYM dist]
 161 THEN MP_TAC(REAL_ARITH`&2 <= dist (v (SUC i),v (SUC(SUC i)))
 162 ==> dist (v (SUC i),v (SUC(SUC i))) = &2 \/ &2 < dist (v (SUC i),(v:num->real^3) (SUC(SUC i)))`)
 163 THEN RESA_TAC
 164 THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`]
 165 THEN MRESA_TAC WL_IN_V[`SUC i`;`v:num->real^3`]
 166 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC i)`;`v`;`SUC i`;`k`]
 167 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (SUC i)`][GSYM ADD1]
 168 THEN THAYTHE_TAC 0[`v i`]
 169 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) (v i) <= pi
 170 ==> azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) (v i) = pi
 171 \/ azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) ((v:num->real^3) i) < pi`)
 172 THEN RESA_TAC;
 173
 174
 175
 176 MP_TAC Jcyfmrp.J_EMPY_CASES_A_EQ_2_V1
 177 THEN DICH_TAC 0
 178 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 179 THEN STRIP_TAC
 180 THEN MP_TAC DIST_EQ_2_IMP_A_EQ_2
 181 THEN RESA_TAC
 182 THEN STRIP_TAC
 183 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 184 THEN MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
 185 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
 186 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
 187 THEN RESA_TAC
 188 THEN POP_ASSUM MP_TAC
 189 THEN REWRITE_TAC[NOT_EXISTS_THM]
 190 THEN STRIP_TAC
 191 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC i)) V' E')` ASSUME_TAC;
 192
 193
 194
 195 REPEAT RESA_TAC
 196 ;
 197
 198
 199
 200 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC i)), v (i)}`
 201 ASSUME_TAC;
 202
 203
 204 MRESAS_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`][BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 205 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC(SUC i))`;`v i`;`V`]
 206 THEN THAYTHES_TAC 0[`v (SUC(SUC i))`;`v i`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
 207 THEN MATCH_DICH_TAC 0
 208 THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
 209 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 210 THEN RESA_TAC
 211 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 2<k/\ ~(2=0)`)
 212 THEN RESA_TAC
 213 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT];
 214
 215
 216
 217
 218
 219 SUBGOAL_THEN`(v:num->real^3) (SUC i) IN aff_gt {vec 0} {v (SUC (SUC i)), v (i)}`
 220 ASSUME_TAC;
 221
 222
 223
 224
 225 MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v ((SUC i))`;`v i`;`V`]
 226 THEN THAYTHES_TAC 0[`v (SUC i)`;`v i`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1]
 227 THEN POP_ASSUM MP_TAC
 228 THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
 229 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 230 THEN RESA_TAC
 231 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 1<k/\ 2<k /\ ~(1=0)/\ ~(2=1)`)
 232 THEN RESA_TAC
 233 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 234 THEN MRESAL_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`][]
 235 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC (SUC i))`;`v (SUC i)`;`V`]
 236 THEN THAYTHES_TAC 0[`(v:num->real^3) (SUC(SUC i))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2`;MOD_LT]
 237 THEN POP_ASSUM MP_TAC
 238 THEN ASM_REWRITE_TAC[ARITH_RULE`i+2=(i+1)+1`;GSYM ADD1]
 239 THEN REPEAT STRIP_TAC
 240 THEN DICH_TAC 1
 241 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 242 THEN RESA_TAC
 243 THEN DICH_TAC (45-3)
 244 THEN REWRITE_TAC[GSYM ADD1;generic]
 245 THEN STRIP_TAC
 246 THEN MRESAL_TAC WL_IN_E[`SUC i`;`v:num->real^3`][]
 247 THEN THAYTHE_TAC 1[`v (SUC i)`;`v(SUC(SUC i))`;`v i`]
 248 THEN MRESAS_TAC Polar_fan.GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE[`v i`;`v (SUC i)`;`v(SUC(SUC i))`;][]
 249 THEN DICH_TAC 0
 250 THEN MRESA_TAC th3[`vec 0:real^3`;`v (SUC(SUC i))`;`v i`]
 251 THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC i)`;`vec 0:real^3`;`v i`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1]
 252 THEN POP_ASSUM MP_TAC
 253 THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
 254 THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 255 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 256 THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC i)`;`vec 0:real^3`;`v (SUC(SUC i))`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`(i+1)+1=i+2`;MOD_LT;Ocbicby.MOD_EQ_MOD_SHIFT]
 257 THEN POP_ASSUM MP_TAC
 258 THEN ASM_REWRITE_TAC[ARITH_RULE`i+2=(i+1)+1`;GSYM ADD1]
 259 THEN STRIP_TAC
 260 THEN STRIP_TAC
 261 THEN MRESAL_TAC Wrgcvdr_cizmrrh.AFF_GE_TO_AFF_GT2_GE1[`v i`;`vec 0:real^3`;`v (SUC(SUC i))`][UNION;IN_ELIM_THM]
 262 THEN REPEAT STRIP_TAC
 263 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 264 THEN ASM_REWRITE_TAC[];
 265
 266
 267
 268
 269 MRESAS_TAC NUXCOEAv2[`s`;`k`;`v`;`SUC i`;`i`][ARITH_RULE`SUC i + k - 1=SUC (i + k - 1)`];
 270
 271
 272
 273
 274 MRESAL_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`][Fnjlbxs.in_ball_annulus]
 275 THEN MP_TAC(REAL_ARITH`&2 <= norm (v (SUC(SUC i)))
 276 ==>  norm (v (SUC(SUC i)))= &2\/ &2 < norm ((v:num->real^3) (SUC(SUC i)))`)
 277 THEN RESA_TAC;
 278
 279
 280
 281
 282
 283 MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
 284 THEN MP_TAC SYNQIWN
 285 THEN RESA_TAC
 286 THEN THAYTHES_TAC 0[`s`;`v`;`SUC i`;`k`][Imjxphr.EQ_W_L_IN_BBS;ARITH_RULE`SUC i + k - 1=SUC( i + k - 1)`]
 287 THEN DICH_TAC 0
 288 THEN ONCE_REWRITE_TAC[DIST_SYM]
 289 THEN ASM_REWRITE_TAC[]
 290 THEN SUBGOAL_THEN`dist (v (SUC (SUC i)),(v:num->real^3) (SUC i)) <= &2 * h0`ASSUME_TAC;
 291
 292
 293
 294 REPLICATE_TAC (31-1) (POP_ASSUM MP_TAC)
 295 THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
 296 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39;BBs_v39]
 297 THEN REPEAT RESA_TAC
 298 THEN THAYTHE_TAC (52-36)[`SUC(SUC i)`;`SUC i`]THEN DICH_TAC (56-29)
 299 THEN DICH_TAC 0
 300 THEN REAL_ARITH_TAC;
 301
 302
 303 ASM_REWRITE_TAC[]
 304 THEN REWRITE_TAC[h0;REAL_ARITH`&2<= &2* #1.26`]
 305 THEN SUBGOAL_THEN`cstab <= dist (v i,(v:num->real^3) (SUC (SUC i)))`ASSUME_TAC
 306 ;
 307
 308
 309 MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= i+ 1*k+0/\ ~(k<=3)/\ ~(k=0)/\ k-1<k
 310 /\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)`)
 311 THEN RESA_TAC
 312 THEN THAYTHES_TAC (43-10)[`SUC(SUC i)`;`i`][scs_diag;ADD1;ARITH_RULE`(i+1)+1=i+2/\(i+2)+1= i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 313 THEN POP_ASSUM MP_TAC
 314 THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
 315 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 316 THEN RESA_TAC
 317 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 318 THEN STRIP_TAC
 319 THEN ONCE_REWRITE_TAC[DIST_SYM]
 320 THEN DICH_TAC 1
 321 THEN REAL_ARITH_TAC;
 322
 323 ASM_REWRITE_TAC[]
 324 THEN STRIP_TAC
 325 THEN ONCE_REWRITE_TAC[DIST_SYM]
 326 THEN MP_TAC(ARITH_RULE`3<k==> SUC i+k-1=SUC(i+k-1)`)
 327 THEN RESA_TAC
 328 ;
 329
 330
 331 MP_TAC Cuxvzoz.CUXVZOZ
 332 THEN RESA_TAC
 333 THEN THAYTHEL_TAC 0[`s`;`FF`;`k`;`SUC i`;`v`][scs_generic;GSYM ADD1;]
 334 THEN MATCH_DICH_TAC 0
 335 THEN STRIP_TAC;
 336
 337
 338 THAYTHES_TAC (35-10)[`i`;`SUC(SUC i)`][SCS_DIAG_2]
 339 THEN DICH_TAC 1
 340 THEN REWRITE_TAC[cstab]
 341 THEN REAL_ARITH_TAC;
 342
 343
 344 REWRITE_TAC[REAL_ARITH`a<= a/\ &2<= #3.01`;cstab]
 345 THEN STRIP_TAC;
 346
 347
 348 REPEAT RESA_TAC
 349 THEN THAYTHE_TAC (37-10)[`i'`;`j`]
 350 THEN DICH_TAC 1
 351 THEN DICH_TAC 1
 352 THEN REAL_ARITH_TAC;
 353
 354
 355 STRIP_TAC
 356 ;
 357
 358
 359 REPEAT RESA_TAC
 360 THEN THAYTHE_TAC (36-10)[`i'`;`j`]
 361 ;
 362
 363 STRIP_TAC
 364 ;
 365
 366
 367
 368 ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 369 ;
 370
 371
 372
 373 ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 374 ;
 375
 376
 377 MP_TAC(REAL_ARITH`&2 < norm ((v:num->real^3) (SUC (SUC i))) ==> ~(&2 = norm (v (SUC (SUC i))))`)
 378 THEN RESA_TAC
 379 THEN SUBGOAL_THEN`(!i'. scs_diag k (SUC (SUC i)) i'
 380               ==> &4 * h0 < scs_b_v39 s (SUC (SUC i)) i')`ASSUME_TAC
 381 ;
 382
 383
 384 REPEAT RESA_TAC
 385 THEN THAYTHE_TAC(33-11)[`SUC(SUC i)`;`i'`]
 386 ;
 387
 388
 389
 390
 391 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 392 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
 393 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
 394 THEN RESA_TAC
 395 THEN POP_ASSUM MP_TAC
 396 THEN REWRITE_TAC[NOT_EXISTS_THM]
 397 THEN STRIP_TAC
 398 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC (SUC i))) V' E')` ASSUME_TAC;
 399
 400
 401
 402 REPEAT RESA_TAC;
 403
 404 MRESA_TAC ODXLSTCv2[`s`;`k`;`v`;`SUC(SUC i)`]
 405 THEN POP_ASSUM MP_TAC
 406 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 407 THEN STRIP_TAC
 408 THEN THAYTHEL_ASM_TAC (41-21)[`SUC(SUC i)`;`i'`][scs_diag;]
 409 THEN DICH_TAC 1
 410 THEN REWRITE_TAC[DE_MORGAN_THM]
 411 THEN ONCE_REWRITE_TAC[SET_RULE`A\/B<=> B\/A`]
 412 THEN STRIP_TAC;
 413
 414
 415
 416 POP_ASSUM MP_TAC
 417 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`3<k==> ~(k=0)`]
 418 THEN REWRITE_TAC[ARITH_RULE`1+i= SUC i`]
 419 THEN STRIP_TAC
 420 THEN DICH_TAC 2
 421 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC i:num`]
 422 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`i' `;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][]
 423 THEN ONCE_REWRITE_TAC[DIST_SYM]
 424 THEN ASM_TAC
 425 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 426 THEN REPEAT RESA_TAC
 427 ;
 428
 429
 430
 431 SUBGOAL_THEN`scs_a_v39 s  (SUC (SUC (SUC i))) (SUC (SUC i))=  dist ((v:num->real^3) (SUC (SUC (SUC i))),v (SUC (SUC i)))`ASSUME_TAC
 432 ;
 433
 434
 435 DICH_TAC 2
 436 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`i' `;`s:scs_v39`;`SUC(SUC i)`;`SUC (SUC(SUC i))`][]
 437 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC (SUC(SUC i)):num`]
 438 THEN DICH_TAC(43-17)
 439 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 440 THEN REPEAT RESA_TAC
 441 THEN THAYTHE_TAC 1[`SUC(SUC i)`;`SUC(SUC(SUC i))`]
 442 THEN DICH_TAC 1
 443 THEN DICH_TAC 1
 444 THEN DICH_TAC(45-4)
 445 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 446 THEN REPEAT RESA_TAC
 447 THEN ONCE_REWRITE_TAC[DIST_SYM]
 448 THEN DICH_TAC 0
 449 THEN DICH_TAC 0
 450 THEN REAL_ARITH_TAC;
 451
 452
 453
 454
 455
 456 MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC (SUC i))`;`v`;`SUC (SUC i)`;`k`]
 457 THEN MRESA_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`]
 458 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (SUC (SUC i))`][GSYM ADD1]
 459 THEN THAYTHE_TAC 0[`v (SUC i)`]
 460 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) (v (SUC i)) <= pi
 461 ==> azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) (v (SUC i)) = pi
 462 \/ azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) ((v:num->real^3) (SUC i)) < pi`)
 463 THEN RESA_TAC;
 464
 465
 466
 467 MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`SUC i`]
 468 THEN SUBGOAL_THEN`dist ((v:num->real^3) (SUC (SUC (SUC i))),v (SUC (SUC i))) <
 469       scs_b_v39 s (SUC (SUC (SUC i))) (SUC (SUC i))` ASSUME_TAC;
 470
 471
 472
 473
 474 DICH_TAC(49-43)
 475 THEN STRIP_TAC
 476 THEN SYM_ASSUM_TAC
 477 THEN DICH_TAC(48-4)
 478 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 479 THEN REPEAT RESA_TAC
 480 ;
 481
 482
 483 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC (SUC i))), v ((SUC i))}`
 484 ASSUME_TAC;
 485
 486
 487 MRESAS_TAC WL_IN_V[`SUC (SUC (SUC i))`;`v:num->real^3`][BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 488 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ 2<k/\ ~(3=1)`)
 489 THEN RESA_TAC
 490 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC(SUC (SUC i)))`;`v (SUC i)`;`V`]
 491 THEN THAYTHES_TAC 0[`v (SUC(SUC (SUC i)))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;ADD1;BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC (SUC x))=x+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 492 ;
 493
 494
 495 SUBGOAL_THEN`(v:num->real^3) (SUC (SUC i)) IN aff_gt {vec 0} {v (SUC (SUC (SUC i))), v (SUC i)}`
 496 ASSUME_TAC;
 497
 498
 499
 500 MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 1<k/\ 2<k /\ ~(3=2)/\ ~(2=1)`)
 501 THEN RESA_TAC
 502 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v ((SUC (SUC i)))`;`v (SUC i)`;`V`]
 503 THEN THAYTHES_TAC 0[`v (SUC (SUC i))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2/\ (i+2)+1=i+3`;MOD_LT]
 504 THEN MRESAL_TAC WL_IN_V[`SUC (SUC (SUC i))`;`v:num->real^3`][]
 505 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC (SUC (SUC i)))`;`v (SUC (SUC i))`;`V`]
 506 THEN THAYTHES_TAC 0[`(v:num->real^3) (SUC(SUC (SUC i)))`;`v (SUC (SUC i))`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2/\ (i+2)+1=i+3`;MOD_LT]
 507 THEN DICH_TAC (60-6)
 508 THEN REWRITE_TAC[GSYM ADD1;generic]
 509 THEN STRIP_TAC
 510 THEN MRESAL_TAC WL_IN_E[`SUC (SUC i)`;`v:num->real^3`][]
 511 THEN THAYTHE_TAC 1[`v (SUC (SUC i))`;`v(SUC(SUC (SUC i)))`;`v (SUC i)`]
 512 THEN MRESAS_TAC Polar_fan.GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE[`v (SUC i)`;`v (SUC (SUC i))`;`v(SUC(SUC (SUC i)))`;][ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`]
 513 THEN DICH_TAC 0
 514 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 515 THEN RESA_TAC
 516 THEN DICH_TAC 0
 517 THEN MRESA_TAC th3[`vec 0:real^3`;`v (SUC(SUC (SUC i)))`;`v (SUC i)`]
 518 THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC (SUC i))`;`vec 0:real^3`;`v (SUC i)`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 519 THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC (SUC i))`;`vec 0:real^3`;`v (SUC(SUC (SUC i)))`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 520 THEN MRESAL_TAC Wrgcvdr_cizmrrh.AFF_GE_TO_AFF_GT2_GE1[`v (SUC i)`;`vec 0:real^3`;`(v:num->real^3) (SUC(SUC (SUC i)))`][UNION;IN_ELIM_THM;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`]
 521 THEN REPEAT STRIP_TAC
 522 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 523 THEN ASM_REWRITE_TAC[]
 524 ;
 525
 526
 527 MRESAS_TAC NUXCOEAv2[`s`;`k`;`v`;`SUC (SUC i)`;`SUC (SUC (SUC i))`][ARITH_RULE`SUC (SUC i) + k - 1=SUC (SUC i + k - 1)`]
 528 THEN ONCE_REWRITE_TAC[DIST_SYM]
 529 THEN SYM_ASSUM_TAC
 530 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`SUC(SUC i+k-1)`;`s:scs_v39`;`SUC(SUC i)`;`SUC(SUC i+k-1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;]
 531 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> SUC (SUC i + k - 1) = 1*k+SUC i `;MOD_MULT_ADD]
 532 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`SUC i MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;]
 533 THEN ASM_TAC
 534 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 535 THEN REPEAT RESA_TAC
 536 ;
 537
 538
 539
 540
 541 ONCE_REWRITE_TAC[DIST_SYM]
 542 THEN MP_TAC(ARITH_RULE`3<k==> SUC i+k-1=SUC(i+k-1)`)
 543 THEN RESA_TAC
 544 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (SUC i)+k-1`;`v:num->real^3`;`(SUC (SUC i)+k-1)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
 545 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(SUC i) MOD k`;`v:num->real^3`;`(SUC i)`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
 546 ;
 547
 548
 549
 550 MP_TAC Cuxvzoz.CJBDXXN
 551 THEN RESA_TAC
 552 THEN THAYTHES_TAC 0[`s`;`FF`;`k`;`SUC(SUC i)`;`v`][scs_generic;MOD_MULT_ADD;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
 553 THEN MATCH_DICH_TAC 0
 554 THEN STRIP_TAC;
 555
 556
 557
 558 ASM_REWRITE_TAC[GSYM ADD1]
 559 THEN ONCE_REWRITE_TAC[DIST_SYM]
 560 THEN MRESA_TAC SCS_DIAG_2[`k`;`SUC i`]
 561 THEN THAYTHE_TAC (52-12)[`SUC i`;`SUC(SUC(SUC i))`]
 562 THEN DICH_TAC 1
 563 THEN REWRITE_TAC[cstab]
 564 THEN REAL_ARITH_TAC;
 565
 566
 567 STRIP_TAC
 568 ;
 569
 570
 571 ASM_SIMP_TAC[interior_angle1;GSYM ivs_rho_node1;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;MOD_MULT_ADD;GSYM ADD1]
 572 ;
 573
 574
 575 STRIP_TAC
 576 ;
 577
 578
 579 ASM_SIMP_TAC[interior_angle1;GSYM ivs_rho_node1;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;MOD_MULT_ADD;GSYM ADD1]
 580 THEN MRESA_TAC Rrcwnsj.BB_F_SUC_PRE[`s`;`v`;`i`]
 581 ;
 582
 583
 584
 585 STRIP_TAC
 586 ;
 587
 588
 589 MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`(1*k+SUC i) `;`s:scs_v39`;`SUC(SUC i)`;`(1*k+SUC i)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
 590 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`(SUC i)  MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
 591 THEN ASM_TAC
 592 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 593 THEN REPEAT RESA_TAC
 594 ;
 595
 596
 597
 598 STRIP_TAC
 599 ;
 600
 601
 602
 603 MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`SUC(SUC i)`;`(1*k+SUC i) `;`s:scs_v39`;`SUC(SUC i)`;`(1*k+SUC i)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
 604 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`SUC(SUC i)`;`(SUC i)  MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
 605 THEN ASM_TAC
 606 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 607 THEN REPEAT RESA_TAC
 608 THEN REAL_ARITH_TAC;
 609
 610
 611 REWRITE_TAC[GSYM ADD1]
 612 THEN ONCE_REWRITE_TAC[DIST_SYM];
 613
 614 MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC(SUC i)`][GSYM dist];
 615
 616
 617 DICH_TAC (52-4)
 618 THEN ASM_REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 619 THEN STRIP_TAC
 620 THEN THAYTHE_TAC (71-68)[`SUC(SUC i)`]
 621 THEN DICH_TAC(71-16)
 622 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 623 THEN STRIP_TAC
 624 THEN THAYTHE_TAC 0[`SUC(SUC i)`;`SUC(SUC(SUC i))`]
 625 THEN POP_ASSUM MP_TAC
 626 THEN DICH_TAC 3
 627 THEN REAL_ARITH_TAC;
 628
 629
 630
 631 ]);;
 632
 633
 634
 635
 636 let TFITSKC_concl = `
 637 main_nonlinear_terminal_v11
 638 ==> (!s (v:num->real^3) i.
 639  scs_a_v39 s (i+2) (i+3)< scs_b_v39 s (i+2) (i+3) /\
 640 3< scs_k_v39 s  /\
 641 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
 642   scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0 /\
 643   dist(v i,v (i+1)) = &2 /\ &2< scs_b_v39 s i (i+1) /\
 644   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) ==>
 645   dist(v (i+1),v(i+2)) = &2)`;;
 646
 647
 648
 649 let TFITSKC=prove( TFITSKC_concl,
 650 STRIP_TAC
 651 THEN REPEAT STRIP_TAC
 652 THEN MP_TAC TFITSKCv1
 653 THEN RESA_TAC
 654 THEN POP_ASSUM MATCH_MP_TAC
 655 THEN EXISTS_TAC`s:scs_v39`
 656 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC i)=i+2/\ SUC i+2=i+3`]
 657 THEN ASM_TAC
 658 THEN REWRITE_TAC[scs_basic]
 659 THEN REPEAT RESA_TAC);;
 660
 661
 662
 663  end;;
 664
 665
 666 (*
 667 let check_completeness_claimA_concl =
 668   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 669 *)
 670
 671
 672
 673