1 (* ---------------------------------------------------------------------- *)
3 (* ---------------------------------------------------------------------- *)
4 let real_ty = `:real`;;
9 let req = `(=):real->real->bool`;;
10 let rneq = `(<>):real->real->bool`;;
11 let rlt = `(<):real->real->bool`;;
12 let rgt = `(>):real->real->bool`;;
13 let rle = `(<=):real->real->bool`;;
14 let rge = `(>=):real->real->bool`;;
15 let rm = `( * ):real->real->real`;;
16 let rs = `(-):real->real->real`;;
17 let rn = `(--):real->real`;;
18 let rd = `(/):real->real->real`;;
19 let rp = `(+):real->real->real`;;
22 let rlast = `LAST:(real) list -> real`;;
23 let rappend = `APPEND:(real) list -> real list -> real list`;;
24 let mk_rlist l = mk_list (l,real_ty);;
26 let diffl_tm = `(diffl)`;;
29 let l,var = dest_comb tm in
30 let dp,p' = dest_comb l in
31 let d,p = dest_comb dp in
32 if not (d = diffl_tm) then failwith "dest_diffl: not a diffl" else
33 let _,bod = dest_abs p in
35 with _ -> failwith "dest_diffl";;
40 with _ -> failwith "dest_mult";;
42 let mk_mult = mk_binop rm;;
44 let pow_tm = `(pow)`;;
48 with _ -> failwith "dest_pow";;
50 let mk_plus = mk_binop rp;;
51 let mk_negative = curry mk_comb rn;;
56 with _ -> failwith "dest_plus";;
58 let REAL_DENSE = prove(
59 `!x y. x < y ==> ?z. x < z /\ z < y`,
62 CLAIM `&0 < y - x` THENL
63 [REWRITE_TAC[REAL_LT_SUB_LADD;REAL_ADD_LID] THEN
64 POP_ASSUM MATCH_ACCEPT_TAC;
65 DISCH_THEN (ASSUME_TAC o (MATCH_MP REAL_DOWN)) THEN
66 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
67 EXISTS_TAC `e + x` THEN
69 [ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
70 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[GSYM REAL_ADD_RID])) THEN
71 MATCH_MP_TAC REAL_LET_ADD2 THEN
73 [MATCH_ACCEPT_TAC REAL_LE_REFL;
74 FIRST_ASSUM MATCH_ACCEPT_TAC];
75 MATCH_EQ_MP_TAC ((GEN `y:real` (GEN `z:real` (ISPECL [`y:real`;`z:real`;`-- x`] REAL_LT_RADD)))) THEN
76 REWRITE_TAC[GSYM REAL_ADD_ASSOC;REAL_ADD_RINV;REAL_ADD_RID] THEN
77 REWRITE_TAC[GSYM real_sub] THEN
78 FIRST_ASSUM MATCH_ACCEPT_TAC]]);;
81 let REAL_LT_EXISTS = prove(
85 EXISTS_TAC `x + &1` THEN
89 let REAL_GT_EXISTS = prove(
93 EXISTS_TAC `x - &1` THEN
97 let REAL_DIV_DISTRIB_L = prove_by_refinement(
98 `!x y z. x / (y * z) = (x / y) * (&1 / z)`,
101 REWRITE_TAC[real_div;REAL_INV_MUL];
106 let REAL_DIV_DISTRIB_R = prove_by_refinement(
107 `!x y z. x / (y * z) = (&1 / y) * (x / z)`,
110 REWRITE_TAC[real_div;REAL_INV_MUL];
115 let REAL_DIV_DISTRIB_2 = prove_by_refinement(
116 `!x y z. (x * w) / (y * z) = (x / y) * (w / z)`,
119 REWRITE_TAC[real_div;REAL_INV_MUL];
124 let REAL_DIV_ADD_DISTRIB = prove_by_refinement(
125 `!x y z. (x + y) / z = (x / z) + (y / z)`,
128 REWRITE_TAC[real_div;REAL_INV_MUL];
133 let DIV_ID = prove_by_refinement(
134 `!x. ~(x = &0) ==> (x / x = &1)`,
139 REWRITE_TAC[real_div];
140 ASM_MESON_TAC[REAL_MUL_LINV;REAL_MUL_SYM];
145 let POS_POW = prove_by_refinement(
146 `!c x. &0 < c /\ &0 < x ==> &0 < c * x pow k`,
150 MESON_TAC[REAL_POW_LT;REAL_LT_MUL]
155 let POS_NAT_POW = prove_by_refinement(
156 `!c n. 0 < n /\ &0 < c ==> &0 < c * &n pow k`,
160 MESON_TAC[REAL_POW_LT;REAL_LT_MUL;REAL_LT;]
165 let REAL_NUM_LE_0 = prove_by_refinement(
176 let REAL_ARCH_SIMPLE_LT = prove_by_refinement(
181 CHOOSE_THEN ASSUME_TAC (ISPEC `x:real` REAL_ARCH_SIMPLE);
184 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
188 let BINOMIAL_LEMMA_LT = prove_by_refinement(
189 `!x y. &0 < x /\ &0 < y
190 ==> !n. 0 < n ==> x pow n + y pow n <= (x + y) pow n`,
198 REWRITE_TAC[real_pow];
201 ASM_REWRITE_TAC[real_pow;REAL_MUL_RID;REAL_LE_REFL];
203 POP_ASSUM MP_TAC THEN ARITH_TAC;
204 DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
205 MATCH_MP_TAC REAL_LE_TRANS;
206 EXISTS_TAC `(x + y) * (x pow n + y pow n)`;
208 REWRITE_TAC[REAL_ADD_RDISTRIB];
209 MATCH_MP_TAC REAL_LE_ADD2;
211 MATCH_MP_TAC REAL_LE_LMUL;
213 FIRST_ASSUM (fun x -> MP_TAC x THEN ARITH_TAC);
214 MATCH_MP_TAC (REAL_ARITH `&0 <= y ==> x <= x + y`);
215 MATCH_MP_TAC REAL_POW_LE;
216 FIRST_ASSUM (fun x -> MP_TAC x THEN ARITH_TAC);
217 REWRITE_TAC[REAL_ADD_LDISTRIB];
218 MATCH_MP_TAC (REAL_ARITH `&0 <= y ==> x <= y + x`);
219 MATCH_MP_TAC REAL_LE_MUL;
221 FIRST_ASSUM (fun x -> MP_TAC x THEN REAL_ARITH_TAC);
222 MATCH_MP_TAC (REAL_ARITH `x < y ==> x <= y`);
223 MATCH_MP_TAC REAL_POW_LT;
224 FIRST_ASSUM MATCH_ACCEPT_TAC;
225 MATCH_MP_TAC REAL_LE_LMUL;
227 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
228 FIRST_ASSUM MATCH_ACCEPT_TAC;
233 let BINOMIAL_LEMMA = prove_by_refinement(
234 `!x y. &0 <= x /\ &0 <= y
235 ==> !n. 0 < n ==> x pow n + y pow n <= (x + y) pow n`,
241 CASES_ON `(x = &0) \/ (y = &0)`;
242 POP_ASSUM DISJ_CASES_TAC;
243 ASM_REWRITE_TAC[real_pow;REAL_ADD_LID;POW_0];
245 CLAIM `n = SUC (PRE n)`;
246 POP_ASSUM MP_TAC THEN ARITH_TAC;
248 ONCE_ASM_REWRITE_TAC[];
249 ASM_REWRITE_TAC[POW_0;REAL_ADD_LID;real_pow;REAL_LE_REFL];
251 CLAIM `n = SUC (PRE n)`;
252 POP_ASSUM MP_TAC THEN ARITH_TAC;
254 ONCE_ASM_REWRITE_TAC[];
255 ASM_REWRITE_TAC[POW_0;REAL_ADD_LID;REAL_ADD_RID;real_pow;REAL_LE_REFL];
256 POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC;
257 MATCH_MP_TAC BINOMIAL_LEMMA_LT;
258 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
263 let NEG_ABS = prove_by_refinement(
264 `!x. -- (abs x) <= &0`,
271 let REAL_MUL_LT = prove_by_refinement(
272 `!x y. x * y < &0 <=> (x < &0 /\ &0 < y) \/ (&0 < x /\ y < &0)`,
279 REWRITE_ASSUMS ([REAL_NOT_LT;DE_MORGAN_THM;] @ !REAL_REWRITES);
280 POP_ASSUM MP_TAC THEN STRIP_TAC;
282 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
283 DISCH_THEN (REWRITE_ASSUMS o list);
284 REWRITE_ASSUMS !REAL_REWRITES;
285 ASM_MESON_TAC !REAL_REWRITES;
286 CLAIM `&0 * &0 <= x * y`;
287 MATCH_MP_TAC REAL_LE_MUL2;
288 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
290 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
291 CLAIM `&0 * &0 <= --x * --y`;
292 MATCH_MP_TAC REAL_LE_MUL2;
294 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
296 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
298 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
299 DISCH_THEN (REWRITE_ASSUMS o list);
300 REWRITE_ASSUMS !REAL_REWRITES;
302 EVERY_ASSUM MP_TAC THEN ARITH_TAC;
306 EVERY_ASSUM MP_TAC THEN ARITH_TAC;
308 CLAIM `&0 * &0 < --x * y`;
309 MATCH_MP_TAC REAL_LT_MUL2;
311 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
313 REWRITE_TAC[REAL_ARITH `--y * x = --(y * x)`];
316 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
318 CLAIM `&0 * &0 < x * --y`;
319 MATCH_MP_TAC REAL_LT_MUL2;
323 REWRITE_TAC[REAL_ARITH `x * --y = --(x * y)`];
328 let REAL_MUL_GT = prove_by_refinement(
329 `!x y. &0 < x * y <=> (x < &0 /\ y < &0) \/ (&0 < x /\ &0 < y)`,
335 ONCE_REWRITE_ASSUMS[ARITH_RULE `x < y <=> -- y < -- x`];
336 REWRITE_ASSUMS[GSYM REAL_MUL_RNEG];
337 REWRITE_ASSUMS[REAL_ARITH `-- &0 = &0`; REAL_MUL_LT];
338 POP_ASSUM MP_TAC THEN REPEAT STRIP_TAC;
340 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
341 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
343 ONCE_REWRITE_TAC [ARITH_RULE `x * y = --x * --y`];
344 ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
345 MATCH_MP_TAC REAL_LT_MUL2;
346 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
347 ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
348 MATCH_MP_TAC REAL_LT_MUL2;
349 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
353 let REAL_DIV_INV = prove_by_refinement(
354 `!y z. &0 < y /\ y < z ==> &1 / z < &1 / y`,
358 REWRITE_TAC[real_div];
360 MATCH_MP_TAC REAL_LT_INV2;
365 let REAL_DIV_DENOM_LT = prove_by_refinement(
366 `!x y z. &0 < x /\ &0 < y /\ y < z ==> x / z < x / y`,
370 MATCH_MP_TAC REAL_LT_LCANCEL_IMP;
374 REWRITE_TAC[real_div];
375 ASM_SIMP_TAC[REAL_LT_IMP_NZ;REAL_MUL_ASSOC;REAL_MUL_LINV;];
377 MATCH_MP_TAC (REWRITE_RULE [REAL_MUL_LID;real_div] REAL_DIV_INV);
382 let REAL_DIV_DENOM_LE = prove_by_refinement(
383 `!x y z. &0 <= x /\ &0 < y /\ y <= z ==> x / z <= x / y`,
389 REWRITE_TAC[real_div;REAL_MUL_LZERO;REAL_LE_REFL];
390 MATCH_MP_TAC REAL_LE_LCANCEL_IMP;
393 MATCH_MP_TAC REAL_LT_INV;
394 ASM_MESON_TAC[REAL_LT_LE];
395 REWRITE_TAC[real_div];
396 ASM_SIMP_TAC[REAL_LT_IMP_NZ;REAL_MUL_ASSOC;REAL_MUL_LINV;];
398 MATCH_MP_TAC REAL_LE_INV2;
403 let REAL_NEG_DIV = prove_by_refinement(
404 `!x y. -- x / -- y = x / y`,
407 REWRITE_TAC[real_div];
408 REWRITE_TAC[REAL_INV_NEG];
413 let REAL_GT_IMP_NZ = prove(
414 `!x. x < &0 ==> ~(x = &0)`,
419 let REAL_NEG_NZ = prove(
420 `!x. x < &0 ==> ~(x = &0)`,
425 let PARITY_POW_LT = prove_by_refinement(
426 `!a n. a < &0 ==> (EVEN n ==> a pow n > &0) /\ (ODD n ==> a pow n < &0)`,
432 REWRITE_TAC[EVEN;ODD;real_pow];
434 DISCH_THEN (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
435 REWRITE_TAC[EVEN;ODD;real_pow;NOT_EVEN;NOT_ODD];
436 DISJ_CASES_TAC (ISPEC `n:num` EVEN_OR_ODD);
439 ASM_REWRITE_TAC[real_gt;REAL_MUL_GT];
440 ASM_MESON_TAC[EVEN_AND_ODD];
441 ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
442 ASM_MESON_TAC[real_gt];
444 ASM_REWRITE_TAC[real_gt;REAL_MUL_LT;REAL_MUL_GT];
447 ASM_MESON_TAC[EVEN_AND_ODD];
452 let EVEN_ODD_POW = prove_by_refinement(
454 (EVEN n ==> a pow n > &0) /\
455 (ODD n ==> a < &0 ==> a pow n < &0) /\
456 (ODD n ==> a > &0 ==> a pow n > &0)`,
460 REPEAT_N 2 STRIP_TAC;
461 CLAIM `a < &0 \/ a > &0 \/ (a = &0)`;
466 ASM_MESON_TAC[PARITY_POW_LT];
467 ASM_MESON_TAC[PARITY_POW_LT];
468 ASM_MESON_TAC[REAL_POW_LT;real_gt];
470 ASM_MESON_TAC[REAL_POW_LT;real_gt];
471 EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
472 ASM_MESON_TAC[REAL_POW_LT;real_gt];