real_sigmaScript.sml
1(* ************************************************************************* *)
2(* Sum of a real-valued function on a set: SIGMA f s *)
3(* ************************************************************************* *)
4
5Theory real_sigma
6Ancestors
7 arithmetic combin pair pred_set cardinal prim_rec permutes real
8 iterate
9Libs
10 res_quanTools hurdUtils numLib tautLib mesonLib jrhUtils
11 pred_setLib RealArith realSimps
12
13(* ------------------------------------------------------------------------- *)
14(* MESON, METIS, SET_TAC, SET_RULE, ASSERT_TAC, ASM_ARITH_TAC *)
15(* ------------------------------------------------------------------------- *)
16
17fun METIS ths tm = prove(tm,METIS_TAC ths);
18
19val DISC_RW_KILL = DISCH_TAC >> ONCE_ASM_REWRITE_TAC [] \\
20 POP_ASSUM K_TAC;
21
22fun ASSERT_TAC tm = SUBGOAL_THEN tm STRIP_ASSUME_TAC;
23
24val ASM_ARITH_TAC = rpt (POP_ASSUM MP_TAC) >> ARITH_TAC;
25val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC;
26
27(* Minimal hol-light compatibility layer *)
28val IMP_CONJ = CONJ_EQ_IMP; (* cardinalTheory *)
29val FINITE_SUBSET = SUBSET_FINITE_I; (* pred_setTheory *)
30
31Theorem REAL_LT_BETWEEN :
32 !a b:real. a < b <=> ?x. a < x /\ x < b
33Proof
34 metis_tac[REAL_MEAN, REAL_LT_TRANS]
35QED
36
37Theorem LOWER_BOUND_FINITE_SET_REAL:
38 !f:('a->real) s. FINITE(s) ==> ?a. !x. x IN s ==> a <= f(x)
39Proof
40 gen_tac >> Induct_on ‘FINITE’ >> rw[DISJ_IMP_THM, FORALL_AND_THM] >>
41 METIS_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS]
42QED
43
44
45Theorem UPPER_BOUND_FINITE_SET_REAL:
46 !f:('a->real) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a
47Proof
48 gen_tac >> Induct_on ‘FINITE’ >> rw[DISJ_IMP_THM, FORALL_AND_THM] >>
49 METIS_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS]
50QED
51
52Theorem REAL_LE_SQUARE_ABS :
53 !x y:real. abs(x) <= abs(y) <=> x pow 2 <= y pow 2
54Proof
55 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
56 EQ_TAC THEN DISCH_TAC THENL
57 [MATCH_MP_TAC POW_LE THEN ASM_REAL_ARITH_TAC,
58 CCONTR_TAC THEN UNDISCH_TAC ``abs (x:real) pow 2 <= abs y pow 2`` THEN
59 REWRITE_TAC [TWO, REAL_NOT_LE] THEN MATCH_MP_TAC POW_LT THEN
60 ASM_REAL_ARITH_TAC]
61QED
62
63Theorem REAL_EQ_SQUARE_ABS :
64 !x y:real. (abs x = abs y) <=> (x pow 2 = y pow 2)
65Proof
66 REWRITE_TAC[GSYM REAL_LE_ANTISYM, REAL_LE_SQUARE_ABS]
67QED
68
69Theorem REAL_HALF :
70 (!e:real. &0 < e / &2 <=> &0 < e) /\
71 (!e:real. e / &2 + e / &2 = e) /\
72 (!e:real. &2 * (e / &2) = e)
73Proof
74 SIMP_TAC std_ss [REAL_LT_HALF1, REAL_HALF_DOUBLE, REAL_DIV_LMUL,
75 REAL_ARITH ``2 <> 0:real``]
76QED
77
78Theorem REAL_BOUNDS_LT :
79 !x k:real. -k < x /\ x < k <=> abs(x) < k
80Proof
81 REAL_ARITH_TAC
82QED
83
84Theorem REAL_LE_BETWEEN :
85 !a b. a <= b <=> ?x:real. a <= x /\ x <= b
86Proof
87 MESON_TAC[REAL_LE_TRANS, REAL_LE_REFL]
88QED
89
90Theorem ABS_LE_0 :
91 !x:real. abs x <= &0 <=> (x = 0)
92Proof
93 MESON_TAC[REAL_LE_ANTISYM, ABS_ZERO, ABS_POS]
94QED
95
96Theorem REAL_OF_NUM_GE :
97 !m n. &m >= (&n:real) <=> m >= n
98Proof
99 REWRITE_TAC[GE, real_ge, REAL_OF_NUM_LE]
100QED
101
102Theorem REAL_LT_LCANCEL_IMP :
103 !x y z:real. &0 < x /\ x * y < x * z ==> y < z
104Proof
105 METIS_TAC [REAL_LT_LMUL]
106QED
107
108Theorem REAL_LT_POW2:
109 !n:num. (&0:real) < &2 pow n
110Proof
111 SIMP_TAC arith_ss [REAL_POW_LT, REAL_LT]
112QED
113
114(* for HOL-Light compatibility *)
115Theorem REAL_LT_INV2 = REAL_LT_INV
116
117Theorem REAL_WLOG_LE:
118 (!x y:real. P x y <=> P y x) /\ (!x y. x <= y ==> P x y) ==> !x y. P x y
119Proof
120 METIS_TAC[REAL_LE_TOTAL]
121QED
122
123Theorem REAL_WLOG_LT:
124 (!x. P x x) /\ (!x y. P x y <=> P y x) /\ (!x y. x < y ==> P x y)
125 ==> !x y:real. P x y
126Proof
127 METIS_TAC[REAL_LT_TOTAL]
128QED
129
130(* ------------------------------------------------------------------------- *)
131(* Non-trivial intervals of reals are infinite. *)
132(* ------------------------------------------------------------------------- *)
133
134Theorem FINITE_REAL_INTERVAL:
135 (!a. ~FINITE {x:real | a < x}) /\
136 (!a. ~FINITE {x:real | a <= x}) /\
137 (!b. ~FINITE {x:real | x < b}) /\
138 (!b. ~FINITE {x:real | x <= b}) /\
139 (!a b. FINITE {x:real | a < x /\ x < b} <=> b <= a) /\
140 (!a b. FINITE {x:real | a <= x /\ x < b} <=> b <= a) /\
141 (!a b. FINITE {x:real | a < x /\ x <= b} <=> b <= a) /\
142 (!a b. FINITE {x:real | a <= x /\ x <= b} <=> b <= a)
143Proof
144 SUBGOAL_THEN ``!a b. FINITE {x:real | a < x /\ x < b} <=> b <= a``
145 ASSUME_TAC THENL
146 [ (* goal 1 (of 2) *)
147 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN
148 ASM_CASES_TAC ``a:real < b`` THEN
149 ASM_SIMP_TAC std_ss [REAL_ARITH ``~(a:real < b) ==> ~(a < x /\ x < b)``] THEN
150 REWRITE_TAC[GSPEC_F, FINITE_EMPTY] THEN
151 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
152 DISCH_THEN(MP_TAC o SPEC ``IMAGE (\n. a + (b - a) / (&n + &2:real)) univ(:num)``) THEN
153 SIMP_TAC std_ss [SUBSET_DEF, FORALL_IN_IMAGE, IN_UNIV, GSPECIFICATION] THEN
154 SIMP_TAC std_ss [REAL_LT_ADDR, REAL_ARITH ``a + x / y < b <=> x / y < b - a:real``] THEN
155 KNOW_TAC ``!n. &0:real < &n + &2`` THENL [GEN_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
156 EXISTS_TAC ``&n:real`` THEN RW_TAC std_ss [REAL_POS, REAL_LT_ADDR] THEN
157 REAL_ARITH_TAC, ALL_TAC] THEN DISCH_TAC THEN
158 ASM_SIMP_TAC std_ss [REAL_LT_DIV, REAL_SUB_LT, REAL_LT_LDIV_EQ, NOT_IMP] THEN
159 REWRITE_TAC[REAL_ARITH ``x:real < x * (n + &2) <=> &0 < x * (n + &1)``] THEN
160 KNOW_TAC ``!n. &0:real < &n + &1`` THENL [GEN_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
161 EXISTS_TAC ``&n:real`` THEN RW_TAC std_ss [REAL_POS, REAL_LT_ADDR] THEN
162 REAL_ARITH_TAC, ALL_TAC] THEN DISCH_TAC THEN
163 ASM_SIMP_TAC std_ss [REAL_SUB_LT, REAL_LT_DIV, REAL_LT_RMUL_0] THEN
164 MP_TAC num_INFINITE THEN MATCH_MP_TAC EQ_IMPLIES THEN
165 AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
166 MATCH_MP_TAC FINITE_IMAGE_INJ_EQ THEN
167 KNOW_TAC ``!n m a b. a < b:real ==> ((a + (b - a) / (&n + &2:real) =
168 a + (b - a) / (&m + &2)) <=> (&n:real = &m:real))`` THENL
169 [REPEAT STRIP_TAC THEN SIMP_TAC std_ss [REAL_EQ_LADD, real_div, REAL_EQ_LMUL] THEN
170 SIMP_TAC std_ss [REAL_INV_INJ, REAL_EQ_RADD] THEN
171 METIS_TAC [REAL_SUB_0, REAL_LT_IMP_NE], ALL_TAC] THEN DISCH_TAC THEN
172 ASM_SIMP_TAC std_ss [REAL_OF_NUM_EQ],
173 (* goal 2 (of 2) *)
174 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL
175 [DISCH_THEN(MP_TAC o SPEC ``{x:real | a < x /\ x < a + &1}`` o
176 MATCH_MP(REWRITE_RULE[GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
177 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN REAL_ARITH_TAC,
178 DISCH_THEN(MP_TAC o SPEC ``{x:real | a < x /\ x < a + &1}`` o
179 MATCH_MP(REWRITE_RULE[GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
180 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN REAL_ARITH_TAC,
181 DISCH_THEN(MP_TAC o SPEC ``{x:real | b - &1 < x /\ x < b}`` o
182 MATCH_MP(REWRITE_RULE[GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
183 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN REAL_ARITH_TAC,
184 DISCH_THEN(MP_TAC o SPEC ``{x:real | b - &1 < x /\ x < b}`` o
185 MATCH_MP(REWRITE_RULE[GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
186 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN REAL_ARITH_TAC,
187 REWRITE_TAC[REAL_ARITH
188 ``a:real <= x /\ x < b <=> (a < x /\ x < b) \/ ~(b <= a) /\ (x = a)``] THEN
189 ASM_CASES_TAC ``b:real <= a`` THEN ASM_REWRITE_TAC[GSPEC_F, FINITE_EMPTY] THEN
190 KNOW_TAC ``!x a b:real. {x | a < x /\ x < b \/ (x = a)} =
191 {x | a < x /\ x < b} UNION {x | x = a}`` THENL
192 [SET_TAC [], ALL_TAC] THEN DISCH_TAC THEN CCONTR_TAC THEN
193 UNDISCH_TAC ``~(b <= a:real)`` THEN FULL_SIMP_TAC std_ss [] THEN
194 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC [] THEN METIS_TAC [FINITE_UNION],
195 REWRITE_TAC[REAL_ARITH
196 ``a:real < x /\ x <= b <=> (a < x /\ x < b) \/ ~(b <= a) /\ (x = b)``] THEN
197 ASM_CASES_TAC ``b:real <= a`` THEN ASM_REWRITE_TAC[GSPEC_F, FINITE_EMPTY] THEN
198 KNOW_TAC ``!x a b:real. {x | a < x /\ x < b \/ (x = b)} =
199 {x | a < x /\ x < b} UNION {x | x = b}`` THENL
200 [SET_TAC [], ALL_TAC] THEN DISCH_TAC THEN CCONTR_TAC THEN
201 UNDISCH_TAC ``~(b <= a:real)`` THEN FULL_SIMP_TAC std_ss [] THEN
202 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC [] THEN METIS_TAC [FINITE_UNION],
203 ASM_CASES_TAC ``b:real = a`` THEN
204 ASM_SIMP_TAC std_ss [REAL_LE_ANTISYM, REAL_LE_REFL, GSPEC_EQ, GSPEC_EQ2, FINITE_SING] THEN
205 ASM_SIMP_TAC std_ss [REAL_ARITH
206 ``~(b:real = a) ==>
207 (a <= x /\ x <= b <=> (a < x /\ x < b) \/ ~(b <= a) /\ (x = a) \/
208 ~(b <= a) /\ (x = b))``] THEN
209 ASM_REWRITE_TAC[FINITE_UNION, SET_RULE
210 ``{x | p x \/ q x} = {x | p x} UNION {x | q x}``] THEN
211 ASM_CASES_TAC ``b:real <= a`` THEN
212 ASM_REWRITE_TAC[GSPEC_F, FINITE_EMPTY] THEN
213 KNOW_TAC ``!x a b:real. {x | a < x /\ x < b \/ (x = a) \/ (x = b)} =
214 {x | a < x /\ x < b} UNION {x | (x = a) \/ (x = b)}`` THENL
215 [SET_TAC [], ALL_TAC] THEN DISCH_TAC THEN CCONTR_TAC THEN
216 UNDISCH_TAC ``~(b <= a:real)`` THEN FULL_SIMP_TAC std_ss [] THEN
217 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC [] THEN METIS_TAC [FINITE_UNION] ] ]
218QED
219
220Theorem real_INFINITE:
221 INFINITE univ(:real)
222Proof
223 DISCH_THEN(MP_TAC o SPEC ``{x:real | 0:real <= x}`` o
224 MATCH_MP(REWRITE_RULE[GSYM AND_IMP_INTRO] SUBSET_FINITE)) THEN
225 REWRITE_TAC[FINITE_REAL_INTERVAL, SUBSET_UNIV]
226QED
227
228(* ------------------------------------------------------------------------- *)
229(* REAL_COMPLETE *)
230(* ------------------------------------------------------------------------- *)
231
232Theorem lemma1[local]:
233 !P s. (!x:real. P x ==> x <= s) = (!y:real. (?x. P x /\ y < x) ==> y < s)
234Proof
235 REPEAT GEN_TAC THEN EQ_TAC THENL
236 [DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THEN
237 FIRST_X_ASSUM (MP_TAC o SPEC ``x:real``) THEN ASM_REWRITE_TAC [] THEN
238 METIS_TAC [REAL_LTE_TRANS],
239 ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN RW_TAC std_ss [REAL_NOT_LE, REAL_NOT_LT] THEN
240 POP_ASSUM MP_TAC THEN GEN_REWR_TAC LAND_CONV [REAL_LT_BETWEEN] THEN
241 STRIP_TAC THEN EXISTS_TAC ``x':real`` THEN ASM_REWRITE_TAC [REAL_LE_LT] THEN
242 EXISTS_TAC ``x:real`` THEN ASM_REWRITE_TAC []]
243QED
244
245Theorem lemma2[local]:
246 !P s. (!M:real. (!x. P x ==> x <= M) ==> s <= M) = (!y. y < s ==> (?x. P x /\ y < x))
247Proof
248 REPEAT GEN_TAC THEN EQ_TAC THENL
249 [ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN
250 RW_TAC std_ss [REAL_NOT_LE, REAL_NOT_LT] THEN UNDISCH_TAC ``y < s:real`` THEN
251 GEN_REWR_TAC LAND_CONV [REAL_LT_BETWEEN] THEN STRIP_TAC THEN
252 EXISTS_TAC ``x:real`` THEN ASM_REWRITE_TAC [] THEN GEN_TAC THEN
253 METIS_TAC [REAL_LE_TRANS, REAL_LE_LT],
254 ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN RW_TAC std_ss [REAL_NOT_LE, REAL_NOT_LT] THEN
255 EXISTS_TAC ``M:real`` THEN METIS_TAC []]
256QED
257
258Theorem lemma3[local]:
259 (?s:real. !y. (?x. P x /\ y < x) <=> y < s) =
260 (?M:real. (!x. P x ==> x <= M) /\ (!M'. (!x. P x ==> x <= M') ==> M <= M'))
261Proof
262 SIMP_TAC std_ss [lemma1, lemma2] THEN METIS_TAC []
263QED
264
265Theorem lemma4[local]:
266 !P:real->bool.
267 ((?x. P x) /\ (?z. !x. P x ==> x < z) ==>
268 (?s. !y. (?x. P x /\ y < x) <=> y < s)) ==>
269 ((?x. P x) /\ (?s. !x. P x ==> x <= s)
270 ==> ?s. (!x. P x ==> x <= s) /\
271 !M'. (!x. P x ==> x <= M') ==> s <= M')
272Proof
273 REPEAT STRIP_TAC THEN REWRITE_TAC [GSYM lemma3] THEN
274 FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
275 [METIS_TAC [], ALL_TAC] THEN
276 EXISTS_TAC ``s + 1:real`` THEN GEN_TAC THEN STRIP_TAC THEN
277 FIRST_X_ASSUM (MP_TAC o SPEC ``x':real``) THEN
278 ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC
279QED
280
281Theorem REAL_COMPLETE:
282 !P:real->bool. (?x. P x) /\ (?M. !x. P x ==> x <= M)
283 ==> ?M. (!x. P x ==> x <= M) /\
284 !M'. (!x. P x ==> x <= M') ==> M <= M'
285Proof
286 GEN_TAC THEN MATCH_MP_TAC lemma4 THEN METIS_TAC [REAL_SUP_EXISTS]
287QED
288
289(* ------------------------------------------------------------------------- *)
290(* Supremum and infimum. *)
291(* ------------------------------------------------------------------------- *)
292
293(* The original definition is in HOL Light's "sets.ml",
294 HOL4's definition is in realTheory *)
295Theorem sup_alt:
296 sup s = @a:real. (!x. x IN s ==> x <= a) /\
297 !b. (!x. x IN s ==> x <= b) ==> a <= b
298Proof
299 SIMP_TAC std_ss [sup] THEN AP_TERM_TAC THEN ABS_TAC THEN
300 SIMP_TAC std_ss [SPECIFICATION, lemma1, lemma2, lemma3] THEN
301 METIS_TAC []
302QED
303
304Theorem SUP_EQ:
305 !s t. (!b:real. (!x. x IN s ==> x <= b) <=> (!x. x IN t ==> x <= b))
306 ==> (sup s = sup t)
307Proof
308 SIMP_TAC std_ss [sup_alt]
309QED
310
311Theorem SUP:
312 !s:real->bool. s <> {} /\ (?b. !x. x IN s ==> x <= b) ==>
313 (!x. x IN s ==> x <= sup s) /\
314 !b. (!x. x IN s ==> x <= b) ==> sup s <= b
315Proof
316 rw[sup_alt, IN_DEF] >> SELECT_ELIM_TAC >> rw[] >>
317 MATCH_MP_TAC REAL_COMPLETE >> metis_tac[MEMBER_NOT_EMPTY, IN_DEF]
318QED
319
320Theorem SUP_FINITE_LEMMA:
321 !s:real->bool. FINITE s /\ ~(s = {}) ==>
322 ?b:real. b IN s /\ !x. x IN s ==> x <= b
323Proof
324 Induct_on ‘FINITE’ >> dsimp[] >>
325 METIS_TAC[REAL_LE_TOTAL, REAL_LE_TRANS, MEMBER_NOT_EMPTY]
326QED
327
328Theorem SUP_FINITE:
329 !s. FINITE s /\ ~(s = {}) ==> (sup s) IN s /\ !x. x IN s ==> x <= sup s
330Proof METIS_TAC [REAL_LE_ANTISYM, REAL_LE_TOTAL, SUP, SUP_FINITE_LEMMA]
331QED
332
333Theorem REAL_LE_SUP_FINITE:
334 !s a:real. FINITE s /\ ~(s = {}) ==> (a <= sup s <=> ?x. x IN s /\ a <= x)
335Proof METIS_TAC[SUP_FINITE, REAL_LE_TRANS]
336QED
337
338Theorem REAL_SUP_LE_FINITE:
339 !s a:real. FINITE s /\ ~(s = {}) ==> (sup s <= a <=> !x. x IN s ==> x <= a)
340Proof MESON_TAC[SUP_FINITE, REAL_LE_TRANS]
341QED
342
343Theorem REAL_LT_SUP_FINITE:
344 !s a:real. FINITE s /\ ~(s = {}) ==> (a < sup s <=> ?x. x IN s /\ a < x)
345Proof MESON_TAC[SUP_FINITE, REAL_LTE_TRANS]
346QED
347
348Theorem REAL_SUP_LT_FINITE:
349 !s a:real. FINITE s /\ ~(s = {}) ==> (sup s < a <=> !x. x IN s ==> x < a)
350Proof MESON_TAC[SUP_FINITE, REAL_LET_TRANS]
351QED
352
353Theorem SUP_UNIQUE_FINITE:
354 !s. FINITE s /\ s <> {} ==> (sup s = a <=> a IN s /\ !y. y IN s ==> y <= a)
355Proof
356 simp[GSYM REAL_LE_ANTISYM, REAL_LE_SUP_FINITE, REAL_SUP_LE_FINITE] THEN
357 MESON_TAC[REAL_LE_REFL, REAL_LE_TRANS, REAL_LE_ANTISYM]
358QED
359
360Theorem REAL_SUP_LE_EQ:
361 !s y:real. ~(s = {}) /\ (?b. !x. x IN s ==> x <= b) ==>
362 (sup s <= y <=> !x. x IN s ==> x <= y)
363Proof
364 METIS_TAC[SUP, REAL_LE_TRANS]
365QED
366
367Theorem REAL_SUP_UNIQUE:
368 !s b:real. (!x. x IN s ==> x <= b) /\
369 (!b'. b' < b ==> ?x. x IN s /\ b' < x)
370 ==> (sup s = b)
371Proof
372 REPEAT STRIP_TAC THEN REWRITE_TAC[sup_alt] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
373 ASM_MESON_TAC[REAL_NOT_LE, REAL_LE_ANTISYM]
374QED
375
376(* there's another REAL_SUP_LE in HOL's realTheory *)
377Theorem REAL_SUP_LE' :
378 !s b:real. ~(s = {}) /\ (!x. x IN s ==> x <= b) ==> sup s <= b
379Proof
380 METIS_TAC [SUP]
381QED
382
383Theorem REAL_SUP_LE_SUBSET:
384 !s t:real->bool. ~(s = {}) /\ s SUBSET t /\ (?b. !x. x IN t ==> x <= b)
385 ==> sup s <= sup t
386Proof
387 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_SUP_LE' THEN
388 MP_TAC(SPEC ``t:real->bool`` SUP) THEN ASM_SET_TAC[]
389QED
390
391Theorem REAL_LE_SUP2 : (* was: REAL_LE_SUP' (conflicted with realTheory) *)
392 !s a b y:real. y IN s /\ a <= y /\ (!x. x IN s ==> x <= b) ==> a <= sup s
393Proof
394 MESON_TAC [SUP, MEMBER_NOT_EMPTY, REAL_LE_TRANS]
395QED
396
397Theorem REAL_SUP_BOUNDS:
398 !s a b:real. ~(s = {}) /\ (!x. x IN s ==> a <= x /\ x <= b)
399 ==> a <= sup s /\ sup s <= b
400Proof
401 REPEAT GEN_TAC THEN STRIP_TAC THEN
402 MP_TAC(SPEC ``s:real->bool`` SUP) THEN
403 KNOW_TAC ``s <> {} /\ (?b. !x. x IN s ==> x <= b:real)`` THENL
404 [METIS_TAC[], DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC] THEN
405 UNDISCH_TAC ``s <> {}:real->bool`` THEN DISCH_TAC THEN
406 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
407 METIS_TAC[REAL_LE_TRANS]
408QED
409
410Theorem REAL_ABS_SUP_LE:
411 !s a:real. ~(s = {}) /\ (!x. x IN s ==> abs(x) <= a) ==> abs(sup s) <= a
412Proof
413 SIMP_TAC std_ss [ABS_BOUNDS] THEN METIS_TAC [REAL_SUP_BOUNDS]
414QED
415
416Theorem REAL_SUP_ASCLOSE:
417 !s l e:real. ~(s = {}) /\ (!x. x IN s ==> abs(x - l) <= e)
418 ==> abs(sup s - l) <= e
419Proof
420 SIMP_TAC std_ss [REAL_ARITH ``abs(x - l):real <= e <=> l - e <= x /\ x <= l + e``] THEN
421 METIS_TAC[REAL_SUP_BOUNDS]
422QED
423
424Theorem SUP_INSERT_FINITE:
425 !x s. FINITE s ==> (sup(x INSERT s) = if s = {} then x else max x (sup s))
426Proof
427 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
428 ASM_SIMP_TAC std_ss [SUP_UNIQUE_FINITE, FINITE_INSERT, FINITE_EMPTY,
429 NOT_INSERT_EMPTY, FORALL_IN_INSERT, NOT_IN_EMPTY] THEN
430 REWRITE_TAC[IN_SING, REAL_LE_REFL] THEN REWRITE_TAC[max_def] THEN
431 COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [SUP_FINITE, IN_INSERT, REAL_LE_REFL] THEN
432 ASM_MESON_TAC[SUP_FINITE, REAL_LE_TOTAL, REAL_LE_TRANS]
433QED
434
435Theorem SUP_SING:
436 !a. sup {a} = a
437Proof
438 SIMP_TAC std_ss [SUP_INSERT_FINITE, FINITE_EMPTY]
439QED
440
441Theorem SUP_UNIQUE:
442 !s b:real. (!c. (!x. x IN s ==> x <= c) <=> b <= c) ==> (sup s = b)
443Proof
444 REPEAT STRIP_TAC THEN GEN_REWR_TAC RAND_CONV [GSYM SUP_SING] THEN
445 MATCH_MP_TAC SUP_EQ THEN ASM_SET_TAC[]
446QED
447
448Theorem SUP_UNION:
449 !s t:real->bool. ~(s = {}) /\ ~(t = {}) /\ (?b. !x. x IN s ==> x <= b) /\
450 (?c. !x. x IN t ==> x <= c) ==> (sup(s UNION t) = max (sup s) (sup t))
451Proof
452 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUP_UNIQUE THEN
453 SIMP_TAC real_ss [FORALL_IN_UNION, REAL_MAX_LE] THEN METIS_TAC[SUP, REAL_LE_TRANS]
454QED
455
456Theorem REAL_IMP_SUP_LE' :
457 !p x. (?r. r IN p) /\ (!r. r IN p ==> r <= x) ==> sup p <= x
458Proof
459 REWRITE_TAC [IN_APP, REAL_IMP_SUP_LE]
460QED
461
462Theorem REAL_IMP_LE_SUP' :
463 !p x. (?z. !r. r IN p ==> r <= z) /\ (?r. r IN p /\ x <= r) ==> x <= sup p
464Proof
465 REWRITE_TAC [IN_APP, REAL_IMP_LE_SUP]
466QED
467
468Theorem REAL_LE_SUP_EQ :
469 !p x : real.
470 (?y. y IN p) /\ (?y. !z. z IN p ==> z <= y) ==>
471 (x <= sup p <=> !y. (!z. z IN p ==> z <= y) ==> x <= y)
472Proof
473 REWRITE_TAC [IN_APP, REAL_LE_SUP]
474QED
475
476(* This requires REAL_SUP_LE_EQ + REAL_LE_SUP_EQ *)
477Theorem SUP_MONO :
478 !p q. (?b. !n. p n <= b) /\ (?c. !n. q n <= c) /\
479 (!n:num. p n <= q n) ==> sup (IMAGE p UNIV) <= sup (IMAGE q UNIV)
480Proof
481 rpt STRIP_TAC
482 >> Q.ABBREV_TAC ‘y = sup (IMAGE q UNIV)’
483 >> Q.ABBREV_TAC ‘s = IMAGE p UNIV’
484 >> Know ‘sup s <= y <=> !x. x IN s ==> x <= y’
485 >- (MATCH_MP_TAC REAL_SUP_LE_EQ \\
486 rw [Abbr ‘s’, Once EXTENSION] \\
487 Q.EXISTS_TAC ‘b’ >> rw [] >> art [])
488 >> Rewr'
489 >> rw [Abbr ‘s’, IN_IMAGE]
490 >> rename1 ‘p x <= y’
491 >> Q.UNABBREV_TAC ‘y’
492 >> Q.ABBREV_TAC ‘s = IMAGE q UNIV’
493 >> Know ‘p x <= sup s <=> !y. (!z. z IN s ==> z <= y) ==> p x <= y’
494 >- (MATCH_MP_TAC REAL_LE_SUP_EQ \\
495 rw [Abbr ‘s’, IN_IMAGE] \\
496 Q.EXISTS_TAC ‘c’ >> rw [] >> art [])
497 >> Rewr'
498 >> rw [Abbr ‘s’, IN_IMAGE]
499 (* here it indicates that ‘!n. p n <= q n’ is too strong *)
500 >> MATCH_MP_TAC REAL_LE_TRANS
501 >> Q.EXISTS_TAC ‘q x’ >> art []
502 >> POP_ASSUM MATCH_MP_TAC
503 >> Q.EXISTS_TAC ‘x’ >> rw []
504QED
505
506(* The original definition of "inf" in HOL Light (sets.ml) *)
507val inf_tm = ``@a:real. (!x. x IN s ==> a <= x) /\
508 !b. (!x. x IN s ==> b <= x) ==> b <= a``;
509
510(* `inf s` exists iff s is non-empty and has a lower bound b *)
511val inf_criteria = ``s <> {} /\ (?b. !x. x IN s ==> b <= x)``;
512
513(* alternative definition of `inf` *)
514Theorem inf_alt :
515 !s. ^inf_criteria ==> (inf s = ^inf_tm)
516Proof
517 RW_TAC std_ss []
518 >> Suff `(\f. inf s = f) (^inf_tm)` >- METIS_TAC []
519 >> MATCH_MP_TAC SELECT_ELIM_THM
520 >> RW_TAC std_ss []
521 >- (Q.EXISTS_TAC `inf s` >> CONJ_TAC
522 >- (Know `(?y. s y) /\ (?y. !z. s z ==> y <= z)`
523 >- (STRONG_CONJ_TAC >- METIS_TAC [MEMBER_NOT_EMPTY, IN_APP] \\
524 STRIP_TAC >> `y IN s` by fs [IN_APP] >> RES_TAC \\
525 Q.EXISTS_TAC `b` >> rpt STRIP_TAC \\
526 FIRST_X_ASSUM MATCH_MP_TAC >> PROVE_TAC [IN_APP]) \\
527 DISCH_THEN (MP_TAC o (MATCH_MP REAL_INF_LE)) >> Rewr \\
528 Q.X_GEN_TAC `z` >> rpt STRIP_TAC \\
529 FIRST_X_ASSUM MATCH_MP_TAC >> fs [IN_APP]) \\
530 rpt STRIP_TAC >> MATCH_MP_TAC REAL_IMP_LE_INF \\
531 CONJ_TAC >- METIS_TAC [MEMBER_NOT_EMPTY, IN_APP] \\
532 fs [IN_APP])
533 >> RW_TAC std_ss [GSYM REAL_LE_ANTISYM]
534 >- (Know `(?y. s y) /\ (?y. !z. s z ==> y <= z)`
535 >- (STRONG_CONJ_TAC >- METIS_TAC [MEMBER_NOT_EMPTY, IN_APP] \\
536 STRIP_TAC >> `y IN s` by fs [IN_APP] >> RES_TAC \\
537 Q.EXISTS_TAC `b` >> rpt STRIP_TAC \\
538 FIRST_X_ASSUM MATCH_MP_TAC >> PROVE_TAC [IN_APP]) \\
539 DISCH_THEN (MP_TAC o (MATCH_MP REAL_INF_LE)) >> Rewr \\
540 rpt STRIP_TAC \\
541 Q.PAT_X_ASSUM `!b. (!x. x IN s ==> b <= x) ==> b <= x`
542 MATCH_MP_TAC >> fs [IN_APP])
543 >> MATCH_MP_TAC REAL_IMP_LE_INF
544 >> CONJ_TAC >- METIS_TAC [MEMBER_NOT_EMPTY, IN_APP]
545 >> fs [IN_APP]
546QED
547
548(* added `s <> EMPTY /\ (?b. !x. x IN s ==> b <= x) /\
549 t <> EMPTY /\ (?b. !x. x IN t ==> b <= x)`
550 to make sure that both `inf s` and `inf t` exist. *)
551Theorem INF_EQ :
552 !s t:real->bool. s <> EMPTY /\ (?b. !x. x IN s ==> b <= x) /\
553 t <> EMPTY /\ (?b. !x. x IN t ==> b <= x) /\
554 (!a. (!x. x IN s ==> a <= x) <=> (!x. x IN t ==> a <= x))
555 ==> (inf s = inf t)
556Proof
557 rpt STRIP_TAC
558 >> Know `(inf s = ^inf_tm) /\
559 (inf t = @a:real. (!x. x IN t ==> a <= x) /\
560 !b. (!x. x IN t ==> b <= x) ==> b <= a)`
561 >- (CONJ_TAC >> MATCH_MP_TAC inf_alt >> PROVE_TAC [])
562 >> ASM_SIMP_TAC std_ss []
563QED
564
565Theorem INF:
566 !s:real->bool. ~(s = {}) /\ (?b. !x. x IN s ==> b <= x)
567 ==> (!x. x IN s ==> inf s <= x) /\
568 !b. (!x. x IN s ==> b <= x) ==> b <= inf s
569Proof
570 GEN_TAC THEN STRIP_TAC THEN
571 Know `inf s = ^inf_tm` >- (MATCH_MP_TAC inf_alt >> PROVE_TAC []) >> Rewr'
572 THEN CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
573 ONCE_REWRITE_TAC[GSYM REAL_LE_NEG2] THEN
574 EXISTS_TAC ``-(sup (IMAGE (\x:real. -x) s))`` THEN
575 MP_TAC(SPEC ``IMAGE (\x. -x) (s:real->bool)`` SUP) THEN
576 REWRITE_TAC[REAL_NEG_NEG] THEN
577 ABBREV_TAC ``a = sup (IMAGE (\x:real. -x) s)`` THEN
578 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY, IN_IMAGE] THEN
579 ASM_MESON_TAC[REAL_NEG_NEG, MEMBER_NOT_EMPTY, REAL_LE_NEG2]
580QED
581
582Theorem INF_FINITE_LEMMA:
583 !s. FINITE s /\ ~(s = {}) ==> ?b:real. b IN s /\ !x. x IN s ==> b <= x
584Proof
585 REWRITE_TAC[CONJ_EQ_IMP] THEN
586 ONCE_REWRITE_TAC [METIS [] ``(s <> {} ==> ?b. b IN s /\ !x. x IN s ==> b <= x) =
587 (\s:real->bool. s <> {} ==> ?b. b IN s /\ !x. x IN s ==> b <= x) s``] THEN
588 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
589 REWRITE_TAC[NOT_INSERT_EMPTY, IN_INSERT] THEN
590 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
591 METIS_TAC[REAL_LE_TOTAL, REAL_LE_TRANS]
592QED
593
594Theorem INF_FINITE:
595 !s. FINITE s /\ ~(s = {}) ==> (inf s) IN s /\ !x. x IN s ==> inf s <= x
596Proof
597 GEN_TAC THEN DISCH_TAC THEN
598 FIRST_ASSUM(MP_TAC o MATCH_MP INF_FINITE_LEMMA) THEN
599 ASM_MESON_TAC[REAL_LE_ANTISYM, REAL_LE_TOTAL, INF]
600QED
601
602Theorem REAL_LE_INF_FINITE:
603 !s a:real. FINITE s /\ ~(s = {}) ==> (a <= inf s <=> !x. x IN s ==> a <= x)
604Proof
605 METIS_TAC[INF_FINITE, REAL_LE_TRANS]
606QED
607
608Theorem REAL_INF_LE_FINITE:
609 !s a:real. FINITE s /\ ~(s = {}) ==> (inf s <= a <=> ?x. x IN s /\ x <= a)
610Proof
611 MESON_TAC[INF_FINITE, REAL_LE_TRANS]
612QED
613
614Theorem REAL_LT_INF_FINITE:
615 !s a:real. FINITE s /\ ~(s = {}) ==> (a < inf s <=> !x. x IN s ==> a < x)
616Proof
617 METIS_TAC[INF_FINITE, REAL_LTE_TRANS]
618QED
619
620Theorem REAL_INF_LT_FINITE:
621 !s a:real. FINITE s /\ ~(s = {}) ==> (inf s < a <=> ?x. x IN s /\ x < a)
622Proof
623 METIS_TAC[INF_FINITE, REAL_LET_TRANS]
624QED
625
626Theorem REAL_INF_UNIQUE:
627 !s b:real. (!x. x IN s ==> b <= x) /\
628 (!b'. b < b' ==> ?x. x IN s /\ x < b')
629 ==> (inf s = b)
630Proof
631 rpt STRIP_TAC THEN
632 Know `s <> EMPTY`
633 >- (REWRITE_TAC [GSYM MEMBER_NOT_EMPTY] \\
634 POP_ASSUM (MP_TAC o (Q.SPEC `b + 1`)) \\
635 RW_TAC real_ss [REAL_LT_ADDR, REAL_LT_01] \\
636 Q.EXISTS_TAC `x` >> ASM_REWRITE_TAC []) >> DISCH_TAC \\
637 Know `inf s = ^inf_tm`
638 >- (MATCH_MP_TAC inf_alt >> PROVE_TAC []) >> Rewr' \\
639 MATCH_MP_TAC SELECT_UNIQUE THEN
640 METIS_TAC[REAL_NOT_LE, REAL_LE_ANTISYM]
641QED
642
643Theorem REAL_LE_INF:
644 !s b:real. ~(s = {}) /\ (!x. x IN s ==> b <= x) ==> b <= inf s
645Proof
646 MESON_TAC[INF]
647QED
648
649Theorem REAL_LE_INF_SUBSET:
650 !s t:real->bool. ~(t = {}) /\ t SUBSET s /\ (?b. !x. x IN s ==> b <= x)
651 ==> inf s <= inf t
652Proof
653 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_INF THEN
654 MP_TAC(SPEC ``s:real->bool`` INF) THEN ASM_SET_TAC[]
655QED
656
657Theorem REAL_INF_LE' :
658 !p x:real. (?y. y IN p) /\ (?y. !z. z IN p ==> y <= z) ==>
659 (inf p <= x <=> !y. (!z. z IN p ==> y <= z) ==> y <= x)
660Proof
661 REWRITE_TAC [IN_APP, REAL_INF_LE]
662QED
663
664Theorem REAL_INF_BOUNDS:
665 !s a b:real. ~(s = {}) /\ (!x. x IN s ==> a <= x /\ x <= b)
666 ==> a <= inf s /\ inf s <= b
667Proof
668 REPEAT GEN_TAC THEN STRIP_TAC THEN
669 MP_TAC(SPEC ``s:real->bool`` INF) THEN
670 KNOW_TAC ``s <> {} /\ (?b:real. !x. x IN s ==> b <= x)`` THENL
671 [ASM_MESON_TAC[], DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC] THEN
672 UNDISCH_TAC ``s <> {}:real->bool`` THEN DISCH_TAC THEN
673 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
674 METIS_TAC[REAL_LE_TRANS]
675QED
676
677Theorem REAL_ABS_INF_LE:
678 !s a:real. ~(s = {}) /\ (!x. x IN s ==> abs(x) <= a) ==> abs(inf s) <= a
679Proof
680 REWRITE_TAC[ABS_BOUNDS] THEN METIS_TAC [REAL_INF_BOUNDS]
681QED
682
683Theorem REAL_INF_ASCLOSE:
684 !s l e:real. ~(s = {}) /\ (!x. x IN s ==> abs(x - l) <= e)
685 ==> abs(inf s - l) <= e
686Proof
687 SIMP_TAC std_ss [REAL_ARITH ``abs(x - l):real <= e <=> l - e <= x /\ x <= l + e``] THEN
688 METIS_TAC[REAL_INF_BOUNDS]
689QED
690
691Theorem INF_UNIQUE_FINITE:
692 !s a. FINITE s /\ ~(s = {})
693 ==> ((inf s = a) <=> a IN s /\ !y. y IN s ==> a <= y)
694Proof
695 ASM_SIMP_TAC std_ss [GSYM REAL_LE_ANTISYM, REAL_LE_INF_FINITE, REAL_INF_LE_FINITE,
696 NOT_INSERT_EMPTY, FINITE_INSERT, FINITE_EMPTY] THEN
697 MESON_TAC[REAL_LE_REFL, REAL_LE_TRANS, REAL_LE_ANTISYM]
698QED
699
700Theorem INF_INSERT_FINITE:
701 !x s:real->bool. FINITE s ==> (inf(x INSERT s) = if s = {} then x else min x (inf s))
702Proof
703 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
704 ASM_SIMP_TAC std_ss [INF_UNIQUE_FINITE, FINITE_INSERT, FINITE_EMPTY,
705 NOT_INSERT_EMPTY, FORALL_IN_INSERT, NOT_IN_EMPTY] THEN
706 REWRITE_TAC[IN_SING, REAL_LE_REFL] THEN
707 REWRITE_TAC[min_def] THEN COND_CASES_TAC THEN
708 ASM_SIMP_TAC std_ss [INF_FINITE, IN_INSERT, REAL_LE_REFL] THEN
709 ASM_MESON_TAC[INF_FINITE, REAL_LE_TOTAL, REAL_LE_TRANS]
710QED
711
712Theorem REAL_SUP_EQ_INF:
713 !s:real->bool. ~(s = {}) /\ (?B. !x. x IN s ==> abs(x) <= B)
714 ==> ((sup s = inf s) <=> ?a. s = {a})
715Proof
716 REPEAT STRIP_TAC THEN EQ_TAC THENL
717 [DISCH_TAC THEN EXISTS_TAC ``sup (s:real->bool)`` THEN MATCH_MP_TAC
718 (SET_RULE ``~(s = {}) /\ (!x. x IN s ==> (x = a)) ==> (s = {a})``) THEN
719 ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
720 ASM_MESON_TAC[SUP, ABS_BOUNDS, INF],
721 STRIP_TAC THEN
722 ASM_SIMP_TAC std_ss [SUP_INSERT_FINITE, INF_INSERT_FINITE, FINITE_EMPTY]]
723QED
724
725Theorem INF_SING:
726 !a. inf {a} = a
727Proof
728 SIMP_TAC std_ss [INF_INSERT_FINITE, FINITE_EMPTY]
729QED
730
731(* ------------------------------------------------------------------------- *)
732(* Sums of real numbers. *)
733(* ------------------------------------------------------------------------- *)
734
735Definition sum_def[nocompute]:
736 (Sum :('a->bool)->('a->real)->real) = iterate (+)
737End
738
739Overload sum = ``Sum``
740
741Theorem NEUTRAL_REAL_ADD:
742 neutral((+):real->real->real) = &0
743Proof
744 REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
745 MESON_TAC[REAL_ADD_LID, REAL_ADD_RID]
746QED
747
748Theorem NEUTRAL_REAL_MUL:
749 neutral(( * ):real->real->real) = &1
750Proof
751 REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
752 MESON_TAC[REAL_MUL_LID, REAL_MUL_RID]
753QED
754
755Theorem MONOIDAL_REAL_ADD:
756 monoidal((+):real->real->real)
757Proof
758 REWRITE_TAC[monoidal, NEUTRAL_REAL_ADD] THEN REAL_ARITH_TAC
759QED
760
761Theorem MONOIDAL_REAL_MUL:
762 monoidal(( * ):real->real->real)
763Proof
764 REWRITE_TAC[monoidal, NEUTRAL_REAL_MUL] THEN REAL_ARITH_TAC
765QED
766
767Theorem SUM_DEGENERATE:
768 !f s. ~(FINITE {x | x IN s /\ ~(f x = &0)}) ==> (sum s f = &0)
769Proof
770 REPEAT GEN_TAC THEN REWRITE_TAC[sum_def] THEN
771 SIMP_TAC std_ss [iterate, support, NEUTRAL_REAL_ADD]
772QED
773
774Theorem SUM_CLAUSES:
775 (!f. sum {} f = &0) /\
776 (!x f s. FINITE(s)
777 ==> ((sum (x INSERT s) f =
778 if x IN s then sum s f else f(x) + sum s f)))
779Proof
780 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
781 KNOW_TAC ``monoidal ((+):real->real->real)`` THENL
782 [REWRITE_TAC[MONOIDAL_REAL_ADD], METIS_TAC [ITERATE_CLAUSES]]
783QED
784
785Theorem SUM_UNION:
786 !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
787 ==> ((sum (s UNION t) f = sum s f + sum t f))
788Proof
789 SIMP_TAC std_ss [sum_def, ITERATE_UNION, MONOIDAL_REAL_ADD]
790QED
791
792(* cf. realTheory.SUM_DIFF *)
793Theorem SUM_DIFF' : (* was: SUM_DIFF *)
794 !f s t. FINITE s /\ t SUBSET s ==> (sum (s DIFF t) f = sum s f - sum t f)
795Proof
796 SIMP_TAC std_ss [REAL_EQ_SUB_LADD, sum_def, ITERATE_DIFF, MONOIDAL_REAL_ADD]
797QED
798val SUM_DIFF = SUM_DIFF';
799
800Theorem SUM_INCL_EXCL:
801 !s t (f:'a->real).
802 FINITE s /\ FINITE t
803 ==> (sum s f + sum t f = sum (s UNION t) f + sum (s INTER t) f)
804Proof
805 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
806 MATCH_MP_TAC ITERATE_INCL_EXCL THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
807QED
808
809Theorem SUM_SUPPORT:
810 !f s. sum (support (+) f s) f = sum s f
811Proof
812 SIMP_TAC std_ss [sum_def, iterate, SUPPORT_SUPPORT]
813QED
814
815(* cf. realTheory.SUM_ADD *)
816Theorem SUM_ADD' : (* was: SUM_ADD *)
817 !f g s. FINITE s ==> (sum s (\x. f(x) + g(x)) = sum s f + sum s g)
818Proof
819 SIMP_TAC std_ss [sum_def, ITERATE_OP, MONOIDAL_REAL_ADD]
820QED
821val SUM_ADD = SUM_ADD';
822
823Theorem SUM_ADD_COUNT :
824 !f g n. sum (count n) (\x. f(x) + g(x)) = sum (count n) f + sum (count n) g
825Proof
826 rpt GEN_TAC
827 >> MATCH_MP_TAC SUM_ADD'
828 >> REWRITE_TAC [FINITE_COUNT]
829QED
830
831Theorem SUM_ADD_GEN:
832 !f g s.
833 FINITE {x | x IN s /\ ~(f x = &0)} /\ FINITE {x | x IN s /\ ~(g x = &0)}
834 ==> (sum s (\x. f x + g x) = sum s f + sum s g)
835Proof
836 REWRITE_TAC[GSYM NEUTRAL_REAL_ADD, GSYM support, sum_def] THEN
837 MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_REAL_ADD
838QED
839
840(* cf. realTheory.SUM_EQ_0 *)
841Theorem SUM_EQ_0' : (* was: SUM_EQ_0 *)
842 !f s. (!x:'a. x IN s ==> (f(x) = &0)) ==> (sum s f = &0)
843Proof
844 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
845 SIMP_TAC std_ss [ITERATE_EQ_NEUTRAL, MONOIDAL_REAL_ADD]
846QED
847val SUM_EQ_0 = SUM_EQ_0';
848
849(* cf. realTheory.SUM_0 *)
850Theorem SUM_0' : (* was: SUM_0 *)
851 !s:'a->bool. sum s (\n. &0) = &0
852Proof
853 SIMP_TAC std_ss [SUM_EQ_0]
854QED
855val SUM_0 = SUM_0';
856
857Theorem SUM_LMUL:
858 !f c s:'a->bool. sum s (\x. c * f(x)) = c * sum s f
859Proof
860 REPEAT GEN_TAC THEN ASM_CASES_TAC ``c = 0:real`` THEN
861 ASM_REWRITE_TAC[REAL_MUL_LZERO, SUM_0] THEN REWRITE_TAC[sum_def] THEN
862 ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
863 SUBGOAL_THEN ``support (+) (\x:'a. (c:real) * f(x)) s = support (+) f s`` SUBST1_TAC
864 THENL [ASM_SIMP_TAC std_ss [support, REAL_ENTIRE, NEUTRAL_REAL_ADD], ALL_TAC] THEN
865 COND_CASES_TAC THEN REWRITE_TAC[NEUTRAL_REAL_ADD, REAL_MUL_RZERO] THEN
866 POP_ASSUM MP_TAC THEN
867 SPEC_TAC(``support (+) f (s:'a->bool)``,``t:'a->bool``) THEN
868 REWRITE_TAC[GSYM sum_def] THEN Q.ABBREV_TAC `ss = support (+) f s` THEN
869 KNOW_TAC ``!ss. ((sum ss (\(x :'a). (c :real) * (f :'a -> real) x) = c * sum ss f)) =
870 (\ss. (sum ss (\(x :'a). (c :real) * (f :'a -> real) x) = c * sum ss f))ss`` THENL
871 [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
872 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
873 SIMP_TAC std_ss [SUM_CLAUSES, REAL_MUL_RZERO, REAL_MUL_LZERO,
874 REAL_ADD_LDISTRIB]]
875QED
876
877Theorem SUM_RMUL:
878 !f c s:'a->bool. sum s (\x. f(x) * c) = sum s f * c
879Proof
880 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[SUM_LMUL]
881QED
882
883(* cf. realTheory.SUM_NEG *)
884Theorem SUM_NEG' : (* was: SUM_NEG *)
885 !f s. sum s (\x. -(f(x))) = -(sum s f)
886Proof
887 ONCE_REWRITE_TAC[REAL_ARITH ``-x = -(1:real) * x``] THEN
888 SIMP_TAC std_ss [SUM_LMUL]
889QED
890val SUM_NEG = SUM_NEG';
891
892(* cf. realTheory.SUM_SUB *)
893Theorem SUM_SUB' : (* was: SUM_SUB *)
894 !f g s. FINITE s ==> (sum s (\x. f(x) - g(x)) = sum s f - sum s g)
895Proof
896 ONCE_REWRITE_TAC[real_sub] THEN SIMP_TAC std_ss [SUM_NEG, SUM_ADD]
897QED
898val SUM_SUB = SUM_SUB';
899
900(* cf. realTheory.SUM_LE *)
901Theorem SUM_LE' : (* was: SUM_LE, SUM_MONO_LE *)
902 !f g s. FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) ==> sum s f <= sum s g
903Proof
904 ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN REPEAT GEN_TAC THEN
905 KNOW_TAC ``((!(x :'a). x IN s ==> (f :'a -> real) x <= (g :'a -> real) x) ==>
906 sum s f <= sum s g) = (\(s:'a->bool). (!(x :'a). x IN s ==>
907 (f :'a -> real) x <= (g :'a -> real) x) ==> sum s f <= sum s g) s`` THENL
908 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
909 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
910 SIMP_TAC std_ss [SUM_CLAUSES, REAL_LE_REFL, REAL_LE_ADD2, IN_INSERT]
911QED
912val SUM_LE = SUM_LE';
913
914(* cf. realTheory.SUM_LT *)
915Theorem SUM_LT' : (* was: SUM_LT, SUM_MONO_LT *)
916 !f g s:'a->bool.
917 FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) /\
918 (?x. x IN s /\ f(x) < g(x))
919 ==> sum s f < sum s g
920Proof
921 REPEAT GEN_TAC THEN
922 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
923 DISCH_THEN(X_CHOOSE_THEN ``a:'a`` STRIP_ASSUME_TAC) THEN
924 SUBGOAL_THEN ``s = (a:'a) INSERT (s DELETE a)`` SUBST1_TAC THENL
925 [UNDISCH_TAC ``a:'a IN s`` THEN SIMP_TAC std_ss [INSERT_DELETE], ALL_TAC]
926 THEN ASM_SIMP_TAC std_ss [SUM_CLAUSES, FINITE_DELETE, IN_DELETE] THEN
927 ASM_SIMP_TAC std_ss [REAL_LTE_ADD2, SUM_LE, IN_DELETE, FINITE_DELETE]
928QED
929val SUM_LT = SUM_LT';
930
931Theorem SUM_LT_ALL:
932 !f g s. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < g(x))
933 ==> sum s f < sum s g
934Proof
935 MESON_TAC[MEMBER_NOT_EMPTY, REAL_LT_IMP_LE, SUM_LT]
936QED
937
938Theorem SUM_POS_LT:
939 !f s:'a->bool.
940 FINITE s /\
941 (!x. x IN s ==> &0 <= f x) /\
942 (?x. x IN s /\ &0 < f x)
943 ==> &0 < sum s f
944Proof
945 REPEAT STRIP_TAC THEN
946 MATCH_MP_TAC REAL_LET_TRANS THEN
947 EXISTS_TAC ``sum (s:'a->bool) (\i. 0:real)`` THEN CONJ_TAC THENL
948 [REWRITE_TAC[SUM_0, REAL_LE_REFL], MATCH_MP_TAC SUM_LT] THEN
949 ASM_MESON_TAC[]
950QED
951
952Theorem SUM_POS_LT_ALL:
953 !s f:'a->real.
954 FINITE s /\ ~(s = {}) /\ (!i. i IN s ==> (0:real) < f i)
955 ==> (0:real) < sum s f
956Proof
957 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_POS_LT THEN
958 ASM_MESON_TAC[MEMBER_NOT_EMPTY, REAL_LT_IMP_LE]
959QED
960
961(* cf. realTheory.SUM_EQ *)
962Theorem SUM_EQ' : (* was: SUM_EQ *)
963 !f g s. (!x. x IN s ==> (f x = g x)) ==> (sum s f = sum s g)
964Proof
965 REWRITE_TAC[sum_def] THEN
966 MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
967QED
968val SUM_EQ = SUM_EQ';
969
970Theorem SUM_EQ_COUNT :
971 !f g n. (!i. i < n ==> (f i = g i)) ==> (sum (count n) f = sum (count n) g)
972Proof
973 rpt STRIP_TAC
974 >> MATCH_MP_TAC SUM_EQ' >> rw []
975QED
976
977(* cf. realTheory.SUM_ABS *)
978Theorem SUM_ABS' : (* was: SUM_ABS *)
979 !f s. FINITE(s) ==> abs(sum s f) <= sum s (\x. abs(f x))
980Proof
981 REPEAT GEN_TAC THEN
982 KNOW_TAC ``(abs(sum s f) <= sum s (\x. abs(f x))) =
983 (\s. abs(sum s f) <= sum s (\x. abs(f x))) s`` THENL
984 [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
985 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
986 SIMP_TAC std_ss [SUM_CLAUSES, ABS_N, REAL_LE_REFL,
987 REAL_ARITH ``abs(a) <= b ==> abs(x + a) <= abs(x) + b:real``]]
988QED
989val SUM_ABS = SUM_ABS';
990
991(* cf. realTheory.SUN_ABS_LE *)
992Theorem SUM_ABS_LE' : (* was: SUM_ABS_LE *)
993 !f:'a->real g s.
994 FINITE s /\ (!x. x IN s ==> abs(f x) <= g x)
995 ==> abs(sum s f) <= sum s g
996Proof
997 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
998 EXISTS_TAC ``sum s (\x:'a. abs(f x))`` THEN
999 ASM_SIMP_TAC std_ss [SUM_ABS] THEN MATCH_MP_TAC SUM_LE THEN
1000 ASM_SIMP_TAC std_ss []
1001QED
1002val SUM_ABS_LE = SUM_ABS_LE';
1003
1004Theorem SUM_CONST:
1005 !c s. FINITE s ==> (sum s (\n. c) = &(CARD s) * c)
1006Proof
1007 REPEAT GEN_TAC THEN KNOW_TAC ``((sum s (\n. c) = &CARD s * c)) =
1008 (\s. (sum s (\n. c) = &CARD s * c)) s`` THENL [FULL_SIMP_TAC std_ss [],
1009 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1010 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1011 SIMP_TAC std_ss [SUM_CLAUSES, CARD_DEF, GSYM REAL_OF_NUM_SUC] THEN
1012 REPEAT STRIP_TAC THEN REAL_ARITH_TAC]
1013QED
1014
1015Theorem SUM_POS_LE:
1016 !s:'a->bool. (!x. x IN s ==> (0:real) <= f x) ==> (0:real) <= sum s f
1017Proof
1018 REPEAT STRIP_TAC THEN
1019 ASM_CASES_TAC ``FINITE {x:'a | x IN s /\ ~(f x = (0:real))}`` THEN
1020 ASM_SIMP_TAC std_ss [SUM_DEGENERATE, REAL_LE_REFL] THEN
1021 ONCE_REWRITE_TAC[GSYM SUM_SUPPORT] THEN
1022 REWRITE_TAC[support, NEUTRAL_REAL_ADD] THEN
1023 MP_TAC(ISPECL [``\x:'a. (0:real)``, ``f:'a->real``,
1024 ``{x:'a | x IN s /\ ~(f x = (0:real))}``] SUM_LE) THEN
1025 ASM_SIMP_TAC std_ss [SUM_0, GSPECIFICATION]
1026QED
1027
1028Theorem SUM_POS_BOUND:
1029 !f b s. FINITE s /\ (!x. x IN s ==> (0:real) <= f x) /\ sum s f <= b
1030 ==> !x:'a. x IN s ==> f x <= b
1031Proof
1032 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
1033 KNOW_TAC ``((!x. x IN s ==> 0 <= f x) ==>
1034 sum s f <= b ==> !x. x IN s ==> f x <= b) =
1035 (\s. (!x. x IN s ==> 0 <= f x) ==>
1036 sum s f <= b ==> !x. x IN s ==> f x <= b) s`` THENL
1037 [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1038 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1039 SIMP_TAC std_ss [SUM_CLAUSES, NOT_IN_EMPTY, IN_INSERT] THEN
1040 MESON_TAC[SUM_POS_LE, REAL_ARITH
1041 ``(0:real) <= x /\ (0:real) <= y /\ x + y <= b ==> x <= b /\ y <= b``]]
1042QED
1043
1044Theorem SUM_POS_EQ_0:
1045 !f s. FINITE s /\ (!x. x IN s ==> (0:real) <= f x) /\ (sum s f = (0:real))
1046 ==> !x. x IN s ==> (f x = (0:real))
1047Proof
1048 REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
1049 MESON_TAC[SUM_POS_BOUND, SUM_POS_LE]
1050QED
1051
1052Theorem SUM_ZERO_EXISTS:
1053 !(u:'a->real) s.
1054 FINITE s /\ (sum s u = (0:real))
1055 ==> (!i. i IN s ==> (u i = (0:real))) \/
1056 (?j k. j IN s /\ u j < (0:real) /\ k IN s /\ u k > (0:real))
1057Proof
1058 REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1059 (METIS [REAL_ARITH ``((0:real) <= -u <=> ~(u > (0:real))) /\
1060 ((0:real) <= u <=> ~(u < (0:real)))``]
1061 ``(?j k:'a. j IN s /\ u j < (0:real) /\ k IN s /\ u k > (0:real)) \/
1062 (!i. i IN s ==> (0:real) <= u i) \/ (!i. i IN s ==> (0:real) <= -(u i))``) THEN
1063 ASM_REWRITE_TAC[] THEN DISJ1_TAC THENL
1064 [ALL_TAC, ONCE_REWRITE_TAC[GSYM REAL_NEG_EQ0]] THENL
1065 [MATCH_MP_TAC SUM_POS_EQ_0 THEN ASM_REWRITE_TAC[SUM_NEG, REAL_NEG_0], ALL_TAC]
1066 THEN GEN_TAC THEN KNOW_TAC ``?(f:'a->real). !i. -(u:'a->real) i = f i`` THENL
1067 [EXISTS_TAC ``(\x. -(u:'a->real) x)`` THEN SIMP_TAC real_ss [], ALL_TAC] THEN
1068 STRIP_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC SUM_POS_EQ_0 THEN
1069 FULL_SIMP_TAC std_ss [] THEN UNDISCH_TAC ``sum s u = 0`` THEN
1070 GEN_REWR_TAC LAND_CONV [EQ_SYM_EQ] THEN DISCH_TAC THEN
1071 ONCE_REWRITE_TAC [GSYM REAL_NEG_EQ0] THEN ONCE_REWRITE_TAC [GSYM SUM_NEG]
1072 THEN ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC SUM_EQ THEN BETA_TAC THEN
1073 METIS_TAC [REAL_NEG_EQ]
1074QED
1075
1076Theorem SUM_DELETE:
1077 !f s a. FINITE s /\ a IN s ==> (sum (s DELETE a) f = sum s f - f(a))
1078Proof
1079 SIMP_TAC std_ss [REAL_ARITH ``(y = z - x) <=> (x + y = z:real)``, sum_def, ITERATE_DELETE,
1080 MONOIDAL_REAL_ADD]
1081QED
1082
1083Theorem SUM_DELETE_CASES:
1084 !f s a. FINITE s
1085 ==> (sum (s DELETE a) f = if a IN s then sum s f - f(a)
1086 else sum s f)
1087Proof
1088 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
1089 METIS_TAC [DELETE_NON_ELEMENT, SUM_DELETE]
1090QED
1091
1092Theorem SUM_SING:
1093 !f x. sum {x} f = f(x)
1094Proof
1095 SIMP_TAC std_ss [SUM_CLAUSES, FINITE_EMPTY, FINITE_INSERT, NOT_IN_EMPTY, REAL_ADD_RID]
1096QED
1097
1098Theorem SUM_DELTA:
1099 !s a. sum s (\x. if x = a:'a then b else &0) = if a IN s then b else &0
1100Proof
1101 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
1102 SIMP_TAC std_ss [ITERATE_DELTA, MONOIDAL_REAL_ADD]
1103QED
1104
1105Theorem SUM_SWAP:
1106 !f:'a->'b->real s t.
1107 FINITE(s) /\ FINITE(t)
1108 ==> ((sum s (\i. sum t (f i)) = sum t (\j. sum s (\i. f i j))))
1109Proof
1110 GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
1111 REPEAT GEN_TAC THEN KNOW_TAC ``(FINITE (t:'b->bool) ==>
1112 (sum s (\i. sum t (f i)) = sum t (\j. sum s (\i. f i j)))) = (\s. FINITE t ==>
1113 (sum s (\i. sum t (f i)) = sum t (\j. sum s (\i. f i j)))) (s:'a->bool)`` THENL
1114 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1115 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1116 FULL_SIMP_TAC std_ss [SUM_CLAUSES, SUM_0] THEN METIS_TAC [SUM_ADD, ETA_AX]
1117QED
1118
1119Theorem SUM_SWAP_COUNT :
1120 !(f:num->num->real) m n.
1121 sum (count m) (\i. sum (count n) (f i)) = sum (count n) (\j. sum (count m) (\i. f i j))
1122Proof
1123 rpt GEN_TAC
1124 >> MATCH_MP_TAC SUM_SWAP
1125 >> REWRITE_TAC [FINITE_COUNT]
1126QED
1127
1128Theorem SUM_IMAGE:
1129 !f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
1130 ==> (sum (IMAGE f s) g = sum s (g o f))
1131Proof
1132 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
1133 MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
1134QED
1135
1136Theorem SUM_SUPERSET:
1137 !f:'a->real u v.
1138 u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = (0:real)))
1139 ==> (sum v f = sum u f)
1140Proof
1141 SIMP_TAC std_ss [sum_def, GSYM NEUTRAL_REAL_ADD, ITERATE_SUPERSET, MONOIDAL_REAL_ADD]
1142QED
1143
1144Theorem lemma[local]:
1145 !s. DISJOINT {x | x IN s /\ P x} {x | x IN s /\ ~P x}
1146Proof
1147 GEN_TAC THEN SIMP_TAC std_ss [DISJOINT_DEF, INTER_DEF, EXTENSION, GSPECIFICATION]
1148 THEN GEN_TAC THEN EQ_TAC THENL
1149 [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]]
1150QED
1151
1152Theorem SUM_UNION_RZERO:
1153 !f:'a->real u v.
1154 FINITE u /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = (0:real)))
1155 ==> (sum (u UNION v) f = sum u f)
1156Proof
1157 REPEAT STRIP_TAC THEN SUBGOAL_THEN ``u UNION v = u UNION (v DIFF u)``
1158 ASSUME_TAC THENL [SET_TAC [], ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[lemma] THEN
1159 MATCH_MP_TAC SUM_SUPERSET THEN
1160 ASM_MESON_TAC[IN_UNION, IN_DIFF, SUBSET_DEF]
1161QED
1162
1163Theorem SUM_UNION_LZERO:
1164 !f:'a->real u v.
1165 FINITE v /\ (!x. x IN u /\ ~(x IN v) ==> (f(x) = (0:real)))
1166 ==> (sum (u UNION v) f = sum v f)
1167Proof
1168 MESON_TAC[SUM_UNION_RZERO, UNION_COMM]
1169QED
1170
1171Theorem SUM_RESTRICT:
1172 !f s. FINITE s ==> (sum s (\x. if x IN s then f(x) else (0:real)) = sum s f)
1173Proof
1174 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC std_ss []
1175QED
1176
1177(* cf. realTheory.SUM_BOUND *)
1178Theorem SUM_BOUND' : (* was: SUM_BOUND *)
1179 !s f b. FINITE s /\ (!x:'a. x IN s ==> f(x) <= b)
1180 ==> sum s f <= &(CARD s) * b
1181Proof
1182 SIMP_TAC std_ss [GSYM SUM_CONST, SUM_LE]
1183QED
1184Theorem SUM_BOUND[local] = SUM_BOUND'
1185
1186Theorem SUM_BOUND_GEN:
1187 !s f b. FINITE s /\ ~(s = {}) /\ (!x:'a. x IN s ==> f(x) <= b / &(CARD s))
1188 ==> sum s f <= b
1189Proof
1190 MESON_TAC[SUM_BOUND, REAL_DIV_LMUL, REAL_OF_NUM_EQ, CARD_EQ_0]
1191QED
1192
1193Theorem SUM_ABS_BOUND:
1194 !s f b. FINITE s /\ (!x:'a. x IN s ==> abs(f(x)) <= b)
1195 ==> abs(sum s f) <= &(CARD s) * b
1196Proof
1197 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1198 EXISTS_TAC ``sum s (\x:'a. abs(f x))`` THEN
1199 ASM_SIMP_TAC std_ss [SUM_BOUND, SUM_ABS]
1200QED
1201
1202Theorem SUM_BOUND_LT:
1203 !s f b. FINITE s /\ (!x:'a. x IN s ==> f x <= b) /\ (?x. x IN s /\ f x < b)
1204 ==> sum s f < &(CARD s) * b
1205Proof
1206 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
1207 EXISTS_TAC ``sum s (\x:'a. b)`` THEN CONJ_TAC THENL
1208 [MATCH_MP_TAC SUM_LT THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[],
1209 ASM_SIMP_TAC std_ss [SUM_CONST, REAL_LE_REFL]]
1210QED
1211
1212Theorem SUM_BOUND_LT_ALL:
1213 !s f b. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < b)
1214 ==> sum s f < &(CARD s) * b
1215Proof
1216 MESON_TAC[MEMBER_NOT_EMPTY, REAL_LT_IMP_LE, SUM_BOUND_LT]
1217QED
1218
1219Theorem SUM_BOUND_LT_GEN:
1220 !s f b. FINITE s /\ ~(s = {}) /\ (!x:'a. x IN s ==> f(x) < b / &(CARD s))
1221 ==> sum s f < b
1222Proof
1223 MESON_TAC[SUM_BOUND_LT_ALL, REAL_DIV_LMUL, REAL_OF_NUM_EQ, CARD_EQ_0]
1224QED
1225
1226Theorem SUM_UNION_EQ:
1227 !s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
1228 ==> (sum s f + sum t f = sum u f)
1229Proof
1230 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWR_TAC LAND_CONV [EQ_SYM_EQ]
1231 THEN GEN_REWR_TAC RAND_CONV [EQ_SYM_EQ] THEN DISCH_TAC THEN
1232 ONCE_ASM_REWRITE_TAC [] THEN
1233 METIS_TAC[SUM_UNION, DISJOINT_DEF, FINITE_UNION]
1234QED
1235
1236Theorem SUM_EQ_SUPERSET:
1237 !f s t:'a->bool.
1238 FINITE t /\ t SUBSET s /\
1239 (!x. x IN t ==> (f x = g x)) /\
1240 (!x. x IN s /\ ~(x IN t) ==> (f(x) = &0))
1241 ==> (sum s f = sum t g)
1242Proof
1243 MESON_TAC[SUM_SUPERSET, SUM_EQ]
1244QED
1245
1246Theorem SUM_RESTRICT_SET:
1247 !P s f. sum {x | x IN s /\ P x} f = sum s (\x. if P x then f x else (0:real))
1248Proof
1249 ONCE_REWRITE_TAC[GSYM SUM_SUPPORT] THEN
1250 SIMP_TAC std_ss [support, NEUTRAL_REAL_ADD, GSPECIFICATION] THEN
1251 REWRITE_TAC[METIS [] ``~((if P x then f x else a) = a) <=> P x /\ ~(f x = a)``,
1252 GSYM CONJ_ASSOC] THEN
1253 REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_EQ THEN SIMP_TAC std_ss [GSPECIFICATION]
1254QED
1255
1256Theorem SUM_SUM_RESTRICT:
1257 !R f s t.
1258 FINITE s /\ FINITE t
1259 ==> (sum s (\x. sum {y | y IN t /\ R x y} (\y. f x y)) =
1260 sum t (\y. sum {x | x IN s /\ R x y} (\x. f x y)))
1261Proof
1262 REPEAT GEN_TAC THEN SIMP_TAC std_ss [SUM_RESTRICT_SET] THEN ASSUME_TAC SUM_SWAP
1263 THEN POP_ASSUM (MP_TAC o Q.SPECL [`(\x y. if R x y then f x y else 0)`,
1264 `s`, `t`]) THEN FULL_SIMP_TAC std_ss []
1265QED
1266
1267Theorem CARD_EQ_SUM:
1268 !s. FINITE s ==> (&(CARD s) = sum s (\x. (1:real)))
1269Proof
1270 SIMP_TAC std_ss [SUM_CONST, REAL_MUL_RID]
1271QED
1272
1273Theorem SUM_MULTICOUNT_GEN:
1274 !R:'a->'b->bool s t k.
1275 FINITE s /\ FINITE t /\
1276 (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k(j)))
1277 ==> (sum s (\i. &(CARD {j | j IN t /\ R i j})) =
1278 sum t (\i. &(k i)))
1279Proof
1280 REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
1281 DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
1282 MATCH_MP_TAC EQ_TRANS THEN
1283 EXISTS_TAC ``sum s (\i:'a. sum {j:'b | j IN t /\ R i j} (\j. (1:real)))`` THEN
1284 CONJ_TAC THENL
1285 [MATCH_MP_TAC SUM_EQ THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1286 ASM_SIMP_TAC std_ss [CARD_EQ_SUM, FINITE_RESTRICT],
1287 ASSUME_TAC SUM_SUM_RESTRICT THEN POP_ASSUM (MP_TAC o Q.SPEC `R`)
1288 THEN FULL_SIMP_TAC std_ss [] THEN DISCH_TAC THEN MATCH_MP_TAC SUM_EQ
1289 THEN ASM_SIMP_TAC std_ss [SUM_CONST, FINITE_RESTRICT] THEN
1290 REWRITE_TAC[REAL_MUL_RID]]
1291QED
1292
1293Theorem SUM_MULTICOUNT:
1294 !R:'a->'b->bool s t k.
1295 FINITE s /\ FINITE t /\
1296 (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k))
1297 ==> (sum s (\i. &(CARD {j | j IN t /\ R i j})) = &(k * CARD t))
1298Proof
1299 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1300 EXISTS_TAC ``sum t (\i:'b. &k)`` THEN CONJ_TAC THENL
1301 [KNOW_TAC ``?j. !i:'b. &k = &(j i):real`` THENL
1302 [EXISTS_TAC ``(\i:'b. k:num)`` THEN METIS_TAC [], ALL_TAC] THEN
1303 STRIP_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC SUM_MULTICOUNT_GEN
1304 THEN FULL_SIMP_TAC std_ss [REAL_OF_NUM_EQ],
1305 ASM_SIMP_TAC std_ss [SUM_CONST, REAL_OF_NUM_MUL] THEN METIS_TAC[MULT_SYM, MULT_ASSOC]]
1306QED
1307
1308Theorem SUM_IMAGE_GEN:
1309 !f:'a->'b g s.
1310 FINITE s
1311 ==> (sum s g =
1312 sum (IMAGE f s) (\y. sum {x | x IN s /\ (f(x) = y)} g))
1313Proof
1314 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1315 ``sum s (\x:'a. sum {y:'b | y IN IMAGE f s /\ (f x = y)} (\y. g x))`` THEN
1316 CONJ_TAC THENL
1317 [MATCH_MP_TAC SUM_EQ THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC ``x:'a`` THEN
1318 DISCH_TAC THEN BETA_TAC THEN
1319 SUBGOAL_THEN ``{y | y IN IMAGE (f:'a->'b) s /\ (f x = y)} = {(f x)}``
1320 (fn th => REWRITE_TAC[th, SUM_SING, o_THM]) THEN
1321 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_SING, IN_IMAGE] THEN
1322 ASM_MESON_TAC[], GEN_REWR_TAC (funpow 2 RAND_CONV o ABS_CONV o RAND_CONV)
1323 [GSYM ETA_AX] THEN KNOW_TAC ``FINITE (IMAGE (f:'a->'b) s)`` THENL
1324 [METIS_TAC [IMAGE_FINITE], ALL_TAC] THEN DISCH_TAC THEN
1325 ASSUME_TAC SUM_SUM_RESTRICT THEN
1326 POP_ASSUM (MP_TAC o Q.SPEC `(\x y. f x = y)`) THEN
1327 FULL_SIMP_TAC std_ss []]
1328QED
1329
1330(* cf. realTheory.SUM_GROUP *)
1331Theorem SUM_GROUP' : (* was: SUM_GROUP *)
1332 !f:'a->'b g s t.
1333 FINITE s /\ (IMAGE f s) SUBSET t
1334 ==> (sum t (\y. sum {x | x IN s /\ (f(x) = y)} g) = sum s g)
1335Proof
1336 REPEAT STRIP_TAC THEN
1337 MP_TAC(ISPECL [``f:'a->'b``, ``g:'a->real``, ``s:'a->bool``] SUM_IMAGE_GEN) THEN
1338 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
1339 MATCH_MP_TAC SUM_SUPERSET THEN ASM_REWRITE_TAC[] THEN
1340 REPEAT STRIP_TAC THEN BETA_TAC THEN MATCH_MP_TAC SUM_EQ_0 THEN
1341 FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_IMAGE] THEN METIS_TAC []
1342QED
1343
1344Theorem REAL_OF_NUM_SUM:
1345 !f s. FINITE s ==> (&(nsum s f) = sum s (\x. &(f x)))
1346Proof
1347 GEN_TAC THEN GEN_TAC THEN
1348 KNOW_TAC ``((&nsum s f = sum s (\x. &f x))) =
1349 (\s. (&nsum s f = sum s (\x. &f x))) s`` THENL
1350 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
1351 ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC FINITE_INDUCT THEN
1352 BETA_TAC THEN SIMP_TAC std_ss[SUM_CLAUSES, NSUM_CLAUSES, GSYM REAL_OF_NUM_ADD]
1353QED
1354
1355Theorem SUM_SUBSET:
1356 !u v f. FINITE u /\ FINITE v /\
1357 (!x. x IN (u DIFF v) ==> f(x) <= &0) /\
1358 (!x:'a. x IN (v DIFF u) ==> &0 <= f(x))
1359 ==> sum u f <= sum v f
1360Proof
1361 REPEAT STRIP_TAC THEN
1362 MP_TAC(ISPECL [``f:'a->real``, ``u INTER v :'a->bool``] SUM_UNION) THEN
1363 DISCH_THEN(fn th => MP_TAC(SPEC ``v DIFF u :'a->bool`` th) THEN
1364 MP_TAC(SPEC ``u DIFF v :'a->bool`` th)) THEN
1365 REWRITE_TAC[SET_RULE ``(u INTER v) UNION (u DIFF v) = u``,
1366 SET_RULE ``(u INTER v) UNION (v DIFF u) = v``] THEN
1367 ASM_SIMP_TAC std_ss [FINITE_DIFF, FINITE_INTER] THEN
1368 KNOW_TAC ``DISJOINT (u INTER v) (u DIFF v) /\ DISJOINT (u INTER v) (v DIFF u)``
1369 THENL [SET_TAC[], ALL_TAC] THEN RW_TAC std_ss [] THEN
1370 MATCH_MP_TAC(REAL_ARITH ``(0:real) <= -x /\ (0:real) <= y ==> a + x <= a + y``) THEN
1371 ASM_SIMP_TAC std_ss [GSYM SUM_NEG, FINITE_DIFF] THEN CONJ_TAC THEN
1372 MATCH_MP_TAC SUM_POS_LE THEN
1373 ASM_SIMP_TAC std_ss [FINITE_DIFF, REAL_LE_RNEG, REAL_ADD_LID]
1374QED
1375
1376Theorem SUM_SUBSET_SIMPLE:
1377 !u v f. FINITE v /\ u SUBSET v /\ (!x:'a. x IN (v DIFF u) ==> (0:real) <= f(x))
1378 ==> sum u f <= sum v f
1379Proof
1380 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_SUBSET THEN
1381 ASM_MESON_TAC[IN_DIFF, SUBSET_DEF, SUBSET_FINITE]
1382QED
1383
1384Theorem SUM_IMAGE_NONZERO:
1385 !d:'b->real i:'a->'b s.
1386 FINITE s /\
1387 (!x y. x IN s /\ y IN s /\ ~(x = y) /\ (i x = i y) ==> (d(i x) = (0:real)))
1388 ==> (sum (IMAGE i s) d = sum s (d o i))
1389Proof
1390 REWRITE_TAC[GSYM NEUTRAL_REAL_ADD, sum_def] THEN
1391 MATCH_MP_TAC ITERATE_IMAGE_NONZERO THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
1392QED
1393
1394Theorem SUM_BIJECTION:
1395 !f p s:'a->bool.
1396 (!x. x IN s ==> p(x) IN s) /\
1397 (!y. y IN s ==> ?!x. x IN s /\ (p(x) = y))
1398 ==> (sum s f = sum s (f o p))
1399Proof
1400 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_BIJECTION THEN
1401 REWRITE_TAC[MONOIDAL_REAL_ADD]
1402QED
1403
1404Theorem SUM_SUM_PRODUCT:
1405 !s:'a->bool t:'a->'b->bool x.
1406 FINITE s /\ (!i. i IN s ==> FINITE(t i))
1407 ==> (sum s (\i. sum (t i) (x i)) =
1408 sum {i,j | i IN s /\ j IN t i} (\(i,j). x i j))
1409Proof
1410 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
1411 REWRITE_TAC[MONOIDAL_REAL_ADD]
1412QED
1413
1414Theorem SUM_EQ_GENERAL:
1415 !s:'a->bool t:'b->bool f g h.
1416 (!y. y IN t ==> ?!x. x IN s /\ (h(x) = y)) /\
1417 (!x. x IN s ==> h(x) IN t /\ (g(h x) = f x))
1418 ==> (sum s f = sum t g)
1419Proof
1420 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL THEN
1421 REWRITE_TAC[MONOIDAL_REAL_ADD]
1422QED
1423
1424Theorem SUM_EQ_GENERAL_INVERSES:
1425 !s:'a->bool t:'b->bool f g h k.
1426 (!y. y IN t ==> k(y) IN s /\ (h(k y) = y)) /\
1427 (!x. x IN s ==> h(x) IN t /\ (k(h x) = x) /\ (g(h x) = f x))
1428 ==> (sum s f = sum t g)
1429Proof
1430 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL_INVERSES THEN
1431 REWRITE_TAC[MONOIDAL_REAL_ADD]
1432QED
1433
1434Theorem SUM_INJECTION:
1435 !f p s. FINITE s /\
1436 (!x. x IN s ==> p x IN s) /\
1437 (!x y. x IN s /\ y IN s /\ (p x = p y) ==> (x = y))
1438 ==> (sum s (f o p) = sum s f)
1439Proof
1440 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_INJECTION THEN
1441 REWRITE_TAC[MONOIDAL_REAL_ADD]
1442QED
1443
1444Theorem SUM_UNION_NONZERO:
1445 !f s t. FINITE s /\ FINITE t /\ (!x. x IN s INTER t ==> (f(x) = (0:real)))
1446 ==> (sum (s UNION t) f = sum s f + sum t f)
1447Proof
1448 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
1449 MATCH_MP_TAC ITERATE_UNION_NONZERO THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
1450QED
1451
1452Theorem SUM_BIGUNION_NONZERO:
1453 !f s. FINITE s /\ (!t:'a->bool. t IN s ==> FINITE t) /\
1454 (!t1 t2 x. t1 IN s /\ t2 IN s /\ ~(t1 = t2) /\ x IN t1 /\ x IN t2
1455 ==> (f x = (0:real)))
1456 ==> (sum (BIGUNION s) f = sum s (\t. sum t f))
1457Proof
1458 GEN_TAC THEN ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC
1459 THEN KNOW_TAC ``( (!(t:'a->bool). t IN s ==> FINITE t) /\
1460 (!t1 t2 x. t1 IN s /\ t2 IN s /\ t1 <> t2 /\ x IN t1 /\ x IN t2 ==>
1461 (f x = 0)) ==> (sum (BIGUNION s) f = sum s (\t. sum t f))) =
1462 (\s. (!t. t IN s ==> FINITE t) /\
1463 (!t1 t2 x. t1 IN s /\ t2 IN s /\ t1 <> t2 /\ x IN t1 /\ x IN t2 ==>
1464 (f x = 0)) ==> (sum (BIGUNION s) f = sum s (\t. sum t f))) s`` THENL
1465 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1466 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1467 REWRITE_TAC[BIGUNION_EMPTY, BIGUNION_INSERT, SUM_CLAUSES, IN_INSERT] THEN
1468 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
1469 MAP_EVERY X_GEN_TAC [``(s':('a->bool)->bool)``, ``t:'a->bool``] THEN
1470 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN REPEAT STRIP_TAC THEN
1471 UNDISCH_TAC ``FINITE (s':('a->bool)->bool)`` THEN
1472 UNDISCH_TAC ``(t :'a -> bool) NOTIN (s' :('a -> bool) -> bool) `` THEN
1473 ONCE_REWRITE_TAC[AND_IMP_INTRO] THEN ASM_SIMP_TAC std_ss [SUM_CLAUSES]
1474 THEN KNOW_TAC ``sum (BIGUNION s') f = sum s' (\t. sum t f)`` THENL
1475 [METIS_TAC [], ALL_TAC] THEN GEN_REWR_TAC (LAND_CONV) [EQ_SYM_EQ]
1476 THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1477 STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_NONZERO THEN
1478 ASM_SIMP_TAC std_ss [FINITE_BIGUNION, IN_INTER, IN_BIGUNION] THEN
1479 ASM_MESON_TAC[]
1480QED
1481
1482Theorem SUM_CASES:
1483 !s P f g. FINITE s
1484 ==> (sum s (\x:'a. if P x then f x else g x) =
1485 sum {x | x IN s /\ P x} f + sum {x | x IN s /\ ~P x} g)
1486Proof
1487 REWRITE_TAC[sum_def, GSYM NEUTRAL_REAL_ADD] THEN
1488 MATCH_MP_TAC ITERATE_CASES THEN REWRITE_TAC[MONOIDAL_REAL_ADD]
1489QED
1490
1491Theorem SUM_CASES_1:
1492 !s a. FINITE s /\ a IN s
1493 ==> (sum s (\x. if x = a then y else f(x)) = sum s f + (y - f a))
1494Proof
1495 REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [SUM_CASES] THEN
1496 KNOW_TAC ``{x | x IN s /\ x <> a} = s DELETE a`` THENL
1497 [FULL_SIMP_TAC std_ss [DELETE_DEF, DIFF_DEF, IN_SING], ALL_TAC] THEN DISCH_TAC
1498 THEN ASM_SIMP_TAC std_ss [SUM_DELETE] THEN
1499 ASM_SIMP_TAC std_ss [SET_RULE ``a IN s ==> ({x | x IN s /\ (x = a)} = {a})``] THEN
1500 REWRITE_TAC[SUM_SING] THEN REAL_ARITH_TAC
1501QED
1502
1503Theorem SUM_LE_INCLUDED:
1504 !f:'a->real g:'b->real s t i.
1505 FINITE s /\ FINITE t /\
1506 (!y. y IN t ==> (0:real) <= g y) /\
1507 (!x. x IN s ==> ?y. y IN t /\ (i y = x) /\ f(x) <= g(y))
1508 ==> sum s f <= sum t g
1509Proof
1510 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1511 EXISTS_TAC ``sum (IMAGE (i:'b->'a) t) (\y. sum {x | x IN t /\ (i x = y)} g)`` THEN
1512 CONJ_TAC THENL
1513 [ALL_TAC,
1514 MATCH_MP_TAC REAL_EQ_IMP_LE THEN
1515 MATCH_MP_TAC(GSYM SUM_IMAGE_GEN) THEN ASM_REWRITE_TAC[]] THEN
1516 MATCH_MP_TAC REAL_LE_TRANS THEN
1517 EXISTS_TAC ``sum s (\y. sum {x | x IN t /\ ((i:'b->'a) x = y)} g)`` THEN
1518 CONJ_TAC THENL
1519 [MATCH_MP_TAC SUM_LE THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC ``x:'a`` THEN
1520 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC ``x:'a``) THEN
1521 ASM_SIMP_TAC std_ss [PULL_EXISTS] THEN X_GEN_TAC ``y:'b`` THEN
1522 STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1523 EXISTS_TAC ``sum {y:'b} g`` THEN CONJ_TAC THENL
1524 [ASM_REWRITE_TAC[SUM_SING], ALL_TAC],
1525 ALL_TAC] THEN
1526 MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN ASM_SIMP_TAC std_ss [IMAGE_FINITE] THEN
1527 ASM_SIMP_TAC std_ss [SUM_POS_LE, FINITE_RESTRICT, GSPECIFICATION] THEN
1528 FULL_SIMP_TAC std_ss [SUBSET_DEF, DIFF_DEF, IN_SING, IN_IMAGE, GSPECIFICATION]
1529 THEN METIS_TAC []
1530QED
1531
1532Theorem SUM_IMAGE_LE:
1533 !f:'a->'b g s.
1534 FINITE s /\
1535 (!x. x IN s ==> (0:real) <= g(f x))
1536 ==> sum (IMAGE f s) g <= sum s (g o f)
1537Proof
1538 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_LE_INCLUDED THEN
1539 ASM_SIMP_TAC std_ss [IMAGE_FINITE,
1540 SET_RULE ``!f s. (!y. y IN IMAGE f s ==> P y) <=> (!x. x IN s ==> P(f x))``] THEN
1541 ASM_REWRITE_TAC[o_THM] THEN EXISTS_TAC ``f:'a->'b`` THEN
1542 MESON_TAC[REAL_LE_REFL]
1543QED
1544
1545Theorem SUM_CLOSED:
1546 !P f:'a->real s.
1547 P(0:real) /\ (!x y. P x /\ P y ==> P(x + y)) /\ (!a. a IN s ==> P(f a))
1548 ==> P(sum s f)
1549Proof
1550 REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_REAL_ADD) THEN
1551 DISCH_THEN(MP_TAC o SPEC ``P:real->bool``) THEN
1552 ASM_SIMP_TAC std_ss [NEUTRAL_REAL_ADD, GSYM sum_def]
1553QED
1554
1555Theorem REAL_OF_NUM_SUM_NUMSEG:
1556 !f m n. (&(nsum{m..n} f) = sum {m..n} (\i. &(f i)))
1557Proof
1558 SIMP_TAC std_ss [REAL_OF_NUM_SUM, FINITE_NUMSEG]
1559QED
1560
1561(* ------------------------------------------------------------------------- *)
1562(* Specialize them to sums over intervals of numbers. *)
1563(* ------------------------------------------------------------------------- *)
1564
1565Theorem SUM_ADD_NUMSEG:
1566 !f g m n. sum{m..n} (\i. f(i) + g(i)) = sum{m..n} f + sum{m..n} g
1567Proof
1568 SIMP_TAC std_ss [SUM_ADD, FINITE_NUMSEG]
1569QED
1570
1571Theorem SUM_SUB_NUMSEG:
1572 !f g m n. sum{m..n} (\i. f(i) - g(i)) = sum{m..n} f - sum{m..n} g
1573Proof
1574 SIMP_TAC std_ss [SUM_SUB, FINITE_NUMSEG]
1575QED
1576
1577Theorem SUM_LE_NUMSEG:
1578 !f g m n. (!i. m <= i /\ i <= n ==> f(i) <= g(i))
1579 ==> sum{m..n} f <= sum{m..n} g
1580Proof
1581 SIMP_TAC std_ss [SUM_LE, FINITE_NUMSEG, IN_NUMSEG]
1582QED
1583
1584Theorem SUM_EQ_NUMSEG:
1585 !f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
1586 ==> (sum{m..n} f = sum{m..n} g)
1587Proof
1588 MESON_TAC[SUM_EQ, FINITE_NUMSEG, IN_NUMSEG]
1589QED
1590
1591Theorem SUM_ABS_NUMSEG:
1592 !f m n. abs(sum{m..n} f) <= sum{m..n} (\i. abs(f i))
1593Proof
1594 SIMP_TAC std_ss [SUM_ABS, FINITE_NUMSEG]
1595QED
1596
1597Theorem SUM_CONST_NUMSEG:
1598 !c m n. sum{m..n} (\n. c) = &((n + 1) - m) * c
1599Proof
1600 SIMP_TAC std_ss [SUM_CONST, FINITE_NUMSEG, CARD_NUMSEG]
1601QED
1602
1603Theorem SUM_EQ_0_NUMSEG:
1604 !f m n. (!i. m <= i /\ i <= n ==> (f(i) = &0)) ==> (sum{m..n} f = &0)
1605Proof
1606 SIMP_TAC std_ss [SUM_EQ_0, IN_NUMSEG]
1607QED
1608
1609Theorem SUM_TRIV_NUMSEG:
1610 !f m n. n < m ==> (sum{m..n} f = &0)
1611Proof
1612 MESON_TAC[SUM_EQ_0_NUMSEG, LESS_EQ_TRANS, NOT_LESS]
1613QED
1614
1615Theorem SUM_POS_LE_NUMSEG:
1616 !m n f. (!p. m <= p /\ p <= n ==> &0 <= f(p)) ==> &0 <= sum{m..n} f
1617Proof
1618 SIMP_TAC std_ss [SUM_POS_LE, FINITE_NUMSEG, IN_NUMSEG]
1619QED
1620
1621Theorem SUM_POS_EQ_0_NUMSEG:
1622 !f m n. (!p. m <= p /\ p <= n ==> &0 <= f(p)) /\ (sum{m..n} f = &0)
1623 ==> !p. m <= p /\ p <= n ==> (f(p) = &0)
1624Proof
1625 MESON_TAC[SUM_POS_EQ_0, FINITE_NUMSEG, IN_NUMSEG]
1626QED
1627
1628Theorem SUM_SING_NUMSEG:
1629 !f n. sum{n..n} f = f(n)
1630Proof
1631 SIMP_TAC std_ss [SUM_SING, NUMSEG_SING]
1632QED
1633
1634Theorem SUM_CLAUSES_NUMSEG:
1635 (!m. sum{m..0} f = if m = 0 then f(0) else &0) /\
1636 (!m n. sum{m..SUC n} f = if m <= SUC n then sum{m..n} f + f(SUC n)
1637 else sum{m..n} f)
1638Proof
1639 MP_TAC(MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_REAL_ADD) THEN
1640 REWRITE_TAC[NEUTRAL_REAL_ADD, sum_def]
1641QED
1642
1643Theorem SUM_SWAP_NUMSEG:
1644 !a b c d f.
1645 sum{a..b} (\i. sum{c..d} (f i)) = sum{c..d} (\j. sum{a..b} (\i. f i j))
1646Proof
1647 REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_SWAP THEN
1648 REWRITE_TAC[FINITE_NUMSEG]
1649QED
1650
1651Theorem SUM_ADD_SPLIT:
1652 !f m n p.
1653 m <= n + 1:num ==> ((sum {m..n+p} f = sum{m..n} f + sum{n+1..n+p} f))
1654Proof
1655 REPEAT STRIP_TAC THEN ASSUME_TAC NUMSEG_ADD_SPLIT THEN
1656 POP_ASSUM (MP_TAC o Q.SPECL [`m`,`n`,`p`]) THEN DISCH_TAC THEN
1657 ASM_SIMP_TAC std_ss [SUM_UNION, DISJOINT_NUMSEG, FINITE_NUMSEG,
1658 ARITH_PROVE ``x < x + 1:num``]
1659QED
1660
1661(* cf. realTheory.SUM_OFFSET *)
1662Theorem SUM_OFFSET' : (* was: SUM_OFFSET *)
1663 !p f m n. sum{m+p..n+p} f = sum{m..n} (\i. f(i + p))
1664Proof
1665 SIMP_TAC std_ss [NUMSEG_OFFSET_IMAGE, SUM_IMAGE,
1666 EQ_ADD_RCANCEL, FINITE_NUMSEG] THEN
1667 RW_TAC std_ss [o_DEF]
1668QED
1669Theorem SUM_OFFSET[local] = SUM_OFFSET'
1670
1671Theorem SUM_OFFSET_0:
1672 !f m n. m <= n ==> (sum{m..n} f = sum{0..n-m} (\i. f(i + m)))
1673Proof
1674 SIMP_TAC std_ss [GSYM SUM_OFFSET, ADD_CLAUSES, SUB_ADD]
1675QED
1676
1677Theorem SUM_CLAUSES_LEFT:
1678 !f m n. m <= n:num ==> (sum{m..n} f = f(m) + sum{m+1..n} f)
1679Proof
1680 RW_TAC arith_ss [GSYM NUMSEG_LREC, SUM_CLAUSES, FINITE_NUMSEG, IN_NUMSEG]
1681QED
1682
1683Theorem SUM_CLAUSES_RIGHT:
1684 !f m n. 0:num < n /\ m <= n ==> (sum{m..n} f = sum{m..n-1} f + f(n))
1685Proof
1686 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1687 SIMP_TAC std_ss [LESS_REFL, SUM_CLAUSES_NUMSEG, SUC_SUB1]
1688QED
1689
1690Theorem SUM_PAIR:
1691 !f m n. sum{2*m..2*n+1} f = sum{m..n} (\i. f(2*i) + f(2*i+1))
1692Proof
1693 MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_REAL_ADD) THEN
1694 REWRITE_TAC[sum_def, NEUTRAL_REAL_ADD]
1695QED
1696
1697(* connection to realTheory.sum *)
1698Theorem sum_real :
1699 !f n. sum{0..n} f = real$sum(0,SUC n) f
1700Proof
1701 GEN_TAC
1702 >> Induct_on `n`
1703 >- (SIMP_TAC real_ss [sum, SUM_CLAUSES_RIGHT, SUM_SING_NUMSEG])
1704 >> ASM_SIMP_TAC real_ss [sum, SUM_CLAUSES_RIGHT]
1705QED
1706
1707(* ------------------------------------------------------------------------- *)
1708(* Partial summation and other theorems specific to number segments. *)
1709(* ------------------------------------------------------------------------- *)
1710
1711Theorem SUM_PARTIAL_SUC:
1712 !f g m n.
1713 sum {m..n} (\k. f(k) * (g(k + 1) - g(k))) =
1714 if m <= n then f(n + 1) * g(n + 1) - f(m) * g(m) -
1715 sum {m..n} (\k. g(k + 1) * (f(k + 1) - f(k)))
1716 else &0
1717Proof
1718 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1719 COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [SUM_TRIV_NUMSEG, GSYM NOT_LESS_EQUAL] THEN
1720 ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG] THENL
1721 [COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [] THENL [REAL_ARITH_TAC, FULL_SIMP_TAC std_ss []],
1722 ALL_TAC] THEN
1723 FULL_SIMP_TAC std_ss [LE] THEN
1724 ASM_SIMP_TAC std_ss [GSYM NOT_LESS, SUM_TRIV_NUMSEG, ARITH_PROVE ``n < SUC n``] THEN
1725 ASM_SIMP_TAC std_ss [GSYM ADD1, ADD_CLAUSES] THEN REAL_ARITH_TAC
1726QED
1727
1728Theorem SUM_PARTIAL_PRE:
1729 !f g m n.
1730 sum {m..n} (\k. f(k) * (g(k) - g(k - 1))) =
1731 if m <= n then f(n + 1) * g(n) - f(m) * g(m - 1) -
1732 sum {m..n} (\k. g k * (f(k + 1) - f(k)))
1733 else &0
1734Proof
1735 REPEAT GEN_TAC THEN
1736 MP_TAC(ISPECL [``f:num->real``, ``\k. (g:num->real)(k - 1)``,
1737 ``m:num``, ``n:num``] SUM_PARTIAL_SUC) THEN
1738 BETA_TAC THEN REWRITE_TAC[ADD_SUB]
1739QED
1740
1741(* cf. realTheory.SUM_DIFFS *)
1742Theorem SUM_DIFFS' : (* was: SUM_DIFFS *)
1743 !m n. sum{m..n} (\k. f(k) - f(k + 1)) =
1744 if m <= n then f(m) - f(n + 1) else (0:real)
1745Proof
1746 ONCE_REWRITE_TAC[REAL_ARITH ``a - b = - (1:real) * (b - a)``] THEN
1747 KNOW_TAC ``?(g:num->real). !k. -1 = g k`` THENL [EXISTS_TAC ``(\k:num. -(1:real))``
1748 THEN SIMP_TAC std_ss [], ALL_TAC] THEN STRIP_TAC THEN ONCE_ASM_REWRITE_TAC []
1749 THEN ONCE_REWRITE_TAC[SUM_PARTIAL_SUC] THEN FULL_SIMP_TAC std_ss [EQ_SYM_EQ]
1750 THEN RW_TAC arith_ss [REAL_SUB_REFL, REAL_MUL_RZERO, SUM_0] THEN
1751 REAL_ARITH_TAC
1752QED
1753val SUM_DIFFS = SUM_DIFFS';
1754
1755Theorem SUM_DIFFS_ALT:
1756 !m n. sum{m..n} (\k. f(k + 1) - f(k)) =
1757 if m <= n then f(n + 1) - f(m) else &0
1758Proof
1759 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN
1760 SIMP_TAC std_ss [SUM_NEG, SUM_DIFFS] THEN
1761 COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_NEG_SUB, REAL_NEG_0]
1762QED
1763
1764Theorem SUM_COMBINE_R:
1765 !f m n p. m <= n + 1 /\ n <= p
1766 ==> (sum{m..n} f + sum{n+1..p} f = sum{m..p} f)
1767Proof
1768 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_EQ THEN
1769 REWRITE_TAC[FINITE_NUMSEG, EXTENSION, IN_INTER, IN_UNION, NOT_IN_EMPTY,
1770 IN_NUMSEG] THEN RW_TAC arith_ss []
1771QED
1772
1773Theorem SUM_COMBINE_L:
1774 !f m n p. 0 < n /\ m <= n /\ n <= p + 1
1775 ==> (sum{m..n-1} f + sum{n..p} f = sum{m..p} f)
1776Proof
1777 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_EQ THEN
1778 REWRITE_TAC[FINITE_NUMSEG, EXTENSION, IN_INTER, IN_UNION, NOT_IN_EMPTY,
1779 IN_NUMSEG] THEN RW_TAC arith_ss []
1780QED
1781
1782Theorem SUM_GP_BASIC:
1783 !x:real n:num. (&1 - x) * sum{0..n} (\i. x pow i) = &1 - x pow (SUC n)
1784Proof
1785 GEN_TAC THEN INDUCT_TAC THEN SIMP_TAC std_ss [SUM_CLAUSES_NUMSEG] THEN
1786 SIMP_TAC std_ss [pow, REAL_MUL_RID, ZERO_LESS_EQ, POW_1] THEN
1787 ASM_REWRITE_TAC[REAL_ADD_LDISTRIB, pow] THEN REAL_ARITH_TAC
1788QED
1789
1790Theorem SUM_GP_MULTIPLIED:
1791 !x m n. m <= n
1792 ==> ((&1 - x) * sum{m..n} (\i. x pow i) = x pow m - x pow (SUC n))
1793Proof
1794 REPEAT STRIP_TAC THEN
1795 Q_TAC KNOW_TAC
1796 ‘(1 - x) * sum {0 .. n - m} (\i. (\i. x pow i) (i + m)) =
1797 x pow m - x pow SUC n’ THENL [ALL_TAC, METIS_TAC [SUM_OFFSET_0]] THEN
1798 ASM_SIMP_TAC std_ss
1799 [REAL_POW_ADD, REAL_MUL_ASSOC, SUM_GP_BASIC, SUM_RMUL] THEN
1800 SIMP_TAC std_ss [REAL_SUB_RDISTRIB, GSYM REAL_POW_ADD, REAL_MUL_LID] THEN
1801 ASM_SIMP_TAC std_ss [ARITH_PROVE ``m <= n ==> (SUC(n - m) + m = SUC n)``]
1802QED
1803
1804Theorem SUM_GP:
1805 !x m n.
1806 sum{m..n} (\i. x pow i) =
1807 if n < m then &0
1808 else if x = &1 then &((n + 1) - m)
1809 else (x pow m - x pow (SUC n)) / (&1 - x)
1810Proof
1811 REPEAT GEN_TAC THEN
1812 DISJ_CASES_TAC(ARITH_PROVE ``n < m \/ ~(n < m) /\ m <= n:num``) THEN
1813 ASM_SIMP_TAC std_ss [SUM_TRIV_NUMSEG] THEN COND_CASES_TAC THENL
1814 [ASM_REWRITE_TAC[POW_ONE, SUM_CONST_NUMSEG, REAL_MUL_RID], ALL_TAC] THEN
1815 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN EXISTS_TAC ``&1 - x:real`` THEN
1816 ASM_SIMP_TAC std_ss [REAL_DIV_LMUL, REAL_SUB_0, SUM_GP_MULTIPLIED]
1817QED
1818
1819Theorem SUMS_SYM:
1820 !s t:real->bool. {x + y | x IN s /\ y IN t} = {y + x | y IN t /\ x IN s}
1821Proof
1822 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN
1823 MESON_TAC[REAL_ADD_SYM]
1824QED
1825
1826Theorem SUM_ABS_TRIANGLE:
1827 !s f b. FINITE s /\ sum s (\a. abs(f a)) <= b ==> abs(sum s f) <= b
1828Proof
1829 METIS_TAC[SUM_ABS, REAL_LE_TRANS]
1830QED
1831
1832Theorem REAL_MUL_SUM :
1833 !s t f g.
1834 FINITE s /\ FINITE t
1835 ==> sum s f * sum t g = sum s (\i. sum t (\j. f(i) * g(j)))
1836Proof
1837 rpt STRIP_TAC
1838 >> SIMP_TAC std_ss [SUM_LMUL]
1839 >> ONCE_REWRITE_TAC[REAL_MUL_SYM]
1840 >> SIMP_TAC std_ss [SUM_LMUL]
1841QED
1842
1843Theorem REAL_MUL_SUM_NUMSEG :
1844 !f g m n p q. sum{m..n} f * sum{p..q} g =
1845 sum{m..n} (\i. sum{p..q} (\j. f(i) * g(j)))
1846Proof
1847 rpt STRIP_TAC
1848 >> SIMP_TAC std_ss [REAL_MUL_SUM, FINITE_NUMSEG]
1849QED
1850
1851(* ------------------------------------------------------------------------- *)
1852(* Extend congruences to deal with sum. Note that we must have the eta *)
1853(* redex or we'll get a loop since f(x) will lambda-reduce recursively. *)
1854(* ------------------------------------------------------------------------- *)
1855
1856Theorem SUM_CONG:
1857 (!f g s. (!x. x IN s ==> (f(x) = g(x)))
1858 ==> (sum s (\i. f(i)) = sum s g)) /\
1859 (!f g a b. (!i. a <= i /\ i <= b ==> (f(i) = g(i)))
1860 ==> (sum{a..b} (\i. f(i)) = sum{a..b} g)) /\
1861 (!f g p. (!x. p x ==> (f x = g x))
1862 ==> (sum {y | p y} (\i. f(i)) = sum {y | p y} g))
1863Proof
1864 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_EQ THEN
1865 ASM_SIMP_TAC std_ss [GSPECIFICATION, IN_NUMSEG]
1866QED
1867
1868(* ------------------------------------------------------------------------- *)
1869(* Some special algebraic rearrangements. *)
1870(* ------------------------------------------------------------------------- *)
1871
1872Theorem REAL_SUB_POW:
1873 !x y n.
1874 1 <= n ==> (x pow n - y pow n =
1875 (x - y) * sum{0n..n-1} (\i. x pow i * y pow (n - 1 - i)))
1876Proof
1877 SIMP_TAC std_ss [GSYM SUM_LMUL] THEN
1878 REWRITE_TAC[REAL_ARITH
1879 ``(x - y) * (a * b):real = (x * a) * b - a * (y * b)``] THEN
1880 SIMP_TAC std_ss [GSYM pow, ADD1, ARITH_PROVE
1881 ``1 <= n /\ x <= n - 1 ==> (n - 1 - x = n - (x + 1)) /\
1882 (SUC(n - 1 - x) = n - x)``] THEN REPEAT STRIP_TAC THEN
1883 Q_TAC KNOW_TAC
1884 ‘(sum {0n .. n - 1}
1885 (\i. x pow (i + 1) * y pow (n - 1 - i) -
1886 x pow i * y pow (n - 1 - i + 1n))) =
1887 (sum {0n .. n - 1}
1888 (\i.
1889 x pow (i + 1) * y pow (n - (i + 1)) -
1890 x pow i * y pow (n - i)))’ THENL
1891 [MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC [IN_NUMSEG] THEN
1892 REPEAT STRIP_TAC THEN FULL_SIMP_TAC arith_ss [], DISC_RW_KILL THEN
1893 ASM_SIMP_TAC std_ss [SUM_DIFFS_ALT, ZERO_LESS_EQ, SUB_0, SUB_ADD,
1894 SUB_EQUAL_0, pow, REAL_MUL_LID, REAL_MUL_RID]]
1895QED
1896
1897Theorem REAL_SUB_POW_R1:
1898 !x:real n:num. 1 <= n ==> (x pow n - &1 = (x - &1) * sum{0..n-1} (\i. x pow i))
1899Proof
1900 REPEAT GEN_TAC THEN
1901 DISCH_THEN(MP_TAC o SPECL [``x:real``, ``1:real``] o MATCH_MP REAL_SUB_POW) THEN
1902 REWRITE_TAC[POW_ONE, REAL_MUL_RID]
1903QED
1904
1905Theorem REAL_SUB_POW_L1:
1906 !x:real n:num. 1 <= n ==> (&1 - x pow n = (&1 - x) * sum{0..n-1} (\i. x pow i))
1907Proof
1908 ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN
1909 SIMP_TAC std_ss [REAL_SUB_POW_R1] THEN REWRITE_TAC[REAL_MUL_LNEG]
1910QED
1911
1912(* ------------------------------------------------------------------------- *)
1913(* Some useful facts about real polynomial functions. *)
1914(* ------------------------------------------------------------------------- *)
1915
1916Theorem REAL_SUB_POLYFUN:
1917 !a x y n. 1 <= n
1918 ==> (sum{0..n} (\i. a i * x pow i) -
1919 sum{0..n} (\i. a i * y pow i) = (x - y) *
1920 sum{0..n-1} (\j. sum{j+1..n} (\i. a i * y pow (i - j - 1)) * x pow j))
1921Proof
1922 REPEAT STRIP_TAC THEN
1923 REWRITE_TAC[GSYM SUM_SUB_NUMSEG] THEN BETA_TAC THEN
1924 REWRITE_TAC [GSYM REAL_SUB_LDISTRIB] THEN
1925 GEN_REWR_TAC LAND_CONV [MATCH_MP SUM_CLAUSES_LEFT (SPEC_ALL ZERO_LESS_EQ)] THEN
1926 FULL_SIMP_TAC std_ss [REAL_SUB_REFL, pow, REAL_MUL_RZERO, REAL_ADD_LID] THEN
1927 KNOW_TAC ``sum {1.. n:num} (\i. a i * (x pow i - y pow i)) =
1928 sum {1.. n} (\i. a i * (x - y) *
1929 sum {0.. i - 1} (\i'. x pow i' * y pow (i - 1n - i')))`` THENL
1930 [MATCH_MP_TAC SUM_EQ THEN REPEAT STRIP_TAC THEN BETA_TAC THEN
1931 FULL_SIMP_TAC std_ss [IN_NUMSEG, REAL_SUB_POW] THEN METIS_TAC [REAL_MUL_ASSOC],
1932 ALL_TAC] THEN DISC_RW_KILL THEN
1933 ONCE_REWRITE_TAC[REAL_ARITH ``a * x * s:real = x * a * s``] THEN
1934 SIMP_TAC std_ss [SUM_LMUL, GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
1935 SIMP_TAC std_ss [GSYM SUM_LMUL, GSYM SUM_RMUL, SUM_SUM_PRODUCT, FINITE_NUMSEG] THEN
1936 MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
1937 REPEAT(EXISTS_TAC ``\(x:num,y:num). (y,x)``) THEN
1938 REWRITE_TAC[FORALL_IN_GSPEC, IN_ELIM_PAIR_THM, IN_NUMSEG] THEN
1939 SRW_TAC [][] THENL [RW_TAC arith_ss [REAL_MUL_ASSOC],RW_TAC arith_ss [REAL_MUL_ASSOC],
1940 RW_TAC arith_ss [REAL_MUL_ASSOC],RW_TAC arith_ss [REAL_MUL_ASSOC],
1941 RW_TAC arith_ss [REAL_MUL_ASSOC, REAL_MUL_SYM]]
1942QED
1943
1944Theorem REAL_SUB_POLYFUN_ALT:
1945 !a x y n.
1946 1 <= n
1947 ==> (sum{0..n} (\i. a i * x pow i) -
1948 sum{0..n} (\i. a i * y pow i) =
1949 (x - y) * sum{0..n-1} (\j. sum{0..n-j-1}
1950 (\k. a(j+k+1) * y pow k) * x pow j))
1951Proof
1952 REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [REAL_SUB_POLYFUN] THEN AP_TERM_TAC THEN
1953 MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC ``j:num`` THEN REPEAT STRIP_TAC THEN
1954 BETA_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1955 MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
1956 MAP_EVERY EXISTS_TAC
1957 [``\i:num. i - (j + 1)``, ``\k:num. j + k + 1``] THEN
1958 REWRITE_TAC[IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
1959 RW_TAC arith_ss []
1960QED
1961
1962Theorem REAL_POLYFUN_ROOTBOUND:
1963 !n c. ~(!i. i IN {0..n} ==> (c i = 0:real))
1964 ==> FINITE {x | sum{0..n} (\i. c i * x pow i) = 0:real} /\
1965 CARD {x | sum{0..n} (\i. c i * x pow i) = 0:real} <= n
1966Proof
1967 REWRITE_TAC[NOT_FORALL_THM, NOT_IMP] THEN INDUCT_TAC THENL
1968 [REWRITE_TAC[NUMSEG_SING, IN_SING, UNWIND_THM2, SUM_CLAUSES_NUMSEG] THEN
1969 SIMP_TAC std_ss [pow, REAL_MUL_RID, GSPEC_F, CARD_EMPTY, CARD_INSERT,
1970 FINITE_EMPTY, LESS_EQ_REFL],
1971 X_GEN_TAC ``c:num->real`` THEN REWRITE_TAC[IN_NUMSEG] THEN
1972 DISCH_TAC THEN ASM_CASES_TAC ``(c:num->real) (SUC n) = 0:real`` THENL
1973 [ASM_SIMP_TAC std_ss [SUM_CLAUSES_NUMSEG, ZERO_LESS_EQ, REAL_MUL_LZERO, REAL_ADD_RID] THEN
1974 REWRITE_TAC[LE, LEFT_AND_OVER_OR] THEN DISJ2_TAC THEN
1975 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IN_NUMSEG, LE],
1976 ASM_CASES_TAC ``{x | sum {0..SUC n} (\i. c i * x pow i) = 0:real} = {}`` THEN
1977 ASM_REWRITE_TAC[FINITE_EMPTY, FINITE_INSERT, CARD_EMPTY, CARD_INSERT, ZERO_LESS_EQ] THEN
1978 POP_ASSUM MP_TAC THEN GEN_REWR_TAC LAND_CONV [GSYM MEMBER_NOT_EMPTY] THEN
1979 SIMP_TAC std_ss [GSPECIFICATION, PULL_EXISTS] THEN
1980 X_GEN_TAC ``r:real`` THEN DISCH_TAC THEN
1981 MP_TAC(GEN ``x:real`` (ISPECL [``c:num->real``, ``x:real``, ``r:real``, ``SUC n``]
1982 REAL_SUB_POLYFUN)) THEN
1983 ASM_REWRITE_TAC[ARITH_PROVE ``1 <= SUC n``, REAL_SUB_RZERO] THEN
1984 DISCH_THEN(fn th => ASM_REWRITE_TAC [th, REAL_ENTIRE, REAL_SUB_0]) THEN
1985 SIMP_TAC std_ss [SET_RULE ``{x | (x = c) \/ P x} = c INSERT {x | P x}``] THEN
1986 MATCH_MP_TAC(METIS[FINITE_INSERT, CARD_EMPTY, CARD_INSERT,
1987 ARITH_PROVE ``x <= n ==> SUC x <= SUC n /\ x <= SUC n``]
1988 ``FINITE s /\ CARD s <= n
1989 ==> FINITE(r INSERT s) /\ CARD(r INSERT s) <= SUC n``) THEN
1990 KNOW_TAC “?j. j IN {0..n} /\
1991 sum {j + 1..SUC n} (\i. c i * r pow (i - j - 1)) <> 0” THENL
1992 [EXISTS_TAC ``n:num`` THEN REWRITE_TAC[IN_NUMSEG, ADD1, LESS_EQ_REFL, ZERO_LESS_EQ] THEN
1993 SIMP_TAC std_ss [SUM_SING_NUMSEG, ARITH_PROVE ``(n + 1) - n - 1 = 0:num``] THEN
1994 ASM_SIMP_TAC std_ss [GSYM ADD1, pow, REAL_MUL_RID], SRW_TAC [][]]]]
1995QED
1996
1997Theorem REAL_POLYFUN_FINITE_ROOTS:
1998 !n c. FINITE {x | sum{0..n} (\i. c i * x pow i) = 0:real} <=>
1999 ?i. i IN {0..n} /\ c i <> 0
2000Proof
2001 REPEAT GEN_TAC THEN REWRITE_TAC[TAUT `a /\ ~b <=> ~(a ==> b)`] THEN
2002 KNOW_TAC ``(?i. ~(i IN {0 .. n} ==> (c i = 0:real))) =
2003 (~(!i. i IN {0 .. n} ==> (c i = 0:real)))`` THENL
2004 [METIS_TAC [NOT_FORALL_THM], ALL_TAC] THEN DISC_RW_KILL THEN
2005 EQ_TAC THENL [ONCE_REWRITE_TAC[MONO_NOT_EQ] THEN DISCH_TAC THEN
2006 KNOW_TAC ``!x. (sum {0.. n} (\i. (c:num->real) i * x pow i)) =
2007 (sum {0.. n} (\i. (0:real) * x pow i))`` THENL
2008 [GEN_TAC THEN MATCH_MP_TAC SUM_EQ THEN METIS_TAC [], ALL_TAC] THEN
2009 DISC_RW_KILL THEN SIMP_TAC std_ss [REAL_MUL_LZERO, SUM_0] THEN
2010 REWRITE_TAC[SET_RULE ``{x | T} = univ(:real)``, real_INFINITE],
2011 SIMP_TAC std_ss [REAL_POLYFUN_ROOTBOUND]]
2012QED
2013
2014Theorem REAL_POLYFUN_EQ_0:
2015 !n c. (!x. sum{0..n} (\i. c i * x pow i) = 0:real) <=>
2016 (!i. i IN {0..n} ==> (c i = 0:real))
2017Proof
2018 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
2019 [GEN_REWR_TAC I [TAUT `p <=> ~ ~p`] THEN DISCH_THEN(MP_TAC o MATCH_MP
2020 REAL_POLYFUN_ROOTBOUND) THEN
2021 ASM_REWRITE_TAC[real_INFINITE, DE_MORGAN_THM,
2022 SET_RULE ``{x | T} = univ(:real)``],
2023 KNOW_TAC ``!x. (sum {0.. n} (\i. (c:num->real) i * x pow i)) =
2024 (sum {0.. n} (\i. (0:real) * x pow i))`` THENL
2025 [GEN_TAC THEN MATCH_MP_TAC SUM_EQ THEN METIS_TAC [], ALL_TAC] THEN
2026 DISC_RW_KILL THEN SIMP_TAC std_ss [REAL_MUL_LZERO, SUM_0]]
2027QED
2028
2029Theorem REAL_POLYFUN_EQ_CONST:
2030 !n c k. (!x. sum{0..n} (\i. c i * x pow i) = k) <=>
2031 (c 0 = k) /\ (!i. i IN {1..n} ==> (c i = 0:real))
2032Proof
2033 REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
2034 ``!x. sum{0..n} (\i. (if i = 0 then c 0 - k else c i) * x pow i) = 0:real`` THEN
2035 CONJ_TAC THENL
2036 [SIMP_TAC std_ss [SUM_CLAUSES_LEFT, ZERO_LESS_EQ, pow, REAL_MUL_RID] THEN
2037 REWRITE_TAC[REAL_ARITH ``((c - k) + s = 0:real) <=> (c + s = k)``] THEN
2038 AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2039 AP_TERM_TAC THEN MATCH_MP_TAC SUM_EQ THEN GEN_TAC THEN
2040 REWRITE_TAC[IN_NUMSEG] THEN BETA_TAC THEN
2041 COND_CASES_TAC THEN RW_TAC arith_ss [],
2042 SIMP_TAC std_ss [REAL_POLYFUN_EQ_0, IN_NUMSEG, ZERO_LESS_EQ] THEN
2043 EQ_TAC THENL [RW_TAC arith_ss [] THENL
2044 [POP_ASSUM (MP_TAC o Q.SPEC `0:num`) THEN COND_CASES_TAC THENL
2045 [RW_TAC arith_ss [REAL_POS] THEN POP_ASSUM MP_TAC THEN
2046 REAL_ARITH_TAC, METIS_TAC []], POP_ASSUM MP_TAC THEN
2047 POP_ASSUM MP_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `i:num`) THEN
2048 RW_TAC arith_ss []], RW_TAC arith_ss [REAL_SUB_REFL]]]
2049QED
2050
2051(* ------------------------------------------------------------------------- *)
2052(* A general notion of polynomial function. *)
2053(* ------------------------------------------------------------------------- *)
2054
2055Definition polynomial_function[nocompute]:
2056 polynomial_function p <=> ?m c. !x. p x = sum{0..m} (\i. c i * x pow i)
2057End
2058
2059Theorem POLYNOMIAL_FUNCTION_CONST:
2060 !c. polynomial_function (\x. c)
2061Proof
2062 GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN
2063 MAP_EVERY EXISTS_TAC [``0:num``, ``(\i. c):num->real``] THEN
2064 SIMP_TAC std_ss [SUM_SING_NUMSEG, pow, REAL_MUL_RID]
2065QED
2066
2067Theorem POLYNOMIAL_FUNCTION_ID:
2068 polynomial_function (\x. x)
2069Proof
2070 REWRITE_TAC[polynomial_function] THEN
2071 MAP_EVERY EXISTS_TAC [``SUC 0``, ``\i. if i = 1:num then 1:real else 0:real``] THEN
2072 SIMP_TAC arith_ss [SUM_CLAUSES_NUMSEG, ZERO_LESS_EQ, pow] THEN REAL_ARITH_TAC
2073QED
2074
2075Theorem POLYNOMIAL_FUNCTION_ADD:
2076 !p q. polynomial_function p /\ polynomial_function q
2077 ==> polynomial_function (\x. p x + q x)
2078Proof
2079 REPEAT GEN_TAC THEN
2080 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, polynomial_function, PULL_EXISTS] THEN
2081 MAP_EVERY X_GEN_TAC [``m:num``, ``a:num->real``] THEN STRIP_TAC THEN
2082 MAP_EVERY X_GEN_TAC [``n:num``, ``b:num->real``] THEN STRIP_TAC THEN
2083 ASM_REWRITE_TAC[] THEN EXISTS_TAC ``MAX m n`` THEN EXISTS_TAC
2084 ``\i:num. (if i <= m then a i else 0:real) + (if i <= n then b i else 0:real)`` THEN
2085 GEN_TAC THEN SIMP_TAC std_ss [REAL_ADD_RDISTRIB, SUM_ADD_NUMSEG] THEN
2086 REWRITE_TAC[COND_RAND, COND_RATOR, REAL_MUL_LZERO] THEN
2087 SIMP_TAC std_ss [GSYM SUM_RESTRICT_SET] THEN
2088 MATCH_MP_TAC (REAL_ARITH ``(a = b) /\ (c = d) ==> (a + c = b + d:real)``) THEN
2089 CONJ_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2090 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_NUMSEG] THEN ARITH_TAC
2091QED
2092
2093Theorem POLYNOMIAL_FUNCTION_LMUL:
2094 !p c. polynomial_function p ==> polynomial_function (\x. c * p x)
2095Proof
2096 REPEAT GEN_TAC THEN
2097 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, polynomial_function, PULL_EXISTS] THEN
2098 MAP_EVERY X_GEN_TAC [``n:num``, ``a:num->real``] THEN STRIP_TAC THEN
2099 MAP_EVERY EXISTS_TAC [``n:num``, ``\i. c * (a:num->real) i``] THEN
2100 ASM_SIMP_TAC std_ss [SUM_LMUL, GSYM REAL_MUL_ASSOC]
2101QED
2102
2103Theorem POLYNOMIAL_FUNCTION_RMUL:
2104 !p c. polynomial_function p ==> polynomial_function (\x. p x * c)
2105Proof
2106 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[POLYNOMIAL_FUNCTION_LMUL]
2107QED
2108
2109Theorem POLYNOMIAL_FUNCTION_NEG:
2110 !p. polynomial_function(\x. -(p x)) <=> polynomial_function p
2111Proof
2112 GEN_TAC THEN EQ_TAC THEN
2113 DISCH_THEN(MP_TAC o SPEC ``-(1:real)`` o MATCH_MP POLYNOMIAL_FUNCTION_LMUL) THEN
2114 SIMP_TAC std_ss [REAL_MUL_LNEG, REAL_MUL_LID, ETA_AX, REAL_NEG_NEG]
2115QED
2116
2117Theorem POLYNOMIAL_FUNCTION_SUB:
2118 !p q. polynomial_function p /\ polynomial_function q
2119 ==> polynomial_function (\x. p x - q x)
2120Proof
2121 SIMP_TAC std_ss [real_sub, POLYNOMIAL_FUNCTION_NEG, POLYNOMIAL_FUNCTION_ADD]
2122QED
2123
2124Theorem POLYNOMIAL_FUNCTION_MUL:
2125 !p q. polynomial_function p /\ polynomial_function q
2126 ==> polynomial_function (\x. p x * q x)
2127Proof
2128 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
2129 GEN_TAC THEN DISCH_TAC THEN
2130 GEN_REWR_TAC (BINDER_CONV o LAND_CONV) [polynomial_function] THEN
2131 SIMP_TAC std_ss [PULL_EXISTS] THEN
2132 SIMP_TAC std_ss [GSYM FUN_EQ_THM] THEN INDUCT_TAC THEN
2133 ASM_SIMP_TAC std_ss [SUM_SING_NUMSEG, pow, POLYNOMIAL_FUNCTION_RMUL] THEN
2134 X_GEN_TAC ``c:num->real`` THEN SIMP_TAC std_ss [SUM_CLAUSES_LEFT] THEN
2135 SIMP_TAC std_ss [ZERO_LESS_EQ, ADD1] THEN
2136 REWRITE_TAC[REAL_ADD_LDISTRIB, pow] THEN
2137 KNOW_TAC ``polynomial_function
2138 (\x. p x * (c 0n * 1:real))`` THENL
2139 [ASM_SIMP_TAC std_ss [POLYNOMIAL_FUNCTION_RMUL], ALL_TAC] THEN
2140 KNOW_TAC ``polynomial_function
2141 (\x. p x * sum {1 .. m + 1} (\i. c i * x pow i))`` THENL
2142 [ONCE_REWRITE_TAC[ARITH_PROVE ``(1:num = 0 + 1)``] THEN
2143 ONCE_REWRITE_TAC[ARITH_PROVE ``(m + (0 + 1:num) = m + 1)``] THEN
2144 REWRITE_TAC [SPEC ``1:num`` SUM_OFFSET] THEN BETA_TAC THEN
2145 SIMP_TAC std_ss [REAL_POW_ADD, POW_1, REAL_MUL_ASSOC, SUM_RMUL] THEN
2146 FIRST_X_ASSUM(MP_TAC o SPEC ``\i. (c:num->real)(i + 1)``) THEN BETA_TAC THEN
2147 ABBREV_TAC ``q = \x. p x * sum {0..m} (\i. c (i + 1:num) * x pow i)`` THEN
2148 RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM]) THEN POP_ASSUM MP_TAC THEN
2149 BETA_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC [] THEN
2150 SIMP_TAC std_ss [polynomial_function] THEN SIMP_TAC std_ss [PULL_EXISTS] THEN
2151 MAP_EVERY X_GEN_TAC [``n:num``, ``a:num->real``] THEN STRIP_TAC THEN
2152 EXISTS_TAC ``n + 1:num`` THEN
2153 EXISTS_TAC ``\i. if i = 0 then 0:real else (a:num->real)(i - 1)`` THEN
2154 POP_ASSUM MP_TAC THEN GEN_REWR_TAC (LAND_CONV o QUANT_CONV) [EQ_SYM_EQ] THEN
2155 DISCH_TAC THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN
2156 KNOW_TAC ``!x:real. (sum {0.. n + 1}
2157 (\i. (if i = 0 then 0 else (a:num->real) (i - 1)) * x pow i)) =
2158 (0:real * x pow 0 + sum {0 + 1..n + 1}
2159 (\i. (if i = 0 then 0 else (a:num->real) (i - 1)) * x pow i))`` THENL
2160 [SIMP_TAC std_ss [SUM_CLAUSES_LEFT], ALL_TAC] THEN DISC_RW_KILL THEN
2161 ASM_SIMP_TAC std_ss [SPEC ``1:num`` SUM_OFFSET, ADD_EQ_0, ADD_SUB] THEN
2162 POP_ASSUM MP_TAC THEN GEN_REWR_TAC (LAND_CONV o QUANT_CONV) [EQ_SYM_EQ] THEN
2163 DISCH_TAC THEN ASM_REWRITE_TAC [] THEN SIMP_TAC arith_ss [REAL_POW_ADD,
2164 REAL_MUL_ASSOC, SUM_RMUL, POW_1, pow] THEN REAL_ARITH_TAC,
2165 METIS_TAC [POLYNOMIAL_FUNCTION_ADD]]
2166QED
2167
2168Theorem POLYNOMIAL_FUNCTION_SUM:
2169 !s:'a->bool p.
2170 FINITE s /\ (!i. i IN s ==> polynomial_function(\x. p x i))
2171 ==> polynomial_function (\x. sum s (p x))
2172Proof
2173 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN
2174 KNOW_TAC ``(!p. (!i. i IN s ==> polynomial_function (\x. p x i)) ==>
2175 polynomial_function (\x. sum s (p x))) =
2176 (\s. !p. (!i. i IN s ==> polynomial_function (\x. p x i)) ==>
2177 polynomial_function (\x. sum s (p x))) (s:'a->bool)`` THENL
2178 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
2179 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2180 SIMP_TAC std_ss [SUM_CLAUSES, POLYNOMIAL_FUNCTION_CONST] THEN
2181 SIMP_TAC std_ss [SET_RULE ``!P a s. (!x. x IN a INSERT s ==> P x) <=>
2182 P a /\ (!x. x IN s ==> P x)``, POLYNOMIAL_FUNCTION_ADD]
2183QED
2184
2185Theorem POLYNOMIAL_FUNCTION_POW:
2186 !p n. polynomial_function p ==> polynomial_function (\x. p x pow n)
2187Proof
2188 SIMP_TAC std_ss [RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN
2189 DISCH_TAC THEN INDUCT_TAC THEN
2190 ASM_SIMP_TAC std_ss [pow, POLYNOMIAL_FUNCTION_CONST, POLYNOMIAL_FUNCTION_MUL]
2191QED
2192
2193Theorem POLYNOMIAL_FUNCTION_INDUCT:
2194 !P. P (\x. x) /\ (!c. P (\x. c)) /\
2195 (!p q. P p /\ P q ==> P (\x. p x + q x)) /\
2196 (!p q. P p /\ P q ==> P (\x. p x * q x))
2197 ==> !p. polynomial_function p ==> P p
2198Proof
2199 GEN_TAC THEN STRIP_TAC THEN
2200 SIMP_TAC std_ss [polynomial_function, PULL_EXISTS] THEN
2201 SIMP_TAC std_ss [GSYM FUN_EQ_THM] THEN
2202 SIMP_TAC std_ss [LEFT_FORALL_IMP_THM, EXISTS_REFL] THEN INDUCT_TAC THEN
2203 ASM_SIMP_TAC arith_ss [SUM_SING_NUMSEG, pow] THEN
2204 KNOW_TAC ``!c x:real. (sum {0.. SUC m} (\i. (c:num->real) i * x pow i)) =
2205 (c 0 * x pow 0 + sum {0 + 1..m + 1} (\i. (c:num->real) i * x pow i))`` THENL
2206 [REPEAT GEN_TAC THEN ASM_SIMP_TAC arith_ss [SUM_CLAUSES_LEFT, ADD1,
2207 ZERO_LESS_EQ, pow], ALL_TAC] THEN DISC_RW_KILL THEN GEN_TAC THEN
2208 KNOW_TAC ``(P :(real -> real) -> bool) (\(x :real).
2209 (c :num -> real) 0n * x pow 0n) /\
2210 P (\x. (sum {0+1 .. m+1}
2211 (\(i :num). c i * x pow i) :real))`` THENL
2212 [ASM_REWRITE_TAC[pow] THEN
2213 REWRITE_TAC[SPEC ``1:num`` SUM_OFFSET] THEN
2214 ASM_SIMP_TAC std_ss [REAL_POW_ADD, POW_1, REAL_MUL_ASSOC, SUM_RMUL],
2215 METIS_TAC []]
2216QED
2217
2218Theorem POLYNOMIAL_FUNCTION_o:
2219 !p q. polynomial_function p /\ polynomial_function q
2220 ==> polynomial_function (p o q)
2221Proof
2222 ONCE_REWRITE_TAC [METIS [] ``(!p q.
2223 polynomial_function p /\ polynomial_function q ==>
2224 polynomial_function (p o q)) = (!q p.
2225 polynomial_function p /\ polynomial_function q ==>
2226 polynomial_function (p o q))``] THEN ONCE_REWRITE_TAC [CONJ_SYM] THEN
2227 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
2228 GEN_TAC THEN DISCH_TAC THEN
2229 KNOW_TAC ``!p. polynomial_function (p o q) =
2230 (\p. polynomial_function (p o q)) (p:real->real)`` THENL
2231 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
2232 MATCH_MP_TAC POLYNOMIAL_FUNCTION_INDUCT THEN BETA_TAC THEN
2233 SIMP_TAC std_ss [o_DEF, POLYNOMIAL_FUNCTION_ADD, POLYNOMIAL_FUNCTION_MUL] THEN
2234 ASM_REWRITE_TAC[ETA_AX, POLYNOMIAL_FUNCTION_CONST]
2235QED
2236
2237Theorem POLYNOMIAL_FUNCTION_FINITE_ROOTS:
2238 !p a. polynomial_function p
2239 ==> (FINITE {x | p x = a} <=> ~(!x. p x = a))
2240Proof
2241 ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
2242 SUBGOAL_THEN
2243 ``!p. polynomial_function p ==> (FINITE {x | p x = 0:real} <=> ~(!x. p x = 0:real))``
2244 (fn th =>
2245 SIMP_TAC std_ss [th, POLYNOMIAL_FUNCTION_SUB, POLYNOMIAL_FUNCTION_CONST]) THEN
2246 GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN
2247 STRIP_TAC THEN EQ_TAC THEN ONCE_REWRITE_TAC[MONO_NOT_EQ] THENL
2248 [SIMP_TAC std_ss [GSPEC_T, real_INFINITE],
2249 ASM_REWRITE_TAC[REAL_POLYFUN_FINITE_ROOTS] THEN
2250 SIMP_TAC std_ss [NOT_EXISTS_THM, TAUT `~(p /\ ~q) <=> p ==> q`] THEN DISCH_TAC THEN
2251 KNOW_TAC ``!x. (sum {0.. m} (\i. (c:num->real) i * x pow i)) =
2252 (sum {0.. m} (\i. (0:real) * x pow i))`` THENL
2253 [GEN_TAC THEN MATCH_MP_TAC SUM_EQ THEN METIS_TAC [], ALL_TAC] THEN DISC_RW_KILL THEN
2254 REWRITE_TAC[REAL_MUL_LZERO, SUM_0]]
2255QED
2256
2257(* ------------------------------------------------------------------------- *)
2258(* Now products over real numbers. *)
2259(* ------------------------------------------------------------------------- *)
2260
2261Definition product[nocompute]:
2262 product = iterate (( * ):real->real->real)
2263End
2264
2265Theorem PRODUCT_CLAUSES:
2266 (!f. product {} f = &1) /\
2267 (!x f s. FINITE(s)
2268 ==> (product (x INSERT s) f =
2269 if x IN s then product s f else f(x) * product s f))
2270Proof
2271 REWRITE_TAC[product, GSYM NEUTRAL_REAL_MUL] THEN
2272 METIS_TAC [SWAP_FORALL_THM, ITERATE_CLAUSES, MONOIDAL_REAL_MUL]
2273QED
2274
2275Theorem PRODUCT_SUPPORT:
2276 !f s. product (support ( * ) f s) f = product s f
2277Proof
2278 REWRITE_TAC[product, ITERATE_SUPPORT]
2279QED
2280
2281Theorem PRODUCT_UNION:
2282 !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
2283 ==> (product (s UNION t) f = product s f * product t f)
2284Proof
2285 SIMP_TAC std_ss [product, ITERATE_UNION, MONOIDAL_REAL_MUL]
2286QED
2287
2288Theorem PRODUCT_IMAGE:
2289 !f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
2290 ==> (product (IMAGE f s) g = product s (g o f))
2291Proof
2292 REWRITE_TAC[product, GSYM NEUTRAL_REAL_MUL] THEN
2293 MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_REAL_MUL]
2294QED
2295
2296Theorem PRODUCT_ADD_SPLIT:
2297 !f m n p.
2298 m <= n + 1
2299 ==> (product {m..n+p} f = product{m..n} f * product{n+1..n+p} f)
2300Proof
2301 METIS_TAC [NUMSEG_ADD_SPLIT, PRODUCT_UNION, DISJOINT_NUMSEG, FINITE_NUMSEG,
2302 ARITH_PROVE ``x < x + 1:num``]
2303QED
2304
2305Theorem PRODUCT_POS_LE:
2306 !f s. FINITE s /\ (!x. x IN s ==> &0 <= f x) ==> &0 <= product s f
2307Proof
2308 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2309 ONCE_REWRITE_TAC [METIS [] ``!s.
2310 ((!x. x IN s ==> 0 <= f x) ==> 0 <= product s f) =
2311 (\s. (!x. x IN s ==> 0 <= f x) ==> 0 <= product s f) s``] THEN
2312 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2313 SIMP_TAC std_ss [PRODUCT_CLAUSES, REAL_POS, IN_INSERT, REAL_LE_MUL]
2314QED
2315
2316Theorem PRODUCT_POS_LE_NUMSEG:
2317 !f m n. (!x. m <= x /\ x <= n ==> &0 <= f x) ==> &0 <= product{m..n} f
2318Proof
2319 SIMP_TAC std_ss [PRODUCT_POS_LE, FINITE_NUMSEG, IN_NUMSEG]
2320QED
2321
2322Theorem PRODUCT_POS_LT:
2323 !f s. FINITE s /\ (!x. x IN s ==> &0 < f x) ==> &0 < product s f
2324Proof
2325 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2326 ONCE_REWRITE_TAC [METIS [] ``!s.
2327 ((!x. x IN s ==> &0 < f x) ==> &0 < product s f) =
2328 (\s. (!x. x IN s ==> &0 < f x) ==> &0 < product s f) s``] THEN
2329 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2330 SIMP_TAC std_ss [PRODUCT_CLAUSES, REAL_LT_01, IN_INSERT, REAL_LT_MUL]
2331QED
2332
2333Theorem PRODUCT_POS_LT_NUMSEG:
2334 !f m n. (!x. m <= x /\ x <= n ==> &0 < f x) ==> &0 < product{m..n} f
2335Proof
2336 SIMP_TAC std_ss [PRODUCT_POS_LT, FINITE_NUMSEG, IN_NUMSEG]
2337QED
2338
2339Theorem PRODUCT_OFFSET:
2340 !f m p. product{m+p..n+p} f = product{m..n} (\i. f(i + p))
2341Proof
2342 SIMP_TAC std_ss [NUMSEG_OFFSET_IMAGE, PRODUCT_IMAGE,
2343 EQ_ADD_RCANCEL, FINITE_NUMSEG] THEN
2344 SIMP_TAC std_ss [o_DEF]
2345QED
2346
2347Theorem PRODUCT_SING:
2348 !f x. product {x} f = f(x)
2349Proof
2350 SIMP_TAC std_ss [PRODUCT_CLAUSES, FINITE_EMPTY, FINITE_INSERT, NOT_IN_EMPTY,
2351 REAL_MUL_RID]
2352QED
2353
2354Theorem PRODUCT_SING_NUMSEG:
2355 !f n. product{n..n} f = f(n)
2356Proof
2357 REWRITE_TAC[NUMSEG_SING, PRODUCT_SING]
2358QED
2359
2360Theorem PRODUCT_CLAUSES_NUMSEG:
2361 (!m. product{m..0n} f = if m = 0 then f(0) else &1) /\
2362 (!m n. product{m..SUC n} f = if m <= SUC n then product{m..n} f * f(SUC n)
2363 else product{m..n} f)
2364Proof
2365 REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
2366 COND_CASES_TAC THEN
2367 ASM_SIMP_TAC std_ss [PRODUCT_SING, PRODUCT_CLAUSES, FINITE_NUMSEG, IN_NUMSEG] THEN
2368 SIMP_TAC std_ss [ARITH_PROVE ``~(SUC n <= n)``, REAL_MUL_ASSOC, REAL_MUL_SYM]
2369QED
2370
2371Theorem PRODUCT_EQ:
2372 !f g s. (!x. x IN s ==> (f x = g x)) ==> (product s f = product s g)
2373Proof
2374 REWRITE_TAC[product] THEN MATCH_MP_TAC ITERATE_EQ THEN
2375 REWRITE_TAC[MONOIDAL_REAL_MUL]
2376QED
2377
2378Theorem PRODUCT_EQ_COUNT :
2379 !f g n. (!i. i < n ==> (f i = g i)) ==>
2380 product (count n) f = product (count n) g
2381Proof
2382 rpt STRIP_TAC
2383 >> MATCH_MP_TAC PRODUCT_EQ >> rw []
2384QED
2385
2386Theorem PRODUCT_EQ_NUMSEG:
2387 !f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
2388 ==> (product{m..n} f = product{m..n} g)
2389Proof
2390 MESON_TAC[PRODUCT_EQ, FINITE_NUMSEG, IN_NUMSEG]
2391QED
2392
2393Theorem PRODUCT_EQ_0:
2394 !f s. FINITE s ==> ((product s f = &0) <=> ?x. x IN s /\ (f(x) = &0))
2395Proof
2396 GEN_TAC THEN
2397 ONCE_REWRITE_TAC [METIS [] ``!s.
2398 (((product s f = &0) <=> ?x. x IN s /\ (f(x) = &0))) =
2399 (\s. ((product s f = &0) <=> ?x. x IN s /\ (f(x) = &0))) s``] THEN
2400 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2401 SIMP_TAC arith_ss [PRODUCT_CLAUSES, REAL_ENTIRE, IN_INSERT, REAL_OF_NUM_EQ,
2402 NOT_IN_EMPTY] THEN
2403 MESON_TAC[]
2404QED
2405
2406Theorem PRODUCT_EQ_0_COUNT :
2407 !f n. product (count n) f = &0 <=> ?i. i < n /\ (f(i) = &0)
2408Proof
2409 rpt GEN_TAC
2410 >> Suff ‘product (count n) f = &0 <=> ?x. x IN count n /\ (f(x) = &0)’ >- rw []
2411 >> MATCH_MP_TAC PRODUCT_EQ_0 >> rw []
2412QED
2413
2414Theorem PRODUCT_EQ_0_NUMSEG:
2415 !f m n. (product{m..n} f = &0) <=> ?x. m <= x /\ x <= n /\ (f(x) = &0)
2416Proof
2417 SIMP_TAC std_ss [PRODUCT_EQ_0, FINITE_NUMSEG, IN_NUMSEG, GSYM CONJ_ASSOC]
2418QED
2419
2420Theorem PRODUCT_LE:
2421 !f s. FINITE s /\ (!x. x IN s ==> &0 <= f(x) /\ f(x) <= g(x))
2422 ==> product s f <= product s g
2423Proof
2424 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2425 ONCE_REWRITE_TAC [METIS [] ``!s.
2426 ((!x. x IN s ==> &0 <= f(x) /\ f(x) <= g(x))
2427 ==> product s f <= product s g) =
2428 (\s. (!x. x IN s ==> &0 <= f(x) /\ f(x) <= g(x))
2429 ==> product s f <= product s g) s``] THEN
2430 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2431 SIMP_TAC std_ss [IN_INSERT, PRODUCT_CLAUSES, NOT_IN_EMPTY, REAL_LE_REFL] THEN
2432 MESON_TAC[REAL_LE_MUL2, PRODUCT_POS_LE]
2433QED
2434
2435Theorem PRODUCT_LE_NUMSEG:
2436 !f m n. (!i. m <= i /\ i <= n ==> &0 <= f(i) /\ f(i) <= g(i))
2437 ==> product{m..n} f <= product{m..n} g
2438Proof
2439 SIMP_TAC std_ss [PRODUCT_LE, FINITE_NUMSEG, IN_NUMSEG]
2440QED
2441
2442Theorem PRODUCT_EQ_1:
2443 !f s. (!x:'a. x IN s ==> (f(x) = &1)) ==> (product s f = &1)
2444Proof
2445 REWRITE_TAC[product, GSYM NEUTRAL_REAL_MUL] THEN
2446 SIMP_TAC std_ss [ITERATE_EQ_NEUTRAL, MONOIDAL_REAL_MUL]
2447QED
2448
2449Theorem PRODUCT_EQ_1_COUNT :
2450 !f n. (!i. i < n ==> f i = &1) ==> product (count n) f = &1
2451Proof
2452 rpt GEN_TAC
2453 >> Suff ‘(!i. i IN count n ==> f i = &1) ==> product (count n) f = &1’ >- rw []
2454 >> DISCH_TAC
2455 >> MATCH_MP_TAC PRODUCT_EQ_1 >> art []
2456QED
2457
2458Theorem PRODUCT_EQ_1_NUMSEG:
2459 !f m n. (!i. m <= i /\ i <= n ==> (f(i) = &1)) ==> (product{m..n} f = &1)
2460Proof
2461 SIMP_TAC std_ss [PRODUCT_EQ_1, IN_NUMSEG]
2462QED
2463
2464Theorem PRODUCT_MUL_GEN:
2465 !f g s.
2466 FINITE {x | x IN s /\ ~(f x = &1)} /\ FINITE {x | x IN s /\ ~(g x = &1)}
2467 ==> (product s (\x. f x * g x) = product s f * product s g)
2468Proof
2469 REWRITE_TAC[GSYM NEUTRAL_REAL_MUL, GSYM support, product] THEN
2470 MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_REAL_MUL
2471QED
2472
2473Theorem PRODUCT_MUL:
2474 !f g s. FINITE s ==> (product s (\x. f x * g x) = product s f * product s g)
2475Proof
2476 GEN_TAC THEN GEN_TAC THEN
2477 ONCE_REWRITE_TAC [METIS [] ``!s.
2478 (product s (\x. f x * g x) = product s f * product s g) =
2479 (\s. product s (\x. f x * g x) = product s f * product s g) s``] THEN
2480 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2481 SIMP_TAC std_ss [PRODUCT_CLAUSES, REAL_MUL_ASSOC, REAL_MUL_LID] THEN
2482 METIS_TAC [REAL_ARITH ``a * b * c * d = a * c * b * d:real``]
2483QED
2484
2485Theorem PRODUCT_MUL_COUNT :
2486 !f g n. product (count n) (\x. f x * g x) =
2487 product (count n) f * product (count n) g
2488Proof
2489 rpt GEN_TAC
2490 >> MATCH_MP_TAC PRODUCT_MUL >> rw []
2491QED
2492
2493Theorem PRODUCT_MUL_NUMSEG:
2494 !f g m n.
2495 product{m..n} (\x. f x * g x) = product{m..n} f * product{m..n} g
2496Proof
2497 SIMP_TAC std_ss [PRODUCT_MUL, FINITE_NUMSEG]
2498QED
2499
2500Theorem PRODUCT_CONST:
2501 !c s. FINITE s ==> (product s (\x. c) = c pow (CARD s))
2502Proof
2503 GEN_TAC THEN
2504 ONCE_REWRITE_TAC [METIS [] ``!s.
2505 (product s (\x. c) = c pow (CARD s)) =
2506 (\s. product s (\x. c) = c pow (CARD s)) s``] THEN
2507 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2508 SIMP_TAC std_ss [PRODUCT_CLAUSES, CARD_EMPTY, CARD_INSERT, pow]
2509QED
2510
2511Theorem PRODUCT_CONST_NUMSEG:
2512 !c m n. product {m..n} (\x. c) = c pow ((n + 1) - m)
2513Proof
2514 SIMP_TAC std_ss [PRODUCT_CONST, CARD_NUMSEG, FINITE_NUMSEG]
2515QED
2516
2517Theorem PRODUCT_CONST_NUMSEG_1:
2518 !c n. product{1n..n} (\x. c) = c pow n
2519Proof
2520 SIMP_TAC std_ss [PRODUCT_CONST, CARD_NUMSEG_1, FINITE_NUMSEG]
2521QED
2522
2523Theorem PRODUCT_NEG:
2524 !f s:'a->bool.
2525 FINITE s ==> (product s (\i. -(f i)) = -(&1) pow (CARD s) * product s f)
2526Proof
2527 SIMP_TAC std_ss [GSYM PRODUCT_CONST, GSYM PRODUCT_MUL] THEN
2528 REWRITE_TAC[REAL_MUL_LNEG, REAL_MUL_LID]
2529QED
2530
2531Theorem PRODUCT_NEG_NUMSEG:
2532 !f m n. product{m..n} (\i. -(f i)) =
2533 -(&1) pow ((n + 1) - m) * product{m..n} f
2534Proof
2535 SIMP_TAC std_ss [PRODUCT_NEG, CARD_NUMSEG, FINITE_NUMSEG]
2536QED
2537
2538Theorem PRODUCT_NEG_NUMSEG_1:
2539 !f n. product{1n..n} (\i. -(f i)) = -(&1) pow n * product{1n..n} f
2540Proof
2541 REWRITE_TAC[PRODUCT_NEG_NUMSEG, ADD_SUB]
2542QED
2543
2544Theorem PRODUCT_INV:
2545 !f s. FINITE s ==> (product s (\x. inv(f x)) = inv(product s f))
2546Proof
2547 GEN_TAC THEN ONCE_REWRITE_TAC [METIS [] ``!s.
2548 (product s (\x. inv(f x)) = inv(product s f)) =
2549 (\s. product s (\x. inv(f x)) = inv(product s f)) s``] THEN
2550 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2551 SIMP_TAC real_ss [PRODUCT_CLAUSES, REAL_INV1] THEN REPEAT STRIP_TAC THEN
2552 ASM_CASES_TAC ``((f:'a->real) e <> 0) /\ (product s f <> 0:real)`` THENL
2553 [ASM_SIMP_TAC real_ss [GSYM REAL_INV_MUL], ALL_TAC] THEN
2554 FULL_SIMP_TAC real_ss [REAL_INV_0]
2555QED
2556
2557Theorem PRODUCT_DIV:
2558 !f g s. FINITE s ==> (product s (\x. f x / g x) = product s f / product s g)
2559Proof
2560 SIMP_TAC std_ss [real_div, PRODUCT_MUL, PRODUCT_INV]
2561QED
2562
2563Theorem PRODUCT_DIV_NUMSEG:
2564 !f g m n.
2565 product{m..n} (\x. f x / g x) = product{m..n} f / product{m..n} g
2566Proof
2567 SIMP_TAC std_ss [PRODUCT_DIV, FINITE_NUMSEG]
2568QED
2569
2570Theorem PRODUCT_ONE:
2571 !s. product s (\n. &1) = &1
2572Proof
2573 SIMP_TAC std_ss [PRODUCT_EQ_1]
2574QED
2575
2576Theorem PRODUCT_LE_1:
2577 !f s. FINITE s /\ (!x. x IN s ==> &0 <= f x /\ f x <= &1)
2578 ==> product s f <= &1
2579Proof
2580 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2581 ONCE_REWRITE_TAC [METIS [] ``!s.
2582 ((!x. x IN s ==> &0 <= f x /\ f x <= &1)
2583 ==> product s f <= &1) =
2584 (\s. (!x. x IN s ==> &0 <= f x /\ f x <= &1)
2585 ==> product s f <= &1) s``] THEN
2586 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2587 SIMP_TAC std_ss [PRODUCT_CLAUSES, REAL_LE_REFL, IN_INSERT] THEN
2588 REPEAT STRIP_TAC THEN GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
2589 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC std_ss [PRODUCT_POS_LE]
2590QED
2591
2592Theorem PRODUCT_ABS:
2593 !f s. FINITE s ==> (product s (\x. abs(f x)) = abs(product s f))
2594Proof
2595 GEN_TAC THEN ONCE_REWRITE_TAC [METIS [] ``!s.
2596 (product s (\x. abs(f x)) = abs(product s f)) =
2597 (\s. product s (\x. abs(f x)) = abs(product s f)) s``] THEN
2598 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2599 SIMP_TAC std_ss [PRODUCT_CLAUSES, ABS_MUL, ABS_N]
2600QED
2601
2602Theorem PRODUCT_CLOSED:
2603 !P f:'a->real s.
2604 P(&1) /\ (!x y. P x /\ P y ==> P(x * y)) /\ (!a. a IN s ==> P(f a))
2605 ==> P(product s f)
2606Proof
2607 rpt STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_REAL_MUL) THEN
2608 DISCH_THEN(MP_TAC o SPEC ``P:real->bool``) THEN
2609 ASM_SIMP_TAC std_ss [NEUTRAL_REAL_MUL, GSYM product]
2610QED
2611
2612Theorem PRODUCT_CLAUSES_LEFT:
2613 !f m n. m <= n ==> (product{m..n} f = f(m) * product{m+1n..n} f)
2614Proof
2615 SIMP_TAC std_ss [GSYM NUMSEG_LREC, PRODUCT_CLAUSES, FINITE_NUMSEG, IN_NUMSEG] THEN
2616 SIMP_TAC arith_ss []
2617QED
2618
2619Theorem PRODUCT_CLAUSES_RIGHT:
2620 !f m n. 0 < n /\ m <= n ==> (product{m..n} f = product{m..n-1} f * f(n))
2621Proof
2622 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
2623 SIMP_TAC std_ss [LESS_REFL, PRODUCT_CLAUSES_NUMSEG, SUC_SUB1]
2624QED
2625
2626Theorem REAL_OF_NUM_NPRODUCT:
2627 !f:'a->num s. FINITE s ==> (&(nproduct s f) = product s (\x. &(f x)))
2628Proof
2629 GEN_TAC THEN ONCE_REWRITE_TAC [METIS [] ``!s.
2630 (&(nproduct s f) = product s (\x. &(f x))) =
2631 (\s. &(nproduct s f) = product s (\x. &(f x))) s``] THEN
2632 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2633 SIMP_TAC std_ss [PRODUCT_CLAUSES, NPRODUCT_CLAUSES] THEN
2634 REWRITE_TAC [GSYM REAL_OF_NUM_MUL] THEN METIS_TAC []
2635QED
2636
2637Theorem PRODUCT_SUPERSET:
2638 !f:'a->real u v.
2639 u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = &1))
2640 ==> (product v f = product u f)
2641Proof
2642 SIMP_TAC std_ss [product, GSYM NEUTRAL_REAL_MUL,
2643 ITERATE_SUPERSET, MONOIDAL_REAL_MUL]
2644QED
2645
2646Theorem PRODUCT_PAIR:
2647 !f m n. product{2*m..2*n+1} f = product{m..n} (\i. f(2*i) * f(2*i+1))
2648Proof
2649 MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_REAL_MUL) THEN
2650 SIMP_TAC std_ss [product, NEUTRAL_REAL_MUL]
2651QED
2652
2653Theorem PRODUCT_DELETE:
2654 !f s a. FINITE s /\ a IN s ==> (f(a) * product(s DELETE a) f = product s f)
2655Proof
2656 SIMP_TAC std_ss [product, ITERATE_DELETE, MONOIDAL_REAL_MUL]
2657QED
2658
2659Theorem PRODUCT_DELTA:
2660 !s a. product s (\x. if x = a then b else &1) =
2661 (if a IN s then b else &1)
2662Proof
2663 REWRITE_TAC[product, GSYM NEUTRAL_REAL_MUL] THEN
2664 SIMP_TAC std_ss [ITERATE_DELTA, MONOIDAL_REAL_MUL]
2665QED
2666
2667(* ------------------------------------------------------------------------- *)
2668(* Extend congruences. *)
2669(* ------------------------------------------------------------------------- *)
2670
2671Theorem PRODUCT_CONG :
2672 (!f g s. (!x. x IN s ==> (f(x) = g(x)))
2673 ==> (product s (\i. f(i)) = product s g)) /\
2674 (!f g a b. (!i. a <= i /\ i <= b ==> (f(i) = g(i)))
2675 ==> (product{a..b} (\i. f(i)) = product{a..b} g)) /\
2676 (!f g p. (!x. p x ==> (f x = g x))
2677 ==> (product {y | p y} (\i. f(i)) = product {y | p y} g))
2678Proof
2679 rpt STRIP_TAC
2680 >> MATCH_MP_TAC PRODUCT_EQ
2681 >> ASM_SIMP_TAC std_ss [GSPECIFICATION, IN_NUMSEG]
2682QED
2683
2684(* ------------------------------------------------------------------------- *)
2685(* Real-valued indicator function (cf. extrealTheory.indicator_fn) *)
2686(* ------------------------------------------------------------------------- *)
2687
2688(* This is originally from HOL Light (Multivariate/vectors.ml). Generalized. *)
2689Definition indicator :
2690 indicator (s :'a -> bool) :'a -> real = \x. if x IN s then 1 else 0
2691End
2692
2693Theorem DROP_INDICATOR :
2694 !s x. (indicator s x) = if x IN s then &1 else &0
2695Proof
2696 SIMP_TAC std_ss [indicator]
2697QED
2698
2699Theorem DROP_INDICATOR_POS_LE :
2700 !s x. &0 <= (indicator s x)
2701Proof
2702 RW_TAC real_ss [DROP_INDICATOR]
2703QED
2704
2705Theorem INDICATOR_POS = DROP_INDICATOR_POS_LE
2706
2707Theorem DROP_INDICATOR_LE_1 :
2708 !s x. (indicator s x) <= &1
2709Proof
2710 RW_TAC real_ss [DROP_INDICATOR]
2711QED
2712
2713Theorem DROP_INDICATOR_ABS_LE_1 :
2714 !s x. abs(indicator s x) <= &1
2715Proof
2716 RW_TAC real_ss [DROP_INDICATOR]
2717QED
2718
2719Theorem ABS_INDICATOR :
2720 !s x. abs(indicator s x) = indicator s x
2721Proof
2722 rw [ABS_REFL, INDICATOR_POS]
2723QED
2724
2725Theorem INDICATOR_EMPTY :
2726 indicator {} = (\x. 0)
2727Proof
2728 SET_TAC [indicator]
2729QED
2730
2731Theorem INDICATOR_COMPLEMENT :
2732 !s. indicator (UNIV DIFF s) = \x. 1 - indicator s x
2733Proof
2734 rw [FUN_EQ_THM, indicator]
2735 >> Cases_on ‘x IN s’ >> rw []
2736QED
2737
2738Theorem INDICATOR_MONO :
2739 !s t x. s SUBSET t ==> indicator s x <= indicator t x
2740Proof
2741 rpt STRIP_TAC
2742 >> Cases_on ‘x IN s’
2743 >- (‘x IN t’ by PROVE_TAC [SUBSET_DEF] \\
2744 RW_TAC real_ss [indicator])
2745 >> ‘indicator s x = 0’ by METIS_TAC [indicator]
2746 >> ASM_REWRITE_TAC [INDICATOR_POS]
2747QED
2748
2749(* ------------------------------------------------------------------------- *)
2750(* This lemma about iterations comes up in a few places. *)
2751(* ------------------------------------------------------------------------- *)
2752
2753Theorem ITERATE_NONZERO_IMAGE_LEMMA:
2754 !op s f g a.
2755 monoidal op /\ FINITE s /\ (g(a) = neutral op) /\
2756 (!x y. x IN s /\ y IN s /\ (f x = f y) /\ ~(x = y) ==> (g(f x) = neutral op))
2757 ==> (iterate op {f x | x | x IN s /\ ~(f x = a)} g =
2758 iterate op s (g o f))
2759Proof
2760 REPEAT STRIP_TAC THEN
2761 GEN_REWR_TAC RAND_CONV [GSYM ITERATE_SUPPORT] THEN
2762 REWRITE_TAC [support] THEN
2763 ONCE_REWRITE_TAC[SET_RULE ``{f x |x| x IN s /\ ~(f x = a)} =
2764 IMAGE f {x | x IN s /\ ~(f x = a)}``] THEN
2765 KNOW_TAC ``(!x y.
2766 x IN {x | x IN s /\ ~((g o f) x = neutral op)} /\
2767 y IN {x | x IN s /\ ~((g o f) x = neutral op)} /\
2768 (f x = f y) ==> (x = y))
2769 ==> (iterate (op:'a->'a->'a) (IMAGE (f:'b->'c) {x | x IN s /\ ~((g o f) x = neutral op)}) g =
2770 iterate op {x | x IN s /\ ~((g o f) x = neutral op)} ((g:'c->'a) o f))`` THENL
2771 [SRW_TAC [][ITERATE_IMAGE], ALL_TAC] THEN
2772 KNOW_TAC ``(!x y.
2773 x IN {x | x IN s /\ ((g:'c->'a) o (f:'b->'c)) x <> neutral op} /\
2774 y IN {x | x IN s /\ (g o f) x <> neutral op} /\
2775 (f x = f y) ==> (x = y))`` THENL
2776 [SIMP_TAC std_ss [GSPECIFICATION, o_THM] THEN ASM_MESON_TAC[],
2777 DISCH_TAC THEN ASM_REWRITE_TAC []] THEN
2778 DISCH_THEN(SUBST1_TAC o SYM) THEN
2779 KNOW_TAC ``IMAGE f {x | x IN s /\ ~(((g:'c->'a) o (f:'b->'c)) x = neutral op)} SUBSET
2780 IMAGE f {x | x IN s /\ ~(f x = a)} /\
2781 (!x. x IN IMAGE f {x | x IN s /\ ~(f x = a)} /\
2782 ~(x IN IMAGE f {x | x IN s /\ ~((g o f) x = neutral op)})
2783 ==> (g x = neutral (op:'a->'a->'a)))`` THENL
2784 [ALL_TAC, METIS_TAC [ITERATE_SUPERSET]] THEN
2785 ASM_SIMP_TAC std_ss [IMAGE_FINITE, FINITE_RESTRICT] THEN
2786 SIMP_TAC std_ss [IMP_CONJ, FORALL_IN_IMAGE, SUBSET_DEF] THEN
2787 SIMP_TAC std_ss [GSPECIFICATION, IN_IMAGE, o_THM] THEN
2788 ASM_MESON_TAC[]
2789QED
2790
2791(* ------------------------------------------------------------------------- *)
2792(* Useful Theorems on Real Numbers (from util_probTheory) *)
2793(* ------------------------------------------------------------------------- *)
2794
2795Theorem REAL_LE_LT_MUL:
2796 !x y : real. 0 <= x /\ 0 < y ==> 0 <= x * y
2797Proof
2798 rpt STRIP_TAC
2799 >> MP_TAC (Q.SPECL [`0`, `x`, `y`] REAL_LE_RMUL)
2800 >> RW_TAC std_ss [REAL_MUL_LZERO]
2801QED
2802
2803Theorem REAL_LT_LE_MUL:
2804 !x y : real. 0 < x /\ 0 <= y ==> 0 <= x * y
2805Proof
2806 PROVE_TAC [REAL_LE_LT_MUL, REAL_MUL_SYM]
2807QED
2808
2809Theorem REAL_MUL_IDEMPOT:
2810 !r: real. (r * r = r) <=> (r = 0) \/ (r = 1)
2811Proof
2812 GEN_TAC
2813 >> reverse EQ_TAC
2814 >- (RW_TAC real_ss [] >> RW_TAC std_ss [REAL_MUL_LZERO, REAL_MUL_LID])
2815 >> RW_TAC std_ss []
2816 >> Know `r * r = 1 * r` >- RW_TAC real_ss []
2817 >> RW_TAC std_ss [REAL_EQ_RMUL]
2818QED
2819
2820Theorem REAL_SUP_LE_X:
2821 !P x:real. (?r. P r) /\ (!r. P r ==> r <= x) ==> sup P <= x
2822Proof
2823 RW_TAC real_ss []
2824 >> Suff `~(x < sup P)` >- REAL_ARITH_TAC
2825 >> STRIP_TAC
2826 >> MP_TAC (SPEC ``P:real->bool`` REAL_SUP_LE)
2827 >> RW_TAC real_ss [] >|
2828 [PROVE_TAC [],
2829 PROVE_TAC [],
2830 EXISTS_TAC ``x:real``
2831 >> RW_TAC real_ss []
2832 >> PROVE_TAC [real_lte]]
2833QED
2834
2835Theorem REAL_X_LE_SUP:
2836 !P x:real. (?r. P r) /\ (?z. !r. P r ==> r <= z) /\ (?r. P r /\ x <= r)
2837 ==> x <= sup P
2838Proof
2839 RW_TAC real_ss []
2840 >> Suff `!y. P y ==> y <= sup P` >- PROVE_TAC [REAL_LE_TRANS]
2841 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE
2842 >> PROVE_TAC []
2843QED
2844
2845Theorem LE_INF:
2846 !p r:real. (?x. x IN p) /\ (!x. x IN p ==> r <= x) ==> r <= inf p
2847Proof
2848 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION]
2849 >> POP_ASSUM MP_TAC
2850 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG]
2851 >> Q.SPEC_TAC (`~r`, `r`)
2852 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG]
2853 >> MATCH_MP_TAC REAL_SUP_LE_X
2854 >> RW_TAC std_ss []
2855 >> PROVE_TAC [REAL_NEGNEG]
2856QED
2857
2858Theorem INF_LE:
2859 !p r:real.
2860 (?z. !x. x IN p ==> z <= x) /\ (?x. x IN p /\ x <= r) ==> inf p <= r
2861Proof
2862 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION]
2863 >> POP_ASSUM MP_TAC
2864 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG]
2865 >> Q.SPEC_TAC (`~r`, `r`)
2866 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG]
2867 >> MATCH_MP_TAC REAL_X_LE_SUP
2868 >> RW_TAC std_ss []
2869 >> PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]
2870QED
2871
2872Theorem INF_GREATER:
2873 !p z:real.
2874 (?x. x IN p) /\ inf p < z ==>
2875 (?x. x IN p /\ x < z)
2876Proof
2877 RW_TAC std_ss []
2878 >> Suff `~(!x. x IN p ==> ~(x < z))` >- PROVE_TAC []
2879 >> REWRITE_TAC [GSYM real_lte]
2880 >> STRIP_TAC
2881 >> Q.PAT_X_ASSUM `inf p < z` MP_TAC
2882 >> RW_TAC std_ss [GSYM real_lte]
2883 >> MATCH_MP_TAC LE_INF
2884 >> PROVE_TAC []
2885QED
2886
2887Theorem INF_CLOSE:
2888 !p e:real.
2889 (?x. x IN p) /\ 0 < e ==> (?x. x IN p /\ x < inf p + e)
2890Proof
2891 RW_TAC std_ss []
2892 >> MATCH_MP_TAC INF_GREATER
2893 >> CONJ_TAC >- PROVE_TAC []
2894 >> POP_ASSUM MP_TAC
2895 >> REAL_ARITH_TAC
2896QED
2897
2898Theorem REAL_NEG_NZ :
2899 !x:real. x < 0 ==> x <> 0
2900Proof
2901 GEN_TAC >> DISCH_TAC
2902 >> MATCH_MP_TAC REAL_LT_IMP_NE
2903 >> ASM_REWRITE_TAC []
2904QED
2905
2906Theorem REAL_LT_LMUL_0_NEG: !x y:real. 0 < x * y /\ x < 0 ==> y < 0
2907Proof
2908 RW_TAC real_ss []
2909 >> SPOSE_NOT_THEN ASSUME_TAC
2910 >> FULL_SIMP_TAC real_ss [REAL_NOT_LT, GSYM REAL_NEG_GT0]
2911 >> METIS_TAC [REAL_MUL_LNEG, REAL_LT_IMP_LE, REAL_LE_MUL,
2912 REAL_NEG_GE0, REAL_NOT_LT]
2913QED
2914
2915Theorem REAL_LT_RMUL_0_NEG: !x y:real. 0 < x * y /\ y < 0 ==> x < 0
2916Proof
2917 RW_TAC real_ss []
2918 >> SPOSE_NOT_THEN ASSUME_TAC
2919 >> FULL_SIMP_TAC real_ss [REAL_NOT_LT,GSYM REAL_NEG_GT0]
2920 >> METIS_TAC [REAL_MUL_RNEG, REAL_LT_IMP_LE, REAL_LE_MUL, REAL_NEG_GE0, REAL_NOT_LT]
2921QED
2922
2923Theorem REAL_LT_LMUL_NEG_0: !x y:real. x * y < 0 /\ 0 < x ==> y < 0
2924Proof
2925 RW_TAC real_ss []
2926 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_RMUL, REAL_LT_LMUL_0]
2927QED
2928
2929Theorem REAL_LT_RMUL_NEG_0: !x y:real. x * y < 0 /\ 0 < y ==> x < 0
2930Proof
2931 RW_TAC real_ss []
2932 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_LMUL, REAL_LT_RMUL_0]
2933QED
2934
2935Theorem REAL_LT_LMUL_NEG_0_NEG: !x y:real. x * y < 0 /\ x < 0 ==> 0 < y
2936Proof
2937 RW_TAC real_ss []
2938 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_LMUL, REAL_LT_LMUL_0]
2939QED
2940
2941Theorem REAL_LT_RMUL_NEG_0_NEG: !x y:real. x * y < 0 /\ y < 0 ==> 0 < x
2942Proof
2943 RW_TAC real_ss []
2944 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_RMUL, REAL_LT_RMUL_0]
2945QED
2946
2947Theorem REAL_LT_RDIV_EQ_NEG: !x y z. z < 0:real ==> (y / z < x <=> x * z < y)
2948Proof
2949 RW_TAC real_ss []
2950 >> `0<-z` by RW_TAC real_ss [REAL_NEG_GT0]
2951 >> `z<>0` by (METIS_TAC [REAL_LT_IMP_NE])
2952 >>EQ_TAC
2953 >- (RW_TAC real_ss []
2954 >> `y/z*(-z) < x*(-z)` by METIS_TAC [GSYM REAL_LT_RMUL]
2955 >> FULL_SIMP_TAC real_ss []
2956 >> METIS_TAC [REAL_DIV_RMUL, REAL_LT_NEG])
2957 >> RW_TAC real_ss []
2958 >> `-y < x*(-z)` by FULL_SIMP_TAC real_ss [REAL_LT_NEG]
2959 >> `-y * inv(-z) < x` by METIS_TAC [GSYM REAL_LT_LDIV_EQ, real_div]
2960 >> METIS_TAC [REAL_NEG_INV, REAL_NEG_MUL2, GSYM real_div]
2961QED
2962
2963(* REAL_LE_RDIV_EQ: |- !x y z. 0 < z ==> (x <= y / z <=> x * z <= y) *)
2964Theorem REAL_LE_RDIV_EQ_NEG :
2965 !x y z. z < (0 :real) ==> (y / z <= x <=> x * z <= y)
2966Proof
2967 RW_TAC real_ss []
2968 >> `0 < -z` by RW_TAC real_ss [REAL_NEG_GT0]
2969 >> `z <> 0` by (METIS_TAC [REAL_LT_IMP_NE])
2970 >> EQ_TAC
2971 >- (RW_TAC real_ss [] \\
2972 `y / z * (-z) <= x * (-z)` by METIS_TAC [GSYM REAL_LE_RMUL] \\
2973 FULL_SIMP_TAC real_ss [] \\
2974 METIS_TAC [REAL_DIV_RMUL, REAL_LE_NEG])
2975 >> RW_TAC real_ss []
2976 >> `-y <= x * (-z)` by FULL_SIMP_TAC real_ss [REAL_LE_NEG]
2977 >> `-y * inv (-z) <= x` by METIS_TAC [GSYM REAL_LE_LDIV_EQ, real_div]
2978 >> METIS_TAC [REAL_NEG_INV, REAL_NEG_MUL2, GSYM real_div]
2979QED
2980
2981(* REAL_LE_LDIV_EQ: |- !x y z. 0 < z ==> (x / z <= y <=> x <= y * z) *)
2982Theorem REAL_LE_LDIV_EQ_NEG :
2983 !x y z. z < (0 :real) ==> (x <= y / z <=> y <= x * z)
2984Proof
2985 RW_TAC real_ss []
2986 >> `0 < -z` by RW_TAC real_ss [REAL_NEG_GT0]
2987 >> `z <> 0` by (METIS_TAC [REAL_LT_IMP_NE])
2988 >> EQ_TAC
2989 >- (RW_TAC real_ss [] \\
2990 `x * (-z) <= y / z * (-z)` by METIS_TAC [GSYM REAL_LE_RMUL] \\
2991 FULL_SIMP_TAC real_ss [] \\
2992 METIS_TAC [REAL_DIV_RMUL, REAL_LE_NEG])
2993 >> RW_TAC real_ss []
2994 >> `x * (-z) <= -y` by FULL_SIMP_TAC real_ss [REAL_LE_NEG]
2995 >> `x <= -y * inv (-z)` by METIS_TAC [GSYM REAL_LE_RDIV_EQ, real_div]
2996 >> METIS_TAC [REAL_NEG_INV, REAL_NEG_MUL2, GSYM real_div]
2997QED
2998
2999Theorem POW_POS_EVEN: !x:real. x < 0 ==> ((0 < x pow n) <=> (EVEN n))
3000Proof
3001 Induct_on `n`
3002 >- RW_TAC std_ss [pow,REAL_LT_01,EVEN]
3003 >> RW_TAC std_ss [pow,EVEN]
3004 >> EQ_TAC
3005 >- METIS_TAC [REAL_LT_ANTISYM, REAL_LT_RMUL_0_NEG, REAL_MUL_COMM]
3006 >> RW_TAC std_ss []
3007 >> `x pow n <= 0` by METIS_TAC [real_lt]
3008 >> `x pow n <> 0` by METIS_TAC [POW_NZ, REAL_LT_IMP_NE]
3009 >> `x pow n < 0` by METIS_TAC [REAL_LT_LE]
3010 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_MUL2, REAL_LT_MUL]
3011QED
3012
3013Theorem POW_NEG_ODD: !x:real. x < 0 ==> ((x pow n < 0) <=> (ODD n))
3014Proof
3015 Induct_on `n`
3016 >- RW_TAC std_ss [pow,GSYM real_lte,REAL_LE_01]
3017 >> RW_TAC std_ss [pow,ODD]
3018 >> EQ_TAC
3019 >- METIS_TAC [REAL_LT_RMUL_NEG_0_NEG, REAL_MUL_COMM, REAL_LT_ANTISYM]
3020 >> RW_TAC std_ss []
3021 >> `0 <= x pow n` by METIS_TAC [real_lt]
3022 >> `x pow n <> 0` by METIS_TAC [POW_NZ, REAL_LT_IMP_NE]
3023 >> `0 < x pow n` by METIS_TAC [REAL_LT_LE]
3024 >> METIS_TAC [REAL_NEG_GT0, REAL_MUL_LNEG, REAL_LT_MUL]
3025QED
3026
3027Theorem REAL_MAX_REDUCE :
3028 !x y :real. x <= y \/ x < y ==> (max x y = y) /\ (max y x = y)
3029Proof
3030 PROVE_TAC [REAL_LT_IMP_LE, REAL_MAX_ACI, max_def]
3031QED
3032
3033Theorem REAL_MIN_REDUCE :
3034 !x y :real. x <= y \/ x < y ==> (min x y = x) /\ (min y x = x)
3035Proof
3036 PROVE_TAC [REAL_LT_IMP_LE, REAL_MIN_ACI, min_def]
3037QED
3038
3039Theorem REAL_LT_MAX_BETWEEN :
3040 !x b d :real. x < max b d /\ b <= x ==> x < d
3041Proof
3042 RW_TAC std_ss [max_def]
3043 >> fs [real_lte]
3044QED
3045
3046Theorem REAL_MIN_LE_BETWEEN :
3047 !x a c :real. min a c <= x /\ x < a ==> c <= x
3048Proof
3049 RW_TAC std_ss [min_def]
3050 >> PROVE_TAC [REAL_LET_ANTISYM]
3051QED
3052
3053Theorem REAL_ARCH_INV_SUC : (* was: reals_Archimedean *)
3054 !x:real. 0 < x ==> ?n. inv &(SUC n) < x
3055Proof
3056 RW_TAC real_ss [REAL_INV_1OVER] THEN SIMP_TAC real_ss [REAL_LT_LDIV_EQ] THEN
3057 ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN
3058 ASM_SIMP_TAC real_ss [GSYM REAL_LT_LDIV_EQ] THEN
3059 MP_TAC (ISPEC ``1 / x:real`` SIMP_REAL_ARCH) THEN STRIP_TAC THEN
3060 Q.EXISTS_TAC `n` THEN FULL_SIMP_TAC real_ss [real_div] THEN
3061 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [GSYM REAL_LT_INV_EQ]) THEN
3062 REWRITE_TAC [ADD1, GSYM add_ints] THEN REAL_ASM_ARITH_TAC
3063QED
3064
3065Theorem REAL_ARCH_INV' : (* was: ex_inverse_of_nat_less *)
3066 !x:real. 0 < x ==> ?n. inv (&n) < x
3067Proof
3068 RW_TAC std_ss [] THEN FIRST_ASSUM (MP_TAC o MATCH_MP REAL_ARCH_INV_SUC) THEN
3069 METIS_TAC []
3070QED
3071
3072Theorem REAL_LE_MUL_NEG : (* was: REAL_LE_MUL' *)
3073 !x y. x <= 0 /\ y <= 0 ==> 0 <= x * y
3074Proof
3075 rpt STRIP_TAC
3076 >> MP_TAC (Q.SPECL [‘-x’, ‘-y’] REAL_LE_MUL)
3077 >> REWRITE_TAC [GSYM REAL_NEG_LE0, REAL_NEGNEG, REAL_NEG_MUL2]
3078 >> DISCH_THEN MATCH_MP_TAC
3079 >> ASM_REWRITE_TAC []
3080QED
3081
3082Theorem REAL_LT_MUL_NEG : (* was: REAL_LT_MUL' *)
3083 !x y. x < 0 /\ y < 0 ==> 0 < x * y
3084Proof
3085 rpt STRIP_TAC
3086 >> MP_TAC (Q.SPECL [‘-x’, ‘-y’] REAL_LT_MUL)
3087 >> REWRITE_TAC [GSYM REAL_NEG_LT0, REAL_NEGNEG, REAL_NEG_MUL2]
3088 >> DISCH_THEN MATCH_MP_TAC
3089 >> ASM_REWRITE_TAC []
3090QED
3091
3092Theorem REAL_LT_LMUL_NEG : (* was: REAL_LT_LMUL' *)
3093 !x y z. x < 0 ==> (x * y < x * z <=> z < y)
3094Proof
3095 rpt STRIP_TAC
3096 >> MP_TAC (Q.SPECL [‘-x’, ‘z’, ‘y’] REAL_LT_LMUL)
3097 >> ‘0 < -x’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEGNEG]
3098 >> rw [GSYM REAL_NEG_RMUL, REAL_LT_NEG]
3099QED
3100
3101Theorem REAL_LT_RMUL_NEG : (* was: REAL_LT_RMUL' *)
3102 !x y z. z < 0 ==> (x * z < y * z <=> y < x)
3103Proof
3104 rpt STRIP_TAC
3105 >> MP_TAC (Q.SPECL [‘y’, ‘x’, ‘-z’] REAL_LT_RMUL)
3106 >> ‘0 < -z’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEGNEG]
3107 >> rw [GSYM REAL_NEG_RMUL, REAL_LT_NEG]
3108QED
3109
3110Theorem REAL_LT_LDIV_CANCEL :
3111 !x y (z :real). 0 < x /\ 0 < y /\ 0 < z ==> (z / x < z / y <=> y < x)
3112Proof
3113 RW_TAC bool_ss [real_div, REAL_LT_LMUL]
3114 >> MATCH_MP_TAC REAL_INV_LT_ANTIMONO
3115 >> ASM_REWRITE_TAC []
3116QED
3117
3118Theorem REAL_LE_LDIV_CANCEL :
3119 !x y (z :real). 0 < x /\ 0 < y /\ 0 < z ==> (z / x <= z / y <=> y <= x)
3120Proof
3121 RW_TAC bool_ss [real_div, REAL_LE_LMUL]
3122 >> MATCH_MP_TAC REAL_INV_LE_ANTIMONO
3123 >> ASM_REWRITE_TAC []
3124QED
3125
3126(* moved here from extrealTheory *)
3127Theorem ABS_LE_HALF_POW2 :
3128 !x y :real. abs (x * y) <= 1/2 * (x pow 2 + y pow 2)
3129Proof
3130 rpt GEN_TAC
3131 >> Cases_on `0 <= x * y`
3132 >- (ASM_SIMP_TAC real_ss [abs] \\
3133 Know `x * y = (1 / 2) * 2 * x * y`
3134 >- (Suff `1 / 2 * 2 = 1r`
3135 >- (Rewr' >> REWRITE_TAC [GSYM REAL_MUL_ASSOC, REAL_MUL_LID]) \\
3136 MATCH_MP_TAC REAL_DIV_RMUL >> SIMP_TAC real_ss []) >> Rewr' \\
3137 REWRITE_TAC [GSYM REAL_MUL_ASSOC] \\
3138 MATCH_MP_TAC REAL_LE_MUL2 >> SIMP_TAC real_ss [REAL_LE_REFL] \\
3139 CONJ_TAC >- (MATCH_MP_TAC REAL_LT_LE_MUL >> ASM_SIMP_TAC real_ss []) \\
3140 ONCE_REWRITE_TAC [GSYM REAL_SUB_LE] \\
3141 Suff `x pow 2 + y pow 2 - 2 * (x * y) = (x - y) pow 2`
3142 >- (Rewr' >> REWRITE_TAC [REAL_LE_POW2]) \\
3143 SIMP_TAC real_ss [REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_ADD_LDISTRIB,
3144 REAL_ADD_RDISTRIB, REAL_ADD_ASSOC, POW_2,
3145 GSYM REAL_DOUBLE] \\
3146 REAL_ARITH_TAC)
3147 >> ASM_SIMP_TAC real_ss [abs]
3148 >> fs [GSYM real_lt]
3149 >> REWRITE_TAC [Once (GSYM REAL_SUB_LE), REAL_SUB_RNEG, REAL_MUL_RNEG]
3150 >> Suff `x pow 2 + y pow 2 - -2 * (x * y) = (x + y) pow 2`
3151 >- (Rewr' >> REWRITE_TAC [REAL_LE_POW2])
3152 >> SIMP_TAC real_ss [REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_ADD_LDISTRIB,
3153 REAL_ADD_RDISTRIB, REAL_ADD_ASSOC, POW_2,
3154 GSYM REAL_DOUBLE]
3155 >> REAL_ARITH_TAC
3156QED
3157
3158(* moved here from extrealTheory *)
3159Theorem REAL_LE_MUL_EPSILON :
3160 !x y:real. (!z. 0 < z /\ z < 1 ==> z * x <= y) ==> x <= y
3161Proof
3162 rpt STRIP_TAC
3163 >> Cases_on `x = 0`
3164 >- (Q.PAT_X_ASSUM `!z. P z` (MP_TAC o Q.SPEC `1/2`)
3165 >> RW_TAC real_ss [REAL_HALF_BETWEEN])
3166 >> Cases_on `0 < x`
3167 >- (MATCH_MP_TAC REAL_LE_EPSILON \\
3168 RW_TAC std_ss [GSYM REAL_LE_SUB_RADD] \\
3169 Cases_on `e < x`
3170 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3171 Q.EXISTS_TAC `(1 - e/x) * x` \\
3172 CONJ_TAC
3173 >- (RW_TAC real_ss [REAL_SUB_RDISTRIB] \\
3174 METIS_TAC [REAL_DIV_RMUL, REAL_LE_REFL]) \\
3175 Q.PAT_X_ASSUM `!z. P z` MATCH_MP_TAC \\
3176 RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_DIV, REAL_LT_SUB_LADD,
3177 REAL_LT_1, REAL_LT_IMP_LE]) \\
3178 FULL_SIMP_TAC std_ss [REAL_NOT_LT] \\
3179 MATCH_MP_TAC REAL_LE_TRANS \\
3180 Q.EXISTS_TAC `0` \\
3181 RW_TAC real_ss [REAL_LE_SUB_RADD] \\
3182 MATCH_MP_TAC REAL_LE_TRANS \\
3183 Q.EXISTS_TAC `(1 / 2) * x` \\
3184 RW_TAC real_ss [REAL_LE_MUL, REAL_LT_IMP_LE])
3185 >> MATCH_MP_TAC REAL_LE_TRANS
3186 >> Q.EXISTS_TAC `(1/2)*x`
3187 >> RW_TAC real_ss []
3188 >> RW_TAC std_ss [Once (GSYM REAL_LE_NEG), GSYM REAL_MUL_RNEG]
3189 >> Suff `1/2 * ~x <= 1 * ~x` >- RW_TAC real_ss []
3190 >> METIS_TAC [REAL_NEG_GT0, REAL_LT_TOTAL, REAL_LE_REFL, REAL_HALF_BETWEEN, REAL_LE_RMUL]
3191QED
3192
3193Theorem SUM_PERMUTE :
3194 !f p s. p permutes s ==> (sum s f = sum s (f o p))
3195Proof
3196 REWRITE_TAC[sum_def] THEN MATCH_MP_TAC ITERATE_PERMUTE THEN
3197 REWRITE_TAC[MONOIDAL_REAL_ADD]
3198QED
3199
3200Theorem SUM_PERMUTE_COUNT :
3201 !f p n. p permutes (count n) ==> (sum (count n) f = sum (count n) (f o p))
3202Proof
3203 PROVE_TAC[SUM_PERMUTE, FINITE_COUNT]
3204QED
3205
3206Theorem SUM_PERMUTE_NUMSEG :
3207 !f p m n.
3208 p permutes (count n DIFF count m) ==>
3209 (sum (count n DIFF count m) f = sum (count n DIFF count m) (f o p))
3210Proof
3211 PROVE_TAC[SUM_PERMUTE, FINITE_COUNT, FINITE_DIFF]
3212QED
3213
3214Theorem PRODUCT_PERMUTE :
3215 !f p s. p permutes s ==> (product s f = product s (f o p))
3216Proof
3217 REWRITE_TAC[product] THEN MATCH_MP_TAC ITERATE_PERMUTE THEN
3218 REWRITE_TAC[MONOIDAL_REAL_MUL]
3219QED
3220
3221Theorem PRODUCT_PERMUTE_COUNT :
3222 !f p n.
3223 p permutes (count n) ==> (product (count n) f = product (count n) (f o p))
3224Proof
3225 PROVE_TAC[PRODUCT_PERMUTE, FINITE_COUNT]
3226QED
3227
3228Theorem PRODUCT_PERMUTE_NUMSEG :
3229 !f p m n.
3230 p permutes (count n DIFF count m) ==>
3231 (product (count n DIFF count m) f = product (count n DIFF count m) (f o p))
3232Proof
3233 PROVE_TAC[PRODUCT_PERMUTE, FINITE_COUNT, FINITE_DIFF]
3234QED
3235
3236Theorem PERMUTES_IN_NUMSEG :
3237 !p n i. p permutes {1 .. n} /\ i IN {1 .. n} ==> 1 <= p(i) /\ p(i) <= n
3238Proof
3239 REWRITE_TAC[permutes, IN_NUMSEG] THEN PROVE_TAC[]
3240QED
3241
3242Theorem SUM_PERMUTATIONS_INVERSE :
3243 !f n. sum {p | p permutes count n } f =
3244 sum {p | p permutes count n } (\p. f(inverse p))
3245Proof
3246 REPEAT GEN_TAC THEN
3247 GEN_REWRITE_TAC (funpow 2 LAND_CONV) empty_rewrites
3248 [GSYM IMAGE_INVERSE_PERMUTATIONS] THEN
3249 SIMP_TAC bool_ss
3250 [Once (Q.prove(`{f x | p x} = IMAGE f {x | p x}`,
3251 REWRITE_TAC[EXTENSION, IN_IMAGE] THEN
3252 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[]))] THEN
3253 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
3254 [GSYM o_DEF] THEN
3255 MATCH_MP_TAC SUM_IMAGE THEN
3256 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
3257 PROVE_TAC[PERMUTES_INVERSE_INVERSE]
3258QED
3259
3260Theorem SUM_PERMUTATIONS_COMPOSE_L :
3261 !f s q. q permutes s ==>
3262 sum {p | p permutes s} f =
3263 sum {p | p permutes s} (\p. f(q o p))
3264Proof
3265 REPEAT STRIP_TAC THEN
3266 FIRST_ASSUM(fn th => GEN_REWRITE_TAC (funpow 2 LAND_CONV) empty_rewrites
3267 [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_L th)]) THEN
3268 SIMP_TAC bool_ss
3269 [Once (Q.prove(`{f x | p x} = IMAGE f {x | p x}`,
3270 REWRITE_TAC[EXTENSION, IN_IMAGE] THEN
3271 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[]))] THEN
3272 REWRITE_TAC[GSYM o_DEF, ETA_THM] THEN
3273 MATCH_MP_TAC SUM_IMAGE THEN
3274 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
3275 REPEAT STRIP_TAC THEN
3276 FIRST_X_ASSUM(MP_TAC o AP_TERM ``\p:'a-> 'a. inverse(q:'a-> 'a) o p``) THEN
3277 BETA_TAC THEN REWRITE_TAC[o_ASSOC] THEN
3278 EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
3279 REWRITE_TAC[I_o_ID]
3280QED
3281
3282Theorem SUM_PERMUTATIONS_COMPOSE_L_COUNT :
3283 !f n q. q permutes count n ==>
3284 sum {p | p permutes count n} f =
3285 sum {p | p permutes count n} (\p. f(q o p))
3286Proof
3287 REWRITE_TAC[SUM_PERMUTATIONS_COMPOSE_L]
3288QED
3289
3290Theorem SUM_PERMUTATIONS_COMPOSE_L_NUMSEG :
3291 !f m n q.
3292 q permutes (count n DIFF count m)
3293 ==> sum {p | p permutes (count n DIFF count m)} f =
3294 sum {p | p permutes (count n DIFF count m)} (\p. f(q o p))
3295Proof
3296 REPEAT STRIP_TAC THEN
3297 FIRST_ASSUM(fn th => GEN_REWRITE_TAC (funpow 2 LAND_CONV) empty_rewrites
3298 [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_L th)]) THEN
3299 SIMP_TAC bool_ss
3300 [Once (Q.prove(`{f x | p x} = IMAGE f {x | p x}`,
3301 REWRITE_TAC[EXTENSION, IN_IMAGE] THEN
3302 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[]))] THEN
3303 REWRITE_TAC[GSYM o_DEF, ETA_THM] THEN
3304 MATCH_MP_TAC SUM_IMAGE THEN
3305 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
3306 REPEAT STRIP_TAC THEN
3307 FIRST_X_ASSUM(MP_TAC o AP_TERM “\p:num-> num. inverse(q:num-> num) o p”) THEN
3308 BETA_TAC THEN REWRITE_TAC[o_ASSOC] THEN
3309 EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
3310 REWRITE_TAC[I_o_ID]
3311QED
3312
3313Theorem SUM_PERMUTATIONS_COMPOSE_R :
3314 !f s q.
3315 q permutes s
3316 ==> sum {p | p permutes s} f =
3317 sum {p | p permutes s} (\p. f(p o q))
3318Proof
3319 REPEAT STRIP_TAC THEN
3320 FIRST_ASSUM(fn th => GEN_REWRITE_TAC (funpow 2 LAND_CONV) empty_rewrites
3321 [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_R th)]) THEN
3322 SIMP_TAC bool_ss
3323 [Once (Q.prove(`{f x | p x} = IMAGE f {x | p x}`,
3324 REWRITE_TAC[EXTENSION, IN_IMAGE] THEN
3325 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[]))] THEN
3326 SIMP_TAC bool_ss[GSYM o_ABS_R] THEN
3327 MATCH_MP_TAC SUM_IMAGE THEN
3328 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
3329 REPEAT STRIP_TAC THEN
3330 FIRST_X_ASSUM(MP_TAC o AP_TERM ``\p:'a-> 'a. p o inverse(q:'a-> 'a)``) THEN
3331 BETA_TAC THEN REWRITE_TAC[GSYM o_ASSOC] THEN
3332 EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
3333 REWRITE_TAC[I_o_ID]
3334QED
3335
3336Theorem SUM_PERMUTATIONS_COMPOSE_R_COUNT :
3337 !f n q.
3338 q permutes count n
3339 ==> sum {p | p permutes count n} f =
3340 sum {p | p permutes count n} (\p. f(p o q))
3341Proof
3342 REWRITE_TAC[SUM_PERMUTATIONS_COMPOSE_R]
3343QED
3344
3345Theorem SUM_PERMUTATIONS_COMPOSE_R_NUMSEG :
3346 !f m n q.
3347 q permutes (count n DIFF count m)
3348 ==> sum {p | p permutes (count n DIFF count m)} f =
3349 sum {p | p permutes (count n DIFF count m)} (\p. f(p o q))
3350Proof
3351 REPEAT STRIP_TAC THEN
3352 FIRST_ASSUM(fn th => GEN_REWRITE_TAC (funpow 2 LAND_CONV) empty_rewrites
3353 [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_R th)]) THEN
3354 SIMP_TAC bool_ss
3355 [Once (Q.prove(`{f x | p x} = IMAGE f {x | p x}`,
3356 REWRITE_TAC[EXTENSION, IN_IMAGE] THEN
3357 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[]))] THEN
3358 SIMP_TAC bool_ss[GSYM o_ABS_R] THEN
3359 MATCH_MP_TAC SUM_IMAGE THEN
3360 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
3361 REPEAT STRIP_TAC THEN
3362 FIRST_X_ASSUM(MP_TAC o AP_TERM “\p:num-> num. p o inverse(q:num-> num)”) THEN
3363 BETA_TAC THEN REWRITE_TAC[GSYM o_ASSOC] THEN
3364 EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
3365 REWRITE_TAC[I_o_ID]
3366QED
3367
3368(* ----------------------------------------------------------------------
3369 REAL_SUM_IMAGE
3370
3371 This constant is the same as standard mathematics \Sigma operator:
3372
3373 \Sigma_{x\in P}{f(x)} = SUM_IMAGE f P
3374
3375 Where f's range is the real numbers and P is finite.
3376 ---------------------------------------------------------------------- *)
3377
3378Definition REAL_SUM_IMAGE_DEF :
3379 REAL_SUM_IMAGE f s = ITSET (\e acc. f e + acc) s (0:real)
3380End
3381
3382Overload SIGMA = “REAL_SUM_IMAGE”
3383
3384Theorem REAL_SUM_IMAGE_EMPTY[simp]:
3385 !f. REAL_SUM_IMAGE f EMPTY = 0
3386Proof
3387 simp[REAL_SUM_IMAGE_DEF]
3388QED
3389
3390Theorem REAL_SUM_IMAGE_THM :
3391 !f. (REAL_SUM_IMAGE f {} = 0) /\
3392 (!e s. FINITE s ==>
3393 (REAL_SUM_IMAGE f (e INSERT s) =
3394 f e + REAL_SUM_IMAGE f (s DELETE e)))
3395Proof
3396 REPEAT STRIP_TAC
3397 >- SIMP_TAC (srw_ss()) [ITSET_THM, REAL_SUM_IMAGE_DEF]
3398 >> SIMP_TAC (srw_ss()) [REAL_SUM_IMAGE_DEF]
3399 >> Q.ABBREV_TAC `g = \e acc. f e + acc`
3400 >> Suff `ITSET g (e INSERT s) 0 =
3401 g e (ITSET g (s DELETE e) 0)`
3402 >- (Q.UNABBREV_TAC `g` >> SRW_TAC [] [])
3403 >> MATCH_MP_TAC COMMUTING_ITSET_RECURSES
3404 >> Q.UNABBREV_TAC `g`
3405 >> RW_TAC real_ss []
3406 >> REAL_ARITH_TAC
3407QED
3408
3409(* An equivalent theorem linking REAL_SUM_IMAGE and Sum *)
3410Theorem REAL_SUM_IMAGE_sum :
3411 !f s. FINITE s ==> REAL_SUM_IMAGE f s = Sum s f
3412Proof
3413 Q.X_GEN_TAC ‘f’
3414 >> HO_MATCH_MP_TAC FINITE_INDUCT
3415 >> CONJ_TAC >- rw [REAL_SUM_IMAGE_THM, SUM_CLAUSES]
3416 >> rpt STRIP_TAC
3417 >> ‘s DELETE e = s’ by METIS_TAC [DELETE_NON_ELEMENT]
3418 >> rw [REAL_SUM_IMAGE_THM, SUM_CLAUSES]
3419QED
3420
3421(* it translates a sum theorem into a SIGMA theorem *)
3422fun translate th = SIMP_RULE std_ss [GSYM REAL_SUM_IMAGE_sum] th;
3423
3424Theorem REAL_SUM_IMAGE_SING[simp] :
3425 !f e. REAL_SUM_IMAGE f {e} = f e
3426Proof
3427 SRW_TAC [][REAL_SUM_IMAGE_THM]
3428QED
3429
3430Theorem REAL_SUM_IMAGE_POS :
3431 !f s. FINITE s /\ (!x. x IN s ==> 0 <= f x) ==>
3432 0 <= REAL_SUM_IMAGE f s
3433Proof
3434 rw [REAL_SUM_IMAGE_sum, SUM_POS_LE]
3435QED
3436
3437Theorem REAL_SUM_IMAGE_SPOS :
3438 !s. FINITE s /\ (~(s = {})) ==>
3439 !f. (!x. x IN s ==> 0 < f x) ==>
3440 0 < REAL_SUM_IMAGE f s
3441Proof
3442 rw [REAL_SUM_IMAGE_sum]
3443 >> MATCH_MP_TAC SUM_POS_LT >> art []
3444 >> CONJ_TAC >- METIS_TAC [REAL_LT_IMP_LE]
3445 >> fs [GSYM MEMBER_NOT_EMPTY]
3446 >> Q.EXISTS_TAC ‘x’ >> rw []
3447QED
3448
3449(* ‘?x. x IN P’ already indicates ‘P <> {}’, thus the actual conclusion is just
3450 ‘SIGMA f P <> 0’
3451 *)
3452Theorem REAL_SUM_IMAGE_NONZERO :
3453 !P. FINITE P ==>
3454 !f. (!x. x IN P ==> 0 <= f x) /\ (?x. x IN P /\ ~(f x = 0)) ==>
3455 ((~(REAL_SUM_IMAGE f P = 0)) <=> (~(P = {})))
3456Proof
3457 rw [REAL_SUM_IMAGE_sum]
3458 >> ‘P <> {}’ by METIS_TAC [MEMBER_NOT_EMPTY]
3459 >> rw []
3460 >> Suff ‘0 < sum P f’ >- METIS_TAC [REAL_LT_IMP_NE]
3461 >> ‘0 < f x’ by METIS_TAC [REAL_LE_LT]
3462 >> MATCH_MP_TAC SUM_POS_LT >> rw []
3463 >> Q.EXISTS_TAC ‘x’ >> art []
3464QED
3465
3466(* |- !f s.
3467 FINITE s /\ (!x. x IN s ==> 0 <= f x) /\ (?x. x IN s /\ 0 < f x) ==>
3468 0 < SIGMA f s
3469 *)
3470Theorem REAL_SUM_IMAGE_POS_LT = translate SUM_POS_LT
3471
3472Theorem REAL_SUM_IMAGE_IF_ELIM_lem[local]:
3473 !s. FINITE s ==>
3474 (\s. !P f. (!x. x IN s ==> P x) ==>
3475 (REAL_SUM_IMAGE (\x. if P x then f x else 0) s =
3476 REAL_SUM_IMAGE f s)) s
3477Proof
3478 MATCH_MP_TAC FINITE_INDUCT
3479 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IN_INSERT, DELETE_NON_ELEMENT]
3480QED
3481
3482Theorem REAL_SUM_IMAGE_IF_ELIM:
3483 !s P f. FINITE s /\ (!x. x IN s ==> P x) ==>
3484 (REAL_SUM_IMAGE (\x. if P x then f x else 0) s =
3485 REAL_SUM_IMAGE f s)
3486Proof
3487 METIS_TAC [REAL_SUM_IMAGE_IF_ELIM_lem]
3488QED
3489
3490Theorem REAL_SUM_IMAGE_FINITE_SAME_lem[local]:
3491 !P. FINITE P ==>
3492 (\P. !f p.
3493 p IN P /\ (!q. q IN P ==> (f p = f q)) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * f p)) P
3494Proof
3495 MATCH_MP_TAC FINITE_INDUCT
3496 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY, DELETE_NON_ELEMENT]
3497 >> `f p = f e` by FULL_SIMP_TAC std_ss [IN_INSERT]
3498 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] >> POP_ASSUM (K ALL_TAC)
3499 >> RW_TAC real_ss [CARD_INSERT, ADD1]
3500 >> ONCE_REWRITE_TAC [GSYM REAL_ADD]
3501 >> RW_TAC real_ss [REAL_ADD_RDISTRIB]
3502 >> Suff `REAL_SUM_IMAGE f s = & (CARD s) * f e`
3503 >- RW_TAC real_ss [REAL_ADD_COMM]
3504 >> (MP_TAC o Q.SPECL [`s`]) SET_CASES >> RW_TAC std_ss []
3505 >- RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY]
3506 >> `f e = f x` by FULL_SIMP_TAC std_ss [IN_INSERT]
3507 >> FULL_SIMP_TAC std_ss [] >> POP_ASSUM (K ALL_TAC)
3508 >> Q.PAT_ASSUM `!f p. b` MATCH_MP_TAC >> METIS_TAC [IN_INSERT]
3509QED
3510
3511Theorem REAL_SUM_IMAGE_FINITE_SAME:
3512 !P. FINITE P ==>
3513 !f p.
3514 p IN P /\ (!q. q IN P ==> (f p = f q)) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * f p)
3515Proof
3516 MP_TAC REAL_SUM_IMAGE_FINITE_SAME_lem >> RW_TAC std_ss []
3517QED
3518
3519Theorem REAL_SUM_IMAGE_FINITE_CONST:
3520 !P. FINITE P ==>
3521 !f x. (!y. f y = x) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * x)
3522Proof
3523 REPEAT STRIP_TAC
3524 >> (MP_TAC o Q.SPECL [`P`]) REAL_SUM_IMAGE_FINITE_SAME
3525 >> RW_TAC std_ss []
3526 >> POP_ASSUM (MP_TAC o (Q.SPECL [`f`]))
3527 >> RW_TAC std_ss []
3528 >> (MP_TAC o Q.SPECL [`P`]) SET_CASES
3529 >> RW_TAC std_ss [] >- RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY]
3530 >> POP_ASSUM (K ALL_TAC)
3531 >> POP_ASSUM MATCH_MP_TAC
3532 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss [IN_INSERT]
3533QED
3534
3535Theorem REAL_SUM_IMAGE_FINITE_CONST2:
3536 !P. FINITE P ==>
3537 !f x. (!y. y IN P ==> (f y = x)) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * x)
3538Proof
3539 REPEAT STRIP_TAC
3540 >> (MP_TAC o Q.SPECL [`P`]) REAL_SUM_IMAGE_FINITE_SAME
3541 >> RW_TAC std_ss []
3542 >> POP_ASSUM (MP_TAC o (Q.SPECL [`f`]))
3543 >> RW_TAC std_ss []
3544 >> (MP_TAC o Q.SPECL [`P`]) SET_CASES
3545 >> RW_TAC std_ss [] >- RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY]
3546 >> POP_ASSUM (K ALL_TAC)
3547 >> POP_ASSUM MATCH_MP_TAC
3548 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss [IN_INSERT]
3549QED
3550
3551Theorem REAL_SUM_IMAGE_FINITE_CONST3 :
3552 !P. FINITE P ==>
3553 !c. (REAL_SUM_IMAGE (\x. c) P = (&(CARD P)) * c)
3554Proof
3555 rw [REAL_SUM_IMAGE_sum, SUM_CONST]
3556QED
3557
3558Theorem REAL_SUM_IMAGE_IN_IF_lem[local]:
3559 !P. FINITE P ==>
3560 (\P.!f. REAL_SUM_IMAGE f P = REAL_SUM_IMAGE (\x. if x IN P then f x else 0) P) P
3561Proof
3562 MATCH_MP_TAC FINITE_INDUCT
3563 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM]
3564 >> POP_ASSUM MP_TAC
3565 >> ONCE_REWRITE_TAC [DELETE_NON_ELEMENT]
3566 >> SIMP_TAC real_ss [IN_INSERT]
3567 >> `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then f x else 0)) s =
3568 REAL_SUM_IMAGE (\x. (if x IN s then f x else 0)) s`
3569 by (POP_ASSUM (MP_TAC o Q.SPECL [`(\x. (if (x = e) \/ x IN s then f x else 0))`])
3570 >> RW_TAC std_ss [])
3571 >> POP_ORW
3572 >> POP_ASSUM (MP_TAC o Q.SPECL [`f`])
3573 >> RW_TAC real_ss []
3574QED
3575
3576Theorem REAL_SUM_IMAGE_IN_IF:
3577 !P. FINITE P ==>
3578 !f. REAL_SUM_IMAGE f P = REAL_SUM_IMAGE (\x. if x IN P then f x else 0) P
3579Proof
3580 METIS_TAC [REAL_SUM_IMAGE_IN_IF_lem]
3581QED
3582
3583Theorem REAL_SUM_IMAGE_CMUL :
3584 !P. FINITE P ==>
3585 !f c. (REAL_SUM_IMAGE (\x. c * f x) P = c * (REAL_SUM_IMAGE f P))
3586Proof
3587 rw [REAL_SUM_IMAGE_sum, SUM_LMUL]
3588QED
3589
3590Theorem REAL_SUM_IMAGE_NEG :
3591 !P. FINITE P ==>
3592 !f. (REAL_SUM_IMAGE (\x. ~ f x) P = ~ (REAL_SUM_IMAGE f P))
3593Proof
3594 rw [REAL_SUM_IMAGE_sum, SUM_NEG']
3595QED
3596
3597Theorem REAL_SUM_IMAGE_IMAGE :
3598 !P. FINITE P ==>
3599 !f'. INJ f' P (IMAGE f' P) ==>
3600 !f. REAL_SUM_IMAGE f (IMAGE f' P) = REAL_SUM_IMAGE (f o f') P
3601Proof
3602 rw [REAL_SUM_IMAGE_sum, INJ_DEF]
3603 >> MATCH_MP_TAC SUM_IMAGE >> rw []
3604QED
3605
3606Theorem REAL_SUM_IMAGE_DISJOINT_UNION :
3607 !P P'. FINITE P /\ FINITE P' /\ DISJOINT P P' ==>
3608 (!f. REAL_SUM_IMAGE f (P UNION P') =
3609 REAL_SUM_IMAGE f P +
3610 REAL_SUM_IMAGE f P')
3611Proof
3612 rw [REAL_SUM_IMAGE_sum]
3613 >> MATCH_MP_TAC SUM_UNION
3614 >> rw [GSYM DISJOINT_DEF, FINITE_UNION]
3615QED
3616
3617Theorem REAL_SUM_IMAGE_EQ_CARD_lem[local]:
3618 !P. FINITE P ==>
3619 (\P. REAL_SUM_IMAGE (\x. if x IN P then 1 else 0) P = (&(CARD P))) P
3620Proof
3621 MATCH_MP_TAC FINITE_INDUCT
3622 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY, IN_INSERT]
3623 >> (MP_TAC o Q.SPECL [`s`]) CARD_INSERT
3624 >> RW_TAC real_ss [ADD1] >> ONCE_REWRITE_TAC [GSYM REAL_ADD]
3625 >> Suff `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then 1 else 0)) (s DELETE e) =
3626 REAL_SUM_IMAGE (\x. (if x IN s then 1 else 0)) s`
3627 >- RW_TAC real_ss []
3628 >> Q.PAT_ASSUM `REAL_SUM_IMAGE (\x. (if x IN s then 1 else 0)) s = & (CARD s)` (K ALL_TAC)
3629 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]
3630 >> `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then 1 else 0)) s =
3631 REAL_SUM_IMAGE (\x. if x IN s then (\x. (if (x = e) \/ x IN s then 1 else 0)) x else 0) s`
3632 by (METIS_TAC [REAL_SUM_IMAGE_IN_IF])
3633 >> RW_TAC std_ss []
3634QED
3635
3636Theorem REAL_SUM_IMAGE_EQ_CARD:
3637 !P. FINITE P ==>
3638 (REAL_SUM_IMAGE (\x. if x IN P then 1 else 0) P = (&(CARD P)))
3639Proof
3640 METIS_TAC [REAL_SUM_IMAGE_EQ_CARD_lem]
3641QED
3642
3643Theorem REAL_SUM_IMAGE_INV_CARD_EQ_1:
3644 !P. (~(P = {})) /\ FINITE P ==>
3645 (REAL_SUM_IMAGE (\s. if s IN P then inv (& (CARD P)) else 0) P = 1)
3646Proof
3647 REPEAT STRIP_TAC
3648 >> `(\s. if s IN P then inv (& (CARD P)) else 0) = (\s. inv (& (CARD P)) * (\s. if s IN P then 1 else 0) s)`
3649 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [])
3650 >> POP_ORW
3651 >> `REAL_SUM_IMAGE (\s. inv (& (CARD P)) * (\s. (if s IN P then 1 else 0)) s) P =
3652 (inv (& (CARD P))) * (REAL_SUM_IMAGE (\s. (if s IN P then 1 else 0)) P)`
3653 by (MATCH_MP_TAC REAL_SUM_IMAGE_CMUL >> RW_TAC std_ss [])
3654 >> POP_ORW
3655 >> `REAL_SUM_IMAGE (\s. (if s IN P then 1 else 0)) P = (&(CARD P))`
3656 by (MATCH_MP_TAC REAL_SUM_IMAGE_EQ_CARD >> RW_TAC std_ss [])
3657 >> POP_ORW
3658 >> MATCH_MP_TAC REAL_MUL_LINV
3659 >> RW_TAC real_ss []
3660 >> METIS_TAC [CARD_EQ_0]
3661QED
3662
3663Theorem REAL_SUM_IMAGE_INTER_NONZERO_lem[local]:
3664 !P. FINITE P ==>
3665 (\P. !f. REAL_SUM_IMAGE f (P INTER (\p. ~(f p = 0))) =
3666 REAL_SUM_IMAGE f P) P
3667Proof
3668 MATCH_MP_TAC FINITE_INDUCT
3669 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, INTER_EMPTY, INSERT_INTER]
3670 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]
3671 >> (RW_TAC std_ss [IN_DEF] >> RW_TAC real_ss [])
3672 >> `FINITE (s INTER (\p. ~(f p = 0)))` by (MATCH_MP_TAC INTER_FINITE >> RW_TAC std_ss [])
3673 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM]
3674 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]
3675 >> `~(e IN (s INTER (\p. ~(f p = 0))))`
3676 by RW_TAC std_ss [IN_INTER]
3677 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]
3678QED
3679
3680Theorem REAL_SUM_IMAGE_INTER_NONZERO:
3681 !P. FINITE P ==>
3682 !f. REAL_SUM_IMAGE f (P INTER (\p. ~(f p = 0))) =
3683 REAL_SUM_IMAGE f P
3684Proof
3685 METIS_TAC [REAL_SUM_IMAGE_INTER_NONZERO_lem]
3686QED
3687
3688Theorem REAL_SUM_IMAGE_INTER_ELIM_lem[local]:
3689 !P. FINITE P ==>
3690 (\P. !f P'. (!x. (~(x IN P')) ==> (f x = 0)) ==>
3691 (REAL_SUM_IMAGE f (P INTER P') =
3692 REAL_SUM_IMAGE f P)) P
3693Proof
3694 MATCH_MP_TAC FINITE_INDUCT
3695 >> RW_TAC std_ss [INTER_EMPTY, REAL_SUM_IMAGE_THM, INSERT_INTER]
3696 >> Cases_on `e IN P'`
3697 >- (`~ (e IN (s INTER P'))` by RW_TAC std_ss [IN_INTER]
3698 >> FULL_SIMP_TAC std_ss [INTER_FINITE, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT])
3699 >> FULL_SIMP_TAC real_ss []
3700 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]
3701QED
3702
3703Theorem REAL_SUM_IMAGE_INTER_ELIM:
3704 !P. FINITE P ==>
3705 !f P'. (!x. (~(x IN P')) ==> (f x = 0)) ==>
3706 (REAL_SUM_IMAGE f (P INTER P') =
3707 REAL_SUM_IMAGE f P)
3708Proof
3709 METIS_TAC [REAL_SUM_IMAGE_INTER_ELIM_lem]
3710QED
3711
3712Theorem REAL_SUM_IMAGE_COUNT:
3713 !f n. REAL_SUM_IMAGE f (pred_set$count n) =
3714 sum (0,n) f
3715Proof
3716 STRIP_TAC >> Induct
3717 >- RW_TAC std_ss [pred_setTheory.count_def, REAL_SUM_IMAGE_THM, GSPEC_F, sum]
3718 >> `pred_set$count (SUC n) = n INSERT pred_set$count n`
3719 by (RW_TAC std_ss [EXTENSION, IN_INSERT, pred_setTheory.IN_COUNT] >> DECIDE_TAC)
3720 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, sum, pred_setTheory.FINITE_COUNT]
3721 >> `pred_set$count n DELETE n = pred_set$count n`
3722 by RW_TAC arith_ss [DELETE_DEF, DIFF_DEF, IN_SING, pred_setTheory.IN_COUNT,
3723 Once EXTENSION, pred_setTheory.IN_COUNT, GSPECIFICATION,
3724 DECIDE ``!(x:num) (y:num). x < y ==> ~(x = y)``]
3725 >> RW_TAC std_ss [REAL_ADD_SYM]
3726QED
3727
3728Theorem REAL_SUM_IMAGE_MONO :
3729 !P. FINITE P ==>
3730 !f f'. (!x. x IN P ==> f x <= f' x) ==>
3731 REAL_SUM_IMAGE f P <= REAL_SUM_IMAGE f' P
3732Proof
3733 rw [REAL_SUM_IMAGE_sum]
3734 >> MATCH_MP_TAC SUM_LE' >> rw []
3735QED
3736
3737(* |- !f g s.
3738 FINITE s /\ (!x. x IN s ==> f x <= g x) /\ (?x. x IN s /\ f x < g x) ==>
3739 SIGMA f s < SIGMA g s
3740 *)
3741Theorem REAL_SUM_IMAGE_MONO_LT = translate SUM_LT'
3742
3743Theorem REAL_SUM_IMAGE_POS_MEM_LE:
3744 !P. FINITE P ==>
3745 !f. (!x. x IN P ==> 0 <= f x) ==>
3746 (!x. x IN P ==> f x <= REAL_SUM_IMAGE f P)
3747Proof
3748 Suff `!P. FINITE P ==>
3749 (\P. !f. (!x. x IN P ==> 0 <= f x) ==>
3750 (!x. x IN P ==> f x <= REAL_SUM_IMAGE f P)) P`
3751 >- PROVE_TAC []
3752 >> MATCH_MP_TAC FINITE_INDUCT
3753 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, NOT_IN_EMPTY, IN_INSERT,
3754 DISJ_IMP_THM, FORALL_AND_THM,
3755 DELETE_NON_ELEMENT]
3756 >- (Suff `f e + 0 <= f e + REAL_SUM_IMAGE f s` >- RW_TAC real_ss []
3757 >> MATCH_MP_TAC REAL_LE_LADD_IMP
3758 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS >> ASM_REWRITE_TAC [])
3759 >> Suff `0 + f x <= f e + REAL_SUM_IMAGE f s` >- RW_TAC real_ss []
3760 >> MATCH_MP_TAC REAL_LE_ADD2 >> PROVE_TAC []
3761QED
3762
3763Theorem REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD:
3764 !P. FINITE P ==>
3765 !f. (REAL_SUM_IMAGE f P = 1) /\
3766 (!x y. x IN P /\ y IN P ==> (f x = f y)) ==>
3767 (!x. x IN P ==> (f x = inv (& (CARD P))))
3768Proof
3769 Suff `!P. FINITE P ==>
3770 (\P. !f. (REAL_SUM_IMAGE f P = 1) /\
3771 (!x y. x IN P /\ y IN P ==> (f x = f y)) ==>
3772 (!x. x IN P ==> (f x = inv (& (CARD P))))) P`
3773 >- RW_TAC std_ss []
3774 >> MATCH_MP_TAC FINITE_INDUCT
3775 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IN_INSERT, DELETE_NON_ELEMENT]
3776 >- (RW_TAC std_ss [(UNDISCH o Q.SPEC `s`) CARD_INSERT]
3777 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]
3778 >> Q.PAT_ASSUM `(f:'a->real) e + REAL_SUM_IMAGE f s = 1`
3779 (MP_TAC o REWRITE_RULE [Once ((UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF)])
3780 >> `(\x:'a. (if (x IN s) then (f:'a -> real) x else (0:real))) =
3781 (\x:'a. (if (x IN s) then (\x:'a. (f:'a -> real) e) x else (0:real)))`
3782 by METIS_TAC []
3783 >> POP_ORW
3784 >> ONCE_REWRITE_TAC [(GSYM o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF]
3785 >> (MP_TAC o Q.SPECL [`(\x. (f:'a->real) e)`, `(f:'a->real) e`] o
3786 UNDISCH o Q.ISPEC `s:'a -> bool`) REAL_SUM_IMAGE_FINITE_CONST
3787 >> SIMP_TAC std_ss []
3788 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC)
3789 >> `f e + & (CARD s) * f e = f e *( & (CARD s) + 1)` by REAL_ARITH_TAC
3790 >> POP_ORW
3791 >> `1:real = &1` by RW_TAC real_ss []
3792 >> POP_ASSUM (fn thm => SIMP_TAC std_ss [thm, REAL_OF_NUM_ADD, GSYM ADD1])
3793 >> REPEAT (POP_ASSUM (K ALL_TAC))
3794 >> METIS_TAC [REAL_NZ_IMP_LT, GSYM REAL_EQ_RDIV_EQ, REAL_INV_1OVER, SUC_NOT])
3795 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]
3796 >> RW_TAC std_ss [(UNDISCH o Q.SPEC `s`) CARD_INSERT]
3797 >> Q.PAT_ASSUM `f e + REAL_SUM_IMAGE f s = 1`
3798 (MP_TAC o REWRITE_RULE [Once ((UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF)])
3799 >> `(\x:'a. (if (x IN s) then (f:'a -> real) x else (0:real))) =
3800 (\x:'a. (if (x IN s) then (\x:'a. (f:'a -> real) e) x else (0:real)))`
3801 by METIS_TAC []
3802 >> POP_ORW
3803 >> ONCE_REWRITE_TAC [(GSYM o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF]
3804 >> (MP_TAC o Q.SPECL [`(\x. (f:'a->real) e)`, `(f:'a->real) e`] o
3805 UNDISCH o Q.ISPEC `s:'a -> bool`) REAL_SUM_IMAGE_FINITE_CONST
3806 >> SIMP_TAC std_ss []
3807 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC)
3808 >> `f e + & (CARD s) * f e = f e *( & (CARD s) + 1)` by REAL_ARITH_TAC
3809 >> POP_ORW
3810 >> `1:real = &1` by RW_TAC real_ss []
3811 >> POP_ASSUM (fn thm => SIMP_TAC std_ss [thm, REAL_OF_NUM_ADD, GSYM ADD1])
3812 >> `f x = f e` by METIS_TAC [] >> POP_ORW
3813 >> REPEAT (POP_ASSUM (K ALL_TAC))
3814 >> METIS_TAC [REAL_NZ_IMP_LT, GSYM REAL_EQ_RDIV_EQ, REAL_INV_1OVER, SUC_NOT]
3815QED
3816
3817Theorem REAL_SUM_IMAGE_ADD :
3818 !s. FINITE s ==>
3819 !f f'. REAL_SUM_IMAGE (\x. f x + f' x) s =
3820 REAL_SUM_IMAGE f s + REAL_SUM_IMAGE f' s
3821Proof
3822 rw [REAL_SUM_IMAGE_sum, SUM_ADD']
3823QED
3824
3825Theorem REAL_SUM_IMAGE_REAL_SUM_IMAGE:
3826 !s s' f. FINITE s /\ FINITE s' ==>
3827 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s =
3828 REAL_SUM_IMAGE (\x. f (FST x) (SND x)) (s CROSS s'))
3829Proof
3830 Suff `!s. FINITE s ==>
3831 (\s. !s' f. FINITE s' ==>
3832 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s =
3833 REAL_SUM_IMAGE (\x. f (FST x) (SND x)) (s CROSS s'))) s`
3834 >- RW_TAC std_ss []
3835 >> MATCH_MP_TAC FINITE_INDUCT
3836 >> RW_TAC std_ss [CROSS_EMPTY, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT]
3837 >> `((e INSERT s) CROSS s') = (IMAGE (\x. (e,x)) s') UNION (s CROSS s')`
3838 by (RW_TAC std_ss [Once EXTENSION, IN_INSERT, IN_SING, IN_CROSS, IN_UNION, IN_IMAGE]
3839 >> (MP_TAC o Q.ISPEC `x:'a#'b`) pair_CASES
3840 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [FST,SND, GSYM DELETE_NON_ELEMENT]
3841 >> METIS_TAC [])
3842 >> POP_ORW
3843 >> `DISJOINT (IMAGE (\x. (e,x)) s') (s CROSS s')`
3844 by (FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT, DISJOINT_DEF, Once EXTENSION,
3845 NOT_IN_EMPTY, IN_INTER, IN_CROSS, IN_SING, IN_IMAGE]
3846 >> STRIP_TAC >> (MP_TAC o Q.ISPEC `x:'a#'b`) pair_CASES
3847 >> RW_TAC std_ss [FST, SND]
3848 >> METIS_TAC [])
3849 >> (MP_TAC o REWRITE_RULE [GSYM AND_IMP_INTRO] o
3850 Q.ISPECL [`IMAGE (\x. (e:'a,x)) (s':'b->bool)`, `(s:'a->bool) CROSS (s':'b->bool)`])
3851 REAL_SUM_IMAGE_DISJOINT_UNION
3852 >> RW_TAC std_ss [FINITE_CROSS, IMAGE_FINITE]
3853 >> POP_ASSUM (K ALL_TAC)
3854 >> (MP_TAC o Q.SPEC `(\x. (e,x))` o UNDISCH o Q.SPEC `s'` o
3855 INST_TYPE [``:'c``|->``:'a # 'b``] o INST_TYPE [``:'a``|->``:'b``] o
3856 INST_TYPE [``:'b``|->``:'c``]) REAL_SUM_IMAGE_IMAGE
3857 >> RW_TAC std_ss [INJ_DEF, IN_IMAGE, o_DEF] >> METIS_TAC []
3858QED
3859
3860Theorem REAL_SUM_IMAGE_0 :
3861 !s. FINITE s ==> (REAL_SUM_IMAGE (\x. 0) s = 0)
3862Proof
3863 rw [REAL_SUM_IMAGE_sum, SUM_0']
3864QED
3865
3866Theorem NESTED_REAL_SUM_IMAGE_REVERSE:
3867 !f s s'. FINITE s /\ FINITE s' ==>
3868 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s =
3869 REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (\y. f y x) s) s')
3870Proof
3871 RW_TAC std_ss [REAL_SUM_IMAGE_REAL_SUM_IMAGE]
3872 >> `(s' CROSS s) = IMAGE (\x. (SND x, FST x)) (s CROSS s')`
3873 by (RW_TAC std_ss [EXTENSION, IN_CROSS, IN_IMAGE]
3874 >> EQ_TAC >- (STRIP_TAC >> Q.EXISTS_TAC `(SND x, FST x)` >> RW_TAC std_ss [PAIR])
3875 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND])
3876 >> POP_ORW
3877 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS]
3878 >> `INJ (\x. (SND x,FST x)) (s CROSS s') (IMAGE (\x. (SND x,FST x)) (s CROSS s'))`
3879 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE] >- METIS_TAC []
3880 >> METIS_TAC [PAIR, PAIR_EQ])
3881 >> `REAL_SUM_IMAGE (\x. f (SND x) (FST x)) (IMAGE (\x. (SND x,FST x)) (s CROSS s')) =
3882 REAL_SUM_IMAGE ((\x. f (SND x) (FST x)) o (\x. (SND x,FST x))) (s CROSS s')`
3883 by METIS_TAC [REAL_SUM_IMAGE_IMAGE]
3884 >> POP_ORW
3885 >> RW_TAC std_ss [o_DEF]
3886QED
3887
3888Theorem REAL_SUM_IMAGE_EQ_sum: !n r. sum (0,n) r = REAL_SUM_IMAGE r (count n)
3889Proof
3890 RW_TAC std_ss []
3891 >> Induct_on `n`
3892 >- RW_TAC std_ss [sum,REAL_SUM_IMAGE_THM,COUNT_ZERO]
3893 >> RW_TAC std_ss [sum,COUNT_SUC,REAL_SUM_IMAGE_THM,FINITE_COUNT]
3894 >> Suff `count n DELETE n = count n`
3895 >- RW_TAC std_ss [REAL_ADD_COMM]
3896 >> RW_TAC std_ss [GSYM DELETE_NON_ELEMENT,IN_COUNT]
3897QED
3898
3899Theorem REAL_SUM_IMAGE_POW: !a s. FINITE s
3900 ==> ((REAL_SUM_IMAGE a s) pow 2 =
3901 REAL_SUM_IMAGE (\(i,j). a i * a j) (s CROSS s):real)
3902Proof
3903 RW_TAC std_ss []
3904 >> `(\(i,j). a i * a j) = (\x. (\i j. a i * a j) (FST x) (SND x))`
3905 by (RW_TAC std_ss [FUN_EQ_THM]
3906 >> Cases_on `x`
3907 >> RW_TAC std_ss [])
3908 >> POP_ORW
3909 >> (MP_TAC o GSYM o Q.SPECL [`s`,`s`,`(\i j. a i * a j)`] o
3910 INST_TYPE [``:'b`` |-> ``:'a``]) REAL_SUM_IMAGE_REAL_SUM_IMAGE
3911 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL]
3912 >> RW_TAC std_ss [Once REAL_MUL_COMM,REAL_SUM_IMAGE_CMUL,POW_2]
3913QED
3914
3915Theorem REAL_SUM_IMAGE_EQ :
3916 !s (f:'a->real) f'. FINITE s /\ (!x. x IN s ==> (f x = f' x))
3917 ==> (REAL_SUM_IMAGE f s = REAL_SUM_IMAGE f' s)
3918Proof
3919 rw [REAL_SUM_IMAGE_sum, SUM_EQ']
3920QED
3921
3922Theorem REAL_SUM_IMAGE_EQ_0 :
3923 !f s. FINITE s /\ (!x. x IN s ==> f x = 0) ==> REAL_SUM_IMAGE f s = 0
3924Proof
3925 rpt STRIP_TAC
3926 >> MP_TAC (UNDISCH (Q.SPEC ‘s’ (GSYM REAL_SUM_IMAGE_0)))
3927 >> Rewr'
3928 >> MATCH_MP_TAC REAL_SUM_IMAGE_EQ >> rw []
3929QED
3930
3931Theorem REAL_SUM_IMAGE_IN_IF_ALT :
3932 !s f (z :real).
3933 FINITE s ==>
3934 REAL_SUM_IMAGE f s = REAL_SUM_IMAGE (\x. if x IN s then f x else z) s
3935Proof
3936 RW_TAC std_ss []
3937 >> MATCH_MP_TAC REAL_SUM_IMAGE_EQ
3938 >> RW_TAC std_ss []
3939QED
3940
3941Theorem REAL_SUM_IMAGE_SUB :
3942 !s (f:'a -> real) f'. FINITE s ==>
3943 (REAL_SUM_IMAGE (\x. f x - f' x) s =
3944 REAL_SUM_IMAGE f s - REAL_SUM_IMAGE f' s)
3945Proof
3946 rw [REAL_SUM_IMAGE_sum, SUM_SUB']
3947QED
3948
3949Theorem REAL_SUM_IMAGE_MONO_SET :
3950 !(f:'a -> real) s t.
3951 FINITE s /\ FINITE t /\ s SUBSET t /\ (!x. x IN t ==> 0 <= f x) ==>
3952 REAL_SUM_IMAGE f s <= REAL_SUM_IMAGE f t
3953Proof
3954 RW_TAC std_ss []
3955 >> `t = s UNION (t DIFF s)` by RW_TAC std_ss [UNION_DIFF]
3956 >> `FINITE (t DIFF s)` by RW_TAC std_ss [FINITE_DIFF]
3957 >> `DISJOINT s (t DIFF s)` by (
3958 RW_TAC std_ss [DISJOINT_DEF,IN_DIFF,EXTENSION,GSPECIFICATION,
3959 NOT_IN_EMPTY,IN_INTER] >-
3960 METIS_TAC [])
3961 >> `REAL_SUM_IMAGE f t = REAL_SUM_IMAGE f s + REAL_SUM_IMAGE f (t DIFF s)`
3962 by METIS_TAC [REAL_SUM_IMAGE_DISJOINT_UNION]
3963 >> POP_ORW
3964 >> Suff `0 <= REAL_SUM_IMAGE f (t DIFF s)`
3965 >- REAL_ARITH_TAC
3966 >> METIS_TAC [REAL_SUM_IMAGE_POS,IN_DIFF]
3967QED
3968
3969Theorem REAL_SUM_IMAGE_CROSS_SYM :
3970 !f s1 s2. FINITE s1 /\ FINITE s2 ==>
3971 (REAL_SUM_IMAGE (\(x,y). f (x,y)) (s1 CROSS s2) =
3972 REAL_SUM_IMAGE (\(y,x). f (x,y)) (s2 CROSS s1))
3973Proof
3974 RW_TAC std_ss []
3975 >> `s2 CROSS s1 = IMAGE (\a. (SND a, FST a)) (s1 CROSS s2)`
3976 by (RW_TAC std_ss [IN_IMAGE, IN_CROSS,EXTENSION] \\
3977 METIS_TAC [FST,SND,PAIR])
3978 >> POP_ORW
3979 >> `INJ (\a. (SND a, FST a)) (s1 CROSS s2)
3980 (IMAGE (\a. (SND a, FST a)) (s1 CROSS s2))`
3981 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE, IN_CROSS]
3982 >> METIS_TAC [FST,SND,PAIR])
3983 >> RW_TAC std_ss [REAL_SUM_IMAGE_IMAGE, IMAGE_FINITE, FINITE_CROSS, o_DEF]
3984 >> `(\(x,y). f (x,y)) = (\a. f a)`
3985 by (RW_TAC std_ss [FUN_EQ_THM] \\
3986 Cases_on `a` >> RW_TAC std_ss [])
3987 >> RW_TAC std_ss []
3988QED
3989
3990Theorem REAL_SUM_IMAGE_ABS_TRIANGLE :
3991 !f s. FINITE s ==> abs (REAL_SUM_IMAGE f s) <= REAL_SUM_IMAGE (abs o f) s
3992Proof
3993 rw [REAL_SUM_IMAGE_sum, SUM_ABS', o_DEF]
3994QED
3995
3996Theorem REAL_SUM_IMAGE_DELETE = translate SUM_DELETE
3997Theorem REAL_SUM_IMAGE_SWAP = translate SUM_SWAP
3998Theorem REAL_SUM_IMAGE_BOUND = translate SUM_BOUND'
3999
4000Theorem REAL_SUM_IMAGE_IMAGE_LE :
4001 !f:'a->'b g s.
4002 FINITE s /\
4003 (!x. x IN s ==> (0:real) <= g (f x))
4004 ==> REAL_SUM_IMAGE g (IMAGE f s) <= REAL_SUM_IMAGE (g o f) s
4005Proof
4006 rpt STRIP_TAC
4007 >> ‘FINITE (IMAGE f s)’ by METIS_TAC [IMAGE_FINITE]
4008 >> rw [REAL_SUM_IMAGE_sum]
4009 >> MATCH_MP_TAC SUM_IMAGE_LE >> art []
4010QED
4011
4012Theorem REAL_SUM_IMAGE_PERMUTES :
4013 !f p s:'a->bool. FINITE s /\ p PERMUTES s ==>
4014 REAL_SUM_IMAGE f s = REAL_SUM_IMAGE (f o p) s
4015Proof
4016 rw [BIJ_ALT, REAL_SUM_IMAGE_sum, IN_FUNSET]
4017 >> MATCH_MP_TAC SUM_BIJECTION >> rw []
4018 >> Q.PAT_X_ASSUM ‘!y. y IN s ==> ?!x. P’ (MP_TAC o Q.SPEC ‘y’)
4019 >> RW_TAC bool_ss [EXISTS_UNIQUE_DEF] (* why it takes so long time? *)
4020 >> Q.EXISTS_TAC ‘x’ >> art []
4021QED
4022
4023(* ------------------------------------------------------------------------- *)
4024(* Analogous notion of finite products *)
4025(* (generally for use in descendent theories) *)
4026(* ------------------------------------------------------------------------- *)
4027
4028Definition REAL_PROD_IMAGE_DEF:
4029 REAL_PROD_IMAGE f s = ITSET (λe acc. f e * acc) s (1:real)
4030End
4031
4032Overload PI = “REAL_PROD_IMAGE”
4033val _ = Unicode.unicode_version {u = UTF8.chr 0x220F, tmnm = "PI"};
4034
4035Theorem REAL_PROD_IMAGE_EMPTY[simp]:
4036 !(f:'a -> real). REAL_PROD_IMAGE f EMPTY = 1
4037Proof
4038 simp[REAL_PROD_IMAGE_DEF]
4039QED
4040
4041Theorem REAL_PROD_IMAGE_INSERT:
4042 !(f:'a -> real) e s. FINITE s ==>
4043 REAL_PROD_IMAGE f (e INSERT s) = f e * REAL_PROD_IMAGE f (s DELETE e)
4044Proof
4045 rw[REAL_PROD_IMAGE_DEF] >>
4046 qspecl_then [‘λe acc. f e * acc’,‘e’,‘s’,‘1r’]
4047 (irule o SIMP_RULE (srw_ss ()) []) COMMUTING_ITSET_RECURSES >>
4048 simp[]
4049QED
4050
4051Theorem REAL_PROD_IMAGE_THM:
4052 !f. REAL_PROD_IMAGE f EMPTY = 1r /\
4053 !e s. FINITE s ==>
4054 REAL_PROD_IMAGE f (e INSERT s) = f e * REAL_PROD_IMAGE f (s DELETE e)
4055Proof
4056 simp[REAL_PROD_IMAGE_EMPTY,REAL_PROD_IMAGE_INSERT]
4057QED
4058
4059Theorem REAL_PROD_IMAGE_SING[simp]:
4060 !f e. REAL_PROD_IMAGE f {e} = f e
4061Proof
4062 SRW_TAC [][REAL_PROD_IMAGE_THM]
4063QED
4064
4065(* ------------------------------------------------------------------------- *)
4066(* ---- jensen's inequality (from "miller" example) ------------ *)
4067(* ------------------------------------------------------------------------- *)
4068
4069Definition convex_fn :
4070 convex_fn =
4071 {f | !x y t. 0 <= t /\ t <= 1 ==>
4072 f (t * x + (1 - t) * y) <= t * f x + (1 - t) * f y}
4073End
4074
4075Definition concave_fn :
4076 concave_fn = {f | (\x. ~(f x)) IN convex_fn}
4077End
4078
4079Definition pos_convex_fn :
4080 pos_convex_fn =
4081 {f | !x y t. 0 < x /\ 0 < y /\ 0 <= t /\ t <= 1 ==>
4082 f (t * x + (1 - t) * y) <= t * f x + (1 - t) * f y}
4083End
4084
4085Definition pos_concave_fn :
4086 pos_concave_fn = {f | (\x. ~ (f x)) IN pos_convex_fn}
4087End
4088
4089Theorem jensen_convex_SIGMA :
4090 !s. FINITE s ==>
4091 !f g g'. SIGMA g s = 1 /\
4092 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\
4093 f IN convex_fn ==>
4094 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s
4095Proof
4096 HO_MATCH_MP_TAC FINITE_INDUCT
4097 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT,
4098 DISJ_IMP_THM, FORALL_AND_THM]
4099 >> Cases_on `g e = 0` >- FULL_SIMP_TAC real_ss []
4100 >> Cases_on `g e = 1`
4101 >- (FULL_SIMP_TAC real_ss [] \\
4102 Know `!s. FINITE s ==>
4103 (\s. !g. SIGMA g s = 0 /\ (!x. x IN s ==> 0 <= g x /\ g x <= 1) ==>
4104 (!x. x IN s ==> (g x = 0))) s`
4105 >- (Q.X_GEN_TAC ‘t’ >> DISCH_TAC \\
4106 BETA_TAC >> Q.X_GEN_TAC ‘h’ \\
4107 Cases_on ‘t = {}’ >- simp [] \\
4108 STRIP_TAC >> CCONTR_TAC >> fs [] \\
4109 MP_TAC (Q.SPEC ‘t’ REAL_SUM_IMAGE_NONZERO) >> simp [] \\
4110 Q.EXISTS_TAC ‘h’ >> simp [] \\
4111 Q.EXISTS_TAC ‘x’ >> art []) \\
4112 Know `!x:real. (1 + x = 1) = (x = 0)` >- REAL_ARITH_TAC \\
4113 STRIP_TAC >> FULL_SIMP_TAC real_ss [] \\
4114 POP_ASSUM (K ALL_TAC) \\
4115 (ASSUME_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF >> POP_ORW \\
4116 DISCH_TAC \\
4117 POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o (REWRITE_RULE [GSYM AND_IMP_INTRO]) o
4118 (Q.SPEC `g`) o UNDISCH o (Q.SPEC `s`)) \\
4119 `(\x. (if x IN s then (\x. g x * g' x) x else 0)) = (\x. 0)`
4120 by RW_TAC real_ss [FUN_EQ_THM] >> POP_ORW \\
4121 `(\x. (if x IN s then (\x. g x * f (g' x)) x else 0)) = (\x. 0)`
4122 by RW_TAC real_ss [FUN_EQ_THM] >> POP_ORW \\
4123 Suff `SIGMA (\x. 0) s = 0` >- RW_TAC real_ss [] \\
4124 (MP_TAC o Q.SPECL [`(\x. 0)`, `0`] o
4125 UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST \\
4126 RW_TAC real_ss [])
4127 (* stage work *)
4128 >> Know `SIGMA (\x. g x * g' x) s =
4129 (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * g' x) s /\
4130 SIGMA (\x. g x * f(g' x)) s =
4131 (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * f(g' x)) s`
4132 >- (Know `~(1 - g e = 0)` >- (POP_ASSUM MP_TAC >> REAL_ARITH_TAC) \\
4133 RW_TAC real_ss [(REWRITE_RULE [Once EQ_SYM_EQ] o UNDISCH o Q.SPEC `s`)
4134 REAL_SUM_IMAGE_CMUL,
4135 REAL_MUL_ASSOC, REAL_DIV_LMUL])
4136 >> RW_TAC std_ss []
4137 >> FULL_SIMP_TAC std_ss [convex_fn, GSPECIFICATION]
4138 >> Q.PAT_X_ASSUM `!f' g'' g'''. SIGMA g'' s = 1 /\ _ ==> P`
4139 (MP_TAC o Q.SPECL [`f`, `(\x. g x / (1 - g e))`, `g'`])
4140 >> RW_TAC std_ss []
4141 >> Q.PAT_X_ASSUM `!x y t. P`
4142 (MP_TAC o Q.SPECL [`g' e`, `SIGMA (\x. g x / (1 - g e) * g' x) s`, `g e`])
4143 >> RW_TAC std_ss []
4144 >> MATCH_MP_TAC REAL_LE_TRANS
4145 >> Q.EXISTS_TAC `g e * f (g' e) +
4146 (1 - g e) * f (SIGMA (\x. g x / (1 - g e) * g' x) s)`
4147 >> RW_TAC real_ss [REAL_LE_LADD]
4148 >> Cases_on `g e = 1` >- RW_TAC real_ss []
4149 >> Know `0 < 1 - g e`
4150 >- (Q.PAT_X_ASSUM `g e <= 1` MP_TAC \\
4151 Q.PAT_X_ASSUM `~ (g e = 1)` MP_TAC >> REAL_ARITH_TAC)
4152 >> STRIP_TAC
4153 >> Suff `f (SIGMA (\x. g x / (1 - g e) * g' x) s) <=
4154 SIGMA (\x. g x / (1 - g e) * f (g' x)) s`
4155 >- PROVE_TAC [REAL_LE_LMUL]
4156 >> FIRST_X_ASSUM MATCH_MP_TAC
4157 >> CONJ_TAC
4158 >- ((MP_TAC o Q.SPECL [`g`, `inv (1- g e)`] o UNDISCH o Q.SPEC `s`)
4159 REAL_SUM_IMAGE_CMUL \\
4160 RW_TAC real_ss [real_div] >> ASM_REWRITE_TAC [Once REAL_MUL_COMM] \\
4161 RW_TAC std_ss [Once REAL_MUL_COMM, GSYM real_div] \\
4162 Suff `SIGMA g s = 1 * (1 - g e)` >- PROVE_TAC [REAL_EQ_LDIV_EQ] \\
4163 Q.PAT_X_ASSUM `g e + SIGMA g s = 1` MP_TAC \\
4164 REAL_ARITH_TAC)
4165 >> RW_TAC std_ss [] >- PROVE_TAC [REAL_LE_DIV, REAL_LT_IMP_LE]
4166 >> Suff `g x <= 1 * (1 - g e)` >- PROVE_TAC [REAL_LE_LDIV_EQ]
4167 >> Suff `g e + g x <= 1` >- REAL_ARITH_TAC
4168 >> Q.PAT_X_ASSUM `g e + SIGMA g s = 1` (fn thm => ONCE_REWRITE_TAC [GSYM thm])
4169 >> MATCH_MP_TAC REAL_LE_ADD2
4170 >> PROVE_TAC [REAL_LE_REFL, REAL_SUM_IMAGE_POS_MEM_LE]
4171QED
4172
4173Theorem jensen_concave_SIGMA :
4174 !s. FINITE s ==>
4175 !f g g'. SIGMA g s = 1 /\
4176 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\
4177 f IN concave_fn ==>
4178 SIGMA (\x. g x * f (g' x)) s <= f (SIGMA (\x. g x * g' x) s)
4179Proof
4180 REPEAT STRIP_TAC
4181 >> ONCE_REWRITE_TAC [GSYM REAL_LE_NEG2]
4182 >> RW_TAC std_ss [(REWRITE_RULE [Once EQ_SYM_EQ]) REAL_SUM_IMAGE_NEG]
4183 >> Suff `(\x. ~ f x) (SIGMA (\x. g x * g' x) s) <=
4184 SIGMA (\x. g x * (\x. ~ f x) (g' x)) s`
4185 >- RW_TAC real_ss []
4186 >> Q.ABBREV_TAC `f' = (\x. ~f x)`
4187 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) jensen_convex_SIGMA
4188 >> Q.UNABBREV_TAC `f'`
4189 >> FULL_SIMP_TAC std_ss [concave_fn, GSPECIFICATION]
4190QED
4191
4192Theorem jensen_pos_convex_SIGMA :
4193 !s. FINITE s ==>
4194 !f g g'. SIGMA g s = 1 /\
4195 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\
4196 (!x. x IN s ==> (0 < g x ==> 0 < g' x)) /\
4197 f IN pos_convex_fn ==>
4198 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s
4199Proof
4200 HO_MATCH_MP_TAC FINITE_INDUCT
4201 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT,
4202 DISJ_IMP_THM, FORALL_AND_THM]
4203 >> Cases_on `g e = 0` >- FULL_SIMP_TAC real_ss []
4204 >> Cases_on `g e = 1`
4205 >- (FULL_SIMP_TAC real_ss [] \\
4206 Know `!s. FINITE s ==>
4207 (\s. !g. SIGMA g s = 0 /\ (!x. x IN s ==> 0 <= g x /\ g x <= 1) ==>
4208 !x. x IN s ==> g x = 0) s`
4209 >- (Q.X_GEN_TAC ‘t’ >> DISCH_TAC \\
4210 BETA_TAC >> Q.X_GEN_TAC ‘h’ \\
4211 Cases_on ‘t = {}’ >- simp [] \\
4212 STRIP_TAC >> CCONTR_TAC >> fs [] \\
4213 MP_TAC (Q.SPEC ‘t’ REAL_SUM_IMAGE_NONZERO) >> simp [] \\
4214 Q.EXISTS_TAC ‘h’ >> simp [] \\
4215 Q.EXISTS_TAC ‘x’ >> art []) \\
4216 Know `!x:real. (1 + x = 1) = (x = 0)` >- REAL_ARITH_TAC \\
4217 STRIP_TAC >> FULL_SIMP_TAC real_ss [] \\
4218 POP_ASSUM (K ALL_TAC) \\
4219 (ASSUME_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF >> POP_ORW \\
4220 DISCH_TAC \\
4221 POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o
4222 (Q.SPEC `g`) o UNDISCH o (Q.SPEC `s`)) \\
4223 `(\x. (if x IN s then (\x. g x * g' x) x else 0)) = (\x. 0)`
4224 by RW_TAC real_ss [FUN_EQ_THM] >> POP_ORW \\
4225 `(\x. (if x IN s then (\x. g x * f (g' x)) x else 0)) = (\x. 0)`
4226 by RW_TAC real_ss [FUN_EQ_THM] >> POP_ORW \\
4227 Suff `SIGMA (\x. 0) s = 0` >- RW_TAC real_ss [] \\
4228 (MP_TAC o Q.SPECL [`(\x. 0)`, `0`] o
4229 UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST \\
4230 RW_TAC real_ss [])
4231 (* stage work *)
4232 >> Know `SIGMA (\x. g x * g' x) s =
4233 (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * g' x) s /\
4234 SIGMA (\x. g x * f (g' x)) s =
4235 (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * f(g' x)) s`
4236 >- (Know `~(1 - g e = 0)` >- (POP_ASSUM MP_TAC >> REAL_ARITH_TAC) \\
4237 RW_TAC real_ss [(REWRITE_RULE [Once EQ_SYM_EQ] o UNDISCH o Q.SPEC `s`)
4238 REAL_SUM_IMAGE_CMUL,
4239 REAL_MUL_ASSOC, REAL_DIV_LMUL])
4240 >> RW_TAC std_ss []
4241 >> FULL_SIMP_TAC std_ss [pos_convex_fn, GSPECIFICATION]
4242 >> Q.PAT_X_ASSUM `!f g g'. P`
4243 (MP_TAC o Q.SPECL [`f`, `(\x. g x / (1 - g e))`, `g'`])
4244 >> RW_TAC std_ss []
4245 >> Know `0 < 1 - g e`
4246 >- (Q.PAT_X_ASSUM `g e <= 1` MP_TAC \\
4247 Q.PAT_X_ASSUM `~(g e = 1)` MP_TAC >> REAL_ARITH_TAC)
4248 >> STRIP_TAC
4249 (* stage work *)
4250 >> Know `SIGMA (\x. g x / (1 - g e)) s = 1`
4251 >- ((MP_TAC o Q.SPECL [`g`, `inv (1- g e)`] o UNDISCH o Q.SPEC `s`)
4252 REAL_SUM_IMAGE_CMUL \\
4253 RW_TAC real_ss [real_div] >> ASM_REWRITE_TAC [Once REAL_MUL_COMM] \\
4254 RW_TAC std_ss [Once REAL_MUL_COMM, GSYM real_div] \\
4255 Suff `SIGMA g s = 1 * (1 - g e)` >- PROVE_TAC [REAL_EQ_LDIV_EQ] \\
4256 Q.PAT_X_ASSUM `g e + SIGMA g s = 1` MP_TAC >> REAL_ARITH_TAC)
4257 >> STRIP_TAC
4258 >> FULL_SIMP_TAC std_ss []
4259 >> Cases_on `s = {}` >- FULL_SIMP_TAC real_ss [REAL_SUM_IMAGE_THM]
4260 >> Know `0 < SIGMA (\x. g x / (1 - g e) * g' x) s`
4261 >- (RW_TAC std_ss [REAL_LT_LE]
4262 >- ((MATCH_MP_TAC o UNDISCH o REWRITE_RULE [GSYM AND_IMP_INTRO] o
4263 Q.SPECL [`(\x. g x / (1 - g e) * g' x)`,`s`]) REAL_SUM_IMAGE_POS \\
4264 RW_TAC real_ss [] >> Cases_on `g x = 0` >- RW_TAC real_ss [] \\
4265 MATCH_MP_TAC REAL_LE_MUL \\
4266 reverse CONJ_TAC >- PROVE_TAC [REAL_LT_IMP_LE, REAL_LT_LE] \\
4267 RW_TAC real_ss [] >> MATCH_MP_TAC REAL_LE_DIV \\
4268 RW_TAC real_ss [] >> PROVE_TAC [REAL_LT_IMP_LE]) \\
4269 Q.PAT_X_ASSUM `SIGMA (\x. g x * g' x) s =
4270 (1 - g e) * SIGMA (\x. g x / (1 - g e) * g' x) s`
4271 (MP_TAC o REWRITE_RULE [Once REAL_MUL_COMM] o GSYM) \\
4272 RW_TAC std_ss [GSYM REAL_EQ_RDIV_EQ] \\
4273 RW_TAC std_ss [real_div, REAL_ENTIRE, REAL_INV_EQ_0, REAL_LT_IMP_NE] \\
4274 SPOSE_NOT_THEN STRIP_ASSUME_TAC \\
4275 Know `!s. FINITE s ==>
4276 (\s. !g g'. (!x. x IN s ==> 0 <= g x) /\
4277 (!x. x IN s ==> 0 < g x ==> 0 < g' x) /\
4278 SIGMA (\x. g x * g' x) s = 0 ==>
4279 !x. x IN s ==> g x = 0) s`
4280 >- (Q.X_GEN_TAC ‘t’ >> DISCH_TAC \\
4281 BETA_TAC \\
4282 qx_genl_tac [‘f1’, ‘f2’] >> STRIP_TAC \\
4283 Cases_on ‘t = {}’ >- simp [] \\
4284 CCONTR_TAC >> fs [] \\
4285 MP_TAC (Q.SPEC ‘t’ REAL_SUM_IMAGE_NONZERO) >> simp [] \\
4286 Q.EXISTS_TAC ‘\x. f1 x * f2 x’ >> simp [] \\
4287 CONJ_TAC
4288 >- (Q.X_GEN_TAC ‘y’ >> DISCH_TAC \\
4289 ‘f1 y = 0 \/ 0 < f1 y’ by PROVE_TAC [REAL_LE_LT] >- simp [] \\
4290 MATCH_MP_TAC REAL_LT_IMP_LE \\
4291 MATCH_MP_TAC REAL_LT_MUL >> simp []) \\
4292 Q.EXISTS_TAC ‘x’ >> art [] \\
4293 Suff ‘0 < f2 x’ >- METIS_TAC [REAL_LT_IMP_NE] \\
4294 FIRST_X_ASSUM irule >> art [] \\
4295 METIS_TAC [REAL_LE_LT]) \\
4296 DISCH_THEN (MP_TAC o UNDISCH o Q.SPEC `s`) >> BETA_TAC \\
4297 simp [IMP_CONJ_THM, FORALL_AND_THM] \\
4298 qexistsl_tac [‘g’, ‘g'’] >> simp [] \\
4299 CCONTR_TAC >> fs [] \\
4300 Suff ‘SIGMA g s = 0’ >- (DISCH_TAC >> fs []) \\
4301 MATCH_MP_TAC REAL_SUM_IMAGE_EQ_0 >> art [] \\
4302 PROVE_TAC [])
4303 >> DISCH_TAC
4304 (* stage work, the rest is fast enough *)
4305 >> Q.PAT_X_ASSUM `!x y t. P`
4306 (MP_TAC o Q.SPECL [`g' e`, `SIGMA (\x. g x / (1 - g e) * g' x) s`, `g e`])
4307 >> Know `0 < g' e` >- METIS_TAC [REAL_LT_LE]
4308 >> RW_TAC std_ss []
4309 >> MATCH_MP_TAC REAL_LE_TRANS
4310 >> Q.EXISTS_TAC `g e * f (g' e) +
4311 (1 - g e) * f (SIGMA (\x. g x / (1 - g e) * g' x) s)`
4312 >> RW_TAC real_ss [REAL_LE_LADD]
4313 >> Suff `f (SIGMA (\x. g x / (1 - g e) * g' x) s) <=
4314 SIGMA (\x. g x / (1 - g e) * f (g' x)) s`
4315 >- PROVE_TAC [REAL_LE_LMUL]
4316 >> Q.PAT_X_ASSUM `(!x. x IN s ==> 0 <= g x / (1 - g e) /\ g x / (1 - g e) <= 1) /\
4317 (!x. x IN s ==> 0 < g x / (1 - g e) ==> 0 < g' x) ==>
4318 f (SIGMA (\x. g x / (1 - g e) * g' x) s) <=
4319 SIGMA (\x. g x / (1 - g e) * f (g' x)) s` MATCH_MP_TAC
4320 >> RW_TAC std_ss [] (* 3 sub-goals *)
4321 >| [ (* goal 1 (of 3) *)
4322 PROVE_TAC [REAL_LE_DIV, REAL_LT_IMP_LE],
4323 (* goal 2 (of 3) *)
4324 Suff `g x <= 1 * (1 - g e)` >- PROVE_TAC [REAL_LE_LDIV_EQ] \\
4325 Suff `g e + g x <= 1` >- REAL_ARITH_TAC \\
4326 Q.PAT_X_ASSUM `g e + SIGMA g s = 1` (fn thm => ONCE_REWRITE_TAC [GSYM thm]) \\
4327 MATCH_MP_TAC REAL_LE_ADD2 \\
4328 PROVE_TAC [REAL_LE_REFL, REAL_SUM_IMAGE_POS_MEM_LE],
4329 (* goal 3 (of 3) *)
4330 Cases_on `g x = 0` >- FULL_SIMP_TAC real_ss [] \\
4331 PROVE_TAC [REAL_LT_LE] ]
4332QED
4333
4334Theorem jensen_pos_concave_SIGMA :
4335 !s. FINITE s ==>
4336 !f g g'. SIGMA g s = 1 /\
4337 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\
4338 (!x. x IN s ==> (0 < g x ==> 0 < g' x)) /\
4339 f IN pos_concave_fn ==>
4340 SIGMA (\x. g x * f (g' x)) s <= f (SIGMA (\x. g x * g' x) s)
4341Proof
4342 REPEAT STRIP_TAC
4343 >> ONCE_REWRITE_TAC [GSYM REAL_LE_NEG2]
4344 >> RW_TAC std_ss [(REWRITE_RULE [Once EQ_SYM_EQ]) REAL_SUM_IMAGE_NEG]
4345 >> Suff `(\x. ~ f x) (SIGMA (\x. g x * g' x) s) <=
4346 SIGMA (\x. g x * (\x. ~ f x) (g' x)) s`
4347 >- RW_TAC real_ss []
4348 >> Q.ABBREV_TAC `f' = (\x. ~f x)`
4349 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) jensen_pos_convex_SIGMA
4350 >> Q.UNABBREV_TAC `f'`
4351 >> FULL_SIMP_TAC std_ss [pos_concave_fn, GSPECIFICATION]
4352QED