(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Wkeidft = struct open Polyhedron;; open Sphere;; open Topology;; open Fan_misc;; open Planarity;; open Conforming;; open Hypermap;; open Fan;; open Topology;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Collect_geom;; open Dih2k_hypermap;; open Wjscpro;; open Tecoxbm;; open Hdplygy;; open Nkezbfc_local;; open Flyspeck_constants;; open Gbycpxs;; open Pcrttid;; open Local_lemmas1;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Hypermap;; open Fan;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Flyspeck_constants;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Zithlqn;; open Xwitccn;; open Ayqjtmd;; open Jkqewgv;; open Mtuwlun;; open Uxckfpe;; open Sgtrnaf;; open Yxionxl;; open Qknvmlb;; open Odxlstcv2;; open Yxionxl2;; open Eyypqdw;; open Ocbicby;; open Imjxphr;; open Nuxcoea;; open Fektyiy;; let SUR_MOD_FUN=prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`, STRIP_TAC THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`) THEN RESA_TAC THENL[ EXISTS_TAC`p' MOD k- p MOD k` THEN MRESA_TAC DIVISION[`p'`;`k`] 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`) THEN RESA_TAC THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION] THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]); EXISTS_TAC`p' MOD k +k - p MOD k` THEN MRESA_TAC DIVISION[`p`;`k`] 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`) THEN RESA_TAC THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION] THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);; let TRANS_DIAG=prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q' ==> (i+q) MOD k= q' MOD k `, STRIP_TAC THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD THEN EXISTS_TAC`p:num` THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`] THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`] THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));; (*************) (*******************) let scs_components = prove_by_refinement( `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`, (* {{{ proof *) [ REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;]; REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;]; REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;]; REWRITE_TAC[scs_str_v39]; BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4; 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]) ]);; (* }}} *) let scs_inj = prove_by_refinement( `!s s'. scs_basic_v39 s /\ scs_basic_v39 s' /\ scs_d_v39 s = scs_d_v39 s' /\ scs_k_v39 s = scs_k_v39 s' /\ (scs_a_v39 s = scs_a_v39 s') /\ (scs_b_v39 s = scs_b_v39 s') ==> (s = s')`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC); REWRITE_TAC[scs_basic;unadorned_v39]; ONCE_REWRITE_TAC[EQ_SYM_EQ]; REWRITE_TAC[SET_RULE `{} = a <=> a = {}`]; REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[GSYM scs_v39]; AP_TERM_TAC; ASM_REWRITE_TAC[scs_components]; TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC); BY(ASM_REWRITE_TAC[FUN_EQ_THM]); BY(REWRITE_TAC[]) ]);; (* }}} *) let DIAG_PSORT1=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q)) ==> (psort k (i+i',i+j) = psort k (p',q'))`, [ REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND ] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC TRANS_DIAG THEN RESA_TAC THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`) THEN RESA_TAC; MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`] THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][] THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`) THEN RESA_TAC; MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`) THEN RESA_TAC; MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`) THEN RESA_TAC; MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`]; MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`) THEN RESA_TAC; MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`) THEN RESA_TAC; MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);; let DIAG_PSORT2=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q')) ==> (psort k (i',j) = psort k (p,q))`, [ REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND ] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC TRANS_DIAG THEN RESA_TAC THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`) THEN RESA_TAC; MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`] THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]; MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`) THEN RESA_TAC; MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`) THEN RESA_TAC; MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`) THEN RESA_TAC; MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`] THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]; MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`) THEN RESA_TAC; MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`) THEN RESA_TAC; MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);; let DIAG_PSORT=prove( ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ p' + q = p + q' /\ ~(k=0) ==> ((psort k (i+i',i+j) = psort k (p',q')) <=> (psort k (i',j) = psort k (p,q)))`, STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL[ MATCH_MP_TAC DIAG_PSORT2 THEN RESA_TAC; MATCH_MP_TAC DIAG_PSORT1 THEN RESA_TAC]);; let TRANS_DIAG=prove(` ~(k=0) ==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `, SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);; let A_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q) ==> scs_a_v39 s i j= scs_a_v39 s p q`, REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC);; let B_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q) ==> scs_b_v39 s i j= scs_b_v39 s p q`, REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC);; 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`, STRIP_TAC THEN MP_TAC Axjrpnc.is_scs_k_le_3 THEN RESA_TAC THEN DICH_TAC 0 THEN ARITH_TAC);; let WKEIDFT_A_concl = `!s s' a b a' b' p q p' q' i. (let k = scs_k_v39 s in (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ (!i. scs_a_v39 s' i (i + 1) = a) /\ (!i. scs_b_v39 s' i (i + 1) = b) /\ scs_k_v39 s' = k /\ p' + q = p + q' /\ scs_d_v39 s = scs_d_v39 s' /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\ 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 ==> (\j j'. scs_a_v39 s' (i + j) (i + j')) = scs_a_v39 s))`;; let WKEIDFT_A=prove_by_refinement( WKEIDFT_A_concl, [ REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`) THEN RESA_TAC; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC A_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`] THEN MRESA_TAC A_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`]; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] THEN MATCH_DICH_TAC (26-13) THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM] THEN STRIP_TAC; MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC; MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`] THEN REWRITE_TAC[ADD1] THEN THAYTHEL_TAC(26-6)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`] THEN THAYTHE_TAC(26-4)[`x`]; MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`] THEN REWRITE_TAC[ADD1] THEN THAYTHEL_TAC(26-6)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`] THEN THAYTHE_TAC(26-4)[`x'`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC]);; let WKEIDFT_B_concl = `!s s' a b a' b' p q p' q' a1 i. (let k = scs_k_v39 s in (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\ (!i. scs_b_v39 s i i = a1) /\ (!i. scs_b_v39 s' i i = a1) /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ (!i. scs_a_v39 s' i (i + 1) = a) /\ (!i. scs_b_v39 s' i (i + 1) = b) /\ scs_k_v39 s' = k /\ p' + q = p + q' /\ scs_d_v39 s = scs_d_v39 s' /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\ 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 ==> (\j j'. scs_b_v39 s' (i + j) (i + j')) = scs_b_v39 s))`;; let WKEIDFT_B=prove_by_refinement( WKEIDFT_B_concl, [ REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`) THEN RESA_TAC; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`] THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`]; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] THEN MATCH_DICH_TAC (26-14) THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM] THEN STRIP_TAC; MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC; MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`] THEN REWRITE_TAC[ADD1] THEN THAYTHEL_TAC(26-7)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`] THEN THAYTHE_TAC(26-5)[`x`]; MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`] THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`] THEN REWRITE_TAC[ADD1] THEN THAYTHEL_TAC(26-7)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`] THEN THAYTHE_TAC(26-5)[`x'`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC]);; let WKEIDFT_EQU_concl = ` (let k = scs_k_v39 s in (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\ (!i. scs_b_v39 s i i = a1) /\ (!i. scs_b_v39 s' i i = a1) /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ (!i. scs_a_v39 s' i (i + 1) = a) /\ (!i. scs_b_v39 s' i (i + 1) = b) /\ scs_k_v39 s' = k /\ p' + q = p + q' /\ scs_d_v39 s = scs_d_v39 s' /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\ 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. s'= scs_prop_equ_v39 s i))`;; let WKEIDFT_EQU=prove( WKEIDFT_EQU_concl, REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`] THEN ASM_TAC THEN REPEAT RESA_TAC THEN EXISTS_TAC`i:num` 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] 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] THEN MATCH_MP_TAC scs_inj THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39] THEN SET_TAC[]);; let WKEIDFT_concl = `!s s' a b a' b' p q p' q'. (let k = scs_k_v39 s in (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\ (!i. scs_b_v39 s i i = a1) /\ (!i. scs_b_v39 s' i i = a1) /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ (!i. scs_a_v39 s' i (i + 1) = a) /\ (!i. scs_b_v39 s' i (i + 1) = b) /\ scs_k_v39 s' = k /\ p' + q = p + q' /\ scs_d_v39 s = scs_d_v39 s' /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\ (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\ scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' ==> scs_arrow_v39 {s} {s'}))`;; let WKEIDFT_PRIME= prove(WKEIDFT_concl, REWRITE_TAC[LET_DEF;LET_END_DEF] THEN REPEAT RESA_TAC THEN MP_TAC WKEIDFT_EQU THEN REWRITE_TAC[LET_DEF;LET_END_DEF] THEN RESA_TAC THEN MATCH_MP_TAC YXIONXL3 THEN ASM_REWRITE_TAC[]);; (********************************) let WKEIDFT_B_v2_concl = `!s a b a' b' p q p' q'. (let k = scs_k_v39 s in (is_scs_v39 s /\ scs_basic_v39 s /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ p' + q = p + q' /\ scs_diag k p q/\ scs_diag k p' q'/\ (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\ (!i. scs_b_v39 s i i = b1) /\ (i+p) MOD k = p' MOD k ==> (\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)))`;; let WKEIDFT_B_V2=prove_by_refinement( WKEIDFT_B_v2_concl, [ 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] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s`; MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`) THEN RESA_TAC; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`] THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`]; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM] THEN STRIP_TAC; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`] THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]; MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`) THEN RESA_TAC THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS] THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`] THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`] THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC]);; let WKEIDFT_A_v2_concl = `!s a b a' b' p q p' q'. (let k = scs_k_v39 s in (is_scs_v39 s /\ scs_basic_v39 s /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ p' + q = p + q' /\ scs_diag k p q/\ scs_diag k p' q'/\ (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\ (!i. scs_b_v39 s i i = b1) /\ (i+p) MOD k = p' MOD k ==> (\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)))`;; let WKEIDFT_A_V2=prove_by_refinement( WKEIDFT_A_v2_concl, [ 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] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s`; MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`) THEN RESA_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESAS_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`][]; POP_ASSUM MP_TAC THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM] THEN STRIP_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`] THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]; MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`] THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`] THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39] THEN REPEAT RESA_TAC]);; let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`, SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);; let WKEIDFT_EQU_v2_concl = ` (let k = scs_k_v39 s in (is_scs_v39 s /\ scs_basic_v39 s /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ p' + q = p + q' /\ scs_diag k p q/\ scs_diag k p' q'/\ 3 < k /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\ (!i. scs_b_v39 s i i = b1) ==> ?i. scs_stab_diag_v39 s p' q'= scs_prop_equ_v39 (scs_stab_diag_v39 s p q) i))`;; let WKEIDFT_EQU_V2= prove(WKEIDFT_EQU_v2_concl, REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC PROPERTY_OF_K_SCS THEN RESA_TAC THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`] THEN ASM_TAC THEN REPEAT RESA_TAC THEN EXISTS_TAC`i:num` 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] 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] THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ] THEN DICH_TAC 1 THEN STRIP_TAC THEN SYM_ASSUM_TAC THEN DICH_TAC 1 THEN STRIP_TAC THEN SYM_ASSUM_TAC THEN MATCH_MP_TAC scs_inj THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p'`;`q'`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ] THEN ASM_SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39] THEN SET_TAC[]);; let WKEIDFT_concl = `!s a b a' b' p q p' q'. (let k = scs_k_v39 s in (is_scs_v39 s /\ scs_basic_v39 s /\ (!i. scs_a_v39 s i (i + 1) = a) /\ (!i. scs_b_v39 s i (i + 1) = b) /\ p' + q = p + q' /\ scs_diag k p q/\ scs_diag k p' q'/\ 3 < k /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\ (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\ (!i j. scs_diag k i j ==> scs_b_v39 s i j = b')/\ (!i. scs_b_v39 s i i = b1) ==> scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;; let WKEIDFT=prove(WKEIDFT_concl, REWRITE_TAC[LET_DEF;LET_END_DEF] THEN REPEAT RESA_TAC THEN MP_TAC WKEIDFT_EQU_V2 THEN REWRITE_TAC[LET_DEF;LET_END_DEF] THEN RESA_TAC THEN MATCH_MP_TAC YXIONXL3 THEN ASM_REWRITE_TAC[] THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)