Library/isum.ml

   1 (* ========================================================================= *)
   2 (* Define integer sums, with most theorems derived automatically.            *)
   3 (* ========================================================================= *)
   4
   5 let isum = new_definition
   6  `isum = iterate((+):int->int->int)`;;
   7
   8 let NEUTRAL_INT_ADD = prove
   9  (`neutral((+):int->int->int) = &0`,
  10   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
  11   MESON_TAC[INT_ADD_LID; INT_ADD_RID]);;
  12
  13 let MONOIDAL_INT_ADD = prove
  14  (`monoidal((+):int->int->int)`,
  15   REWRITE_TAC[monoidal; NEUTRAL_INT_ADD] THEN INT_ARITH_TAC);;
  16
  17 let ISUM_SUPPORT = prove
  18  (`!f s. isum (support (+) f s) f = isum s f`,
  19   REWRITE_TAC[isum; ITERATE_SUPPORT]);;
  20
  21 let int_isum = prove
  22  (`!f:A->int s. real_of_int(isum s f) = sum s (\x. real_of_int(f x))`,
  23   REPEAT GEN_TAC THEN REWRITE_TAC[sum; isum] THEN
  24   ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
  25   SUBGOAL_THEN
  26    `support(+) (\x:A. real_of_int(f x)) s = support(+) f s`
  27   SUBST1_TAC THENL
  28    [REWRITE_TAC[support; NEUTRAL_REAL_ADD; NEUTRAL_INT_ADD] THEN
  29     REWRITE_TAC[GSYM int_of_num_th; GSYM int_eq];
  30     ALL_TAC] THEN
  31   COND_CASES_TAC THEN
  32   ASM_REWRITE_TAC[NEUTRAL_REAL_ADD; NEUTRAL_INT_ADD; int_of_num_th] THEN
  33   POP_ASSUM MP_TAC THEN SPEC_TAC(`support(+) (f:A->int) s`,`s:A->bool`) THEN
  34   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  35   SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_INT_ADD; MONOIDAL_REAL_ADD] THEN
  36   SIMP_TAC[NEUTRAL_INT_ADD; NEUTRAL_REAL_ADD; int_of_num_th; int_add_th]);;
  37
  38 (* ------------------------------------------------------------------------- *)
  39 (* Generalize INT_OF_REAL_THM for most common sum patterns.                  *)
  40 (* ------------------------------------------------------------------------- *)
  41
  42 let INT_OF_REAL_THM =
  43   let dest = `real_of_int`
  44   and real_ty = `:real`
  45   and int_ty = `:int`
  46   and cond_th = prove
  47    (`real_of_int(if b then x else y) =
  48        if b then real_of_int x else real_of_int y`,
  49     COND_CASES_TAC THEN REWRITE_TAC[])
  50   and compose_th = prove
  51    (`(\x. real_of_int((f o g) x)) = (\x. real_of_int(f x)) o g`,
  52     REWRITE_TAC[o_DEF]) in
  53   let thlist = map GSYM
  54    [int_eq; int_le; int_lt; int_ge; int_gt;
  55     int_of_num_th; int_neg_th; int_add_th; int_mul_th;
  56     int_sub_th; int_abs_th; int_max_th; int_min_th; int_pow_th;
  57     int_isum; GSYM BETA_THM; GSYM ETA_AX; compose_th; cond_th] in
  58   let REW_RULE = GEN_REWRITE_RULE REDEPTH_CONV thlist in
  59   let is_fun_into_real ty =
  60     try match dest_type ty with
  61           "fun",[s;t] when t = real_ty -> mk_fun_ty s int_ty
  62         | "real",[] -> int_ty
  63         | _ -> failwith ""
  64     with Failure _ -> ty in
  65   let int_of_real_ty ty =
  66     try match dest_type ty with
  67           "real",[] -> int_ty
  68         | "fun",[s;t] when t = real_ty -> mk_fun_ty s int_ty
  69         | _ -> ty
  70     with Failure _ -> ty in
  71   let int_tm_of_real_var v =
  72      let s,ty = dest_var v in
  73      let tys,rty = splitlist dest_fun_ty ty in
  74      if rty <> real_ty then v else
  75      let ity = itlist mk_fun_ty tys int_ty in
  76      let vs = map genvar tys in
  77      list_mk_abs(vs,mk_comb(dest,list_mk_comb(mk_var(s,ity),vs))) in
  78   let int_of_real_var v =
  79      let s,ty = dest_var v in
  80      let tys,rty = splitlist dest_fun_ty ty in
  81      if rty <> real_ty then v else
  82      let ity = itlist mk_fun_ty tys int_ty in
  83      mk_var(s,ity) in
  84   let INT_OF_REAL_THM1 th =
  85     let newavs = subtract (frees (concl th)) (freesl (hyp th)) in
  86     let avs,bod = strip_forall(concl th) in
  87     let allavs = newavs@avs in
  88     let avs' = map int_tm_of_real_var allavs in
  89     let avs'' = map int_of_real_var avs in
  90     GENL avs'' (REW_RULE(SPECL avs' (GENL newavs th))) in
  91   let rec INT_OF_REAL_THM th =
  92     if is_conj(concl th) then CONJ (INT_OF_REAL_THM1 (CONJUNCT1 th))
  93                                    (INT_OF_REAL_THM1 (CONJUNCT2 th))
  94     else INT_OF_REAL_THM1 th in
  95   INT_OF_REAL_THM;;
  96
  97 (* ------------------------------------------------------------------------- *)
  98 (* Apply it in all the cases where it works.                                 *)
  99 (* ------------------------------------------------------------------------- *)
 100
 101 let CARD_EQ_ISUM = INT_OF_REAL_THM CARD_EQ_SUM;;
 102 let INT_SUB_POW = INT_OF_REAL_THM REAL_SUB_POW;;
 103 let ISUM_0 = INT_OF_REAL_THM SUM_0;;
 104 let ISUM_ABS = INT_OF_REAL_THM SUM_ABS;;
 105 let ISUM_ABS_BOUND = INT_OF_REAL_THM SUM_ABS_BOUND;;
 106 let ISUM_ABS_LE = INT_OF_REAL_THM SUM_ABS_LE;;
 107 let ISUM_ABS_NUMSEG = INT_OF_REAL_THM SUM_ABS_NUMSEG;;
 108 let ISUM_ADD = INT_OF_REAL_THM SUM_ADD;;
 109 let ISUM_ADD_NUMSEG = INT_OF_REAL_THM SUM_ADD_NUMSEG;;
 110 let ISUM_ADD_SPLIT = INT_OF_REAL_THM SUM_ADD_SPLIT;;
 111 let ISUM_BIJECTION = INT_OF_REAL_THM SUM_BIJECTION;;
 112 let ISUM_BOUND = INT_OF_REAL_THM SUM_BOUND;;
 113 let ISUM_BOUND_LT = INT_OF_REAL_THM SUM_BOUND_LT;;
 114 let ISUM_BOUND_LT_ALL = INT_OF_REAL_THM SUM_BOUND_LT_ALL;;
 115 let ISUM_CASES = INT_OF_REAL_THM SUM_CASES;;
 116 let ISUM_CLAUSES = INT_OF_REAL_THM SUM_CLAUSES;;
 117 let ISUM_CLAUSES_LEFT = INT_OF_REAL_THM SUM_CLAUSES_LEFT;;
 118 let ISUM_CLAUSES_NUMSEG = INT_OF_REAL_THM SUM_CLAUSES_NUMSEG;;
 119 let ISUM_CLAUSES_RIGHT = INT_OF_REAL_THM SUM_CLAUSES_RIGHT;;
 120 let ISUM_COMBINE_L = INT_OF_REAL_THM SUM_COMBINE_L;;
 121 let ISUM_COMBINE_R = INT_OF_REAL_THM SUM_COMBINE_R;;
 122 let ISUM_CONST = INT_OF_REAL_THM SUM_CONST;;
 123 let ISUM_CONST_NUMSEG = INT_OF_REAL_THM SUM_CONST_NUMSEG;;
 124 let ISUM_DELETE = INT_OF_REAL_THM SUM_DELETE;;
 125 let ISUM_DELETE_CASES = INT_OF_REAL_THM SUM_DELETE_CASES;;
 126 let ISUM_DELTA = INT_OF_REAL_THM SUM_DELTA;;
 127 let ISUM_DIFF = INT_OF_REAL_THM SUM_DIFF;;
 128 let ISUM_DIFFS = INT_OF_REAL_THM SUM_DIFFS;;
 129 let ISUM_EQ = INT_OF_REAL_THM SUM_EQ;;
 130 let ISUM_EQ_0 = INT_OF_REAL_THM SUM_EQ_0;;
 131 let ISUM_EQ_0_NUMSEG = INT_OF_REAL_THM SUM_EQ_0_NUMSEG;;
 132 let ISUM_EQ_GENERAL = INT_OF_REAL_THM SUM_EQ_GENERAL;;
 133 let ISUM_EQ_GENERAL_INVERSES = INT_OF_REAL_THM SUM_EQ_GENERAL_INVERSES;;
 134 let ISUM_EQ_NUMSEG = INT_OF_REAL_THM SUM_EQ_NUMSEG;;
 135 let ISUM_EQ_SUPERSET = INT_OF_REAL_THM SUM_EQ_SUPERSET;;
 136 let ISUM_GROUP = INT_OF_REAL_THM SUM_GROUP;;
 137 let ISUM_IMAGE = INT_OF_REAL_THM SUM_IMAGE;;
 138 let ISUM_IMAGE_GEN = INT_OF_REAL_THM SUM_IMAGE_GEN;;
 139 let ISUM_IMAGE_LE = INT_OF_REAL_THM SUM_IMAGE_LE;;
 140 let ISUM_IMAGE_NONZERO = INT_OF_REAL_THM SUM_IMAGE_NONZERO;;
 141 let ISUM_INCL_EXCL = INT_OF_REAL_THM SUM_INCL_EXCL;;
 142 let ISUM_INJECTION = INT_OF_REAL_THM SUM_INJECTION;;
 143 let ISUM_LE = INT_OF_REAL_THM SUM_LE;;
 144 let ISUM_LE_INCLUDED = INT_OF_REAL_THM SUM_LE_INCLUDED;;
 145 let ISUM_LE_NUMSEG = INT_OF_REAL_THM SUM_LE_NUMSEG;;
 146 let ISUM_LMUL = INT_OF_REAL_THM SUM_LMUL;;
 147 let ISUM_LT = INT_OF_REAL_THM SUM_LT;;
 148 let ISUM_LT_ALL = INT_OF_REAL_THM SUM_LT_ALL;;
 149 let ISUM_MULTICOUNT = INT_OF_REAL_THM SUM_MULTICOUNT;;
 150 let ISUM_MULTICOUNT_GEN = INT_OF_REAL_THM SUM_MULTICOUNT_GEN;;
 151 let ISUM_NEG = INT_OF_REAL_THM SUM_NEG;;
 152 let ISUM_OFFSET = INT_OF_REAL_THM SUM_OFFSET;;
 153 let ISUM_OFFSET_0 = INT_OF_REAL_THM SUM_OFFSET_0;;
 154 let ISUM_PARTIAL_PRE = INT_OF_REAL_THM SUM_PARTIAL_PRE;;
 155 let ISUM_PARTIAL_SUC = INT_OF_REAL_THM SUM_PARTIAL_SUC;;
 156 let ISUM_POS_BOUND = INT_OF_REAL_THM SUM_POS_BOUND;;
 157 let ISUM_POS_EQ_0 = INT_OF_REAL_THM SUM_POS_EQ_0;;
 158 let ISUM_POS_EQ_0_NUMSEG = INT_OF_REAL_THM SUM_POS_EQ_0_NUMSEG;;
 159 let ISUM_POS_LE = INT_OF_REAL_THM SUM_POS_LE;;
 160 let ISUM_POS_LE_NUMSEG = INT_OF_REAL_THM SUM_POS_LE_NUMSEG;;
 161 let ISUM_RESTRICT = INT_OF_REAL_THM SUM_RESTRICT;;
 162 let ISUM_RESTRICT_SET = INT_OF_REAL_THM SUM_RESTRICT_SET;;
 163 let ISUM_RMUL = INT_OF_REAL_THM SUM_RMUL;;
 164 let ISUM_SING = INT_OF_REAL_THM SUM_SING;;
 165 let ISUM_SING_NUMSEG = INT_OF_REAL_THM SUM_SING_NUMSEG;;
 166 let ISUM_SUB = INT_OF_REAL_THM SUM_SUB;;
 167 let ISUM_SUBSET = INT_OF_REAL_THM SUM_SUBSET;;
 168 let ISUM_SUBSET_SIMPLE = INT_OF_REAL_THM SUM_SUBSET_SIMPLE;;
 169 let ISUM_SUB_NUMSEG = INT_OF_REAL_THM SUM_SUB_NUMSEG;;
 170 let ISUM_ISUM_RESTRICT = INT_OF_REAL_THM SUM_SUM_RESTRICT;;
 171 let ISUM_SUPERSET = INT_OF_REAL_THM SUM_SUPERSET;;
 172 let ISUM_SWAP = INT_OF_REAL_THM SUM_SWAP;;
 173 let ISUM_SWAP_NUMSEG = INT_OF_REAL_THM SUM_SWAP_NUMSEG;;
 174 let ISUM_TRIV_NUMSEG = INT_OF_REAL_THM SUM_TRIV_NUMSEG;;
 175 let ISUM_UNION = INT_OF_REAL_THM SUM_UNION;;
 176 let ISUM_UNIONS_NONZERO = INT_OF_REAL_THM SUM_UNIONS_NONZERO;;
 177 let ISUM_UNION_EQ = INT_OF_REAL_THM SUM_UNION_EQ;;
 178 let ISUM_UNION_LZERO = INT_OF_REAL_THM SUM_UNION_LZERO;;
 179 let ISUM_UNION_NONZERO = INT_OF_REAL_THM SUM_UNION_NONZERO;;
 180 let ISUM_UNION_RZERO = INT_OF_REAL_THM SUM_UNION_RZERO;;
 181 let ISUM_ZERO_EXISTS = INT_OF_REAL_THM SUM_ZERO_EXISTS;;
 182 let REAL_OF_NUM_ISUM = INT_OF_REAL_THM REAL_OF_NUM_SUM;;
 183 let REAL_OF_NUM_ISUM_NUMSEG = INT_OF_REAL_THM REAL_OF_NUM_SUM_NUMSEG;;
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Manually derive the few cases where it doesn't.                           *)
 187 (*                                                                           *)
 188 (* Note that SUM_BOUND_GEN and SUM_BOUND_LT_GEN don't seem to have immediate *)
 189 (* analogs over the integers since they involve division.                    *)
 190 (*                                                                           *)
 191 (* Should really roll ADMISSIBLE_ISUM into "define" as well.                 *)
 192 (* ------------------------------------------------------------------------- *)
 193
 194 let ISUM_ISUM_PRODUCT = prove
 195  (`!s:A->bool t:A->B->bool x.
 196         FINITE s /\ (!i. i IN s ==> FINITE(t i))
 197         ==> isum s (\i. isum (t i) (x i)) =
 198             isum {i,j | i IN s /\ j IN t i} (\(i,j). x i j)`,
 199   REWRITE_TAC[isum] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
 200   REWRITE_TAC[MONOIDAL_INT_ADD]);;
 201
 202 let ADMISSIBLE_ISUM = prove
 203  (`!(<<) p:(B->C)->P->bool s:P->A h a b.
 204         admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
 205                        (\(k,x). s x) (\f (k,x). h f x k)
 206    ==> admissible(<<) p s (\f x. isum(a(x)..b(x)) (h f x))`,
 207   REWRITE_TAC[admissible; FORALL_PAIR_THM] THEN REPEAT STRIP_TAC THEN
 208   MATCH_MP_TAC ISUM_EQ_NUMSEG THEN ASM_MESON_TAC[]);;
 209
 210 let INT_SUB_POW_L1 = prove
 211  (`!x n. 1 <= n ==> &1 - x pow n = (&1 - x) * isum (0..n - 1) (\i. x pow i)`,
 212   SIMP_TAC[INT_OF_REAL_THM REAL_SUB_POW_L1; ETA_AX]);;
 213
 214 let INT_SUB_POW_R1 = prove
 215  (`!x n. 1 <= n ==> x pow n - &1 = (x - &1) * isum (0..n - 1) (\i. x pow i)`,
 216   SIMP_TAC[INT_OF_REAL_THM REAL_SUB_POW_R1; ETA_AX]);;
 217
 218 (* ------------------------------------------------------------------------- *)
 219 (* Extend the congruences.                                                   *)
 220 (* ------------------------------------------------------------------------- *)
 221
 222 let th = prove
 223  (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
 224               ==> isum s (\i. f(i)) = isum s g) /\
 225    (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
 226               ==> isum(a..b) (\i. f(i)) = isum(a..b) g) /\
 227    (!f g p.   (!x. p x ==> f x = g x)
 228               ==> isum {y | p y} (\i. f(i)) = isum {y | p y} g)`,
 229   REPEAT STRIP_TAC THEN MATCH_MP_TAC ISUM_EQ THEN
 230   ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
 231   extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;