1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Wkeidft = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
92 let SUR_MOD_FUN=prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,
94 THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
97 EXISTS_TAC`p' MOD k- p MOD k`
98 THEN MRESA_TAC DIVISION[`p'`;`k`]
99 THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
101 THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
102 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
103 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
105 EXISTS_TAC`p' MOD k +k - p MOD k`
106 THEN MRESA_TAC DIVISION[`p`;`k`]
107 THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
109 THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
110 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
111 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
113 let TRANS_DIAG=prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
114 ==> (i+q) MOD k= q' MOD k `,
116 THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
117 THEN EXISTS_TAC`p:num`
118 THEN ASM_REWRITE_TAC[]
119 THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
120 THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
121 THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;
127 (*******************)
130 let scs_components = prove_by_refinement(
131 `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
132 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
133 scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,
136 REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
137 REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
138 REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
139 REWRITE_TAC[scs_str_v39];
141 BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
142 Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
146 let scs_inj = prove_by_refinement(
147 `!s s'. scs_basic_v39 s /\ scs_basic_v39 s' /\
148 scs_d_v39 s = scs_d_v39 s' /\
149 scs_k_v39 s = scs_k_v39 s' /\
150 (scs_a_v39 s = scs_a_v39 s') /\
151 (scs_b_v39 s = scs_b_v39 s')
156 REPEAT WEAKER_STRIP_TAC;
157 REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
158 REWRITE_TAC[scs_basic;unadorned_v39];
159 ONCE_REWRITE_TAC[EQ_SYM_EQ];
160 REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
161 REPEAT WEAKER_STRIP_TAC;
162 ONCE_REWRITE_TAC[GSYM scs_v39];
164 ASM_REWRITE_TAC[scs_components];
165 TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
166 BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
173 let DIAG_PSORT1=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
174 p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
175 ==> (psort k (i+i',i+j) = psort k (p',q'))`,
178 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
181 THEN POP_ASSUM MP_TAC
182 THEN MP_TAC TRANS_DIAG
184 THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
187 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
192 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
193 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
197 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
198 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
199 THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
202 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
205 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
208 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
213 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
214 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];
217 MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
220 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
223 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
228 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
229 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
235 let DIAG_PSORT2=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
236 p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
238 (psort k (i',j) = psort k (p,q))`,
240 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
243 THEN POP_ASSUM MP_TAC
244 THEN MP_TAC TRANS_DIAG
246 THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
249 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
254 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
255 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
259 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
260 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
262 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
266 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
269 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
272 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
277 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
278 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
280 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
283 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
286 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
291 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
292 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
297 let DIAG_PSORT=prove(
298 ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
299 p' + q = p + q' /\ ~(k=0)
301 ((psort k (i+i',i+j) = psort k (p',q'))
303 (psort k (i',j) = psort k (p,q)))`,
308 MATCH_MP_TAC DIAG_PSORT2
310 MATCH_MP_TAC DIAG_PSORT1
313 let TRANS_DIAG=prove(`
315 ==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,
316 SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;
319 let A_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
320 ==> scs_a_v39 s i j= scs_a_v39 s p q`,
321 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
323 THEN POP_ASSUM MP_TAC
324 THEN ABBREV_TAC`k=scs_k_v39 s`
325 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
327 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
332 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
333 THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
335 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
336 THEN REPEAT RESA_TAC);;
339 let B_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
340 ==> scs_b_v39 s i j= scs_b_v39 s p q`,
341 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
343 THEN POP_ASSUM MP_TAC
344 THEN ABBREV_TAC`k=scs_k_v39 s`
345 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
347 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
352 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
353 THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
355 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
356 THEN REPEAT RESA_TAC);;
358 let PROPERTY_OF_K_SCS=prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,
360 THEN MP_TAC Axjrpnc.is_scs_k_le_3
365 let WKEIDFT_A_concl = `!s s' a b a' b' p q p' q' i.
366 (let k = scs_k_v39 s in
367 (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
368 (!i. scs_a_v39 s i (i + 1) = a) /\
369 (!i. scs_b_v39 s i (i + 1) = b) /\
370 (!i. scs_a_v39 s' i (i + 1) = a) /\
371 (!i. scs_b_v39 s' i (i + 1) = b) /\
374 scs_d_v39 s = scs_d_v39 s' /\
375 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
376 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
377 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
378 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
379 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
380 (\j j'. scs_a_v39 s' (i + j) (i + j')) = scs_a_v39 s))`;;
384 let WKEIDFT_A=prove_by_refinement( WKEIDFT_A_concl,
386 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
388 THEN ABBREV_TAC`k= scs_k_v39 s`
389 THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
392 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
395 MP_TAC PROPERTY_OF_K_SCS
397 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
398 THEN MRESA_TAC A_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
399 THEN MRESA_TAC A_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
401 MP_TAC PROPERTY_OF_K_SCS
403 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
404 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`]
405 THEN MATCH_DICH_TAC (26-13)
406 THEN ASM_REWRITE_TAC[];
410 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
413 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
414 THEN MP_TAC PROPERTY_OF_K_SCS
416 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
417 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
419 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
420 THEN REPEAT RESA_TAC;
422 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
423 THEN MP_TAC PROPERTY_OF_K_SCS
425 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
426 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
427 THEN REWRITE_TAC[ADD1]
428 THEN THAYTHEL_TAC(26-6)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
429 THEN THAYTHE_TAC(26-4)[`x`];
432 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
433 THEN MP_TAC PROPERTY_OF_K_SCS
435 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
436 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
437 THEN REWRITE_TAC[ADD1]
438 THEN THAYTHEL_TAC(26-6)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
439 THEN THAYTHE_TAC(26-4)[`x'`]
441 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
442 THEN REPEAT RESA_TAC]);;
448 let WKEIDFT_B_concl = `!s s' a b a' b' p q p' q' a1 i.
449 (let k = scs_k_v39 s in
450 (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
451 (!i. scs_b_v39 s i i = a1) /\
452 (!i. scs_b_v39 s' i i = a1) /\
453 (!i. scs_a_v39 s i (i + 1) = a) /\
454 (!i. scs_b_v39 s i (i + 1) = b) /\
455 (!i. scs_a_v39 s' i (i + 1) = a) /\
456 (!i. scs_b_v39 s' i (i + 1) = b) /\
459 scs_d_v39 s = scs_d_v39 s' /\
460 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
461 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
462 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
463 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
464 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
465 (\j j'. scs_b_v39 s' (i + j) (i + j')) = scs_b_v39 s))`;;
469 let WKEIDFT_B=prove_by_refinement( WKEIDFT_B_concl,
471 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
473 THEN ABBREV_TAC`k= scs_k_v39 s`
474 THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
477 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
480 MP_TAC PROPERTY_OF_K_SCS
482 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
483 THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
484 THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
486 MP_TAC PROPERTY_OF_K_SCS
488 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
489 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`]
490 THEN MATCH_DICH_TAC (26-14)
491 THEN ASM_REWRITE_TAC[];
494 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
497 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
498 THEN MP_TAC PROPERTY_OF_K_SCS
500 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
501 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
503 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
504 THEN REPEAT RESA_TAC;
506 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
507 THEN MP_TAC PROPERTY_OF_K_SCS
509 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
510 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
511 THEN REWRITE_TAC[ADD1]
512 THEN THAYTHEL_TAC(26-7)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
513 THEN THAYTHE_TAC(26-5)[`x`];
515 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
516 THEN MP_TAC PROPERTY_OF_K_SCS
518 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
519 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
520 THEN REWRITE_TAC[ADD1]
521 THEN THAYTHEL_TAC(26-7)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
522 THEN THAYTHE_TAC(26-5)[`x'`]
524 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
525 THEN REPEAT RESA_TAC]);;
531 let WKEIDFT_EQU_concl = `
532 (let k = scs_k_v39 s in
533 (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
534 (!i. scs_b_v39 s i i = a1) /\
535 (!i. scs_b_v39 s' i i = a1) /\
536 (!i. scs_a_v39 s i (i + 1) = a) /\
537 (!i. scs_b_v39 s i (i + 1) = b) /\
538 (!i. scs_a_v39 s' i (i + 1) = a) /\
539 (!i. scs_b_v39 s' i (i + 1) = b) /\
542 scs_d_v39 s = scs_d_v39 s' /\
543 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
544 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
545 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
546 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
547 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' ==>
548 ?i. s'= scs_prop_equ_v39 s i))`;;
554 let WKEIDFT_EQU=prove( WKEIDFT_EQU_concl,
555 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
557 THEN ABBREV_TAC`k= scs_k_v39 s`
558 THEN MP_TAC PROPERTY_OF_K_SCS
560 THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
563 THEN EXISTS_TAC`i:num`
564 THEN MRESAL_TAC WKEIDFT_B[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`a1:real`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
565 THEN MRESAL_TAC WKEIDFT_A[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
566 THEN MATCH_MP_TAC scs_inj
567 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
570 let WKEIDFT_concl = `!s s' a b a' b' p q p' q'.
571 (let k = scs_k_v39 s in
572 (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
573 (!i. scs_b_v39 s i i = a1) /\
574 (!i. scs_b_v39 s' i i = a1) /\
575 (!i. scs_a_v39 s i (i + 1) = a) /\
576 (!i. scs_b_v39 s i (i + 1) = b) /\
577 (!i. scs_a_v39 s' i (i + 1) = a) /\
578 (!i. scs_b_v39 s' i (i + 1) = b) /\
581 scs_d_v39 s = scs_d_v39 s' /\
582 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
583 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
584 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
585 (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
586 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' ==>
587 scs_arrow_v39 {s} {s'}))`;;
591 let WKEIDFT_PRIME= prove(WKEIDFT_concl,
592 REWRITE_TAC[LET_DEF;LET_END_DEF]
594 THEN MP_TAC WKEIDFT_EQU
595 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
597 THEN MATCH_MP_TAC YXIONXL3
598 THEN ASM_REWRITE_TAC[]);;
602 (********************************)
604 let WKEIDFT_B_v2_concl = `!s a b a' b' p q p' q'.
605 (let k = scs_k_v39 s in
606 (is_scs_v39 s /\ scs_basic_v39 s /\
607 (!i. scs_a_v39 s i (i + 1) = a) /\
608 (!i. scs_b_v39 s i (i + 1) = b) /\
612 (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
613 (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
614 (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\
615 (!i. scs_b_v39 s i i = b1) /\
616 (i+p) MOD k = p' MOD k ==>
617 (\j j'. scs_b_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_b_v39 (scs_stab_diag_v39 s p q)))`;;
620 let WKEIDFT_B_V2=prove_by_refinement( WKEIDFT_B_v2_concl,
622 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
624 THEN ABBREV_TAC`k= scs_k_v39 s`;
626 MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
629 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
632 MP_TAC PROPERTY_OF_K_SCS
634 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
635 THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
636 THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
638 MP_TAC PROPERTY_OF_K_SCS
640 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
641 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] ;
644 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
647 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
649 THEN MP_TAC PROPERTY_OF_K_SCS
651 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
652 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
653 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
654 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`];
656 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
658 THEN MP_TAC PROPERTY_OF_K_SCS
660 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
661 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
662 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
663 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
664 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];
667 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
669 THEN MP_TAC PROPERTY_OF_K_SCS
671 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
672 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
673 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
674 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
675 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
677 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
678 THEN REPEAT RESA_TAC]);;
685 let WKEIDFT_A_v2_concl = `!s a b a' b' p q p' q'.
686 (let k = scs_k_v39 s in
687 (is_scs_v39 s /\ scs_basic_v39 s /\
688 (!i. scs_a_v39 s i (i + 1) = a) /\
689 (!i. scs_b_v39 s i (i + 1) = b) /\
693 (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
694 (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
695 (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\
696 (!i. scs_b_v39 s i i = b1) /\
697 (i+p) MOD k = p' MOD k ==>
698 (\j j'. scs_a_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_a_v39 (scs_stab_diag_v39 s p q)))`;;
701 let WKEIDFT_A_V2=prove_by_refinement( WKEIDFT_A_v2_concl,
703 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
705 THEN ABBREV_TAC`k= scs_k_v39 s`;
707 MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
710 MP_TAC PROPERTY_OF_K_SCS
712 THEN MRESAS_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`][];
715 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
718 MP_TAC PROPERTY_OF_K_SCS
720 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
721 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
722 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
724 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
725 THEN REPEAT RESA_TAC;
727 MP_TAC PROPERTY_OF_K_SCS
729 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
730 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
731 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
732 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];
734 MP_TAC PROPERTY_OF_K_SCS
736 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
737 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
738 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
739 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
741 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
742 THEN REPEAT RESA_TAC]);;
745 let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
746 /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
747 /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
748 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);;
753 let WKEIDFT_EQU_v2_concl = `
754 (let k = scs_k_v39 s in
755 (is_scs_v39 s /\ scs_basic_v39 s /\
756 (!i. scs_a_v39 s i (i + 1) = a) /\
757 (!i. scs_b_v39 s i (i + 1) = b) /\
762 (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
763 (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
764 (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\
765 (!i. scs_b_v39 s i i = b1) ==>
766 ?i. scs_stab_diag_v39 s p' q'= scs_prop_equ_v39 (scs_stab_diag_v39 s p q) i))`;;
769 let WKEIDFT_EQU_V2= prove(WKEIDFT_EQU_v2_concl,
770 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
772 THEN ABBREV_TAC`k= scs_k_v39 s`
773 THEN MP_TAC PROPERTY_OF_K_SCS
775 THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
778 THEN EXISTS_TAC`i:num`
779 THEN MRESAL_TAC WKEIDFT_B_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
780 THEN MRESAL_TAC WKEIDFT_A_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
781 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
788 THEN MATCH_MP_TAC scs_inj
789 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p'`;`q'`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
790 THEN ASM_SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
793 let WKEIDFT_concl = `!s a b a' b' p q p' q'.
794 (let k = scs_k_v39 s in
795 (is_scs_v39 s /\ scs_basic_v39 s /\
796 (!i. scs_a_v39 s i (i + 1) = a) /\
797 (!i. scs_b_v39 s i (i + 1) = b) /\
802 (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
803 (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
804 (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\
805 (!i. scs_b_v39 s i i = b1) ==>
806 scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;;
809 let WKEIDFT=prove(WKEIDFT_concl,
810 REWRITE_TAC[LET_DEF;LET_END_DEF]
812 THEN MP_TAC WKEIDFT_EQU_V2
813 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
815 THEN MATCH_MP_TAC YXIONXL3
816 THEN ASM_REWRITE_TAC[]
817 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]);;
828 let check_completeness_claimA_concl =
829 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)