extreal_baseScript.sml
1(* ------------------------------------------------------------------------- *)
2(* Extended Real Numbers - Basic Theory *)
3(* *)
4(* Original Authors: Tarek Mhamdi, Osman Hasan, Sofiene Tahar (2013, 2015) *)
5(* HVG Group, Concordia University, Montreal *)
6(* ------------------------------------------------------------------------- *)
7(* Updated and further enriched by Chun Tian (2018 - 2025) *)
8(* ------------------------------------------------------------------------- *)
9Theory extreal_base
10Ancestors
11 combin prim_rec arithmetic real iterate real_sigma real_of_rat pred_set
12Libs
13 tautLib numLib hurdUtils realLib
14
15val _ = intLib.deprecate_int ();
16val _ = ratLib.deprecate_rat ();
17
18Datatype : (* extreal_TY_DEF *)
19 extreal = NegInf | PosInf | Normal real
20End
21
22val extreal_11 = DB.fetch "-" "extreal_11";
23
24(* INFINITY, the vertical position of UTF8.chr 0x2212 is better than "-" *)
25val _ = Unicode.unicode_version {u = "+" ^ UTF8.chr 0x221E,
26 tmnm = "PosInf"};
27val _ = Unicode.unicode_version {u = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
28 tmnm = "NegInf"};
29
30val _ = TeX_notation {hol = "+" ^ UTF8.chr 0x221E,
31 TeX = ("\\ensuremath{+\\infty}", 1)};
32
33val _ = TeX_notation {hol = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
34 TeX = ("\\ensuremath{-\\infty}", 1)};
35
36Definition extreal_of_num_def :
37 extreal_of_num n = Normal (&n)
38End
39
40(* from now on, ``0x`` is intepreted as ``0 :extreal`` *)
41val _ = add_numeral_form (#"x", SOME "extreal_of_num");
42
43Definition real_def :
44 real x = if (x = NegInf) \/ (x = PosInf) then (0 :real)
45 else @r. x = Normal r
46End
47
48Theorem real_normal[simp] :
49 !x. real (Normal x) = x
50Proof
51 RW_TAC std_ss [real_def]
52QED
53
54Theorem real_infty[simp] :
55 real PosInf = 0 /\ real NegInf = 0
56Proof
57 SIMP_TAC std_ss [real_def]
58QED
59
60Theorem normal_real :
61 !x. x <> NegInf /\ x <> PosInf ==> (Normal (real x) = x)
62Proof
63 RW_TAC std_ss [real_def]
64 >> SELECT_ELIM_TAC
65 >> RW_TAC std_ss []
66 >> Cases_on `x`
67 >> METIS_TAC []
68QED
69
70Theorem extreal_cases :
71 !x. (x = NegInf) \/ (x = PosInf) \/ (?r. x = Normal r)
72Proof
73 Cases >> RW_TAC std_ss []
74QED
75
76Theorem extreal_not_infty[simp] :
77 !x. (Normal x <> NegInf) /\ (Normal x <> PosInf)
78Proof
79 RW_TAC std_ss []
80QED
81
82val extreal_distinct = DB.fetch "-" "extreal_distinct";
83
84Theorem extreal_eq_zero[simp] :
85 !x. (Normal x = 0) <=> (x = 0)
86Proof
87 RW_TAC std_ss [extreal_of_num_def]
88QED
89
90Theorem num_not_infty[simp] :
91 !n. (&n <> NegInf) /\ (&n <> PosInf)
92Proof
93 RW_TAC std_ss [extreal_of_num_def]
94QED
95
96Theorem real_0[simp] :
97 real 0 = 0
98Proof
99 rw [extreal_of_num_def]
100QED
101
102Theorem normal_0:
103 Normal 0 = 0
104Proof
105 rw [extreal_of_num_def]
106QED
107
108Theorem normal_1:
109 Normal 1 = 1
110Proof
111 rw [extreal_of_num_def]
112QED
113
114(* ------------------------------------------------------------------------- *)
115(* Definitions of Arithmetic Operations *)
116(* ------------------------------------------------------------------------- *)
117
118(* old definition, which (wrongly) allows `PosInf + NegInf = PosInf`:
119
120val extreal_add_def = Define
121 `(extreal_add (Normal x) (Normal y) = Normal (x + y)) /\
122 (extreal_add PosInf a = PosInf) /\
123 (extreal_add a PosInf = PosInf) /\
124 (extreal_add NegInf b = NegInf) /\
125 (extreal_add c NegInf = NegInf)`;
126
127 new definition:
128 *)
129Definition extreal_add_def :
130 (extreal_add (Normal x) (Normal y) = Normal (x + y)) /\
131 (extreal_add (Normal _) a = a) /\
132 (extreal_add b (Normal _) = b) /\
133 (extreal_add NegInf NegInf = NegInf) /\
134 (extreal_add PosInf PosInf = PosInf)
135End
136
137(* This definition never changed but is moved here to be used by extreal_sub *)
138Definition extreal_ainv_def :
139 (extreal_ainv NegInf = PosInf) /\
140 (extreal_ainv PosInf = NegInf) /\
141 (extreal_ainv (Normal x) = Normal (- x))
142End
143
144(* old definition, which (wrongly) allows `PosInf - PosInf = PosInf` and
145 `NegInf - NegInf = PosInf`:
146
147val extreal_sub_def = Define
148 `(extreal_sub (Normal x) (Normal y) = Normal (x - y)) /\
149 (extreal_sub PosInf a = PosInf) /\
150 (extreal_sub b PosInf = NegInf) /\
151 (extreal_sub NegInf NegInf = PosInf) /\
152 (extreal_sub NegInf c = NegInf) /\
153 (extreal_sub c NegInf = PosInf)`;
154
155 new definition:
156 *)
157Definition extreal_sub :
158 extreal_sub x y = extreal_add x (extreal_ainv y)
159End
160
161(* The previous definition now becomes a theorem *)
162Theorem extreal_sub_def :
163 (extreal_sub (Normal x) (Normal y) = Normal (x - y)) /\
164 (extreal_sub PosInf (Normal x) = PosInf) /\
165 (extreal_sub NegInf (Normal x) = NegInf) /\
166 (extreal_sub (Normal x) NegInf = PosInf) /\
167 (extreal_sub (Normal x) PosInf = NegInf) /\
168 (extreal_sub NegInf PosInf = NegInf) /\
169 (extreal_sub PosInf NegInf = PosInf)
170Proof
171 rw [extreal_sub, extreal_add_def, extreal_ainv_def, real_sub]
172QED
173
174Definition extreal_le_def :
175 (extreal_le (Normal x) (Normal y) = (x <= y)) /\
176 (extreal_le NegInf _ = T) /\
177 (extreal_le _ PosInf = T) /\
178 (extreal_le _ NegInf = F) /\
179 (extreal_le PosInf _ = F)
180End
181
182Definition extreal_lt_def :
183 extreal_lt x y = ~extreal_le y x
184End
185
186(* "The rationaly behind our definitions is to understand PosInf (or
187 NegInf) in every instance as the limit of some (possibly each time
188 different) sequence, and '0' as a bona fide zero. Then
189
190 `0 * PosInf (or NegInf) = 0 * lim a_n = lim (0 * a_n) = lim 0 = 0`
191
192 while expressions of the type `PosInf - PosInf` or `PosInf / PosInf`
193 become `lim (a_n - b_n)` or `lim a_n / lim b_n` where two
194 sequences compete and do not lead to unique results." [1, p.58]
195 *)
196Definition extreal_mul_def :
197 (extreal_mul NegInf NegInf = PosInf) /\
198 (extreal_mul NegInf PosInf = NegInf) /\
199 (extreal_mul PosInf NegInf = NegInf) /\
200 (extreal_mul PosInf PosInf = PosInf) /\
201 (extreal_mul (Normal x) NegInf =
202 (if x = 0 then (Normal 0) else (if 0 < x then NegInf else PosInf))) /\
203 (extreal_mul NegInf (Normal y) =
204 (if y = 0 then (Normal 0) else (if 0 < y then NegInf else PosInf))) /\
205 (extreal_mul (Normal x) PosInf =
206 (if x = 0 then (Normal 0) else (if 0 < x then PosInf else NegInf))) /\
207 (extreal_mul PosInf (Normal y) =
208 (if y = 0 then (Normal 0) else (if 0 < y then PosInf else NegInf))) /\
209 (extreal_mul (Normal x) (Normal y) = Normal (x * y))
210End
211
212Overload "+" = “extreal_add”
213Overload "-" = “extreal_sub”
214Overload "*" = “extreal_mul”
215Overload "<=" = “extreal_le”
216
217(* old definition, which allows `extreal_inv (Normal 0) = Normal 0`:
218
219val extreal_inv_def = Define
220 `(extreal_inv NegInf = Normal 0) /\
221 (extreal_inv PosInf = Normal 0) /\
222 (extreal_inv (Normal x) = Normal (inv x)`;
223
224 new definition, where `extreal_inv 0` is *unspecified*:
225 *)
226local
227 val thm = Q.prove (
228 `?f. (f NegInf = Normal 0) /\
229 (f PosInf = Normal 0) /\
230 (!r. r <> 0 ==> (f (Normal r) = Normal (inv r)))`,
231 (* proof *)
232 Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
233 else if x = Normal 0 then ARB
234 else Normal (inv (real x))` \\
235 RW_TAC std_ss [extreal_not_infty, real_normal]);
236in
237 (* |- extreal_inv NegInf = Normal 0 /\
238 extreal_inv PosInf = Normal 0 /\
239 !r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
240 *)
241 val extreal_inv_def = new_specification
242 ("extreal_inv_def", ["extreal_inv"], thm);
243end;
244
245(* old definition, which "deliberately" allows `0 / 0 = 0` [3]
246val extreal_div_def = Define
247 `extreal_div x y = extreal_mul x (extreal_inv y)`;
248
249 new definition, where `x / 0`, `PosInf / PosInf` and `NegInf / NegInf`
250 are all *unspecified*:
251 *)
252local
253 val thm = Q.prove (
254 `?f. (!r. f (Normal r) PosInf = Normal 0) /\
255 (!r. f (Normal r) NegInf = Normal 0) /\
256 (!x r. r <> 0 ==> (f x (Normal r) = extreal_mul x (extreal_inv (Normal r))))`,
257 (* proof *)
258 Q.EXISTS_TAC `\x y.
259 if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
260 else if y = Normal 0 then ARB
261 else extreal_mul x (extreal_inv y)` \\
262 RW_TAC std_ss [extreal_not_infty, real_normal]);
263in
264 (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
265 (!r. extreal_div (Normal r) NegInf = Normal 0) /\
266 !x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
267 *)
268 val extreal_div_def = new_specification
269 ("extreal_div_def", ["extreal_div"], thm);
270end;
271
272Definition extreal_abs_def :
273 (extreal_abs (Normal x) = Normal (abs x)) /\
274 (extreal_abs _ = PosInf)
275End
276
277Definition extreal_pow_def :
278 (extreal_pow (Normal a) n = Normal (a pow n)) /\
279 (extreal_pow PosInf n = (if n = 0 then Normal 1 else PosInf)) /\
280 (extreal_pow NegInf n =
281 (if n = 0 then Normal 1 else (if (EVEN n) then PosInf else NegInf)))
282End
283
284Theorem extreal_pow_eq = cj 1 extreal_pow_def
285
286Definition extreal_sqrt_def :
287 (extreal_sqrt (Normal x) = Normal (sqrt x)) /\
288 (extreal_sqrt PosInf = PosInf)
289End
290
291Overload "/" = “extreal_div”
292Overload "<" = “extreal_lt”
293Overload "~" = “extreal_ainv”
294Overload numeric_negate = “extreal_ainv”
295Overload "~" = “bool$~”
296Overload "¬" = “bool$~”
297Overload inv = “extreal_inv”
298Overload realinv = “extreal_inv”
299Overload abs = “extreal_abs”
300Overload pow = “extreal_pow”
301Overload sqrt = “extreal_sqrt”
302
303(* pow-2 integrals appear in Variances and many other probability lemmas *)
304val _ = overload_on (UnicodeChars.sup_2, “\x :extreal. x pow 2”);
305
306(* pow-3 integrals appear in Liapounov's form of the central limit theorem *)
307val _ = overload_on (UnicodeChars.sup_3, “\x :extreal. x pow 3”);
308
309(* pow-4 integrals appear in Cantelli's Strong Law of Large Numbers *)
310val _ = add_rule {fixity = Suffix 2100,
311 term_name = UnicodeChars.sup_4,
312 block_style = (AroundEachPhrase,(PP.CONSISTENT, 0)),
313 paren_style = ParoundPrec,
314 pp_elements = [TOK UnicodeChars.sup_4]};
315
316val _ = overload_on (UnicodeChars.sup_4, “\x :extreal. x pow 4”);
317val _ = TeX_notation {hol = UnicodeChars.sup_4,
318 TeX = ("\\HOLTokenSupFour{}", 1)};
319
320Definition extreal_min_def :
321 extreal_min (x :extreal) y = if x <= y then x else y
322End
323
324Definition extreal_max_def :
325 extreal_max (x :extreal) y = if x <= y then y else x
326End
327
328Overload min = “extreal_min”
329Overload max = “extreal_max”
330
331(* ------------------------------------------------------------------------- *)
332(* Addition *)
333(* ------------------------------------------------------------------------- *)
334
335Theorem extreal_add_eq :
336 !x y. Normal x + Normal y = Normal (x + y)
337Proof
338 rw [extreal_add_def]
339QED
340
341(* added two antecedents due to new definition of ``extreal_add``, excluded cases are:
342 1. x = NegInf /\ y = PosInf
343 2. x = PosInf /\ y = NegInf *)
344Theorem add_comm :
345 !x y. (x <> NegInf /\ y <> NegInf) \/ (x <> PosInf /\ y <> PosInf) ==>
346 (x + y = y + x)
347Proof
348 Cases >> Cases_on `y`
349 >> RW_TAC std_ss [extreal_add_def, REAL_ADD_COMM]
350QED
351
352Theorem add_comm_normal :
353 !x y. Normal x + y = y + Normal x
354Proof
355 rpt STRIP_TAC
356 >> Cases_on `y`
357 >> RW_TAC std_ss [extreal_add_def, REAL_ADD_COMM]
358QED
359
360(* added two antecedents due to new definition of ``extreal_add``, excluded cases are:
361 - all mixes of PosInf and NegInf in x, y and z.
362 *)
363Theorem add_assoc :
364 !x y z. (x <> NegInf /\ y <> NegInf /\ z <> NegInf) \/
365 (x <> PosInf /\ y <> PosInf /\ z <> PosInf) ==>
366 (x + (y + z) = x + y + z)
367Proof
368 Cases >> Cases_on `y` >> Cases_on `z`
369 >> RW_TAC std_ss [extreal_add_def, REAL_ADD_ASSOC]
370QED
371
372Theorem add_rzero[simp] :
373 !x :extreal. x + 0 = x
374Proof
375 Cases >> METIS_TAC [extreal_add_def, extreal_of_num_def, REAL_ADD_RID]
376QED
377
378Theorem add_lzero[simp] :
379 !x :extreal. 0 + x = x
380Proof
381 Cases >> METIS_TAC [extreal_add_def, extreal_of_num_def, REAL_ADD_LID]
382QED
383
384(* added one antecedent in the first part due to new definition of ``extreal_add`` *)
385Theorem add_infty :
386 (!x. x <> NegInf ==> ((x + PosInf = PosInf) /\ (PosInf + x = PosInf))) /\
387 (!x. x <> PosInf ==> ((x + NegInf = NegInf) /\ (NegInf + x = NegInf)))
388Proof
389 RW_TAC std_ss [] >> Cases_on `x`
390 >> RW_TAC std_ss [extreal_add_def, extreal_not_infty]
391QED
392
393Theorem add_not_infty :
394 !x y. (x <> NegInf /\ y <> NegInf ==> x + y <> NegInf) /\
395 (x <> PosInf /\ y <> PosInf ==> x + y <> PosInf)
396Proof
397 NTAC 2 Cases >> RW_TAC std_ss [extreal_add_def]
398QED
399
400Theorem EXTREAL_EQ_LADD :
401 !x y z. x <> NegInf /\ x <> PosInf ==> ((x + y = x + z) <=> (y = z))
402Proof
403 NTAC 3 Cases
404 >> RW_TAC std_ss [extreal_add_def, REAL_EQ_LADD]
405QED
406
407Theorem EXTREAL_EQ_RADD :
408 !x y z. z <> NegInf /\ z <> PosInf ==> ((x + z = y + z) <=> (x = y))
409Proof
410 NTAC 3 Cases
411 >> RW_TAC std_ss [extreal_add_def, REAL_EQ_RADD]
412QED
413
414Theorem extreal_double : (* cf. realTheory.REAL_DOUBLE *)
415 !(x :extreal). x + x = 2 * x
416Proof
417 Cases
418 >> rw [extreal_of_num_def, extreal_add_def, extreal_mul_def, REAL_DOUBLE]
419QED
420
421(* ------------------------------------------------------------------------- *)
422(* Ordering *)
423(* ------------------------------------------------------------------------- *)
424
425(* |- !x y. ~(y <= x) <=> x < y *)
426Theorem extreal_not_le = GSYM extreal_lt_def
427
428Theorem extreal_not_lt :
429 !x y:extreal. ~(x < y) <=> y <= x
430Proof
431 REWRITE_TAC [TAUT `(~a <=> b) <=> (a <=> ~b)`] THEN
432 SIMP_TAC std_ss [extreal_lt_def]
433QED
434
435Theorem extreal_lt_eq :
436 !x y. Normal x < Normal y <=> x < y
437Proof
438 METIS_TAC [extreal_lt_def, extreal_le_def, real_lt]
439QED
440
441Theorem extreal_le_eq :
442 !x y. Normal x <= Normal y <=> x <= y
443Proof
444 METIS_TAC [extreal_le_def]
445QED
446
447Theorem le_refl[simp] :
448 !x:extreal. x <= x
449Proof
450 Cases >> RW_TAC std_ss [extreal_le_def, REAL_LE_REFL]
451QED
452
453Theorem lt_refl[simp] :
454 !x:extreal. ~(x < x)
455Proof
456 RW_TAC std_ss [extreal_lt_def, le_refl]
457QED
458
459Theorem le_infty :
460 (!x. NegInf <= x /\ x <= PosInf) /\
461 (!x. x <= NegInf <=> (x = NegInf)) /\
462 (!x. PosInf <= x <=> (x = PosInf))
463Proof
464 RW_TAC std_ss []
465 >> Cases_on `x`
466 >> RW_TAC std_ss [extreal_le_def]
467QED
468
469(* NOTE: The statements of this theorem were slightly refined when moving
470 here from extrealTheory. Old statements:
471
472 |- !x y. NegInf < Normal y /\ Normal y < PosInf /\
473 NegInf < PosInf /\ ~(x < NegInf) /\ ~(PosInf < x) /\
474 (x <> PosInf <=> x < PosInf) /\ (x <> NegInf <=> NegInf < x)
475 *)
476Theorem lt_infty :
477 NegInf < PosInf /\
478 (!x. NegInf < Normal x /\ Normal x < PosInf) /\
479 (!x. ~(x < NegInf) /\ ~(PosInf < x)) /\
480 (!x. x <> PosInf <=> x < PosInf) /\
481 (!x. x <> NegInf <=> NegInf < x)
482Proof
483 rpt STRIP_TAC
484 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, lt_refl]
485 >> Cases_on ‘x’
486 >> fs [extreal_lt_def, extreal_le_def, lt_refl]
487QED
488
489Theorem lt_imp_le :
490 !x y :extreal. x < y ==> x <= y
491Proof
492 NTAC 2 Cases
493 >> RW_TAC std_ss [lt_refl, le_refl, extreal_lt_def, extreal_le_def]
494 >> METIS_TAC [real_lt, REAL_LT_IMP_LE]
495QED
496
497Theorem lt_imp_ne :
498 !x y :extreal. x < y ==> x <> y
499Proof
500 NTAC 2 Cases
501 >> RW_TAC std_ss [lt_refl, le_refl, extreal_lt_def, extreal_le_def]
502 >> METIS_TAC [real_lt, REAL_LT_IMP_NE]
503QED
504
505Theorem le_trans :
506 !x y z :extreal. x <= y /\ y <= z ==> x <= z
507Proof
508 NTAC 3 Cases
509 >> RW_TAC std_ss [extreal_le_def,le_refl]
510 >> METIS_TAC [REAL_LE_TRANS]
511QED
512
513Theorem lt_trans :
514 !x y z :extreal. x < y /\ y < z ==> x < z
515Proof
516 NTAC 3 Cases
517 >> RW_TAC std_ss [extreal_lt_def, lt_refl, extreal_le_def, le_refl, GSYM real_lt]
518 >> METIS_TAC [REAL_LT_TRANS]
519QED
520
521Theorem let_trans :
522 !x y z:extreal. x <= y /\ y < z ==> x < z
523Proof
524 NTAC 3 Cases
525 >> RW_TAC std_ss [lt_refl, le_refl, extreal_lt_def, extreal_le_def]
526 >> METIS_TAC [real_lt,REAL_LET_TRANS]
527QED
528
529Theorem le_antisym :
530 !x y :extreal. (x <= y /\ y <= x) <=> (x = y)
531Proof
532 NTAC 2 Cases
533 >> RW_TAC std_ss [extreal_le_def, le_refl, REAL_LE_ANTISYM]
534QED
535
536Theorem lt_antisym :
537 !x y. ~(x < y /\ y < x)
538Proof
539 NTAC 2 Cases
540 >> RW_TAC std_ss [lt_infty, extreal_lt_eq]
541 >> METIS_TAC [REAL_LT_ANTISYM, DE_MORGAN_THM]
542QED
543
544Theorem lte_trans :
545 !x y z:extreal. x < y /\ y <= z ==> x < z
546Proof
547 NTAC 3 Cases
548 >> RW_TAC std_ss [lt_refl, le_refl, extreal_lt_def, extreal_le_def]
549 >> METIS_TAC [real_lt, REAL_LTE_TRANS]
550QED
551
552Theorem let_antisym :
553 !x y. ~(x < y /\ y <= x)
554Proof
555 rpt GEN_TAC
556 >> CCONTR_TAC >> fs []
557 >> `x < x` by PROVE_TAC [lte_trans]
558 >> PROVE_TAC [lt_refl]
559QED
560
561(* NOTE: The statements of this theorem were slightly refined when moving
562 here from extrealTheory. Old statements:
563
564 |- !x. (0 <= x ==> x <> NegInf) /\ (x <= 0 ==> x <> PosInf)
565*)
566Theorem le_not_infty :
567 (!x. 0 <= x ==> x <> NegInf) /\
568 (!x. x <= 0 ==> x <> PosInf)
569Proof
570 NTAC 3 STRIP_TAC
571 >> ONCE_REWRITE_TAC [lt_infty]
572 >| [ (* goal 1 (of 2) *)
573 MATCH_MP_TAC (Q.SPECL [`NegInf`, `0`, `x`] lte_trans) \\
574 PROVE_TAC [lt_infty, num_not_infty],
575 (* goal 2 (of 2) *)
576 MATCH_MP_TAC (Q.SPECL [`x`, `0`, `PosInf`] let_trans) \\
577 PROVE_TAC [lt_infty, num_not_infty] ]
578QED
579
580(* |- !x. 0 <= x ==> x <> NegInf, very useful in measureTheory *)
581Theorem pos_not_neginf = CONJUNCT1 le_not_infty
582
583(* |- !x. x <= 0 ==> x <> PosInf *)
584Theorem neg_not_posinf = CONJUNCT2 le_not_infty
585
586Theorem le_total :
587 !x y. x <= y \/ y <= x
588Proof
589 NTAC 2 Cases
590 >> RW_TAC std_ss [extreal_le_def, REAL_LE_TOTAL]
591QED
592
593Theorem lt_total :
594 !x y. (x = y) \/ x < y \/ y < x
595Proof
596 NTAC 2 Cases
597 >> RW_TAC std_ss [extreal_le_def, extreal_lt_def, GSYM real_lt, REAL_LT_TOTAL]
598QED
599
600Theorem le_01[simp] : 0 <= 1
601Proof
602 RW_TAC std_ss [extreal_of_num_def, extreal_le_eq, REAL_LE_01]
603QED
604
605Theorem lt_01[simp] : 0 < 1
606Proof
607 RW_TAC std_ss [extreal_of_num_def, extreal_lt_eq, REAL_LT_01]
608QED
609
610Theorem ne_01[simp] : 0 <> 1
611Proof
612 RW_TAC std_ss [extreal_of_num_def, REAL_10]
613QED
614
615Theorem le_02[simp] : 0 <= 2
616Proof
617 RW_TAC real_ss [extreal_of_num_def, extreal_le_eq]
618QED
619
620Theorem lt_02[simp] : 0 < 2
621Proof
622 RW_TAC real_ss [extreal_of_num_def, extreal_lt_eq]
623QED
624
625Theorem lt_10[simp] : -1 < 0
626Proof
627 RW_TAC real_ss [extreal_of_num_def, extreal_lt_eq, extreal_ainv_def]
628QED
629
630Theorem ne_02[simp] : 0 <> 2
631Proof
632 RW_TAC real_ss [extreal_of_num_def]
633QED
634
635(* NOTE: added [simp] when moving here from extrealTheory *)
636Theorem le_num[simp] :
637 !n:num. 0 <= &n
638Proof
639 RW_TAC real_ss [extreal_of_num_def, extreal_le_def]
640QED
641
642Theorem num_lt_infty[simp] :
643 !n:num. &n < PosInf
644Proof
645 RW_TAC std_ss [extreal_of_num_def, lt_infty]
646QED
647
648Theorem lt_le :
649 !x y. x < y <=> (x <= y /\ x <> y)
650Proof
651 NTAC 2 Cases
652 >> RW_TAC std_ss [extreal_lt_eq, extreal_le_def, lt_infty, le_infty, REAL_LT_LE]
653QED
654
655Theorem le_lt :
656 !x y. (x <= y) <=> x < y \/ (x = y)
657Proof
658 NTAC 2 Cases
659 >> RW_TAC std_ss [extreal_lt_eq, extreal_le_def, lt_infty, le_infty, REAL_LE_LT]
660QED
661
662Theorem le_neg :
663 !x y. -x <= -y <=> y <= x
664Proof
665 NTAC 2 Cases
666 >> RW_TAC std_ss [extreal_lt_eq, extreal_le_def, extreal_ainv_def, lt_infty, le_infty,
667 REAL_LE_NEG]
668QED
669
670Theorem lt_neg :
671 !x y. -x < -y <=> y < x
672Proof
673 NTAC 2 Cases
674 >> RW_TAC std_ss [extreal_lt_eq, extreal_le_def, extreal_ainv_def, lt_infty,le_infty,
675 REAL_LT_NEG]
676QED
677
678Theorem le_add :
679 !x y :extreal. 0 <= x /\ 0 <= y ==> 0 <= x + y
680Proof
681 NTAC 2 Cases
682 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_of_num_def, REAL_LE_ADD]
683QED
684
685Theorem lt_add :
686 !x y :extreal. 0 < x /\ 0 < y ==> 0 < x + y
687Proof
688 NTAC 2 Cases
689 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_of_num_def]
690 >> METIS_TAC [real_lt, REAL_LT_ADD]
691QED
692
693Theorem let_add :
694 !x y:extreal. 0 <= x /\ 0 < y ==> 0 < x + y
695Proof
696 NTAC 2 Cases
697 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_of_num_def]
698 >> METIS_TAC [real_lt, REAL_LET_ADD]
699QED
700
701Theorem lte_add :
702 !x y:extreal. 0 < x /\ 0 <= y ==> 0 < x + y
703Proof
704 NTAC 2 Cases
705 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_of_num_def]
706 >> METIS_TAC [real_lt, REAL_LTE_ADD]
707QED
708
709Theorem le_add2 :
710 !w x y z. w <= x /\ y <= z ==> w + y <= x + z
711Proof
712 NTAC 4 Cases
713 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, le_infty, le_refl]
714 >> METIS_TAC [REAL_LE_ADD2]
715QED
716
717Theorem lt_add2 :
718 !w x y z. w < x /\ y < z ==> w + y < x + z
719Proof
720 rpt Cases
721 >> RW_TAC std_ss [extreal_add_def, extreal_lt_eq, lt_infty, REAL_LT_ADD2]
722QED
723
724Theorem let_add2 :
725 !w x y z. w <> NegInf /\ w <> PosInf /\ w <= x /\ y < z ==> w + y < x + z
726Proof
727 NTAC 4 Cases
728 >> RW_TAC std_ss [extreal_le_def, extreal_lt_def, extreal_add_def, le_infty, le_refl]
729 >> METIS_TAC [real_lt, REAL_LET_ADD2]
730QED
731
732Theorem let_add2_alt :
733 !w x y z. x <> NegInf /\ x <> PosInf /\ w <= x /\ y < z ==> w + y < x + z
734Proof
735 NTAC 4 Cases
736 >> RW_TAC std_ss [extreal_le_def, extreal_lt_def, extreal_add_def, le_infty, le_refl]
737 >> METIS_TAC [real_lt, REAL_LET_ADD2]
738QED
739
740(* This theorem is newly added in extreal_baseTheory *)
741Theorem le_addl :
742 !x y. y <> NegInf /\ y <> PosInf ==> (y <= x + y <=> (0 <= x))
743Proof
744 rpt Cases
745 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, le_infty, extreal_of_num_def,
746 extreal_not_infty, REAL_LE_ADDL]
747QED
748
749Theorem le_addr :
750 !x y. x <> NegInf /\ x <> PosInf ==> (x <= x + y <=> (0 <= y))
751Proof
752 rpt Cases
753 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, le_infty, extreal_of_num_def,
754 extreal_not_infty, REAL_LE_ADDR]
755QED
756
757Theorem le_addl_imp :
758 !x y. 0 <= x ==> y <= x + y
759Proof
760 rpt Cases
761 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, le_infty, extreal_of_num_def,
762 extreal_not_infty, REAL_LE_ADDL]
763QED
764
765Theorem le_addr_imp :
766 !x y. 0 <= y ==> x <= x + y
767Proof
768 rpt Cases
769 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, le_infty, extreal_of_num_def,
770 extreal_not_infty, REAL_LE_ADDR]
771QED
772
773Theorem le_ladd :
774 !x y z. x <> NegInf /\ x <> PosInf ==> (x + y <= x + z <=> y <= z)
775Proof
776 rpt Cases
777 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, REAL_LE_LADD]
778QED
779
780Theorem le_radd :
781 !x y z. x <> NegInf /\ x <> PosInf ==> (y + x <= z + x <=> y <= z)
782Proof
783 rpt Cases
784 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, REAL_LE_RADD]
785QED
786
787Theorem le_radd_imp :
788 !x y z. y <= z ==> y + x <= z + x
789Proof
790 rpt Cases
791 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, REAL_LE_RADD, le_infty, le_refl]
792QED
793
794Theorem le_ladd_imp :
795 !x y z. y <= z ==> x + y <= x + z
796Proof
797 rpt Cases
798 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, REAL_LE_LADD, le_infty, le_refl]
799QED
800
801Theorem lt_ladd :
802 !x y z. x <> NegInf /\ x <> PosInf ==> (x + y < x + z <=> y < z)
803Proof
804 rpt Cases
805 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, extreal_lt_def, REAL_LE_LADD]
806QED
807
808Theorem lt_radd :
809 !x y z. x <> NegInf /\ x <> PosInf ==> (y + x < z + x <=> y < z)
810Proof
811 rpt Cases
812 >> RW_TAC std_ss [extreal_add_def, extreal_le_def, extreal_lt_def, REAL_LE_RADD]
813QED
814
815Theorem lt_addl :
816 !x y. y <> NegInf /\ y <> PosInf ==> (y < x + y <=> 0 < x)
817Proof
818 rpt Cases
819 >> RW_TAC std_ss [extreal_add_def, extreal_lt_def, extreal_le_def,
820 le_infty, extreal_of_num_def, extreal_not_infty]
821 >> REAL_ARITH_TAC
822QED
823
824(* This theorem is newly added in extreal_baseTheory *)
825Theorem lt_addr :
826 !x y. x <> NegInf /\ x <> PosInf ==> (x < x + y <=> 0 < y)
827Proof
828 rpt Cases
829 >> RW_TAC std_ss [extreal_add_def, extreal_lt_def, extreal_le_def,
830 le_infty, extreal_of_num_def, extreal_not_infty]
831 >> REAL_ARITH_TAC
832QED
833
834(* NOTE: two antecedents were added due to new definitions of ‘extreal_add’ *)
835Theorem le_lneg :
836 !x y. ((x <> NegInf /\ y <> NegInf) \/
837 (x <> PosInf /\ y <> PosInf)) ==> (-x <= y <=> 0 <= x + y)
838Proof
839 rpt Cases
840 >> RW_TAC std_ss [extreal_ainv_def, extreal_le_def, extreal_add_def, extreal_sub_def,
841 le_infty, extreal_of_num_def, extreal_not_infty, REAL_LE_LNEG]
842QED
843
844Theorem let_total :
845 !x y :extreal. x <= y \/ y < x
846Proof
847 rpt GEN_TAC
848 >> STRIP_ASSUME_TAC (Q.SPECL [`x`, `y`] lt_total)
849 >- (DISJ1_TAC >> REWRITE_TAC [le_lt] >> art [])
850 >- (DISJ1_TAC >> MATCH_MP_TAC lt_imp_le >> art [])
851 >> DISJ2_TAC >> art []
852QED
853
854Theorem lte_total :
855 !x y :extreal. x < y \/ y <= x
856Proof
857 rpt GEN_TAC
858 >> STRIP_ASSUME_TAC (Q.SPECL [`x`, `y`] lt_total)
859 >- (DISJ2_TAC >> REWRITE_TAC [le_lt] >> art [])
860 >- (DISJ1_TAC >> art [])
861 >> DISJ2_TAC >> MATCH_MP_TAC lt_imp_le >> art []
862QED
863
864(* |- !x y. x <= 0 /\ y <= 0 ==> x + y <= 0 *)
865Theorem le_add_neg =
866 (Q.GENL [`x`, `y`] (REWRITE_RULE [add_rzero] (Q.SPECL [`x`, `0`, `y`, `0`] le_add2)))
867
868(* |- !x y. x < 0 /\ y < 0 ==> x + y < 0 *)
869Theorem lt_add_neg =
870 (Q.GENL [`x`, `y`] (REWRITE_RULE [add_rzero] (Q.SPECL [`x`, `0`, `y`, `0`] lt_add2)))
871
872(* |- !x y. x <> NegInf /\ x <> PosInf /\ 0 < y ==> x < x + y *)
873Theorem lt_addr_imp =
874 (Q.GENL [`x`, `y`]
875 (REWRITE_RULE [le_refl, add_rzero] (Q.SPECL [`x`, `x`, `0`, `y`] let_add2)))
876
877(* ------------------------------------------------------------------------- *)
878(* Substraction (often with order) *)
879(* ------------------------------------------------------------------------- *)
880
881Theorem extreal_sub_eq :
882 !x y. Normal x - Normal y = Normal (x - y)
883Proof
884 rw [extreal_sub_def]
885QED
886
887Theorem sub_rzero[simp] :
888 !x :extreal. x - 0 = x
889Proof
890 Cases >> METIS_TAC [extreal_sub_def, extreal_of_num_def, REAL_SUB_RZERO]
891QED
892
893Theorem sub_lzero[simp] :
894 !x :extreal. 0 - x = -x
895Proof
896 Cases
897 >> METIS_TAC [extreal_ainv_def, extreal_sub_def, extreal_of_num_def, REAL_SUB_LZERO]
898QED
899
900Theorem sub_le_imp :
901 !x y z. x <> NegInf /\ x <> PosInf /\ y <= z + x ==> y - x <= z
902Proof
903 rpt Cases
904 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
905 REAL_LE_SUB_RADD]
906QED
907
908Theorem sub_le_imp2 :
909 !x y z. y <> NegInf /\ y <> PosInf /\ y <= z + x ==> y - x <= z
910Proof
911 rpt Cases
912 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
913 REAL_LE_SUB_RADD]
914QED
915
916Theorem le_sub_imp :
917 !x y z. x <> NegInf /\ x <> PosInf /\ y + x <= z ==> y <= z - x
918Proof
919 rpt Cases
920 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
921 REAL_LE_SUB_LADD]
922QED
923
924Theorem le_sub_imp2 : (* new *)
925 !x y z. z <> NegInf /\ z <> PosInf /\ y + x <= z ==> y <= z - x
926Proof
927 rpt Cases
928 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
929 REAL_LE_SUB_LADD]
930QED
931
932Theorem lt_sub_imp :
933 !x y z. x <> NegInf /\ y <> NegInf /\ y + x < z ==> y < z - x
934Proof
935 rpt Cases
936 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
937 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_ADD_SUB]
938QED
939
940Theorem lt_sub_imp' :
941 !x y z. x <> PosInf /\ y <> PosInf /\ y + x < z ==> y < z - x
942Proof
943 rpt Cases
944 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
945 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_ADD_SUB]
946QED
947
948Theorem lt_sub_imp2 : (* new *)
949 !x y z. x <> NegInf /\ x <> PosInf /\ y + x < z ==> y < z - x
950Proof
951 rpt Cases
952 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
953 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_ADD_SUB]
954QED
955
956Theorem sub_lt_imp :
957 !x y z. x <> NegInf /\ x <> PosInf /\ y < z + x ==> y - x < z
958Proof
959 rpt Cases
960 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
961 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_SUB_RADD]
962QED
963
964Theorem sub_lt_eq :
965 !x y z. x <> NegInf /\ x <> PosInf ==> (y - x < z <=> y < z + x)
966Proof
967 rpt STRIP_TAC
968 >> reverse EQ_TAC >- PROVE_TAC [sub_lt_imp]
969 >> Cases_on `x` >> Cases_on `y` >> Cases_on `z`
970 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
971 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_SUB_RADD]
972QED
973
974Theorem sub_lt_imp2 :
975 !x y z. z <> NegInf /\ z <> PosInf /\ y < z + x ==> y - x < z
976Proof
977 rpt Cases
978 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def, extreal_sub_def]
979 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_SUB_RADD]
980QED
981
982Theorem sub_zero_lt :
983 !x y. x < y ==> 0 < y - x
984Proof
985 rpt Cases
986 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def, extreal_lt_eq,
987 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_SUB_LT]
988QED
989
990Theorem sub_zero_lt2 :
991 !x y. x <> NegInf /\ x <> PosInf /\ 0 < y - x ==> x < y
992Proof
993 rpt Cases
994 >> RW_TAC real_ss [extreal_le_def,extreal_add_def,extreal_sub_def, extreal_lt_eq,
995 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_SUB_LT]
996QED
997
998Theorem sub_lt_zero :
999 !x y. x < y ==> x - y < 0
1000Proof
1001 rpt Cases
1002 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def, extreal_lt_eq,
1003 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_LT_SUB_RADD]
1004QED
1005
1006Theorem sub_lt_zero2 :
1007 !x y. y <> NegInf /\ y <> PosInf /\ x - y < 0 ==> x < y
1008Proof
1009 rpt Cases
1010 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def, extreal_lt_eq,
1011 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_LT_SUB_RADD]
1012QED
1013
1014(* more antecedents added *)
1015Theorem sub_zero_le :
1016 !x y. x <> NegInf /\ x <> PosInf ==> (x <= y <=> 0 <= y - x)
1017Proof
1018 rpt Cases
1019 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
1020 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_SUB_LE]
1021QED
1022
1023Theorem sub_le_zero :
1024 !x y. y <> NegInf /\ y <> PosInf ==> (x <= y <=> x - y <= 0)
1025Proof
1026 rpt Cases
1027 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def,
1028 lt_infty, extreal_of_num_def, extreal_not_infty, REAL_LE_SUB_RADD]
1029QED
1030
1031Theorem le_sub_eq :
1032 !x y z. x <> NegInf /\ x <> PosInf ==> (y <= z - x <=> y + x <= z)
1033Proof
1034 METIS_TAC [le_sub_imp, sub_lt_imp, extreal_lt_def]
1035QED
1036
1037Theorem le_sub_eq2 :
1038 !x y z. z <> NegInf /\ z <> PosInf /\ x <> NegInf /\ y <> NegInf ==>
1039 (y <= z - x <=> y + x <= z)
1040Proof
1041 rpt Cases
1042 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def, lt_infty,
1043 extreal_of_num_def, extreal_not_infty, REAL_LE_SUB_LADD]
1044QED
1045
1046Theorem sub_le_eq :
1047 !x y z. x <> NegInf /\ x <> PosInf ==> (y - x <= z <=> y <= z + x)
1048Proof
1049 METIS_TAC [sub_le_imp, lt_sub_imp2, extreal_lt_def]
1050QED
1051
1052Theorem sub_le_eq2 :
1053 !x y z. y <> NegInf /\ y <> PosInf /\ x <> NegInf /\ z <> NegInf ==>
1054 (y - x <= z <=> y <= z + x)
1055Proof
1056 rpt Cases
1057 >> RW_TAC real_ss [extreal_le_def, extreal_add_def, extreal_sub_def, lt_infty,
1058 extreal_of_num_def, extreal_not_infty, REAL_LE_SUB_RADD]
1059QED
1060
1061Theorem sub_le_switch :
1062 !x y z. x <> NegInf /\ x <> PosInf /\ z <> NegInf /\ z <> PosInf ==>
1063 (y - x <= z <=> y - z <= x)
1064Proof
1065 NTAC 3 Cases
1066 >> RW_TAC std_ss [extreal_sub_def, extreal_le_def, le_infty, lt_infty]
1067 >> REAL_ARITH_TAC
1068QED
1069
1070Theorem sub_le_switch2 :
1071 !x y z. x <> NegInf /\ x <> PosInf /\ y <> NegInf /\ y <> PosInf ==>
1072 (y - x <= z <=> y - z <= x)
1073Proof
1074 NTAC 3 Cases
1075 >> RW_TAC std_ss [extreal_sub_def, extreal_le_def, le_infty, lt_infty]
1076 >> REAL_ARITH_TAC
1077QED
1078
1079(* more antecedents ‘x <> NegInf /\ y <> NegInf’ added *)
1080Theorem lt_sub :
1081 !x y z. x <> NegInf /\ y <> NegInf /\ z <> NegInf /\ z <> PosInf ==>
1082 (y + x < z <=> y < z - x)
1083Proof
1084 rpt Cases
1085 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def,
1086 extreal_sub_def, le_infty]
1087 >> METIS_TAC [REAL_LE_SUB_RADD]
1088QED
1089
1090Theorem lt_sub' :
1091 !x y z. x <> PosInf /\ y <> PosInf /\ z <> NegInf /\ z <> PosInf ==>
1092 (y + x < z <=> y < z - x)
1093Proof
1094 rpt Cases
1095 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def,
1096 extreal_sub_def, le_infty]
1097 >> METIS_TAC [REAL_LE_SUB_RADD]
1098QED
1099
1100Theorem sub_add2 :
1101 !x y. x <> NegInf /\ x <> PosInf ==> (x + (y - x) = y)
1102Proof
1103 rpt Cases
1104 >> RW_TAC std_ss [extreal_le_def, extreal_add_def, extreal_sub_def, REAL_SUB_ADD2]
1105QED
1106
1107Theorem add_sub :
1108 !x y. y <> NegInf /\ y <> PosInf ==> (x + y - y = x)
1109Proof
1110 rpt Cases
1111 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def,
1112 extreal_sub_def, REAL_ADD_SUB_ALT]
1113QED
1114
1115Theorem add_sub_normal[simp] :
1116 !x r. x + Normal r - Normal r = x
1117Proof
1118 rpt GEN_TAC
1119 >> MATCH_MP_TAC add_sub
1120 >> REWRITE_TAC [extreal_not_infty]
1121QED
1122
1123Theorem add_sub2 :
1124 !x y. y <> NegInf /\ y <> PosInf ==> (y + x - y = x)
1125Proof
1126 rpt Cases
1127>> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def,
1128 extreal_sub_def, REAL_ADD_SUB]
1129QED
1130
1131Theorem sub_add :
1132 !x y. y <> NegInf /\ y <> PosInf ==> (x - y + y = x)
1133Proof
1134 rpt Cases
1135 >> RW_TAC std_ss [extreal_lt_def, extreal_le_def, extreal_add_def,
1136 extreal_sub_def, REAL_SUB_ADD]
1137QED
1138
1139Theorem sub_add_normal[simp] :
1140 !x r. x - Normal r + Normal r = x
1141Proof
1142 rpt GEN_TAC
1143 >> MATCH_MP_TAC sub_add
1144 >> REWRITE_TAC [extreal_not_infty]
1145QED
1146
1147(* NOTE: this theorem is for compatibility purposes only, cf. extreal_sub *)
1148Theorem extreal_sub_add :
1149 !x y. (x <> NegInf /\ y <> PosInf) \/ (x <> PosInf /\ y <> NegInf) ==>
1150 (x - y = x + -y)
1151Proof
1152 rpt Cases
1153 >> RW_TAC std_ss [extreal_ainv_def, extreal_sub_def, extreal_add_def, real_sub]
1154QED
1155
1156Theorem sub_0 :
1157 !x y :extreal. (x - y = 0) ==> (x = y)
1158Proof
1159 rpt Cases >> simp[extreal_sub_def]
1160QED
1161
1162Theorem sub_eq_0 :
1163 !x y. x <> PosInf /\ x <> NegInf /\ (x = y) ==> (x - y = 0)
1164Proof
1165 RW_TAC std_ss []
1166 >> `?a. x = Normal a` by METIS_TAC [extreal_cases]
1167 >> simp[extreal_of_num_def, extreal_sub_def, REAL_SUB_REFL]
1168QED
1169
1170Theorem sub_not_infty :
1171 !x y. (x <> NegInf /\ y <> PosInf ==> x - y <> NegInf) /\
1172 (x <> PosInf /\ y <> NegInf ==> x - y <> PosInf)
1173Proof
1174 rpt Cases >> RW_TAC std_ss [extreal_sub_def]
1175QED
1176
1177(* ------------------------------------------------------------------------- *)
1178(* Negation *)
1179(* ------------------------------------------------------------------------- *)
1180
1181Theorem neg_neg[simp] :
1182 !x. --x = x
1183Proof
1184 Cases >> RW_TAC std_ss [extreal_ainv_def, REAL_NEG_NEG]
1185QED
1186
1187Theorem neg_0[simp] :
1188 -0 = 0
1189Proof
1190 RW_TAC real_ss [extreal_ainv_def, extreal_of_num_def]
1191QED
1192
1193Theorem neg_eq0[simp] :
1194 !x :extreal. (-x = 0) <=> (x = 0)
1195Proof
1196 Cases
1197 >> RW_TAC std_ss [extreal_ainv_def, extreal_of_num_def, REAL_NEG_EQ0]
1198QED
1199
1200Theorem eq_neg[simp] :
1201 !x y :extreal. (-x = -y) <=> (x = y)
1202Proof
1203 NTAC 2 Cases >> RW_TAC std_ss [extreal_ainv_def, REAL_EQ_NEG]
1204QED
1205
1206(* NOTE: using this theorem directly in any rewriting tactics will cause a self loop,
1207 while (GSYM neg_minus1) is more useful in turning ‘-1 * x’ to -x.
1208 *)
1209Theorem neg_minus1 :
1210 !x. -x = -1 * x
1211Proof
1212 Cases
1213 >> RW_TAC real_ss [extreal_ainv_def, extreal_of_num_def, extreal_mul_def]
1214QED
1215
1216Theorem neg_minus1' :
1217 !x. -x = Normal (-1) * x
1218Proof
1219 rw [Once neg_minus1, extreal_of_num_def, extreal_ainv_def]
1220QED
1221
1222(* NOTE: the original unconditional statement is recovered *)
1223Theorem sub_rneg :
1224 !x y :extreal. x - -y = x + y
1225Proof
1226 rw [extreal_sub, neg_neg]
1227QED
1228
1229Theorem sub_lneg :
1230 !x y. (x <> NegInf /\ y <> NegInf) \/ (x <> PosInf /\ y <> PosInf) ==>
1231 (-x - y = -(x + y))
1232Proof
1233 rpt Cases
1234 >> RW_TAC std_ss [extreal_sub_def, extreal_add_def, extreal_ainv_def, REAL_SUB_LNEG]
1235QED
1236
1237Theorem neg_add :
1238 !x y. (x <> NegInf /\ y <> NegInf) \/ (x <> PosInf /\ y <> PosInf) ==>
1239 (-(x + y) = -x + -y)
1240Proof
1241 rpt Cases
1242 >> RW_TAC std_ss [extreal_sub_def, extreal_add_def, extreal_ainv_def, REAL_NEG_ADD]
1243QED
1244
1245Theorem neg_sub :
1246 !x y. (x <> NegInf /\ x <> PosInf) \/ (y <> NegInf /\ y <> PosInf) ==>
1247 (-(x - y) = y - x)
1248Proof
1249 rpt Cases
1250 >> RW_TAC std_ss [extreal_sub_def, extreal_ainv_def, REAL_NEG_SUB]
1251QED
1252
1253Theorem le_lsub_imp :
1254 !x y z. y <= z ==> x - z <= x - y
1255Proof
1256 rpt Cases
1257 >> RW_TAC std_ss [extreal_le_def, extreal_sub_def, le_infty, le_refl]
1258 >> METIS_TAC [real_sub, REAL_LE_ADD2, REAL_LE_NEG, REAL_LE_REFL]
1259QED
1260
1261Theorem lt_lsub_imp :
1262 !x y z. x <> PosInf /\ x <> NegInf /\ y < z ==> x - z < x - y
1263Proof
1264 rpt STRIP_TAC
1265 >> ‘?r. x = Normal r’ by METIS_TAC [extreal_cases]
1266 >> POP_ASSUM (fs o wrap)
1267 >> Cases_on ‘y’ >> Cases_on ‘z’
1268 >> rw [extreal_sub_def, lt_infty]
1269 >> fs [lt_infty, lt_refl, extreal_lt_eq]
1270 >> RealArith.REAL_ASM_ARITH_TAC
1271QED
1272
1273Theorem lt_lsub :
1274 !x y z. x <> PosInf /\ x <> NegInf ==> (x - z < x - y <=> y < z)
1275Proof
1276 rw [extreal_sub]
1277 >> ‘y < z <=> -z < -y’ by rw [lt_neg] >> POP_ORW
1278 >> MATCH_MP_TAC lt_ladd >> art []
1279QED
1280
1281Theorem le_rsub_imp :
1282 !x y z. x <= y ==> x - z <= y - z
1283Proof
1284 rpt Cases
1285 >> RW_TAC std_ss [extreal_le_def, extreal_sub_def, le_infty, le_refl]
1286 >> METIS_TAC [real_sub, REAL_LE_ADD2, REAL_LE_NEG, REAL_LE_REFL]
1287QED
1288
1289Theorem le_rsub :
1290 !x y z. z <> PosInf /\ z <> NegInf ==> (x - z <= y - z <=> x <= y)
1291Proof
1292 rw [extreal_sub]
1293 >> MATCH_MP_TAC le_radd
1294 >> ‘?r. z = Normal r’ by METIS_TAC [extreal_cases]
1295 >> rw [extreal_ainv_def, extreal_not_infty]
1296QED
1297
1298Theorem lt_rsub_imp :
1299 !x y z. z <> PosInf /\ z <> NegInf /\ x < y ==> x - z < y - z
1300Proof
1301 rpt STRIP_TAC
1302 >> ‘?r. z = Normal r’ by METIS_TAC [extreal_cases]
1303 >> POP_ASSUM (fs o wrap)
1304 >> Cases_on ‘x’ >> Cases_on ‘y’
1305 >> rw [extreal_sub_def, lt_infty]
1306 >> fs [lt_infty, lt_refl, extreal_lt_eq]
1307 >> RealArith.REAL_ASM_ARITH_TAC
1308QED
1309
1310Theorem lt_rsub :
1311 !x y z. z <> PosInf /\ z <> NegInf ==> (x - z < y - z <=> x < y)
1312Proof
1313 rw [extreal_sub]
1314 >> MATCH_MP_TAC lt_radd
1315 >> ‘?r. z = Normal r’ by METIS_TAC [extreal_cases]
1316 >> rw [extreal_ainv_def, extreal_not_infty]
1317QED
1318
1319Theorem eq_sub_ladd_normal :
1320 !x y z. (x = y - Normal z) <=> (x + Normal z = y)
1321Proof
1322 NTAC 2 Cases
1323 >> RW_TAC std_ss [extreal_le_def, extreal_sub_def, le_infty, le_refl,
1324 extreal_add_def, REAL_EQ_SUB_LADD]
1325QED
1326
1327Theorem eq_sub_radd :
1328 !x y z. y <> NegInf /\ y <> PosInf ==> ((x - y = z) <=> (x = z + y))
1329Proof
1330 rpt Cases
1331 >> RW_TAC std_ss [extreal_add_def, extreal_sub_def, REAL_EQ_SUB_RADD]
1332QED
1333
1334Theorem eq_sub_ladd :
1335 !x y z. z <> NegInf /\ z <> PosInf ==> ((x = y - z) <=> (x + z = y))
1336Proof
1337 rpt Cases
1338 >> RW_TAC std_ss [extreal_add_def, extreal_sub_def, REAL_EQ_SUB_LADD]
1339QED
1340
1341Theorem eq_sub_switch :
1342 !x y z. (x = Normal z - y) <=> (y = Normal z - x)
1343Proof
1344 NTAC 2 Cases
1345 >> RW_TAC std_ss [extreal_le_def, extreal_sub_def, le_infty, le_refl, extreal_add_def]
1346 >> REAL_ARITH_TAC
1347QED
1348
1349Theorem eq_add_sub_switch :
1350 !a b c d. b <> NegInf /\ b <> PosInf /\ c <> NegInf /\ c <> PosInf ==>
1351 ((a + b = c + d) <=> (a - c = d - b))
1352Proof
1353 rpt Cases
1354 >> RW_TAC std_ss [extreal_add_def,extreal_sub_def]
1355 >> REAL_ARITH_TAC
1356QED
1357
1358Theorem sub_refl :
1359 !x. x <> NegInf /\ x <> PosInf ==> x - x = 0
1360Proof
1361 Cases >> RW_TAC real_ss [extreal_sub_def, extreal_of_num_def]
1362QED
1363
1364Theorem sub_infty :
1365 (!x. x <> NegInf ==> (x - NegInf = PosInf)) /\
1366 (!x. x <> PosInf ==> (x - PosInf = NegInf)) /\
1367 (!x. x <> PosInf ==> (PosInf - x = PosInf)) /\
1368 (!x. x <> NegInf ==> (NegInf - x = NegInf))
1369Proof
1370 RW_TAC std_ss []
1371 >> Cases_on `x` >> FULL_SIMP_TAC std_ss [extreal_sub_def]
1372QED
1373
1374(* ------------------------------------------------------------------------- *)
1375(* Multiplication *)
1376(* ------------------------------------------------------------------------- *)
1377
1378Theorem extreal_mul_eq :
1379 !x y. extreal_mul (Normal x) (Normal y) = Normal (x * y)
1380Proof
1381 rw [extreal_mul_def]
1382QED
1383
1384Theorem mul_comm :
1385 !x y:extreal. x * y = y * x
1386Proof
1387 NTAC 2 Cases
1388 >> RW_TAC std_ss [extreal_mul_def, REAL_MUL_COMM]
1389QED
1390
1391Theorem mul_assoc :
1392 !x y z:extreal. x * (y * z) = x * y * z
1393Proof
1394 NTAC 3 Cases
1395 >> RW_TAC real_ss [extreal_mul_def, REAL_MUL_ASSOC, REAL_MUL_LZERO,
1396 REAL_MUL_RZERO, REAL_ENTIRE, REAL_LT_LMUL_0, REAL_POS_NZ,
1397 DE_MORGAN_THM]
1398 >> FULL_SIMP_TAC real_ss [DE_MORGAN_THM, REAL_NOT_LT, REAL_LT_LMUL_0, GSYM REAL_LT_LE]
1399 >> METIS_TAC [REAL_LT_LMUL_0_NEG, REAL_LT_RMUL_0_NEG, REAL_LT_RMUL_NEG_0,
1400 REAL_LT_LE, REAL_LT_GT, REAL_ENTIRE, REAL_LT_LMUL_NEG_0,
1401 REAL_LT_LMUL_NEG_0_NEG, REAL_LT_RMUL_0, REAL_LT_LMUL_0,
1402 REAL_LT_RMUL_NEG_0_NEG]
1403QED
1404
1405Theorem mul_rzero[simp] :
1406 !x :extreal. x * 0 = 0
1407Proof
1408 Cases
1409 >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, REAL_MUL_RZERO]
1410QED
1411
1412Theorem mul_lzero[simp] :
1413 !x :extreal. 0 * x = 0
1414Proof
1415 Cases
1416 >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, REAL_MUL_LZERO]
1417QED
1418
1419Theorem mul_rone[simp] :
1420 !x :extreal. x * 1 = x
1421Proof
1422 Cases
1423 >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, REAL_MUL_RID]
1424QED
1425
1426Theorem mul_lone[simp] :
1427 !x :extreal. 1 * x = x
1428Proof
1429 Cases
1430 >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, REAL_MUL_LID]
1431QED
1432
1433Theorem entire[simp] : (* was: mul2_zero *)
1434 !x y :extreal. (x * y = 0) <=> (x = 0) \/ (y = 0)
1435Proof
1436 rpt Cases >> rw[extreal_mul_def]
1437QED
1438
1439Theorem le_mul :
1440 !x y :extreal. 0 <= x /\ 0 <= y ==> 0 <= x * y
1441Proof
1442 NTAC 2 Cases
1443 >> RW_TAC std_ss [extreal_le_def, extreal_mul_def, extreal_of_num_def,
1444 REAL_LE_MUL, GSYM real_lt]
1445 >> METIS_TAC [REAL_LT_LE, real_lte]
1446QED
1447
1448Theorem let_mul :
1449 !x y :extreal. 0 <= x /\ 0 < y ==> 0 <= x * y
1450Proof
1451 rpt Cases
1452 >> RW_TAC real_ss [extreal_mul_def, extreal_le_def, extreal_lt_eq, lt_infty,
1453 le_infty, le_refl, extreal_of_num_def]
1454 >> METIS_TAC [real_lt, REAL_LT_LE, REAL_LT_IMP_LE, REAL_LE_MUL]
1455QED
1456
1457Theorem lte_mul :
1458 !x y :extreal. 0 < x /\ 0 <= y ==> 0 <= x * y
1459Proof
1460 rpt Cases
1461 >> RW_TAC real_ss [extreal_mul_def, extreal_le_def, extreal_lt_eq,
1462 lt_infty, le_infty, le_refl, extreal_of_num_def]
1463 >> METIS_TAC [real_lt, REAL_LT_LE, REAL_LT_IMP_LE, REAL_LE_MUL]
1464QED
1465
1466Theorem le_mul_neg :
1467 !x y :extreal. x <= 0 /\ y <= 0 ==> 0 <= x * y
1468Proof
1469 NTAC 2 Cases
1470 >> RW_TAC std_ss [extreal_le_def, extreal_mul_def, extreal_of_num_def,
1471 REAL_LE_MUL, GSYM real_lt]
1472 >> METIS_TAC [REAL_LE_NEG, REAL_NEG_0, REAL_NEG_MUL2, REAL_MUL_RZERO,
1473 REAL_LE_MUL]
1474QED
1475
1476Theorem mul_le :
1477 !x y :extreal. 0 <= x /\ y <= 0 ==> x * y <= 0
1478Proof
1479 NTAC 2 Cases
1480 >> RW_TAC std_ss [extreal_le_def, extreal_mul_def, extreal_of_num_def,
1481 REAL_LE_MUL, GSYM real_lt]
1482 >- METIS_TAC [REAL_LT_LE, real_lt]
1483 >> `0 <= -r'` by METIS_TAC [REAL_LE_NEG, REAL_NEG_0]
1484 >> METIS_TAC [REAL_LE_NEG, REAL_NEG_0, REAL_LE_MUL, REAL_MUL_RNEG]
1485QED
1486
1487Theorem lt_mul :
1488 !x y:extreal. 0 < x /\ 0 < y ==> 0 < x * y
1489Proof
1490 NTAC 2 Cases
1491 >> RW_TAC std_ss [extreal_lt_eq, extreal_mul_def, extreal_of_num_def,
1492 REAL_LT_MUL, lt_infty]
1493QED
1494
1495Theorem lt_mul_neg :
1496 !x y :extreal. x < 0 /\ y < 0 ==> 0 < x * y
1497Proof
1498 rpt Cases
1499 >> RW_TAC real_ss [extreal_of_num_def, extreal_lt_eq, lt_infty, extreal_mul_def]
1500 >> METIS_TAC [REAL_LT_LE, real_lt, REAL_LT_NEG, REAL_NEG_0, REAL_NEG_MUL2,
1501 REAL_LT_MUL]
1502QED
1503
1504Theorem mul_lt :
1505 !x y:extreal. 0 < x /\ y < 0 ==> x * y < 0
1506Proof
1507 NTAC 2 Cases
1508 >> RW_TAC std_ss [extreal_lt_eq, extreal_mul_def, extreal_of_num_def,
1509 REAL_LT_MUL, lt_infty]
1510 >- METIS_TAC [REAL_LT_LE, real_lt]
1511 >> `0 < -r'` by METIS_TAC [REAL_LT_NEG, REAL_NEG_0]
1512 >> METIS_TAC [REAL_MUL_RNEG, REAL_LT_MUL, REAL_LT_NEG, REAL_NEG_0]
1513QED
1514
1515Theorem mul_let :
1516 !x y :extreal. 0 <= x /\ y < 0 ==> x * y <= 0
1517Proof
1518 NTAC 2 Cases
1519 >> RW_TAC real_ss [extreal_lt_eq, extreal_mul_def, extreal_of_num_def,
1520 lt_infty, extreal_le_def, le_refl, le_infty]
1521 >> METIS_TAC [REAL_LT_NEG, REAL_LT_IMP_LE, REAL_NEG_0, REAL_LE_MUL, real_lt,
1522 REAL_MUL_RNEG, REAL_NEG_NEG, REAL_LE_NEG, REAL_LT_LE]
1523QED
1524
1525Theorem mul_lte :
1526 !x y :extreal. 0 < x /\ y <= 0 ==> x * y <= 0
1527Proof
1528 NTAC 2 Cases
1529 >> RW_TAC real_ss [extreal_lt_eq, extreal_mul_def, extreal_of_num_def,
1530 lt_infty, extreal_le_def, le_refl, le_infty]
1531 >> METIS_TAC [REAL_LT_NEG, REAL_LT_IMP_LE, REAL_NEG_0, REAL_LE_MUL,
1532 REAL_MUL_RNEG, REAL_NEG_NEG, REAL_LE_NEG, real_lt, REAL_LT_LE]
1533QED
1534
1535Theorem lt_rmul :
1536 !x y z. 0 < z /\ z <> PosInf ==> (x * z < y * z <=> x < y)
1537Proof
1538 rpt Cases
1539 >> RW_TAC real_ss [extreal_lt_eq, extreal_mul_def, le_infty, lt_infty,
1540 REAL_LT_REFL, REAL_LT_RMUL, extreal_of_num_def]
1541QED
1542
1543Theorem lt_rmul_imp :
1544 !x y z. x < y /\ 0 < z /\ z <> PosInf ==> x * z < y * z
1545Proof
1546 METIS_TAC [lt_rmul]
1547QED
1548
1549Theorem le_rmul :
1550 !x y z. 0 < z /\ z <> PosInf ==> (x * z <= y * z <=> x <= y)
1551Proof
1552 rpt Cases
1553 >> RW_TAC real_ss [extreal_le_eq, extreal_mul_def, le_infty, extreal_of_num_def,
1554 REAL_LE_REFL, REAL_LE_RMUL, lt_infty, extreal_lt_eq]
1555QED
1556
1557Theorem le_rmul_imp :
1558 !x y z :extreal. 0 <= z /\ x <= y ==> x * z <= y * z
1559Proof
1560 RW_TAC std_ss []
1561 >> Cases_on `z = 0` >- RW_TAC std_ss [mul_rzero, le_refl]
1562 >> `0 < z` by METIS_TAC [lt_le]
1563 >> reverse (Cases_on ‘z = PosInf’) >- METIS_TAC [le_rmul]
1564 >> fs [le_infty, lt_infty, extreal_of_num_def]
1565 >> Cases_on `x` >> Cases_on `y`
1566 >> RW_TAC real_ss [extreal_le_def, extreal_lt_eq, extreal_mul_def,
1567 REAL_LE_REFL, REAL_LT_REFL, GSYM real_lte, GSYM real_lt,
1568 le_infty, lt_infty, extreal_of_num_def, REAL_LT_IMP_LE]
1569 >> FULL_SIMP_TAC std_ss [le_infty, extreal_not_infty]
1570 >> METIS_TAC [REAL_LT_LE, REAL_LTE_TRANS, extreal_le_eq, REAL_LET_ANTISYM]
1571QED
1572
1573Theorem lt_mul2 :
1574 !x1 x2 y1 y2. 0 <= x1 /\ 0 <= y1 /\ x1 <> PosInf /\ y1 <> PosInf /\
1575 x1 < x2 /\ y1 < y2 ==> x1 * y1 < x2 * y2
1576Proof
1577 RW_TAC std_ss []
1578 >> `0 < x2 /\ 0 < y2` by METIS_TAC [let_trans]
1579 >> Cases_on `x1` >> Cases_on `y1`
1580 >> Cases_on `x2` >> Cases_on `y2`
1581 >> FULL_SIMP_TAC real_ss [extreal_lt_eq, extreal_le_def, extreal_mul_def,
1582 le_infty, lt_infty, real_lte, REAL_LT_MUL2,
1583 extreal_of_num_def, extreal_not_infty]
1584 >> METIS_TAC [extreal_not_infty,lt_infty]
1585QED
1586
1587Theorem mul_lposinf :
1588 !x. 0 < x ==> (PosInf * x = PosInf)
1589Proof
1590 Cases >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, lt_infty,
1591 num_not_infty, extreal_lt_eq]
1592QED
1593
1594Theorem mul_rposinf :
1595 !x. 0 < x ==> (x * PosInf = PosInf)
1596Proof
1597 Cases >> RW_TAC real_ss [extreal_mul_def, extreal_of_num_def, lt_infty,
1598 num_not_infty, extreal_lt_eq]
1599QED
1600
1601Theorem mul_infty :
1602 !x. 0 < x ==> (PosInf * x = PosInf) /\ (x * PosInf = PosInf) /\
1603 (NegInf * x = NegInf) /\ (x * NegInf = NegInf)
1604Proof
1605 GEN_TAC >> DISCH_TAC
1606 >> STRONG_CONJ_TAC
1607 >- (Cases_on ‘x’ >> rw [extreal_mul_def] \\
1608 fs [lt_infty, extreal_of_num_def, extreal_lt_eq] \\
1609 PROVE_TAC [REAL_LT_ANTISYM])
1610 >> DISCH_TAC
1611 >> CONJ_TAC >- art [Once mul_comm]
1612 >> STRONG_CONJ_TAC
1613 >- (Cases_on ‘x’ >> rw [extreal_mul_def] \\
1614 fs [lt_infty, extreal_of_num_def, extreal_lt_eq] \\
1615 PROVE_TAC [REAL_LT_ANTISYM])
1616 >> REWRITE_TAC [Once mul_comm]
1617QED
1618
1619Theorem mul_infty' :
1620 !x. x < 0 ==> (PosInf * x = NegInf) /\ (x * PosInf = NegInf) /\
1621 (NegInf * x = PosInf) /\ (x * NegInf = PosInf)
1622Proof
1623 GEN_TAC >> DISCH_TAC
1624 >> STRONG_CONJ_TAC
1625 >- (Cases_on ‘x’ >> rw [extreal_mul_def] \\
1626 fs [lt_infty, extreal_of_num_def, extreal_lt_eq] \\
1627 PROVE_TAC [REAL_LT_ANTISYM])
1628 >> DISCH_TAC
1629 >> CONJ_TAC >- art [Once mul_comm]
1630 >> STRONG_CONJ_TAC
1631 >- (Cases_on ‘x’ >> rw [extreal_mul_def] \\
1632 fs [lt_infty, extreal_of_num_def, extreal_lt_eq] \\
1633 PROVE_TAC [REAL_LT_ANTISYM])
1634 >> REWRITE_TAC [Once mul_comm]
1635QED
1636
1637Theorem mul_not_infty :
1638 (!c y. 0 <= c /\ y <> NegInf ==> Normal (c) * y <> NegInf) /\
1639 (!c y. 0 <= c /\ y <> PosInf ==> Normal (c) * y <> PosInf) /\
1640 (!c y. c <= 0 /\ y <> NegInf ==> Normal (c) * y <> PosInf) /\
1641 (!c y. c <= 0 /\ y <> PosInf ==> Normal (c) * y <> NegInf)
1642Proof
1643 RW_TAC std_ss [] >> Cases_on `y`
1644 >> RW_TAC std_ss [extreal_mul_def, extreal_le_def]
1645 >> METIS_TAC [real_lte, REAL_LE_ANTISYM]
1646QED
1647
1648Theorem mul_not_infty2 :
1649 !x y. x <> NegInf /\ x <> PosInf /\ y <> NegInf /\ y <> PosInf ==>
1650 (x * y <> NegInf) /\ (x * y <> PosInf)
1651Proof
1652 rpt Cases
1653 >> RW_TAC std_ss [extreal_mul_def, extreal_not_infty]
1654QED
1655
1656Theorem mul_lt2 :
1657 !x y :extreal. x < 0 /\ 0 < y ==> x * y < 0
1658Proof
1659 METIS_TAC [mul_comm, mul_lt]
1660QED
1661
1662Theorem mul_le2 :
1663 !x y :extreal. x <= 0 /\ 0 <= y ==> x * y <= 0
1664Proof
1665 METIS_TAC [mul_comm, mul_le]
1666QED
1667
1668Theorem add_ldistrib_pos :
1669 !x y z. 0 <= y /\ 0 <= z ==> (x * (y + z) = x * y + x * z)
1670Proof
1671 NTAC 3 Cases
1672 >> RW_TAC real_ss [extreal_add_def, extreal_mul_def, extreal_le_def,
1673 extreal_of_num_def, real_lt, REAL_LT_ANTISYM,
1674 REAL_LE_ANTISYM, REAL_ADD_LID, REAL_ADD_RID, REAL_LT_LE]
1675 >> FULL_SIMP_TAC real_ss [GSYM real_lt, GSYM real_lte]
1676 >> METIS_TAC [REAL_LE_ANTISYM, REAL_LT_ADD, REAL_LT_IMP_LE, REAL_LT_IMP_NE,
1677 REAL_LT_LE, REAL_ADD_LDISTRIB]
1678QED
1679
1680Theorem add_ldistrib_neg :
1681 !x y z. y <= 0 /\ z <= 0 ==> (x * (y + z) = x * y + x * z)
1682Proof
1683 NTAC 3 Cases (* 27 sub-goals here *)
1684 >> RW_TAC real_ss [extreal_add_def, extreal_mul_def, extreal_le_def,
1685 extreal_of_num_def, real_lt, REAL_LT_ANTISYM,
1686 REAL_LE_ANTISYM, REAL_ADD_LID, REAL_ADD_RID, REAL_LT_LE] (* 17 goals *)
1687 >> FULL_SIMP_TAC real_ss [GSYM real_lt, GSYM real_lte, REAL_ADD_LDISTRIB] (* 4 goals *)
1688 >> (Cases_on `0 < r` >- RW_TAC std_ss [] \\
1689 Cases_on `0 < r'` >- RW_TAC std_ss [] \\
1690 `r < 0 /\ r' < 0` by METIS_TAC [real_lte, REAL_LT_LE] \\
1691 METIS_TAC [REAL_LT_ADD2, REAL_ADD_LID, REAL_LT_IMP_NE, REAL_LT_ANTISYM])
1692QED
1693
1694(* changed var name from `x` to `r` *)
1695Theorem add_ldistrib_normal :
1696 !r y z. (y <> PosInf /\ z <> PosInf) \/ (y <> NegInf /\ z <> NegInf)
1697 ==> (Normal r * (y + z) = Normal r * y + Normal r * z)
1698Proof
1699 RW_TAC std_ss [] >> Cases_on `y` >> Cases_on `z`
1700 >> RW_TAC std_ss [extreal_add_def] (* 8 sub-goals here, same tacticals *)
1701 >> (Cases_on `r = 0`
1702 >- METIS_TAC [extreal_of_num_def, mul_lzero, add_lzero] \\
1703 RW_TAC std_ss [extreal_mul_def, extreal_add_def, REAL_ADD_LDISTRIB])
1704QED
1705
1706Theorem add_ldistrib_normal2 = add_ldistrib_normal (* backward compatible *)
1707
1708Theorem add_rdistrib_normal :
1709 !x y z. (y <> PosInf /\ z <> PosInf) \/ (y <> NegInf /\ z <> NegInf) ==>
1710 ((y + z) * Normal x = y * Normal x + z * Normal x)
1711Proof
1712 RW_TAC std_ss []
1713 >> Cases_on `y` >> Cases_on `z`
1714 >> RW_TAC std_ss [extreal_add_def]
1715 >> (Cases_on `x = 0`
1716 >- METIS_TAC [extreal_of_num_def, mul_rzero, add_rzero] \\
1717 RW_TAC std_ss [extreal_mul_def, extreal_add_def, REAL_ADD_RDISTRIB])
1718QED
1719
1720Theorem add_rdistrib_normal2 = add_rdistrib_normal (* backward compatible *)
1721
1722Theorem add_ldistrib :
1723 !x y z. (0 <= y /\ 0 <= z) \/ (y <= 0 /\ z <= 0) ==>
1724 (x * (y + z) = x * y + x * z)
1725Proof
1726 METIS_TAC [add_ldistrib_pos, add_ldistrib_neg]
1727QED
1728
1729Theorem add_rdistrib :
1730 !x y z. (0 <= y /\ 0 <= z) \/ (y <= 0 /\ z <= 0) ==>
1731 ((y + z) * x = y * x + z * x)
1732Proof
1733 METIS_TAC [add_ldistrib, mul_comm]
1734QED
1735
1736Theorem mul_lneg :
1737 !x y. -x * y = -(x * y)
1738Proof
1739 NTAC 2 Cases
1740 >> RW_TAC real_ss [extreal_ainv_def, extreal_mul_def, REAL_MUL_LNEG, REAL_NEG_EQ0]
1741 >> METIS_TAC [REAL_NEG_GT0, REAL_LT_REFL, REAL_LT_TRANS, real_lte, REAL_LE_ANTISYM]
1742QED
1743
1744Theorem mul_rneg :
1745 !x y. x * -y = -(x * y)
1746Proof
1747 NTAC 2 Cases
1748 >> RW_TAC real_ss [extreal_ainv_def, extreal_mul_def, REAL_MUL_RNEG, REAL_NEG_EQ0]
1749 >> METIS_TAC [REAL_NEG_GT0, REAL_LT_REFL, REAL_LT_TRANS, real_lte, REAL_LE_ANTISYM]
1750QED
1751
1752Theorem neg_mul2 :
1753 !x y. -x * -y = x * y
1754Proof
1755 rpt Cases >> RW_TAC real_ss [extreal_mul_def, extreal_ainv_def, REAL_NEG_EQ0]
1756 >> METIS_TAC [REAL_LT_NEG, REAL_NEG_0, REAL_LT_ANTISYM, real_lt, REAL_LE_ANTISYM]
1757QED
1758
1759(* NOTE: the number of necessary antecedents are reduced *)
1760Theorem add2_sub2 :
1761 !a b c d. a <> NegInf /\ b <> PosInf /\ c <> NegInf /\ d <> PosInf
1762 ==> a - b + (c - d) = a + c - (b + d)
1763Proof
1764 rpt Cases >> rw [extreal_sub_def, extreal_add_def, REAL_ADD2_SUB2]
1765QED
1766
1767Theorem add2_assoc :
1768 !a b c d. a <> NegInf /\ b <> NegInf /\ c <> NegInf /\ d <> NegInf
1769 ==> a + b + (c + d) = a + c + (b + d)
1770Proof
1771 rpt Cases >> rw [extreal_add_def]
1772 >> REAL_ARITH_TAC
1773QED
1774
1775Theorem sub_ldistrib :
1776 !x y z. x <> NegInf /\ x <> PosInf /\
1777 y <> NegInf /\ y <> PosInf /\
1778 z <> NegInf /\ z <> PosInf ==> (x * (y - z) = x * y - x * z)
1779Proof
1780 rpt Cases
1781 >> RW_TAC real_ss [extreal_add_def, extreal_sub_def, extreal_mul_def,
1782 REAL_SUB_LDISTRIB]
1783QED
1784
1785Theorem sub_rdistrib :
1786 !x y z. x <> NegInf /\ x <> PosInf /\
1787 y <> NegInf /\ y <> PosInf /\
1788 z <> NegInf /\ z <> PosInf ==> ((x - y) * z = x * z - y * z)
1789Proof
1790 rpt Cases
1791 >> RW_TAC real_ss [extreal_add_def, extreal_sub_def, extreal_mul_def,
1792 REAL_SUB_RDISTRIB]
1793QED
1794
1795Theorem mul_linv :
1796 !x. x <> 0 /\ x <> PosInf /\ x <> NegInf ==> (inv x * x = 1)
1797Proof
1798 Cases
1799 >> RW_TAC real_ss [extreal_div_def, extreal_mul_def, extreal_inv_def,
1800 extreal_not_infty, extreal_of_num_def, REAL_MUL_LINV]
1801QED
1802
1803Theorem mul_linv_pos :
1804 !x. 0 < x /\ x <> PosInf ==> (inv x * x = 1)
1805Proof
1806 rpt STRIP_TAC
1807 >> MATCH_MP_TAC mul_linv >> fs [lt_le]
1808 >> MATCH_MP_TAC pos_not_neginf >> art []
1809QED
1810
1811Theorem le_lmul :
1812 !x y z. 0 < x /\ x <> PosInf ==> (x * y <= x * z <=> y <= z)
1813Proof
1814 METIS_TAC [mul_comm, le_rmul]
1815QED
1816
1817Theorem le_lmul_imp :
1818 !x y z :extreal. 0 <= z /\ x <= y ==> z * x <= z * y
1819Proof
1820 METIS_TAC [mul_comm, le_rmul_imp]
1821QED
1822
1823Theorem lt_lmul :
1824 !x y z. 0 < x /\ x <> PosInf ==> (x * y < x * z <=> y < z)
1825Proof
1826 METIS_TAC [mul_comm, lt_rmul]
1827QED
1828
1829Theorem lt_lmul_imp :
1830 !x y z. 0 < x /\ x <> PosInf /\ y < z ==> x * y < x * z
1831Proof
1832 METIS_TAC [lt_lmul]
1833QED
1834
1835(* cf. REAL_LE_MUL2 *)
1836Theorem le_mul2 :
1837 !x1 x2 y1 y2. 0 <= x1 /\ 0 <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> x1 * y1 <= x2 * y2
1838Proof
1839 rpt STRIP_TAC
1840 >> MATCH_MP_TAC le_trans
1841 >> Q.EXISTS_TAC ‘x1 * y2’
1842 >> CONJ_TAC >- (MATCH_MP_TAC le_lmul_imp >> art [])
1843 >> MATCH_MP_TAC le_rmul_imp >> art []
1844 >> MATCH_MP_TAC le_trans
1845 >> Q.EXISTS_TAC ‘y1’ >> art []
1846QED
1847
1848(* ------------------------------------------------------------------------- *)
1849(* Absolute value (abs) *)
1850(* ------------------------------------------------------------------------- *)
1851
1852Theorem abs_0[simp] :
1853 extreal_abs 0 = 0
1854Proof
1855 simp[extreal_abs_def, extreal_of_num_def]
1856QED
1857
1858Theorem abs_pos[simp] :
1859 !x :extreal. 0 <= abs x
1860Proof
1861 Cases
1862 >> RW_TAC std_ss [extreal_abs_def, ABS_POS, extreal_le_def,
1863 extreal_of_num_def, le_infty]
1864QED
1865
1866Theorem abs_neg :
1867 !x :extreal. x < 0 ==> (abs x = -x)
1868Proof
1869 RW_TAC std_ss [extreal_lt_def]
1870 >> Cases_on `x`
1871 >- REWRITE_TAC [extreal_abs_def, extreal_ainv_def]
1872 >- fs [extreal_of_num_def, le_infty]
1873 >> fs [extreal_abs_def, extreal_of_num_def, extreal_le_eq, abs, extreal_ainv_def]
1874QED
1875
1876(* an enhanced version of abs_neg *)
1877Theorem abs_neg' :
1878 !x :extreal. x <= 0 ==> (abs x = -x)
1879Proof
1880 RW_TAC std_ss [le_lt]
1881 >- (MATCH_MP_TAC abs_neg >> art [])
1882 >> REWRITE_TAC [abs_0, neg_0]
1883QED
1884
1885Theorem abs_refl :
1886 !x :extreal. (abs x = x) <=> (0 <= x)
1887Proof
1888 Cases
1889 >> RW_TAC std_ss [extreal_abs_def, le_infty, extreal_of_num_def,
1890 extreal_le_def, ABS_REFL]
1891QED
1892
1893Theorem abs_abs[simp]:
1894 !x :extreal. abs(abs(x)) = abs(x)
1895Proof
1896 RW_TAC std_ss [abs_refl, abs_pos]
1897QED
1898
1899Theorem abs_real :
1900 !x. x <> PosInf /\ x <> NegInf ==> abs (real x) = real (abs x)
1901Proof
1902 Cases >> rw [extreal_abs_def, real_normal]
1903QED
1904
1905Theorem abs_bounds :
1906 !x k :extreal. abs x <= k <=> -k <= x /\ x <= k
1907Proof
1908 NTAC 2 Cases
1909 >> RW_TAC std_ss [extreal_abs_def, extreal_le_def, lt_infty,
1910 le_infty, extreal_ainv_def, ABS_BOUNDS]
1911QED
1912
1913Theorem abs_bounds_lt :
1914 !x k :extreal. abs x < k <=> -k < x /\ x < k
1915Proof
1916 NTAC 2 Cases
1917 >> RW_TAC std_ss [extreal_abs_def, extreal_lt_eq, lt_infty, le_infty,
1918 extreal_ainv_def, ABS_BOUNDS_LT]
1919QED
1920
1921Theorem lt_abs_bounds :
1922 !k x :extreal. k < abs x <=> x < -k \/ k < x
1923Proof
1924 RW_TAC std_ss [extreal_lt_def]
1925 >> PROVE_TAC [abs_bounds]
1926QED
1927
1928Theorem le_abs_bounds :
1929 !k x :extreal. k <= abs x <=> x <= -k \/ k <= x
1930Proof
1931 METIS_TAC [extreal_lt_def, abs_bounds_lt]
1932QED
1933
1934Theorem abs_not_infty :
1935 !x. x <> PosInf /\ x <> NegInf ==> abs x <> PosInf /\ abs x <> NegInf
1936Proof
1937 Q.X_GEN_TAC ‘x’ >> STRIP_TAC
1938 >> `?c. x = Normal c` by PROVE_TAC [extreal_cases]
1939 >> ASM_REWRITE_TAC [extreal_abs_def, extreal_not_infty]
1940QED
1941
1942(* NOTE: cf. le_abs_bounds for a better version without antecedents *)
1943Theorem abs_unbounds :
1944 !x k :extreal. 0 <= k ==> (k <= abs x <=> x <= -k \/ k <= x)
1945Proof
1946 rw [le_abs_bounds]
1947QED
1948
1949Theorem le_abs :
1950 !x :extreal. x <= abs x /\ -x <= abs x
1951Proof
1952 GEN_TAC
1953 >> `0 <= x \/ x < 0` by PROVE_TAC [let_total]
1954 >| [ (* goal 1 (of 2) *)
1955 `abs x = x` by PROVE_TAC [GSYM abs_refl] >> POP_ORW \\
1956 rw [le_refl] \\
1957 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0` >> art [] \\
1958 POP_ASSUM (REWRITE_TAC o wrap o
1959 (REWRITE_RULE [Once (GSYM le_neg), neg_0])),
1960 (* goal 2 (of 2) *)
1961 IMP_RES_TAC abs_neg >> POP_ORW \\
1962 rw [le_refl] \\
1963 MATCH_MP_TAC lt_imp_le \\
1964 MATCH_MP_TAC lt_trans >> Q.EXISTS_TAC `0` >> art [] \\
1965 POP_ASSUM (REWRITE_TAC o wrap o
1966 (REWRITE_RULE [Once (GSYM lt_neg), neg_0])) ]
1967QED
1968
1969Theorem abs_eq_0[simp] :
1970 !x. (abs x = 0) <=> (x = 0)
1971Proof
1972 GEN_TAC
1973 >> reverse EQ_TAC >- rw [abs_0]
1974 >> `0 <= abs x` by PROVE_TAC [abs_pos]
1975 >> rw [Once (GSYM le_antisym)]
1976 >> fs [REWRITE_RULE [neg_0, le_antisym] (Q.SPECL [`x`, `0`] abs_bounds)]
1977QED
1978
1979Theorem abs_not_zero :
1980 !x. abs x <> 0 <=> x <> 0
1981Proof
1982 PROVE_TAC [abs_eq_0]
1983QED
1984
1985Theorem abs_le_0[simp] :
1986 !x. abs x <= 0 <=> (x = 0)
1987Proof
1988 METIS_TAC [abs_pos, abs_eq_0, le_antisym]
1989QED
1990
1991Theorem abs_gt_0[simp] :
1992 !x. 0 < abs x <=> x <> 0
1993Proof
1994 RW_TAC std_ss [Once (GSYM abs_eq_0)]
1995 >> STRIP_ASSUME_TAC (REWRITE_RULE [le_lt] (Q.SPEC `x` abs_pos))
1996 >- fs [lt_le]
1997 >> FULL_SIMP_TAC std_ss [lt_refl]
1998QED
1999
2000Theorem abs_triangle :
2001 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
2002 abs(x + y) <= abs(x) + abs(y)
2003Proof
2004 RW_TAC std_ss []
2005 >> Cases_on `x` >> Cases_on `y`
2006 >> rw [extreal_abs_def, extreal_add_def, extreal_le_eq, ABS_TRIANGLE]
2007QED
2008
2009(* NOTE: although is possible that ‘x + y’ may be unspecific, this unspecific
2010 value is indeed <= PosInf
2011 *)
2012Theorem abs_triangle_full :
2013 !x y. abs(x + y) <= abs(x) + abs(y)
2014Proof
2015 rpt GEN_TAC
2016 >> Cases_on ‘x <> PosInf /\ x <> NegInf’
2017 >- (Cases_on ‘y <> PosInf /\ y <> NegInf’
2018 >- (MATCH_MP_TAC abs_triangle >> art []) \\
2019 ‘abs y = PosInf’ by fs [extreal_abs_def] >> POP_ORW \\
2020 Suff ‘abs x + PosInf = PosInf’ >- rw [le_infty] \\
2021 Suff ‘abs x <> NegInf’ >- METIS_TAC [add_infty] \\
2022 MATCH_MP_TAC pos_not_neginf >> rw [abs_pos])
2023 >> ‘abs x = PosInf’ by fs [extreal_abs_def] >> POP_ORW
2024 >> Suff ‘PosInf + abs y = PosInf’ >- rw [le_infty]
2025 >> Suff ‘abs y <> NegInf’ >- METIS_TAC [add_infty]
2026 >> MATCH_MP_TAC pos_not_neginf >> rw [abs_pos]
2027QED
2028
2029Theorem abs_triangle_sub :
2030 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
2031 abs(x) <= abs(y) + abs(x - y)
2032Proof
2033 RW_TAC std_ss []
2034 >> Cases_on `x` >> Cases_on `y`
2035 >> rw [extreal_abs_def, extreal_add_def, extreal_sub_def, extreal_le_eq,
2036 ABS_TRIANGLE_SUB]
2037QED
2038
2039Theorem abs_triangle_sub_full :
2040 !x y. abs(x) <= abs(y) + abs(x - y)
2041Proof
2042 rpt GEN_TAC
2043 >> Cases_on ‘x <> PosInf /\ x <> NegInf’
2044 >- (Cases_on ‘y <> PosInf /\ y <> NegInf’
2045 >- (MATCH_MP_TAC abs_triangle_sub >> art []) \\
2046 ‘abs y = PosInf’ by fs [extreal_abs_def] >> POP_ORW \\
2047 Suff ‘PosInf + abs (x - y) = PosInf’ >- rw [le_infty] \\
2048 Suff ‘abs (x - y) <> NegInf’ >- METIS_TAC [add_infty] \\
2049 MATCH_MP_TAC pos_not_neginf >> rw [abs_pos])
2050 >> ‘abs x = PosInf’ by fs [extreal_abs_def] >> POP_ORW
2051 >> Cases_on ‘y’
2052 >> fs [extreal_abs_def, extreal_sub_def, extreal_add_def] (* 2 subgoals left *)
2053 >| [ (* goal 1 (of 2) *)
2054 Suff ‘PosInf + abs (NegInf - NegInf) = PosInf’ >- rw [le_infty] \\
2055 Suff ‘abs (NegInf - NegInf) <> NegInf’ >- METIS_TAC [add_infty] \\
2056 MATCH_MP_TAC pos_not_neginf >> rw [abs_pos],
2057 (* goal 2 (of 2) *)
2058 Suff ‘PosInf + abs (PosInf - PosInf) = PosInf’ >- rw [le_infty] \\
2059 Suff ‘abs (PosInf - PosInf) <> NegInf’ >- METIS_TAC [add_infty] \\
2060 MATCH_MP_TAC pos_not_neginf >> rw [abs_pos] ]
2061QED
2062
2063Theorem abs_sub :
2064 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
2065 abs(x - y) = abs(y - x)
2066Proof
2067 RW_TAC std_ss []
2068 >> Cases_on `x` >> Cases_on `y`
2069 >> rw [ABS_SUB, extreal_abs_def, extreal_sub_eq]
2070QED
2071
2072Theorem abs_sub' :
2073 !x y. abs(x - y) = abs(y - x)
2074Proof
2075 rpt GEN_TAC
2076 >> Cases_on `x` >> Cases_on `y`
2077 >> rw [abs_sub, extreal_abs_def, extreal_sub_def, extreal_add_def]
2078QED
2079
2080Theorem abs_triangle_sub' :
2081 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
2082 abs(x) <= abs(y) + abs(y - x)
2083Proof
2084 rpt STRIP_TAC
2085 >> Know ‘abs (y - x) = abs (x - y)’
2086 >- (MATCH_MP_TAC abs_sub >> art [])
2087 >> Rewr'
2088 >> MATCH_MP_TAC abs_triangle_sub >> art []
2089QED
2090
2091Theorem abs_triangle_sub_full' :
2092 !x y. abs(x) <= abs(y) + abs(y - x)
2093Proof
2094 rpt GEN_TAC
2095 >> ONCE_REWRITE_TAC [abs_sub']
2096 >> REWRITE_TAC [abs_triangle_sub_full]
2097QED
2098
2099Theorem abs_neg_eq[simp] :
2100 !x :extreal. abs (-x) = abs x
2101Proof
2102 GEN_TAC
2103 >> ‘0 <= x \/ x < 0’ by METIS_TAC [let_total]
2104 >- (‘abs x = x’ by PROVE_TAC [abs_refl] >> POP_ORW \\
2105 fs [le_lt] >> MP_TAC (Q.SPEC ‘-x’ abs_neg) \\
2106 ‘-x < 0’ by METIS_TAC [lt_neg, neg_0] >> rw [neg_neg])
2107 >> rw [abs_neg, abs_refl]
2108 >> rw [Once (GSYM le_neg), neg_0]
2109 >> MATCH_MP_TAC lt_imp_le >> art []
2110QED
2111
2112(* cf. realTheory.ABS_TRIANGLE_NEG *)
2113Theorem abs_triangle_neg :
2114 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
2115 abs(x - y) <= abs(x) + abs(y)
2116Proof
2117 rpt STRIP_TAC
2118 >> Know ‘x - y = x + -y’
2119 >- (MATCH_MP_TAC extreal_sub_add >> art [])
2120 >> Rewr'
2121 >> ‘abs y = abs (-y)’ by rw [] >> POP_ORW
2122 >> MATCH_MP_TAC abs_triangle >> art []
2123 >> Cases_on ‘y’ >> rw [extreal_ainv_def]
2124QED
2125
2126Theorem abs_triangle_neg_full :
2127 !x y. abs(x - y) <= abs(x) + abs(y)
2128Proof
2129 rpt GEN_TAC
2130 >> Cases_on ‘x <> PosInf /\ x <> NegInf’
2131 >- (Cases_on ‘y <> PosInf /\ y <> NegInf’
2132 >- (MATCH_MP_TAC abs_triangle_neg >> art []) \\
2133 ‘abs y = PosInf’ by fs [extreal_abs_def] >> POP_ORW \\
2134 Suff ‘abs x + PosInf = PosInf’ >- rw [le_infty] \\
2135 Suff ‘abs x <> NegInf’ >- METIS_TAC [add_infty] \\
2136 MATCH_MP_TAC pos_not_neginf >> rw [abs_pos])
2137 >> ‘abs x = PosInf’ by fs [extreal_abs_def] >> POP_ORW
2138 >> Suff ‘PosInf + abs y = PosInf’ >- rw [le_infty]
2139 >> Suff ‘abs y <> NegInf’ >- METIS_TAC [add_infty]
2140 >> MATCH_MP_TAC pos_not_neginf >> rw [abs_pos]
2141QED
2142
2143Theorem abs_mul :
2144 !x y :extreal. abs (x * y) = abs x * abs y
2145Proof
2146 rpt STRIP_TAC
2147 >> Cases_on `x` >> Cases_on `y`
2148 >> RW_TAC std_ss [extreal_abs_def, extreal_mul_def]
2149 >> fs []
2150 >> REWRITE_TAC [ABS_MUL]
2151QED
2152
2153(* ------------------------------------------------------------------------- *)
2154(* Division and Inversion *)
2155(* ------------------------------------------------------------------------- *)
2156
2157(* added antecedent `y <> 0` *)
2158Theorem extreal_div_eq :
2159 !x y. y <> 0 ==> (Normal x / Normal y = Normal (x / y))
2160Proof
2161 rpt Cases
2162 >> RW_TAC std_ss [extreal_div_def, extreal_inv_def, extreal_mul_def, real_div]
2163QED
2164
2165(* added antecedent ``m <> 0`` *)
2166Theorem quotient_normal :
2167 !n m. m <> 0 ==> (&n / &m = Normal (&n / &m))
2168Proof
2169 RW_TAC std_ss [extreal_div_eq, extreal_of_num_def, REAL_OF_NUM_EQ]
2170QED
2171
2172Theorem extreal_inv_eq :
2173 !x. x <> 0 ==> (inv (Normal x) = Normal (inv x))
2174Proof
2175 METIS_TAC [extreal_inv_def]
2176QED
2177
2178Theorem normal_inv_eq :
2179 !x. x <> 0 ==> (Normal (inv x) = inv (Normal x))
2180Proof
2181 METIS_TAC [extreal_inv_def]
2182QED
2183
2184Theorem inv_one[simp] :
2185 extreal_inv 1 = 1
2186Proof
2187 RW_TAC std_ss [extreal_inv_def, extreal_of_num_def, REAL_10, REAL_INV1]
2188QED
2189
2190Theorem inv_1over : (* was: div_lone *)
2191 !x. x <> 0 ==> (inv x = 1 / x)
2192Proof
2193 rpt Cases
2194 >> RW_TAC real_ss [extreal_inv_def, extreal_div_def, extreal_mul_def,
2195 extreal_of_num_def, REAL_10, REAL_INV1]
2196QED
2197
2198Theorem div_one[simp] : (* was: div_rone *)
2199 !x :extreal. x / 1 = x
2200Proof
2201 RW_TAC real_ss [extreal_div_def, extreal_of_num_def, extreal_inv_def]
2202 >> REWRITE_TAC [REAL_INV1, GSYM extreal_of_num_def, mul_rone]
2203QED
2204
2205Theorem div_refl :
2206 !x :extreal. x <> 0 /\ x <> PosInf /\ x <> NegInf ==> (x / x = 1)
2207Proof
2208 Cases
2209 >> RW_TAC real_ss [extreal_div_def, extreal_mul_def, extreal_inv_def,
2210 extreal_not_infty, extreal_of_num_def, REAL_MUL_RINV]
2211QED
2212
2213Theorem div_refl_pos :
2214 !x :extreal. 0 < x /\ x <> PosInf ==> (x / x = 1)
2215Proof
2216 rpt STRIP_TAC
2217 >> MATCH_MP_TAC div_refl >> fs [lt_le]
2218 >> MATCH_MP_TAC pos_not_neginf >> art []
2219QED
2220
2221Theorem inv_pos :
2222 !x. 0 < x /\ x <> PosInf ==> 0 < 1 / x
2223Proof
2224 Cases
2225 >> RW_TAC real_ss [extreal_inv_def, extreal_of_num_def, extreal_lt_def,
2226 extreal_mul_def, extreal_le_def, lt_infty, le_infty]
2227 >> FULL_SIMP_TAC real_ss [Once real_lte, Once REAL_LT_LE, extreal_div_eq,
2228 extreal_le_def]
2229 >> METIS_TAC [REAL_LE_DIV, REAL_LE_01, REAL_INV_NZ, REAL_INV_1OVER]
2230QED
2231
2232Theorem inv_pos' :
2233 !x. 0 < x /\ x <> PosInf ==> 0 < inv x
2234Proof
2235 RW_TAC std_ss []
2236 >> `x <> 0` by PROVE_TAC [lt_le]
2237 >> ASM_SIMP_TAC std_ss [inv_1over]
2238 >> MATCH_MP_TAC inv_pos >> art []
2239QED
2240
2241(* due to new definition of extreal_inv, `0 <= x` is changed to `0 < x`,
2242 `x <> 0` is added as an antecedent.
2243 *)
2244Theorem inv_pos_eq : (* was: ereal_0_gt_inverse *)
2245 !x. x <> 0 ==> (0 < inv x <=> x <> PosInf /\ 0 <= x)
2246Proof
2247 rpt STRIP_TAC
2248 >> EQ_TAC >> RW_TAC std_ss [] (* 3 subgoals *)
2249 >| [ (* goal 1 (of 3) *)
2250 CCONTR_TAC \\
2251 fs [extreal_inv_def, lt_refl, GSYM extreal_of_num_def],
2252 (* goal 2 (of 3) *)
2253 Know `x <> PosInf /\ x <> NegInf`
2254 >- (CONJ_TAC \\
2255 CCONTR_TAC >> fs [extreal_inv_def, lt_refl, GSYM extreal_of_num_def]) \\
2256 STRIP_TAC \\
2257 `?r. x = Normal r` by METIS_TAC [extreal_cases] \\
2258 `Normal r <> 0` by METIS_TAC [extreal_of_num_def] \\
2259 fs [real_normal, extreal_of_num_def, extreal_le_eq, extreal_lt_eq,
2260 extreal_inv_def, REAL_LT_INV_EQ] \\
2261 MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
2262 (* goal 3 (of 3) *)
2263 MATCH_MP_TAC inv_pos' >> art [] \\
2264 METIS_TAC [le_lt] ]
2265QED
2266
2267Theorem rinv_uniq :
2268 !x y. (x * y = 1) ==> (y = inv x)
2269Proof
2270 rpt Cases
2271 >> RW_TAC real_ss [extreal_inv_def, extreal_mul_def, extreal_of_num_def]
2272 >> Know `r <> 0`
2273 >- (CCONTR_TAC >> fs [])
2274 >> IMP_RES_TAC REAL_RINV_UNIQ >> POP_ORW
2275 >> METIS_TAC [extreal_inv_def]
2276QED
2277
2278Theorem linv_uniq :
2279 !x y. (x * y = 1) ==> (x = inv y)
2280Proof
2281 RW_TAC std_ss [rinv_uniq, mul_comm]
2282QED
2283
2284Theorem le_rdiv :
2285 !x y z. 0 < x ==> (y * Normal x <= z <=> y <= z / Normal x)
2286Proof
2287 STRIP_TAC >> rpt Cases
2288 >> RW_TAC std_ss [extreal_mul_def, extreal_div_def, extreal_inv_def, extreal_le_def,
2289 le_infty, extreal_of_num_def, extreal_not_infty, REAL_LT_REFL,
2290 REAL_INV_EQ_0, REAL_INV_POS, REAL_LT_IMP_NE]
2291 >> METIS_TAC [REAL_NEG_NZ, REAL_LE_RDIV_EQ, real_div]
2292QED
2293
2294Theorem le_ldiv :
2295 !x y z. 0 < x ==> (y <= z * Normal x <=> y / Normal x <= z)
2296Proof
2297 STRIP_TAC >> rpt Cases
2298 >> RW_TAC std_ss [extreal_mul_def, extreal_div_def, extreal_inv_def, extreal_le_def,
2299 le_infty, extreal_of_num_def, extreal_not_infty, REAL_LT_REFL,
2300 REAL_INV_EQ_0, REAL_INV_POS, REAL_LT_IMP_NE]
2301 >> METIS_TAC [REAL_NEG_NZ, REAL_LE_LDIV_EQ, real_div]
2302QED
2303
2304Theorem lt_rdiv :
2305 !x y z. 0 < z ==> (x < y / Normal z <=> x * Normal z < y)
2306Proof
2307 NTAC 2 Cases
2308 >> RW_TAC std_ss [REAL_INV_EQ_0, REAL_INV_POS, extreal_lt_eq, REAL_LT_RDIV_EQ,
2309 GSYM real_div, extreal_inv_def,
2310 REAL_LT_REFL, lt_refl, lt_infty, le_infty, extreal_div_def,
2311 extreal_div_eq, extreal_mul_def, REAL_LT_IMP_NE]
2312QED
2313
2314Theorem lt_div : (* cf. REAL_LT_DIV *)
2315 !y z. 0 < y /\ 0 < z ==> 0 < y / Normal z
2316Proof
2317 rpt STRIP_TAC
2318 >> MP_TAC (REWRITE_RULE [mul_lzero] (Q.SPECL [`0`, `y`, `z`] lt_rdiv))
2319 >> RW_TAC std_ss []
2320QED
2321
2322Theorem le_div : (* cf. REAL_LE_DIV *)
2323 !y z. 0 <= y /\ 0 < z ==> 0 <= y / Normal z
2324Proof
2325 rpt STRIP_TAC
2326 >> MP_TAC (GSYM (Q.SPECL [`z`, `0`, `y`] le_rdiv))
2327 >> RW_TAC std_ss [mul_lzero]
2328QED
2329
2330Theorem lt_ldiv :
2331 !x y z. 0 < z ==> (x / Normal z < y <=> x < y * Normal z)
2332Proof
2333 NTAC 2 Cases
2334 >> RW_TAC std_ss [REAL_INV_EQ_0, REAL_INV_POS, extreal_lt_eq, REAL_LT_LDIV_EQ,
2335 GSYM real_div, extreal_inv_def,
2336 REAL_LT_REFL, lt_refl, lt_infty, le_infty, extreal_div_def,
2337 extreal_div_eq, extreal_mul_def, REAL_LT_IMP_NE]
2338QED
2339
2340Theorem lt_rdiv_neg :
2341 !x y z. z < 0 ==> (y / Normal z < x <=> x * Normal z < y)
2342Proof
2343 NTAC 2 Cases >> RW_TAC std_ss []
2344 >> RW_TAC std_ss [REAL_INV_POS, REAL_LE_LT, GSYM real_lte, REAL_INV_EQ_0,
2345 REAL_INV_POS, REAL_LT_REFL, lt_refl, extreal_div_eq,
2346 extreal_lt_eq, REAL_LT_RDIV_EQ_NEG, GSYM real_div,
2347 lt_infty, le_infty, extreal_div_def, extreal_inv_def,
2348 extreal_mul_def, REAL_LT_REFL, REAL_LT_IMP_NE]
2349 >> METIS_TAC [REAL_LT_ANTISYM, real_lte, REAL_NEG_NZ, REAL_LT_INV_EQ,
2350 lt_refl, lt_infty]
2351QED
2352
2353(* `x, y` must be reals, `z <> 0` *)
2354Theorem div_add :
2355 !x y z. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf /\ z <> 0 ==>
2356 (x / z + y / z = (x + y) / z)
2357Proof
2358 rpt Cases
2359 >> RW_TAC real_ss [extreal_add_def, extreal_div_def, extreal_mul_def,
2360 extreal_of_num_def, extreal_inv_def]
2361 >> REAL_ARITH_TAC
2362QED
2363
2364(* `z` must be non-zero normal reals, `x + y` must be defined *)
2365Theorem div_add2 :
2366 !x y z. ((x <> PosInf /\ y <> PosInf) \/ (x <> NegInf /\ y <> NegInf)) /\
2367 z <> 0 /\ z <> PosInf /\ z <> NegInf ==>
2368 (x / z + y / z = (x + y) / z)
2369Proof
2370 rpt Cases
2371 >> RW_TAC real_ss [extreal_add_def, extreal_div_def, extreal_mul_def,
2372 extreal_of_num_def, extreal_inv_def]
2373 >> REAL_ARITH_TAC
2374QED
2375
2376Theorem div_sub :
2377 !x y z. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf /\ z <> 0 ==>
2378 (x / z - y / z = (x - y) / z)
2379Proof
2380 rpt Cases
2381 >> RW_TAC real_ss [extreal_sub_def, extreal_div_def, extreal_mul_def,
2382 extreal_of_num_def, extreal_inv_def]
2383 >> REAL_ARITH_TAC
2384QED
2385
2386(* NOTE: `0 <= x` is changed to `0 < x` otherwise `inv x` is not defined *)
2387Theorem le_inv :
2388 !x. 0 < x ==> 0 <= inv x
2389Proof
2390 Cases >> RW_TAC real_ss [extreal_inv_def, extreal_of_num_def, extreal_le_def,
2391 le_infty, lt_refl, extreal_lt_eq, REAL_LT_IMP_NE]
2392 >> MATCH_MP_TAC REAL_LE_INV
2393 >> MATCH_MP_TAC REAL_LT_IMP_LE >> art []
2394QED
2395
2396Theorem div_infty :
2397 !x. x <> PosInf /\ x <> NegInf ==> (x / PosInf = 0) /\ (x / NegInf = 0)
2398Proof
2399 Cases
2400 >> RW_TAC std_ss [extreal_div_def, extreal_inv_def, GSYM extreal_of_num_def, mul_rzero]
2401QED
2402
2403Theorem infty_div :
2404 !r. 0 < r ==> (PosInf / Normal r = PosInf) /\ (NegInf / Normal r = NegInf)
2405Proof
2406 GEN_TAC >> DISCH_TAC
2407 >> IMP_RES_TAC REAL_LT_IMP_NE
2408 >> RW_TAC real_ss [extreal_div_def, extreal_inv_def, GSYM extreal_of_num_def,
2409 extreal_mul_def, mul_rzero, REAL_INV_POS, REAL_INV_EQ_0]
2410QED
2411
2412Theorem zero_div : (* cf. REAL_DIV_LZERO *)
2413 !x :extreal. x <> 0 ==> (0 / x = 0)
2414Proof
2415 Cases
2416 >> RW_TAC std_ss [extreal_div_def, mul_lzero, extreal_of_num_def]
2417QED
2418
2419Theorem ldiv_eq : (* REAL_EQ_LDIV_EQ *)
2420 !x y z. 0 < z /\ z < PosInf ==> ((x / z = y) <=> (x = y * z))
2421Proof
2422 NTAC 3 Cases
2423 >> RW_TAC std_ss [lt_infty, extreal_of_num_def, extreal_lt_eq, extreal_not_infty,
2424 extreal_mul_def, infty_div, REAL_LT_REFL, extreal_div_def,
2425 extreal_inv_def, extreal_mul_def, GSYM real_div, REAL_LT_IMP_NE]
2426 >> MATCH_MP_TAC REAL_EQ_LDIV_EQ >> art []
2427QED
2428
2429Theorem rdiv_eq : (* REAL_EQ_RDIV_EQ *)
2430 !x y z. 0 < z /\ z < PosInf ==> ((x = y / z) <=> (x * z = y))
2431Proof
2432 NTAC 3 Cases
2433 >> RW_TAC std_ss [lt_infty, extreal_of_num_def, extreal_lt_eq, extreal_not_infty,
2434 extreal_mul_def, infty_div, REAL_LT_REFL, extreal_div_def,
2435 extreal_inv_def, extreal_mul_def, GSYM real_div, REAL_POS_NZ]
2436 >> MATCH_MP_TAC REAL_EQ_RDIV_EQ >> art []
2437QED
2438
2439Theorem eq_rdiv :
2440 !x y z. 0 < z ==> ((x = y / Normal z) <=> (x * Normal z = y))
2441Proof
2442 rpt STRIP_TAC >> MATCH_MP_TAC rdiv_eq
2443 >> RW_TAC std_ss [extreal_of_num_def, extreal_lt_eq, lt_infty]
2444QED
2445
2446(* NOTE: ‘x <> PosInf /\ x <> NegInf’ cannot be removed when ‘y = PosInf’ *)
2447Theorem div_eq_mul_linv :
2448 !x y. x <> PosInf /\ x <> NegInf /\ 0 < y ==> (x / y = (inv y) * x)
2449Proof
2450 RW_TAC std_ss []
2451 >> Cases_on `y = PosInf`
2452 >- ASM_SIMP_TAC std_ss [div_infty, extreal_inv_def, GSYM extreal_of_num_def,
2453 mul_lzero]
2454 >> Know `0 < y /\ y < PosInf` >- art [GSYM lt_infty]
2455 >> DISCH_THEN (REWRITE_TAC o wrap o (MATCH_MP ldiv_eq))
2456 >> REWRITE_TAC [GSYM mul_assoc, Once mul_comm]
2457 >> `y * inv y = 1` by PROVE_TAC [mul_comm, mul_linv_pos]
2458 >> ASM_REWRITE_TAC [mul_rone]
2459QED
2460
2461(* |- !x y. x <> PosInf /\ x <> NegInf /\ 0 < y ==> x / y = x * realinv y *)
2462Theorem div_eq_mul_rinv = ONCE_REWRITE_RULE [mul_comm] div_eq_mul_linv
2463
2464Theorem inv_lt_antimono: (* new *)
2465 !x y :extreal. 0 < x /\ 0 < y ==> (inv x < inv y <=> y < x)
2466Proof
2467 rpt strip_tac
2468 >> `x <> 0 /\ y <> 0` by PROVE_TAC [lt_le]
2469 >> Cases_on `x`
2470 >> fs [lt_infty, extreal_inv_def, extreal_of_num_def, lt_refl,
2471 extreal_lt_eq]
2472 >- (fs [GSYM extreal_of_num_def] \\
2473 reverse EQ_TAC >> DISCH_TAC >| (* 2 subgoals *)
2474 [ (* goal 1 (of 2) *)
2475 MATCH_MP_TAC inv_pos' >> art [lt_infty],
2476 (* goal 2 (of 2) *)
2477 REWRITE_TAC [GSYM lt_infty] \\
2478 CCONTR_TAC >> fs [extreal_inv_def] \\
2479 fs [GSYM extreal_of_num_def, lt_refl] ])
2480 >> Cases_on `y`
2481 >> fs [lt_infty, extreal_inv_def, extreal_of_num_def, lt_refl,
2482 extreal_lt_eq]
2483 >> ASM_REWRITE_TAC [real_lt, REAL_LE_LT]
2484QED
2485
2486Theorem inv_inj: (* new *)
2487 !x y :extreal. 0 < x /\ 0 < y ==> ((inv x = inv y) <=> (x = y))
2488Proof
2489 rpt STRIP_TAC
2490 >> `x <> 0 /\ y <> 0` by PROVE_TAC [lt_le]
2491 >> Cases_on `x` >> Cases_on `y`
2492 >> fs [extreal_inv_def, extreal_of_num_def, extreal_not_infty,
2493 lt_infty, extreal_lt_eq]
2494QED
2495
2496Theorem inv_le_antimono :
2497 !x y :extreal. 0 < x /\ 0 < y ==> (inv x <= inv y <=> y <= x)
2498Proof
2499 rpt STRIP_TAC
2500 >> REWRITE_TAC [le_lt]
2501 >> EQ_TAC >> STRIP_TAC
2502 >| [ DISJ1_TAC >> PROVE_TAC [inv_lt_antimono],
2503 DISJ2_TAC >> PROVE_TAC [inv_inj],
2504 DISJ1_TAC >> PROVE_TAC [inv_lt_antimono],
2505 DISJ2_TAC >> PROVE_TAC [inv_inj] ]
2506QED
2507
2508Theorem inv_le_antimono_imp :
2509 !x y :extreal. 0 < y /\ y <= x ==> inv x <= inv y
2510Proof
2511 rpt STRIP_TAC
2512 >> Suff ‘inv x <= inv y <=> y <= x’ >- rw []
2513 >> MATCH_MP_TAC inv_le_antimono >> art []
2514 >> MATCH_MP_TAC lte_trans
2515 >> Q.EXISTS_TAC ‘y’ >> art []
2516QED
2517
2518Theorem inv_not_infty :
2519 !x :extreal. x <> 0 ==> inv x <> PosInf /\ inv x <> NegInf
2520Proof
2521 Cases >> rw[extreal_inv_def]
2522QED
2523
2524Theorem inv_infty :
2525 inv PosInf = 0 /\ inv NegInf = 0
2526Proof
2527 rw [extreal_of_num_def, extreal_inv_def]
2528QED
2529
2530Theorem div_not_infty :
2531 !x y:extreal. y <> 0 ==> Normal x / y <> PosInf /\ Normal x / y <> NegInf
2532Proof
2533 rpt GEN_TAC
2534 >> Cases_on `y`
2535 >> rw[extreal_div_def, extreal_inv_def, extreal_not_infty,
2536 extreal_of_num_def]
2537 >> simp[extreal_mul_def]
2538QED
2539
2540Theorem div_mul_refl :
2541 !(x :extreal) r. r <> 0 ==> x = x / Normal r * Normal r
2542Proof
2543 RW_TAC std_ss [extreal_div_def, extreal_inv_def, GSYM mul_assoc,
2544 extreal_mul_def]
2545 >> RW_TAC real_ss [REAL_MUL_LINV, GSYM extreal_of_num_def, mul_rone]
2546QED
2547
2548(* NOTE: removed ‘x <> PosInf /\ x <> NegInf’; changed ‘0 < r’ to ‘r <> 0’ *)
2549Theorem mul_div_refl :
2550 !(x :extreal) r. r <> 0 ==> x = x * Normal r / Normal r
2551Proof
2552 rpt STRIP_TAC
2553 >> ‘x * Normal r / Normal r = x * Normal r * inv (Normal r)’
2554 by rw [extreal_div_def]
2555 >> POP_ORW
2556 >> ‘x * Normal r * inv (Normal r) = x * inv (Normal r) * Normal r’
2557 by PROVE_TAC [mul_comm, mul_assoc]
2558 >> POP_ORW
2559 >> ‘x * inv (Normal r) = x / Normal r’ by rw [extreal_div_def]
2560 >> POP_ORW
2561 >> MATCH_MP_TAC div_mul_refl >> art []
2562QED
2563
2564Theorem ldiv_le_imp :
2565 !x y (z :extreal). 0 < z /\ z <> PosInf /\ x <= y ==> x / z <= y / z
2566Proof
2567 RW_TAC std_ss []
2568 >> `z <> NegInf` by METIS_TAC [lt_imp_le, pos_not_neginf]
2569 >> `?r. z = Normal r` by METIS_TAC [extreal_cases]
2570 >> `0 < r` by METIS_TAC [extreal_of_num_def, extreal_lt_eq]
2571 >> `r <> 0` by METIS_TAC [REAL_LT_LE]
2572 >> Cases_on `x` >> Cases_on `y`
2573 >> fs [le_infty, extreal_div_eq, infty_div, le_refl, extreal_le_eq]
2574 >> fs [REAL_LE_LT] >> DISJ1_TAC >> rw [REAL_LT_RDIV]
2575QED
2576
2577(* cf. REAL_EQ_MUL_LCANCEL *)
2578Theorem mul_lcancel :
2579 !x y (z :extreal). x <> PosInf /\ x <> NegInf ==>
2580 (x * y = x * z <=> x = 0 \/ y = z)
2581Proof
2582 rpt STRIP_TAC
2583 >> `?r. x = Normal r` by METIS_TAC [extreal_cases]
2584 >> POP_ORW >> KILL_TAC
2585 >> Cases_on `y` >> Cases_on `z`
2586 >> rw[extreal_mul_def, extreal_not_infty, extreal_of_num_def,
2587 REAL_MUL_LZERO, REAL_MUL_RZERO]
2588 >> REWRITE_TAC [REAL_EQ_MUL_LCANCEL]
2589QED
2590
2591(* |- !x y z. x <> PosInf /\ x <> NegInf ==> (y * x = z * x <=> x = 0 \/ y = z) *)
2592Theorem mul_rcancel = ONCE_REWRITE_RULE [mul_comm] mul_lcancel
2593
2594Theorem inv_mul :
2595 !x y. x <> 0 /\ y <> 0 ==> inv (x * y) = inv x * inv y
2596Proof
2597 rpt STRIP_TAC
2598 >> Cases_on `x` >> Cases_on `y`
2599 >> fs[extreal_mul_def, extreal_inv_def, extreal_not_infty,
2600 extreal_of_num_def]
2601 >> rw[extreal_inv_def]
2602QED
2603
2604Theorem abs_div :
2605 !x y. x <> PosInf /\ x <> NegInf /\ y <> 0 ==> abs (x / y) = abs x / abs y
2606Proof
2607 rpt STRIP_TAC
2608 >> Cases_on `x` >> Cases_on `y`
2609 >> fs[extreal_div_def, extreal_inv_def, extreal_not_infty,
2610 extreal_of_num_def, extreal_abs_def, extreal_mul_def]
2611 >> rename1 `s <> 0`
2612 >> `abs s <> 0` by PROVE_TAC [ABS_ZERO]
2613 >> simp[extreal_div_eq, ABS_MUL, real_div, ABS_INV]
2614QED
2615
2616Theorem abs_div_normal :
2617 !x y. y <> 0 ==> abs (x / Normal y) = abs x / Normal (abs y)
2618Proof
2619 rpt STRIP_TAC
2620 >> ‘abs y <> 0’ by PROVE_TAC [ABS_ZERO]
2621 >> Cases_on `x`
2622 >> RW_TAC std_ss [extreal_div_def, abs_mul, extreal_inv_def, extreal_abs_def,
2623 ABS_INV]
2624QED
2625
2626(* cf. REAL_INVINV *)
2627Theorem inv_inv :
2628 !x. x <> 0 /\ x <> PosInf /\ x <> NegInf ==> inv (inv x) = x
2629Proof
2630 Cases >> rw [extreal_of_num_def, extreal_inv_eq]
2631 >> ASM_SIMP_TAC std_ss [REAL_INVINV]
2632QED
2633
2634(* ------------------------------------------------------------------------- *)
2635(* x pow n *)
2636(* ------------------------------------------------------------------------- *)
2637
2638Theorem pow_0[simp] :
2639 !x. x pow 0 = 1
2640Proof
2641 Cases >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, pow]
2642QED
2643
2644(* an equivalent "recursive" definition like realTheory.pow *)
2645Theorem extreal_pow :
2646 (!x :extreal. x pow 0 = 1) /\ !(x :extreal) n. x pow SUC n = x * x pow n
2647Proof
2648 rw [] >> Cases_on ‘x’
2649 >> RW_TAC arith_ss [extreal_pow_def, extreal_mul_def, GSYM extreal_of_num_def, pow,
2650 mul_rone, EVEN] >- fs [EVEN]
2651 >> PROVE_TAC []
2652QED
2653
2654Theorem zero_pow : (* POW_0 *)
2655 !n. 0 < n ==> (extreal_pow 0 n = 0)
2656Proof
2657 rw[extreal_of_num_def, extreal_pow_def]
2658QED
2659
2660Theorem pow_1[simp] :
2661 !x. x pow 1 = x
2662Proof
2663 Cases >> RW_TAC std_ss [extreal_pow_def, POW_1]
2664QED
2665
2666Theorem one_pow[simp] : (* POW_ONE *)
2667 !n. extreal_pow 1 n = 1
2668Proof
2669 rw[extreal_of_num_def, extreal_pow_def, POW_ONE]
2670QED
2671
2672Theorem pow_2 :
2673 !x. x pow 2 = x * x
2674Proof
2675 Cases >> RW_TAC std_ss [extreal_pow_def, extreal_mul_def, POW_2]
2676QED
2677
2678Theorem pow_zero[simp] :
2679 !n x :extreal. (x pow (SUC n) = 0) <=> (x = 0)
2680Proof
2681 STRIP_TAC >> Cases
2682 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, POW_ZERO_EQ]
2683QED
2684
2685Theorem pow_zero_imp:
2686 !n x. (x pow n = 0) ==> (x = 0)
2687Proof
2688 STRIP_TAC >> Cases
2689 >> RW_TAC std_ss [extreal_pow_def,extreal_of_num_def,REAL_LT_01,REAL_LT_IMP_NE]
2690 >> METIS_TAC [POW_ZERO]
2691QED
2692
2693Theorem le_pow2 :
2694 !x. 0 <= x pow 2
2695Proof
2696 Cases
2697 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, REAL_LE_POW2]
2698QED
2699
2700Theorem abs_pow2[simp] :
2701 !x. (abs x) pow 2 = x pow 2
2702Proof
2703 GEN_TAC
2704 >> Cases_on `0 <= x` >- fs [GSYM abs_refl]
2705 >> fs [GSYM extreal_lt_def, abs_neg, pow_2, neg_mul2]
2706QED
2707
2708Theorem pow_2_abs :
2709 !x. x pow 2 = abs x * abs x
2710Proof
2711 RW_TAC std_ss [Once (GSYM abs_pow2), pow_2]
2712QED
2713
2714(* NOTE: ‘!n’ is moved to top-level *)
2715Theorem pow_pos_le :
2716 !n x. 0 <= x ==> 0 <= x pow n
2717Proof
2718 Q.X_GEN_TAC ‘n’
2719 >> Cases
2720 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, POW_POS]
2721 >> METIS_TAC [le_infty, le_01, REAL_LE_01, extreal_of_num_def]
2722QED
2723
2724(* NOTE: ‘!n’ is moved to top-level *)
2725Theorem pow_pos_lt :
2726 !n x. 0 < x ==> 0 < x pow n
2727Proof
2728 NTAC 2 Cases
2729 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, extreal_lt_eq,
2730 POW_POS_LT, REAL_LT_01, lt_infty, extreal_not_infty]
2731 >> METIS_TAC [pow, REAL_LT_01]
2732QED
2733
2734Theorem pow_le :
2735 !n x y. 0 <= x /\ x <= y ==> x pow n <= y pow n
2736Proof
2737 STRIP_TAC >> NTAC 2 Cases
2738 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, POW_LE,
2739 lt_infty, le_infty, extreal_not_infty, REAL_LE_REFL, pow]
2740QED
2741
2742Theorem pow_lt :
2743 !n x y. 0 <= x /\ x < y ==> x pow SUC n < y pow SUC n
2744Proof
2745 STRIP_TAC >> NTAC 2 Cases
2746 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, REAL_POW_LT2,
2747 lt_infty, le_infty, extreal_not_infty, extreal_lt_eq]
2748QED
2749
2750Theorem pow_lt2 :
2751 !n x y. n <> 0 /\ 0 <= x /\ x < y ==> x pow n < y pow n
2752Proof
2753 STRIP_TAC >> NTAC 2 Cases
2754 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def, REAL_POW_LT2,
2755 lt_infty, le_infty, extreal_not_infty, extreal_lt_eq]
2756QED
2757
2758Theorem pow_le_full :
2759 !n x y :extreal. n <> 0 /\ 0 <= x /\ 0 <= y ==>
2760 (x <= y <=> x pow n <= y pow n)
2761Proof
2762 rpt STRIP_TAC
2763 >> EQ_TAC >> DISCH_TAC
2764 >- (MATCH_MP_TAC pow_le >> art [])
2765 >> SPOSE_NOT_THEN (ASSUME_TAC o (REWRITE_RULE [GSYM extreal_lt_def]))
2766 >> `y pow n < x pow n` by PROVE_TAC [pow_lt2]
2767 >> METIS_TAC [let_antisym]
2768QED
2769
2770Theorem pow_eq :
2771 !n x y. n <> 0 /\ 0 <= x /\ 0 <= y ==> ((x = y) <=> (x pow n = y pow n))
2772Proof
2773 rpt STRIP_TAC
2774 >> EQ_TAC >> rw []
2775 >> fs [GSYM le_antisym]
2776 >> METIS_TAC [pow_le_full]
2777QED
2778
2779Theorem pow_le_mono :
2780 !x n m. 1 <= x /\ n <= m ==> x pow n <= x pow m
2781Proof
2782 Cases
2783 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_le_def,
2784 lt_infty, le_infty, extreal_not_infty, REAL_LE_REFL]
2785 >> Cases_on `n = m` >- RW_TAC std_ss [REAL_LE_REFL]
2786 >> `n < m` by METIS_TAC [LESS_OR_EQ]
2787 >> `?p. m = p + n` by METIS_TAC [LESS_ADD]
2788 >> FULL_SIMP_TAC std_ss []
2789 >> NTAC 3 (POP_ASSUM (K ALL_TAC))
2790 >> Induct_on `p` >- RW_TAC real_ss [REAL_LE_REFL]
2791 >> RW_TAC real_ss [GSYM ADD_SUC,pow]
2792 >> `0 <= r` by METIS_TAC [REAL_LE_01,REAL_LE_TRANS]
2793 >> `0 <= r pow n` by METIS_TAC [POW_POS]
2794 >> ONCE_REWRITE_TAC [ADD_COMM]
2795 >> (MP_TAC o Q.SPECL [`1:real`,`r`,`r pow n`,`r pow (p + n)`]) REAL_LE_MUL2
2796 >> RW_TAC real_ss []
2797QED
2798
2799Theorem pow_pos_even :
2800 !x. x < 0 ==> ((0 < x pow n) <=> (EVEN n))
2801Proof
2802 Cases
2803 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_not_infty,
2804 le_infty, lt_infty, extreal_lt_eq, REAL_LT_01, POW_POS_EVEN]
2805QED
2806
2807Theorem pow_neg_odd :
2808 !x. x < 0 ==> ((x pow n < 0) <=> (ODD n))
2809Proof
2810 Cases
2811 >> RW_TAC std_ss [extreal_pow_def, extreal_of_num_def, extreal_not_infty,
2812 le_infty, lt_infty, extreal_lt_eq, extreal_le_def,
2813 REAL_LT_01, EVEN_ODD, extreal_lt_def, extreal_le_def,
2814 REAL_LE_01, POW_NEG_ODD, GSYM real_lt]
2815QED
2816
2817(* antecedents added due to new definition of `extreal_add` *)
2818Theorem add_pow2 :
2819 !x y. x <> NegInf /\ x <> PosInf /\ y <> NegInf /\ y <> PosInf ==>
2820 ((x + y) pow 2 = x pow 2 + y pow 2 + 2 * x * y)
2821Proof
2822 NTAC 2 Cases
2823 >> RW_TAC real_ss [extreal_pow_def, extreal_mul_def, extreal_add_def,
2824 extreal_of_num_def]
2825 >> REWRITE_TAC [ADD_POW_2]
2826QED
2827
2828Theorem REAL_MUL_POS_LT[local] : (* from intergrationTheory *)
2829 !x y:real. &0 < x * y <=> &0 < x /\ &0 < y \/ x < &0 /\ y < &0
2830Proof
2831 REPEAT STRIP_TAC THEN
2832 STRIP_ASSUME_TAC(SPEC ``x:real`` REAL_LT_NEGTOTAL) THEN
2833 STRIP_ASSUME_TAC(SPEC ``y:real`` REAL_LT_NEGTOTAL) THEN
2834 ASM_REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO, REAL_LT_REFL] THEN
2835 ASSUM_LIST(MP_TAC o MATCH_MP REAL_LT_MUL o end_itlist CONJ) THEN
2836 REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
2837QED
2838
2839Theorem infty_pow2[simp] :
2840 (PosInf pow 2 = PosInf) /\ (NegInf pow 2 = PosInf)
2841Proof
2842 rw [pow_2, extreal_mul_def]
2843QED
2844
2845Theorem add_pow2_pos : (* was: add_pow02 *)
2846 !x y. 0 < x /\ x <> PosInf /\ 0 <= y ==>
2847 (x + y) pow 2 = x pow 2 + y pow 2 + 2 * x * y
2848Proof
2849 RW_TAC std_ss []
2850 >> `x <> NegInf` by METIS_TAC [lt_trans, lt_infty, num_not_infty]
2851 >> `y <> NegInf` by METIS_TAC [lte_trans, lt_infty, num_not_infty]
2852 >> ASM_CASES_TAC ``y = PosInf`` >| [ALL_TAC, METIS_TAC [add_pow2]]
2853 >> ASM_SIMP_TAC std_ss []
2854 >> `x = Normal (real x)` by METIS_TAC [normal_real]
2855 >> ONCE_ASM_REWRITE_TAC []
2856 >> SIMP_TAC std_ss [extreal_add_def, extreal_mul_def, extreal_of_num_def]
2857 >> ONCE_REWRITE_TAC [infty_pow2]
2858 >> rpt COND_CASES_TAC
2859 >> ASM_SIMP_TAC std_ss [extreal_pow_def, extreal_add_def]
2860 >> POP_ASSUM MP_TAC
2861 >> ONCE_REWRITE_TAC [MONO_NOT_EQ]
2862 >> RW_TAC std_ss [real_normal, REAL_MUL_POS_LT]
2863 >> DISJ1_TAC
2864 >> ASM_SIMP_TAC real_ss [GSYM extreal_lt_eq, normal_real, GSYM extreal_of_num_def]
2865QED
2866
2867Theorem sub_pow2 :
2868 !x y. x <> NegInf /\ x <> PosInf /\ y <> NegInf /\ y <> PosInf ==>
2869 (x - y) pow 2 = x pow 2 + y pow 2 - 2 * x * y
2870Proof
2871 NTAC 2 Cases
2872 >> RW_TAC real_ss [extreal_pow_def, extreal_mul_def, extreal_add_def,
2873 extreal_of_num_def, extreal_ainv_def, extreal_sub_def]
2874 >> REWRITE_TAC [SUB_POW_2]
2875QED
2876
2877Theorem pow_add :
2878 !x n m. x pow (n + m) = x pow n * x pow m
2879Proof
2880 Cases
2881 >> RW_TAC real_ss [extreal_pow_def, POW_ADD, extreal_of_num_def,
2882 extreal_mul_def, mul_rone, mul_lone]
2883 >> METIS_TAC [ADD_CLAUSES, EVEN_ADD]
2884QED
2885
2886Theorem pow_mul :
2887 !n x y. (x * y) pow n = x pow n * y pow n
2888Proof
2889 Cases >- RW_TAC std_ss [pow_0,mul_lone]
2890 >> NTAC 2 Cases
2891 >> RW_TAC real_ss [extreal_mul_def, extreal_pow_def, pow_zero, POW_ZERO_EQ,
2892 POW_POS_LT, POW_MUL]
2893 >> FULL_SIMP_TAC real_ss [GSYM real_lte]
2894 >> METIS_TAC [POW_POS_EVEN, POW_NEG_ODD, REAL_LT_LE, POW_POS_LT, real_lt,
2895 POW_ZERO_EQ, EVEN_ODD]
2896QED
2897
2898Theorem pow_minus1[simp] :
2899 !n. -1 pow (2 * n) = (1 :extreal)
2900Proof
2901 RW_TAC std_ss [extreal_of_num_def, extreal_ainv_def, extreal_pow_def, POW_MINUS1]
2902QED
2903
2904Theorem pow_not_infty :
2905 !n x. x <> NegInf /\ x <> PosInf ==> x pow n <> NegInf /\ x pow n <> PosInf
2906Proof
2907 Cases >> METIS_TAC [extreal_pow_def, extreal_not_infty, extreal_cases]
2908QED
2909
2910Theorem pow_inv : (* cf. REAL_POW_INV *)
2911 !n y. y <> 0 ==> inv (y pow n) = (inv y) pow n
2912Proof
2913 rpt STRIP_TAC
2914 >> Cases_on `n = 0` >- rw [pow_0, inv_one]
2915 >> `0 < n` by RW_TAC arith_ss []
2916 >> `0 pow n = (0 :real)` by (Cases_on `n` >> rw [POW_0])
2917 >> Cases_on `y` >> RW_TAC std_ss [extreal_pow_def, extreal_inv_def]
2918 >> `r <> 0` by (strip_tac >> gvs[])
2919 >> `r pow n <> 0` by PROVE_TAC [POW_NZ]
2920 >> simp[extreal_inv_eq, extreal_pow_def]
2921QED
2922
2923Theorem pow_div : (* cf. REAL_POW_DIV *)
2924 !n x y. x <> PosInf /\ x <> NegInf /\ 0 < y ==>
2925 (x / y) pow n = x pow n / y pow n
2926Proof
2927 rpt STRIP_TAC
2928 >> `x pow n <> PosInf /\ x pow n <> NegInf` by METIS_TAC [pow_not_infty]
2929 >> `0 < y pow n` by METIS_TAC [pow_pos_lt]
2930 >> ASM_SIMP_TAC std_ss [div_eq_mul_linv, pow_mul]
2931 >> Suff `inv (y pow n) = (inv y) pow n` >- RW_TAC std_ss []
2932 >> MATCH_MP_TAC pow_inv
2933 >> FULL_SIMP_TAC std_ss [lt_le]
2934QED
2935
2936Theorem pow_pow : (* cf. REAL_POW_POW *)
2937 !(x :extreal) m n. (x pow m) pow n = x pow (m * n)
2938Proof
2939 rpt GEN_TAC
2940 >> Cases_on ‘x’
2941 >| [ (* goal 1 (of 3) *)
2942 Cases_on ‘m = 0’ >- rw [extreal_pow_def] \\
2943 Cases_on ‘EVEN m’
2944 >- (rw [extreal_pow_def] >> fs [EVEN_MULT]) \\
2945 rw [extreal_pow_def] >> gs [EVEN_MULT],
2946 (* goal 2 (of 3) *)
2947 Cases_on ‘m = 0’ >- rw [extreal_pow_def] \\
2948 Cases_on ‘EVEN m’ >- rw [extreal_pow_def] \\
2949 rw [extreal_pow_def],
2950 (* goal 3 (of 3) *)
2951 rw [extreal_pow_def, REAL_POW_POW] ]
2952QED
2953
2954Theorem abs_le_square_plus1 :
2955 !(x :extreal). abs x <= x pow 2 + 1
2956Proof
2957 GEN_TAC
2958 >> Cases_on `0 <= x`
2959 >- (fs [GSYM abs_refl] \\
2960 Cases_on `1 <= x`
2961 >- (MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `x pow 2 + 0` \\
2962 reverse CONJ_TAC
2963 >- (MATCH_MP_TAC le_add2 >> REWRITE_TAC [le_refl, le_01]) \\
2964 REWRITE_TAC [add_rzero, pow_2] \\
2965 `x = 1 * x` by PROVE_TAC [mul_lone] \\
2966 POP_ASSUM
2967 ((GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites) o wrap) \\
2968 MATCH_MP_TAC le_rmul_imp >> art [] \\
2969 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `1` >> art [le_01]) \\
2970 fs [GSYM extreal_lt_def] \\
2971 Know `x <= x pow 2 + 1 <=> x - 1 <= x pow 2`
2972 >- (MATCH_MP_TAC EQ_SYM \\
2973 MATCH_MP_TAC sub_le_eq \\
2974 REWRITE_TAC [extreal_of_num_def, extreal_not_infty]) \\
2975 Rewr' \\
2976 `x - 1 < 0` by PROVE_TAC [sub_lt_zero] \\
2977 `0 <= x pow 2` by PROVE_TAC [le_pow2] \\
2978 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0` >> art [] \\
2979 IMP_RES_TAC lt_imp_le)
2980 >> fs [GSYM extreal_lt_def]
2981 >> `abs x = -x` by PROVE_TAC [abs_neg] >> POP_ORW
2982 >> Cases_on `-1 < x`
2983 >- (`-x < 1` by PROVE_TAC [neg_neg, GSYM lt_neg] \\
2984 Know `-x <= x pow 2 + 1 <=> -x - 1 <= x pow 2`
2985 >- (MATCH_MP_TAC EQ_SYM \\
2986 MATCH_MP_TAC sub_le_eq \\
2987 REWRITE_TAC [extreal_of_num_def, extreal_not_infty]) \\
2988 Rewr' \\
2989 `-x - 1 < 0` by PROVE_TAC [sub_lt_zero] \\
2990 `0 <= x pow 2` by PROVE_TAC [le_pow2] \\
2991 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0` >> art [] \\
2992 IMP_RES_TAC lt_imp_le)
2993 >> fs [extreal_lt_def]
2994 >> `1 <= -x` by PROVE_TAC [le_neg, neg_neg]
2995 >> MATCH_MP_TAC le_trans
2996 >> Q.EXISTS_TAC `x pow 2 + 0`
2997 >> reverse CONJ_TAC
2998 >- (MATCH_MP_TAC le_add2 >> REWRITE_TAC [le_refl, le_01])
2999 >> REWRITE_TAC [add_rzero]
3000 >> `x pow 2 = -x * -x` by REWRITE_TAC [pow_2, neg_mul2] >> POP_ORW
3001 >> `-x = 1 * -x` by PROVE_TAC [mul_lone]
3002 >> POP_ASSUM ((GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites) o wrap)
3003 >> MATCH_MP_TAC le_rmul_imp >> art []
3004 >> MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `1` >> art [le_01]
3005QED
3006
3007Theorem abs_pow_le_mono :
3008 !(x :extreal) n m. n <= m ==> (abs x) pow n <= 1 + (abs x) pow m
3009Proof
3010 rpt STRIP_TAC
3011 >> Cases_on `1 <= x`
3012 >- (MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0 + (abs x) pow m` \\
3013 reverse CONJ_TAC
3014 >- (MATCH_MP_TAC le_add2 >> REWRITE_TAC [le_01, le_refl]) \\
3015 REWRITE_TAC [add_lzero] \\
3016 MATCH_MP_TAC pow_le_mono >> art [] \\
3017 Suff `abs x = x` >- RW_TAC std_ss [] \\
3018 REWRITE_TAC [abs_refl] \\
3019 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `1` >> art [le_01])
3020 >> fs [GSYM extreal_lt_def]
3021 >> Cases_on `x <= -1`
3022 >- (MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0 + (abs x) pow m` \\
3023 reverse CONJ_TAC
3024 >- (MATCH_MP_TAC le_add2 >> REWRITE_TAC [le_01, le_refl]) \\
3025 REWRITE_TAC [add_lzero] \\
3026 MATCH_MP_TAC pow_le_mono >> art [] \\
3027 Suff `abs x = -x` >- (Rewr' >> METIS_TAC [le_neg, neg_neg]) \\
3028 MATCH_MP_TAC abs_neg \\
3029 MATCH_MP_TAC let_trans >> Q.EXISTS_TAC `-1` >> art [lt_10])
3030 >> fs [GSYM extreal_lt_def]
3031 >> MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `1 + 0`
3032 >> reverse CONJ_TAC
3033 >- (MATCH_MP_TAC le_add2 >> art [le_refl] \\
3034 MATCH_MP_TAC pow_pos_le >> REWRITE_TAC [abs_pos])
3035 >> REWRITE_TAC [add_rzero, Once (GSYM (Q.SPEC `n` one_pow))]
3036 >> MATCH_MP_TAC pow_le
3037 >> REWRITE_TAC [abs_pos, abs_bounds]
3038 >> CONJ_TAC >> MATCH_MP_TAC lt_imp_le >> art []
3039QED
3040
3041(* This result is needed for proving Cauchy-Schwarz inequality *)
3042Theorem abs_le_half_pow2 :
3043 !x y :extreal. abs (x * y) <= Normal (1 / 2) * (x pow 2 + y pow 2)
3044Proof
3045 NTAC 2 Cases
3046 >> ASM_SIMP_TAC real_ss [extreal_abs_def, extreal_mul_def, pow_2, extreal_add_def,
3047 le_refl, le_infty, extreal_le_eq]
3048 >> REWRITE_TAC [GSYM POW_2, ABS_LE_HALF_POW2]
3049QED
3050
3051(* ------------------------------------------------------------------------- *)
3052(* SQRT *)
3053(* ------------------------------------------------------------------------- *)
3054
3055Theorem sqrt_pos_le :
3056 !x. 0 <= x ==> 0 <= sqrt x
3057Proof
3058 Cases
3059 >> RW_TAC std_ss [extreal_sqrt_def, extreal_of_num_def, extreal_le_def, SQRT_POS_LE]
3060QED
3061
3062Theorem sqrt_pos_lt :
3063 !x. 0 < x ==> 0 < sqrt x
3064Proof
3065 Cases
3066 >> RW_TAC std_ss [extreal_sqrt_def, extreal_of_num_def, extreal_le_def,
3067 extreal_lt_eq, lt_infty, SQRT_POS_LT]
3068QED
3069
3070Theorem sqrt_pos_ne :
3071 !x. 0 < x ==> sqrt x <> 0
3072Proof
3073 Q.X_GEN_TAC ‘x’
3074 >> DISCH_THEN (ASSUME_TAC o (MATCH_MP sqrt_pos_lt))
3075 >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
3076 >> MATCH_MP_TAC lt_imp_ne >> art []
3077QED
3078
3079Theorem pow2_sqrt :
3080 !x. 0 <= x ==> (sqrt (x pow 2) = x)
3081Proof
3082 Cases
3083 >> RW_TAC real_ss [extreal_sqrt_def, extreal_pow_def, POW_2_SQRT, extreal_of_num_def,
3084 extreal_le_def]
3085QED
3086
3087Theorem sqrt_0 :
3088 sqrt 0 = 0
3089Proof
3090 rw [extreal_of_num_def, extreal_sqrt_def, SQRT_0]
3091QED
3092
3093Theorem sqrt_1 :
3094 sqrt 1 = 1
3095Proof
3096 rw [extreal_of_num_def, extreal_sqrt_def, SQRT_1]
3097QED
3098
3099Theorem sqrt_pow2 :
3100 !x. ((sqrt x) pow 2 = x) <=> 0 <= x
3101Proof
3102 Cases
3103 >> RW_TAC real_ss [extreal_sqrt_def, extreal_pow_def, SQRT_POW2,
3104 extreal_of_num_def, extreal_le_def]
3105 >> METIS_TAC [le_pow2, lt_infty, extreal_of_num_def, extreal_not_infty, lte_trans]
3106QED
3107
3108Theorem sqrt_mono_le :
3109 !x y. 0 <= x /\ x <= y ==> sqrt x <= sqrt y
3110Proof
3111 NTAC 2 Cases
3112 >> RW_TAC real_ss [SQRT_MONO_LE, extreal_sqrt_def, extreal_pow_def, POW_2_SQRT,
3113 extreal_of_num_def, extreal_le_def, le_infty, extreal_not_infty]
3114QED
3115
3116Theorem pow2_le_eq :
3117 !x y. 0 <= x /\ 0 <= y ==> (x <= y <=> x pow 2 <= y pow 2)
3118Proof
3119 rpt STRIP_TAC
3120 >> EQ_TAC >> DISCH_TAC >- (MATCH_MP_TAC pow_le >> art [])
3121 >> `0 <= x pow 2` by PROVE_TAC [le_pow2]
3122 >> `sqrt (x pow 2) <= sqrt (y pow 2)` by PROVE_TAC [sqrt_mono_le]
3123 >> METIS_TAC [GSYM pow2_sqrt]
3124QED
3125
3126Theorem sqrt_le_x :
3127 !(x :extreal). 1 <= x ==> sqrt x <= x
3128Proof
3129 rpt STRIP_TAC
3130 >> ‘0 <= x’ by PROVE_TAC [le_01, le_trans]
3131 >> Know ‘sqrt x <= x <=> (sqrt x) pow 2 <= x pow 2’
3132 >- (MATCH_MP_TAC pow2_le_eq >> rw [sqrt_pos_le])
3133 >> Rewr'
3134 >> ‘(sqrt x) pow 2 = x’ by rw [sqrt_pow2]
3135 >> POP_ORW
3136 >> REWRITE_TAC [pow_2]
3137 >> GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [GSYM mul_rone]
3138 >> MATCH_MP_TAC le_lmul_imp >> art []
3139QED
3140
3141(* In sqrt_le_x, if ‘x’ is an integer then ‘1 <= x’ can be dropped. *)
3142Theorem sqrt_le_n :
3143 !n. sqrt (&n :extreal) <= &n
3144Proof
3145 Q.X_GEN_TAC ‘n’
3146 >> Cases_on ‘n’ >- (rw [extreal_of_num_def, extreal_sqrt_def, SQRT_0])
3147 >> MATCH_MP_TAC sqrt_le_x
3148 >> rw [extreal_of_num_def, extreal_le_eq]
3149QED
3150
3151Theorem sqrt_mul :
3152 !x y. 0 <= x /\ 0 <= y ==> sqrt (x * y) = sqrt x * sqrt y
3153Proof
3154 rpt STRIP_TAC
3155 >> Cases_on ‘x = PosInf’
3156 >- (‘y = 0 \/ 0 < y’ by PROVE_TAC [le_lt] \\
3157 fs [extreal_sqrt_def, mul_infty, sqrt_0] \\
3158 ‘0 < sqrt y’ by PROVE_TAC [sqrt_pos_lt] \\
3159 METIS_TAC [mul_infty])
3160 >> Cases_on ‘y = PosInf’
3161 >- (‘x = 0 \/ 0 < x’ by PROVE_TAC [le_lt] \\
3162 fs [extreal_sqrt_def, mul_infty, sqrt_0] \\
3163 ‘0 < sqrt x’ by PROVE_TAC [sqrt_pos_lt] \\
3164 METIS_TAC [mul_infty])
3165 >> ‘x <> NegInf /\ y <> NegInf’ by rw [pos_not_neginf]
3166 >> ‘?X. 0 <= X /\ x = Normal X’
3167 by METIS_TAC [extreal_cases, extreal_of_num_def, extreal_le_eq] >> POP_ORW
3168 >> ‘?Y. 0 <= Y /\ y = Normal Y’
3169 by METIS_TAC [extreal_cases, extreal_of_num_def, extreal_le_eq] >> POP_ORW
3170 >> ‘0 <= X * Y’ by rw [REAL_LE_MUL]
3171 >> rw [extreal_mul_def, extreal_sqrt_def, SQRT_MUL]
3172QED
3173
3174(* ------------------------------------------------------------------------- *)
3175(* Special values *)
3176(* ------------------------------------------------------------------------- *)
3177
3178Theorem half_between[simp] :
3179 (0 < 1 / 2 /\ 1 / 2 < 1) /\ (0 <= 1 / 2 /\ 1 / 2 <= 1)
3180Proof
3181 MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``)
3182 >> CONJ_TAC >- PROVE_TAC [lt_imp_le]
3183 >> RW_TAC real_ss [extreal_div_def, extreal_inv_def, mul_lone, extreal_lt_def,
3184 extreal_le_def, extreal_of_num_def, extreal_not_infty,
3185 GSYM real_lt, REAL_INV_1OVER, extreal_mul_def]
3186QED
3187
3188Theorem half_not_infty[simp] :
3189 1 / 2 <> PosInf /\ 1 / 2 <> NegInf
3190Proof
3191 rw [lt_infty]
3192 >- (MATCH_MP_TAC lt_trans \\
3193 Q.EXISTS_TAC `1` >> rw [half_between] \\
3194 rw [extreal_of_num_def, lt_infty])
3195 >> MATCH_MP_TAC lt_trans
3196 >> Q.EXISTS_TAC `0` >> rw [half_between]
3197 >> rw [extreal_of_num_def, lt_infty]
3198QED
3199
3200Theorem thirds_between[simp] :
3201 ((0 < 1 / 3 /\ 1 / 3 < 1) /\ (0 < 2 / 3 /\ 2 / 3 < 1)) /\
3202 ((0 <= 1 / 3 /\ 1 / 3 <= 1) /\ (0 <= 2 / 3 /\ 2 / 3 <= 1))
3203Proof
3204 MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``)
3205 >> CONJ_TAC >- PROVE_TAC [lt_imp_le]
3206 >> RW_TAC real_ss [extreal_div_def, extreal_inv_def, mul_lone, extreal_lt_def,
3207 extreal_le_def, extreal_of_num_def, extreal_not_infty,
3208 GSYM real_lt, extreal_mul_def, REAL_INV_1OVER]
3209QED
3210
3211Theorem fourths_between[simp] :
3212 ((0 < 1 / 4 /\ 1 / 4 < 1) /\ (0 < 3 / 4 /\ 3 / 4 < 1)) /\
3213 ((0 <= 1 / 4 /\ 1 / 4 <= 1) /\ (0 <= 3 / 4 /\ 3 / 4 <= 1))
3214Proof
3215 MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``)
3216 >> CONJ_TAC >- PROVE_TAC [lt_imp_le]
3217 >> RW_TAC real_ss [extreal_div_def, extreal_inv_def, mul_lone, extreal_lt_def,
3218 extreal_le_def, extreal_of_num_def, extreal_not_infty,
3219 GSYM real_lt, extreal_mul_def, REAL_INV_1OVER]
3220QED
3221
3222Theorem half_cancel :
3223 2 * (1 / 2) = 1
3224Proof
3225 RW_TAC real_ss [extreal_of_num_def, extreal_mul_def, extreal_div_eq,
3226 EVAL ``2 <> 0:real``, REAL_MUL_RINV, real_div]
3227QED
3228
3229(* cf. realTheory.REAL_HALF_DOUBLE *)
3230Theorem half_double :
3231 !x :extreal. x / 2 + x / 2 = x
3232Proof
3233 ‘0 < (2 :real)’ by rw []
3234 >> Q.X_GEN_TAC ‘x’ >> Cases_on ‘x’
3235 >> rw [extreal_of_num_def, extreal_div_eq, extreal_add_def]
3236 >- rw [infty_div, extreal_add_def]
3237 >- rw [infty_div, extreal_add_def]
3238 >> REWRITE_TAC [REAL_HALF_DOUBLE]
3239QED
3240
3241(* cf. seqTheory.X_HALF_HALF *)
3242Theorem x_half_half :
3243 !x :extreal. 1 / 2 * x + 1 / 2 * x = x
3244Proof
3245 STRIP_ASSUME_TAC half_between
3246 >> Q.X_GEN_TAC ‘x’
3247 >> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [GSYM mul_lone]
3248 >> Know ‘1 * x = (1 / 2 + 1 / 2) * x’
3249 >- (rw [extreal_double, half_cancel])
3250 >> Rewr'
3251 >> MATCH_MP_TAC (GSYM add_rdistrib) >> rw []
3252QED
3253
3254Theorem third_cancel :
3255 3 * (1 / 3) = 1
3256Proof
3257 RW_TAC real_ss [extreal_of_num_def, extreal_mul_def, extreal_div_eq,
3258 EVAL ``3 <> 0:real``, REAL_MUL_RINV, real_div]
3259QED
3260
3261Theorem fourth_cancel :
3262 4 * (1 / 4) = 1
3263Proof
3264 RW_TAC real_ss [extreal_of_num_def, extreal_mul_def, extreal_div_eq,
3265 EVAL ``4 <> 0:real``, REAL_MUL_RINV, real_div]
3266QED
3267
3268(* ------------------------------------------------------------------------- *)
3269(* Minimum and maximum *)
3270(* ------------------------------------------------------------------------- *)
3271
3272Theorem extreal_min_eq :
3273 !a b. min (Normal a) (Normal b) = Normal (min a b)
3274Proof
3275 rw [min_def, extreal_min_def, extreal_le_eq]
3276QED
3277
3278Theorem extreal_max_eq :
3279 !a b. max (Normal a) (Normal b) = Normal (max a b)
3280Proof
3281 rw [max_def, extreal_max_def, extreal_le_eq]
3282QED
3283
3284Theorem min_le :
3285 !z x y. min x y <= z <=> x <= z \/ y <= z
3286Proof
3287 RW_TAC std_ss [extreal_min_def]
3288 >> PROVE_TAC [le_total, le_trans]
3289QED
3290
3291Theorem min_le1 :
3292 !x y. min x y <= x
3293Proof
3294 PROVE_TAC [min_le, le_refl]
3295QED
3296
3297Theorem min_le2 :
3298 !x y. min x y <= y
3299Proof
3300 PROVE_TAC [min_le, le_refl]
3301QED
3302
3303Theorem le_min :
3304 !z x y. z <= min x y <=> z <= x /\ z <= y
3305Proof
3306 RW_TAC std_ss [extreal_min_def]
3307 >> PROVE_TAC [le_total, le_trans]
3308QED
3309
3310Theorem min_le2_imp :
3311 !x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> min x1 x2 <= min y1 y2
3312Proof
3313 RW_TAC std_ss [le_min]
3314 >> RW_TAC std_ss [min_le]
3315QED
3316
3317Theorem min_refl :
3318 !x. min x x = x
3319Proof
3320 RW_TAC std_ss [extreal_min_def, le_refl]
3321QED
3322
3323Theorem min_comm :
3324 !x y. min x y = min y x
3325Proof
3326 RW_TAC std_ss [extreal_min_def]
3327 >> PROVE_TAC [le_antisym, le_total]
3328QED
3329
3330Theorem min_infty :
3331 !x. (min x PosInf = x) /\ (min PosInf x = x) /\
3332 (min NegInf x = NegInf) /\ (min x NegInf = NegInf)
3333Proof
3334 RW_TAC std_ss [extreal_min_def, le_infty]
3335QED
3336
3337Theorem le_max :
3338 !z x y. z <= max x y <=> z <= x \/ z <= y
3339Proof
3340 RW_TAC std_ss [extreal_max_def]
3341 >> PROVE_TAC [le_total, le_trans]
3342QED
3343
3344Theorem le_max1 :
3345 !x y. x <= max x y
3346Proof
3347 PROVE_TAC [le_max, le_refl]
3348QED
3349
3350Theorem le_max2 :
3351 !x y. y <= max x y
3352Proof
3353 PROVE_TAC [le_max, le_refl]
3354QED
3355
3356Theorem max_le :
3357 !z x y. max x y <= z <=> x <= z /\ y <= z
3358Proof
3359 RW_TAC std_ss [extreal_max_def]
3360 >> PROVE_TAC [le_total, le_trans]
3361QED
3362
3363Theorem max_le2_imp :
3364 !x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> max x1 x2 <= max y1 y2
3365Proof
3366 RW_TAC std_ss [max_le]
3367 >> RW_TAC std_ss [le_max]
3368QED
3369
3370(* cf. REAL_LT_MAX *)
3371Theorem lt_max :
3372 !x y z :extreal. x < max y z <=> x < y \/ x < z
3373Proof
3374 rw [extreal_lt_def]
3375 >> METIS_TAC [max_le]
3376QED
3377
3378Theorem lt_min :
3379 !x y z :extreal. z < min x y <=> z < x /\ z < y
3380Proof
3381 rw [extreal_lt_def]
3382 >> METIS_TAC [min_le]
3383QED
3384
3385(* cf. REAL_MAX_LT *)
3386Theorem max_lt :
3387 !x y z :extreal. max x y < z <=> x < z /\ y < z
3388Proof
3389 rw [extreal_lt_def]
3390 >> METIS_TAC [le_max]
3391QED
3392
3393Theorem max_refl[simp] :
3394 !x. max x x = x
3395Proof
3396 RW_TAC std_ss [extreal_max_def, le_refl]
3397QED
3398
3399Theorem max_comm :
3400 !x y. max x y = max y x
3401Proof
3402 RW_TAC std_ss [extreal_max_def]
3403 >> PROVE_TAC [le_antisym, le_total]
3404QED
3405
3406Theorem max_infty[simp] :
3407 !x. (max x PosInf = PosInf) /\ (max PosInf x = PosInf) /\
3408 (max NegInf x = x) /\ (max x NegInf = x)
3409Proof
3410 RW_TAC std_ss [extreal_max_def, le_infty]
3411QED
3412
3413Theorem max_reduce :
3414 !x y :extreal. x <= y \/ x < y ==> (max x y = y) /\ (max y x = y)
3415Proof
3416 PROVE_TAC [lt_imp_le, extreal_max_def, max_comm]
3417QED
3418
3419Theorem min_reduce :
3420 !x y :extreal. x <= y \/ x < y ==> (min x y = x) /\ (min y x = x)
3421Proof
3422 PROVE_TAC [lt_imp_le, extreal_min_def, min_comm]
3423QED
3424
3425Theorem lt_max_between :
3426 !x b d. x < max b d /\ b <= x ==> x < d
3427Proof
3428 RW_TAC std_ss [extreal_max_def]
3429 >> fs [GSYM extreal_lt_def]
3430 >> PROVE_TAC [let_antisym]
3431QED
3432
3433Theorem min_le_between :
3434 !x a c. min a c <= x /\ x < a ==> c <= x
3435Proof
3436 RW_TAC std_ss [extreal_min_def]
3437 >> PROVE_TAC [let_antisym]
3438QED
3439
3440Theorem abs_max :
3441 !x :extreal. abs x = max x (-x)
3442Proof
3443 GEN_TAC >> `0 <= x \/ x < 0` by PROVE_TAC [let_total]
3444 >- (`abs x = x` by PROVE_TAC [GSYM abs_refl] >> POP_ORW \\
3445 RW_TAC std_ss [GSYM le_antisym, le_max, le_refl, max_le] \\
3446 MATCH_MP_TAC le_trans >> Q.EXISTS_TAC `0` >> art [] \\
3447 POP_ASSUM (REWRITE_TAC o wrap o
3448 (REWRITE_RULE [Once (GSYM le_neg), neg_0])))
3449 >> IMP_RES_TAC abs_neg >> POP_ORW
3450 >> RW_TAC std_ss [GSYM le_antisym, le_max, le_refl, max_le]
3451 >> MATCH_MP_TAC lt_imp_le
3452 >> MATCH_MP_TAC lt_trans >> Q.EXISTS_TAC `0` >> art []
3453 >> POP_ASSUM (REWRITE_TAC o wrap o
3454 (REWRITE_RULE [Once (GSYM lt_neg), neg_0]))
3455QED
3456
3457Theorem max_0_reduce :
3458 !x. 0 <= x ==> max 0 x = (x :extreal)
3459Proof
3460 rw [extreal_max_def]
3461QED
3462
3463(* ------------------------------------------------------------------------- *)
3464(* Completeness of Extended Real Numbers *)
3465(* ------------------------------------------------------------------------- *)
3466
3467(* This is proved by REAL_MEAN, SIMP_REAL_ARCH and SIMP_REAL_ARCH_NEG *)
3468Theorem extreal_mean :
3469 !x y :extreal. x < y ==> ?z. x < z /\ z < y
3470Proof
3471 rpt STRIP_TAC
3472 >> Cases_on `y` >- fs [lt_infty]
3473 >- (Cases_on `x`
3474 >- (Q.EXISTS_TAC `Normal 0` >> REWRITE_TAC [lt_infty])
3475 >- fs [lt_infty] \\
3476 STRIP_ASSUME_TAC (Q.SPEC `r` SIMP_REAL_ARCH) \\
3477 Q.EXISTS_TAC `&SUC n` \\
3478 REWRITE_TAC [lt_infty, extreal_of_num_def, extreal_lt_eq] \\
3479 MATCH_MP_TAC REAL_LET_TRANS \\
3480 Q.EXISTS_TAC `&n` >> art [] \\
3481 SIMP_TAC real_ss [])
3482 >> Cases_on `x`
3483 >- (STRIP_ASSUME_TAC (Q.SPEC `r` SIMP_REAL_ARCH_NEG) \\
3484 Q.EXISTS_TAC `-&SUC n` \\
3485 `-&SUC n = Normal (-&(SUC n))`
3486 by PROVE_TAC [extreal_ainv_def, extreal_of_num_def] \\
3487 POP_ORW >> REWRITE_TAC [lt_infty, extreal_lt_eq] \\
3488 MATCH_MP_TAC REAL_LTE_TRANS \\
3489 Q.EXISTS_TAC `-&n` >> art [] \\
3490 SIMP_TAC real_ss [])
3491 >- fs [lt_infty]
3492 >> rename1 `Normal a < Normal b`
3493 >> `a < b` by PROVE_TAC [extreal_lt_eq]
3494 >> POP_ASSUM (STRIP_ASSUME_TAC o (MATCH_MP REAL_MEAN))
3495 >> Q.EXISTS_TAC `Normal z` >> art [extreal_lt_eq]
3496QED
3497
3498Theorem EXTREAL_ARCH :
3499 !x. 0 < x ==> !y. y <> PosInf ==> ?n. y < &n * x
3500Proof
3501 Cases
3502 >| [ (* goal 1 (of 3) *)
3503 RW_TAC std_ss [lt_infty],
3504 (* goal 2 (of 3) *)
3505 RW_TAC std_ss [lt_infty] \\
3506 Q.EXISTS_TAC `1` >> RW_TAC std_ss [mul_lone, lt_infty],
3507 (* goal 3 (of 3) *)
3508 RW_TAC std_ss [lt_infty] \\
3509 Cases_on `y = NegInf`
3510 >- (Q.EXISTS_TAC `1` >> RW_TAC std_ss [mul_lone, lt_infty]) \\
3511 `?z. y = Normal z` by METIS_TAC [extreal_cases, lt_infty] \\
3512 `0 < r` by METIS_TAC [extreal_lt_eq, extreal_of_num_def] \\
3513 `?n. z < &n * r` by METIS_TAC [REAL_ARCH] \\
3514 Q.EXISTS_TAC `n` \\
3515 RW_TAC real_ss [extreal_lt_eq, REAL_LE_MUL, extreal_of_num_def,
3516 extreal_mul_def] ]
3517QED
3518
3519Theorem SIMP_EXTREAL_ARCH :
3520 !x. x <> PosInf ==> ?n. x <= &n
3521Proof
3522 Cases
3523 >> RW_TAC std_ss [le_infty]
3524 >> `?n. r <= &n` by RW_TAC std_ss [SIMP_REAL_ARCH]
3525 >> Q.EXISTS_TAC `n`
3526 >> RW_TAC real_ss [extreal_of_num_def,extreal_le_def]
3527QED
3528
3529Theorem SIMP_EXTREAL_ARCH_NEG :
3530 !x. x <> NegInf ==> ?n. -&n <= x
3531Proof
3532 Cases
3533 >> RW_TAC std_ss [le_infty]
3534 >> `?n. - &n <= r` by RW_TAC std_ss [SIMP_REAL_ARCH_NEG]
3535 >> Q.EXISTS_TAC `n`
3536 >> RW_TAC real_ss [extreal_of_num_def, extreal_le_eq, extreal_ainv_def]
3537QED
3538
3539Theorem EXTREAL_ARCH_INV :
3540 !(x :extreal). 0 < x ==> ?n. inv (&SUC n) < x
3541Proof
3542 rpt STRIP_TAC
3543 >> Cases_on ‘x = PosInf’
3544 >- (Q.EXISTS_TAC ‘0’ >> rw [inv_one, lt_infty])
3545 >> ‘x <> 0’ by PROVE_TAC [lt_imp_ne]
3546 >> Know ‘?n. inv x <= &n’
3547 >- (MATCH_MP_TAC SIMP_EXTREAL_ARCH \\
3548 METIS_TAC [inv_not_infty])
3549 >> STRIP_TAC
3550 >> ‘&n < &SUC n’ by rw [extreal_of_num_def, extreal_lt_eq]
3551 >> ‘inv x < &SUC n’ by PROVE_TAC [let_trans]
3552 >> Q.EXISTS_TAC ‘n’
3553 >> Know ‘x = inv (inv x)’
3554 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
3555 MATCH_MP_TAC inv_inv >> art [] \\
3556 rw [lt_infty] \\
3557 MATCH_MP_TAC lt_trans >> Q.EXISTS_TAC ‘0’ >> art [] \\
3558 rw [extreal_of_num_def, lt_infty])
3559 >> Rewr'
3560 >> Suff ‘inv (&SUC n) < inv (inv x) <=> inv x < &SUC n’ >- rw []
3561 >> MATCH_MP_TAC inv_lt_antimono
3562 >> CONJ_TAC >- rw [extreal_of_num_def, extreal_lt_eq]
3563 >> MATCH_MP_TAC inv_pos' >> rw []
3564QED
3565
3566Theorem EXTREAL_ARCH_INV' :
3567 !(x :extreal). 0 < x ==> ?n. inv (&SUC n) <= x
3568Proof
3569 rpt STRIP_TAC
3570 >> ‘?n. inv (&SUC n) < x’ by METIS_TAC [EXTREAL_ARCH_INV]
3571 >> Q.EXISTS_TAC ‘n’
3572 >> MATCH_MP_TAC lt_imp_le >> art []
3573QED
3574
3575Theorem real_11 :
3576 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
3577 (real x = real y <=> x = y)
3578Proof
3579 rpt STRIP_TAC
3580 >> reverse EQ_TAC >- rw []
3581 >> Cases_on ‘x’ >> fs [real_normal]
3582 >> Cases_on ‘y’ >> fs [real_normal]
3583QED
3584
3585(* NOTE: The (good) theorem name is given by Kai Phan *)
3586Theorem real_lt_eq :
3587 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
3588 (real x < real y <=> x < y)
3589Proof
3590 rpt STRIP_TAC
3591 >> ‘∃a. x = Normal a’ by METIS_TAC [extreal_cases]
3592 >> ‘∃b. y = Normal b’ by METIS_TAC [extreal_cases]
3593 >> ASM_SIMP_TAC std_ss [real_normal, extreal_lt_eq]
3594QED
3595
3596Theorem real_le_eq :
3597 !x y. x <> PosInf /\ x <> NegInf /\ y <> PosInf /\ y <> NegInf ==>
3598 (real x <= real y <=> x <= y)
3599Proof
3600 rpt STRIP_TAC
3601 >> ‘?a. x = Normal a’ by METIS_TAC [extreal_cases]
3602 >> ‘?b. y = Normal b’ by METIS_TAC [extreal_cases]
3603 >> ASM_SIMP_TAC std_ss [real_normal, extreal_le_eq]
3604QED
3605
3606Theorem le_real_imp :
3607 !x y. 0 <= x /\ x <= y /\ y <> PosInf ==> real x <= real y
3608Proof
3609 rpt STRIP_TAC
3610 >> ‘0 <= y’ by PROVE_TAC [le_trans]
3611 >> Know ‘x <> PosInf’
3612 >- (fs [lt_infty] \\
3613 Q_TAC (TRANS_TAC let_trans) ‘y’ >> art [])
3614 >> DISCH_TAC
3615 >> ‘x <> NegInf /\ y <> NegInf’ by PROVE_TAC [pos_not_neginf]
3616 >> ‘?a. x = Normal a’ by METIS_TAC [extreal_cases]
3617 >> ‘?b. y = Normal b’ by METIS_TAC [extreal_cases]
3618 >> ASM_SIMP_TAC std_ss [real_normal]
3619 >> Q.PAT_X_ASSUM ‘x <= y’ MP_TAC
3620 >> ASM_SIMP_TAC std_ss [extreal_le_eq]
3621QED
3622
3623Theorem real_positive :
3624 !x. 0 <= x ==> 0 <= real x
3625Proof
3626 Q.X_GEN_TAC ‘x’
3627 >> Cases_on ‘x’ >> simp [extreal_of_num_def, extreal_le_eq]
3628QED
3629
3630Theorem pow_real :
3631 !x n. x <> PosInf /\ x <> NegInf ==> real x pow n = real (x pow n)
3632Proof
3633 rw []
3634 >> ASM_SIMP_TAC std_ss [GSYM extreal_11, normal_real, pow_not_infty]
3635 >> ‘?r. x = Normal r’ by METIS_TAC [extreal_cases]
3636 >> gs [real_normal, extreal_pow_def]
3637QED
3638
3639Theorem add_real :
3640 !x y. x <> PosInf /\ x <> NegInf /\
3641 y <> PosInf /\ y <> NegInf ==> real (x + y) = real x + real y
3642Proof
3643 rw []
3644 >> ASM_SIMP_TAC std_ss [GSYM extreal_11, normal_real, add_not_infty,
3645 GSYM extreal_add_eq]
3646QED
3647
3648Theorem sub_real :
3649 !x y. x <> PosInf /\ x <> NegInf /\
3650 y <> PosInf /\ y <> NegInf ==> real (x - y) = real x - real y
3651Proof
3652 rw []
3653 >> ASM_SIMP_TAC std_ss [GSYM extreal_11, normal_real, sub_not_infty,
3654 GSYM extreal_sub_eq]
3655QED
3656
3657Theorem mul_real :
3658 !x y. x <> PosInf /\ x <> NegInf /\
3659 y <> PosInf /\ y <> NegInf ==> real (x * y) = real x * real y
3660Proof
3661 rpt STRIP_TAC
3662 >> ‘?a. x = Normal a’ by METIS_TAC [extreal_cases]
3663 >> ‘?b. y = Normal b’ by METIS_TAC [extreal_cases]
3664 >> simp [real_normal, extreal_mul_eq]
3665QED
3666
3667(*****************)
3668(* Ceiling *)
3669(*****************)
3670
3671Definition ceiling_def :
3672 ceiling (Normal x) = LEAST (n:num). x <= &n
3673End
3674
3675Theorem CEILING_LBOUND :
3676 !x. Normal x <= &(ceiling (Normal x))
3677Proof
3678 RW_TAC std_ss [ceiling_def]
3679 >> LEAST_ELIM_TAC
3680 >> REWRITE_TAC [SIMP_REAL_ARCH]
3681 >> METIS_TAC [extreal_of_num_def, extreal_le_def]
3682QED
3683
3684Theorem CEILING_UBOUND :
3685 !x. (0 <= x) ==> &(ceiling (Normal x)) < (Normal x) + 1
3686Proof
3687 RW_TAC std_ss [ceiling_def, extreal_of_num_def, extreal_add_def, extreal_lt_eq]
3688 >> LEAST_ELIM_TAC
3689 >> REWRITE_TAC [SIMP_REAL_ARCH]
3690 >> RW_TAC real_ss []
3691 >> FULL_SIMP_TAC real_ss [GSYM real_lt]
3692 >> PAT_X_ASSUM ``!m. P`` (MP_TAC o Q.SPEC `n-1`)
3693 >> RW_TAC real_ss []
3694 >> Cases_on `n = 0` >- METIS_TAC [REAL_LET_ADD2, REAL_LT_01, REAL_ADD_RID]
3695 >> `0 < n` by RW_TAC real_ss []
3696 >> `&(n - 1) < x:real` by RW_TAC real_ss []
3697 >> `0 <= n-1` by RW_TAC real_ss []
3698 >> `0:real <= (&(n-1))` by RW_TAC real_ss []
3699 >> `0 < x` by METIS_TAC [REAL_LET_TRANS]
3700 >> Cases_on `n = 1`
3701 >- METIS_TAC [REAL_LE_REFL, REAL_ADD_RID, REAL_LTE_ADD2, REAL_ADD_COMM]
3702 >> `0 <> n-1` by RW_TAC real_ss []
3703 >> `&n - 1 < x` by RW_TAC real_ss [REAL_SUB]
3704 >> FULL_SIMP_TAC real_ss [REAL_LT_SUB_RADD]
3705QED
3706
3707(* ========================================================================= *)
3708(* Subsets of extended real numbers *)
3709(* ========================================================================= *)
3710
3711(* convert an extreal set to a real set, used in borelTheory *)
3712Definition real_set_def :
3713 real_set s = {real x | x <> PosInf /\ x <> NegInf /\ x IN s}
3714End
3715
3716Theorem real_set_empty[simp] :
3717 real_set {} = {}
3718Proof
3719 simp [real_set_def]
3720QED
3721
3722Theorem real_set_infty[simp] :
3723 real_set {PosInf} = {} /\ real_set {NegInf} = {}
3724Proof
3725 simp [real_set_def]
3726 >> rw [Once EXTENSION, NOT_IN_EMPTY]
3727QED
3728
3729Theorem normal_real_set :
3730 !(s :extreal set). s INTER (IMAGE Normal UNIV) = IMAGE Normal (real_set s)
3731Proof
3732 rw [Once EXTENSION, real_set_def]
3733 >> EQ_TAC >> rw []
3734 >- (rename1 ‘Normal y IN s’ \\
3735 Q.EXISTS_TAC ‘Normal y’ >> rw [real_normal, extreal_not_infty])
3736 >> rename1 ‘Normal (real y) IN s’
3737 >> Suff ‘Normal (real y) = y’ >- rw []
3738 >> MATCH_MP_TAC normal_real >> art []
3739QED
3740
3741Theorem real_set_UNION :
3742 !s t. real_set (s UNION t) = real_set s UNION real_set t
3743Proof
3744 rw [Once EXTENSION, real_set_def]
3745 >> EQ_TAC >> rw [] >> rename1 ‘y <> PosInf’ (* 4 subgoals *)
3746 >| [ (* goal 1 (of 4) *)
3747 DISJ1_TAC >> Q.EXISTS_TAC ‘y’ >> art [],
3748 (* goal 2 (of 4) *)
3749 DISJ2_TAC >> Q.EXISTS_TAC ‘y’ >> art [],
3750 (* goal 3 (of 4) *)
3751 Q.EXISTS_TAC ‘y’ >> simp [],
3752 (* goal 4 (of 4) *)
3753 Q.EXISTS_TAC ‘y’ >> simp [] ]
3754QED
3755
3756Theorem real_set_INTER :
3757 !s t. real_set (s INTER t) = real_set s INTER real_set t
3758Proof
3759 rw [Once EXTENSION, real_set_def]
3760 >> EQ_TAC >> rw [] >> rename1 ‘y <> PosInf’ (* 3 subgoals *)
3761 >| [ (* goal 1 (of 3) *)
3762 Q.EXISTS_TAC ‘y’ >> art [],
3763 (* goal 2 (of 3) *)
3764 Q.EXISTS_TAC ‘y’ >> art [],
3765 (* goal 3 (of 3) *)
3766 rename1 ‘real y = real x’ \\
3767 ‘y = x’ by METIS_TAC [real_11] \\
3768 Q.EXISTS_TAC ‘y’ >> simp [] ]
3769QED
3770
3771(* new definition based on real_rat_set (q_set), now in real_of_ratTheory *)
3772Definition Q_set :
3773 Q_set = IMAGE Normal q_set
3774End
3775
3776(* DOUBLE-STRUCK CAPITAL Q, plus a "star" of superscript *)
3777val _ = Unicode.unicode_version {u = UTF8.chr 0x211A ^ UTF8.chr 0xA673,
3778 tmnm = "Q_set"};
3779val _ = TeX_notation {hol = "Q_set",
3780 TeX = ("\\ensuremath{\\mathbb{Q}\\HOLTokenSupStar{}}", 1)};
3781
3782(* old definition as equivalent theorem (not used anywhere) *)
3783Theorem Q_set_def :
3784 Q_set = {x | ?a b. (x = (&a / &b)) /\ ((0 :extreal) < &b)} UNION
3785 {x | ?a b. (x = -(&a / &b)) /\ ((0 :extreal) < &b)}
3786Proof
3787 rw [Q_set, real_rat_set_def, extreal_of_num_def, extreal_lt_eq, Once EXTENSION]
3788 >> EQ_TAC >> rw []
3789 >| [ (* goal 1 (of 4) *)
3790 DISJ1_TAC >> qexistsl_tac [‘a’, ‘b’] >> art [] \\
3791 ‘&b <> (0 :real)’ by rw [] \\
3792 ‘&b <> (0 :extreal)’ by METIS_TAC [extreal_11, extreal_of_num_def] \\
3793 rw [extreal_div_eq],
3794 (* goal 2 (of 4) *)
3795 DISJ2_TAC >> qexistsl_tac [‘a’, ‘b’] >> art [GSYM extreal_ainv_def] \\
3796 Suff ‘Normal (&a / &b) = Normal (&a) / Normal (&b)’ >- Rewr \\
3797 ‘&b <> (0 :real)’ by rw [] \\
3798 ‘&b <> (0 :extreal)’ by METIS_TAC [extreal_11, extreal_of_num_def] \\
3799 rw [extreal_div_eq],
3800 (* goal 3 (of 4) *)
3801 DISJ1_TAC >> Q.EXISTS_TAC ‘&a / &b’ \\
3802 ‘&b <> (0 :real)’ by rw [] \\
3803 ‘&b <> (0 :extreal)’ by METIS_TAC [extreal_11, extreal_of_num_def] \\
3804 rw [extreal_div_eq] \\
3805 qexistsl_tac [‘a’, ‘b’] >> art [] >> simp[],
3806 (* goal 4 (of 4) *)
3807 DISJ2_TAC >> Q.EXISTS_TAC ‘-(&a / &b)’ \\
3808 ‘&b <> (0 :real)’ by rw [] \\
3809 ‘&b <> (0 :extreal)’ by METIS_TAC [extreal_11, extreal_of_num_def] \\
3810 rw [extreal_div_eq, GSYM extreal_ainv_def] \\
3811 qexistsl_tac [‘a’, ‘b’] >> art [] >> simp[] ]
3812QED
3813
3814Theorem Q_not_infty :
3815 !x. x IN Q_set ==> ?y. x = Normal y
3816Proof
3817 rw [Q_set]
3818QED
3819
3820Theorem Q_COUNTABLE :
3821 countable Q_set
3822Proof
3823 REWRITE_TAC [Q_set]
3824 >> MATCH_MP_TAC image_countable
3825 >> REWRITE_TAC [QSET_COUNTABLE]
3826QED
3827
3828Theorem NUM_IN_Q :
3829 !n:num. (&n IN Q_set) /\ (-&n IN Q_set)
3830Proof
3831 rw [Q_set]
3832 >| [ (* goal 1 (of 2) *)
3833 Q.EXISTS_TAC ‘&n’ \\
3834 rw [extreal_of_num_def, NUM_IN_QSET],
3835 (* goal 2 (of 2) *)
3836 Q.EXISTS_TAC ‘-&n’ \\
3837 rw [extreal_of_num_def, NUM_IN_QSET, GSYM extreal_ainv_def] ]
3838QED
3839
3840Theorem Q_INFINITE :
3841 INFINITE Q_set
3842Proof
3843 `{x | ?n:num. x = (&n)} SUBSET Q_set`
3844 by (RW_TAC std_ss [SUBSET_DEF,EXTENSION,GSPECIFICATION]
3845 >> METIS_TAC [NUM_IN_Q])
3846 >> Suff `~(FINITE {x | ?n:num. x = (&n)})`
3847 >- METIS_TAC [INFINITE_SUBSET]
3848 >> RW_TAC std_ss []
3849 >> MATCH_MP_TAC (INST_TYPE [alpha |-> ``:num``] INFINITE_INJ)
3850 >> Q.EXISTS_TAC `(\n. &n)`
3851 >> Q.EXISTS_TAC `UNIV`
3852 >> RW_TAC real_ss [INFINITE_NUM_UNIV, INJ_DEF,GSPECIFICATION]
3853 >- METIS_TAC []
3854 >> FULL_SIMP_TAC real_ss [extreal_11,extreal_of_num_def]
3855QED
3856
3857Theorem OPP_IN_Q :
3858 !x. x IN Q_set ==> -x IN Q_set
3859Proof
3860 rw [Q_set] >> rename1 ‘x IN q_set’
3861 >> Q.EXISTS_TAC ‘-x’
3862 >> rw [extreal_ainv_def, OPP_IN_QSET]
3863QED
3864
3865Theorem INV_IN_Q :
3866 !x. (x IN Q_set) /\ (x <> 0) ==> 1 / x IN Q_set
3867Proof
3868 rw [Q_set, extreal_of_num_def, extreal_11] >> rename1 ‘x IN q_set’
3869 >> Q.EXISTS_TAC ‘1 / x’
3870 >> rw [extreal_div_eq, INV_IN_QSET]
3871QED
3872
3873Theorem ADD_IN_Q :
3874 !x y. (x IN Q_set) /\ (y IN Q_set) ==> (x + y IN Q_set)
3875Proof
3876 rw [Q_set]
3877 >> Q.EXISTS_TAC ‘x' + x''’
3878 >> rw [extreal_add_def, ADD_IN_QSET]
3879QED
3880
3881Theorem SUB_IN_Q :
3882 !x y. (x IN Q_set) /\ (y IN Q_set) ==> (x - y IN Q_set)
3883Proof
3884 rw [Q_set]
3885 >> Q.EXISTS_TAC ‘x' - x''’
3886 >> rw [extreal_sub_def, SUB_IN_QSET]
3887QED
3888
3889Theorem MUL_IN_Q :
3890 !x y. (x IN Q_set) /\ (y IN Q_set) ==> (x * y IN Q_set)
3891Proof
3892 rw [Q_set]
3893 >> Q.EXISTS_TAC ‘x' * x''’
3894 >> rw [extreal_mul_def, MUL_IN_QSET]
3895QED
3896
3897Theorem DIV_IN_Q :
3898 !x y. (x IN Q_set) /\ (y IN Q_set) /\ (y <> 0) ==> (x / y IN Q_set)
3899Proof
3900 rw [Q_set, extreal_of_num_def, extreal_11]
3901 >> Q.EXISTS_TAC ‘x' / x''’
3902 >> rw [extreal_div_eq, DIV_IN_QSET]
3903QED
3904
3905Theorem CMUL_IN_Q :
3906 !z:num x. x IN Q_set ==> (&z * x IN Q_set) /\ (-&z * x IN Q_set)
3907Proof
3908 rpt STRIP_TAC
3909 >| [ (* goal 1 (of 2) *)
3910 MATCH_MP_TAC MUL_IN_Q >> art [NUM_IN_Q],
3911 (* goal 2 (of 2) *)
3912 MATCH_MP_TAC MUL_IN_Q >> art [NUM_IN_Q] ]
3913QED
3914
3915Theorem rat_not_infty :
3916 !r. r IN Q_set ==> r <> NegInf /\ r <> PosInf
3917Proof
3918 rw [Q_set]
3919QED
3920
3921Theorem Q_DENSE_IN_R_LEMMA :
3922 !x y. 0 <= x /\ x < y ==> ?r. r IN Q_set /\ x < r /\ r < y
3923Proof
3924 rw [Q_set]
3925 >> Cases_on ‘x = PosInf’ >- fs [lt_infty]
3926 >> Know ‘x <> NegInf’ >- (MATCH_MP_TAC pos_not_neginf >> art [])
3927 >> DISCH_TAC
3928 >> ‘0 <= real x’
3929 by (rw [GSYM extreal_le_eq, normal_real, GSYM extreal_of_num_def])
3930 >> Cases_on ‘y = PosInf’
3931 >- (rw [GSYM lt_infty] \\
3932 MP_TAC (Q.SPECL [‘real x’, ‘real x + 1’] Q_DENSE_IN_REAL_LEMMA) \\
3933 ‘real x < real x + 1’ by rw [REAL_LT_ADDR] \\
3934 RW_TAC std_ss [] \\
3935 Q.EXISTS_TAC ‘Normal r’ >> rw [extreal_not_infty] \\
3936 ‘x = Normal (real x)’ by METIS_TAC [normal_real] >> POP_ORW \\
3937 rw [extreal_lt_eq])
3938 >> Know ‘y <> NegInf’
3939 >- (MATCH_MP_TAC pos_not_neginf \\
3940 MATCH_MP_TAC lt_imp_le \\
3941 MATCH_MP_TAC let_trans \\
3942 Q.EXISTS_TAC ‘x’ >> art [])
3943 >> DISCH_TAC
3944 >> MP_TAC (Q.SPECL [‘real x’, ‘real y’] Q_DENSE_IN_REAL_LEMMA)
3945 >> ‘real x < real y’ by METIS_TAC [GSYM extreal_lt_eq, normal_real]
3946 >> RW_TAC std_ss []
3947 >> Q.EXISTS_TAC ‘Normal r’ >> rw []
3948 >| [ (* goal 1 (of 2) *)
3949 ‘x = Normal (real x)’ by METIS_TAC [normal_real] >> POP_ORW \\
3950 rw [extreal_lt_eq],
3951 (* goal 2 (of 2) *)
3952 ‘y = Normal (real y)’ by METIS_TAC [normal_real] >> POP_ORW \\
3953 rw [extreal_lt_eq] ]
3954QED
3955
3956Theorem Q_DENSE_IN_R :
3957 !x y. (x < y) ==> ?r. (r IN Q_set) /\ (x < r) /\ (r < y)
3958Proof
3959 RW_TAC std_ss []
3960 >> Cases_on `0<=x` >- RW_TAC std_ss [Q_DENSE_IN_R_LEMMA]
3961 >> FULL_SIMP_TAC std_ss [GSYM extreal_lt_def]
3962 >> `y <> NegInf` by METIS_TAC [lt_infty]
3963 >> (Cases_on `y` >> RW_TAC std_ss [])
3964 >- (Q.EXISTS_TAC `0` \\
3965 METIS_TAC [NUM_IN_Q,extreal_of_num_def,extreal_not_infty,lt_infty])
3966 >> `x <> PosInf`
3967 by METIS_TAC [lt_infty,lt_trans,extreal_not_infty,extreal_of_num_def]
3968 >> Cases_on `x = NegInf`
3969 >- (Cases_on `0<=r`
3970 >- (Q.EXISTS_TAC ‘&ceiling (Normal r) - 1’ \\
3971 RW_TAC std_ss [extreal_of_num_def, extreal_sub_def, extreal_not_infty,
3972 lt_infty, extreal_lt_eq]
3973 >- METIS_TAC [SUB_IN_Q,NUM_IN_Q,extreal_sub_def,extreal_of_num_def]
3974 >> METIS_TAC [CEILING_UBOUND,REAL_LT_SUB_RADD,extreal_of_num_def,
3975 extreal_lt_eq,extreal_add_def])
3976 >> Q.EXISTS_TAC `- &ceiling (Normal (-r)) - 1`
3977 >> RW_TAC std_ss [extreal_of_num_def,extreal_sub_def,extreal_not_infty,
3978 lt_infty,extreal_lt_eq,extreal_ainv_def]
3979 >- METIS_TAC [SUB_IN_Q,NUM_IN_Q,extreal_sub_def,extreal_of_num_def,OPP_IN_Q,
3980 extreal_ainv_def]
3981 >> (MP_TAC o Q.SPEC `-r`) CEILING_LBOUND
3982 >> RW_TAC std_ss [extreal_of_num_def,extreal_le_def]
3983 >> POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM REAL_LE_NEG])
3984 >> RW_TAC std_ss [REAL_NEG_NEG]
3985 >> METIS_TAC [REAL_LT_SUB_RADD,REAL_LET_TRANS,REAL_LT_ADDR,REAL_LT_01])
3986 >> `?r. x = Normal r` by METIS_TAC [extreal_cases]
3987 >> FULL_SIMP_TAC std_ss [extreal_of_num_def,extreal_lt_eq]
3988 >> `Normal (-r') <= &(ceiling (Normal (-r')))` by RW_TAC real_ss [CEILING_LBOUND]
3989 >> `-Normal (r') <= &ceiling (Normal (-r'))` by METIS_TAC [extreal_ainv_def]
3990 >> `0 <= Normal (r') + &(ceiling (Normal (-r')))`
3991 by METIS_TAC [le_lneg,extreal_of_num_def,extreal_add_def,extreal_not_infty]
3992 >> `&(ceiling (Normal (-r'))) <> NegInf /\ &(ceiling (Normal (-r'))) <> PosInf`
3993 by METIS_TAC [extreal_of_num_def,extreal_not_infty]
3994 >> `Normal (r') + &(ceiling (Normal (-r'))) < Normal (r) + &(ceiling (Normal (-r')))`
3995 by METIS_TAC [extreal_lt_eq,lt_radd]
3996 >> Suff `?r2. (r2 IN Q_set) /\ (Normal r' + &ceiling (Normal (-r')) < r2) /\
3997 (r2 < Normal r + &ceiling (Normal (-r')))`
3998 >- (RW_TAC std_ss []
3999 >> Q.EXISTS_TAC `r2 - &ceiling (Normal (-r'))`
4000 >> CONJ_TAC >- METIS_TAC [SUB_IN_Q,NUM_IN_Q,extreal_of_num_def]
4001 >> `?y. r2 = Normal y` by METIS_TAC [Q_not_infty]
4002 >> FULL_SIMP_TAC std_ss [extreal_of_num_def,extreal_lt_eq,extreal_le_def,
4003 extreal_sub_def,extreal_add_def]
4004 >> RW_TAC std_ss [GSYM REAL_LT_ADD_SUB,REAL_LT_SUB_RADD])
4005 >> RW_TAC std_ss [Q_DENSE_IN_R_LEMMA]
4006QED
4007
4008(* NOTE: This version asserts a real number instead of extreal number. *)
4009Theorem Q_DENSE_IN_R' :
4010 !x y. x < y ==> ?r. r IN q_set /\ x < Normal r /\ Normal r < y
4011Proof
4012 rpt STRIP_TAC
4013 >> drule Q_DENSE_IN_R >> rw [Q_set]
4014 >> rename1 ‘r IN q_set’
4015 >> Q.EXISTS_TAC ‘r’ >> art []
4016QED
4017
4018Theorem COUNTABLE_ENUM_Q :
4019 !c. countable c <=> (c = {}) \/ (?f:extreal->'a. c = IMAGE f Q_set)
4020Proof
4021 RW_TAC std_ss []
4022 >> reverse EQ_TAC
4023 >- (NTAC 2 (RW_TAC std_ss [countable_EMPTY])
4024 >> RW_TAC std_ss [image_countable, Q_COUNTABLE])
4025 >> reverse (RW_TAC std_ss [COUNTABLE_ALT_BIJ])
4026 >- (DISJ2_TAC
4027 >> `countable Q_set` by RW_TAC std_ss [Q_COUNTABLE]
4028 >> `~(FINITE Q_set)` by RW_TAC std_ss [Q_INFINITE]
4029 >> (MP_TAC o Q.SPEC `Q_set`)
4030 (INST_TYPE [alpha |-> ``:extreal``] COUNTABLE_ALT_BIJ)
4031 >> RW_TAC std_ss []
4032 >> (MP_TAC o Q.SPECL [`enumerate Q_set`,`UNIV`,`Q_set`])
4033 (INST_TYPE [alpha |-> ``:num``, ``:'b`` |-> ``:extreal``] BIJ_INV)
4034 >> (MP_TAC o Q.SPECL [`enumerate c`,`UNIV`,`c`])
4035 (INST_TYPE [alpha |-> ``:num``, ``:'b`` |-> ``:'a``] BIJ_INV)
4036 >> RW_TAC std_ss []
4037 >> Q.EXISTS_TAC `(enumerate c) o g'`
4038 >> RW_TAC std_ss [IMAGE_DEF,EXTENSION,GSPECIFICATION]
4039 >> EQ_TAC
4040 >- (RW_TAC std_ss []
4041 >> Q.EXISTS_TAC `enumerate Q_set (g x)`
4042 >- METIS_TAC [BIJ_DEF,INJ_DEF]
4043 >> METIS_TAC [BIJ_DEF,INJ_DEF])
4044 >> RW_TAC std_ss []
4045 >> METIS_TAC [BIJ_DEF,INJ_DEF])
4046 >> POP_ASSUM MP_TAC
4047 >> Q.SPEC_TAC (`c`, `c`)
4048 >> HO_MATCH_MP_TAC FINITE_INDUCT
4049 >> RW_TAC std_ss []
4050 >- (DISJ2_TAC
4051 >> Q.EXISTS_TAC `K e`
4052 >> RW_TAC std_ss [EXTENSION, IN_SING, IN_IMAGE, IN_UNIV, K_THM]
4053 >> EQ_TAC
4054 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `0` >> METIS_TAC [NUM_IN_Q])
4055 >> RW_TAC std_ss [])
4056 >> DISJ2_TAC
4057 >> ASSUME_TAC (Q.SPECL [`f:extreal->'a`,`Q_set`,`IMAGE f Q_set`]
4058 (INST_TYPE [alpha |-> ``:extreal``, ``:'b`` |-> ``:'a``]
4059 INFINITE_INJ))
4060 >> `~(INJ f Q_set (IMAGE f Q_set))` by METIS_TAC [MONO_NOT,Q_INFINITE]
4061 >> FULL_SIMP_TAC std_ss [INJ_DEF] >- METIS_TAC [IN_IMAGE]
4062 >> Q.EXISTS_TAC `(\u. if u=x then e else f u)`
4063 >> `Q_set = (Q_set DIFF {x}) UNION {x}`
4064 by (RW_TAC std_ss [DIFF_DEF,UNION_DEF,EXTENSION,GSPECIFICATION,IN_SING] \\
4065 METIS_TAC [])
4066 >> `(IMAGE (\u. if u = x then e else f u) Q_set) =
4067 (IMAGE (\u. if u = x then e else f u) (Q_set DIFF {x})) UNION
4068 (IMAGE (\u. if u = x then e else f u) {x})`
4069 by METIS_TAC [IMAGE_UNION]
4070 >> `IMAGE (\u. if u = x then e else f u) {x} = {e}`
4071 by RW_TAC std_ss [IMAGE_DEF,EXTENSION,GSPECIFICATION,IN_SING]
4072 >> `IMAGE (\u. if u = x then e else f u) (Q_set DIFF {x}) = IMAGE f Q_set`
4073 by ( RW_TAC std_ss [IMAGE_DEF,EXTENSION,GSPECIFICATION,DIFF_DEF,
4074 IN_UNION,IN_SING] \\
4075 METIS_TAC[] )
4076 >> `IMAGE f Q_set = (IMAGE f (Q_set DIFF {x})) UNION (IMAGE f {x})`
4077 by METIS_TAC [IMAGE_UNION]
4078 >> `IMAGE f {x} = {f y}`
4079 by RW_TAC std_ss [IMAGE_DEF,EXTENSION,GSPECIFICATION,IN_SING]
4080 >> `IMAGE f Q_set = (IMAGE f (Q_set DIFF {x})) UNION {f y}` by METIS_TAC []
4081 >> `{f y} SUBSET IMAGE f (Q_set DIFF {x})`
4082 by ( RW_TAC std_ss [SUBSET_DEF,IN_IMAGE,IN_SING] >> Q.EXISTS_TAC `y` \\
4083 RW_TAC std_ss [IN_DIFF,IN_SING] )
4084 >> `IMAGE f Q_set = IMAGE f (Q_set DIFF {x})`
4085 by METIS_TAC [SUBSET_UNION_ABSORPTION,UNION_COMM]
4086 >> `IMAGE (\u. if u = x then e else f u) (Q_set DIFF {x}) =
4087 IMAGE f (Q_set DIFF {x})`
4088 by (RW_TAC std_ss [IMAGE_DEF,EXTENSION,GSPECIFICATION,DIFF_DEF,IN_SING] \\
4089 ( EQ_TAC >- ( RW_TAC std_ss [] >> Q.EXISTS_TAC `u` >> RW_TAC std_ss [] )
4090 >> RW_TAC std_ss []
4091 >> Q.EXISTS_TAC `x''`
4092 >> RW_TAC std_ss [] ))
4093 >> METIS_TAC [INSERT_SING_UNION,UNION_COMM]
4094QED
4095
4096(* ------------------------------------------------------------------------- *)
4097(* Contract and expand (extreal to/from real, order-preserving) *)
4098(* ------------------------------------------------------------------------- *)
4099
4100(* The function “contract” and “expand” maps [-inf,+inf] to/from [-1,1]. [5] *)
4101Definition contract_def :
4102 contract (Normal r) = r / (1 + abs r) /\
4103 contract PosInf = 1 /\
4104 contract NegInf = -1
4105End
4106
4107Theorem contract_lemma[local] :
4108 !r. -1 < r / (1 + abs r) /\ r / (1 + abs r) < (1 :real)
4109Proof
4110 Q.X_GEN_TAC ‘r’
4111 >> ‘0 <= abs r’ by simp [ABS_POS]
4112 >> ‘0 < 1 + abs r’ by REAL_ASM_ARITH_TAC
4113 >> ‘1 + abs r <> 0’ by simp [REAL_LT_IMP_NE]
4114 >> MP_TAC (Q.SPECL [‘-1’, ‘r’, ‘1 + abs r’] REAL_LT_RDIV_EQ) >> simp []
4115 >> Cases_on ‘0 <= r’
4116 >- (‘abs r = r’ by simp [ABS_REFL] >> POP_ORW >> simp [] \\
4117 POP_ASSUM MP_TAC >> REAL_ARITH_TAC)
4118 >> fs [REAL_NOT_LE]
4119 >> ‘abs r = -r’ by simp [ABS_EQ_NEG] >> POP_ORW
4120 >> POP_ASSUM MP_TAC >> REAL_ARITH_TAC
4121QED
4122
4123Theorem abs_contract_lt_1 :
4124 !r. abs (contract (Normal r)) < 1
4125Proof
4126 rw [ABS_BOUNDS_LT, contract_def, contract_lemma]
4127QED
4128
4129Theorem abs_contract_le_1 :
4130 !x. abs (contract x) <= 1
4131Proof
4132 Q.X_GEN_TAC ‘x’
4133 >> Cases_on ‘x’ >> simp [contract_def, ABS_BOUNDS]
4134 >> CONJ_TAC >> MATCH_MP_TAC REAL_LT_IMP_LE
4135 >> REWRITE_TAC [contract_lemma]
4136QED
4137
4138Theorem contract_le_eq_lemma1[local] :
4139 !(r :real). 0 <= r ==> r / (1 + r) = 1 - inv (1 + r)
4140Proof
4141 rpt STRIP_TAC
4142 >> ‘1 + r <> 0’ by REAL_ASM_ARITH_TAC
4143 >> ‘1 - inv (1 + r) = (1 + r) / (1 + r) - inv (1 + r)’ by simp [REAL_DIV_REFL]
4144 >> POP_ORW
4145 >> REWRITE_TAC [REAL_INV_1OVER]
4146 >> simp [REAL_DIV_SUB]
4147 >> REAL_ARITH_TAC
4148QED
4149
4150Theorem contract_le_eq_lemma2[local] :
4151 !(r :real). r < 0 ==> r / (1 - r) = inv (1 - r) - 1
4152Proof
4153 rpt STRIP_TAC
4154 >> ‘1 - r <> 0’ by REAL_ASM_ARITH_TAC
4155 >> ‘inv (1 - r) - 1 = inv (1 - r) - (1 - r) / (1 - r)’ by simp [REAL_DIV_REFL]
4156 >> POP_ORW
4157 >> REWRITE_TAC [REAL_INV_1OVER]
4158 >> simp [REAL_DIV_SUB]
4159 >> REAL_ARITH_TAC
4160QED
4161
4162Theorem contract_le_eq :
4163 !x y. contract x <= contract y <=> x <= y
4164Proof
4165 rpt GEN_TAC
4166 >> Cases_on ‘x’ >> Cases_on ‘y’
4167 >> simp [contract_def, le_infty, REAL_NOT_LE]
4168 >> simp [contract_lemma, REAL_LT_IMP_LE, extreal_le_eq]
4169 >> Cases_on ‘0 <= r’
4170 >- (‘abs r = r’ by simp [ABS_REFL] >> POP_ORW >> simp [] \\
4171 reverse (Cases_on ‘0 <= r'’)
4172 >- (fs [REAL_NOT_LE] \\
4173 ‘~(r <= r')’ by REAL_ASM_ARITH_TAC >> POP_ORW \\
4174 simp [REAL_NOT_LE] \\
4175 Q_TAC (TRANS_TAC REAL_LTE_TRANS) ‘0’ \\
4176 reverse CONJ_TAC
4177 >- (MATCH_MP_TAC REAL_LE_DIV >> simp [] \\
4178 REAL_ASM_ARITH_TAC) \\
4179 ‘0 <= abs r'’ by simp [ABS_POS] \\
4180 ‘0 < 1 + abs r'’ by REAL_ASM_ARITH_TAC \\
4181 MP_TAC (Q.SPECL [‘r'’, ‘0’, ‘1 + abs r'’] REAL_LT_LDIV_EQ) \\
4182 simp []) \\
4183 ‘abs r' = r'’ by simp [ABS_REFL] >> POP_ORW \\
4184 simp [contract_le_eq_lemma1] \\
4185 simp [REAL_ARITH “1 - a <= 1 - b <=> b <= (a :real)”] \\
4186 Know ‘inv (1 + r') <= inv (1 + r) <=> 1 + r <= 1 + r'’
4187 >- (MATCH_MP_TAC REAL_INV_LE_ANTIMONO \\
4188 REAL_ASM_ARITH_TAC) >> Rewr' \\
4189 REAL_ARITH_TAC)
4190 >> fs [REAL_NOT_LE]
4191 >> ‘abs r = -r’ by simp [ABS_EQ_NEG] >> POP_ORW
4192 >> Cases_on ‘0 <= r'’
4193 >- (‘abs r' = r'’ by simp [ABS_REFL] >> POP_ORW \\
4194 ‘r <= r'’ by REAL_ASM_ARITH_TAC >> POP_ORW \\
4195 simp [GSYM real_sub] \\
4196 Suff ‘r / (1 - r) < 0 /\ 0 <= r' / (1 + r')’ >- REAL_ARITH_TAC \\
4197 reverse CONJ_TAC
4198 >- (MATCH_MP_TAC REAL_LE_DIV >> art [] \\
4199 REAL_ASM_ARITH_TAC) \\
4200 ‘0 < 1 - r’ by REAL_ASM_ARITH_TAC \\
4201 ‘1 - r <> 0’ by PROVE_TAC [REAL_LT_IMP_NE] \\
4202 MP_TAC (Q.SPECL [‘r’, ‘0’, ‘1 - r’] REAL_LT_LDIV_EQ) >> simp [])
4203 >> fs [REAL_NOT_LE]
4204 >> ‘abs r' = -r'’ by simp [ABS_EQ_NEG] >> POP_ORW
4205 >> simp [GSYM real_sub]
4206 >> simp [contract_le_eq_lemma2]
4207 >> simp [REAL_ARITH “a - 1 <= b - 1 <=> a <= (b :real)”]
4208 >> Know ‘inv (1 - r) <= inv (1 - r') <=> 1 - r' <= 1 - r’
4209 >- (MATCH_MP_TAC REAL_INV_LE_ANTIMONO \\
4210 REAL_ASM_ARITH_TAC)
4211 >> Rewr'
4212 >> REAL_ARITH_TAC
4213QED
4214
4215Theorem contract_11 :
4216 !x y. contract x = contract y <=> x = y
4217Proof
4218 METIS_TAC [le_antisym, contract_le_eq]
4219QED
4220
4221Theorem contract_neg :
4222 !x. contract (-x) = -contract x
4223Proof
4224 Q.X_GEN_TAC ‘x’
4225 >> Cases_on ‘x’ >> simp [contract_def, extreal_ainv_def]
4226QED
4227
4228Definition expand_def :
4229 expand c = if 1 <= c then PosInf
4230 else if c <= -1 then NegInf
4231 else Normal (c / (1 - abs c))
4232End
4233
4234Theorem expand_contract :
4235 !x. expand (contract x) = x
4236Proof
4237 Q.X_GEN_TAC ‘x’
4238 >> Cases_on ‘x’ >> simp [contract_def, expand_def]
4239 >> Cases_on ‘r = 0’ >- simp []
4240 >> ‘0 < r \/ r < 0’ by PROVE_TAC [REAL_LT_TOTAL]
4241 >| [ (* goal 1 (of 2) *)
4242 ‘0 <= r’ by simp [REAL_LT_IMP_LE] \\
4243 ‘abs r = r’ by simp [ABS_REFL] >> POP_ORW \\
4244 ‘0 < 1 + r’ by REAL_ASM_ARITH_TAC \\
4245 ‘0 < r / (1 + r)’ by simp [REAL_LT_DIV] \\
4246 Know ‘r / (1 + r) < 1’
4247 >- (MP_TAC (Q.SPECL [‘r’, ‘1’, ‘1 + r’] REAL_LT_LDIV_EQ) >> simp []) \\
4248 DISCH_TAC \\
4249 ‘~(1 <= r / (1 + r))’ by REAL_ASM_ARITH_TAC \\
4250 ‘~(r / (1 + r) <= -1)’ by REAL_ASM_ARITH_TAC \\
4251 ASM_SIMP_TAC real_ss [extreal_11] \\
4252 qabbrev_tac ‘z = r / (1 + r)’ \\
4253 ‘0 <= z’ by simp [REAL_LT_IMP_LE] \\
4254 ‘abs z = z’ by simp [ABS_REFL] >> POP_ORW \\
4255 ‘1 + r <> 0’ by simp [REAL_LT_IMP_NE] \\
4256 Know ‘(1 + r) / (1 + r) - z = 1 / (1 + r)’
4257 >- (qunabbrev_tac ‘z’ \\
4258 simp [REAL_DIV_SUB, REAL_ADD_SUB_ALT]) \\
4259 ASM_SIMP_TAC std_ss [REAL_DIV_REFL] \\
4260 DISCH_THEN K_TAC \\
4261 simp [div_ratr, Abbr ‘z’],
4262 (* goal 2 (of 2) *)
4263 ‘r <= 0’ by simp [REAL_LT_IMP_LE] \\
4264 ‘abs r = -r’ by simp [ABS_EQ_NEG] >> POP_ORW \\
4265 simp [GSYM real_sub] \\
4266 ‘0 < 1 - r’ by REAL_ASM_ARITH_TAC \\
4267 Know ‘r / (1 - r) < 0’
4268 >- (MP_TAC (Q.SPECL [‘r’, ‘0’, ‘1 - r’] REAL_LT_LDIV_EQ) >> simp []) \\
4269 DISCH_TAC \\
4270 ‘1 - r <> 0’ by PROVE_TAC [REAL_LT_IMP_NE] \\
4271 Know ‘-1 < r / (1 - r)’
4272 >- (MP_TAC (Q.SPECL [‘-1’, ‘r’, ‘1 - r’] REAL_LT_RDIV_EQ) >> simp [] \\
4273 REAL_ARITH_TAC) >> DISCH_TAC \\
4274 ‘~(1 <= r / (1 - r))’ by REAL_ASM_ARITH_TAC \\
4275 ‘~(r / (1 - r) <= -1)’ by REAL_ASM_ARITH_TAC \\
4276 ASM_SIMP_TAC real_ss [extreal_11] \\
4277 qabbrev_tac ‘z = r / (1 - r)’ \\
4278 ‘z <= 0’ by PROVE_TAC [REAL_LT_IMP_LE] \\
4279 ‘abs z = -z’ by simp [ABS_EQ_NEG] >> POP_ORW \\
4280 simp [REAL_SUB_RNEG] \\
4281 Know ‘(1 - r) / (1 - r) + z = 1 / (1 - r)’
4282 >- (qunabbrev_tac ‘z’ \\
4283 simp [REAL_DIV_ADD, REAL_SUB_ADD]) \\
4284 ASM_SIMP_TAC std_ss [REAL_DIV_REFL] \\
4285 DISCH_THEN K_TAC \\
4286 simp [div_ratr, Abbr ‘z’] ]
4287QED