text_formalization/local/JEJTVGB.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Appendix, Main Estimate, check_completeness                       *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Lemma: JEJTVGB                                                             *)
   6 (* Author: Hoang Le Truong and Thomas Hales                                   *)
   7 (* Date: 2013-08-15                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Jejtvgb = struct
  11
  12   open Hales_tactic;;
  13
  14 let SCS_ARROW_TRANS_SING = prove_by_refinement(
  15   `!a S. scs_arrow_v39 {a} S /\ (!x. x IN S ==> scs_arrow_v39 {x} {}) ==> scs_arrow_v39 {a} {}`,
  16   (* {{{ proof *)
  17   [
  18   REWRITE_TAC[Appendix.scs_arrow_v39;NOT_IN_EMPTY;IN_SING];
  19   BY(MESON_TAC[])
  20   ]);;
  21   (* }}} *)
  22
  23 let JEJTVGB_case_breakdown = prove_by_refinement(
  24   (* main_work4 ==> *) ` main_nonlinear_terminal_v11 ==> (
  25   scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 } /\ // OEHDBEN
  26     scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 } /\ // OTMTOTJ1
  27 scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 } /\ //
  28
  29 scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 ,
  30                                                     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 } /\ //  OTMTOTJ3
  31
  32 scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 ,  scs_stab_diag_v39 scs_5M1 0 3,
  33     scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 } /\ // OTMTOTJ4
  34 scs_arrow_v39 { scs_5M2 }  {scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39  scs_5M1 0  2,
  35     scs_stab_diag_v39   scs_5M1  0   3, scs_stab_diag_v39  scs_5M1  2  4,
  36      scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4} /\ // HIJQAHA
  37 //{ scs_3T1,scs_3T4,scs_4M6',scs_4M7,scs_4M8,
  38 //                                                 scs_5T1, scs_stab_diag_v39 scs_5I2 0 2 ,
  39 //                                                 scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4 } /\ // HIJQAHA
  40
  41 scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 0 2 }
  42     {scs_3M1, scs_4M2  } /\ //  CNICGSF1 ..
  43
  44 scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 0 2 }
  45     {scs_3T1, scs_4M3'  } /\ //  CNICGSF2
  46
  47 scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 2 }
  48     {scs_3T4, scs_4M2  } /\ //  CNICGSF3
  49
  50 scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 3 }
  51     {scs_4M4', scs_3M1 } /\ //  CNICGSF4
  52
  53 scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 2 4 }
  54     {scs_3M1, scs_4M5'  } /\ //  CNICGSF5 ..
  55
  56   scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 } /\ // FYSSVEV
  57
  58
  59   scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 } /\ // ARDBZYE
  60
  61
  62   scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 0 2 } { scs_3M1 } /\ // AUEAHEH
  63
  64   // scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 } /\ // ZNLLLDL (internal)
  65
  66   scs_arrow_v39 { scs_4I3 } {scs_4M6', scs_4T4} /\  // VQFYMZY ..
  67
  68 //  scs_arrow_v39 { scs_4M1 } { scs_4M2, scs_4M6' } /\ // unused.
  69
  70   scs_arrow_v39 { scs_4M2 } {scs_4M6', scs_3M1, scs_3T4}  /\ //  BNAWVNH
  71
  72   scs_arrow_v39 { scs_4M3' } {scs_4M6', scs_3T1, scs_3T6'}  /\ // RAWZDIB
  73
  74   scs_arrow_v39 { scs_4M4' } {scs_4M7, scs_3T3, scs_3M1, scs_3T4} /\ //  MFKLVDK
  75
  76   scs_arrow_v39 { scs_4M5' } {scs_4M8, scs_3T4} /\ // RYPDIXT
  77
  78 scs_arrow_v39 {scs_4M6'} {scs_4T3,scs_4T5} /\ // NWDGKXH
  79
  80 scs_arrow_v39 {scs_4M7} {scs_4M6', scs_3T3, scs_3M1, scs_3T4} /\ // YOBIMPP
  81
  82 scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7,scs_3T4} /\ // MIQMCSN
  83
  84     scs_arrow_v39 {scs_3M1} {scs_3T1,scs_3T5} // BKOSSGE
  85
  86 ==>
  87 JEJTVGB_assume_v39)
  88 `,
  89   (* {{{ proof *)
  90   [
  91   REPEAT WEAKER_STRIP_TAC;
  92   INTRO_TAC (UNDISCH Ocbicby.OCBICBY) [];
  93   REPEAT WEAKER_STRIP_TAC;
  94   TYPIFY `scs_arrow_v39 {scs_3M1} {}` (C SUBGOAL_THEN ASSUME_TAC);
  95     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
  96     TYPIFY `{scs_3T1, scs_3T5}` EXISTS_TAC;
  97     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
  98     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  99   TYPIFY `scs_arrow_v39 {scs_4M6'} {}` (C SUBGOAL_THEN ASSUME_TAC);
 100     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 101     TYPIFY `{scs_4T3,scs_4T5}` EXISTS_TAC;
 102     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 103     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 104   TYPIFY `scs_arrow_v39 {scs_4M7} {}` (C SUBGOAL_THEN ASSUME_TAC);
 105     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 106     TYPIFY `{scs_4M6', scs_3T3, scs_3M1, scs_3T4}` EXISTS_TAC;
 107     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 108     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 109   TYPIFY `scs_arrow_v39 {scs_4M8} {}` (C SUBGOAL_THEN ASSUME_TAC);
 110     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 111     TYPIFY `{scs_4M6', scs_3T7, scs_3T4}` EXISTS_TAC;
 112     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 113     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 114   TYPIFY `scs_arrow_v39 {scs_4M5'} {}` (C SUBGOAL_THEN ASSUME_TAC);
 115     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 116     TYPIFY `{scs_4M8, scs_3T4}` EXISTS_TAC;
 117     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 118     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 119   TYPIFY `scs_arrow_v39 {scs_4M4'} {}` (C SUBGOAL_THEN ASSUME_TAC);
 120     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 121     TYPIFY `{scs_4M7, scs_3T3, scs_3M1, scs_3T4}` EXISTS_TAC; (* revised *)
 122     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 123     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 124   TYPIFY `scs_arrow_v39 {scs_4M3'} {}` (C SUBGOAL_THEN ASSUME_TAC);
 125     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 126     TYPIFY `{scs_4M6', scs_3T1, scs_3T6'}` EXISTS_TAC;
 127     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 128     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 129   TYPIFY `scs_arrow_v39 {scs_4M2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 130     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 131     TYPIFY `{scs_4M6', scs_3M1, scs_3T4}` EXISTS_TAC;
 132     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 133     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 134   TYPIFY `scs_arrow_v39 {scs_4I3} {}` (C SUBGOAL_THEN ASSUME_TAC);
 135     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 136     TYPIFY `{scs_4M6', scs_4T4}` EXISTS_TAC;
 137     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 138     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 139   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 140     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 141     TYPIFY `{scs_3M1}` EXISTS_TAC;
 142     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 143     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 144   TYPIFY `scs_arrow_v39 {scs_4I2}  {}` (C SUBGOAL_THEN ASSUME_TAC);
 145     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 146     TYPIFY `{scs_4T1, scs_4T2}` EXISTS_TAC;
 147     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 148     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 149   TYPIFY `scs_arrow_v39 {scs_4I1}  {}` (C SUBGOAL_THEN ASSUME_TAC);
 150     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 151     TYPIFY `{scs_4I2, scs_stab_diag_v39 scs_4I1 0 2}` EXISTS_TAC;
 152     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 153     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 154   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 2 4}   {}` (C SUBGOAL_THEN ASSUME_TAC);
 155     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 156     TYPIFY `{scs_3M1, scs_4M5'}` EXISTS_TAC;
 157     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 158     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 159   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 0 3}   {}` (C SUBGOAL_THEN ASSUME_TAC);
 160     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 161     TYPIFY `{scs_4M4', scs_3M1}` EXISTS_TAC;
 162     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 163     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 164   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 165     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 166     TYPIFY `{scs_3T4, scs_4M2}` EXISTS_TAC;
 167     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 168     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 169   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5I2 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 170     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 171     TYPIFY `{scs_3T1, scs_4M3'}` EXISTS_TAC;
 172     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 173     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 174   TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5I1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 175     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 176     TYPIFY `{scs_3M1, scs_4M2}` EXISTS_TAC;
 177     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 178     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 179   TYPIFY `scs_arrow_v39 {scs_5M2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 180     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 181     TYPIFY `{scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39                                                       scs_5M1                                                      0                                                      2, scs_stab_diag_v39                                                         scs_5M1                                                         0                                                         3, scs_stab_diag_v39                                                            scs_5M1                                                            2                                                            4, scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}` EXISTS_TAC;
 182     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 183     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 184   TYPIFY `scs_arrow_v39 {scs_5M1} {}` (C SUBGOAL_THEN ASSUME_TAC);
 185     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 186     TYPIFY `{scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,       scs_stab_diag_v39 scs_5M1 2      4, scs_5M2}` EXISTS_TAC;
 187     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 188     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 189   TYPIFY `scs_arrow_v39 {scs_5I3} {}` (C SUBGOAL_THEN ASSUME_TAC);
 190     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 191     TYPIFY `{scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,       scs_stab_diag_v39 scs_5M1 2      4, scs_5M2}` EXISTS_TAC;
 192     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 193     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 194   TYPIFY `scs_arrow_v39 {scs_5I2} {}` (C SUBGOAL_THEN ASSUME_TAC);
 195     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 196     TYPIFY `{scs_stab_diag_v39 scs_5I2 0 2, scs_5M2}` EXISTS_TAC;
 197     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 198     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 199   TYPIFY `scs_arrow_v39 {scs_5I1} {}` (C SUBGOAL_THEN ASSUME_TAC);
 200     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 201     TYPIFY ` {scs_stab_diag_v39 scs_5I1 0 2, scs_5M2}` EXISTS_TAC;
 202     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 203     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 204   TYPIFY `scs_arrow_v39 {scs_6I1} {}` (C SUBGOAL_THEN ASSUME_TAC);
 205     MATCH_MP_TAC SCS_ARROW_TRANS_SING;
 206     TYPIFY `{scs_6T1, scs_5M1, scs_4M2, scs_3M1}` EXISTS_TAC;
 207     ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 208     BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 209   COMMENT "final kill";
 210   MATCH_MP_TAC Ayqjtmd.EAPGLE;
 211   REWRITE_TAC[GSYM Ocbicby.scs_arrow_sing_empty];
 212   REWRITE_TAC[Jotswix.s_init_list_alt;MEM];
 213   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 214   BY(REWRITE_TAC[UNDISCH2 Jotswix.LFLACKU])
 215   ]);;
 216   (* }}} *)
 217
 218 let JEJTVGB = prove_by_refinement(
 219  `main_nonlinear_terminal_v11 ==> JEJTVGB_assume_v39`,
 220   (* {{{ proof *)
 221   [
 222   DISCH_TAC;
 223   MATCH_MP_TAC (UNDISCH JEJTVGB_case_breakdown);
 224   REWRITE_TAC (map UNDISCH2 [Hexagons.OEHDBEN;Otmtotj.OTMTOTJ1;Otmtotj.OTMTOTJ2;Otmtotj.OTMTOTJ3;Otmtotj.OTMTOTJ4]);
 225   REWRITE_TAC (map UNDISCH2 [Hijqaha.HIJQAHA;Cnicgsf.CNICGSF1;Cnicgsf.CNICGSF2;Cnicgsf.CNICGSF3;Cnicgsf.CNICGSF4;Cnicgsf.CNICGSF5]);
 226   REWRITE_TAC (map UNDISCH2 [Ardbzye.FYSSVEV;Ardbzye.ARDBZYE;Aueaheh.AUEAHEH;Aueaheh.VQFYMZY]);
 227   REWRITE_TAC (map UNDISCH2 [Aueaheh.BNAWVNH;Aueaheh.RAWZDIB;Aueaheh.MFKLVDK;Aueaheh.RYPDIXT]);
 228   BY(REWRITE_TAC (map UNDISCH2 [Miqmcsn.NWDGKXH;Miqmcsn.YOBIMPP;Miqmcsn.MIQMCSN;Bkossge.BKOSSGE]))
 229   ]);;
 230   (* }}} *)
 231
 232
 233 end;;