(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Lemma: OXLZLEZ                                                             *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-11-23                                                           *)
(* ========================================================================== *)

(*
Basic definitions (and type) and properties used for proof 
OXLZLEZ
*)

(*
_v11, 2013-2-14, changed constant cc_eps -> &0 in quqy cc_real_model_v10.
*)

module Oxl_def = struct

  open Hales_tactic;;

let cc_eps = new_definition `cc_eps = #0.0057`;;
let cc_v11_exists = MESON[] `?(x:((num->real) list) # ((num->bool)list) # num ). T`;; let cc_v11 = REWRITE_RULE[] (new_type_definition "cc_v11" ("cc_v11", "pair_of_cc_v11")cc_v11_exists);; (* discarded ccx1, cc_bool *)
let cc_real_v11 = new_definition `cc_real_v11 cc = FST (pair_of_cc_v11 cc)`;;
let cc_bool_v11 = new_definition `cc_bool_v11 (cc) = FST(SND (pair_of_cc_v11 cc))`;;
let cc_card_v11 = new_definition `cc_card_v11 (cc) = SND(SND (pair_of_cc_v11 cc))`;;
let cc_azim_v11 = new_definition `cc_azim_v11 cc i = EL 0 (cc_real_v11 cc) i`;;
let cc_gg_v11 = new_definition `cc_gg_v11 cc i = EL 1 (cc_real_v11 cc) i`;;
let cc_gg3a_v11 = new_definition `cc_gg3a_v11 cc i = EL 2 (cc_real_v11 cc) i`;;
let cc_gg3b_v11 = new_definition `cc_gg3b_v11 cc i = EL 3 (cc_real_v11 cc) i`;;
let cc_subcrit_v11 = new_definition `cc_subcrit_v11 cc i = EL 0 (cc_bool_v11 cc) i`;;
let cc_crit_v11 = new_definition `cc_crit_v11 cc i = EL 1 (cc_bool_v11 cc) i`;;
let cc_supercrit_v11 = new_definition `cc_supercrit_v11 cc i = EL 2 (cc_bool_v11 cc) i`;;
let cc_small_v11 = new_definition `cc_small_v11 cc i = EL 3 (cc_bool_v11 cc) i`;;
let cc_small_eta_v11 = new_definition `cc_small_eta_v11 cc i = EL 4 (cc_bool_v11 cc) i`;;
let cc_4cell_v11 = new_definition `cc_4cell_v11 cc i = EL 5 (cc_bool_v11 cc) i`;;
let cc_hassmall_v11 = new_definition 
  `cc_hassmall_v11 cc i = (cc_small_v11 cc i /\ cc_small_v11 cc (i+1))`;;
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)`;;
let cc_qx_v11 = new_definition `cc_qx_v11 cc i = (cc_4cell_v11 cc i /\ ~(cc_qu_v11 cc i))`;;
let cc_qy_v11 = new_definition `cc_qy_v11 cc i = ~cc_4cell_v11 cc i`;;
let cc_size_v11 = new_definition `cc_size_v11 cc p = 
  CARD {i | i IN 0..(cc_card_v11 cc -1) /\ p i }`;;
let periodic = new_definition `periodic (f:num->A) n = (!i. (f (i+n) = f (i:num)))`;;
let cc_bool_model_v11 = new_definition `cc_bool_model_v11 cc <=> 
  ~(cc_card_v11 cc = 0) /\
  periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_small_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\
(!i. ~(cc_crit_v11 cc i /\ cc_supercrit_v11 cc i)) /\
(!i. ~(cc_crit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
(!i. ~(cc_supercrit_v11 cc i /\ cc_subcrit_v11 cc i)) /\
(!i. (cc_4cell_v11 cc i ==> cc_crit_v11 cc i \/ cc_subcrit_v11 cc i \/ cc_supercrit_v11 cc i)) /\
(!i. (cc_small_eta_v11 cc i ==> cc_small_v11 cc i)) // jsp
`;;
let cc_bool_prep_v11 = new_definition `cc_bool_prep_v11 cc = (!i. cc_qy_v11 cc i ==> ~cc_qy_v11 cc (i+1))`;;
(* thales 2013-2-14, corrected quqy constants cc_eps -> &0 *)
let cc_real_model_v11 = new_definition `cc_real_model_v11 cc <=> 
  periodic (cc_azim_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_gg_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_gg3a_v11 cc) (cc_card_v11 cc) /\
  periodic (cc_gg3b_v11 cc) (cc_card_v11 cc) /\
//
// general bounds.
//
(!i. #0.606 <= cc_azim_v11 cc i) /\ // gckb
(!i. cc_4cell_v11 cc i ==> cc_azim_v11 cc i < #2.8) /\ // azim_c4
(sum (0.. (cc_card_v11 cc - 1)) (cc_azim_v11 cc) = &2 * pi) /\
((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\ 
			   cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3)) ==>
   (&0 <= sum (0.. (cc_card_v11 cc -1)) (cc_gg_v11 cc))) /\  // ox3q1h
//
// quarters
//
(!i. cc_qu_v11 cc i ==> -- cc_eps <= cc_gg_v11 cc i) /\ // gamma_qu
(!i. cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc i) ==> cc_eps <= cc_gg_v11 cc i ) /\ // fhbv2
(!i. cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc (i+1)) ==> cc_eps <= cc_gg_v11 cc i ) /\ // fhbv2
(!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
(!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
(!i. cc_4cell_v11 cc  i ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // ztg4
(!i. cc_qu_v11 cc  i ==>  -- #0.0659 + #0.042 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // azim1
(!i. cc_qu_v11 cc  i ==> -- #0.0142852 + #0.00609451 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // gaz4
(!i. cc_qu_v11 cc  i ==>  #0.161517 - #0.119482 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // gaz6
//
// nonquarter 4-cells
//
(!i. cc_qx_v11 cc i ==> #0.0 <= cc_gg_v11 cc i) /\ // gamma_qx
(!i. cc_qx_v11 cc i /\ #2.3 < cc_azim_v11 cc i ==> cc_eps <= cc_gg_v11 cc i) /\ // g_qxd
(!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
(!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
(!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
(!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
(!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
(!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
//
// 23-cells
//
  (!i. cc_qy_v11 cc i ==> cc_gg3a_v11 cc i + cc_gg3b_v11 cc i <= cc_gg_v11 cc i) /\
  (!i. cc_qy_v11 cc i ==> &0 <= cc_gg3a_v11 cc i) /\
  (!i. cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i) /\
(!i. cc_qy_v11 cc i ==> #0.008 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // cell3, grki
(!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 ==>
   a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // pem
(!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 ==>
   a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // pem
(!i. cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) ==> 
   a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ // tew
(!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 /\ 
 cc_azim_v11 cc i <= #2.089 ==> 
 #3.0 * cc_eps <= cc_gg_v11 cc i) // txq
`;;
let CHQSQEY_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (3 <= cc_size_v11 cc (cc_4cell_v11 cc))`;; let MTMLSRF_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (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 /\ cc_4cell_v11 cc (i+1) /\ cc_4cell_v11 cc (i-1))`;; let LXDEYBO_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_size_v11 cc (cc_4cell_v11 cc) <= 4)`;; let UNPNFVW_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_size_v11 cc (cc_qy_v11 cc) <= 1)`;; let DHCVTVE_concl = `T`;; (* This is just a repeat of CHQSQEY, LXDEYBO, UNPNFVW *) let PMZTATI_concl = `T`;; (* This is a restatement of gamma8 *) let RJSZKQX_concl = `T`;; (* This is a restatement of fhvb2 *) let IXPFBKA_concl = `T`;; (* This is a restatement of jsp *) let IPVICGW_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (!i. cc_small_v11 cc i)`;; let RSIWAMP_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_card_v11 cc <= 4)`;; let RSIWAMP_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (cc_card_v11 cc <= 4)`;; let BKLETJQ_concl = `T`;; (* This is a restatement of gamma10_gamma11 *) let UTEOITF_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (!i. cc_4cell_v11 cc i)`;; let LUIKGMH_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (4 <= cc_card_v11 cc)`;; let GRHIDFA_concl = `!cc. cc_bool_model_v11 cc /\ cc_bool_prep_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (F)`;; (* main conclusion *) (* let XSBYGIQ_concl = `(?cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0)) ==> (?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))`;; *)
let periodic_nk = 
prove_by_refinement( `!i k f n. periodic (f:num->A) n /\ (0 < n) ==> (f (i + k * n) = f i)`,
(* {{{ proof *) [ REWRITE_TAC[periodic]; REPEAT WEAK_STRIP_TAC; SPEC_TAC (`k:num`,`k:num`); INDUCT_TAC; AP_TERM_TAC; BY(ARITH_TAC); SUBST1_TAC (arith `i + SUC k * n = (i+ k * n) + n`); BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let periodic_mod = 
prove_by_refinement( `!f n m. periodic (f:num->A) n /\ ~( n=0) ==> (f m = f (m MOD n))`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC DIVISION [`m`;`n`]; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[arith `x + (y:num) = y + x`]; BY(ASM_MESON_TAC[periodic_nk;arith `~(n=0) ==> (0 < n)`]) ]);;
(* }}} *)
let MOD_IN_NUMSEG = 
prove_by_refinement( `!m n. ~(n =0) ==> (m MOD n IN (0..(n-1)))`,
(* {{{ proof *) [ REWRITE_TAC[IN_NUMSEG]; REPEAT WEAK_STRIP_TAC; INTRO_TAC DIVISION [`m`;`n`]; ASM_REWRITE_TAC[]; BY(ARITH_TAC) ]);;
(* }}} *)
let MOD_INJ = 
prove_by_refinement( `!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)`,
(* {{{ proof *) [ REPEAT GEN_TAC; 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; BY(MESON_TAC[ (arith `a <= b \/ b <= (a:num)`)]); CONJ2_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAK_STRIP_TAC; INTRO_TAC DIVISION [`a`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); INTRO_TAC DIVISION [`b`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `(b - a) DIV n = 0` ASSUME_TAC; GMATCH_SIMP_TAC DIV_LT; REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC); REWRITE_TAC[IN_NUMSEG]; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); SUBGOAL_THEN `(b - a) MOD n = 0` ASSUME_TAC; REWRITE_TAC[MOD_EQ_0]; ASM_SIMP_TAC[MOD_EQ_0]; EXISTS_TAC (`b DIV n - a DIV n`); REPEAT (FIRST_X_ASSUM_ST `( * ):num->num->num` MP_TAC); ASM_REWRITE_TAC[]; REWRITE_TAC[RIGHT_SUB_DISTRIB]; FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC; BY(ARITH_TAC); ENOUGH_TO_SHOW_TAC `b - a = 0`; FIRST_X_ASSUM_ST `a <= (b:num)` MP_TAC; BY(ARITH_TAC); INTRO_TAC DIVISION [`b - (a:num)`;`n`]; ASM_REWRITE_TAC[]; BY(ARITH_TAC) ]);;
(* }}} *)
let MOD_INJ1_ALT = 
prove_by_refinement (`!k n. ~( n = 0) /\ k < n /\ ~( k = 0) ==> (! x. ~( x MOD n = (x + k) MOD n)) `,
[ REPEAT STRIP_TAC; INTRO_TAC MOD_INJ [`n`;`x`;`x`;`x + (k:num)`]; ANTS_TAC; ASM_REWRITE_TAC[IN_NUMSEG]; REPEAT (FIRST_X_ASSUM MP_TAC); SIMP_TAC[LE_REFL; ARITH_RULE` ~( n = 0) ==> x <= n - 1 + x `; ARITH_RULE` a <= a + x:num `]; BY(ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC) ]);;
let MOD_SURJ = 
prove_by_refinement( `!n r a. ~(n=0) /\ a IN (0..(n-1)) ==> (?b. b IN (r..((n-1)+r)) /\ b MOD n = a)`,
(* {{{ proof *) [ REWRITE_TAC[IN_NUMSEG]; REPEAT WEAK_STRIP_TAC; ASM_CASES_TAC `r MOD n <= a`; EXISTS_TAC (`(r DIV n) * n + a`); INTRO_TAC DIVISION [`r`;`n`]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); REWRITE_TAC[ MOD_MULT_ADD]; MATCH_MP_TAC MOD_LT; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); EXISTS_TAC (`((r DIV n) + 1) * n + a`); REWRITE_TAC[ MOD_MULT_ADD ]; CONJ2_TAC; MATCH_MP_TAC MOD_LT; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); INTRO_TAC DIVISION [`r`;`n`]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC) ]);;
(* }}} *)
let BIJ_SUM = 
prove_by_refinement( `!(A:A->bool) (B:B->bool) f ab. BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
(* {{{ proof *) [ REWRITE_TAC[BIJ;INJ]; BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ]) ]);;
(* }}} *)
let periodic_sum = 
prove_by_refinement( `!f n. periodic f n /\ ~( n=0) ==> (!i. sum (i..((n-1) +i)) f = sum (0..(n-1)) f)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC BIJ_SUM [`i..((n-1)+i)`;`0..(n-1)`;`f`;`(\j. (j MOD n))`]; ANTS_TAC; REWRITE_TAC[BIJ;INJ]; SUBCONJ_TAC; CONJ_TAC; REPEAT WEAK_STRIP_TAC; BY(ASM_SIMP_TAC[ MOD_IN_NUMSEG]); REPEAT WEAK_STRIP_TAC; MATCH_MP_TAC MOD_INJ; BY(ASM_MESON_TAC[]); REPEAT WEAK_STRIP_TAC; REWRITE_TAC[SURJ]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; BY(ASM_MESON_TAC[MOD_SURJ]); DISCH_THEN (SUBST1_TAC o GSYM); AP_TERM_TAC; REWRITE_TAC[FUN_EQ_THM]; GEN_TAC; REWRITE_TAC[o_THM]; BY(ASM_MESON_TAC[periodic_mod]) ]);;
(* }}} *)
let periodic_fn = 
prove_by_refinement( `!cc. cc_bool_model_v11 cc ==> (periodic (cc_hassmall_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qu_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qx_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qy_v11 cc) (cc_card_v11 cc)) `,
(* {{{ proof *) [ REWRITE_TAC[cc_bool_model_v11;periodic;cc_hassmall_v11;cc_qu_v11;cc_qx_v11;cc_qy_v11]; REPEAT WEAK_STRIP_TAC; BY(ASM_SIMP_TAC[arith `!i. (i + cc_card_v11 cc) + 1 = (i + 1) + cc_card_v11 cc`]) ]);;
(* }}} *)
let QX_NN = 
prove_by_refinement( `!cc i. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (cc_qx_v11 cc i) ==> (#0.0 <= cc_gg_v11 cc i)`,
(* {{{ proof *) [ REWRITE_TAC[cc_bool_model_v11;cc_real_model_v11]; REPEAT WEAK_STRIP_TAC; BY(ASM_SIMP_TAC[]) ]);;
(* }}} *)
let QY_NN = 
prove_by_refinement( `!cc i. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (cc_qy_v11 cc i) ==> (#0.0 <= cc_gg_v11 cc i)`,
(* {{{ proof *) [ REWRITE_TAC[cc_bool_model_v11;cc_real_model_v11]; REPEAT WEAK_STRIP_TAC; 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`; BY(REAL_ARITH_TAC); BY(ASM_SIMP_TAC[]) ]);;
(* }}} *)
let QY_QX_QU = 
prove_by_refinement( `!cc i. cc_bool_model_v11 cc ==> (cc_qu_v11 cc i \/ cc_qy_v11 cc i \/ cc_qx_v11 cc i)`,
(* {{{ proof *) [ REWRITE_TAC[cc_bool_model_v11]; REWRITE_TAC[cc_qu_v11;cc_qy_v11;cc_qx_v11]; BY(MESON_TAC[]) ]);;
(* }}} *)
let QUARTER1 = 
prove_by_refinement( `!cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ (sum (0..cc_card_v11 cc -1) (cc_gg_v11 cc) < &0) ==> (1 <= cc_size_v11 cc (cc_qu_v11 cc))`,
(* {{{ proof *) [ GEN_TAC; REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM_ST `cc_real_model_v11` MP_TAC; COPY_TAC; FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_TAC; COPY_TAC; REWRITE_TAC[cc_size_v11;cc_real_model_v11;cc_bool_model_v11]; REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `~(cc_card_v11 cc = 0)` ASSUME_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[arith `1 <= x <=> ~(x = 0)`]; GMATCH_SIMP_TAC CARD_EQ_0; CONJ_TAC; MATCH_MP_TAC FINITE_SUBSET; TYPIFY `0..cc_card_v11 cc - 1` EXISTS_TAC; REWRITE_TAC[FINITE_NUMSEG]; BY(SET_TAC[]); REWRITE_TAC[Misc_defs_and_lemmas.EMPTY_EXISTS]; TYPIFY `~(!i. ~(cc_qu_v11 cc i))` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[NOT_FORALL_THM]; REPEAT WEAK_STRIP_TAC; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `i MOD (cc_card_v11 cc)`))); REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; GMATCH_SIMP_TAC MOD_IN_NUMSEG; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC (GSYM periodic_mod); ASM_REWRITE_TAC[]; BY(ASM_SIMP_TAC[periodic_fn]); DISCH_TAC; GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `?p. cc_gg_v11 cc p < &0`) MP_TAC)); TYPIFY `~(!i. &0 <= cc_gg_v11 cc i)` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[arith `&0 <= x <=> ~(x < &0)`]); DISCH_TAC; FIRST_X_ASSUM_ST `sum X f < &0` MP_TAC; REWRITE_TAC[arith `((x < &0) ==> F) <=> &0 <= x`]; MATCH_MP_TAC SUM_POS_LE; REWRITE_TAC[FINITE_NUMSEG]; REPEAT WEAK_STRIP_TAC; BY(ASM_SIMP_TAC[]); REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (ISPEC `p:num`)); REWRITE_TAC[]; GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `~(cc_qx_v11 cc p \/ cc_qy_v11 cc p)`))); BY(ASM_MESON_TAC[ QY_QX_QU]); FIRST_X_ASSUM MP_TAC; REWRITE_TAC[arith `x < &0 <=> ~(#0.0 <= x)`]; REWRITE_TAC[TAUT `(~a ==> ~b) <=> (b ==> a)`]; BY(ASM_MESON_TAC[QX_NN;QY_NN]) ]);;
(* }}} *)
let QU_EXISTS = 
prove_by_refinement( `!cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ sum (0..cc_card_v11 cc - 1) (cc_gg_v11 cc) < &0 ==> (?q. cc_qu_v11 cc q /\ q IN 0..cc_card_v11 cc - 1)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC QUARTER1 [`cc`]; ASM_REWRITE_TAC[]; REWRITE_TAC[cc_size_v11;arith `1 <= x <=> ~(x = 0)`]; GMATCH_SIMP_TAC CARD_EQ_0; REWRITE_TAC[Misc_defs_and_lemmas.EMPTY_EXISTS]; REWRITE_TAC[IN_ELIM_THM]; GMATCH_SIMP_TAC FINITE_SUBSET; CONJ2_TAC; BY(MESON_TAC[]); GOAL_TERM (fun w -> (EXISTS_TAC ( env w `0..cc_card_v11 cc - 1`))); REWRITE_TAC[FINITE_NUMSEG]; REWRITE_TAC[SUBSET;IN_ELIM_THM]; BY(MESON_TAC[]) ]);;
(* }}} *)
let CC_CARD2 = 
prove_by_refinement( `!cc. cc_bool_model_v11 cc /\ cc_real_model_v11 cc /\ sum (0..cc_card_v11 cc - 1) (cc_gg_v11 cc) < &0 ==> (2 <= cc_card_v11 cc)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC QU_EXISTS [`cc`]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; ENOUGH_TO_SHOW_TAC `~(cc_card_v11 cc = 1)`; REWRITE_TAC[arith `2 <= x <=> ~(x = 0) /\ ~(x = 1)`]; BY(ASM_MESON_TAC[cc_bool_model_v11]); DISCH_TAC; SUBGOAL_THEN `sum (0..cc_card_v11 cc -1) (cc_azim_v11 cc) = &2 * pi /\ cc_azim_v11 cc q < #2.8` MP_TAC; FIRST_X_ASSUM_ST `cc_qu_v11` MP_TAC; REWRITE_TAC[cc_qu_v11]; REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM_ST `cc_real_model_v11` MP_TAC; REWRITE_TAC[cc_real_model_v11]; REPEAT WEAK_STRIP_TAC; BY(ASM_SIMP_TAC[]); SUBGOAL_THEN `cc_card_v11 cc - 1 = 0` SUBST1_TAC; FIRST_X_ASSUM MP_TAC; BY(ARITH_TAC); REWRITE_TAC[NUMSEG_SING;SUM_SING]; SUBGOAL_THEN `q = 0` SUBST1_TAC; FIRST_X_ASSUM_ST `IN` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_NUMSEG]; BY(ARITH_TAC); REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM MP_TAC; ASM_REWRITE_TAC[]; MP_TAC Flyspeck_constants.bounds; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let CASE_3Q1H = 
prove_by_refinement( `!cc. cc_bool_model_v11 cc /\ ((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\ cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3))) ==> ~(?i. cc_qy_v11 cc i)`,
(* {{{ proof *) [ REWRITE_TAC[cc_qu_v11;cc_qy_v11]; REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\ ~(0 = cc_card_v11 cc)` ASSUME_TAC; BY(ASM_MESON_TAC[cc_bool_model_v11]); 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; FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM); REPEAT (GMATCH_SIMP_TAC (GSYM periodic_mod)); BY(ASM_REWRITE_TAC[]); REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `~(cc_4cell_v11 cc (i' MOD 4))` MP_TAC; FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM); REPEAT (GMATCH_SIMP_TAC (GSYM periodic_mod)); BY(ASM_REWRITE_TAC[]); REWRITE_TAC[TAUT `(~a ==> F) <=> a`]; 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; INTRO_TAC MOD_SURJ [`4`;`i`;`i' MOD 4`]; ASM_SIMP_TAC[MOD_IN_NUMSEG;arith `~(4 = 0)`]; REWRITE_TAC[IN_NUMSEG;arith `4 - 1 +i = i + 3`]; REWRITE_TAC[arith `(i <= b /\ b <= i + 3) <=> (b = i \/ b = i+1 \/ b = i+2 \/ b = i+3)`]; BY(MESON_TAC[]); BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let CC_EXISTS = 
prove_by_refinement( `!az gg gg3a gg3b sub cri super sma eta cell4 n. ?cc. cc_azim_v11 cc = az /\ cc_gg_v11 cc = gg /\ cc_gg3a_v11 cc = gg3a /\ cc_gg3b_v11 cc = gg3b /\ cc_subcrit_v11 cc = sub /\ cc_crit_v11 cc = cri /\ cc_supercrit_v11 cc = super /\ cc_small_v11 cc = sma /\ cc_small_eta_v11 cc = eta /\ cc_4cell_v11 cc = cell4 /\ cc_card_v11 cc = n`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `cc_v11 ([az;gg;gg3a;gg3b],([sub;cri;super;sma;eta;cell4],n))`))); REWRITE_TAC[FUN_EQ_THM]; 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]; BY(REWRITE_TAC[EL;HD;TL;arith `5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`]) ]);;
(* }}} *)
let periodic_numseg = 
prove_by_refinement( `!p n. periodic p n /\ ~(n = 0) /\ (!i. i IN 0..(n-1) ==> p i) ==> (!i. p i)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC periodic_mod; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; GMATCH_SIMP_TAC MOD_IN_NUMSEG; BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let cc_bool_model_simple = 
prove_by_refinement( `!cc. ~(cc_card_v11 cc = 0) /\ periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\ periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\ (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_crit_v11 cc i /\ cc_supercrit_v11 cc i)) /\ (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_crit_v11 cc i /\ cc_subcrit_v11 cc i)) /\ (!i. i IN 0..(cc_card_v11 cc - 1) ==> ~(cc_supercrit_v11 cc i /\ cc_subcrit_v11 cc i)) /\ (!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)) /\ (!i. i IN 0..(cc_card_v11 cc - 1) ==> (cc_small_eta_v11 cc i ==> cc_small_v11 cc i)) ==> cc_bool_model_v11 cc `,
(* {{{ proof *) [ REWRITE_TAC[cc_bool_model_v11]; REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; ABBREV_TAC `n = cc_card_v11 cc`; CONJ_TAC; MATCH_MP_TAC periodic_numseg; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; REWRITE_TAC[periodic]; BY(ASM_MESON_TAC[periodic]); CONJ_TAC; MATCH_MP_TAC periodic_numseg; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; REWRITE_TAC[periodic]; BY(ASM_MESON_TAC[periodic]); CONJ_TAC; MATCH_MP_TAC periodic_numseg; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; REWRITE_TAC[periodic]; BY(ASM_MESON_TAC[periodic]); CONJ_TAC; MATCH_MP_TAC periodic_numseg; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; REWRITE_TAC[periodic]; BY(ASM_MESON_TAC[periodic]); MATCH_MP_TAC periodic_numseg; GOAL_TERM (fun w -> (EXISTS_TAC ( env w `n`))); ASM_REWRITE_TAC[]; REWRITE_TAC[periodic]; BY(ASM_MESON_TAC[periodic]) ]);;
(* }}} *)
let cc_bool_model_simple2 = 
prove_by_refinement( `!cc cc'. ~(cc_card_v11 cc = 0) /\ cc_bool_model_v11 cc' /\ periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\ periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\ (!i. i IN 0..(cc_card_v11 cc - 1) ==> (?j. (cc_subcrit_v11 cc i = cc_subcrit_v11 cc' j) /\ (cc_crit_v11 cc i = cc_crit_v11 cc' j) /\ (cc_supercrit_v11 cc i = cc_supercrit_v11 cc' j) /\ (cc_small_v11 cc i = cc_small_v11 cc' j) /\ (cc_small_eta_v11 cc i = cc_small_eta_v11 cc' j) /\ (cc_4cell_v11 cc i = cc_4cell_v11 cc' j))) ==> cc_bool_model_v11 cc `,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; MATCH_MP_TAC cc_bool_model_simple; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `cc_bool_model_v11` MP_TAC; REWRITE_TAC[cc_bool_model_v11]; REPEAT WEAK_STRIP_TAC; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let cc_real_model_simple = 
prove_by_refinement( `!cc n. (cc_card_v11 cc = n) /\ ~(n = 0) /\ periodic (cc_azim_v11 cc) (cc_card_v11 cc) /\ periodic (cc_gg_v11 cc) (cc_card_v11 cc) /\ periodic (cc_gg3a_v11 cc) (cc_card_v11 cc) /\ periodic (cc_gg3b_v11 cc) (cc_card_v11 cc) /\ periodic (cc_subcrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_crit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_supercrit_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_v11 cc) (cc_card_v11 cc) /\ periodic (cc_small_eta_v11 cc) (cc_card_v11 cc) /\ periodic (cc_4cell_v11 cc) (cc_card_v11 cc) /\ periodic (cc_hassmall_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qu_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qx_v11 cc) (cc_card_v11 cc) /\ periodic (cc_qy_v11 cc) (cc_card_v11 cc) /\ (!i. (i IN 0..(n-1)) ==> (#0.606 <= cc_azim_v11 cc i)) /\ (!i. (i IN 0..(n-1)) ==> cc_4cell_v11 cc i ==> cc_azim_v11 cc i < #2.8) /\ (sum (0.. (cc_card_v11 cc - 1)) (cc_azim_v11 cc) = &2 * pi) /\ ((cc_card_v11 cc = 4) /\ (?i. cc_4cell_v11 cc i /\ cc_crit_v11 cc i /\ cc_qu_v11 cc (i+1) /\ cc_qu_v11 cc (i+2) /\ cc_qu_v11 cc (i+3)) ==> (&0 <= sum (0.. (cc_card_v11 cc -1)) (cc_gg_v11 cc))) /\ (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc i ==> -- cc_eps <= cc_gg_v11 cc i) /\ (!i. (i IN 0..(n-1)) ==> cc_qu_v11 cc i /\ ~(cc_small_eta_v11 cc i) ==> cc_eps <= cc_gg_v11 cc i ) /\ (!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 ) /\ (!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)) /\ (!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)) /\ (!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) /\ (!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) /\ (!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) /\ (!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) /\ (!i. (i IN 0..(n-1)) ==> cc_qx_v11 cc i ==> #0.0 <= cc_gg_v11 cc i) /\ (!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) /\ (!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)) /\ (!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)) /\ (!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) /\ (!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) /\ (!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) /\ (!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) /\ (!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) /\ (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> &0 <= cc_gg3a_v11 cc i) /\ (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> &0 <= cc_gg3b_v11 cc i) /\ (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i ==> #0.008 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ (!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 ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ (!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 ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ (!i. (i IN 0..(n-1)) ==> cc_qy_v11 cc i /\ cc_small_eta_v11 cc i /\ cc_small_eta_v11 cc (i+1) ==> a_spine5 + b_spine5 * cc_azim_v11 cc i <= cc_gg_v11 cc i) /\ (!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 /\ cc_azim_v11 cc i <= #2.089 ==> #3.0 * cc_eps <= cc_gg_v11 cc i) ==> cc_real_model_v11 cc `,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[cc_real_model_v11]; ASM_REWRITE_TAC[]; 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])) ]);;
(* }}} *)
let BIJ_NUMSEG = 
prove_by_refinement( `!s a b. BIJ (\j. j+ s) (a..b) (a+s..b+s)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[BIJ;INJ]; SUBCONJ_TAC; REWRITE_TAC[IN_NUMSEG]; BY(ARITH_TAC); REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[SURJ]; REWRITE_TAC[IN_NUMSEG]; REPEAT WEAK_STRIP_TAC; TYPIFY `(x:num) - s` EXISTS_TAC; REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC); BY(ARITH_TAC) ]);;
(* }}} *)
let cc_cut_sum = 
prove_by_refinement( `!f' x f n. ~(n=0) /\ periodic f' (n+1) /\ f 0 = f' x + f' (x +1) /\ (!i. i IN 1..n-1 ==> f i = f' (x + 1 + i)) ==> sum (0..n-1) f = sum (0..n) f'`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `sum (0..n) f' = sum(x..(x+n)) f'` (C SUBGOAL_THEN SUBST1_TAC); SUBST1_TAC (arith `(x:num) + n = (n + 1 ) - 1 + x` ); GMATCH_SIMP_TAC periodic_sum; ASM_REWRITE_TAC[arith `(n+1) - 1 = n`]; BY(ARITH_TAC); GMATCH_SIMP_TAC SUM_CLAUSES_LEFT; ASM_REWRITE_TAC[arith `0 + 1 = 1`;arith `0 <= n-1`]; ASM_CASES_TAC `n=1`; ASM_REWRITE_TAC[arith `1 - 1 = 0`]; ASM_SIMP_TAC[arith `0 < 1`;SUM_TRIV_NUMSEG]; GMATCH_SIMP_TAC SUM_CLAUSES_LEFT; REWRITE_TAC[SUM_SING_NUMSEG]; REWRITE_TAC[arith `x <= x + 1`]; BY(REAL_ARITH_TAC); SUBGOAL_THEN `2 <= n` ASSUME_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); TYPIFY `sum (x..x+n) f' = f' x + f' (x+1) + sum (x+2..x+n) f'` (C SUBGOAL_THEN SUBST1_TAC); GMATCH_SIMP_TAC SUM_CLAUSES_LEFT; GMATCH_SIMP_TAC SUM_CLAUSES_LEFT; BY(ASM_SIMP_TAC[arith `2 <= n ==> x + 1 <= x + n`;arith `x <= x + (n:num)`;arith `(x+1)+1 = x+2`]); TYPIFY `sum (x+2..x+n) f' = sum (1..(n-1)) (\i. f' (i + (x+1)))` (C SUBGOAL_THEN ASSUME_TAC); SUBST1_TAC (arith `x+2 = 1 + (x+1)`); MP_TAC (arith `~(n=0) ==> x + n = (n-1) + (x+1)`); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[ SUM_OFFSET]); ASM_REWRITE_TAC[]; REWRITE_TAC[arith `(a + b) + c = a + b + d <=> c = d`]; MATCH_MP_TAC SUM_EQ; BETA_TAC; REPEAT WEAK_STRIP_TAC; ASM_SIMP_TAC[]; AP_TERM_TAC; BY(ARITH_TAC) ]);;
(* }}} *)
let PERIODIC_PROPERTY= 
prove( ` ~(k = 0) /\ periodic vv k ==> (!i. vv (i MOD k)= vv i)`,
REWRITE_TAC[periodic] THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[th] THEN MP_TAC th) THEN ABBREV_TAC`n= i DIV k` THEN ASM_TAC THEN SPEC_TAC (`i:num`,`i:num`) THEN SPEC_TAC (`n:num`,`n:num`) THEN INDUCT_TAC THENL[REWRITE_TAC[ARITH_RULE`0*K+A=A`]; POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th`n *k + i MOD k`) THEN POP_ASSUM MP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MRESA_TAC MOD_MULT_ADD[`n:num`;`k:num`;`i MOD k`] THEN MRESA_TAC DIV_UNIQ[`n * k + i MOD k`;`k:num`;`n:num`;`i MOD k`] THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`SUC n * k + i MOD k = (n * k + i MOD k) +k`]]) ;;
end;;