(* ========================================================================= *)
(* Define integer sums, with most theorems derived automatically.            *)
(* ========================================================================= *)

let isum = new_definition
 `isum = iterate((+):int->int->int)`;;
let NEUTRAL_INT_ADD = 
prove
 (`neutral((+):int->int->int) = &0`,

  REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
  MESON_TAC[INT_ADD_LID; INT_ADD_RID]);;
let MONOIDAL_INT_ADD = 
prove
 (`monoidal((+):int->int->int)`,

  REWRITE_TAC[monoidal; NEUTRAL_INT_ADD] THEN INT_ARITH_TAC);;
let ISUM_SUPPORT = 
prove
 (`!f s. isum (support (+) f s) f = isum s f`,

  REWRITE_TAC[isum; ITERATE_SUPPORT]);;
let int_isum = 
prove
 (`!f:A->int s. real_of_int(isum s f) = sum s (\x. real_of_int(f x))`,

  REPEAT GEN_TAC THEN REWRITE_TAC[sum; isum] THEN
  ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
  SUBGOAL_THEN
   `support(+) (\x:A. real_of_int(f x)) s = support(+) f s`
  SUBST1_TAC THENL
   [REWRITE_TAC[support; NEUTRAL_REAL_ADD; NEUTRAL_INT_ADD] THEN
    REWRITE_TAC[GSYM int_of_num_th; GSYM int_eq];
    ALL_TAC] THEN
  COND_CASES_TAC THEN
  ASM_REWRITE_TAC[NEUTRAL_REAL_ADD; NEUTRAL_INT_ADD; int_of_num_th] THEN
  POP_ASSUM MP_TAC THEN SPEC_TAC(`support(+) (f:A->int) s`,`s:A->bool`) THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_INT_ADD; MONOIDAL_REAL_ADD] THEN
  SIMP_TAC[NEUTRAL_INT_ADD; NEUTRAL_REAL_ADD; int_of_num_th; int_add_th]);;
(* ------------------------------------------------------------------------- *)
(* Generalize INT_OF_REAL_THM for most common sum patterns.                  *)
(* ------------------------------------------------------------------------- *)

let INT_OF_REAL_THM =
  let dest = `real_of_int`
  and real_ty = `:real`
  and int_ty = `:int`
  and cond_th = prove
   (`real_of_int(if b then x else y) =
       if b then real_of_int x else real_of_int y`,
    COND_CASES_TAC THEN REWRITE_TAC[])
  and compose_th = prove
   (`(\x. real_of_int((f o g) x)) = (\x. real_of_int(f x)) o g`,
    REWRITE_TAC[o_DEF]) in
  let thlist = map GSYM
   [int_eq; int_le; int_lt; int_ge; int_gt;
    int_of_num_th; int_neg_th; int_add_th; int_mul_th;
    int_sub_th; int_abs_th; int_max_th; int_min_th; int_pow_th;
    int_isum; GSYM BETA_THM; GSYM ETA_AX; compose_th; cond_th] in
  let REW_RULE = GEN_REWRITE_RULE REDEPTH_CONV thlist in
  let is_fun_into_real ty =
    try match dest_type ty with
          "fun",[s;t] when t = real_ty -> mk_fun_ty s int_ty
        | "real",[] -> int_ty
        | _ -> failwith ""
    with Failure _ -> ty in
  let int_of_real_ty ty =
    try match dest_type ty with
          "real",[] -> int_ty
        | "fun",[s;t] when t = real_ty -> mk_fun_ty s int_ty
        | _ -> ty
    with Failure _ -> ty in
  let int_tm_of_real_var v =
     let s,ty = dest_var v in
     let tys,rty = splitlist dest_fun_ty ty in
     if rty <> real_ty then v else
     let ity = itlist mk_fun_ty tys int_ty in
     let vs = map genvar tys in
     list_mk_abs(vs,mk_comb(dest,list_mk_comb(mk_var(s,ity),vs))) in
  let int_of_real_var v =
     let s,ty = dest_var v in
     let tys,rty = splitlist dest_fun_ty ty in
     if rty <> real_ty then v else
     let ity = itlist mk_fun_ty tys int_ty in
     mk_var(s,ity) in
  let INT_OF_REAL_THM1 th =
    let newavs = subtract (frees (concl th)) (freesl (hyp th)) in
    let avs,bod = strip_forall(concl th) in
    let allavs = newavs@avs in
    let avs' = map int_tm_of_real_var allavs in
    let avs'' = map int_of_real_var avs in
    GENL avs'' (REW_RULE(SPECL avs' (GENL newavs th))) in
  let rec INT_OF_REAL_THM th =
    if is_conj(concl th) then CONJ (INT_OF_REAL_THM1 (CONJUNCT1 th))
                                   (INT_OF_REAL_THM1 (CONJUNCT2 th))
    else INT_OF_REAL_THM1 th in
  INT_OF_REAL_THM;;

(* ------------------------------------------------------------------------- *)
(* Apply it in all the cases where it works.                                 *)
(* ------------------------------------------------------------------------- *)

let CARD_EQ_ISUM = INT_OF_REAL_THM CARD_EQ_SUM;;
let INT_SUB_POW = INT_OF_REAL_THM REAL_SUB_POW;;
let ISUM_0 = INT_OF_REAL_THM SUM_0;;
let ISUM_ABS = INT_OF_REAL_THM SUM_ABS;;
let ISUM_ABS_BOUND = INT_OF_REAL_THM SUM_ABS_BOUND;;
let ISUM_ABS_LE = INT_OF_REAL_THM SUM_ABS_LE;;
let ISUM_ABS_NUMSEG = INT_OF_REAL_THM SUM_ABS_NUMSEG;;
let ISUM_ADD = INT_OF_REAL_THM SUM_ADD;;
let ISUM_ADD_NUMSEG = INT_OF_REAL_THM SUM_ADD_NUMSEG;;
let ISUM_ADD_SPLIT = INT_OF_REAL_THM SUM_ADD_SPLIT;;
let ISUM_BIJECTION = INT_OF_REAL_THM SUM_BIJECTION;;
let ISUM_BOUND = INT_OF_REAL_THM SUM_BOUND;;
let ISUM_BOUND_LT = INT_OF_REAL_THM SUM_BOUND_LT;;
let ISUM_BOUND_LT_ALL = INT_OF_REAL_THM SUM_BOUND_LT_ALL;;
let ISUM_CASES = INT_OF_REAL_THM SUM_CASES;;
let ISUM_CLAUSES = INT_OF_REAL_THM SUM_CLAUSES;;
let ISUM_CLAUSES_LEFT = INT_OF_REAL_THM SUM_CLAUSES_LEFT;;
let ISUM_CLAUSES_NUMSEG = INT_OF_REAL_THM SUM_CLAUSES_NUMSEG;;
let ISUM_CLAUSES_RIGHT = INT_OF_REAL_THM SUM_CLAUSES_RIGHT;;
let ISUM_COMBINE_L = INT_OF_REAL_THM SUM_COMBINE_L;;
let ISUM_COMBINE_R = INT_OF_REAL_THM SUM_COMBINE_R;;
let ISUM_CONST = INT_OF_REAL_THM SUM_CONST;;
let ISUM_CONST_NUMSEG = INT_OF_REAL_THM SUM_CONST_NUMSEG;;
let ISUM_DELETE = INT_OF_REAL_THM SUM_DELETE;;
let ISUM_DELETE_CASES = INT_OF_REAL_THM SUM_DELETE_CASES;;
let ISUM_DELTA = INT_OF_REAL_THM SUM_DELTA;;
let ISUM_DIFF = INT_OF_REAL_THM SUM_DIFF;;
let ISUM_DIFFS = INT_OF_REAL_THM SUM_DIFFS;;
let ISUM_EQ = INT_OF_REAL_THM SUM_EQ;;
let ISUM_EQ_0 = INT_OF_REAL_THM SUM_EQ_0;;
let ISUM_EQ_0_NUMSEG = INT_OF_REAL_THM SUM_EQ_0_NUMSEG;;
let ISUM_EQ_GENERAL = INT_OF_REAL_THM SUM_EQ_GENERAL;;
let ISUM_EQ_GENERAL_INVERSES = INT_OF_REAL_THM SUM_EQ_GENERAL_INVERSES;;
let ISUM_EQ_NUMSEG = INT_OF_REAL_THM SUM_EQ_NUMSEG;;
let ISUM_EQ_SUPERSET = INT_OF_REAL_THM SUM_EQ_SUPERSET;;
let ISUM_GROUP = INT_OF_REAL_THM SUM_GROUP;;
let ISUM_IMAGE = INT_OF_REAL_THM SUM_IMAGE;;
let ISUM_IMAGE_GEN = INT_OF_REAL_THM SUM_IMAGE_GEN;;
let ISUM_IMAGE_LE = INT_OF_REAL_THM SUM_IMAGE_LE;;
let ISUM_IMAGE_NONZERO = INT_OF_REAL_THM SUM_IMAGE_NONZERO;;
let ISUM_INCL_EXCL = INT_OF_REAL_THM SUM_INCL_EXCL;;
let ISUM_INJECTION = INT_OF_REAL_THM SUM_INJECTION;;
let ISUM_LE = INT_OF_REAL_THM SUM_LE;;
let ISUM_LE_INCLUDED = INT_OF_REAL_THM SUM_LE_INCLUDED;;
let ISUM_LE_NUMSEG = INT_OF_REAL_THM SUM_LE_NUMSEG;;
let ISUM_LMUL = INT_OF_REAL_THM SUM_LMUL;;
let ISUM_LT = INT_OF_REAL_THM SUM_LT;;
let ISUM_LT_ALL = INT_OF_REAL_THM SUM_LT_ALL;;
let ISUM_MULTICOUNT = INT_OF_REAL_THM SUM_MULTICOUNT;;
let ISUM_MULTICOUNT_GEN = INT_OF_REAL_THM SUM_MULTICOUNT_GEN;;
let ISUM_NEG = INT_OF_REAL_THM SUM_NEG;;
let ISUM_OFFSET = INT_OF_REAL_THM SUM_OFFSET;;
let ISUM_OFFSET_0 = INT_OF_REAL_THM SUM_OFFSET_0;;
let ISUM_PARTIAL_PRE = INT_OF_REAL_THM SUM_PARTIAL_PRE;;
let ISUM_PARTIAL_SUC = INT_OF_REAL_THM SUM_PARTIAL_SUC;;
let ISUM_POS_BOUND = INT_OF_REAL_THM SUM_POS_BOUND;;
let ISUM_POS_EQ_0 = INT_OF_REAL_THM SUM_POS_EQ_0;;
let ISUM_POS_EQ_0_NUMSEG = INT_OF_REAL_THM SUM_POS_EQ_0_NUMSEG;;
let ISUM_POS_LE = INT_OF_REAL_THM SUM_POS_LE;;
let ISUM_POS_LE_NUMSEG = INT_OF_REAL_THM SUM_POS_LE_NUMSEG;;
let ISUM_RESTRICT = INT_OF_REAL_THM SUM_RESTRICT;;
let ISUM_RESTRICT_SET = INT_OF_REAL_THM SUM_RESTRICT_SET;;
let ISUM_RMUL = INT_OF_REAL_THM SUM_RMUL;;
let ISUM_SING = INT_OF_REAL_THM SUM_SING;;
let ISUM_SING_NUMSEG = INT_OF_REAL_THM SUM_SING_NUMSEG;;
let ISUM_SUB = INT_OF_REAL_THM SUM_SUB;;
let ISUM_SUBSET = INT_OF_REAL_THM SUM_SUBSET;;
let ISUM_SUBSET_SIMPLE = INT_OF_REAL_THM SUM_SUBSET_SIMPLE;;
let ISUM_SUB_NUMSEG = INT_OF_REAL_THM SUM_SUB_NUMSEG;;
let ISUM_ISUM_RESTRICT = INT_OF_REAL_THM SUM_SUM_RESTRICT;;
let ISUM_SUPERSET = INT_OF_REAL_THM SUM_SUPERSET;;
let ISUM_SWAP = INT_OF_REAL_THM SUM_SWAP;;
let ISUM_SWAP_NUMSEG = INT_OF_REAL_THM SUM_SWAP_NUMSEG;;
let ISUM_TRIV_NUMSEG = INT_OF_REAL_THM SUM_TRIV_NUMSEG;;
let ISUM_UNION = INT_OF_REAL_THM SUM_UNION;;
let ISUM_UNIONS_NONZERO = INT_OF_REAL_THM SUM_UNIONS_NONZERO;;
let ISUM_UNION_EQ = INT_OF_REAL_THM SUM_UNION_EQ;;
let ISUM_UNION_LZERO = INT_OF_REAL_THM SUM_UNION_LZERO;;
let ISUM_UNION_NONZERO = INT_OF_REAL_THM SUM_UNION_NONZERO;;
let ISUM_UNION_RZERO = INT_OF_REAL_THM SUM_UNION_RZERO;;
let ISUM_ZERO_EXISTS = INT_OF_REAL_THM SUM_ZERO_EXISTS;;
let REAL_OF_NUM_ISUM = INT_OF_REAL_THM REAL_OF_NUM_SUM;;
let REAL_OF_NUM_ISUM_NUMSEG = INT_OF_REAL_THM REAL_OF_NUM_SUM_NUMSEG;;
(* ------------------------------------------------------------------------- *)
(* Manually derive the few cases where it doesn't.                           *)
(*                                                                           *)
(* Note that SUM_BOUND_GEN and SUM_BOUND_LT_GEN don't seem to have immediate *)
(* analogs over the integers since they involve division.                    *)
(*                                                                           *)
(* Should really roll ADMISSIBLE_ISUM into "define" as well.                 *)
(* ------------------------------------------------------------------------- *)

let ISUM_ISUM_PRODUCT = 
prove
 (`!s:A->bool t:A->B->bool x.
        FINITE s /\ (!i. i IN s ==> FINITE(t i))
        ==> isum s (\i. isum (t i) (x i)) =
            isum {i,j | i IN s /\ j IN t i} (\(i,j). x i j)`,

  REWRITE_TAC[isum] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
  REWRITE_TAC[MONOIDAL_INT_ADD]);;
let ADMISSIBLE_ISUM = 
prove
 (`!(<<) p:(B->C)->P->bool s:P->A h a b.
        admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
                       (\(k,x). s x) (\f (k,x). h f x k)
   ==> admissible(<<) p s (\f x. isum(a(x)..b(x)) (h f x))`,

  REWRITE_TAC[admissible; FORALL_PAIR_THM] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC ISUM_EQ_NUMSEG THEN ASM_MESON_TAC[]);;
let INT_SUB_POW_L1 = 
prove
 (`!x n. 1 <= n ==> &1 - x pow n = (&1 - x) * isum (0..n - 1) (\i. x pow i)`,

  SIMP_TAC[INT_OF_REAL_THM REAL_SUB_POW_L1; ETA_AX]);;
let INT_SUB_POW_R1 = 
prove
 (`!x n. 1 <= n ==> x pow n - &1 = (x - &1) * isum (0..n - 1) (\i. x pow i)`,

  SIMP_TAC[INT_OF_REAL_THM REAL_SUB_POW_R1; ETA_AX]);;
(* ------------------------------------------------------------------------- *)
(* Extend the congruences.                                                   *)
(* ------------------------------------------------------------------------- *)

let th = 
prove
 (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
              ==> isum s (\i. f(i)) = isum s g) /\
   (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
              ==> isum(a..b) (\i. f(i)) = isum(a..b) g) /\
   (!f g p.   (!x. p x ==> f x = g x)
              ==> isum {y | p y} (\i. f(i)) = isum {y | p y} g)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC ISUM_EQ THEN
  ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
  extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;