1 (* ========================================================================= *)
2 (* Various convenient background stuff. *)
4 (* (c) Copyright, John Harrison 1998-2008 *)
5 (* ========================================================================= *)
9 (* ------------------------------------------------------------------------- *)
10 (* A couple of extra tactics used in some proofs below. *)
11 (* ------------------------------------------------------------------------- *)
14 SUBGOAL_THEN tm STRIP_ASSUME_TAC;;
17 MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC tm THEN CONJ_TAC;;
19 (* ------------------------------------------------------------------------- *)
20 (* Miscellaneous lemmas. *)
21 (* ------------------------------------------------------------------------- *)
23 let EXISTS_DIFF = prove
24 (`(?s:A->bool. P(UNIV DIFF s)) <=> (?s. P s)`,
25 MESON_TAC[prove(`UNIV DIFF (UNIV DIFF s) = s`,SET_TAC[])]);;
29 REWRITE_TAC[GE; LE_REFL]);;
31 let FORALL_SUC = prove
32 (`(!n. ~(n = 0) ==> P n) <=> (!n. P(SUC n))`,
33 MESON_TAC[num_CASES; NOT_SUC]);;
35 let SEQ_MONO_LEMMA = prove
36 (`!d e. (!n. n >= m ==> d(n) < e(n)) /\ (!n. n >= m ==> e(n) <= e(m))
37 ==> !n:num. n >= m ==> d(n) < e(m)`,
38 MESON_TAC[GE; REAL_LTE_TRANS]);;
41 (`(!e. &0 < e / &2 <=> &0 < e) /\
42 (!e. e / &2 + e / &2 = e) /\
43 (!e. &2 * (e / &2) = e)`,
46 let UPPER_BOUND_FINITE_SET = prove
47 (`!f:(A->num) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a`,
48 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
49 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
50 MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;
52 let UPPER_BOUND_FINITE_SET_REAL = prove
53 (`!f:(A->real) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a`,
54 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
55 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
56 MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);;
58 let LOWER_BOUND_FINITE_SET = prove
59 (`!f:(A->num) s. FINITE(s) ==> ?a. !x. x IN s ==> a <= f(x)`,
60 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
61 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
62 MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;
64 let LOWER_BOUND_FINITE_SET_REAL = prove
65 (`!f:(A->real) s. FINITE(s) ==> ?a. !x. x IN s ==> a <= f(x)`,
66 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
67 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
68 MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);;
70 let REAL_CONVEX_BOUND2_LT = prove
71 (`!x y a u v. x < a /\ y < b /\ &0 <= u /\ &0 <= v /\ u + v = &1
72 ==> u * x + v * y < u * a + v * b`,
73 REPEAT GEN_TAC THEN ASM_CASES_TAC `u = &0` THENL
74 [ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN REPEAT STRIP_TAC;
75 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN
76 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE]] THEN
77 MATCH_MP_TAC REAL_LT_LMUL THEN ASM_REAL_ARITH_TAC);;
79 let REAL_CONVEX_BOUND_LT = prove
80 (`!x y a u v. x < a /\ y < a /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
81 ==> u * x + v * y < a`,
82 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
83 EXISTS_TAC `u * a + v * a:real` THEN CONJ_TAC THENL
84 [ASM_SIMP_TAC[REAL_CONVEX_BOUND2_LT];
85 MATCH_MP_TAC REAL_EQ_IMP_LE THEN
86 UNDISCH_TAC `u + v = &1` THEN CONV_TAC REAL_RING]);;
88 let REAL_CONVEX_BOUND_LE = prove
89 (`!x y a u v. x <= a /\ y <= a /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
90 ==> u * x + v * y <= a`,
92 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(u + v) * a` THEN
93 CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[REAL_LE_REFL; REAL_MUL_LID]] THEN
94 ASM_SIMP_TAC[REAL_ADD_RDISTRIB; REAL_LE_ADD2; REAL_LE_LMUL]);;
96 let INFINITE_ENUMERATE_WEAK = prove
99 ==> ?r:num->num. (!m n. m < n ==> r(m) < r(n)) /\ (!n. r n IN s)`,
100 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INFINITE_ENUMERATE) THEN
101 MATCH_MP_TAC MONO_EXISTS THEN SET_TAC[]);;
103 let APPROACHABLE_LT_LE = prove
104 (`!P f. (?d. &0 < d /\ !x. f(x) < d ==> P x) =
105 (?d. &0 < d /\ !x. f(x) <= d ==> P x)`,
107 (`&0 < d ==> x <= d / &2 ==> x < d`,
108 SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN REAL_ARITH_TAC) in
109 MESON_TAC[REAL_LT_IMP_LE; lemma; REAL_HALF]);;
111 let REAL_LE_BETWEEN = prove
112 (`!a b. a <= b <=> ?x. a <= x /\ x <= b`,
113 MESON_TAC[REAL_LE_TRANS; REAL_LE_REFL]);;
115 let REAL_LET_BETWEEN = prove
116 (`!a b. a < b <=> (?x. a <= x /\ x < b)`,
117 MESON_TAC[REAL_LE_REFL; REAL_LET_TRANS]);;
119 let REAL_LTE_BETWEEN = prove
120 (`!a b. a < b <=> (?x. a < x /\ x <= b)`,
121 MESON_TAC[REAL_LE_REFL; REAL_LTE_TRANS]);;
123 let REAL_LT_BETWEEN = prove
124 (`!a b. a < b <=> ?x. a < x /\ x < b`,
125 REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[REAL_LT_TRANS]] THEN
126 DISCH_TAC THEN EXISTS_TAC `(a + b) / &2` THEN
127 SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
128 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
130 let TRIANGLE_LEMMA = prove
131 (`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ x pow 2 <= y pow 2 + z pow 2
134 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
135 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
136 REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
137 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(y + z) pow 2` THEN
138 ASM_SIMP_TAC[REAL_POW_LT2; REAL_LE_ADD; ARITH_EQ] THEN
139 ASM_SIMP_TAC[REAL_LE_MUL; REAL_POW_2; REAL_ARITH
140 `x * x + y * y <= (x + y) * (x + y) <=> &0 <= x * y`]);;
142 let LAMBDA_SKOLEM = prove
143 (`(!i. 1 <= i /\ i <= dimindex(:N) ==> ?x. P i x) =
144 (?x:A^N. !i. 1 <= i /\ i <= dimindex(:N) ==> P i (x$i))`,
145 REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN EQ_TAC THENL
146 [DISCH_THEN(X_CHOOSE_TAC `x:num->A`) THEN
147 EXISTS_TAC `(lambda i. x i):A^N` THEN ASM_SIMP_TAC[LAMBDA_BETA];
148 DISCH_THEN(X_CHOOSE_TAC `x:A^N`) THEN
149 EXISTS_TAC `\i. (x:A^N)$i` THEN ASM_REWRITE_TAC[]]);;
151 let LAMBDA_PAIR = prove
152 (`(\(x,y). P x y) = (\p. P (FST p) (SND p))`,
153 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM] THEN
154 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[]);;
156 let EPSILON_DELTA_MINIMAL = prove
157 (`!P:real->A->bool Q.
159 (!d e x. Q x /\ &0 < e /\ e < d ==> P d x ==> P e x) /\
160 (!x. Q x ==> ?d. &0 < d /\ P d x)
161 ==> ?d. &0 < d /\ !x. Q x ==> P d x`,
162 REWRITE_TAC[IMP_IMP] THEN REPEAT STRIP_TAC THEN
163 ASM_CASES_TAC `{x:A | Q x} = {}` THENL
164 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EXTENSION]) THEN
165 REWRITE_TAC[NOT_IN_EMPTY; IN_ELIM_THM] THEN
166 DISCH_TAC THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_LT_01];
167 FIRST_X_ASSUM(MP_TAC o
168 GEN_REWRITE_RULE BINDER_CONV [RIGHT_IMP_EXISTS_THM]) THEN
169 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
170 X_GEN_TAC `d:A->real` THEN DISCH_TAC THEN
171 EXISTS_TAC `inf(IMAGE d {x:A | Q x})` THEN
172 ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
173 ASM_SIMP_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
174 X_GEN_TAC `a:A` THEN DISCH_TAC THEN
176 `&0 < inf(IMAGE d {x:A | Q x}) /\ inf(IMAGE d {x | Q x}) <= d a`
178 [ASM_SIMP_TAC[REAL_LT_INF_FINITE; REAL_INF_LE_FINITE;
179 FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
180 REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
181 ASM_MESON_TAC[REAL_LE_REFL];
182 REWRITE_TAC[REAL_LE_LT] THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
183 FIRST_X_ASSUM MATCH_MP_TAC THEN
184 EXISTS_TAC `(d:A->real) a` THEN ASM_SIMP_TAC[]]]);;
186 (* ------------------------------------------------------------------------- *)
187 (* A generic notion of "hull" (convex, affine, conic hull and closure). *)
188 (* ------------------------------------------------------------------------- *)
190 parse_as_infix("hull",(21,"left"));;
192 let hull = new_definition
193 `P hull s = INTERS {t | P t /\ s SUBSET t}`;;
196 (`!P s. P s ==> (P hull s = s)`,
197 REWRITE_TAC[hull; EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
201 (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f)) ==> P(P hull s)`,
202 REWRITE_TAC[hull] THEN SIMP_TAC[IN_ELIM_THM]);;
205 (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f))
206 ==> ((P hull s = s) <=> P s)`,
207 MESON_TAC[P_HULL; HULL_P]);;
209 let HULL_HULL = prove
210 (`!P s. P hull (P hull s) = P hull s`,
211 REWRITE_TAC[hull; EXTENSION; IN_INTERS; IN_ELIM_THM; SUBSET] THEN
214 let HULL_SUBSET = prove
215 (`!P s. s SUBSET (P hull s)`,
216 REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
218 let HULL_MONO = prove
219 (`!P s t. s SUBSET t ==> (P hull s) SUBSET (P hull t)`,
220 REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
222 let HULL_ANTIMONO = prove
223 (`!P Q s. P SUBSET Q ==> (Q hull s) SUBSET (P hull s)`,
224 REWRITE_TAC[SUBSET; hull; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[IN]);;
226 let HULL_MINIMAL = prove
227 (`!P s t. s SUBSET t /\ P t ==> (P hull s) SUBSET t`,
228 REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
230 let SUBSET_HULL = prove
231 (`!P s t. P t ==> ((P hull s) SUBSET t <=> s SUBSET t)`,
232 REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
234 let HULL_UNIQUE = prove
235 (`!P s t. s SUBSET t /\ P t /\ (!t'. s SUBSET t' /\ P t' ==> t SUBSET t')
237 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
238 REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN
239 ASM_MESON_TAC[SUBSET_HULL; SUBSET]);;
241 let HULL_UNION_SUBSET = prove
242 (`!P s t. (P hull s) UNION (P hull t) SUBSET (P hull (s UNION t))`,
243 SIMP_TAC[UNION_SUBSET; HULL_MONO; SUBSET_UNION]);;
245 let HULL_UNION = prove
246 (`!P s t. P hull (s UNION t) = P hull (P hull s UNION P hull t)`,
247 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
248 AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
249 MESON_TAC[SUBSET_HULL]);;
251 let HULL_UNION_LEFT = prove
253 P hull (s UNION t) = P hull (P hull s UNION t)`,
254 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
255 AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
256 MESON_TAC[SUBSET_HULL]);;
258 let HULL_UNION_RIGHT = prove
260 P hull (s UNION t) = P hull (s UNION P hull t)`,
261 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
262 AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
263 MESON_TAC[SUBSET_HULL]);;
265 let HULL_REDUNDANT_EQ = prove
266 (`!P a s. a IN (P hull s) <=> (P hull (a INSERT s) = P hull s)`,
267 REWRITE_TAC[hull] THEN SET_TAC[]);;
269 let HULL_REDUNDANT = prove
270 (`!P a s. a IN (P hull s) ==> (P hull (a INSERT s) = P hull s)`,
271 REWRITE_TAC[HULL_REDUNDANT_EQ]);;
273 let HULL_INDUCT = prove
274 (`!P p s. (!x:A. x IN s ==> p x) /\ P {x | p x}
275 ==> !x. x IN P hull s ==> p x`,
277 MP_TAC(ISPECL [`P:(A->bool)->bool`; `s:A->bool`; `{x:A | p x}`]
279 REWRITE_TAC[SUBSET; IN_ELIM_THM]);;
282 (`!P s x. x IN s ==> x IN P hull s`,
283 MESON_TAC[REWRITE_RULE[SUBSET] HULL_SUBSET]);;
285 let HULL_IMAGE_SUBSET = prove
286 (`!P f s. P(P hull s) /\ (!s. P s ==> P(IMAGE f s))
287 ==> P hull (IMAGE f s) SUBSET (IMAGE f (P hull s))`,
288 REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
289 ASM_SIMP_TAC[IMAGE_SUBSET; HULL_SUBSET]);;
291 let HULL_IMAGE_GALOIS = prove
292 (`!P f g s. (!s. P(P hull s)) /\
293 (!s. P s ==> P(IMAGE f s)) /\ (!s. P s ==> P(IMAGE g s)) /\
294 (!s t. s SUBSET IMAGE g t <=> IMAGE f s SUBSET t)
295 ==> P hull (IMAGE f s) = IMAGE f (P hull s)`,
296 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
297 ASM_SIMP_TAC[HULL_IMAGE_SUBSET] THEN
298 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
299 MATCH_MP_TAC HULL_MINIMAL THEN
300 ASM_SIMP_TAC[HULL_SUBSET]);;
302 let HULL_IMAGE = prove
303 (`!P f s. (!s. P(P hull s)) /\ (!s. P(IMAGE f s) <=> P s) /\
304 (!x y:A. f x = f y ==> x = y) /\ (!y. ?x. f x = y)
305 ==> P hull (IMAGE f s) = IMAGE f (P hull s)`,
307 REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
308 REWRITE_TAC[BIJECTIVE_LEFT_RIGHT_INVERSE] THEN
309 DISCH_THEN(X_CHOOSE_THEN `g:A->A` STRIP_ASSUME_TAC) THEN
310 MATCH_MP_TAC HULL_IMAGE_GALOIS THEN EXISTS_TAC `g:A->A` THEN
311 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
312 X_GEN_TAC `s:A->bool` THEN
313 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
314 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN ASM SET_TAC[]);;
317 (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f))
318 ==> (P s <=> ?t. s = P hull t)`,
319 MESON_TAC[HULL_P; P_HULL]);;
323 (!f. (!s. s IN f ==> P s) ==> P (INTERS f)) /\
324 s SUBSET P hull t /\ t SUBSET P hull s
325 ==> P hull s = P hull t`,
326 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
327 CONJ_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
328 ASM_SIMP_TAC[P_HULL]);;
330 let HULL_P_AND_Q = prove
331 (`!P Q. (!f. (!s. s IN f ==> P s) ==> P(INTERS f)) /\
332 (!f. (!s. s IN f ==> Q s) ==> Q(INTERS f)) /\
333 (!s. Q s ==> Q(P hull s))
334 ==> (\x. P x /\ Q x) hull s = P hull (Q hull s)`,
335 REPEAT STRIP_TAC THEN
336 MATCH_MP_TAC HULL_UNIQUE THEN ASM_SIMP_TAC[HULL_INC; SUBSET_HULL] THEN
337 ASM_MESON_TAC[P_HULL; HULL_SUBSET; SUBSET_TRANS]);;
339 (* ------------------------------------------------------------------------- *)
340 (* More variants of the Archimedian property and useful consequences. *)
341 (* ------------------------------------------------------------------------- *)
343 let REAL_ARCH_INV = prove
344 (`!e. &0 < e <=> ?n. ~(n = 0) /\ &0 < inv(&n) /\ inv(&n) < e`,
345 GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[REAL_LT_TRANS]] THEN
346 DISCH_TAC THEN MP_TAC(SPEC `inv(e)` REAL_ARCH_LT) THEN
347 MATCH_MP_TAC MONO_EXISTS THEN
348 ASM_MESON_TAC[REAL_LT_INV2; REAL_INV_INV; REAL_LT_INV_EQ; REAL_LT_TRANS;
351 let REAL_POW_LBOUND = prove
352 (`!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n`,
353 GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
355 REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_ADD_RID; REAL_LE_REFL] THEN
356 REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
357 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 + x) * (&1 + &n * x)` THEN
358 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ARITH `&0 <= x ==> &0 <= &1 + x`] THEN
359 ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ARITH
360 `&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x`]);;
362 let REAL_ARCH_POW = prove
363 (`!x y. &1 < x ==> ?n. y < x pow n`,
364 REPEAT STRIP_TAC THEN
365 MP_TAC(SPEC `x - &1` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
366 DISCH_THEN(MP_TAC o SPEC `y:real`) THEN MATCH_MP_TAC MONO_EXISTS THEN
367 X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
368 EXISTS_TAC `&1 + &n * (x - &1)` THEN
369 ASM_SIMP_TAC[REAL_ARITH `x < y ==> x < &1 + y`] THEN
370 ASM_MESON_TAC[REAL_POW_LBOUND; REAL_SUB_ADD2; REAL_ARITH
371 `&1 < x ==> &0 <= x - &1`]);;
373 let REAL_ARCH_POW2 = prove
374 (`!x. ?n. x < &2 pow n`,
375 SIMP_TAC[REAL_ARCH_POW; REAL_OF_NUM_LT; ARITH]);;
377 let REAL_ARCH_POW_INV = prove
378 (`!x y. &0 < y /\ x < &1 ==> ?n. x pow n < y`,
379 REPEAT STRIP_TAC THEN ASM_CASES_TAC `&0 < x` THENL
380 [ALL_TAC; ASM_MESON_TAC[REAL_POW_1; REAL_LET_TRANS; REAL_NOT_LT]] THEN
381 SUBGOAL_THEN `inv(&1) < inv(x)` MP_TAC THENL
382 [ASM_SIMP_TAC[REAL_LT_INV2]; REWRITE_TAC[REAL_INV_1]] THEN
383 DISCH_THEN(MP_TAC o SPEC `inv(y)` o MATCH_MP REAL_ARCH_POW) THEN
384 MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN
385 GEN_REWRITE_TAC BINOP_CONV [GSYM REAL_INV_INV] THEN
386 ASM_SIMP_TAC[GSYM REAL_POW_INV; REAL_LT_INV; REAL_LT_INV2]);;
388 let FORALL_POS_MONO = prove
389 (`!P. (!d e. d < e /\ P d ==> P e) /\ (!n. ~(n = 0) ==> P(inv(&n)))
390 ==> !e. &0 < e ==> P e`,
391 MESON_TAC[REAL_ARCH_INV; REAL_LT_TRANS]);;
393 let FORALL_POS_MONO_1 = prove
394 (`!P. (!d e. d < e /\ P d ==> P e) /\ (!n. P(inv(&n + &1)))
395 ==> !e. &0 < e ==> P e`,
396 REWRITE_TAC[REAL_OF_NUM_SUC; GSYM FORALL_SUC; FORALL_POS_MONO]);;
398 let REAL_ARCH_RDIV_EQ_0 = prove
399 (`!x c. &0 <= x /\ &0 <= c /\ (!m. 0 < m ==> &m * x <= c) ==> x = &0`,
400 SIMP_TAC [GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT] THEN REPEAT STRIP_TAC THEN
401 POP_ASSUM (STRIP_ASSUME_TAC o SPEC `c:real` o MATCH_MP REAL_ARCH) THEN
402 ASM_CASES_TAC `n=0` THENL
403 [POP_ASSUM SUBST_ALL_TAC THEN
404 RULE_ASSUM_TAC (REWRITE_RULE [REAL_MUL_LZERO]) THEN
405 ASM_MESON_TAC [REAL_LET_ANTISYM];
406 ASM_MESON_TAC [REAL_LET_ANTISYM; REAL_MUL_SYM; LT_NZ]]);;
408 (* ------------------------------------------------------------------------- *)
409 (* Relate max and min to sup and inf. *)
410 (* ------------------------------------------------------------------------- *)
412 let REAL_MAX_SUP = prove
413 (`!x y. max x y = sup {x,y}`,
414 SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_SUP_LE_FINITE; REAL_LE_SUP_FINITE;
415 FINITE_RULES; NOT_INSERT_EMPTY; REAL_MAX_LE; REAL_LE_MAX] THEN
416 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LE_TOTAL]);;
418 let REAL_MIN_INF = prove
419 (`!x y. min x y = inf {x,y}`,
420 SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_INF_LE_FINITE; REAL_LE_INF_FINITE;
421 FINITE_RULES; NOT_INSERT_EMPTY; REAL_MIN_LE; REAL_LE_MIN] THEN
422 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LE_TOTAL]);;
424 (* ------------------------------------------------------------------------- *)
425 (* Define square root here to decouple it from the existing analysis theory. *)
426 (* We totalize by making sqrt(-x) = -sqrt(x), which looks rather unnatural *)
427 (* but allows many convenient properties to be used without sideconditions. *)
428 (* ------------------------------------------------------------------------- *)
430 let sqrt = new_definition
431 `sqrt(x) = @y. real_sgn y = real_sgn x /\ y pow 2 = abs x`;;
433 let SQRT_UNIQUE = prove
434 (`!x y. &0 <= y /\ y pow 2 = x ==> sqrt(x) = y`,
435 REPEAT STRIP_TAC THEN REWRITE_TAC[sqrt] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
436 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
437 REWRITE_TAC[REAL_SGN_POW_2; REAL_ABS_POW] THEN
438 X_GEN_TAC `z:real` THEN ASM_REWRITE_TAC[real_abs] THEN
439 REWRITE_TAC[REAL_RING `x pow 2 = y pow 2 <=> x:real = y \/ x = --y`] THEN
440 REWRITE_TAC[real_sgn] THEN ASM_REAL_ARITH_TAC);;
442 let POW_2_SQRT = prove
443 (`!x. &0 <= x ==> sqrt(x pow 2) = x`,
444 MESON_TAC[SQRT_UNIQUE]);;
448 MESON_TAC[SQRT_UNIQUE; REAL_POW_2; REAL_MUL_LZERO; REAL_POS]);;
452 MESON_TAC[SQRT_UNIQUE; REAL_POW_2; REAL_MUL_LID; REAL_POS]);;
454 let POW_2_SQRT_ABS = prove
455 (`!x. sqrt(x pow 2) = abs(x)`,
456 GEN_TAC THEN MATCH_MP_TAC SQRT_UNIQUE THEN
457 REWRITE_TAC[REAL_ABS_POS; REAL_POW_2; GSYM REAL_ABS_MUL] THEN
458 REWRITE_TAC[real_abs; REAL_LE_SQUARE]);;
460 (* ------------------------------------------------------------------------- *)
461 (* Geometric progression. *)
462 (* ------------------------------------------------------------------------- *)
464 let SUM_GP_BASIC = prove
465 (`!x n. (&1 - x) * sum(0..n) (\i. x pow i) = &1 - x pow (SUC n)`,
466 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN
467 REWRITE_TAC[real_pow; REAL_MUL_RID; LE_0] THEN
468 ASM_REWRITE_TAC[REAL_ADD_LDISTRIB; real_pow] THEN REAL_ARITH_TAC);;
470 let SUM_GP_MULTIPLIED = prove
472 ==> ((&1 - x) * sum(m..n) (\i. x pow i) = x pow m - x pow (SUC n))`,
473 REPEAT STRIP_TAC THEN ASM_SIMP_TAC
474 [SUM_OFFSET_0; REAL_POW_ADD; REAL_MUL_ASSOC; SUM_GP_BASIC; SUM_RMUL] THEN
475 REWRITE_TAC[REAL_SUB_RDISTRIB; GSYM REAL_POW_ADD; REAL_MUL_LID] THEN
476 ASM_SIMP_TAC[ARITH_RULE `m <= n ==> (SUC(n - m) + m = SUC n)`]);;
480 sum(m..n) (\i. x pow i) =
482 else if x = &1 then &((n + 1) - m)
483 else (x pow m - x pow (SUC n)) / (&1 - x)`,
485 DISJ_CASES_TAC(ARITH_RULE `n < m \/ ~(n < m) /\ m <= n:num`) THEN
486 ASM_SIMP_TAC[SUM_TRIV_NUMSEG] THEN COND_CASES_TAC THENL
487 [ASM_REWRITE_TAC[REAL_POW_ONE; SUM_CONST_NUMSEG; REAL_MUL_RID]; ALL_TAC] THEN
488 MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&1 - x` THEN
489 ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_SUB_0; SUM_GP_MULTIPLIED]);;
491 let SUM_GP_OFFSET = prove
492 (`!x m n. sum(m..m+n) (\i. x pow i) =
493 if x = &1 then &n + &1
494 else x pow m * (&1 - x pow (SUC n)) / (&1 - x)`,
495 REPEAT GEN_TAC THEN REWRITE_TAC[SUM_GP; ARITH_RULE `~(m + n < m:num)`] THEN
496 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
497 [REWRITE_TAC[REAL_OF_NUM_ADD] THEN AP_TERM_TAC THEN ARITH_TAC;
498 REWRITE_TAC[real_div; real_pow; REAL_POW_ADD] THEN REAL_ARITH_TAC]);;
500 (* ------------------------------------------------------------------------- *)
501 (* Segment of natural numbers starting at a specific number. *)
502 (* ------------------------------------------------------------------------- *)
504 let from = new_definition
505 `from n = {m:num | n <= m}`;;
509 REWRITE_TAC[from; LE_0] THEN SET_TAC[]);;
512 (`!m n. m IN from n <=> n <= m`,
513 REWRITE_TAC[from; IN_ELIM_THM]);;
515 let FROM_INTER_NUMSEG_GEN = prove
516 (`!k m n. (from k) INTER (m..n) = (if m < k then k..n else m..n)`,
517 REPEAT GEN_TAC THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN
518 REWRITE_TAC[from; IN_ELIM_THM; IN_INTER; IN_NUMSEG; EXTENSION] THEN
521 let FROM_INTER_NUMSEG_MAX = prove
522 (`!m n p. from p INTER (m..n) = (MAX p m..n)`,
523 REWRITE_TAC[EXTENSION; IN_INTER; IN_NUMSEG; IN_FROM] THEN ARITH_TAC);;
525 let FROM_INTER_NUMSEG = prove
526 (`!k n. (from k) INTER (0..n) = k..n`,
527 REWRITE_TAC[from; IN_ELIM_THM; IN_INTER; IN_NUMSEG; EXTENSION] THEN
530 let INFINITE_FROM = prove
531 (`!n. INFINITE(from n)`,
533 SUBGOAL_THEN `from n = (:num) DIFF {i | i < n}`
534 (fun th -> SIMP_TAC[th; INFINITE_DIFF_FINITE; FINITE_NUMSEG_LT;
536 REWRITE_TAC[EXTENSION; from; IN_DIFF; IN_UNIV; IN_ELIM_THM] THEN ARITH_TAC);;
538 (* ------------------------------------------------------------------------- *)
539 (* Make a Horner-style evaluation of sum(m..n) (\k. a(k) * x pow k). *)
540 (* ------------------------------------------------------------------------- *)
542 let HORNER_SUM_CONV =
543 let horner_0,horner_s = (CONJ_PAIR o prove)
544 (`(sum(0..0) (\i. c(i) * x pow i) = c 0) /\
545 (sum(0..SUC n) (\i. c(i) * x pow i) =
546 c(0) + x * sum(0..n) (\i. c(i+1) * x pow i))`,
547 REWRITE_TAC[CONJUNCT1 SUM_CLAUSES_NUMSEG] THEN
548 REWRITE_TAC[GSYM SUM_LMUL] THEN
549 ONCE_REWRITE_TAC[REAL_ARITH `x * c * y:real = c * x * y`] THEN
550 REWRITE_TAC[GSYM(CONJUNCT2 real_pow); ADD1] THEN
551 REWRITE_TAC[GSYM(SPEC `1` SUM_OFFSET)] THEN
552 SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; real_pow; REAL_MUL_RID]) in
553 let conv_0 = GEN_REWRITE_CONV I [horner_0] THENC NUM_REDUCE_CONV
554 and conv_s = LAND_CONV(RAND_CONV(num_CONV)) THENC
555 GEN_REWRITE_CONV I [horner_s] THENC
556 GEN_REWRITE_CONV ONCE_DEPTH_CONV [LEFT_ADD_DISTRIB] THENC
557 GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM ADD_ASSOC] THENC
560 try (conv_0 THENC REAL_RAT_REDUCE_CONV) tm with Failure _ ->
561 (conv_s THENC RAND_CONV(RAND_CONV conv) THENC REAL_RAT_REDUCE_CONV) tm in