text_formalization/packing/OXL_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Lemma: OXLZLEZ                                                             *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2012-11-23                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 Basic definitions (and type) and properties used for proof
  12 OXLZLEZ
  13 *)
  14
  15 (*
  16 _v11, 2013-2-14, changed constant cc_eps -> &0 in quqy cc_real_model_v10.
  17 *)
  18
  19 module Oxl_def = struct
  20
  21   open Hales_tactic;;
  22
  23 let cc_eps = new_definition `cc_eps = #0.0057`;;
  24
  25 let cc_v11_exists = MESON[]   `?(x:((num->real) list) # ((num->bool)list) # num ). T`;;
  26
  27 let cc_v11 = REWRITE_RULE[] (new_type_definition "cc_v11" ("cc_v11", "pair_of_cc_v11")cc_v11_exists);;
  28
  29 (* discarded ccx1, cc_bool *)
  30
  31 let cc_real_v11 = new_definition `cc_real_v11 cc = FST (pair_of_cc_v11 cc)`;;
  32 let cc_bool_v11 = new_definition `cc_bool_v11 (cc) = FST(SND (pair_of_cc_v11 cc))`;;
  33 let cc_card_v11 = new_definition `cc_card_v11 (cc) = SND(SND (pair_of_cc_v11 cc))`;;
  34
  35 let cc_azim_v11 = new_definition `cc_azim_v11 cc i = EL 0 (cc_real_v11 cc) i`;;
  36 let cc_gg_v11 = new_definition `cc_gg_v11 cc i = EL 1 (cc_real_v11 cc) i`;;
  37 let cc_gg3a_v11 = new_definition `cc_gg3a_v11 cc i = EL 2 (cc_real_v11 cc) i`;;
  38 let cc_gg3b_v11 = new_definition `cc_gg3b_v11 cc i = EL 3 (cc_real_v11 cc) i`;;
  39
  40
  41 let cc_subcrit_v11 = new_definition `cc_subcrit_v11 cc i = EL 0 (cc_bool_v11 cc) i`;;
  42 let cc_crit_v11 = new_definition `cc_crit_v11 cc i = EL 1 (cc_bool_v11 cc) i`;;
  43 let cc_supercrit_v11 = new_definition `cc_supercrit_v11 cc i = EL 2 (cc_bool_v11 cc) i`;;
  44 let cc_small_v11 = new_definition `cc_small_v11 cc i = EL 3 (cc_bool_v11 cc) i`;;
  45 let cc_small_eta_v11 = new_definition `cc_small_eta_v11 cc i = EL 4 (cc_bool_v11 cc) i`;;
  46 let cc_4cell_v11 = new_definition `cc_4cell_v11 cc i = EL 5 (cc_bool_v11 cc) i`;;
  47
  48
  49 let cc_hassmall_v11 = new_definition
  50   `cc_hassmall_v11 cc i = (cc_small_v11 cc i /\ cc_small_v11 cc (i+1))`;;
  51
  52 let cc_qu_v11 = new_definition `cc_qu_v11 cc i = (cc_hassmall_v11 cc i /\ cc_4cell_v11 cc i /\ cc_subcrit_v11 cc i)`;;
  53 let cc_qx_v11 = new_definition `cc_qx_v11 cc i = (cc_4cell_v11 cc i /\ ~(cc_qu_v11 cc i))`;;
  54 let cc_qy_v11 = new_definition `cc_qy_v11 cc i = ~cc_4cell_v11 cc i`;;
  55
  56 let cc_size_v11 = new_definition `cc_size_v11 cc p =
  57   CARD {i | i IN 0..(cc_card_v11 cc -1) /\ p i }`;;
  58
  59 let periodic = new_definition `periodic (f:num->A) n = (!i. (f (i+n) = f (i:num)))`;;
  60
  61 let cc_bool_model_v11 = new_definition `cc_bool_model_v11 cc <=>
  62   ~(cc_card_v11 cc = 0) /\
  63   periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\
  64   periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\
  65   periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\
  66   periodic (cc_small_v11 cc) (cc_card_v11 cc) /\
  67   periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\
  68   periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\
  69 (!i. ~(cc_crit_v11 cc i /\ cc_supercrit_v11 cc i)) /\
  70 (!i. ~(cc_crit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
  71 (!i. ~(cc_supercrit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
  72 (!i. (cc_4cell_v11 cc i ==> cc_crit_v11 cc i \/ cc_subcrit_v11 cc i \/ cc_supercrit_v11 cc i)) /\
  73 (!i. (cc_small_eta_v11 cc i ==> cc_small_v11 cc i)) // jsp
  74 `;;
  75
  76 let cc_bool_prep_v11 = new_definition `cc_bool_prep_v11 cc = (!i. cc_qy_v11 cc i ==> ~cc_qy_v11 cc (i+1))`;;
  77
  78 (* thales 2013-2-14, corrected quqy constants cc_eps -> &0 *)
  79
  80 let cc_real_model_v11 = new_definition `cc_real_model_v11 cc <=>
  81   periodic (cc_azim_v11 cc) (cc_card_v11 cc) /\
  82   periodic (cc_gg_v11 cc) (cc_card_v11 cc) /\
  83   periodic (cc_gg3a_v11 cc) (cc_card_v11 cc) /\
  84   periodic (cc_gg3b_v11 cc) (cc_card_v11 cc) /\
  85 //
  86 // general bounds.
  87 //
  88 (!i. #0.606 <= cc_azim_v11 cc i) /\ // gckb
  89 (!i. cc_4cell_v11 cc i ==> cc_azim_v11 cc i < #2.8) /\ // azim_c4
  90 (sum (0.. (cc_card_v11 cc - 1)) (cc_azim_v11 cc) = &2 * pi) /\
  91 ((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\
  92                            cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3)) ==>
  93    (&0 <= sum (0.. (cc_card_v11 cc -1)) (cc_gg_v11 cc))) /\  // ox3q1h
  94 //
  95 // quarters
  96 //
  97 (!i. cc_qu_v11 cc i ==> -- cc_eps <= cc_gg_v11 cc i) /\ // gamma_qu
  98 (!i. cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc i) ==> cc_eps <= cc_gg_v11 cc i ) /\ // fhbv2
  99 (!i. cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc (i+1)) ==> cc_eps <= cc_gg_v11 cc i ) /\ // fhbv2
 100 (!i. cc_qu_v11 cc i /\ cc_qy_v11 cc (i+1) ==> &0 <= cc_gg_v11 cc i + cc_gg3a_v11 cc (i+1)) /\ // quqy
 101 (!i. cc_qu_v11 cc (i+1) /\ cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i + cc_gg_v11 cc (i+1)) /\ // quqy
 102 (!i. cc_4cell_v11 cc  i ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // ztg4
 103 (!i. cc_qu_v11 cc  i ==>  -- #0.0659 + #0.042 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // azim1
 104 (!i. cc_qu_v11 cc  i ==> -- #0.0142852 + #0.00609451 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // gaz4
 105 (!i. cc_qu_v11 cc  i ==>  #0.161517 - #0.119482 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // gaz6
 106 //
 107 // nonquarter 4-cells
 108 //
 109 (!i. cc_qx_v11 cc i ==> #0.0 <= cc_gg_v11 cc i) /\ // gamma_qx
 110 (!i. cc_qx_v11 cc i /\ #2.3 < cc_azim_v11 cc i ==> cc_eps <= cc_gg_v11 cc i) /\ // g_qxd
 111 (!i. cc_qx_v11 cc i /\ cc_hassmall_v11 cc i /\ cc_qy_v11 cc (i+1) ==> cc_eps <= cc_gg_v11 cc i + cc_gg3a_v11 cc (i+1)) /\ // gamma10
 112 (!i. cc_qx_v11 cc (i+1) /\ cc_hassmall_v11 cc (i+1) /\ cc_qy_v11 cc i ==> cc_eps <= cc_gg3b_v11 cc i + cc_gg_v11 cc (i+1)) /\ // gamma11
 113 (!i. cc_qx_v11 cc i /\ cc_small_v11 cc i /\ ~cc_small_v11 cc (i+1)  ==> cc_eps <= cc_gg_v11 cc i) /\ // gamma8
 114 (!i. cc_qx_v11 cc i /\ cc_small_v11 cc (i+1) /\ ~cc_small_v11 cc i  ==> cc_eps <= cc_gg_v11 cc i) /\ // gamma8
 115 (!i. cc_qx_v11 cc i /\ cc_hassmall_v11 cc i ==>  #0.213849 - #0.119482* cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // gaz9
 116 (!i. cc_qx_v11 cc i /\ cc_hassmall_v11 cc i /\ cc_supercrit_v11 cc i ==>  #0.00457511 + #0.00609451*cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // azim2
 117 //
 118 // 23-cells
 119 //
 120   (!i. cc_qy_v11 cc i ==> cc_gg3a_v11 cc i + cc_gg3b_v11 cc i <= cc_gg_v11 cc i) /\
 121   (!i. cc_qy_v11 cc i ==> &0 <= cc_gg3a_v11 cc i) /\
 122   (!i. cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i) /\
 123 (!i. cc_qy_v11 cc i ==> #0.008 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // cell3, grki
 124 (!i. cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ ~cc_small_eta_v11 cc (i+1) /\ cc_azim_v11 cc i < #1.074 ==>
 125    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // pem
 126 (!i. cc_qy_v11 cc i /\ ~cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) /\ cc_azim_v11 cc i < #1.074 ==>
 127    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // pem
 128 (!i. cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) ==>
 129    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // tew
 130 (!i. cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) /\ #1.946 <= cc_azim_v11 cc i /\
 131  cc_azim_v11 cc i <= #2.089 ==>
 132  #3.0 * cc_eps <= cc_gg_v11 cc i) // txq
 133 `;;
 134
 135 let CHQSQEY_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 136    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (3 <= cc_size_v11 cc (cc_4cell_v11 cc))`;;
 137
 138 let MTMLSRF_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 139    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (?i. 0 < i /\ cc_gg_v11 cc i < &0 /\ cc_qu_v11 cc i /\
 140                                                       cc_4cell_v11 cc (i+1) /\ cc_4cell_v11 cc (i-1))`;;
 141
 142 let LXDEYBO_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 143    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_size_v11 cc (cc_4cell_v11 cc) <= 4)`;;
 144
 145 let UNPNFVW_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 146    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_size_v11 cc (cc_qy_v11 cc) <= 1)`;;
 147
 148 let DHCVTVE_concl = `T`;; (* This is just a repeat of CHQSQEY, LXDEYBO, UNPNFVW *)
 149
 150 let PMZTATI_concl = `T`;; (* This is a restatement of gamma8 *)
 151
 152 let RJSZKQX_concl = `T`;; (* This is a restatement of fhvb2 *)
 153
 154 let IXPFBKA_concl = `T`;; (* This is a restatement of jsp *)
 155
 156 let IPVICGW_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 157    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (!i. cc_small_v11 cc i)`;;
 158
 159 let RSIWAMP_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 160    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_card_v11 cc <= 4)`;;
 161
 162 let RSIWAMP_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 163    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_card_v11 cc <= 4)`;;
 164
 165 let BKLETJQ_concl = `T`;; (* This is a restatement of gamma10_gamma11 *)
 166
 167 let UTEOITF_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 168    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (!i. cc_4cell_v11 cc i)`;;
 169
 170 let LUIKGMH_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 171    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (4 <= cc_card_v11 cc)`;;
 172
 173 let GRHIDFA_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\
 174    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (F)`;;  (* main conclusion *)
 175
 176 (*
 177 let XSBYGIQ_concl =
 178   `(?cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0))
 179   ==> (?cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ cc_bool_prep_v11 cc /\  (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0))`;;
 180 *)
 181
 182
 183
 184 let periodic_nk = prove_by_refinement(
 185   `!i k f n. periodic (f:num->A) n /\ (0 < n) ==> (f (i + k * n) = f i)`,
 186   (* {{{ proof *)
 187   [
 188   REWRITE_TAC[periodic];
 189   REPEAT WEAK_STRIP_TAC;
 190   SPEC_TAC (`k:num`,`k:num`);
 191   INDUCT_TAC;
 192     AP_TERM_TAC;
 193     BY(ARITH_TAC);
 194   SUBST1_TAC (arith `i + SUC k * n  = (i+ k * n) + n`);
 195   BY(ASM_MESON_TAC[])
 196   ]);;
 197   (* }}} *)
 198
 199 let periodic_mod = prove_by_refinement(
 200   `!f n m. periodic (f:num->A) n /\ ~( n=0) ==> (f m = f (m MOD n))`,
 201   (* {{{ proof *)
 202   [
 203   REPEAT WEAK_STRIP_TAC;
 204   INTRO_TAC DIVISION [`m`;`n`];
 205   ASM_REWRITE_TAC[];
 206   ONCE_REWRITE_TAC[arith `x + (y:num) = y + x`];
 207   BY(ASM_MESON_TAC[periodic_nk;arith `~(n=0) ==> (0 < n)`])
 208   ]);;
 209   (* }}} *)
 210
 211 let MOD_IN_NUMSEG = prove_by_refinement(
 212   `!m n. ~(n =0) ==> (m MOD n IN (0..(n-1)))`,
 213   (* {{{ proof *)
 214   [
 215   REWRITE_TAC[IN_NUMSEG];
 216   REPEAT WEAK_STRIP_TAC;
 217   INTRO_TAC DIVISION [`m`;`n`];
 218   ASM_REWRITE_TAC[];
 219   BY(ARITH_TAC)
 220   ]);;
 221   (* }}} *)
 222
 223 let MOD_INJ = prove_by_refinement(
 224   `!n r a b. ~(n = 0) /\ a IN (r..((n-1)+r)) /\ b IN (r..((n-1)+r)) /\ a MOD n = b MOD n ==> (a = b)`,
 225   (* {{{ proof *)
 226   [
 227   REPEAT GEN_TAC;
 228   SUBGOAL_THEN `!P. ((!a b. (a <= (b:num)) ==> P a b) /\ (!a b. P a b <=> P b a)) ==> (P a b)` MATCH_MP_TAC;
 229     BY(MESON_TAC[ (arith `a <= b \/ b <= (a:num)`)]);
 230   CONJ2_TAC;
 231     BY(ASM_MESON_TAC[]);
 232   REPEAT WEAK_STRIP_TAC;
 233   INTRO_TAC DIVISION [`a`;`n`];
 234   ANTS_TAC;
 235     BY(ASM_REWRITE_TAC[]);
 236   INTRO_TAC DIVISION [`b`;`n`];
 237   ANTS_TAC;
 238     BY(ASM_REWRITE_TAC[]);
 239   REPEAT WEAK_STRIP_TAC;
 240   SUBGOAL_THEN `(b - a) DIV n = 0` ASSUME_TAC;
 241     GMATCH_SIMP_TAC DIV_LT;
 242     REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC);
 243     REWRITE_TAC[IN_NUMSEG];
 244     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 245   SUBGOAL_THEN `(b - a) MOD n = 0` ASSUME_TAC;
 246     REWRITE_TAC[MOD_EQ_0];
 247     ASM_SIMP_TAC[MOD_EQ_0];
 248     EXISTS_TAC (`b DIV n - a DIV n`);
 249     REPEAT (FIRST_X_ASSUM_ST `( * ):num->num->num` MP_TAC);
 250     ASM_REWRITE_TAC[];
 251     REWRITE_TAC[RIGHT_SUB_DISTRIB];
 252     FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC;
 253     BY(ARITH_TAC);
 254   ENOUGH_TO_SHOW_TAC `b - a = 0`;
 255     FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC;
 256     BY(ARITH_TAC);
 257   INTRO_TAC DIVISION [`b - (a:num)`;`n`];
 258   ASM_REWRITE_TAC[];
 259   BY(ARITH_TAC)
 260   ]);;
 261   (* }}} *)
 262
 263 let MOD_INJ1_ALT = prove_by_refinement
 264 (`!k n. ~( n = 0) /\ k < n /\ ~( k = 0) ==> (! x. ~( x MOD n = (x + k) MOD n)) `,
 265 [
 266   REPEAT STRIP_TAC;
 267   INTRO_TAC MOD_INJ [`n`;`x`;`x`;`x + (k:num)`];
 268   ANTS_TAC;
 269     ASM_REWRITE_TAC[IN_NUMSEG];
 270     REPEAT (FIRST_X_ASSUM MP_TAC);
 271     SIMP_TAC[LE_REFL; ARITH_RULE` ~( n = 0) ==> x <= n - 1 + x `; ARITH_RULE` a <= a + x:num `];
 272     BY(ARITH_TAC);
 273   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
 274 ]);;
 275
 276
 277 let MOD_SURJ = prove_by_refinement(
 278   `!n r a. ~(n=0) /\ a IN (0..(n-1)) ==> (?b. b IN (r..((n-1)+r)) /\ b MOD n = a)`,
 279   (* {{{ proof *)
 280   [
 281   REWRITE_TAC[IN_NUMSEG];
 282   REPEAT WEAK_STRIP_TAC;
 283   ASM_CASES_TAC `r MOD n <= a`;
 284     EXISTS_TAC (`(r DIV n) * n + a`);
 285     INTRO_TAC DIVISION [`r`;`n`];
 286     ASM_REWRITE_TAC[];
 287     REPEAT WEAK_STRIP_TAC;
 288     CONJ_TAC;
 289       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 290     REWRITE_TAC[ MOD_MULT_ADD];
 291     MATCH_MP_TAC MOD_LT;
 292     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 293   EXISTS_TAC (`((r DIV n) + 1) * n + a`);
 294   REWRITE_TAC[ MOD_MULT_ADD ];
 295   CONJ2_TAC;
 296     MATCH_MP_TAC MOD_LT;
 297     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 298   INTRO_TAC DIVISION [`r`;`n`];
 299   ASM_REWRITE_TAC[];
 300   REPEAT WEAK_STRIP_TAC;
 301   CONJ_TAC;
 302     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 303   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
 304   ]);;
 305   (* }}} *)
 306
 307 let BIJ_SUM = prove_by_refinement(
 308   `!(A:A->bool) (B:B->bool) f ab.
 309     BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
 310   (* {{{ proof *)
 311   [
 312   REWRITE_TAC[BIJ;INJ];
 313   BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ])
 314   ]);;
 315   (* }}} *)
 316
 317
 318 let periodic_sum = prove_by_refinement(
 319   `!f n. periodic f n /\ ~( n=0) ==> (!i. sum (i..((n-1) +i)) f = sum (0..(n-1)) f)`,
 320   (* {{{ proof *)
 321   [
 322   REPEAT WEAK_STRIP_TAC;
 323   INTRO_TAC BIJ_SUM [`i..((n-1)+i)`;`0..(n-1)`;`f`;`(\j. (j MOD n))`];
 324   ANTS_TAC;
 325     REWRITE_TAC[BIJ;INJ];
 326     SUBCONJ_TAC;
 327       CONJ_TAC;
 328         REPEAT WEAK_STRIP_TAC;
 329         BY(ASM_SIMP_TAC[ MOD_IN_NUMSEG]);
 330       REPEAT WEAK_STRIP_TAC;
 331       MATCH_MP_TAC MOD_INJ;
 332       BY(ASM_MESON_TAC[]);
 333     REPEAT WEAK_STRIP_TAC;
 334     REWRITE_TAC[SURJ];
 335     ASM_REWRITE_TAC[];
 336     REPEAT WEAK_STRIP_TAC;
 337     BY(ASM_MESON_TAC[MOD_SURJ]);
 338   DISCH_THEN (SUBST1_TAC o GSYM);
 339   AP_TERM_TAC;
 340   REWRITE_TAC[FUN_EQ_THM];
 341   GEN_TAC;
 342   REWRITE_TAC[o_THM];
 343   BY(ASM_MESON_TAC[periodic_mod])
 344   ]);;
 345   (* }}} *)
 346
 347 let periodic_fn = prove_by_refinement(
 348   `!cc. cc_bool_model_v11 cc ==> (periodic (cc_hassmall_v11 cc) (cc_card_v11 cc) /\
 349    periodic (cc_qu_v11 cc) (cc_card_v11 cc) /\
 350    periodic (cc_qx_v11 cc) (cc_card_v11 cc) /\
 351    periodic (cc_qy_v11 cc) (cc_card_v11 cc))
 352    `,
 353   (* {{{ proof *)
 354   [
 355   REWRITE_TAC[cc_bool_model_v11;periodic;cc_hassmall_v11;cc_qu_v11;cc_qx_v11;cc_qy_v11];
 356   REPEAT WEAK_STRIP_TAC;
 357   BY(ASM_SIMP_TAC[arith `!i. (i + cc_card_v11 cc) + 1 = (i + 1) + cc_card_v11 cc`])
 358   ]);;
 359   (* }}} *)
 360
 361
 362 let QX_NN = prove_by_refinement(
 363   `!cc i. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (cc_qx_v11 cc i) ==>
 364     (#0.0 <= cc_gg_v11 cc i)`,
 365   (* {{{ proof *)
 366   [
 367   REWRITE_TAC[cc_bool_model_v11;cc_real_model_v11];
 368   REPEAT WEAK_STRIP_TAC;
 369   BY(ASM_SIMP_TAC[])
 370   ]);;
 371   (* }}} *)
 372
 373 let QY_NN = prove_by_refinement(
 374   `!cc i. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (cc_qy_v11 cc i) ==>
 375     (#0.0 <= cc_gg_v11 cc i)`,
 376   (* {{{ proof *)
 377   [
 378   REWRITE_TAC[cc_bool_model_v11;cc_real_model_v11];
 379   REPEAT WEAK_STRIP_TAC;
 380   ENOUGH_TO_SHOW_TAC `&0 <= cc_gg3a_v11 cc i /\ &0 <= cc_gg3b_v11 cc i /\ cc_gg3a_v11 cc i + cc_gg3b_v11 cc i <= cc_gg_v11 cc i`;
 381     BY(REAL_ARITH_TAC);
 382   BY(ASM_SIMP_TAC[])
 383   ]);;
 384   (* }}} *)
 385
 386 let QY_QX_QU = prove_by_refinement(
 387   `!cc i. cc_bool_model_v11 cc ==>
 388     (cc_qu_v11 cc i \/ cc_qy_v11 cc i \/ cc_qx_v11 cc i)`,
 389   (* {{{ proof *)
 390   [
 391   REWRITE_TAC[cc_bool_model_v11];
 392   REWRITE_TAC[cc_qu_v11;cc_qy_v11;cc_qx_v11];
 393   BY(MESON_TAC[])
 394   ]);;
 395   (* }}} *)
 396
 397 let QUARTER1 = prove_by_refinement(
 398 `!cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\
 399    (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (1 <= cc_size_v11 cc (cc_qu_v11 cc))`,
 400   (* {{{ proof *)
 401   [
 402   GEN_TAC;
 403   REPEAT WEAK_STRIP_TAC;
 404   FIRST_X_ASSUM_ST `cc_real_model_v11` MP_TAC;
 405   COPY_TAC;
 406   FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_TAC;
 407   COPY_TAC;
 408   REWRITE_TAC[cc_size_v11;cc_real_model_v11;cc_bool_model_v11];
 409   REPEAT WEAK_STRIP_TAC;
 410   SUBGOAL_THEN `~(cc_card_v11 cc = 0)` ASSUME_TAC;
 411     BY(ASM_REWRITE_TAC[]);
 412   REWRITE_TAC[arith `1 <= x <=> ~(x = 0)`];
 413   GMATCH_SIMP_TAC CARD_EQ_0;
 414   CONJ_TAC;
 415     MATCH_MP_TAC FINITE_SUBSET;
 416     TYPIFY `0..cc_card_v11 cc - 1` EXISTS_TAC;
 417     REWRITE_TAC[FINITE_NUMSEG];
 418     BY(SET_TAC[]);
 419   REWRITE_TAC[Misc_defs_and_lemmas.EMPTY_EXISTS];
 420   TYPIFY `~(!i. ~(cc_qu_v11 cc i))` ENOUGH_TO_SHOW_TAC;
 421     REWRITE_TAC[NOT_FORALL_THM];
 422     REPEAT WEAK_STRIP_TAC;
 423     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `i MOD (cc_card_v11 cc)`)));
 424     REWRITE_TAC[IN_ELIM_THM];
 425     CONJ_TAC;
 426       GMATCH_SIMP_TAC MOD_IN_NUMSEG;
 427       BY(ASM_REWRITE_TAC[]);
 428     GMATCH_SIMP_TAC (GSYM periodic_mod);
 429     ASM_REWRITE_TAC[];
 430     BY(ASM_SIMP_TAC[periodic_fn]);
 431   DISCH_TAC;
 432   GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `?p. cc_gg_v11 cc p < &0`) MP_TAC));
 433     TYPIFY `~(!i. &0 <= cc_gg_v11 cc i)` ENOUGH_TO_SHOW_TAC;
 434       BY(MESON_TAC[arith `&0 <= x <=> ~(x < &0)`]);
 435     DISCH_TAC;
 436     FIRST_X_ASSUM_ST `sum X f < &0` MP_TAC;
 437     REWRITE_TAC[arith `((x < &0) ==> F) <=> &0 <= x`];
 438     MATCH_MP_TAC SUM_POS_LE;
 439     REWRITE_TAC[FINITE_NUMSEG];
 440     REPEAT WEAK_STRIP_TAC;
 441     BY(ASM_SIMP_TAC[]);
 442   REPEAT WEAK_STRIP_TAC;
 443   FIRST_X_ASSUM (MP_TAC o (ISPEC `p:num`));
 444   REWRITE_TAC[];
 445   GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `~(cc_qx_v11 cc p \/ cc_qy_v11 cc p)`)));
 446     BY(ASM_MESON_TAC[ QY_QX_QU]);
 447   FIRST_X_ASSUM MP_TAC;
 448   REWRITE_TAC[arith `x < &0 <=> ~(#0.0 <= x)`];
 449   REWRITE_TAC[TAUT `(~a ==> ~b) <=> (b ==> a)`];
 450   BY(ASM_MESON_TAC[QX_NN;QY_NN])
 451   ]);;
 452   (* }}} *)
 453
 454 let QU_EXISTS = prove_by_refinement(
 455   `!cc. cc_bool_model_v11 cc /\
 456           cc_real_model_v11 cc /\
 457           sum (0..cc_card_v11 cc - 1) (cc_gg_v11 cc) < &0 ==>
 458    (?q. cc_qu_v11 cc q /\ q IN 0..cc_card_v11 cc - 1)`,
 459   (* {{{ proof *)
 460   [
 461   REPEAT WEAK_STRIP_TAC;
 462   INTRO_TAC QUARTER1 [`cc`];
 463   ASM_REWRITE_TAC[];
 464   REWRITE_TAC[cc_size_v11;arith `1 <= x <=> ~(x = 0)`];
 465   GMATCH_SIMP_TAC CARD_EQ_0;
 466   REWRITE_TAC[Misc_defs_and_lemmas.EMPTY_EXISTS];
 467   REWRITE_TAC[IN_ELIM_THM];
 468   GMATCH_SIMP_TAC FINITE_SUBSET;
 469   CONJ2_TAC;
 470     BY(MESON_TAC[]);
 471   GOAL_TERM (fun w -> (EXISTS_TAC ( env w `0..cc_card_v11 cc  - 1`)));
 472   REWRITE_TAC[FINITE_NUMSEG];
 473   REWRITE_TAC[SUBSET;IN_ELIM_THM];
 474   BY(MESON_TAC[])
 475   ]);;
 476   (* }}} *)
 477
 478 let CC_CARD2 = prove_by_refinement(
 479   `!cc. cc_bool_model_v11 cc /\
 480           cc_real_model_v11 cc /\
 481           sum (0..cc_card_v11 cc - 1) (cc_gg_v11 cc) < &0 ==>
 482     (2 <= cc_card_v11 cc)`,
 483   (* {{{ proof *)
 484   [
 485   REPEAT WEAK_STRIP_TAC;
 486   INTRO_TAC QU_EXISTS [`cc`];
 487   ASM_REWRITE_TAC[];
 488   REPEAT WEAK_STRIP_TAC;
 489   ENOUGH_TO_SHOW_TAC `~(cc_card_v11 cc = 1)`;
 490     REWRITE_TAC[arith `2 <= x <=> ~(x = 0) /\ ~(x = 1)`];
 491     BY(ASM_MESON_TAC[cc_bool_model_v11]);
 492   DISCH_TAC;
 493   SUBGOAL_THEN `sum (0..cc_card_v11 cc -1) (cc_azim_v11 cc) = &2 * pi /\ cc_azim_v11 cc q <  #2.8` MP_TAC;
 494     FIRST_X_ASSUM_ST `cc_qu_v11` MP_TAC;
 495     REWRITE_TAC[cc_qu_v11];
 496     REPEAT WEAK_STRIP_TAC;
 497     FIRST_X_ASSUM_ST `cc_real_model_v11` MP_TAC;
 498     REWRITE_TAC[cc_real_model_v11];
 499     REPEAT WEAK_STRIP_TAC;
 500     BY(ASM_SIMP_TAC[]);
 501   SUBGOAL_THEN `cc_card_v11 cc - 1 = 0` SUBST1_TAC;
 502     FIRST_X_ASSUM MP_TAC;
 503     BY(ARITH_TAC);
 504   REWRITE_TAC[NUMSEG_SING;SUM_SING];
 505   SUBGOAL_THEN `q = 0` SUBST1_TAC;
 506     FIRST_X_ASSUM_ST `IN` MP_TAC;
 507     ASM_REWRITE_TAC[];
 508     REWRITE_TAC[IN_NUMSEG];
 509     BY(ARITH_TAC);
 510   REPEAT WEAK_STRIP_TAC;
 511   FIRST_X_ASSUM MP_TAC;
 512   ASM_REWRITE_TAC[];
 513   MP_TAC Flyspeck_constants.bounds;
 514   BY(REAL_ARITH_TAC)
 515   ]);;
 516   (* }}} *)
 517
 518 let CASE_3Q1H = prove_by_refinement(
 519   `!cc.  cc_bool_model_v11 cc /\
 520 ((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\
 521                            cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3))) ==>
 522    ~(?i. cc_qy_v11 cc i)`,
 523   (* {{{ proof *)
 524   [
 525   REWRITE_TAC[cc_qu_v11;cc_qy_v11];
 526   REPEAT WEAK_STRIP_TAC;
 527   SUBGOAL_THEN `periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\ ~(0 = cc_card_v11 cc)` ASSUME_TAC;
 528     BY(ASM_MESON_TAC[cc_bool_model_v11]);
 529   SUBGOAL_THEN `cc_4cell_v11 cc (i MOD 4) /\ cc_4cell_v11 cc ((i+1) MOD 4) /\ cc_4cell_v11 cc ((i+2) MOD 4) /\ cc_4cell_v11 cc ((i+3) MOD 4)` MP_TAC;
 530     FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM);
 531     REPEAT (GMATCH_SIMP_TAC (GSYM periodic_mod));
 532     BY(ASM_REWRITE_TAC[]);
 533   REPEAT WEAK_STRIP_TAC;
 534   SUBGOAL_THEN `~(cc_4cell_v11 cc (i' MOD 4))` MP_TAC;
 535     FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM);
 536     REPEAT (GMATCH_SIMP_TAC (GSYM periodic_mod));
 537     BY(ASM_REWRITE_TAC[]);
 538   REWRITE_TAC[TAUT `(~a ==> F) <=> a`];
 539   SUBGOAL_THEN `(i' MOD 4 = i MOD 4) \/ (i' MOD 4 = (i+1) MOD 4) \/ (i' MOD 4 = (i+2) MOD 4) \/ (i' MOD 4 =  (i+3) MOD 4)` ASSUME_TAC;
 540     INTRO_TAC MOD_SURJ [`4`;`i`;`i' MOD 4`];
 541     ASM_SIMP_TAC[MOD_IN_NUMSEG;arith `~(4 = 0)`];
 542     REWRITE_TAC[IN_NUMSEG;arith `4 - 1 +i = i + 3`];
 543     REWRITE_TAC[arith `(i <= b /\ b <= i + 3) <=> (b = i \/ b = i+1 \/ b = i+2 \/ b = i+3)`];
 544     BY(MESON_TAC[]);
 545   BY(ASM_MESON_TAC[])
 546   ]);;
 547   (* }}} *)
 548
 549 let CC_EXISTS = prove_by_refinement(
 550   `!az gg gg3a gg3b sub cri super sma eta cell4 n.  ?cc.
 551     cc_azim_v11 cc = az /\
 552     cc_gg_v11 cc = gg /\
 553     cc_gg3a_v11 cc = gg3a /\
 554     cc_gg3b_v11 cc = gg3b /\
 555     cc_subcrit_v11 cc = sub /\
 556     cc_crit_v11 cc = cri /\
 557     cc_supercrit_v11 cc = super /\
 558     cc_small_v11 cc = sma /\
 559     cc_small_eta_v11 cc = eta /\
 560     cc_4cell_v11 cc = cell4 /\
 561     cc_card_v11 cc = n`,
 562   (* {{{ proof *)
 563   [
 564   REPEAT WEAK_STRIP_TAC;
 565   GOAL_TERM (fun w -> (EXISTS_TAC ( env w `cc_v11 ([az;gg;gg3a;gg3b],([sub;cri;super;sma;eta;cell4],n))`)));
 566   REWRITE_TAC[FUN_EQ_THM];
 567   REWRITE_TAC[cc_azim_v11;cc_gg_v11;cc_gg3a_v11;cc_gg3b_v11;cc_subcrit_v11;cc_crit_v11;cc_supercrit_v11;cc_small_v11;cc_small_eta_v11;cc_4cell_v11;cc_card_v11;cc_real_v11;cc_bool_v11;cc_v11];
 568   BY(REWRITE_TAC[EL;HD;TL;arith `5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
 569   ]);;
 570   (* }}} *)
 571
 572 let periodic_numseg = prove_by_refinement(
 573   `!p n.  periodic p n /\ ~(n = 0) /\
 574     (!i. i IN 0..(n-1) ==> p i) ==>
 575     (!i. p i)`,
 576   (* {{{ proof *)
 577   [
 578   REPEAT WEAK_STRIP_TAC;
 579   GMATCH_SIMP_TAC periodic_mod;
 580   GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 581   ASM_REWRITE_TAC[];
 582   FIRST_X_ASSUM MATCH_MP_TAC;
 583   GMATCH_SIMP_TAC MOD_IN_NUMSEG;
 584   BY(ASM_REWRITE_TAC[])
 585   ]);;
 586   (* }}} *)
 587
 588 let cc_bool_model_simple = prove_by_refinement(
 589  `!cc.
 590   ~(cc_card_v11 cc = 0) /\
 591   periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\
 592   periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\
 593   periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\
 594   periodic (cc_small_v11 cc) (cc_card_v11 cc) /\
 595   periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\
 596   periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\
 597 (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_crit_v11 cc i /\ cc_supercrit_v11 cc i)) /\
 598 (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_crit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
 599 (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_supercrit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
 600 (!i. i IN 0..(cc_card_v11 cc - 1) ==> (cc_4cell_v11 cc i ==> cc_crit_v11 cc i \/ cc_subcrit_v11 cc i \/ cc_supercrit_v11 cc i)) /\
 601 (!i. i IN 0..(cc_card_v11 cc - 1) ==> (cc_small_eta_v11 cc i ==> cc_small_v11 cc i))
 602  ==> cc_bool_model_v11 cc
 603 `,
 604   (* {{{ proof *)
 605   [
 606   REWRITE_TAC[cc_bool_model_v11];
 607   REPEAT WEAK_STRIP_TAC;
 608   ASM_REWRITE_TAC[];
 609   ABBREV_TAC `n  = cc_card_v11 cc`;
 610   CONJ_TAC;
 611     MATCH_MP_TAC periodic_numseg;
 612     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 613     ASM_REWRITE_TAC[];
 614     REWRITE_TAC[periodic];
 615     BY(ASM_MESON_TAC[periodic]);
 616   CONJ_TAC;
 617     MATCH_MP_TAC periodic_numseg;
 618     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 619     ASM_REWRITE_TAC[];
 620     REWRITE_TAC[periodic];
 621     BY(ASM_MESON_TAC[periodic]);
 622   CONJ_TAC;
 623     MATCH_MP_TAC periodic_numseg;
 624     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 625     ASM_REWRITE_TAC[];
 626     REWRITE_TAC[periodic];
 627     BY(ASM_MESON_TAC[periodic]);
 628   CONJ_TAC;
 629     MATCH_MP_TAC periodic_numseg;
 630     GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 631     ASM_REWRITE_TAC[];
 632     REWRITE_TAC[periodic];
 633     BY(ASM_MESON_TAC[periodic]);
 634   MATCH_MP_TAC periodic_numseg;
 635   GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
 636   ASM_REWRITE_TAC[];
 637   REWRITE_TAC[periodic];
 638   BY(ASM_MESON_TAC[periodic])
 639   ]);;
 640   (* }}} *)
 641
 642 let cc_bool_model_simple2 = prove_by_refinement(
 643  `!cc cc'.
 644   ~(cc_card_v11 cc = 0) /\
 645    cc_bool_model_v11 cc' /\
 646   periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\
 647   periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\
 648   periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\
 649   periodic (cc_small_v11 cc) (cc_card_v11 cc) /\
 650   periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\
 651   periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\
 652    (!i. i IN 0..(cc_card_v11 cc - 1) ==> (?j.
 653                 (cc_subcrit_v11 cc i = cc_subcrit_v11 cc' j) /\
 654                 (cc_crit_v11 cc i = cc_crit_v11 cc' j) /\
 655                 (cc_supercrit_v11 cc i = cc_supercrit_v11 cc' j) /\
 656                 (cc_small_v11 cc i = cc_small_v11 cc' j) /\
 657                 (cc_small_eta_v11 cc i = cc_small_eta_v11 cc' j) /\
 658                 (cc_4cell_v11 cc i = cc_4cell_v11 cc' j)))
 659  ==> cc_bool_model_v11 cc
 660 `,
 661   (* {{{ proof *)
 662   [
 663   REPEAT WEAK_STRIP_TAC;
 664   MATCH_MP_TAC cc_bool_model_simple;
 665   ASM_REWRITE_TAC[];
 666   FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_TAC;
 667   REWRITE_TAC[cc_bool_model_v11];
 668   REPEAT WEAK_STRIP_TAC;
 669   BY(ASM_MESON_TAC[])
 670   ]);;
 671   (* }}} *)
 672
 673 let cc_real_model_simple = prove_by_refinement(
 674   `!cc n.
 675     (cc_card_v11 cc = n) /\
 676     ~(n = 0) /\
 677   periodic (cc_azim_v11 cc) (cc_card_v11 cc) /\
 678   periodic (cc_gg_v11 cc) (cc_card_v11 cc) /\
 679   periodic (cc_gg3a_v11 cc) (cc_card_v11 cc) /\
 680   periodic (cc_gg3b_v11 cc) (cc_card_v11 cc) /\
 681   periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\
 682   periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\
 683   periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\
 684   periodic (cc_small_v11 cc) (cc_card_v11 cc) /\
 685   periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\
 686   periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\
 687     periodic (cc_hassmall_v11 cc) (cc_card_v11 cc) /\
 688     periodic (cc_qu_v11 cc) (cc_card_v11 cc) /\
 689     periodic (cc_qx_v11 cc) (cc_card_v11 cc) /\
 690     periodic (cc_qy_v11 cc) (cc_card_v11 cc) /\
 691 (!i. (i IN 0..(n-1)) ==> (#0.606 <= cc_azim_v11 cc i)) /\
 692 (!i. (i IN 0..(n-1)) ==> cc_4cell_v11 cc i ==> cc_azim_v11 cc i < #2.8) /\
 693 (sum (0.. (cc_card_v11 cc - 1)) (cc_azim_v11 cc) = &2 * pi) /\
 694 ((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\
 695                            cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3)) ==>
 696    (&0 <= sum (0.. (cc_card_v11 cc -1)) (cc_gg_v11 cc))) /\
 697 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc i ==> -- cc_eps <= cc_gg_v11 cc i) /\
 698 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc i) ==> cc_eps <= cc_gg_v11 cc i ) /\
 699 (!i. (i IN 0..(n-1)) ==>  cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc (i+1)) ==> cc_eps <= cc_gg_v11 cc i ) /\
 700 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc i /\ cc_qy_v11 cc (i+1) ==> &0 <= cc_gg_v11 cc i + cc_gg3a_v11 cc (i+1)) /\
 701 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc (i+1) /\ cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i + cc_gg_v11 cc (i+1)) /\
 702 (!i. (i IN 0..(n-1)) ==>  cc_4cell_v11 cc  i ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 703 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc  i ==>  -- #0.0659 + #0.042 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 704 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc  i ==> -- #0.0142852 + #0.00609451 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 705 (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc  i ==>  #0.161517 - #0.119482 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 706 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i ==> #0.0 <= cc_gg_v11 cc i) /\
 707 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ #2.3 < cc_azim_v11 cc i ==> cc_eps <= cc_gg_v11 cc i) /\
 708 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ cc_hassmall_v11 cc i /\ cc_qy_v11 cc (i+1) ==> cc_eps <= cc_gg_v11 cc i + cc_gg3a_v11 cc (i+1)) /\
 709 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc (i+1) /\ cc_hassmall_v11 cc (i+1) /\ cc_qy_v11 cc i ==> cc_eps <= cc_gg3b_v11 cc i + cc_gg_v11 cc (i+1)) /\
 710 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ cc_small_v11 cc i /\ ~cc_small_v11 cc (i+1)  ==> cc_eps <= cc_gg_v11 cc i) /\
 711 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ cc_small_v11 cc (i+1) /\ ~cc_small_v11 cc i  ==> cc_eps <= cc_gg_v11 cc i) /\
 712 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ cc_hassmall_v11 cc i ==>  #0.213849 - #0.119482* cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 713 (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i /\ cc_hassmall_v11 cc i /\ cc_supercrit_v11 cc i ==>  #0.00457511 + #0.00609451*cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 714   (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> cc_gg3a_v11 cc i + cc_gg3b_v11 cc i <= cc_gg_v11 cc i) /\
 715   (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> &0 <= cc_gg3a_v11 cc i) /\
 716   (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i) /\
 717 (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> #0.008 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 718 (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ ~cc_small_eta_v11 cc (i+1) /\ cc_azim_v11 cc i < #1.074 ==>
 719    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 720 (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i /\ ~cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) /\ cc_azim_v11 cc i < #1.074 ==>
 721    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 722 (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) ==>
 723    a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\
 724 (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) /\ #1.946 <= cc_azim_v11 cc i /\
 725  cc_azim_v11 cc i <= #2.089 ==>
 726  #3.0 * cc_eps <= cc_gg_v11 cc i)
 727  ==> cc_real_model_v11 cc
 728 `,
 729   (* {{{ proof *)
 730   [
 731   REPEAT WEAK_STRIP_TAC;
 732   REWRITE_TAC[cc_real_model_v11];
 733   ASM_REWRITE_TAC[];
 734   BY(REPEAT (CONJ_TAC) THEN (MATCH_MP_TAC periodic_numseg) THEN EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[periodic] THEN GEN_TAC THEN SUBST1_TAC (arith `(i+n) + 1 = (i+1) + n`) THEN TRY(ASM_MESON_TAC[periodic]))
 735   ]);;
 736   (* }}} *)
 737
 738 let BIJ_NUMSEG = prove_by_refinement(
 739   `!s a b.  BIJ (\j. j+ s) (a..b) (a+s..b+s)`,
 740   (* {{{ proof *)
 741   [
 742   REPEAT WEAK_STRIP_TAC;
 743   REWRITE_TAC[BIJ;INJ];
 744   SUBCONJ_TAC;
 745     REWRITE_TAC[IN_NUMSEG];
 746     BY(ARITH_TAC);
 747   REPEAT WEAK_STRIP_TAC;
 748   ASM_REWRITE_TAC[SURJ];
 749   REWRITE_TAC[IN_NUMSEG];
 750   REPEAT WEAK_STRIP_TAC;
 751   TYPIFY `(x:num) - s` EXISTS_TAC;
 752   REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
 753   BY(ARITH_TAC)
 754   ]);;
 755   (* }}} *)
 756
 757
 758 let cc_cut_sum = prove_by_refinement(
 759   `!f' x f  n.
 760     ~(n=0) /\
 761     periodic f' (n+1) /\
 762     f 0 = f' x + f' (x +1) /\
 763     (!i. i IN 1..n-1 ==> f i = f' (x + 1 + i)) ==>
 764     sum (0..n-1) f = sum (0..n) f'`,
 765   (* {{{ proof *)
 766   [
 767   REPEAT WEAK_STRIP_TAC;
 768   TYPIFY `sum (0..n) f' = sum(x..(x+n)) f'` (C SUBGOAL_THEN SUBST1_TAC);
 769     SUBST1_TAC (arith `(x:num) + n = (n + 1 ) - 1 + x` );
 770     GMATCH_SIMP_TAC periodic_sum;
 771     ASM_REWRITE_TAC[arith `(n+1) - 1 = n`];
 772     BY(ARITH_TAC);
 773   GMATCH_SIMP_TAC SUM_CLAUSES_LEFT;
 774   ASM_REWRITE_TAC[arith `0 + 1 = 1`;arith `0 <= n-1`];
 775   ASM_CASES_TAC `n=1`;
 776     ASM_REWRITE_TAC[arith `1 - 1 = 0`];
 777     ASM_SIMP_TAC[arith `0 < 1`;SUM_TRIV_NUMSEG];
 778     GMATCH_SIMP_TAC SUM_CLAUSES_LEFT;
 779     REWRITE_TAC[SUM_SING_NUMSEG];
 780     REWRITE_TAC[arith `x <= x + 1`];
 781     BY(REAL_ARITH_TAC);
 782   SUBGOAL_THEN `2 <= n` ASSUME_TAC;
 783     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 784   TYPIFY `sum (x..x+n) f' = f' x + f' (x+1) + sum (x+2..x+n) f'` (C SUBGOAL_THEN SUBST1_TAC);
 785     GMATCH_SIMP_TAC SUM_CLAUSES_LEFT;
 786     GMATCH_SIMP_TAC SUM_CLAUSES_LEFT;
 787     BY(ASM_SIMP_TAC[arith `2 <= n ==> x + 1 <= x + n`;arith `x <= x + (n:num)`;arith `(x+1)+1 = x+2`]);
 788   TYPIFY `sum (x+2..x+n) f' = sum (1..(n-1)) (\i. f' (i + (x+1)))` (C SUBGOAL_THEN ASSUME_TAC);
 789     SUBST1_TAC (arith `x+2 = 1 + (x+1)`);
 790     MP_TAC (arith `~(n=0) ==> x + n = (n-1) + (x+1)`);
 791     ASM_REWRITE_TAC[];
 792     DISCH_THEN SUBST1_TAC;
 793     BY(REWRITE_TAC[ SUM_OFFSET]);
 794   ASM_REWRITE_TAC[];
 795   REWRITE_TAC[arith `(a + b) + c = a + b + d <=> c = d`];
 796   MATCH_MP_TAC SUM_EQ;
 797   BETA_TAC;
 798   REPEAT WEAK_STRIP_TAC;
 799   ASM_SIMP_TAC[];
 800   AP_TERM_TAC;
 801   BY(ARITH_TAC)
 802   ]);;
 803   (* }}} *)
 804
 805 let PERIODIC_PROPERTY= prove(
 806 ` ~(k = 0) /\ periodic vv k ==>  (!i.  vv (i MOD k)= vv i)`,
 807 REWRITE_TAC[periodic]
 808 THEN REPEAT STRIP_TAC
 809 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
 810 THEN REMOVE_ASSUM_TAC
 811 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[th]
 812 THEN MP_TAC th)
 813 THEN ABBREV_TAC`n= i DIV k`
 814 THEN ASM_TAC
 815 THEN SPEC_TAC (`i:num`,`i:num`)
 816 THEN SPEC_TAC (`n:num`,`n:num`)
 817 THEN INDUCT_TAC
 818 THENL[REWRITE_TAC[ARITH_RULE`0*K+A=A`];
 819 POP_ASSUM(fun th-> REPEAT STRIP_TAC
 820 THEN MRESA1_TAC th`n *k + i MOD k`)
 821 THEN POP_ASSUM MP_TAC
 822 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
 823 THEN MRESA_TAC MOD_MULT_ADD[`n:num`;`k:num`;`i MOD k`]
 824 THEN MRESA_TAC DIV_UNIQ[`n * k + i MOD k`;`k:num`;`n:num`;`i MOD k`]
 825 THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`SUC n * k + i MOD k = (n * k + i MOD k) +k`]])
 826 ;;
 827
 828
 829
 830 end;;