1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
11 Basic definitions (and type) and properties used for proof
16 _v11, 2013-2-14, changed constant cc_eps -> &0 in quqy cc_real_model_v10.
19 module Oxl_def = struct
23 let cc_eps = new_definition `cc_eps = #0.0057`;;
25 let cc_v11_exists = MESON[] `?(x:((num->real) list) # ((num->bool)list) # num ). T`;;
27 let cc_v11 = REWRITE_RULE[] (new_type_definition "cc_v11" ("cc_v11", "pair_of_cc_v11")cc_v11_exists);;
29 (* discarded ccx1, cc_bool *)
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))`;;
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`;;
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`;;
49 let cc_hassmall_v11 = new_definition
50 `cc_hassmall_v11 cc i = (cc_small_v11 cc i /\ cc_small_v11 cc (i+1))`;;
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`;;
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 }`;;
59 let periodic = new_definition `periodic (f:num->A) n = (!i. (f (i+n) = f (i:num)))`;;
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
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))`;;
78 (* thales 2013-2-14, corrected quqy constants cc_eps -> &0 *)
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) /\
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
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
107 // nonquarter 4-cells
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
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
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))`;;
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))`;;
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)`;;
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)`;;
148 let DHCVTVE_concl = `T`;; (* This is just a repeat of CHQSQEY, LXDEYBO, UNPNFVW *)
150 let PMZTATI_concl = `T`;; (* This is a restatement of gamma8 *)
152 let RJSZKQX_concl = `T`;; (* This is a restatement of fhvb2 *)
154 let IXPFBKA_concl = `T`;; (* This is a restatement of jsp *)
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)`;;
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)`;;
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)`;;
165 let BKLETJQ_concl = `T`;; (* This is a restatement of gamma10_gamma11 *)
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)`;;
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)`;;
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 *)
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))`;;
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)`,
188 REWRITE_TAC[periodic];
189 REPEAT WEAK_STRIP_TAC;
190 SPEC_TAC (`k:num`,`k:num`);
194 SUBST1_TAC (arith `i + SUC k * n = (i+ k * n) + n`);
199 let periodic_mod = prove_by_refinement(
200 `!f n m. periodic (f:num->A) n /\ ~( n=0) ==> (f m = f (m MOD n))`,
203 REPEAT WEAK_STRIP_TAC;
204 INTRO_TAC DIVISION [`m`;`n`];
206 ONCE_REWRITE_TAC[arith `x + (y:num) = y + x`];
207 BY(ASM_MESON_TAC[periodic_nk;arith `~(n=0) ==> (0 < n)`])
211 let MOD_IN_NUMSEG = prove_by_refinement(
212 `!m n. ~(n =0) ==> (m MOD n IN (0..(n-1)))`,
215 REWRITE_TAC[IN_NUMSEG];
216 REPEAT WEAK_STRIP_TAC;
217 INTRO_TAC DIVISION [`m`;`n`];
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)`,
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)`)]);
232 REPEAT WEAK_STRIP_TAC;
233 INTRO_TAC DIVISION [`a`;`n`];
235 BY(ASM_REWRITE_TAC[]);
236 INTRO_TAC DIVISION [`b`;`n`];
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);
251 REWRITE_TAC[RIGHT_SUB_DISTRIB];
252 FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC;
254 ENOUGH_TO_SHOW_TAC `b - a = 0`;
255 FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC;
257 INTRO_TAC DIVISION [`b - (a:num)`;`n`];
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)) `,
267 INTRO_TAC MOD_INJ [`n`;`x`;`x`;`x + (k:num)`];
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 `];
273 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
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)`,
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`];
287 REPEAT WEAK_STRIP_TAC;
289 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
290 REWRITE_TAC[ MOD_MULT_ADD];
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 ];
297 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
298 INTRO_TAC DIVISION [`r`;`n`];
300 REPEAT WEAK_STRIP_TAC;
302 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
303 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
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)`,
312 REWRITE_TAC[BIJ;INJ];
313 BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ])
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)`,
322 REPEAT WEAK_STRIP_TAC;
323 INTRO_TAC BIJ_SUM [`i..((n-1)+i)`;`0..(n-1)`;`f`;`(\j. (j MOD n))`];
325 REWRITE_TAC[BIJ;INJ];
328 REPEAT WEAK_STRIP_TAC;
329 BY(ASM_SIMP_TAC[ MOD_IN_NUMSEG]);
330 REPEAT WEAK_STRIP_TAC;
331 MATCH_MP_TAC MOD_INJ;
333 REPEAT WEAK_STRIP_TAC;
336 REPEAT WEAK_STRIP_TAC;
337 BY(ASM_MESON_TAC[MOD_SURJ]);
338 DISCH_THEN (SUBST1_TAC o GSYM);
340 REWRITE_TAC[FUN_EQ_THM];
343 BY(ASM_MESON_TAC[periodic_mod])
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))
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`])
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)`,
367 REWRITE_TAC[cc_bool_model_v11;cc_real_model_v11];
368 REPEAT WEAK_STRIP_TAC;
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)`,
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`;
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)`,
391 REWRITE_TAC[cc_bool_model_v11];
392 REWRITE_TAC[cc_qu_v11;cc_qy_v11;cc_qx_v11];
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))`,
403 REPEAT WEAK_STRIP_TAC;
404 FIRST_X_ASSUM_ST `cc_real_model_v11` MP_TAC;
406 FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_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;
415 MATCH_MP_TAC FINITE_SUBSET;
416 TYPIFY `0..cc_card_v11 cc - 1` EXISTS_TAC;
417 REWRITE_TAC[FINITE_NUMSEG];
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];
426 GMATCH_SIMP_TAC MOD_IN_NUMSEG;
427 BY(ASM_REWRITE_TAC[]);
428 GMATCH_SIMP_TAC (GSYM periodic_mod);
430 BY(ASM_SIMP_TAC[periodic_fn]);
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)`]);
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;
442 REPEAT WEAK_STRIP_TAC;
443 FIRST_X_ASSUM (MP_TAC o (ISPEC `p:num`));
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])
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)`,
461 REPEAT WEAK_STRIP_TAC;
462 INTRO_TAC QUARTER1 [`cc`];
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;
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];
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)`,
485 REPEAT WEAK_STRIP_TAC;
486 INTRO_TAC QU_EXISTS [`cc`];
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]);
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;
501 SUBGOAL_THEN `cc_card_v11 cc - 1 = 0` SUBST1_TAC;
502 FIRST_X_ASSUM MP_TAC;
504 REWRITE_TAC[NUMSEG_SING;SUM_SING];
505 SUBGOAL_THEN `q = 0` SUBST1_TAC;
506 FIRST_X_ASSUM_ST `IN` MP_TAC;
508 REWRITE_TAC[IN_NUMSEG];
510 REPEAT WEAK_STRIP_TAC;
511 FIRST_X_ASSUM MP_TAC;
513 MP_TAC Flyspeck_constants.bounds;
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)`,
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)`];
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 /\
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 /\
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`])
572 let periodic_numseg = prove_by_refinement(
573 `!p n. periodic p n /\ ~(n = 0) /\
574 (!i. i IN 0..(n-1) ==> p i) ==>
578 REPEAT WEAK_STRIP_TAC;
579 GMATCH_SIMP_TAC periodic_mod;
580 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
582 FIRST_X_ASSUM MATCH_MP_TAC;
583 GMATCH_SIMP_TAC MOD_IN_NUMSEG;
584 BY(ASM_REWRITE_TAC[])
588 let cc_bool_model_simple = prove_by_refinement(
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
606 REWRITE_TAC[cc_bool_model_v11];
607 REPEAT WEAK_STRIP_TAC;
609 ABBREV_TAC `n = cc_card_v11 cc`;
611 MATCH_MP_TAC periodic_numseg;
612 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
614 REWRITE_TAC[periodic];
615 BY(ASM_MESON_TAC[periodic]);
617 MATCH_MP_TAC periodic_numseg;
618 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
620 REWRITE_TAC[periodic];
621 BY(ASM_MESON_TAC[periodic]);
623 MATCH_MP_TAC periodic_numseg;
624 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
626 REWRITE_TAC[periodic];
627 BY(ASM_MESON_TAC[periodic]);
629 MATCH_MP_TAC periodic_numseg;
630 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`)));
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`)));
637 REWRITE_TAC[periodic];
638 BY(ASM_MESON_TAC[periodic])
642 let cc_bool_model_simple2 = prove_by_refinement(
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
663 REPEAT WEAK_STRIP_TAC;
664 MATCH_MP_TAC cc_bool_model_simple;
666 FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_TAC;
667 REWRITE_TAC[cc_bool_model_v11];
668 REPEAT WEAK_STRIP_TAC;
673 let cc_real_model_simple = prove_by_refinement(
675 (cc_card_v11 cc = n) /\
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
731 REPEAT WEAK_STRIP_TAC;
732 REWRITE_TAC[cc_real_model_v11];
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]))
738 let BIJ_NUMSEG = prove_by_refinement(
739 `!s a b. BIJ (\j. j+ s) (a..b) (a+s..b+s)`,
742 REPEAT WEAK_STRIP_TAC;
743 REWRITE_TAC[BIJ;INJ];
745 REWRITE_TAC[IN_NUMSEG];
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);
758 let cc_cut_sum = prove_by_refinement(
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'`,
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`];
773 GMATCH_SIMP_TAC SUM_CLAUSES_LEFT;
774 ASM_REWRITE_TAC[arith `0 + 1 = 1`;arith `0 <= 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`];
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)`);
792 DISCH_THEN SUBST1_TAC;
793 BY(REWRITE_TAC[ SUM_OFFSET]);
795 REWRITE_TAC[arith `(a + b) + c = a + b + d <=> c = d`];
798 REPEAT WEAK_STRIP_TAC;
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]
813 THEN ABBREV_TAC`n= i DIV k`
815 THEN SPEC_TAC (`i:num`,`i:num`)
816 THEN SPEC_TAC (`n:num`,`n:num`)
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`]])