1 (* ========================================================================= *)
2 (* Define integer sums, with most theorems derived automatically. *)
3 (* ========================================================================= *)
5 let isum = new_definition
6 `isum = iterate((+):int->int->int)`;;
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]);;
13 let MONOIDAL_INT_ADD = prove
14 (`monoidal((+):int->int->int)`,
15 REWRITE_TAC[monoidal; NEUTRAL_INT_ADD] THEN INT_ARITH_TAC);;
17 let ISUM_SUPPORT = prove
18 (`!f s. isum (support (+) f s) f = isum s f`,
19 REWRITE_TAC[isum; ITERATE_SUPPORT]);;
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
26 `support(+) (\x:A. real_of_int(f x)) s = support(+) f s`
28 [REWRITE_TAC[support; NEUTRAL_REAL_ADD; NEUTRAL_INT_ADD] THEN
29 REWRITE_TAC[GSYM int_of_num_th; GSYM int_eq];
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]);;
38 (* ------------------------------------------------------------------------- *)
39 (* Generalize INT_OF_REAL_THM for most common sum patterns. *)
40 (* ------------------------------------------------------------------------- *)
43 let dest = `real_of_int`
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
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
64 with Failure _ -> ty in
65 let int_of_real_ty ty =
66 try match dest_type ty with
68 | "fun",[s;t] when t = real_ty -> mk_fun_ty s int_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
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
97 (* ------------------------------------------------------------------------- *)
98 (* Apply it in all the cases where it works. *)
99 (* ------------------------------------------------------------------------- *)
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;;
185 (* ------------------------------------------------------------------------- *)
186 (* Manually derive the few cases where it doesn't. *)
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. *)
191 (* Should really roll ADMISSIBLE_ISUM into "define" as well. *)
192 (* ------------------------------------------------------------------------- *)
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]);;
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[]);;
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]);;
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]);;
218 (* ------------------------------------------------------------------------- *)
219 (* Extend the congruences. *)
220 (* ------------------------------------------------------------------------- *)
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));;