text_formalization/local/YRTAFYH.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 Yrtafyh = 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 let SUR_MOD_FUN=prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,
  91 STRIP_TAC
  92 THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
  93 THEN RESA_TAC
  94 THENL[
  95 EXISTS_TAC`p' MOD k- p MOD k`
  96 THEN MRESA_TAC DIVISION[`p'`;`k`]
  97 THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
  98 THEN RESA_TAC
  99 THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
 100 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
 101 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
 102
 103 EXISTS_TAC`p' MOD k +k - p MOD k`
 104 THEN MRESA_TAC DIVISION[`p`;`k`]
 105 THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
 106 THEN RESA_TAC
 107 THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
 108 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
 109 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
 110
 111 let TRANS_DIAG=prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
 112 ==> (i+q) MOD k= q' MOD k `,
 113 STRIP_TAC
 114 THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
 115 THEN EXISTS_TAC`p:num`
 116 THEN ASM_REWRITE_TAC[]
 117 THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
 118 THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
 119 THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;
 120
 121
 122 (*************)
 123
 124
 125 (*******************)
 126
 127
 128 let scs_components = prove_by_refinement(
 129   `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
 130 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
 131                          scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,
 132   (* {{{ proof *)
 133   [
 134   REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
 135   REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
 136   REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
 137   REWRITE_TAC[scs_str_v39];
 138
 139 BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
 140 Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
 141   ]);;
 142   (* }}} *)
 143
 144 let scs_inj = prove_by_refinement(
 145   `!s s'. scs_basic_v39 s /\  scs_basic_v39 s' /\
 146     scs_d_v39 s = scs_d_v39 s' /\
 147     scs_k_v39 s = scs_k_v39 s' /\
 148     (scs_a_v39 s = scs_a_v39 s') /\
 149     (scs_b_v39 s = scs_b_v39 s')
 150   ==> (s = s')`,
 151
 152   (* {{{ proof *)
 153   [
 154   REPEAT WEAKER_STRIP_TAC;
 155   REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
 156   REWRITE_TAC[scs_basic;unadorned_v39];
 157   ONCE_REWRITE_TAC[EQ_SYM_EQ];
 158   REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
 159   REPEAT WEAKER_STRIP_TAC;
 160   ONCE_REWRITE_TAC[GSYM scs_v39];
 161   AP_TERM_TAC;
 162   ASM_REWRITE_TAC[scs_components];
 163   TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
 164     BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
 165   BY(REWRITE_TAC[])
 166   ]);;
 167   (* }}} *)
 168
 169
 170
 171 let DIAG_PSORT1=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 172 p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
 173 ==>  (psort k (i+i',i+j) = psort k (p',q'))`,
 174
 175 [
 176 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
 177 ]
 178 THEN RESA_TAC
 179 THEN POP_ASSUM MP_TAC
 180 THEN MP_TAC TRANS_DIAG
 181 THEN RESA_TAC
 182 THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
 183 THEN RESA_TAC;
 184
 185 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 186 THEN RESA_TAC;
 187
 188 REWRITE_TAC[PAIR_EQ]
 189 THEN RESA_TAC
 190 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 191 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
 192
 193 REWRITE_TAC[PAIR_EQ]
 194 THEN RESA_TAC
 195 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 196 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
 197 THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
 198 THEN RESA_TAC;
 199
 200 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
 201 THEN RESA_TAC;
 202
 203 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
 204 THEN RESA_TAC;
 205
 206 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 207 THEN RESA_TAC;
 208
 209 REWRITE_TAC[PAIR_EQ]
 210 THEN RESA_TAC
 211 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 212 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];
 213
 214
 215 MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
 216 THEN RESA_TAC;
 217
 218 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
 219 THEN RESA_TAC;
 220
 221 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
 222 THEN RESA_TAC;
 223
 224 REWRITE_TAC[PAIR_EQ]
 225 THEN RESA_TAC
 226 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 227 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
 228
 229
 230
 231
 232
 233 let DIAG_PSORT2=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 234 p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
 235 ==>
 236 (psort k (i',j) = psort k (p,q))`,
 237 [
 238 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
 239 ]
 240 THEN RESA_TAC
 241 THEN POP_ASSUM MP_TAC
 242 THEN MP_TAC TRANS_DIAG
 243 THEN RESA_TAC
 244 THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
 245 THEN RESA_TAC;
 246
 247 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
 248 THEN RESA_TAC;
 249
 250 REWRITE_TAC[PAIR_EQ]
 251 THEN RESA_TAC
 252 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 253 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
 254
 255 REWRITE_TAC[PAIR_EQ]
 256 THEN RESA_TAC
 257 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 258 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
 259
 260 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
 261 THEN RESA_TAC;
 262
 263
 264 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
 265 THEN RESA_TAC;
 266
 267 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
 268 THEN RESA_TAC;
 269
 270 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
 271 THEN RESA_TAC;
 272
 273 REWRITE_TAC[PAIR_EQ]
 274 THEN RESA_TAC
 275 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 276 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
 277
 278 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
 279 THEN RESA_TAC;
 280
 281 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
 282 THEN RESA_TAC;
 283
 284 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
 285 THEN RESA_TAC;
 286
 287 REWRITE_TAC[PAIR_EQ]
 288 THEN RESA_TAC
 289 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 290 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
 291
 292
 293
 294
 295 let DIAG_PSORT=prove(
 296  ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 297 p' + q = p + q' /\ ~(k=0)
 298 ==>
 299 ((psort k (i+i',i+j) = psort k (p',q'))
 300 <=>
 301 (psort k (i',j) = psort k (p,q)))`,
 302 STRIP_TAC
 303 THEN EQ_TAC
 304 THEN STRIP_TAC
 305 THENL[
 306 MATCH_MP_TAC DIAG_PSORT2
 307 THEN RESA_TAC;
 308 MATCH_MP_TAC DIAG_PSORT1
 309 THEN RESA_TAC]);;
 310
 311 let TRANS_DIAG=prove(`
 312 ~(k=0)
 313 ==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,
 314 SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;
 315
 316
 317 let A_EQ_PSORT=prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
 318 ==> scs_a_v39 s i j= scs_a_v39 s p q`,
 319 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
 320 THEN REPEAT RESA_TAC
 321 THEN POP_ASSUM MP_TAC
 322 THEN ABBREV_TAC`k=scs_k_v39 s`
 323 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
 324 THEN RESA_TAC
 325 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 326 THEN RESA_TAC
 327 THEN
 328 REWRITE_TAC[PAIR_EQ]
 329 THEN STRIP_TAC
 330 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
 331 THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
 332 THEN ASM_TAC
 333 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 334 THEN REPEAT RESA_TAC);;
 335
 336
 337 let B_EQ_PSORT=prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
 338 ==> scs_b_v39 s i j= scs_b_v39 s p q`,
 339 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
 340 THEN REPEAT RESA_TAC
 341 THEN POP_ASSUM MP_TAC
 342 THEN ABBREV_TAC`k=scs_k_v39 s`
 343 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
 344 THEN RESA_TAC
 345 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 346 THEN RESA_TAC
 347 THEN
 348 REWRITE_TAC[PAIR_EQ]
 349 THEN STRIP_TAC
 350 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
 351 THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
 352 THEN ASM_TAC
 353 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 354 THEN REPEAT RESA_TAC);;
 355
 356 let PROPERTY_OF_K_SCS=prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,
 357 STRIP_TAC
 358 THEN MP_TAC Axjrpnc.is_scs_k_le_3
 359 THEN RESA_TAC
 360 THEN DICH_TAC 0
 361 THEN ARITH_TAC);;
 362
 363
 364 let PSORT_PERIODIC=prove(`~(k=0) ==> psort (k) (i + k,j) = psort (k) (i,j)
 365 /\ psort (k) (i,j+k) = psort (k) (i,j)`,
 366 REPEAT RESA_TAC
 367 THEN REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
 368 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k=1*k+i`]
 369 THEN ASM_SIMP_TAC[MOD_MULT_ADD]);;
 370
 371
 372 let DIAG_NOT_PSORT = prove_by_refinement(
 373 `~(k=0) /\ scs_diag k i j ==> !i'. ~(psort k (i,j) = psort k (i',SUC i'))`,
 374 [
 375 REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
 376 THEN STRIP_TAC
 377 THEN GEN_TAC
 378 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k\/ ~(i MOD k <= j MOD k)`)
 379 THEN RESA_TAC;
 380
 381 MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
 382 THEN RESA_TAC;
 383
 384 REWRITE_TAC[PAIR_EQ]
 385 THEN STRIP_TAC
 386 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
 387 THEN POP_ASSUM MP_TAC
 388 THEN SYM_ASSUM_TAC
 389 THEN ASM_REWRITE_TAC[];
 390
 391 REWRITE_TAC[PAIR_EQ]
 392 THEN STRIP_TAC
 393 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
 394 THEN POP_ASSUM MP_TAC
 395 THEN REMOVE_ASSUM_TAC
 396 THEN SYM_ASSUM_TAC
 397 THEN ASM_REWRITE_TAC[];
 398
 399 MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
 400 THEN RESA_TAC;
 401
 402
 403 REWRITE_TAC[PAIR_EQ]
 404 THEN STRIP_TAC
 405 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
 406 THEN POP_ASSUM MP_TAC
 407 THEN SYM_ASSUM_TAC
 408 THEN ASM_REWRITE_TAC[];
 409
 410 REWRITE_TAC[PAIR_EQ]
 411 THEN STRIP_TAC
 412 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
 413 THEN POP_ASSUM MP_TAC
 414 THEN REMOVE_ASSUM_TAC
 415 THEN SYM_ASSUM_TAC
 416 THEN ASM_REWRITE_TAC[]]);;
 417
 418
 419 let YRTAFYH_concl =
 420   `!s i j.
 421     is_scs_v39 s /\
 422     scs_basic_v39 s /\
 423     3 < scs_k_v39 s /\
 424     scs_diag (scs_k_v39 s) i j /\
 425     scs_a_v39 s i j <= cstab ==>
 426     is_scs_v39 (scs_stab_diag_v39 s i j) /\ scs_basic_v39 (scs_stab_diag_v39 s i j)
 427     `;;
 428
 429
 430 let YRTAFYH=  prove_by_refinement(YRTAFYH_concl,
 431 [
 432
 433 REPEAT RESA_TAC
 434 THEN MP_TAC PROPERTY_OF_K_SCS
 435 THEN RESA_TAC;
 436
 437 DICH_TAC 8
 438 THEN STRIP_TAC
 439 THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC(th))
 440 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;scs_stab_diag_v39;is_scs_v39;scs_v39_explicit;mk_unadorned_v39;scs_basic;periodic;periodic2]
 441 THEN REPEAT RESA_TAC
 442 THEN ABBREV_TAC`k= scs_k_v39 s`;
 443
 444 SET_TAC[];
 445
 446 SET_TAC[];
 447
 448 SET_TAC[];
 449
 450 SET_TAC[];
 451
 452 ASM_SIMP_TAC[PSORT_PERIODIC];
 453
 454 ASM_SIMP_TAC[PSORT_PERIODIC];
 455
 456 ASM_SIMP_TAC[PSORT_PERIODIC];
 457
 458 ASM_SIMP_TAC[PSORT_PERIODIC];
 459
 460 ASM_SIMP_TAC[Terminal.psort_sym];
 461
 462 REAL_ARITH_TAC;
 463
 464 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
 465 THEN RESA_TAC;
 466
 467 MRESAL_TAC A_EQ_PSORT[`i'`;`j'`;`s`;`i`;`j`][];
 468
 469 THAYTHE_TAC (30-21)[`i'`;`j'`]
 470 THEN DICH_TAC 0
 471 THEN DICH_TAC 0
 472 THEN DICH_TAC 0
 473 THEN REAL_ARITH_TAC;
 474
 475 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
 476 THEN RESA_TAC
 477 THEN REAL_ARITH_TAC;
 478
 479 MP_TAC(SET_RULE`psort 3 (i,j) = psort 3 (i',SUC i') \/ ~(psort 3 (i,j) = psort 3 (i', SUC i'))`)
 480 THEN RESA_TAC;
 481
 482 REWRITE_TAC[cstab]
 483 THEN REAL_ARITH_TAC;
 484
 485 MATCH_DICH_TAC (31-24)
 486 THEN ASM_REWRITE_TAC[];
 487
 488 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',SUC i') \/ ~(psort k (i,j) = psort k (i', SUC i'))`)
 489 THEN RESA_TAC;
 490
 491 REAL_ARITH_TAC;
 492
 493 MP_TAC DIAG_NOT_PSORT
 494 THEN RESA_TAC;
 495
 496 REWRITE_TAC[scs_basic;scs_stab_diag_v39;LET_DEF;LET_END_DEF;unadorned_v39;mk_unadorned_v39;scs_v39_explicit]]);;
 497
 498
 499
 500 let STAB_IS_SCS=prove(`!s i j.
 501     is_scs_v39 s /\
 502     scs_basic_v39 s /\
 503     3 < scs_k_v39 s /\
 504     scs_diag (scs_k_v39 s) i j /\
 505     scs_a_v39 s i j <= cstab ==>
 506     is_scs_v39 (scs_stab_diag_v39 s i j) `,
 507 SIMP_TAC[YRTAFYH]);;
 508
 509
 510  end;;
 511
 512
 513 (*
 514 let check_completeness_claimA_concl =
 515   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 516 *)
 517
 518
 519
 520