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 Ppbtydq = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
92 let PPBTYDQ_concl = `!(u:real^3) v p. ~collinear {vec 0,v,p} /\ ~collinear {vec 0,u,p} /\
93 arcV (vec 0) u p + arcV (vec 0) p v < pi ==> ~(vec 0 IN conv{u,v})`;;
97 let PPBTYDQ= prove_by_refinement((PPBTYDQ_concl),
100 THEN POP_ASSUM MP_TAC
101 THEN ABBREV_TAC `e= u cross (p:real^3)`
102 THEN SUBGOAL_THEN`orthogonal e (u:real^3)`ASSUME_TAC;
105 THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];
108 SUBGOAL_THEN`orthogonal e (p:real^3)`ASSUME_TAC;
111 THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];
114 REWRITE_TAC[Collect_geom.CONV_SET2;IN_ELIM_THM;VECTOR_ARITH`vec 0 = a % u + b % v<=> b % v = (--a) % u `]
115 THEN REPEAT STRIP_TAC
116 THEN POP_ASSUM MP_TAC
117 THEN POP_ASSUM MP_TAC
118 THEN MP_TAC(REAL_ARITH`&0<=b==> b= &0\/ &0< b`)
122 REWRITE_TAC[VECTOR_ARITH`&0 % v = --a % u<=> a % u= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH`a + &0= &1<=> a= &1`]
124 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
125 THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];
128 MP_TAC(REAL_ARITH`&0<=a==> a= &0\/ &0< a`)
132 REWRITE_TAC[VECTOR_ARITH`b % v = -- &0 % u<=> b % v= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH` &0+a= &1<=> a= &1`]
134 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
135 THEN MRESA_TAC th3[`vec 0:real^3`;`v`;`p`];
138 THEN MP_TAC(SET_RULE`b % v = --a % u
139 ==> (inv b) %b % v = (inv b) % --a % u:real^3`)
140 THEN REWRITE_TAC[VECTOR_ARITH`a%b%c=(a*b)%c`]
141 THEN ASM_REWRITE_TAC[]
142 THEN MP_TAC(ARITH_RULE`&0< b==> ~(b= &0)`)
144 THEN ASM_SIMP_TAC[REAL_MUL_LINV;VECTOR_ARITH`&1 %v= v`]
145 THEN SUBGOAL_THEN`(inv b * --a)< &0` ASSUME_TAC;
147 MATCH_MP_TAC(REAL_ARITH`&0<(inv b *a)==> (inv b * --a)< &0`)
148 THEN MATCH_MP_TAC REAL_LT_MUL
149 THEN ASM_REWRITE_TAC[]
150 THEN MATCH_MP_TAC REAL_LT_INV
151 THEN ASM_REWRITE_TAC[];
153 ABBREV_TAC `v'=(inv b * --a)`
156 THEN ASM_REWRITE_TAC[]
157 THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];
162 MRESA_TAC Local_lemmas1.ARCV_PI_OPPOSITE[`v'`;`u`;`vec 0:real^3`]
163 THEN POP_ASSUM MP_TAC
164 THEN REDUCE_VECTOR_TAC
167 THEN REWRITE_TAC[REAL_ARITH`~(a<b)<=> b<=a`]
168 THEN MATCH_MP_TAC Trigonometry.KEITDWB
169 THEN MRESAL_TAC th3[`vec 0:real^3`;`v`;`p`][VECTOR_ARITH`&0 % a= vec 0`]]);;
172 let OIQKKEP_concl = `!u v c.
173 u IN ball_annulus /\ v IN ball_annulus /\ c < &4 /\ dist(u,v) <= c /\ &2<= dist(u,v)==>
174 arcV (vec 0) u v <= arclength (&2) (&2) c`;;
177 let OIQKKEP = prove_by_refinement(
180 REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus;dist]
181 THEN REPEAT STRIP_TAC
182 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`v`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
183 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
184 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
185 THEN MRESAL_TAC NORM_TRIANGLE[`u:real^3`;`-- v:real^3`][VECTOR_ARITH`a+ --b=a-b:real^3`;NORM_NEG]
186 THEN MRESAL_TAC NORM_TRIANGLE[`v:real^3`;`u- v:real^3`][VECTOR_ARITH`a+ b-a=b:real^3`;NORM_NEG]
187 THEN MRESAL_TAC NORM_TRIANGLE[`u-v:real^3`;`-- u:real^3`][VECTOR_ARITH`a- b+ --a= --b:real^3`;NORM_NEG]
188 THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`norm (u)`;`norm v`;`norm(u-v)`]
190 THEN MP_TAC(REAL_ARITH`norm (u - v:real^3) <= c /\ c< &4 /\ &0<= norm (u - v)
191 ==> &0 <= c /\ c <= &2 + &2 /\ &2 <= &2 + c /\ &2 <= c + &2 /\ c<= &4`)
192 THEN ASM_REWRITE_TAC[NORM_POS_LE]
194 THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`&2`;`&2`;`c:real`]
195 [NORM_POS_LE;REAL_ARITH`&0< &2`]
196 THEN MATCH_MP_TAC ACS_MONO_LE
200 REWRITE_TAC[REAL_ARITH`-- &1 <= (&2 * &2 + &2 * &2 - c * c) / (&2 * &2 * &2)
202 THEN MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE
203 THEN MRESA_TAC REAL_ABS_REFL[`c`];
207 MRESAL_TAC Imjxphr.xrr_increasing_le[`&2`;`&2`;`norm(u-v)`;`c`][NORM_POS_LE;REAL_ARITH`&0< &2`]
208 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm u`;`&2`;`norm(u-v)`]
209 [NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0]
210 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm v`;`norm u`;`norm(u-v)`]
211 [NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0;]
212 THEN POP_ASSUM MP_TAC
213 THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
215 THEN MP_TAC(REAL_ARITH`xrr (&2) (&2) (norm (u - v)) <= xrr (&2) (&2) c
216 /\ xrr (norm u) (&2) (norm (u - v)) <= xrr (&2) (&2) (norm (u - v))
217 /\ xrr (norm u) (norm v) (norm (u - v)) <= xrr (norm u) (&2) (norm (u - v:real^3))
218 ==> xrr (norm u) (norm v) (norm (u - v))<= xrr (&2) (&2) c`)
220 THEN POP_ASSUM MP_TAC
221 THEN REWRITE_TAC[xrr]
224 MRESAL_TAC Trigonometry1.TRI_SQUARES_BOUNDS[`norm u`;`norm v`;`norm(u-v)`]
231 let MXQTIED_concl = `!s s' v.
232 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
233 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
234 scs_d_v39 s'= scs_d_v39 s /\
235 v IN MMs_v39 s /\ v IN BBs_v39 s' /\
236 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
237 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
241 let MXQTIED_PRIME2_concl = `
242 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
243 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
244 scs_d_v39 s'= scs_d_v39 s /\
245 v IN MMs_v39 s /\ v IN BBs_v39 s' /\
246 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
247 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
252 let MXQTIED_PRIME_concl = `
253 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
254 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
255 scs_d_v39 s'= scs_d_v39 s /\
256 v IN BBprime_v39 s /\ v IN BBs_v39 s' /\
257 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
258 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
265 let MXQTIED_TAU_concl = `
266 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
267 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
268 scs_d_v39 s'= scs_d_v39 s /\
269 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) ==>
270 taustar_v39 s' v= taustar_v39 s v`;;
273 let MXQTIED_TAU_DSV_concl = `
274 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
275 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
276 scs_d_v39 s'= scs_d_v39 s /\
277 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
279 dsv_v39 s' v= dsv_v39 s v`;;
282 let MXQTIED_BB_concl = `!s s' v.
283 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
284 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
285 scs_d_v39 s'= scs_d_v39 s /\
287 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
288 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
297 let MXQTIED_INDEX_concl = `
298 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
299 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
300 scs_d_v39 s'= scs_d_v39 s /\
302 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
303 /\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
304 BBindex_v39 s' v= BBindex_v39 s v`;;
308 let MXQTIED_INDEX=prove( MXQTIED_INDEX_concl,
309 REWRITE_TAC[IN;BBindex_v39]
310 THEN REPEAT RESA_TAC);;
317 let MXQTIED_BB=prove_by_refinement( MXQTIED_BB_concl,
318 [REWRITE_TAC[IN;scs_basic]
319 THEN REPEAT STRIP_TAC
321 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
322 THEN REPEAT RESA_TAC;
324 THAYTHE_TAC 1[`i`;`j:num`]
325 THEN THAYTHE_TAC (15-10)[`i`;`j`]
330 THAYTHE_TAC 1[`i`;`j:num`]
331 THEN THAYTHE_TAC (15-10)[`i`;`j`]
336 THAYTHE_TAC 1[`i`;`j:num`]
337 THEN THAYTHE_TAC (15-10)[`i`;`j`]
342 THAYTHE_TAC 1[`i`;`j:num`]
343 THEN THAYTHE_TAC (15-10)[`i`;`j`]
346 THEN REAL_ARITH_TAC]);;
350 let MXQTIED_TAU_DSV =prove(MXQTIED_TAU_DSV_concl,
351 REWRITE_TAC[IN;scs_basic]
352 THEN REPEAT STRIP_TAC
353 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
354 THEN REPEAT STRIP_TAC);;
358 let MXQTIED_TAU =prove(MXQTIED_TAU_concl,
359 REWRITE_TAC[IN;scs_basic]
360 THEN REPEAT STRIP_TAC
361 THEN MP_TAC MXQTIED_TAU_DSV
362 THEN REWRITE_TAC[IN;scs_basic]
363 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;]
364 THEN REPEAT STRIP_TAC);;
369 let MXQTIED_PRIME=prove_by_refinement(
372 REWRITE_TAC[IN;scs_basic]
373 THEN REPEAT STRIP_TAC
374 THEN MP_TAC MXQTIED_TAU_DSV
375 THEN REWRITE_TAC[IN;scs_basic]
376 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
377 THEN REPEAT STRIP_TAC;
380 THEN REWRITE_TAC[IN;scs_basic]
382 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][IN;scs_basic]
384 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
386 THEN MATCH_DICH_TAC (18-17)
387 THEN ASM_REWRITE_TAC[]
388 THEN MATCH_MP_TAC MXQTIED_BB
389 THEN ASM_REWRITE_TAC[IN;scs_basic]
390 THEN EXISTS_TAC`s':scs_v39`
391 THEN ASM_REWRITE_TAC[];
394 THEN REWRITE_TAC[IN;scs_basic]
397 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
398 THEN REPEAT RESA_TAC]);;
402 let BBPRIME_IMP_BB=prove(`BBprime_v39 s' w ==> BBs_v39 s' w`,
403 ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime_v39;]
408 let MXQTIED_PRIME2=prove_by_refinement( MXQTIED_PRIME2_concl,
410 REWRITE_TAC[IN;scs_basic]
411 THEN REPEAT STRIP_TAC
412 THEN MRESA_TAC(GEN_ALL Nuxcoea.MMS_IMP_BBPRIME)[`s`;`v`]
413 THEN MP_TAC MXQTIED_PRIME
414 THEN REWRITE_TAC[IN;scs_basic]
415 THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
416 THEN REPEAT STRIP_TAC
417 THEN MP_TAC MXQTIED_INDEX
418 THEN REWRITE_TAC[IN;scs_basic]
420 THEN MP_TAC(SET_RULE`(?w. BBprime_v39 (s':scs_v39) w /\ BBindex_v39 s w< BBindex_v39 s v) \/ ~(?w. BBprime_v39 s' w /\ BBindex_v39 s w< BBindex_v39 s v)`)
423 MP_TAC BBPRIME_IMP_BB
425 THEN MRESAL_TAC MXQTIED_BB[`s`;`s'`;`w`][scs_basic;IN]
427 THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
430 THEN REWRITE_TAC[BBindex_min_v39]
431 THEN SUBGOAL_THEN`BBprime_v39 s (w:num->real^3)`ASSUME_TAC;
434 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39;]
436 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN]
437 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww:num->real^3`][scs_basic;IN]
440 THEN DICH_TAC (28-19)
444 THEN THAYTHE_TAC (28-13)[`ww`]
445 THEN POP_ASSUM MP_TAC
446 THEN POP_ASSUM MP_TAC
447 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`v`][scs_basic;IN]
448 THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][scs_basic;IN]
451 MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN];
453 SUBGOAL_THEN`BBindex_v39 s w IN IMAGE (BBindex_v39 s) (BBprime_v39 s)`ASSUME_TAC;
455 REWRITE_TAC[IMAGE;IN_ELIM_THM]
457 THEN EXISTS_TAC`w:num->real^3`
458 THEN ASM_REWRITE_TAC[];
460 MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s w`]
464 THEN ASM_REWRITE_TAC[]
469 THEN REWRITE_TAC[NOT_EXISTS_THM;BBindex_min_v39]
471 THEN SUBGOAL_THEN`BBindex_v39 s v IN IMAGE (BBindex_v39 s') (BBprime_v39 s')`ASSUME_TAC;
473 REWRITE_TAC[IN_ELIM_THM;IMAGE]
475 THEN EXISTS_TAC`v:num->real^3`
476 THEN ASM_REWRITE_TAC[];
478 MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s') (BBprime_v39 s'))`;`BBindex_v39 s v`]
479 THEN MP_TAC(ARITH_RULE`min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) <= BBindex_v39 s v
480 ==> min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) < BBindex_v39 s v
481 \/ min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) = BBindex_v39 s v`)
485 THEN REWRITE_TAC[GSYM BBindex_min_v39]
486 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
489 THEN THAYTHE_TAC(21-16)[`x`]
490 THEN POP_ASSUM MP_TAC
492 THEN ASM_REWRITE_TAC[GSYM BBindex_min_v39]
493 THEN ASM_REWRITE_TAC[]
494 THEN MRESA_TAC BBPRIME_IMP_BB[`s'`;`x`]
495 THEN MRESAL_TAC MXQTIED_INDEX[`s'`;`s`;`x`][IN;scs_basic]
502 let MXQTIED=prove(MXQTIED_concl,
503 REWRITE_TAC[IN;scs_basic;]
504 THEN REPEAT STRIP_TAC
505 THEN MP_TAC MXQTIED_PRIME2
506 THEN REWRITE_TAC[IN;scs_basic;]
508 THEN MRESA_TAC Ayqjtmd.unadorned_MMs[`s'`]);;
516 let SCS_BASIC_DSV=prove(` is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
517 scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' ==>
518 dsv_v39 s v <= dsv_v39 s' v`,
519 REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;IN;dsv_v39;scs_basic;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
521 THEN ASM_REWRITE_TAC[SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0/\ a+ &0=a`]);;
529 let SCS_BASIC_TAUSTAR=prove(` is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
530 scs_k_v39 s = scs_k_v39 s'
531 /\ scs_d_v39 s<= scs_d_v39 s'
532 ==> taustar_v39 s' v <= taustar_v39 s v`,
534 THEN MP_TAC SCS_BASIC_DSV
536 THEN POP_ASSUM MP_TAC
537 THEN REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF]
538 THEN MP_TAC(SET_RULE`scs_k_v39 s' <= 3 \/ ~(scs_k_v39 s' <= 3)`)
540 THEN REAL_ARITH_TAC);;
543 let TAUSTAR_LE_0_XWNHLMD=prove(` is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
544 scs_k_v39 s = scs_k_v39 s' /\
545 v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s'
546 ==> taustar_v39 s' v< &0`,
547 REWRITE_TAC[IN;LET_DEF;LET_END_DEF;MMs_v39;BBprime2_v39;BBprime_v39]
549 THEN MP_TAC SCS_BASIC_TAUSTAR
551 THEN POP_ASSUM MP_TAC
553 THEN REAL_ARITH_TAC);;
560 let XWNHLMD_MM=prove(` is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
561 scs_k_v39 s = scs_k_v39 s' /\
562 v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s'
563 ==> ~(MMs_v39 s' ={})`,
565 THEN MP_TAC TAUSTAR_LE_0_XWNHLMD
567 THEN MATCH_MP_TAC SGTRNAF
568 THEN EXISTS_TAC`v:num->real^3`
569 THEN ASM_REWRITE_TAC[]
571 THEN REWRITE_TAC[scs_basic]
572 THEN REPEAT RESA_TAC);;
574 let XWNHLMD_concl = `!s s' v.
575 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
576 scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' /\
577 v IN MMs_v39 s /\ v IN BBs_v39 s' ==>
578 scs_arrow_v39 {s} {s'}`;;
583 let XWNHLMD=prove_by_refinement(XWNHLMD_concl,
585 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
586 THEN ABBREV_TAC`k=scs_k_v39 s`
587 THEN REPEAT RESA_TAC;
589 DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);
594 THEN POP_ASSUM MP_TAC
595 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
596 THEN REPEAT STRIP_TAC
597 THEN POP_ASSUM MP_TAC
599 THEN EXISTS_TAC`s':scs_v39`
600 THEN ASM_REWRITE_TAC[]
601 THEN MATCH_MP_TAC XWNHLMD_MM
602 THEN ASM_REWRITE_TAC[IN]]);;
608 let check_completeness_claimA_concl =
609 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)