text_formalization/local/UXCKFPE.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 Uxckfpe = struct
  16
  17 open Polyhedron;;
  18 open Sphere;;
  19 open Topology;;
  20 open Fan_misc;;
  21 open Planarity;;
  22 open Conforming;;
  23 open Hypermap;;
  24 open Fan;;
  25 open Topology;;
  26 open Wrgcvdr_cizmrrh;;
  27 open Local_lemmas;;
  28 open Collect_geom;;
  29 open Dih2k_hypermap;;
  30 open Wjscpro;;
  31 open Tecoxbm;;
  32 open Hdplygy;;
  33 open Nkezbfc_local;;
  34 open Flyspeck_constants;;
  35 open Gbycpxs;;
  36 open Pcrttid;;
  37 open Local_lemmas;;
  38 open Pack_defs;;
  39
  40 open Hales_tactic;;
  41
  42 open Appendix;;
  43
  44
  45
  46
  47
  48 open Hypermap;;
  49 open Fan;;
  50 open Wrgcvdr_cizmrrh;;
  51 open Local_lemmas;;
  52 open Flyspeck_constants;;
  53 open Pack_defs;;
  54
  55 open Hales_tactic;;
  56
  57 open Appendix;;
  58
  59
  60 open Zithlqn;;
  61
  62
  63 open Xwitccn;;
  64
  65 open Ayqjtmd;;
  66
  67 open Jkqewgv;;
  68
  69
  70 let NOT_EMPTY_CASE_4_IS_SCS=prove_by_refinement(
  71 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv
  72 /\  dimindex(:M)= scs_k_v39 s
  73 ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
  74 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
  75 THEN STRIP_TAC
  76 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
  77 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
  78 THEN EXISTS_TAC`a:real^(M,3)finite_product`
  79 THEN MATCH_MP_TAC IN_IS_SCS_CASE_4
  80 THEN ASM_REWRITE_TAC[]]);;
  81
  82
  83
  84 let ARITH_4_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 4 MOD 4=0/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 4=1/\ 1<=1/\ 1<=4/\ 1 MOD 4=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 4=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 4=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 4=1/\ ~(4=0)/\ 0 MOD 4=0`;;
  85
  86
  87 let VV_IN_BALL_ANNULUS_TAC_4=
  88 fun (so:term)->
  89 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
  90 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
  91 THEN MRESAL1_TAC th so[ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
  92 ;;
  93
  94
  95 let SCS_A_LE_NORM_4_IS_SCS=
  96 fun (so:term) (so1:term)->
  97 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
  98 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
  99 THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
 100 THEN ASM_TAC
 101 THEN REWRITE_TAC[periodic2]
 102 THEN REPEAT STRIP_TAC
 103 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
 104 THEN POP_ASSUM(fun th->
 105 ASM_TAC
 106 THEN REWRITE_TAC[th]
 107 THEN REPEAT STRIP_TAC
 108 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 109 THEN ASSUME_TAC th)
 110 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 111 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
 112 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
 113 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
 114 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 115 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
 116 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
 117 THEN REPEAT RESA_TAC
 118 ;;
 119
 120 let PROVE_INEQUALITY_TAC_4=
 121 fun (th:term)->
 122 MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
 123 THEN RESA_TAC
 124 THENL[
 125 SCS_A_LE_NORM_4_IS_SCS th `4`;
 126 SCS_A_LE_NORM_4_IS_SCS th `1`;
 127 SCS_A_LE_NORM_4_IS_SCS th `2`;
 128 SCS_A_LE_NORM_4_IS_SCS th `3`];;
 129
 130
 131
 132
 133 let SCS_B_LE_NORM_4_IS_SCS=
 134 fun (so:term) (so1:term)->
 135 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
 136 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 137 THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
 138 THEN ASM_TAC
 139 THEN REWRITE_TAC[periodic2]
 140 THEN REPEAT STRIP_TAC
 141 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
 142 THEN POP_ASSUM(fun th->
 143 ASM_TAC
 144 THEN REWRITE_TAC[th]
 145 THEN REPEAT STRIP_TAC
 146 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 147 THEN ASSUME_TAC th)
 148 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 149 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
 150 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
 151 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
 152 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 153 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
 154 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
 155 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (4)`][ARITH_RULE`~(4=0)`;periodic]
 156 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
 157 THEN REPEAT RESA_TAC
 158 ;;
 159
 160 let PROVE_INEQUALITY_TAC_4B=
 161 fun (th:term)->
 162 MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
 163 THEN RESA_TAC
 164 THENL[
 165 SCS_B_LE_NORM_4_IS_SCS th `4`;
 166 SCS_B_LE_NORM_4_IS_SCS th `1`;
 167 SCS_B_LE_NORM_4_IS_SCS th `2`;
 168 SCS_B_LE_NORM_4_IS_SCS th `3`];;
 169
 170
 171
 172
 173 let V_SY_EQ_IMAGE_VV_TAC4=
 174 fun (th:term)->
 175 ASM_REWRITE_TAC[]
 176 THEN EXISTS_TAC th
 177 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_4_TAC];;
 178
 179
 180 let PROVE_E_SY_EQ_MOD_TAC_4=
 181 fun (so:term)->
 182 EXISTS_TAC so
 183 THEN ASM_REWRITE_TAC[ARITH_4_TAC]
 184 ;;
 185
 186
 187
 188
 189
 190
 191
 192 let PROOF_E_EQ_TAC_4=
 193 fun (so:term)->
 194 EXISTS_TAC so
 195 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_4_TAC;]
 196 ;;
 197
 198
 199 let PROVE_E_SY_EQ_IMAGE_VV_4=
 200 fun (so:term) (so1:term)->
 201 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_4_TAC]
 202 THEN EXISTS_TAC so
 203 THEN ASM_REWRITE_TAC[ARITH_4_TAC];;
 204
 205
 206
 207
 208 let  IN_NOT_EMPTY_B1_SY_4_IS_SCS=prove_by_refinement(
 209 `is_scs_v39 s /\ scs_k_v39 s=4 /\
 210 dimindex(:M) = scs_k_v39 s/\
 211  matvec (v:real^3^M) =a/\
 212 (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\
 213  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
 214  CONDITION2_SY v
 215 /\ (!i. vv i =
 216 if i MOD scs_k_v39 s = 0 then row 4 v else
 217 if i MOD scs_k_v39 s = 1 then row 1 v else
 218 if i MOD scs_k_v39 s = 2 then row 2 v else
 219 row 3 v)
 220 ==> vv IN BBs_v39 s`,
 221 [
 222
 223 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
 224 THEN REPEAT STRIP_TAC
 225 THEN ASM_TAC
 226 THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
 227 THEN REPEAT RESA_TAC;
 228
 229
 230 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
 231 THEN REPEAT STRIP_TAC
 232 THEN ASM_REWRITE_TAC[]
 233 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 234 THEN MP_TAC(ARITH_RULE`x' MOD 4<4 ==> x' MOD 4 = 0 \/ x' MOD 4 = 1 \/ x' MOD 4 = 2 \/ x' MOD 4 = 3`)
 235 THEN RESA_TAC
 236 THENL[
 237 VV_IN_BALL_ANNULUS_TAC_4 `4`;
 238 VV_IN_BALL_ANNULUS_TAC_4 `1`;
 239 VV_IN_BALL_ANNULUS_TAC_4 `2`;
 240 VV_IN_BALL_ANNULUS_TAC_4 `3`];
 241
 242
 243
 244 ASM_REWRITE_TAC[periodic]
 245 THEN GEN_TAC
 246 THEN MRESAL_TAC MOD_EQ[`i+4:num`;`i:num`;`4:num`;`1`][ARITH_RULE`1*A=A`];
 247
 248
 249
 250 REWRITE_TAC[dist]
 251 THEN REPEAT GEN_TAC
 252 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;
 253
 254
 255 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 256 THEN GEN_TAC
 257 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];
 258
 259
 260
 261 MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
 262 THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
 263 THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
 264 THEN RESA_TAC
 265 THENL[
 266 PROVE_INEQUALITY_TAC_4 `4`;
 267 PROVE_INEQUALITY_TAC_4 `1`;
 268 PROVE_INEQUALITY_TAC_4 `2`;
 269 PROVE_INEQUALITY_TAC_4 `3`]
 270 ;
 271
 272
 273
 274
 275
 276 REWRITE_TAC[dist]
 277 THEN REPEAT GEN_TAC
 278 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;
 279
 280
 281 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 282 THEN GEN_TAC
 283 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];
 284
 285
 286
 287 MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
 288 THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
 289 THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
 290 THEN RESA_TAC
 291 THENL[
 292 PROVE_INEQUALITY_TAC_4B `4`;
 293 PROVE_INEQUALITY_TAC_4B `1`;
 294 PROVE_INEQUALITY_TAC_4B `2`;
 295 PROVE_INEQUALITY_TAC_4B `3`]
 296 ;
 297
 298
 299
 300
 301
 302
 303
 304
 305
 306
 307
 308 POP_ASSUM MP_TAC
 309 THEN ASM_REWRITE_TAC[ARITH_RULE`~(4<=3)`]
 310 THEN STRIP_TAC
 311 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
 312
 313
 314
 315 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
 316 THEN GEN_TAC
 317 THEN EQ_TAC;
 318
 319
 320 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
 321 THEN STRIP_TAC
 322 THENL[
 323 V_SY_EQ_IMAGE_VV_TAC4 `1`;
 324 V_SY_EQ_IMAGE_VV_TAC4 `2`;
 325 V_SY_EQ_IMAGE_VV_TAC4 `3`;
 326 V_SY_EQ_IMAGE_VV_TAC4 `4`];
 327
 328
 329
 330 RESA_TAC
 331 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 332 THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
 333 THEN RESA_TAC
 334 THENL[
 335 PROVE_E_SY_EQ_MOD_TAC_4 `4`;
 336 PROVE_E_SY_EQ_MOD_TAC_4 `1`;
 337 PROVE_E_SY_EQ_MOD_TAC_4 `2`;
 338 PROVE_E_SY_EQ_MOD_TAC_4 `3`]
 339 ;
 340
 341
 342
 343
 344
 345
 346
 347 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
 348
 349
 350
 351 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
 352 THEN ONCE_REWRITE_TAC[EXTENSION;]
 353 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 354 THEN GEN_TAC
 355 THEN EQ_TAC
 356 ;
 357
 358
 359
 360
 361 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
 362 THEN RESA_TAC
 363 THENL[
 364 PROOF_E_EQ_TAC_4`1`;
 365 PROOF_E_EQ_TAC_4`2`;
 366 PROOF_E_EQ_TAC_4`3`;
 367 PROOF_E_EQ_TAC_4`4`]
 368 ;
 369
 370
 371
 372 RESA_TAC
 373 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 374 THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
 375 THEN RESA_TAC
 376 THENL[
 377 PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
 378 PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
 379 PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
 380 PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];
 381
 382
 383
 384 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
 385
 386
 387 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
 388 THEN ONCE_REWRITE_TAC[EXTENSION;]
 389 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 390 THEN GEN_TAC
 391 THEN EQ_TAC
 392 ;
 393
 394
 395
 396
 397 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
 398 THEN RESA_TAC
 399 THENL[
 400 PROOF_E_EQ_TAC_4`1`;
 401 PROOF_E_EQ_TAC_4`2`;
 402 PROOF_E_EQ_TAC_4`3`;
 403 PROOF_E_EQ_TAC_4`4`]
 404 ;
 405
 406
 407
 408 RESA_TAC
 409 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 410 THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
 411 THEN RESA_TAC
 412 THENL[
 413 PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
 414 PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
 415 PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
 416 PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];
 417
 418
 419
 420 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 421 THEN ASM_REWRITE_TAC[]
 422 THEN REPEAT STRIP_TAC
 423 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
 424 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 425 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 426 THEN ASM_REWRITE_TAC[];
 427 ]);;
 428   (* }}} *)
 429
 430
 431
 432 let XWITCCN_CASE_4_IS_SCS=prove_by_refinement(
 433 ` is_scs_v39 s /\ BBs_v39 s vv
 434 /\ scs_k_v39 s=4
 435 /\  dimindex(:M) =scs_k_v39 s
 436 /\  taustar_v39 s vv < &0
 437  ==> ~(BBprime_v39 s = {})`,
 438   (* {{{ proof *)
 439 [
 440
 441
 442 STRIP_TAC
 443 THEN MP_TAC IS_SCS_STABLE_SYSTEM
 444 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
 445 THEN STRIP_TAC
 446 THEN MP_TAC NOT_EMPTY_CASE_4_IS_SCS
 447 THEN RESA_TAC
 448 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
 449 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
 450          (change_type_v3 (scs_a_v39 s)),
 451          (change_type_v3 (scs_b_v39 s)),
 452          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
 453          (\i. (1 + i) MOD scs_k_v39 s))`
 454 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
 455          (change_type_v3 (scs_a_v39 s))`;`
 456          (change_type_v3 (scs_b_v39 s))`;`
 457          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
 458          (\i. (1 + i) MOD scs_k_v39 s)`]
 459 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<4`;]
 460 THEN POP_ASSUM (fun th->
 461 POP_ASSUM MP_TAC
 462 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 463 THEN STRIP_TAC
 464 THEN ASSUME_TAC th)
 465 THEN REWRITE_TAC[BBprime_v39;IN]
 466 THEN ABBREV_TAC`( vv1 i =
 467 if i MOD scs_k_v39 s = 0 then row 4 v else
 468 if i MOD scs_k_v39 s = 1 then row 1 v else
 469 if i MOD scs_k_v39 s = 2 then row 2 v else
 470 row 3 (v:real^3^M))`
 471 THEN EXISTS_TAC`vv1:num->real^3`
 472 THEN STRIP_TAC;
 473
 474
 475 ONCE_REWRITE_TAC[GSYM IN]
 476 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
 477 THEN EXISTS_TAC`x:real^(M,3)finite_product`
 478 THEN EXISTS_TAC`v:real^3^M`
 479 THEN ASM_REWRITE_TAC[]
 480 THEN POP_ASSUM MP_TAC
 481 ;
 482
 483
 484 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 0] = v:real^3^M`
 485 ASSUME_TAC;
 486
 487 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
 488 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 0 MOD 4=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
 489 THEN ONCE_REWRITE_TAC[CART_EQ]
 490 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=4 <=>i=1\/ i=2\/ i=3\/ i=4`]
 491 THEN REPEAT RESA_TAC
 492 THEN
 493 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
 494 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
 495 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
 496
 497
 498
 499 STRIP_TAC;
 500
 501 GEN_TAC
 502 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
 503 THEN REPEAT STRIP_TAC
 504 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
 505 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
 506 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
 507 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
 508 [`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;]
 509 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
 510 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
 511 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
 512 THEN MP_TAC th
 513 THEN REWRITE_TAC[IN]
 514 THEN STRIP_TAC)
 515 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
 516 THEN REWRITE_TAC[th]
 517 THEN RESA_TAC)
 518 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
 519 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 520 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`);
 521
 522 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
 523 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
 524 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
 525 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
 526 [`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;]
 527 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
 528 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
 529 THEN ASM_REWRITE_TAC[IN]
 530 THEN STRIP_TAC
 531 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
 532 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 533 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`)
 534 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
 535 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 536 THEN MP_TAC th)
 537 THEN ASM_REWRITE_TAC[]
 538 THEN POP_ASSUM MP_TAC
 539 THEN POP_ASSUM MP_TAC
 540 THEN REAL_ARITH_TAC;
 541
 542 ]);;
 543   (* }}} *)
 544
 545 (*************CASE 5****************)
 546
 547 let NOT_EMPTY_CASE_5_IS_SCS=prove_by_refinement(
 548 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv
 549 /\  dimindex(:M)= scs_k_v39 s
 550 ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
 551 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
 552 THEN STRIP_TAC
 553 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
 554 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
 555 THEN EXISTS_TAC`a:real^(M,3)finite_product`
 556 THEN MATCH_MP_TAC IN_IS_SCS_CASE_5
 557 THEN ASM_REWRITE_TAC[]]);;
 558
 559
 560
 561
 562
 563 let ARITH_5_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=5/\3<=5/\5<=5 /\ 4<=5/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=4/\ 4 MOD 5=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 5=0/\ ~(4=0)/\ 0 MOD 5=0
 564 /\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)
 565 `;;
 566
 567
 568
 569 let VV_IN_BALL_ANNULUS_TAC_5=
 570 fun (so:term)->
 571 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
 572 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 573 THEN MRESAL1_TAC th so[ARITH_5_TAC;IN])
 574 ;;
 575
 576
 577
 578
 579 let SCS_A_LE_NORM_5_IS_SCS=
 580 fun (so:term) (so1:term)->
 581 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
 582 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 583 THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
 584 THEN ASM_TAC
 585 THEN REWRITE_TAC[periodic2]
 586 THEN REPEAT STRIP_TAC
 587 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
 588 THEN POP_ASSUM(fun th->
 589 ASM_TAC
 590 THEN REWRITE_TAC[th]
 591 THEN REPEAT STRIP_TAC
 592 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 593 THEN ASSUME_TAC th)
 594 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
 595 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
 596 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
 597 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
 598 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 599 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
 600 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
 601 THEN REPEAT RESA_TAC
 602 ;;
 603
 604 let PROVE_INEQUALITY_TAC_5=
 605 fun (th:term)->
 606 MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
 607 THEN RESA_TAC
 608 THENL[
 609 SCS_A_LE_NORM_5_IS_SCS th `5`;
 610 SCS_A_LE_NORM_5_IS_SCS th `1`;
 611 SCS_A_LE_NORM_5_IS_SCS th `2`;
 612 SCS_A_LE_NORM_5_IS_SCS th `3`;
 613 SCS_A_LE_NORM_5_IS_SCS th `4`];;
 614
 615
 616
 617
 618
 619
 620 let SCS_B_LE_NORM_5_IS_SCS=
 621 fun (so:term) (so1:term)->
 622 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
 623 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 624 THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
 625 THEN ASM_TAC
 626 THEN REWRITE_TAC[periodic2]
 627 THEN REPEAT STRIP_TAC
 628 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
 629 THEN POP_ASSUM(fun th->
 630 ASM_TAC
 631 THEN REWRITE_TAC[th]
 632 THEN REPEAT STRIP_TAC
 633 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 634 THEN ASSUME_TAC th)
 635 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
 636 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
 637 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
 638 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
 639 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 640 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
 641 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
 642 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (5)`][ARITH_RULE`~(5=0)`;periodic]
 643 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
 644 THEN REPEAT RESA_TAC
 645 ;;
 646
 647 let PROVE_INEQUALITY_TAC_5B=
 648 fun (th:term)->
 649 MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
 650 THEN RESA_TAC
 651 THENL[
 652 SCS_B_LE_NORM_5_IS_SCS th `5`;
 653 SCS_B_LE_NORM_5_IS_SCS th `1`;
 654 SCS_B_LE_NORM_5_IS_SCS th `2`;
 655 SCS_B_LE_NORM_5_IS_SCS th `3`;
 656 SCS_B_LE_NORM_5_IS_SCS th `4`];;
 657
 658
 659
 660
 661
 662
 663
 664
 665
 666
 667
 668
 669 let V_SY_EQ_IMAGE_VV_TAC5=
 670 fun (th:term)->
 671 ASM_REWRITE_TAC[]
 672 THEN EXISTS_TAC th
 673 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_5_TAC];;
 674
 675
 676 let PROVE_E_SY_EQ_MOD_TAC_5=
 677 fun (so:term)->
 678 EXISTS_TAC so
 679 THEN ASM_REWRITE_TAC[ARITH_5_TAC]
 680 ;;
 681
 682
 683
 684
 685
 686
 687
 688 let PROOF_E_EQ_TAC_5=
 689 fun (so:term)->
 690 EXISTS_TAC so
 691 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_5_TAC;]
 692 ;;
 693
 694
 695 let PROVE_E_SY_EQ_IMAGE_VV_5=
 696 fun (so:term) (so1:term)->
 697 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_5_TAC]
 698 THEN EXISTS_TAC so
 699 THEN ASM_REWRITE_TAC[ARITH_5_TAC];;
 700
 701
 702
 703
 704 let  IN_NOT_EMPTY_B1_SY_5_IS_SCS=prove_by_refinement(
 705 `is_scs_v39 s /\ scs_k_v39 s=5 /\
 706 dimindex(:M) = scs_k_v39 s/\
 707  matvec (v:real^3^M) =a/\
 708 (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\
 709  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
 710  CONDITION2_SY v
 711 /\ (!i. vv i =
 712 if i MOD scs_k_v39 s = 0 then row 5 v else
 713 if i MOD scs_k_v39 s = 1 then row 1 v else
 714 if i MOD scs_k_v39 s = 2 then row 2 v else
 715 if i MOD scs_k_v39 s = 3 then row 3 v else
 716 row 4 v)
 717 ==> vv IN BBs_v39 s`,
 718 [
 719 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
 720 THEN REPEAT STRIP_TAC
 721 THEN ASM_TAC
 722 THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39;]
 723 THEN REPEAT RESA_TAC;
 724
 725 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
 726 THEN REPEAT STRIP_TAC
 727 THEN ASM_REWRITE_TAC[]
 728 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
 729 THEN MP_TAC(ARITH_RULE`x' MOD 5<5 ==> x' MOD 5 = 0 \/ x' MOD 5 = 1 \/ x' MOD 5 = 2 \/ x' MOD 5 = 3\/ x' MOD 5 = 4`)
 730 THEN RESA_TAC
 731 THENL[
 732 VV_IN_BALL_ANNULUS_TAC_5 `5`;
 733 VV_IN_BALL_ANNULUS_TAC_5 `1`;
 734 VV_IN_BALL_ANNULUS_TAC_5 `2`;
 735 VV_IN_BALL_ANNULUS_TAC_5 `3`;
 736 VV_IN_BALL_ANNULUS_TAC_5 `4`];
 737
 738 ASM_REWRITE_TAC[periodic]
 739 THEN GEN_TAC
 740 THEN MRESAL_TAC MOD_EQ[`i+5:num`;`i:num`;`5:num`;`1`][ARITH_RULE`1*A=A`];
 741
 742 REWRITE_TAC[dist]
 743 THEN REPEAT GEN_TAC
 744 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;
 745
 746 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 747 THEN GEN_TAC
 748 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];
 749
 750 MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
 751 THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
 752 THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
 753 THEN RESA_TAC
 754 THENL[
 755 PROVE_INEQUALITY_TAC_5 `5`;
 756 PROVE_INEQUALITY_TAC_5 `1`;
 757 PROVE_INEQUALITY_TAC_5 `2`;
 758 PROVE_INEQUALITY_TAC_5 `3`;
 759 PROVE_INEQUALITY_TAC_5 `4`];
 760
 761
 762
 763
 764 REWRITE_TAC[dist]
 765 THEN REPEAT GEN_TAC
 766 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;
 767
 768 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 769 THEN GEN_TAC
 770 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];
 771
 772
 773
 774 MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
 775 THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
 776 THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
 777 THEN RESA_TAC
 778 THENL[
 779 PROVE_INEQUALITY_TAC_5B `5`;
 780 PROVE_INEQUALITY_TAC_5B `1`;
 781 PROVE_INEQUALITY_TAC_5B `2`;
 782 PROVE_INEQUALITY_TAC_5B `3`;
 783 PROVE_INEQUALITY_TAC_5B `4`];
 784
 785 POP_ASSUM MP_TAC
 786 THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
 787 THEN STRIP_TAC
 788 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
 789
 790 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
 791 THEN GEN_TAC
 792 THEN EQ_TAC;
 793
 794 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5`]
 795 THEN STRIP_TAC
 796 THENL[
 797 V_SY_EQ_IMAGE_VV_TAC5 `1`;
 798 V_SY_EQ_IMAGE_VV_TAC5 `2`;
 799 V_SY_EQ_IMAGE_VV_TAC5 `3`;
 800 V_SY_EQ_IMAGE_VV_TAC5 `4`;
 801 V_SY_EQ_IMAGE_VV_TAC5 `5`;];
 802
 803
 804 RESA_TAC
 805 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
 806 THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3)\/ (x' MOD 5=4)`)
 807 THEN RESA_TAC
 808 THENL[
 809 PROVE_E_SY_EQ_MOD_TAC_5 `5`;
 810 PROVE_E_SY_EQ_MOD_TAC_5 `1`;
 811 PROVE_E_SY_EQ_MOD_TAC_5 `2`;
 812 PROVE_E_SY_EQ_MOD_TAC_5 `3`;
 813 PROVE_E_SY_EQ_MOD_TAC_5 `4`];
 814
 815
 816 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
 817
 818 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
 819 THEN ONCE_REWRITE_TAC[EXTENSION;]
 820 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 821 THEN GEN_TAC
 822 THEN EQ_TAC;
 823
 824
 825 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
 826 THEN RESA_TAC
 827 THENL[
 828 PROOF_E_EQ_TAC_5`1`;
 829 PROOF_E_EQ_TAC_5`2`;
 830 PROOF_E_EQ_TAC_5`3`;
 831 PROOF_E_EQ_TAC_5`4`;
 832 PROOF_E_EQ_TAC_5`5`];
 833
 834
 835 RESA_TAC
 836 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
 837 THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`)
 838 THEN RESA_TAC
 839 THENL[
 840 PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
 841 PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
 842 PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
 843 PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
 844 PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];
 845
 846 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
 847
 848 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
 849 THEN ONCE_REWRITE_TAC[EXTENSION;]
 850 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 851 THEN GEN_TAC
 852 THEN EQ_TAC;
 853
 854
 855 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
 856 THEN RESA_TAC
 857 THENL[
 858 PROOF_E_EQ_TAC_5`1`;
 859 PROOF_E_EQ_TAC_5`2`;
 860 PROOF_E_EQ_TAC_5`3`;
 861 PROOF_E_EQ_TAC_5`4`;
 862 PROOF_E_EQ_TAC_5`5`];
 863
 864
 865 RESA_TAC
 866 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
 867 THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`)
 868 THEN RESA_TAC
 869 THENL[
 870 PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
 871 PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
 872 PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
 873 PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
 874 PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];
 875
 876 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 877 THEN ASM_REWRITE_TAC[]
 878 THEN REPEAT STRIP_TAC
 879 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
 880 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 881 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 882 THEN ASM_REWRITE_TAC[];
 883
 884 ]);;
 885   (* }}} *)
 886
 887
 888
 889 let XWITCCN_CASE_5_IS_SCS=prove_by_refinement(
 890 ` is_scs_v39 s /\ BBs_v39 s vv
 891 /\ scs_k_v39 s=5
 892 /\  dimindex(:M) =scs_k_v39 s
 893 /\  taustar_v39 s vv < &0
 894  ==> ~(BBprime_v39 s = {})`,
 895   (* {{{ proof *)
 896 [
 897 STRIP_TAC
 898 THEN MP_TAC IS_SCS_STABLE_SYSTEM
 899 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
 900 THEN STRIP_TAC
 901 THEN MP_TAC NOT_EMPTY_CASE_5_IS_SCS
 902 THEN RESA_TAC
 903 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
 904 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
 905          (change_type_v3 (scs_a_v39 s)),
 906          (change_type_v3 (scs_b_v39 s)),
 907          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
 908          (\i. (1 + i) MOD scs_k_v39 s))`
 909 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
 910          (change_type_v3 (scs_a_v39 s))`;`
 911          (change_type_v3 (scs_b_v39 s))`;`
 912          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
 913          (\i. (1 + i) MOD scs_k_v39 s)`]
 914 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<5`;]
 915 THEN POP_ASSUM (fun th->
 916 POP_ASSUM MP_TAC
 917 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 918 THEN STRIP_TAC
 919 THEN ASSUME_TAC th)
 920 THEN REWRITE_TAC[BBprime_v39;IN]
 921 THEN ABBREV_TAC`( vv1 i =
 922 if i MOD scs_k_v39 s = 0 then row 5 v else
 923 if i MOD scs_k_v39 s = 1 then row 1 v else
 924 if i MOD scs_k_v39 s = 2 then row 2 v else
 925 if i MOD scs_k_v39 s = 3 then row 3 v else
 926 row 4 (v:real^3^M))`
 927 THEN EXISTS_TAC`vv1:num->real^3`
 928 THEN STRIP_TAC;
 929
 930 ONCE_REWRITE_TAC[GSYM IN]
 931 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
 932 THEN EXISTS_TAC`x:real^(M,3)finite_product`
 933 THEN EXISTS_TAC`v:real^3^M`
 934 THEN ASM_REWRITE_TAC[]
 935 THEN POP_ASSUM MP_TAC;
 936
 937 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 0] = v:real^3^M`
 938 ASSUME_TAC;
 939
 940 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
 941 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 0 MOD 5=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 5=4`;]
 942 THEN ONCE_REWRITE_TAC[CART_EQ]
 943 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=5 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5`]
 944 THEN REPEAT RESA_TAC
 945 THEN
 946 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
 947 REWRITE_TAC[num_CONV `4`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
 948 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
 949
 950
 951 STRIP_TAC;
 952
 953 GEN_TAC
 954 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
 955 THEN REPEAT STRIP_TAC
 956 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
 957 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
 958 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
 959 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
 960 [`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;]
 961 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
 962 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
 963 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
 964 THEN MP_TAC th
 965 THEN REWRITE_TAC[IN]
 966 THEN STRIP_TAC)
 967 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
 968 THEN REWRITE_TAC[th]
 969 THEN RESA_TAC)
 970 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
 971 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 972 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`);
 973
 974 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
 975 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
 976 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
 977 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
 978 [`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;]
 979 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
 980 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
 981 THEN ASM_REWRITE_TAC[IN]
 982 THEN STRIP_TAC
 983 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
 984 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 985 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`)
 986 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
 987 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 988 THEN MP_TAC th)
 989 THEN ASM_REWRITE_TAC[]
 990 THEN POP_ASSUM MP_TAC
 991 THEN POP_ASSUM MP_TAC
 992 THEN REAL_ARITH_TAC;
 993
 994 ]);;
 995   (* }}} *)
 996
 997
 998
 999
1000
1001 (*************CASE 6****************)
1002
1003 let NOT_EMPTY_CASE_6_IS_SCS=prove_by_refinement(
1004 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv
1005 /\  dimindex(:M)= scs_k_v39 s
1006 ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
1007 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
1008 THEN STRIP_TAC
1009 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
1010 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
1011 THEN EXISTS_TAC`a:real^(M,3)finite_product`
1012 THEN MATCH_MP_TAC IN_IS_SCS_CASE_6
1013 THEN ASM_REWRITE_TAC[]]);;
1014
1015
1016
1017
1018 let ARITH_6_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=6/\3<=6/\5<=6 /\ 4<=6/\5<=6/\ 6<=6/\ 1<=6 /\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=4/\ 4 MOD 6=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 6=5/\ ~(4=0)/\ 0 MOD 6=0/\ 6 MOD 6=0/\ 7 MOD 6=1 /\ SUC 6=7
1019 /\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)/\ ~(6=0)
1020 /\ ~(5=1)/\ ~(5=2)/\ ~(5=3)/\ ~(5=4)`;;
1021
1022
1023
1024 let VV_IN_BALL_ANNULUS_TAC_6=
1025 fun (so:term)->
1026 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
1027 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1028 THEN MRESAL1_TAC th so[ARITH_6_TAC;IN])
1029 ;;
1030
1031
1032
1033
1034 let SCS_A_LE_NORM_6_IS_SCS=
1035 fun (so:term) (so1:term)->
1036 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1037 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1038 THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
1039 THEN ASM_TAC
1040 THEN REWRITE_TAC[periodic2]
1041 THEN REPEAT STRIP_TAC
1042 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
1043 THEN POP_ASSUM(fun th->
1044 ASM_TAC
1045 THEN REWRITE_TAC[th]
1046 THEN REPEAT STRIP_TAC
1047 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1048 THEN ASSUME_TAC th)
1049 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
1050 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1051 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1052 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
1053 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1054 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1055 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1056 THEN REPEAT RESA_TAC
1057 ;;
1058
1059 let PROVE_INEQUALITY_TAC_6=
1060 fun (th:term)->
1061 MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`)
1062 THEN RESA_TAC
1063 THENL[
1064 SCS_A_LE_NORM_6_IS_SCS th `6`;
1065 SCS_A_LE_NORM_6_IS_SCS th `1`;
1066 SCS_A_LE_NORM_6_IS_SCS th `2`;
1067 SCS_A_LE_NORM_6_IS_SCS th `3`;
1068 SCS_A_LE_NORM_6_IS_SCS th `4`;
1069 SCS_A_LE_NORM_6_IS_SCS th `5`];;
1070
1071
1072
1073
1074
1075
1076 let SCS_B_LE_NORM_6_IS_SCS=
1077 fun (so:term) (so1:term)->
1078 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1079 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1080 THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
1081 THEN ASM_TAC
1082 THEN REWRITE_TAC[periodic2]
1083 THEN REPEAT STRIP_TAC
1084 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
1085 THEN POP_ASSUM(fun th->
1086 ASM_TAC
1087 THEN REWRITE_TAC[th]
1088 THEN REPEAT STRIP_TAC
1089 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1090 THEN ASSUME_TAC th)
1091 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
1092 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1093 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1094 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
1095 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1096 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1097 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1098 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (6)`][ARITH_RULE`~(6=0)`;periodic]
1099 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1100 THEN REPEAT RESA_TAC
1101 ;;
1102
1103 let PROVE_INEQUALITY_TAC_6B=
1104 fun (th:term)->
1105 MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/  (j MOD 6=5)`)
1106 THEN RESA_TAC
1107 THENL[
1108 SCS_B_LE_NORM_6_IS_SCS th `6`;
1109 SCS_B_LE_NORM_6_IS_SCS th `1`;
1110 SCS_B_LE_NORM_6_IS_SCS th `2`;
1111 SCS_B_LE_NORM_6_IS_SCS th `3`;
1112 SCS_B_LE_NORM_6_IS_SCS th `4`;
1113 SCS_B_LE_NORM_6_IS_SCS th `5`];;
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126 let V_SY_EQ_IMAGE_VV_TAC6=
1127 fun (th:term)->
1128 ASM_REWRITE_TAC[]
1129 THEN EXISTS_TAC th
1130 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_6_TAC];;
1131
1132
1133 let PROVE_E_SY_EQ_MOD_TAC_6=
1134 fun (so:term)->
1135 EXISTS_TAC so
1136 THEN ASM_REWRITE_TAC[ARITH_6_TAC]
1137 ;;
1138
1139
1140
1141
1142
1143
1144
1145 let PROOF_E_EQ_TAC_6=
1146 fun (so:term)->
1147 EXISTS_TAC so
1148 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_6_TAC;]
1149 ;;
1150
1151
1152 let PROVE_E_SY_EQ_IMAGE_VV_6=
1153 fun (so:term) (so1:term)->
1154 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_6_TAC]
1155 THEN EXISTS_TAC so
1156 THEN ASM_REWRITE_TAC[ARITH_6_TAC];;
1157
1158
1159
1160
1161 let  IN_NOT_EMPTY_B1_SY_6_IS_SCS=prove_by_refinement(`is_scs_v39 s /\ scs_k_v39 s=6 /\
1162 dimindex(:M) = scs_k_v39 s/\
1163  matvec (v:real^3^M) =a/\
1164 (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\
1165  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
1166  CONDITION2_SY v
1167 /\ (!i. vv i =
1168 if i MOD scs_k_v39 s = 0 then row 6 v else
1169 if i MOD scs_k_v39 s = 1 then row 1 v else
1170 if i MOD scs_k_v39 s = 2 then row 2 v else
1171 if i MOD scs_k_v39 s = 3 then row 3 v else
1172 if i MOD scs_k_v39 s = 4 then row 4 v else
1173 row 5 v)
1174 ==> vv IN BBs_v39 s`,
1175 [
1176 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
1177 THEN REPEAT STRIP_TAC
1178 THEN ASM_TAC
1179 THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39;]
1180 THEN REPEAT RESA_TAC;
1181
1182
1183 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
1184 THEN REPEAT STRIP_TAC
1185 THEN ASM_REWRITE_TAC[]
1186 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1187 THEN MP_TAC(ARITH_RULE`x' MOD 6<6 ==> x' MOD 6 = 0 \/ x' MOD 6 = 1 \/ x' MOD 6 = 2 \/ x' MOD 6 = 3\/ x' MOD 6 = 4\/ x' MOD 6 = 5`)
1188 THEN RESA_TAC
1189 THENL[
1190 VV_IN_BALL_ANNULUS_TAC_6 `6`;
1191 VV_IN_BALL_ANNULUS_TAC_6 `1`;
1192 VV_IN_BALL_ANNULUS_TAC_6 `2`;
1193 VV_IN_BALL_ANNULUS_TAC_6 `3`;
1194 VV_IN_BALL_ANNULUS_TAC_6 `4`;
1195 VV_IN_BALL_ANNULUS_TAC_6 `5`];
1196
1197
1198 ASM_REWRITE_TAC[periodic]
1199 THEN GEN_TAC
1200 THEN MRESAL_TAC MOD_EQ[`i+6:num`;`i:num`;`6:num`;`1`][ARITH_RULE`1*A=A`];
1201
1202
1203 REWRITE_TAC[dist]
1204 THEN REPEAT GEN_TAC
1205 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;
1206
1207
1208 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1209 THEN GEN_TAC
1210 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];
1211
1212
1213 MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
1214 THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
1215 THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
1216 THEN RESA_TAC
1217 THENL[
1218 PROVE_INEQUALITY_TAC_6 `6`;
1219 PROVE_INEQUALITY_TAC_6 `1`;
1220 PROVE_INEQUALITY_TAC_6 `2`;
1221 PROVE_INEQUALITY_TAC_6 `3`;
1222 PROVE_INEQUALITY_TAC_6 `4`;
1223 PROVE_INEQUALITY_TAC_6 `5`];
1224
1225
1226
1227
1228
1229 REWRITE_TAC[dist]
1230 THEN REPEAT GEN_TAC
1231 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;
1232
1233
1234 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1235 THEN GEN_TAC
1236 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];
1237
1238
1239 MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
1240 THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
1241 THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
1242 THEN RESA_TAC
1243 THENL[
1244 PROVE_INEQUALITY_TAC_6B `6`;
1245 PROVE_INEQUALITY_TAC_6B `1`;
1246 PROVE_INEQUALITY_TAC_6B `2`;
1247 PROVE_INEQUALITY_TAC_6B `3`;
1248 PROVE_INEQUALITY_TAC_6B `4`;
1249 PROVE_INEQUALITY_TAC_6B `5`];
1250
1251
1252
1253 POP_ASSUM MP_TAC
1254 THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
1255 THEN STRIP_TAC
1256 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
1257
1258
1259 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
1260 THEN GEN_TAC
1261 THEN EQ_TAC;
1262
1263
1264 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5\/ i=6`]
1265 THEN STRIP_TAC
1266 THENL[
1267 V_SY_EQ_IMAGE_VV_TAC6 `1`;
1268 V_SY_EQ_IMAGE_VV_TAC6 `2`;
1269 V_SY_EQ_IMAGE_VV_TAC6 `3`;
1270 V_SY_EQ_IMAGE_VV_TAC6 `4`;
1271 V_SY_EQ_IMAGE_VV_TAC6 `5`;
1272 V_SY_EQ_IMAGE_VV_TAC6 `6`;];
1273
1274
1275 RESA_TAC
1276 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1277 THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3)\/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
1278 THEN RESA_TAC
1279 THENL[
1280 PROVE_E_SY_EQ_MOD_TAC_6 `6`;
1281 PROVE_E_SY_EQ_MOD_TAC_6 `1`;
1282 PROVE_E_SY_EQ_MOD_TAC_6 `2`;
1283 PROVE_E_SY_EQ_MOD_TAC_6 `3`;
1284 PROVE_E_SY_EQ_MOD_TAC_6 `4`;
1285 PROVE_E_SY_EQ_MOD_TAC_6 `5`;];
1286
1287
1288
1289 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
1290
1291
1292 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
1293 THEN ONCE_REWRITE_TAC[EXTENSION;]
1294 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1295 THEN GEN_TAC
1296 THEN EQ_TAC;
1297
1298
1299
1300 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
1301 THEN RESA_TAC
1302 THENL[
1303 PROOF_E_EQ_TAC_6`1`;
1304 PROOF_E_EQ_TAC_6`2`;
1305 PROOF_E_EQ_TAC_6`3`;
1306 PROOF_E_EQ_TAC_6`4`;
1307 PROOF_E_EQ_TAC_6`5`;
1308 PROOF_E_EQ_TAC_6`6`];
1309
1310
1311
1312 RESA_TAC
1313 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1314 THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
1315 THEN RESA_TAC
1316 THENL[
1317 PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
1318 PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
1319 PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
1320 PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
1321 PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
1322 PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];
1323
1324
1325 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
1326
1327
1328 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
1329 THEN ONCE_REWRITE_TAC[EXTENSION;]
1330 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1331 THEN GEN_TAC
1332 THEN EQ_TAC;
1333
1334
1335
1336 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
1337 THEN RESA_TAC
1338 THENL[
1339 PROOF_E_EQ_TAC_6`1`;
1340 PROOF_E_EQ_TAC_6`2`;
1341 PROOF_E_EQ_TAC_6`3`;
1342 PROOF_E_EQ_TAC_6`4`;
1343 PROOF_E_EQ_TAC_6`5`;
1344 PROOF_E_EQ_TAC_6`6`];
1345
1346
1347
1348 RESA_TAC
1349 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1350 THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
1351 THEN RESA_TAC
1352 THENL[
1353 PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
1354 PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
1355 PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
1356 PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
1357 PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
1358 PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];
1359
1360
1361 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1362 THEN ASM_REWRITE_TAC[]
1363 THEN REPEAT STRIP_TAC
1364 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
1365 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1366 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1367 THEN ASM_REWRITE_TAC[];
1368
1369
1370 ]);;
1371   (* }}} *)
1372
1373
1374 let XWITCCN_CASE_6_IS_SCS=prove_by_refinement(
1375 ` is_scs_v39 s /\ BBs_v39 s vv
1376 /\ scs_k_v39 s=6
1377 /\  dimindex(:M) =scs_k_v39 s
1378 /\  taustar_v39 s vv < &0
1379  ==> ~(BBprime_v39 s = {})`,
1380   (* {{{ proof *)
1381 [
1382 STRIP_TAC
1383 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1384 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
1385 THEN STRIP_TAC
1386 THEN MP_TAC NOT_EMPTY_CASE_6_IS_SCS
1387 THEN RESA_TAC
1388 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
1389 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1390          (change_type_v3 (scs_a_v39 s)),
1391          (change_type_v3 (scs_b_v39 s)),
1392          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1393          (\i. (1 + i) MOD scs_k_v39 s))`
1394 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1395          (change_type_v3 (scs_a_v39 s))`;`
1396          (change_type_v3 (scs_b_v39 s))`;`
1397          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1398          (\i. (1 + i) MOD scs_k_v39 s)`]
1399 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<6`;]
1400 THEN POP_ASSUM (fun th->
1401 POP_ASSUM MP_TAC
1402 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1403 THEN STRIP_TAC
1404 THEN ASSUME_TAC th)
1405 THEN REWRITE_TAC[BBprime_v39;IN]
1406 THEN ABBREV_TAC`( vv1 i =
1407 if i MOD scs_k_v39 s = 0 then row 6 v else
1408 if i MOD scs_k_v39 s = 1 then row 1 v else
1409 if i MOD scs_k_v39 s = 2 then row 2 v else
1410 if i MOD scs_k_v39 s = 3 then row 3 v else
1411 if i MOD scs_k_v39 s = 4 then row 4 v else
1412 row 5 (v:real^3^M))`
1413 THEN EXISTS_TAC`vv1:num->real^3`
1414 THEN STRIP_TAC;
1415
1416 ONCE_REWRITE_TAC[GSYM IN]
1417 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1418 THEN EXISTS_TAC`x:real^(M,3)finite_product`
1419 THEN EXISTS_TAC`v:real^3^M`
1420 THEN ASM_REWRITE_TAC[]
1421 THEN POP_ASSUM MP_TAC;
1422
1423 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 5; vv1 0] = v:real^3^M`
1424 ASSUME_TAC;
1425
1426 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
1427 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 0 MOD 6
1428 =0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 6=4/\ 5 MOD 6=5/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)/\ ~(0=5)`;]
1429 THEN ONCE_REWRITE_TAC[CART_EQ]
1430 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=6
1431  <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5\/ i=6`]
1432 THEN REPEAT RESA_TAC
1433 THEN
1434 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
1435 REWRITE_TAC[num_CONV `4`;num_CONV `5`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
1436 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
1437
1438
1439 STRIP_TAC;
1440
1441 GEN_TAC
1442 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
1443 THEN REPEAT STRIP_TAC
1444 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1445 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
1446 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
1447 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
1448 [`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;]
1449 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
1450 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
1451 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
1452 THEN MP_TAC th
1453 THEN REWRITE_TAC[IN]
1454 THEN STRIP_TAC)
1455 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
1456 THEN REWRITE_TAC[th]
1457 THEN RESA_TAC)
1458 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
1459 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1460 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`);
1461
1462 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1463 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
1464 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
1465 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
1466 [`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;]
1467 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1468 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
1469 THEN ASM_REWRITE_TAC[IN]
1470 THEN STRIP_TAC
1471 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1472 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1473 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5;vv 0]:real^3^M):real^(M,3)finite_product`)
1474 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
1475 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1476 THEN MP_TAC th)
1477 THEN ASM_REWRITE_TAC[]
1478 THEN POP_ASSUM MP_TAC
1479 THEN POP_ASSUM MP_TAC
1480 THEN REAL_ARITH_TAC;
1481
1482 ]);;
1483   (* }}} *)
1484
1485
1486 (****************CASE 3**************)
1487
1488 let IS_SCS_IN_BALL_ANNULUS_3=
1489 fun (so:term)->
1490 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1491 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1492 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1493 THEN STRIP_TAC
1494 THEN POP_ASSUM MATCH_MP_TAC
1495 THEN EXISTS_TAC so
1496 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1497 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
1498 ;;
1499
1500
1501
1502 let IN_IS_SCS_CASE_3=prove_by_refinement(
1503 ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv
1504 /\  dimindex(:M)= scs_k_v39 s
1505 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
1506 /\ matvec (v:real^3^M) =a
1507 ==>
1508 a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v }`,
1509   (* {{{ proof *)
1510 [
1511 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
1512 THEN STRIP_TAC;
1513
1514 EXISTS_TAC`v:real^3^M`
1515 THEN ASM_REWRITE_TAC[]
1516 THEN STRIP_TAC;
1517
1518 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`]
1519 THEN REPEAT STRIP_TAC
1520 THENL[
1521 IS_SCS_IN_BALL_ANNULUS_3 `1`;
1522 IS_SCS_IN_BALL_ANNULUS_3 `2`;
1523 IS_SCS_IN_BALL_ANNULUS_3 `0`];
1524
1525 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`]
1526 THEN REPEAT GEN_TAC
1527 THEN STRIP_TAC
1528 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
1529 THEN RESA_TAC
1530 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1531 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
1532 THEN ASM_TAC
1533 THEN REWRITE_TAC[is_scs_v39;periodic2]
1534 THEN STRIP_TAC
1535 THEN REPEAT DISCH_TAC
1536 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1537 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1538 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1539 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1540 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1541 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1542 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1543 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1544 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1545 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1546 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1547 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1548 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1549 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1550 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1551 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1552 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1553 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1554 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1555 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1556 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1557 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1558 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1559 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
1560 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];
1561
1562 EXISTS_TAC`v:real^3^M`
1563 THEN ASM_REWRITE_TAC[]
1564 THEN STRIP_TAC;
1565
1566 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`]
1567 THEN REPEAT STRIP_TAC
1568 THENL[
1569 IS_SCS_IN_BALL_ANNULUS_3 `1`;
1570 IS_SCS_IN_BALL_ANNULUS_3 `2`;
1571 IS_SCS_IN_BALL_ANNULUS_3 `0`];
1572
1573 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`]
1574 THEN REPEAT GEN_TAC
1575 THEN STRIP_TAC
1576 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
1577 THEN RESA_TAC
1578 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1579 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
1580 THEN ASM_TAC
1581 THEN REWRITE_TAC[is_scs_v39;periodic2]
1582 THEN STRIP_TAC
1583 THEN REPEAT DISCH_TAC
1584 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1585 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1586 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1587 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1588 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1589 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1590 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1591 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1592 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1593 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1594 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1595 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1596 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1597 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1598 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1599 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1600 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1601 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1602 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1603 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1604 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1605 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1606 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1607 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
1608 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];
1609 ]);;
1610
1611
1612
1613 let ARITH_3_TAC =ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 0 MOD 3=0/\ 1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ SUC 0=1 /\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ 0<3/\ a+0=a/\ 0+a=a/\ 3-1=2/\ 3-2=1/\ 3-0=3/\ 3-3=0`;;
1614
1615
1616
1617
1618 let VV_IN_BALL_ANNULUS_TAC_3=
1619 fun (so:term)->
1620 REPLICATE_TAC (30-23)(POP_ASSUM MP_TAC)
1621 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1622 THEN MRESAL1_TAC th so[ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
1623 ;;
1624
1625
1626 let SCS_A_LE_NORM_3_IS_SCS=
1627 fun (so:term) (so1:term)->
1628 REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
1629 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1630 THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
1631 THEN ASM_TAC
1632 THEN REWRITE_TAC[periodic2]
1633 THEN REPEAT STRIP_TAC
1634 THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
1635 THEN POP_ASSUM(fun th->
1636 ASM_TAC
1637 THEN REWRITE_TAC[th]
1638 THEN REPEAT STRIP_TAC
1639 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1640 THEN ASSUME_TAC th)
1641 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
1642 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1643 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1644 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
1645 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1646 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1647 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1648 THEN REPEAT RESA_TAC
1649 ;;
1650
1651 let PROVE_INEQUALITY_TAC_3=
1652 fun (th:term)->
1653 MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
1654 THEN RESA_TAC
1655 THENL[
1656 SCS_A_LE_NORM_3_IS_SCS th `3`;
1657 SCS_A_LE_NORM_3_IS_SCS th `1`;
1658 SCS_A_LE_NORM_3_IS_SCS th `2`;];;
1659
1660
1661
1662
1663 let SCS_B_LE_NORM_3_IS_SCS=
1664 fun (so:term) (so1:term)->
1665 REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
1666 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1667 THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
1668 THEN ASM_TAC
1669 THEN REWRITE_TAC[periodic2]
1670 THEN REPEAT STRIP_TAC
1671 THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
1672 THEN POP_ASSUM(fun th->
1673 ASM_TAC
1674 THEN REWRITE_TAC[th]
1675 THEN REPEAT STRIP_TAC
1676 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1677 THEN ASSUME_TAC th)
1678 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
1679 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1680 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1681 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
1682 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1683 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1684 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1685 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (3)`][ARITH_RULE`~(3=0)`;periodic]
1686 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1687 THEN REPEAT RESA_TAC
1688 ;;
1689
1690 let PROVE_INEQUALITY_TAC_3B=
1691 fun (th:term)->
1692 MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
1693 THEN RESA_TAC
1694 THENL[
1695 SCS_B_LE_NORM_3_IS_SCS th `3`;
1696 SCS_B_LE_NORM_3_IS_SCS th `1`;
1697 SCS_B_LE_NORM_3_IS_SCS th `2`;];;
1698
1699
1700
1701 let  IN_NOT_EMPTY_B1_SY_3_IS_SCS=prove_by_refinement(
1702 `is_scs_v39 s /\ scs_k_v39 s=3 /\
1703 dimindex(:M) = scs_k_v39 s/\
1704  matvec (v:real^3^M) =a/\
1705 (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\
1706  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ (!i. vv i =
1707 if i MOD scs_k_v39 s = 0 then row 3 v else
1708 if i MOD scs_k_v39 s = 1 then row 1 v else
1709 row 2 v)
1710 ==> vv IN BBs_v39 s`,
1711 [
1712 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
1713 THEN REPEAT STRIP_TAC
1714 THEN ASM_TAC
1715 THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
1716 THEN REPEAT RESA_TAC;
1717
1718 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
1719 THEN REPEAT STRIP_TAC
1720 THEN ASM_REWRITE_TAC[]
1721 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
1722 THEN MP_TAC(ARITH_RULE`x' MOD 3<3 ==> x' MOD 3 = 0 \/ x' MOD 3 = 1 \/ x' MOD 3 = 2 `)
1723 THEN RESA_TAC
1724 THENL[
1725 VV_IN_BALL_ANNULUS_TAC_3 `3`;
1726 VV_IN_BALL_ANNULUS_TAC_3 `1`;
1727 VV_IN_BALL_ANNULUS_TAC_3 `2`;];
1728
1729
1730 ASM_REWRITE_TAC[periodic]
1731 THEN GEN_TAC
1732 THEN MRESAL_TAC MOD_EQ[`i+3:num`;`i:num`;`3:num`;`1`][ARITH_RULE`1*A=A`];
1733
1734 REWRITE_TAC[dist]
1735 THEN REPEAT GEN_TAC
1736 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;
1737
1738 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1739 THEN GEN_TAC
1740 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];
1741
1742 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
1743 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
1744 THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
1745 THEN RESA_TAC
1746 THENL[
1747 PROVE_INEQUALITY_TAC_3 `3`;
1748 PROVE_INEQUALITY_TAC_3 `1`;
1749 PROVE_INEQUALITY_TAC_3 `2`;];
1750
1751
1752 REWRITE_TAC[dist]
1753 THEN REPEAT GEN_TAC
1754 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;
1755
1756 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1757 THEN GEN_TAC
1758 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];
1759
1760 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
1761 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
1762 THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
1763 THEN RESA_TAC
1764 THENL[
1765 PROVE_INEQUALITY_TAC_3B `3`;
1766 PROVE_INEQUALITY_TAC_3B `1`;
1767 PROVE_INEQUALITY_TAC_3B `2`;];
1768
1769 REWRITE_TAC[ARITH_RULE`3<=3`];
1770
1771 ]);;
1772   (* }}} *)
1773
1774
1775 let NOT_EMPTY_CASE_3_IS_SCS=prove_by_refinement(
1776 ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv
1777 /\  dimindex(:M)= scs_k_v39 s
1778 ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v  }={})`,
1779 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
1780 THEN STRIP_TAC
1781 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M`
1782 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
1783 THEN EXISTS_TAC`a:real^(M,3)finite_product`
1784 THEN MATCH_MP_TAC IN_IS_SCS_CASE_3
1785 THEN ASM_REWRITE_TAC[]]);;
1786
1787
1788
1789
1790
1791
1792 let J1_TS=new_definition `J1_TS (s:tri_sy)= {x| ?i. {i MOD 3,f_ts s (i MOD (3))} IN J_TS s /\ i IN 1..3 /\ x=i,SUC(i MOD (3))}`;;
1793
1794
1795
1796
1797 let d_fun3=new_definition `d_fun3 (s1:scs_v39)(s:tri_sy,l:real^(M,3)finite_product) = (d_ts s) + #0.1 * (if is_ear_v39 s1 then &1 else -- &1) * sum (J1_TS s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;
1798
1799
1800
1801 let FINITE_J1_TS=prove(`!s:tri_sy .
1802 FINITE (J1_TS s)`,
1803 GEN_TAC
1804 THEN REWRITE_TAC[J1_TS]
1805 THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (3)))`;`1..3`][FINITE_NUMSEG;IMAGE]
1806 THEN MATCH_MP_TAC FINITE_SUBSET
1807 THEN EXISTS_TAC`{y | ?x. x IN 1..(3) /\ y = x,SUC(x MOD (3))}`
1808 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]
1809 THEN REPEAT RESA_TAC
1810 THEN EXISTS_TAC`i:num`
1811 THEN ASM_REWRITE_TAC[]);;
1812
1813 let INDEX_J1_TS=prove(`!s:tri_sy .
1814 x IN J1_TS s ==> 1 <= FST x /\ FST x <= 3`,
1815 REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1816 THEN REPEAT STRIP_TAC
1817 THEN ASM_REWRITE_TAC[]);;
1818
1819
1820
1821 let CONTINUOUS_ON_D_FUN3=prove(`!s:tri_sy .
1822 k=3 /\
1823 k_ts s =k /\ dimindex(:M) =k/\ I_TS s= 0..k-1 /\ f_ts s=(\i. ((1+i):num MOD k))
1824 ==> lift o(\l:real^(M,3)finite_product. d_fun3 s1 (s,l)) continuous_on (
1825 {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (a_ts s) (b_ts s) v  })`,
1826 REPEAT STRIP_TAC
1827 THEN REWRITE_TAC[d_fun3;LIFT_ADD;o_DEF;]
1828 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1829 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
1830 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1831 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1832 THEN ASSUME_TAC FINITE_J1_TS
1833 THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:tri_sy`)
1834 THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF]
1835 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
1836 THEN ASM_REWRITE_TAC[]
1837 THEN REPEAT STRIP_TAC
1838 THEN REWRITE_TAC[LIFT_SUB]
1839 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1840 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
1841 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
1842 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1843 THEN STRIP_TAC
1844 THENL[
1845 MATCH_MP_TAC CONTINUOUS_ON_ROW
1846 THEN POP_ASSUM MP_TAC
1847 THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1848 THEN REPEAT RESA_TAC;
1849
1850 MATCH_MP_TAC CONTINUOUS_ON_ROW
1851 THEN POP_ASSUM MP_TAC
1852 THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1853 THEN REPEAT RESA_TAC
1854 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1855 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1856 THEN POP_ASSUM MP_TAC
1857 THEN ARITH_TAC]);;
1858
1859
1860
1861
1862
1863
1864 let tri_sy_explicit = prove_by_refinement(
1865  `!k d s a b J f. tri_stable k d s a b J f ==> k_ts (tri_sy (k,d,s, a,b,J,f)) =  k/\
1866 d_ts (tri_sy (k,d,s, a,b,J,f)) =  d /\
1867 a_ts (tri_sy (k,d,s, a,b,J,f)) =  a /\
1868 b_ts (tri_sy (k,d,s, a,b,J,f)) =  b /\
1869 J_TS (tri_sy (k,d,s, a,b,J,f)) =  J /\
1870 I_TS (tri_sy (k,d,s, a,b,J,f)) =  s /\
1871 f_ts (tri_sy (k,d,s, a,b,J,f)) =  f `,
1872   (* {{{ proof *)
1873   [   REWRITE_TAC[k_ts;d_ts;a_ts;b_ts;J_TS;I_TS;f_ts;tri_sy_tybij;]
1874 THEN MP_TAC tri_sy_tybij
1875 THEN STRIP_TAC
1876 THEN REPEAT GEN_TAC
1877 THEN STRIP_TAC
1878 THEN POP_ASSUM(fun th->
1879 POP_ASSUM (fun th1-> ASSUME_TAC th THEN MRESA1_TAC th1`(k,d,s,a,b,J,f):(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num))`))
1880 ]);;
1881   (* }}} *)
1882
1883
1884
1885
1886 let IN_B_SY1_COLLINEAR_CASE_3_IS_SCS=prove_by_refinement(
1887 `is_scs_v39 s
1888 /\ scs_k_v39 s=3/\
1889 dimindex(:M)= scs_k_v39 s
1890 ==>
1891  (!a. a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v  }
1892 ==> ~collinear{vec 0, row 1 (vecmats a),row 2 (vecmats a)}/\
1893 ~collinear{vec 0, row 1 (vecmats a),row 3 (vecmats a)}/\
1894 ~collinear{vec 0, row 2 (vecmats a),row 3 (vecmats a)})`,
1895   (* {{{ proof *)
1896 [
1897 REWRITE_TAC[IN_ELIM_THM;]
1898 THEN STRIP_TAC
1899 THEN GEN_TAC
1900 THEN STRIP_TAC
1901 THEN ABBREV_TAC`( vv i =
1902 if i MOD scs_k_v39 s = 0 then row 3 v else
1903 if i MOD scs_k_v39 s = 1 then row 1 v else
1904 row 2 (v:real^3^M))`
1905 THEN MP_TAC IN_NOT_EMPTY_B1_SY_3_IS_SCS
1906 THEN ASM_REWRITE_TAC[]
1907 THEN POP_ASSUM MP_TAC
1908 THEN ASM_REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1909 THEN RESA_TAC
1910 THEN STRIP_TAC
1911 THEN MP_TAC IS_SCS_NOT_COLLINEAR_BBs_CASE_3
1912 THEN RESA_TAC;
1913
1914 SUBGOAL_THEN`vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M
1915 =v`ASSUME_TAC;
1916
1917 REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
1918 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
1919 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
1920 THEN ONCE_REWRITE_TAC[CART_EQ]
1921 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
1922 THEN REPEAT RESA_TAC
1923 THEN
1924 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
1925 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
1926 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
1927
1928 MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`];
1929 ]);;
1930   (* }}} *)
1931
1932
1933
1934 let HDPLYGY_CASE_30=prove_by_refinement(
1935 `tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
1936 /\ 2<k
1937 /\ ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  } = {}:real^(M,3)finite_product->bool)
1938 /\ (!l. l IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }
1939 ==> ~collinear{vec 0, row 1 (vecmats l),row 2 (vecmats l)}/\
1940 ~collinear{vec 0, row 1 (vecmats l),row 3 (vecmats l)}/\
1941 ~collinear{vec 0, row 2 (vecmats l),row 3 (vecmats l)})
1942 /\ k_ts s = 3 /\ I_TS s = 0..3 - 1 /\ f_ts s = (\i. (1 + i) MOD 3)
1943 /\ a_ts s =a /\ b_ts s =b
1944 ==> ?x:real^(M,3)finite_product. x IN  ({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
1945 /\ (!y:real^(M,3)finite_product. y IN ({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
1946 ==> tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))
1947 -  d_fun3 s1 (s,x)
1948  <= tau3 (row 1 (vecmats y)) (row 2 (vecmats y)) (row 3 (vecmats y))
1949 -  d_fun3 s1 (s,y)
1950 )`,
1951   (* {{{ proof *)
1952 [
1953
1954 REPEAT STRIP_TAC
1955 THEN MP_TAC TRI_STABLE_K_EQ_3
1956 THEN RESA_TAC
1957 THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\x:real^(M,3)finite_product. tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))-  d_fun3 s1 (s,x))`;`{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }:real^(M,3)finite_product->bool`]
1958 THEN POP_ASSUM MATCH_MP_TAC
1959 THEN STRIP_TAC;
1960
1961 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1962 THEN MATCH_MP_TAC COMPACT_TRI_STABLE
1963 THEN ASM_REWRITE_TAC[];
1964
1965 SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
1966 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1967 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B <=> B/\ A`]
1968 THEN STRIP_TAC;
1969
1970 MRESAL_TAC(GEN_ALL CONTINUOUS_ON_D_FUN3)[`k:num`;`s1:scs_v39`;`s:tri_sy`][o_DEF];
1971
1972 POP_ASSUM MP_TAC
1973 THEN REPLICATE_TAC 5(REMOVE_ASSUM_TAC)
1974 THEN STRIP_TAC
1975 THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG;tau3; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
1976 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1977 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1978 THEN SIMP_TAC[o_DEF;LIFT_ADD;]
1979 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1980 THEN STRIP_TAC;
1981
1982
1983 SIMP_TAC[o_DEF;LIFT_ADD;]
1984 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1985 THEN STRIP_TAC;
1986
1987
1988 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
1989 THEN REPEAT STRIP_TAC
1990 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1991 THEN STRIP_TAC;
1992
1993
1994 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
1995 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1996 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1997 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1998 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1999 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2000 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2001 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2002 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2003 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2004 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2005 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2006 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2007 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2008 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2009 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2010 THEN ARITH_TAC;
2011
2012 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2013 THEN REPEAT STRIP_TAC
2014 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2015 THEN REWRITE_TAC[o_DEF]
2016 THEN STRIP_TAC
2017 THEN POP_ASSUM MATCH_MP_TAC
2018 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2019 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2020 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2021 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2022 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2023 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2024 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2025 THEN ASSUME_TAC th)
2026 THEN GEN_TAC
2027 THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2028
2029 ;
2030
2031
2032
2033 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
2034 THEN REPEAT STRIP_TAC
2035 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
2036 THEN STRIP_TAC;
2037
2038
2039 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
2040 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2041 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2042 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2043 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2044 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2045 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2046 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2047 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2048 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2049 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2050 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2051 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2052 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2053 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2054 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2055 THEN ARITH_TAC;
2056
2057 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2058 THEN REPEAT STRIP_TAC
2059 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2060 THEN REWRITE_TAC[o_DEF]
2061 THEN STRIP_TAC
2062 THEN POP_ASSUM MATCH_MP_TAC
2063 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2064 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2065 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2066 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2067 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2068 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2069 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2070 THEN ASSUME_TAC th)
2071 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2072 THEN ASM_REWRITE_TAC[]
2073 THEN GEN_TAC
2074 THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2076 THEN ASM_REWRITE_TAC[]
2077
2078 ;
2079
2080
2081
2082 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
2083 THEN REPEAT STRIP_TAC
2084 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
2085 THEN STRIP_TAC;
2086
2087
2088 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
2089 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2090 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2091 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2092 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2093 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2094 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2095 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2096 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2097 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2098 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2099 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2100 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2101 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2102 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2103 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2104 THEN ARITH_TAC;
2105
2106 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2107 THEN REPEAT STRIP_TAC
2108 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2109 THEN REWRITE_TAC[o_DEF]
2110 THEN STRIP_TAC
2111 THEN POP_ASSUM MATCH_MP_TAC
2112 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2113 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2114 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2115 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2116 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2117 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2118 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2119 THEN ASSUME_TAC th)
2120 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2121 THEN ASM_REWRITE_TAC[]
2122 THEN GEN_TAC
2123 THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2124 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2125 THEN ASM_REWRITE_TAC[];
2126 ]);;
2127   (* }}} *)
2128
2129
2130
2131
2132
2133
2134 let TAUSTAR_EQ_TAU_STAR_3_IS_SCS=prove_by_refinement(
2135 `is_scs_v39 s /\ BBs_v39 s vv
2136 /\ scs_k_v39 s=3
2137 /\ dimindex (:M)=3
2138 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
2139 /\ matvec (v:real^3^M) =a
2140 /\ tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2141          (change_type_v3 (scs_a_v39 s)),
2142          (change_type_v3 (scs_b_v39 s)),
2143          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2144          (\i. (1 + i) MOD scs_k_v39 s))=s1
2145 ==>  taustar_v39 s vv = tau3  (vv 1) (vv 2) (vv 0) -d_fun3 s (s1,a)`,
2146   (* {{{ proof *)
2147 [
2148
2149 REPEAT STRIP_TAC
2150 THEN ASM_REWRITE_TAC[taustar_v39;tau_star;LET_DEF;LET_END_DEF;ARITH_RULE`3<=3`;]
2151 THEN MATCH_MP_TAC(REAL_ARITH`a=b /\ c=d==> a -c= b- d`)
2152 THEN STRIP_TAC
2153 ;
2154
2155 REWRITE_TAC[tau3]
2156 THEN REAL_ARITH_TAC;
2157
2158 REWRITE_TAC[dsv_v39;d_fun3]
2159 THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
2160 THEN RESA_TAC
2161 THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2162          (change_type_v3 (scs_a_v39 s))`;`
2163          (change_type_v3 (scs_b_v39 s))`;`
2164          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2165          (\i. (1 + i) MOD scs_k_v39 s)`]
2166 THEN EXPAND_TAC"a"
2167 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2168 THEN MATCH_MP_TAC(REAL_ARITH`a=b ==> d+ a=d+b`)
2169 THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`)
2170 THEN RESA_TAC
2171
2172 ;
2173
2174
2175 MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * &1 * a= #0.1 * &1 *b`)
2176 THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
2177 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2178 THEN REWRITE_TAC[IN_ELIM_THM;dist]
2179 THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else  i, SUC(i MOD 3))`
2180 THEN STRIP_TAC;
2181
2182
2183 REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
2184 THEN REPEAT RESA_TAC
2185 THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
2186 THEN RESA_TAC;
2187
2188 REWRITE_TAC[ARITH_3_TAC]
2189 THEN EXISTS_TAC`0`
2190 THEN ASM_REWRITE_TAC[ARITH_3_TAC]
2191 THEN POP_ASSUM(fun th->
2192 ASM_TAC
2193 THEN REWRITE_TAC[th;ARITH_3_TAC]
2194 THEN REPEAT DISCH_TAC)
2195 THEN STRIP_TAC
2196 ;
2197
2198 MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
2199 THEN RESA_TAC;
2200
2201
2202 ASM_TAC
2203 THEN REWRITE_TAC[is_scs_v39;periodic2]
2204 THEN REPEAT STRIP_TAC
2205 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2206 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2207 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
2208 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2209 ;
2210
2211
2212 ASM_TAC
2213 THEN REWRITE_TAC[is_scs_v39;periodic2]
2214 THEN REPEAT STRIP_TAC
2215 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2216 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2217 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
2218 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2219 ;
2220
2221 REPEAT STRIP_TAC
2222 THEN POP_ASSUM MP_TAC
2223 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2224 THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
2225 THEN RESA_TAC
2226 THEN REWRITE_TAC[PAIR_EQ]
2227 THEN STRIP_TAC
2228 THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];
2229
2230
2231 EXISTS_TAC`i:num`
2232 THEN ASM_REWRITE_TAC[]
2233 THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;
2234
2235 MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
2236 THEN RESA_TAC
2237 THEN REWRITE_TAC[ARITH_3_TAC]
2238 ;
2239
2240 ASM_REWRITE_TAC[]
2241 THEN STRIP_TAC
2242 ;
2243
2244 REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
2245 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2246 THEN MP_TAC th)
2247 THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
2248 THEN STRIP_TAC
2249 THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
2250 ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
2251 THEN RESA_TAC;
2252
2253
2254 ASM_TAC
2255 THEN REWRITE_TAC[is_scs_v39;periodic2]
2256 THEN REPEAT STRIP_TAC
2257 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2258 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2259 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
2260 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2261 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2262 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2263 THEN REWRITE_TAC[ADD1;]
2264 THEN ONCE_REWRITE_TAC[ADD_SYM]
2265 THEN ASM_REWRITE_TAC[];
2266
2267
2268
2269 ASM_TAC
2270 THEN REWRITE_TAC[is_scs_v39;periodic2]
2271 THEN REPEAT STRIP_TAC
2272 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2273 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2274 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2275 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2276 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2277 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2278 THEN REWRITE_TAC[ADD1;]
2279 THEN ONCE_REWRITE_TAC[ADD_SYM]
2280 THEN ASM_REWRITE_TAC[];
2281
2282
2283
2284 REPEAT STRIP_TAC
2285 THEN POP_ASSUM MP_TAC
2286 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2287 THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
2288 THEN RESA_TAC
2289 ;
2290
2291 REWRITE_TAC[PAIR_EQ]
2292 THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
2293 THEN RESA_TAC;
2294
2295 REWRITE_TAC[PAIR_EQ]
2296 THEN RESA_TAC;
2297
2298
2299 REPEAT RESA_TAC
2300 THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
2301 ;
2302
2303 MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
2304 THEN RESA_TAC
2305 ;
2306
2307 EXISTS_TAC`3`
2308 THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
2309 THEN EXISTS_TAC`x:num`
2310 THEN EXISTS_TAC`SUC x:num`
2311 THEN ASM_REWRITE_TAC[ARITH_3_TAC];
2312
2313 EXISTS_TAC`x:num`
2314 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2315 THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
2316 THEN RESA_TAC
2317 THEN EXISTS_TAC`x:num`
2318 THEN EXISTS_TAC`SUC x`
2319 THEN ASM_REWRITE_TAC[]
2320 THEN ONCE_REWRITE_TAC[ADD_SYM]
2321 THEN REWRITE_TAC[ADD1]
2322 ;
2323
2324
2325 MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
2326 THEN RESA_TAC
2327 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
2328 THEN ASM_TAC
2329 THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
2330 THEN REPEAT STRIP_TAC
2331 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
2332 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])
2333
2334 ;
2335
2336
2337 (*************-1*************)
2338
2339 MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * -- &1 * a= #0.1 * -- &1 *b`)
2340 THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
2341 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2342 THEN REWRITE_TAC[IN_ELIM_THM;dist]
2343 THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else  i, SUC(i MOD 3))`
2344 THEN STRIP_TAC;
2345
2346
2347 REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
2348 THEN REPEAT RESA_TAC
2349 THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
2350 THEN RESA_TAC;
2351
2352 REWRITE_TAC[ARITH_3_TAC]
2353 THEN EXISTS_TAC`0`
2354 THEN ASM_REWRITE_TAC[ARITH_3_TAC]
2355 THEN POP_ASSUM(fun th->
2356 ASM_TAC
2357 THEN REWRITE_TAC[th;ARITH_3_TAC]
2358 THEN REPEAT DISCH_TAC)
2359 THEN STRIP_TAC
2360 ;
2361
2362 MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
2363 THEN RESA_TAC;
2364
2365
2366 ASM_TAC
2367 THEN REWRITE_TAC[is_scs_v39;periodic2]
2368 THEN REPEAT STRIP_TAC
2369 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2370 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2371 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
2372 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2373 ;
2374
2375
2376 ASM_TAC
2377 THEN REWRITE_TAC[is_scs_v39;periodic2]
2378 THEN REPEAT STRIP_TAC
2379 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2380 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2381 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
2382 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2383 ;
2384
2385 REPEAT STRIP_TAC
2386 THEN POP_ASSUM MP_TAC
2387 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2388 THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
2389 THEN RESA_TAC
2390 THEN REWRITE_TAC[PAIR_EQ]
2391 THEN STRIP_TAC
2392 THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];
2393
2394
2395 EXISTS_TAC`i:num`
2396 THEN ASM_REWRITE_TAC[]
2397 THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;
2398
2399 MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
2400 THEN RESA_TAC
2401 THEN REWRITE_TAC[ARITH_3_TAC]
2402 ;
2403
2404 ASM_REWRITE_TAC[]
2405 THEN STRIP_TAC
2406 ;
2407
2408 REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
2409 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2410 THEN MP_TAC th)
2411 THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
2412 THEN STRIP_TAC
2413 THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
2414 ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
2415 THEN RESA_TAC;
2416
2417
2418 ASM_TAC
2419 THEN REWRITE_TAC[is_scs_v39;periodic2]
2420 THEN REPEAT STRIP_TAC
2421 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2422 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2423 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
2424 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2425 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2426 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2427 THEN REWRITE_TAC[ADD1;]
2428 THEN ONCE_REWRITE_TAC[ADD_SYM]
2429 THEN ASM_REWRITE_TAC[];
2430
2431
2432
2433 ASM_TAC
2434 THEN REWRITE_TAC[is_scs_v39;periodic2]
2435 THEN REPEAT STRIP_TAC
2436 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2437 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2438 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2439 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2440 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2441 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2442 THEN REWRITE_TAC[ADD1;]
2443 THEN ONCE_REWRITE_TAC[ADD_SYM]
2444 THEN ASM_REWRITE_TAC[];
2445
2446
2447
2448 REPEAT STRIP_TAC
2449 THEN POP_ASSUM MP_TAC
2450 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2451 THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
2452 THEN RESA_TAC
2453 ;
2454
2455 REWRITE_TAC[PAIR_EQ]
2456 THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
2457 THEN RESA_TAC;
2458
2459 REWRITE_TAC[PAIR_EQ]
2460 THEN RESA_TAC;
2461
2462
2463 REPEAT RESA_TAC
2464 THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
2465 ;
2466
2467 MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
2468 THEN RESA_TAC
2469 ;
2470
2471 EXISTS_TAC`3`
2472 THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
2473 THEN EXISTS_TAC`x:num`
2474 THEN EXISTS_TAC`SUC x:num`
2475 THEN ASM_REWRITE_TAC[ARITH_3_TAC];
2476
2477 EXISTS_TAC`x:num`
2478 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2479 THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
2480 THEN RESA_TAC
2481 THEN EXISTS_TAC`x:num`
2482 THEN EXISTS_TAC`SUC x`
2483 THEN ASM_REWRITE_TAC[]
2484 THEN ONCE_REWRITE_TAC[ADD_SYM]
2485 THEN REWRITE_TAC[ADD1]
2486 ;
2487
2488
2489 MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
2490 THEN RESA_TAC
2491 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
2492 THEN ASM_TAC
2493 THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
2494 THEN REPEAT STRIP_TAC
2495 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
2496 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])
2497
2498 ;
2499
2500 ]);;
2501
2502
2503 let XWITCCN_CASE_3_IS_SCS=prove_by_refinement(
2504 `is_scs_v39 s /\ BBs_v39 s vv
2505 /\ scs_k_v39 s=3
2506 /\  dimindex(:M) =scs_k_v39 s
2507 /\  taustar_v39 s vv < &0
2508  ==> ~(BBprime_v39 s = {})`,
2509
2510   (* {{{ proof *)
2511 [
2512 STRIP_TAC
2513 THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
2514 THEN RESA_TAC
2515 THEN MP_TAC NOT_EMPTY_CASE_3_IS_SCS
2516 THEN RESA_TAC
2517 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
2518 THEN MP_TAC IN_B_SY1_COLLINEAR_CASE_3_IS_SCS
2519 THEN RESA_TAC
2520 THEN ABBREV_TAC`s1 =tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2521          (change_type_v3 (scs_a_v39 s)),
2522          (change_type_v3 (scs_b_v39 s)),
2523          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2524          (\i. (1 + i) MOD scs_k_v39 s))`
2525 THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2526          (change_type_v3 (scs_a_v39 s))`;`
2527          (change_type_v3 (scs_b_v39 s))`;`
2528          (change_type_v2 (scs_J_v39 s)(scs_k_v39 s))`;`
2529          (\i. (1 + i) MOD scs_k_v39 s)`]
2530 THEN  MRESAL_TAC (GEN_ALL HDPLYGY_CASE_30)[`scs_d_v39 s`;`(change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`scs_k_v39 s`;`(change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;`s:scs_v39`;`s1:tri_sy`][ARITH_RULE`2<3`]
2531 THEN POP_ASSUM (fun th->
2532 POP_ASSUM MP_TAC
2533 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
2534 THEN STRIP_TAC
2535 THEN ASSUME_TAC th)
2536 THEN REWRITE_TAC[BBprime_v39;IN]
2537 THEN ABBREV_TAC`( vv1 i =
2538 if i MOD scs_k_v39 s = 0 then row 3 v else
2539 if i MOD scs_k_v39 s = 1 then row 1 v else
2540 row 2 (v:real^3^M))`
2541 THEN EXISTS_TAC`vv1:num->real^3`
2542 THEN STRIP_TAC;
2543
2544 ONCE_REWRITE_TAC[GSYM IN]
2545 THEN MATCH_MP_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2546 THEN EXISTS_TAC`x:real^(M,3)finite_product`
2547 THEN EXISTS_TAC`v:real^3^M`
2548 THEN ASM_REWRITE_TAC[]
2549 THEN POP_ASSUM MP_TAC
2550 THEN RESA_TAC;
2551
2552 SUBGOAL_THEN`vector [ vv1 1; (vv1:num->real^3) 2;vv1 0] = v:real^3^M`
2553 ASSUME_TAC;
2554
2555 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
2556 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
2557 THEN ONCE_REWRITE_TAC[CART_EQ]
2558 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
2559 THEN REPEAT RESA_TAC
2560 THEN
2561 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
2562 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
2563 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
2564
2565 STRIP_TAC;
2566
2567 GEN_TAC
2568 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
2569 THEN REPEAT STRIP_TAC
2570 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2571 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
2572 THEN POP_ASSUM MP_TAC
2573 THEN POP_ASSUM MP_TAC
2574 THEN REWRITE_TAC[IN]
2575 THEN REPEAT STRIP_TAC
2576 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
2577 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(ww:num->real^3) 1; ww 2; ww 0]:real^3^M`;`ww:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`]
2578 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
2579 THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2580 THEN MRESAL_TAC VECTOR_3_3[`(ww:num->real^3) 1`;`(ww:num->real^3) 2`;`(ww:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2581 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2582 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2583 THEN MRESAL1_TAC th `matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID]);
2584
2585 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2586 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
2587 THEN POP_ASSUM MP_TAC
2588 THEN REWRITE_TAC[IN]
2589 THEN STRIP_TAC
2590 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
2591 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M`;`vv:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`]
2592 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
2593 THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2594 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2595 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2596 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2597 THEN MRESAL1_TAC th `matvec(vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID])
2598 THEN REPLICATE_TAC (31-4) (POP_ASSUM MP_TAC)
2599 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2600 THEN MP_TAC th
2601 THEN ASM_REWRITE_TAC[])
2602 THEN POP_ASSUM MP_TAC
2603 THEN REAL_ARITH_TAC;
2604 ]);;
2605   (* }}} *)
2606
2607
2608
2609
2610 let UXCKFPE=prove_by_refinement(
2611 ` !s vv . is_scs_v39 s /\ vv IN BBs_v39 s
2612 /\  taustar_v39 s vv < &0
2613  ==> ~(BBprime_v39 s = {})`,
2614
2615   (* {{{ proof *)
2616 [
2617 REPEAT GEN_TAC
2618 THEN REWRITE_TAC[IN]
2619 THEN DISCH_TAC
2620 THEN SUBGOAL_THEN`3<= scs_k_v39 s /\ scs_k_v39 s<=6` ASSUME_TAC;
2621
2622 ASM_TAC
2623 THEN REWRITE_TAC[is_scs_v39]
2624 THEN RESA_TAC;
2625
2626 MP_TAC(ARITH_RULE`3<= scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s=6`)
2627 THEN RESA_TAC;
2628
2629 MP_TAC(INST_TYPE [`:3`,`:M`]XWITCCN_CASE_3_IS_SCS)
2630 THEN ASM_REWRITE_TAC[DIMINDEX_3]
2631 THEN STRIP_TAC ;
2632
2633 MP_TAC(INST_TYPE [`:2+2`,`:M`]XWITCCN_CASE_4_IS_SCS)
2634 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
2635 THEN STRIP_TAC;
2636
2637 MP_TAC(INST_TYPE [`:2+3`,`:M`]XWITCCN_CASE_5_IS_SCS)
2638 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
2639 THEN STRIP_TAC ;
2640 MP_TAC(INST_TYPE [`:3+3`,`:M`]XWITCCN_CASE_6_IS_SCS)
2641 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
2642 THEN STRIP_TAC ]);;
2643
2644
2645
2646  end;;
2647
2648
2649 (*
2650 let check_completeness_claimA_concl =
2651   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
2652 *)
2653
2654
2655
2656