text_formalization/local/JLXFDMJ.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 Jlxfdmj = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89
  90
  91
  92 let SCS_M_EQ_0= prove_by_refinement(
  93 ` CARD (scs_M s) = 0 /\ is_scs_v39 s
  94 ==> (!i. scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
  95 [
  96 STRIP_TAC
  97 THEN POP_ASSUM (fun th-> MP_TAC th
  98 THEN ASSUME_TAC th)
  99 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 100 THEN RESA_TAC
 101 THEN DICH_TAC (21)
 102 THEN REWRITE_TAC[scs_M]
 103 THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
 104 THEN SUBGOAL_THEN`FINITE
 105       {i | i < scs_k_v39 s /\
 106            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 107
 108 MATCH_MP_TAC FINITE_SUBSET
 109 THEN EXISTS_TAC`0..6`
 110 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 111 THEN GEN_TAC
 112 THEN DICH_TAC(20-3)
 113 THEN ARITH_TAC;
 114
 115 ABBREV_TAC`k=scs_k_v39 s`
 116 THEN RESA_TAC;
 117
 118 MRESA_TAC CARD_EQ_0[`{i | i < scs_k_v39 s /\
 119         (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 120 THEN POP_ASSUM MP_TAC
 121 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
 122 THEN STRIP_TAC
 123 THEN REPEAT GEN_TAC
 124 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 125 THEN RESA_TAC
 126 THEN THAYTHES_TAC 2[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
 127 THEN DICH_TAC 0
 128 THEN DICH_TAC 0
 129 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 130 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 131 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 132 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 133 THEN THAYTHES_TAC (29-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
 134 THEN POP_ASSUM MP_TAC
 135 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 136 THEN REAL_ARITH_TAC]);;
 137
 138
 139 let FINITE_SCS_M=prove(`is_scs_v39 s ==> FINITE (scs_M s)`,
 140 REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39;scs_M]
 141 THEN STRIP_TAC
 142 THEN MATCH_MP_TAC FINITE_SUBSET
 143 THEN EXISTS_TAC`0..(scs_k_v39 s)`
 144 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 145 THEN DICH_TAC(19-1)
 146 THEN ARITH_TAC);;
 147
 148 let SCS_A_2=prove(`is_scs_v39 s
 149 ==> !i. &2<= scs_a_v39 s i (i+1)`,
 150 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;GSYM ADD1]
 151 THEN RESA_TAC
 152 THEN STRIP_TAC
 153 THEN ABBREV_TAC`k=scs_k_v39 s`
 154 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;is_scs_v39;LET_DEF;LET_END_DEF]
 155 THEN THAYTHES_TAC (21-14)[`i MOD k`;`(SUC i) MOD k`][DIVISION;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;Qknvmlb.SUC_MOD_NOT_EQ;]
 156 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`]);;
 157
 158
 159 let SCS_M_EQ_1= prove_by_refinement(` scs_M s={x} /\ is_scs_v39 s
 160 ==> (!i. ~(i MOD scs_k_v39 s=x )==> scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
 161 [
 162 STRIP_TAC
 163 THEN POP_ASSUM (fun th-> MP_TAC th
 164 THEN ASSUME_TAC th)
 165 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 166 THEN RESA_TAC
 167 THEN DICH_TAC (21)
 168 THEN REWRITE_TAC[scs_M]
 169 THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
 170 THEN SUBGOAL_THEN`FINITE
 171       {i | i < scs_k_v39 s /\
 172            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 173
 174 MATCH_MP_TAC FINITE_SUBSET
 175 THEN EXISTS_TAC`0..6`
 176 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 177 THEN GEN_TAC
 178 THEN DICH_TAC(20-3)
 179 THEN ARITH_TAC;
 180
 181 ABBREV_TAC`k=scs_k_v39 s`
 182 THEN RESA_TAC;
 183
 184 POP_ASSUM MP_TAC
 185 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
 186 THEN STRIP_TAC
 187 THEN GEN_TAC
 188 THEN STRIP_TAC
 189 THEN THAYTHEL_ASM_TAC 1[`x:num`][]
 190 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 191 THEN RESA_TAC
 192 THEN DICH_TAC 5
 193 THEN ASM_SIMP_TAC[MOD_LT]
 194 THEN STRIP_TAC
 195 THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
 196 THEN DICH_TAC 0
 197 THEN DICH_TAC 0
 198 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 199 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 200 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 201 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 202 THEN THAYTHES_TAC (31-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
 203 THEN POP_ASSUM MP_TAC
 204 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
 205 THEN REAL_ARITH_TAC]);;
 206
 207 let SCS_M_LE_K=prove(` scs_M s={x}
 208 ==> x<scs_k_v39 s`,
 209 REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
 210 THEN STRIP_TAC
 211 THEN THAYTHE_TAC 0[`x:num`]);;
 212
 213
 214 let JLXFDMJ_concl = `
 215 main_nonlinear_terminal_v11
 216 ==>(!s (v:num->real^3) i.
 217   3< scs_k_v39 s/\
 218   is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
 219   (  dist(v i,v (i+1)) = &2) /\
 220   CARD (scs_M s) <= 1 /\
 221   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
 222 (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\
 223   scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1) <= &2 * h0 ==>
 224    (!j. ~(j MOD scs_k_v39 s IN scs_M s)==>   dist(v j , v(j+1)) = &2))`;;
 225
 226
 227 let JLXFDMJ = prove_by_refinement(
 228  JLXFDMJ_concl,
 229
 230 [
 231
 232 STRIP_TAC
 233 THEN REPEAT GEN_TAC
 234 THEN ABBREV_TAC`k= scs_k_v39 s`
 235 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 236 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 237 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 238 THEN REPEAT RESA_TAC
 239 THEN POP_ASSUM MP_TAC
 240 THEN MP_TAC SCS_A_2
 241 THEN RESA_TAC
 242 THEN SUBGOAL_THEN`!i. &2< scs_b_v39 s i (i + 1)`ASSUME_TAC;
 243
 244
 245 GEN_TAC
 246 THEN THAYTHE_TAC 0[`i'`]
 247 THEN THAYTHE_TAC 3[`i'`]
 248 THEN DICH_TAC 0
 249 THEN DICH_TAC 0
 250 THEN REAL_ARITH_TAC;
 251
 252 MP_TAC(ARITH_RULE`CARD (scs_M s)<=1==> CARD (scs_M s) =0 \/ CARD (scs_M s) =1`)
 253 THEN RESA_TAC;
 254
 255
 256
 257 MP_TAC FINITE_SCS_M
 258 THEN RESA_TAC
 259 THEN MRESA_TAC CARD_EQ_0[`scs_M s`]
 260 THEN STRIP_TAC
 261 THEN REMOVE_ASSUM_TAC
 262 THEN MP_TAC(ARITH_RULE`i<=j \/ j<=i:num`)
 263 THEN RESA_TAC
 264 ;
 265
 266
 267 POP_ASSUM MP_TAC
 268 THEN SPEC_TAC (`j:num`,`j:num`)
 269 THEN INDUCT_TAC
 270 ;
 271
 272 REWRITE_TAC[ARITH_RULE`i<= 0<=> i=0`]
 273 THEN STRIP_TAC
 274 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
 275 THEN REPEAT RESA_TAC)
 276 ;
 277
 278
 279 STRIP_TAC
 280 THEN MP_TAC(ARITH_RULE`i<= SUC j==> SUC j=i \/ i<=j`)
 281 THEN RESA_TAC
 282 THEN DICH_TAC 2
 283 THEN RESA_TAC
 284 THEN MP_TAC SCS_M_EQ_0
 285 THEN RESA_TAC
 286 THEN THAYTHEL_ASM_TAC(24-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
 287 THEN THAYTHEL_ASM_TAC(25-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
 288 THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
 289 THEN RESA_TAC
 290 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 291 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 292 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 293 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 294 THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 295 THEN MP_TAC Cqaoqlr.CQAOQLR
 296 THEN RESA_TAC
 297 THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 298 THEN MATCH_DICH_TAC 0
 299 THEN THAYTHEL_ASM_TAC (32-22)[`j`][ARITH_RULE`SUC i= i+1`]
 300 THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`];
 301
 302
 303
 304 POP_ASSUM MP_TAC
 305 THEN ABBREV_TAC`t= i-j:num`
 306 THEN POP_ASSUM MP_TAC
 307 THEN SPEC_TAC (`j:num`,`j:num`)
 308 THEN SPEC_TAC (`t:num`,`t:num`)
 309 THEN INDUCT_TAC
 310 ;
 311
 312
 313
 314 REPEAT STRIP_TAC
 315 THEN MP_TAC(ARITH_RULE`i-j=0/\ j<=i ==> j=i:num`)
 316 THEN RESA_TAC;
 317
 318
 319 REPEAT RESA_TAC
 320 THEN MP_TAC(ARITH_RULE`i-j= SUC t/\ j<=i ==> i- SUC j=t/\ SUC j<= i:num`)
 321 THEN RESA_TAC
 322 THEN THAYTHEL_TAC 4 [`SUC j`][ARITH_RULE`SUC i= i+1/\ (i+1)+1=i+2`]
 323 THEN MP_TAC SCS_M_EQ_0
 324 THEN RESA_TAC
 325 THEN THAYTHEL_ASM_TAC(26-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
 326 THEN THAYTHEL_ASM_TAC(27-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
 327 THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
 328 THEN RESA_TAC
 329 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 330 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 331 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 332 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 333 THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 334 THEN MP_TAC Cqaoqlr.CQAOQLR
 335 THEN RESA_TAC
 336 THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 337 THEN MATCH_DICH_TAC 0
 338 THEN THAYTHEL_ASM_TAC (34-24)[`j`][ARITH_RULE`SUC i= i+1`]
 339 THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`]
 340 ;
 341
 342
 343
 344 MP_TAC FINITE_SCS_M
 345 THEN RESA_TAC
 346 THEN MRESAL_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][IN_SING]
 347 THEN MP_TAC SCS_M_EQ_1
 348 THEN RESA_TAC
 349 THEN SUBGOAL_THEN`~(i MOD k=x)` ASSUME_TAC;
 350
 351
 352 STRIP_TAC
 353 THEN DICH_TAC 2
 354 THEN ASM_REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
 355 THEN STRIP_TAC
 356 THEN THAYTHE_TAC 0[`i MOD k`]
 357 THEN POP_ASSUM MP_TAC
 358 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`x`;`k`][MOD_LT;ARITH_RULE`3<k==> ~(k=0)`]
 359 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
 360 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
 361 THEN ASM_REWRITE_TAC[ADD1;REAL_ARITH`~(a<b)<=> b<=a`;REAL_ARITH`a<=a`]
 362 ;
 363
 364
 365
 366
 367
 368 MP_TAC(ARITH_RULE`~(i MOD k= x)==>  i MOD k< x\/ x< i MOD k`)
 369 THEN RESA_TAC
 370 ;
 371
 372
 373
 374
 375 SUBGOAL_THEN `!t. t< i MOD k + k - x ==> dist ((v:num->real^3) (i MOD k+k - t),v ( (i MOD k+k -t) + 1)) = &2`
 376 ASSUME_TAC
 377 ;
 378
 379
 380
 381 INDUCT_TAC
 382 ;
 383
 384
 385 STRIP_TAC
 386 THEN REWRITE_TAC[ARITH_RULE`a-0=a/\ (1 * k + i MOD k) + 1= 1*k+SUC(i MOD k)/\ i MOD k +k=1*k+ i MOD k`]
 387 THEN DICH_TAC(24-7)
 388 THEN REWRITE_TAC[IN]
 389 THEN STRIP_TAC
 390 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 391 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+i MOD k`;`v:num->real^3`;`(1*k+i MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
 392 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(i MOD k)`;`v:num->real^3`;`(1*k+SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
 393 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
 394 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;` i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 395 ;
 396
 397
 398
 399 STRIP_TAC
 400 THEN MP_TAC SCS_M_LE_K
 401 THEN RESA_TAC
 402 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k ==> t< i MOD k+k-x`)
 403 THEN RESA_TAC
 404 THEN DICH_TAC 3
 405 THEN RESA_TAC
 406 THEN POP_ASSUM MP_TAC
 407 THEN ABBREV_TAC`j1= i MOD k + k - (t+1)`
 408 THEN MRESA_TAC Ssrnat.subn_sub[`t`;`k`;`1`]
 409 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> i MOD k+ k-t=(i MOD k +k-t-1)+1 `)
 410 THEN RESA_TAC
 411 THEN ASM_REWRITE_TAC[ADD1;ARITH_RULE`(i+1)+1=i+2`]
 412 THEN STRIP_TAC
 413 THEN THAYTHEL_ASM_TAC(30-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
 414 THEN THAYTHEL_ASM_TAC(31-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
 415 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
 416 THEN RESA_TAC
 417 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 418 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 419 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 420 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 421 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 422 THEN MP_TAC Cqaoqlr.CQAOQLR
 423 THEN RESA_TAC
 424 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 425 THEN MATCH_DICH_TAC 0
 426 THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;
 427
 428 MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
 429 THEN RESA_TAC
 430 ;
 431
 432
 433
 434
 435 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
 436 THEN RESA_TAC
 437 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
 438
 439
 440 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= i MOD k +k-(t+1) ==>  i MOD k +k-(t+1) = 1*k+ i MOD k-(t+1)/\ i MOD k-(t+1)<k/\ ~(i MOD k - (t + 1) = x)`)
 441 THEN RESA_TAC
 442 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
 443
 444
 445
 446
 447
 448 SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;
 449
 450 MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
 451 THEN RESA_TAC
 452 ;
 453
 454
 455
 456
 457 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
 458 THEN RESA_TAC
 459 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
 460
 461
 462 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x  ==>    (SUC(i MOD k) +k-(t+1)) =(i MOD k +k-(t+1)) +1`)
 463 THEN RESA_TAC
 464 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= (SUC(i MOD k) +k-(t+1)) ==>  (i MOD k +k-(t+1))+1 = 1*k+ SUC(i MOD k)-(t+1)/\  (i MOD k +k-(t+1)) +1=(SUC(i MOD k) +k-(t+1)) /\ SUC(i MOD k)-(t+1)<k/\ ~(i MOD k - t = x) `)
 465 THEN RESA_TAC
 466 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
 467 THEN ASM_REWRITE_TAC[ADD1;SUB_ADD_RCANCEL];
 468
 469
 470 THAYTHEL_ASM_TAC (40-19)[`j1`][ARITH_RULE`SUC i= i+1`;MOD_LT]
 471 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
 472 ;
 473
 474
 475
 476
 477 SUBGOAL_THEN `!t. t< x-i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+ t) + 1)) = &2`
 478 ASSUME_TAC
 479 ;
 480
 481
 482 REMOVE_ASSUM_TAC
 483 THEN INDUCT_TAC
 484 ;
 485
 486
 487
 488
 489 STRIP_TAC
 490 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
 491 THEN DICH_TAC(24-7)
 492 THEN REWRITE_TAC[IN]
 493 THEN STRIP_TAC
 494 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 495 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
 496 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
 497 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 498 ;
 499
 500 STRIP_TAC
 501 THEN MP_TAC(ARITH_RULE`i MOD k< x/\ SUC t< x - i MOD k
 502 ==> t< x - i MOD k`)
 503 THEN RESA_TAC
 504 THEN DICH_TAC 2
 505 THEN RESA_TAC
 506 THEN ABBREV_TAC`j1=i MOD k+t`
 507 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
 508 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
 509 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
 510 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
 511 THEN RESA_TAC
 512 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 513 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 514 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 515 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 516 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 517 THEN MP_TAC Cqaoqlr.CQAOQLR
 518 THEN RESA_TAC
 519 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 520 THEN MATCH_DICH_TAC 0
 521 THEN MP_TAC SCS_M_LE_K
 522 THEN RESA_TAC
 523 THEN MP_TAC(ARITH_RULE`SUC t < x - i MOD k/\ x<k /\ i MOD k<x/\ 3<k==>  i MOD k + t <k /\ ~(i MOD k+t= x)/\ ~((i MOD k +t)+1=x)/\ (i MOD k + t)+1 <k/\ ~(k=0)`)
 524 THEN RESA_TAC;
 525
 526
 527
 528 THAYTHEL_ASM_TAC (41-19)[`j1`][ARITH_RULE` SUC i= i+1`;]
 529 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
 530 THEN DICH_TAC 1
 531 THEN DICH_TAC 1
 532 THEN ASM_SIMP_TAC[MOD_LT];
 533
 534
 535
 536 MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
 537 THEN RESA_TAC
 538 ;
 539
 540
 541 MP_TAC SCS_M_LE_K
 542 THEN RESA_TAC
 543 THEN MP_TAC(ARITH_RULE`j MOD k <= i MOD k /\ i MOD k< x /\ x<k
 544 ==> (i MOD k- j MOD k) < i MOD k + k - x /\ i MOD k + k - (i MOD k - j MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
 545 THEN RESA_TAC
 546 THEN THAYTHE_TAC 6[`i MOD k - j MOD k`]
 547 THEN DICH_TAC 0
 548 THEN DICH_TAC(29-7)
 549 THEN REWRITE_TAC[IN]
 550 THEN STRIP_TAC
 551 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 552 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+j MOD k`;`v:num->real^3`;`(1*k+j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 553 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 554 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(j MOD k)`;`v:num->real^3`;`(1*k+ SUC(j MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 555 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 556 ;
 557
 558
 559
 560
 561 STRIP_TAC
 562 THEN MP_TAC(ARITH_RULE`~(j MOD k= x)==> j MOD k< x \/ x< j MOD k`)
 563 THEN RESA_TAC
 564 ;
 565
 566
 567 MP_TAC(ARITH_RULE`j MOD k< x/\ i MOD k<= j MOD k==> j MOD k- i MOD k< x- i MOD k /\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
 568 THEN RESA_TAC
 569 THEN THAYTHE_TAC (30-25)[`j MOD k- i MOD k`]
 570 THEN DICH_TAC 0
 571 THEN DICH_TAC(29-7)
 572 THEN REWRITE_TAC[IN]
 573 THEN STRIP_TAC
 574 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 575 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 576 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 577 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 578 ;
 579
 580
 581
 582 MP_TAC(ARITH_RULE`i MOD k< x/\ x< j MOD k /\ j MOD k<k==> i MOD k+k- j MOD k< i MOD k+ k- x
 583 /\ i MOD k +k -(i MOD k+k- j MOD k)= j MOD k`)
 584 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;DIVISION]
 585 THEN RESA_TAC
 586 THEN THAYTHE_TAC (30-24)[`i MOD k+k- j MOD k`]
 587 THEN DICH_TAC 0
 588 THEN DICH_TAC(29-7)
 589 THEN REWRITE_TAC[IN]
 590 THEN STRIP_TAC
 591 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 592 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 593 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 594 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 595 ;
 596
 597
 598
 599
 600
 601
 602 SUBGOAL_THEN `!t. t< x +k- i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+t) + 1)) = &2`
 603 ASSUME_TAC
 604 ;
 605
 606
 607
 608 INDUCT_TAC
 609 ;
 610
 611
 612
 613
 614 STRIP_TAC
 615 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
 616 THEN DICH_TAC(24-7)
 617 THEN REWRITE_TAC[IN]
 618 THEN STRIP_TAC
 619 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 620 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
 621 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
 622 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 623 ;
 624
 625 STRIP_TAC
 626 THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t< x +k- i MOD k
 627 ==> t< x +k - i MOD k`)
 628 THEN RESA_TAC
 629 THEN DICH_TAC 2
 630 THEN RESA_TAC
 631 THEN ABBREV_TAC`j1=i MOD k+t`
 632 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
 633 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
 634 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
 635 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
 636 THEN RESA_TAC
 637 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 638 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 639 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 640 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 641 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 642 THEN MP_TAC Cqaoqlr.CQAOQLR
 643 THEN RESA_TAC
 644 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 645 THEN MATCH_DICH_TAC 0
 646 THEN MP_TAC SCS_M_LE_K
 647 THEN RESA_TAC
 648 THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;
 649
 650 MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
 651 THEN RESA_TAC
 652 ;
 653
 654
 655
 656
 657 MP_TAC(ARITH_RULE`x<i MOD k ==> ~(i MOD k +t =x) `)
 658 THEN RESA_TAC
 659 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
 660
 661
 662 MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= i MOD k +t ==>  (i MOD k+t) -k<k/\ ~((i MOD k+t) -k= x)/\ i MOD k+t = 1*k+ (i MOD k+t) -k`)
 663 THEN RESA_TAC
 664 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 665 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
 666
 667
 668
 669
 670
 671 SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;
 672
 673 MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
 674 THEN RESA_TAC
 675 ;
 676
 677
 678 MP_TAC(ARITH_RULE`x<i MOD k ==> ~((i MOD k +t) +1=x) `)
 679 THEN RESA_TAC
 680 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
 681
 682
 683 MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= (i MOD k +t)+1 ==>  ((i MOD k+t)+1) -k<k/\ ~(((i MOD k+t) +1)-k= x)/\ (i MOD k+t)+1 = 1*k+ ((i MOD k+t) +1)-k`)
 684 THEN RESA_TAC
 685 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 686 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
 687
 688
 689 THAYTHEL_ASM_TAC (38-19)[`j1`][ADD1]
 690 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`]
 691 ;
 692
 693
 694
 695
 696
 697 SUBGOAL_THEN `!t. t< i MOD k- x ==> dist ((v:num->real^3) (i MOD k-t),v ( (i MOD k-t) + 1)) = &2`
 698 ASSUME_TAC
 699 ;
 700
 701
 702 REMOVE_ASSUM_TAC
 703 THEN INDUCT_TAC
 704 ;
 705
 706
 707 STRIP_TAC
 708 THEN REWRITE_TAC[ARITH_RULE`a-0=a`;GSYM ADD1]
 709 THEN DICH_TAC(24-7)
 710 THEN REWRITE_TAC[IN]
 711 THEN STRIP_TAC
 712 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 713 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
 714 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
 715 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 716 ;
 717
 718 STRIP_TAC
 719 THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t<  i MOD k-x
 720 ==> t<  i MOD k- x`)
 721 THEN RESA_TAC
 722 THEN DICH_TAC 2
 723 THEN RESA_TAC
 724 THEN ABBREV_TAC`j1=i MOD k-(t+1)`
 725 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k +  t)+1/\ (j1 + 1) + 1= j1+2`]
 726 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
 727 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
 728 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
 729 THEN RESA_TAC
 730 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 731 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 732 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 733 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
 734 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
 735 THEN DICH_TAC(35-24)
 736 THEN MP_TAC(ARITH_RULE`SUC t< i MOD k- x /\ x< i MOD k/\ i MOD k<k==> i MOD k - t=(i MOD k - (t+1)) + 1/\ i MOD k - t +1=(i MOD k - (t+1)) + 2/\ i MOD k - (t+1)<k/\ (i MOD k - (t+1))+1<k/\ ~((i MOD k - (t+1))+1= x)/\ ~((i MOD k - (t+1))= x)`)
 737 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
 738 THEN RESA_TAC
 739 THEN RESA_TAC
 740 THEN MP_TAC Cqaoqlr.CQAOQLR
 741 THEN RESA_TAC
 742 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
 743 THEN MATCH_DICH_TAC 0
 744 ;
 745
 746
 747
 748 THAYTHEL_ASM_TAC (41-19)[`j1`][ADD1;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
 749 THEN THAYTHES_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
 750 ;
 751
 752
 753
 754
 755
 756 STRIP_TAC
 757 THEN MP_TAC(ARITH_RULE`~(j MOD k = x)==> j MOD k< x\/ x< j MOD k`)
 758 THEN RESA_TAC;
 759
 760
 761
 762 MP_TAC(ARITH_RULE`j MOD k< x/\ x< i MOD k/\ i MOD k<k==> j MOD k+ k- i MOD k< x+k- i MOD k/\ i MOD k+(j MOD k+ k- i MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
 763 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
 764 THEN RESA_TAC
 765 THEN THAYTHE_TAC 6[`j MOD k+ k- i MOD k`]
 766 THEN DICH_TAC 0
 767 THEN DICH_TAC(29-7)
 768 THEN REWRITE_TAC[IN]
 769 THEN STRIP_TAC
 770 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 771 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + j MOD k`;`v:num->real^3`;`(1 * k + j MOD k)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 772 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 773 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + SUC(j MOD k)`;`v:num->real^3`;`(1 * k + SUC(j MOD k))MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 774 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;` SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
 775 ;
 776
 777
 778 MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
 779 THEN RESA_TAC
 780 ;
 781
 782
 783 MP_TAC(ARITH_RULE`x< j MOD k/\ j MOD k<= i MOD k==> i MOD k- j MOD k< i MOD k - x/\ i MOD k- (i MOD k- j MOD k)= j MOD k`)
 784 THEN RESA_TAC
 785 THEN THAYTHE_TAC (30-25)[`i MOD k- j MOD k`]
 786 THEN DICH_TAC 0
 787 THEN DICH_TAC(29-7)
 788 THEN REWRITE_TAC[IN]
 789 THEN STRIP_TAC
 790 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 791 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 792 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 793 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 794 ;
 795
 796
 797 MP_TAC(ARITH_RULE`i MOD k<= j MOD k /\ j MOD k< k ==> j MOD k- i MOD k< x+k-i MOD k/\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
 798 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
 799 THEN RESA_TAC
 800 THEN THAYTHE_TAC (30-24)[`j MOD k- i MOD k`]
 801 THEN DICH_TAC 0
 802 THEN DICH_TAC(29-7)
 803 THEN REWRITE_TAC[IN]
 804 THEN STRIP_TAC
 805 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 806 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
 807 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 808 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
 809 ;
 810
 811 ]);;
 812
 813
 814
 815  end;;
 816
 817
 818 (*
 819 let check_completeness_claimA_concl =
 820   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 821 *)
 822
 823
 824
 825