realaxScript.sml
1(*===========================================================================*)
2(* Construct reals from positive reals *)
3(*===========================================================================*)
4Theory realax
5Ancestors
6 pair arithmetic num normalizer prim_rec hreal
7Libs
8 numLib reduceLib pairLib jrhUtils mesonLib tautLib
9 realPP[qualified]
10
11
12val _ = ParseExtras.temp_loose_equality()
13
14val TAUT_CONV = jrhUtils.TAUT_CONV; (* conflict with tautLib.TAUT_CONV *)
15val TAUT = tautLib.TAUT_CONV; (* conflict with tautLib.TAUT *)
16val GEN_ALL = hol88Lib.GEN_ALL; (* it has old reverted variable order *)
17
18(*---------------------------------------------------------------------------*)
19(* Now define the functions over the equivalence classes *)
20(*---------------------------------------------------------------------------*)
21
22val [REAL_10, REAL_ADD_SYM, REAL_MUL_SYM, REAL_ADD_ASSOC,
23 REAL_MUL_ASSOC, REAL_LDISTRIB, REAL_ADD_LID, REAL_MUL_LID,
24 REAL_ADD_LINV, REAL_MUL_LINV, REAL_LT_TOTAL, REAL_LT_REFL,
25 REAL_LT_TRANS, REAL_LT_IADD, REAL_LT_MUL, REAL_BIJ, REAL_ISO,
26 REAL_INV_0] =
27 let fun mk_def (d,t,n,f) = {def_name=d, fixity=f, fname=n, func=t}
28 in
29 quotient.define_equivalence_type
30 {name = "real",
31 equiv = TREAL_EQ_EQUIV,
32 defs = [mk_def("real_0", “treal_0”, "real_0", NONE),
33 mk_def("real_1", “treal_1”, "real_1", NONE),
34 mk_def("real_neg", “treal_neg”, "real_neg", NONE),
35 mk_def("real_inv", “treal_inv”, "inv", NONE),
36 mk_def("real_add", “$treal_add”, "real_add", SOME(Infixl 500)),
37 mk_def("real_mul", “$treal_mul”, "real_mul", SOME(Infixl 600)),
38 mk_def("real_lt", “$treal_lt”, "real_lt", NONE),
39 mk_def("real_of_hreal", “$treal_of_hreal”, "real_of_hreal", NONE),
40 mk_def("hreal_of_real", “$hreal_of_treal”, "hreal_of_real", NONE)],
41 welldefs = [TREAL_NEG_WELLDEF, TREAL_INV_WELLDEF, TREAL_LT_WELLDEF,
42 TREAL_ADD_WELLDEF, TREAL_MUL_WELLDEF, TREAL_BIJ_WELLDEF],
43 old_thms = ([TREAL_10]
44 @ (map (GEN_ALL o MATCH_MP TREAL_EQ_AP o SPEC_ALL)
45 [TREAL_ADD_SYM, TREAL_MUL_SYM, TREAL_ADD_ASSOC,
46 TREAL_MUL_ASSOC, TREAL_LDISTRIB])
47 @ [TREAL_ADD_LID, TREAL_MUL_LID, TREAL_ADD_LINV,
48 TREAL_MUL_LINV, TREAL_LT_TOTAL, TREAL_LT_REFL,
49 TREAL_LT_TRANS, TREAL_LT_ADD, TREAL_LT_MUL, TREAL_BIJ,
50 TREAL_ISO, TREAL_INV_0])}
51 end;
52
53(* Export all 18 primitive theorems in total, without any changes (yet) *)
54Theorem REAL_10 = REAL_10;
55Theorem REAL_ADD_SYM = REAL_ADD_SYM;
56Theorem REAL_MUL_SYM = REAL_MUL_SYM;
57Theorem REAL_ADD_ASSOC = REAL_ADD_ASSOC;
58Theorem REAL_MUL_ASSOC = REAL_MUL_ASSOC;
59Theorem REAL_LDISTRIB = REAL_LDISTRIB;
60Theorem REAL_ADD_LID = REAL_ADD_LID;
61Theorem REAL_MUL_LID = REAL_MUL_LID;
62Theorem REAL_ADD_LINV = REAL_ADD_LINV;
63Theorem REAL_MUL_LINV = REAL_MUL_LINV;
64Theorem REAL_LT_TOTAL = REAL_LT_TOTAL;
65Theorem REAL_LT_REFL = REAL_LT_REFL;
66Theorem REAL_LT_TRANS = REAL_LT_TRANS;
67Theorem REAL_LT_IADD = REAL_LT_IADD;
68Theorem REAL_LT_MUL = REAL_LT_MUL;
69Theorem REAL_BIJ = REAL_BIJ;
70Theorem REAL_ISO = REAL_ISO;
71Theorem REAL_INV_0 = REAL_INV_0;
72
73(*---------------------------------------------------------------------------
74 Overload arithmetic operations.
75 ---------------------------------------------------------------------------*)
76
77val _ =
78 add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
79 fixity = Suffix 2100,
80 paren_style = ParoundPrec,
81 pp_elements = [TOK (UnicodeChars.sup_minus ^ UnicodeChars.sup_1)],
82 term_name = "realinv"};
83
84Overload realinv = “inv”
85
86val _ = TeX_notation {hol = "realinv", TeX = ("\\HOLTokenInverse{}", 1)};
87val _ = TeX_notation {hol = (UnicodeChars.sup_minus ^ UnicodeChars.sup_1),
88 TeX = ("\\HOLTokenInverse{}", 1)};
89
90val natplus = Term`$+`;
91val natless = Term`$<`;
92val bool_not = “$~ : bool -> bool”
93val natmult = Term`$*`;
94
95Overload "+" = natplus
96Overload "*" = natmult
97Overload "<" = natless
98
99Overload "~" = “$real_neg”
100Overload "~" = bool_not
101Overload "¬" = bool_not
102Overload "numeric_negate" = “$real_neg”
103
104Overload "+" = Term`$real_add`
105Overload "*" = Term`$real_mul`
106Overload "<" = Term`real_lt`
107
108(*---------------------------------------------------------------------------*)
109(* Transfer of supremum property for all-positive sets - bit painful *)
110(*---------------------------------------------------------------------------*)
111
112Theorem REAL_ISO_EQ:
113 !h i. h hreal_lt i = real_of_hreal h < real_of_hreal i
114Proof
115 REPEAT GEN_TAC THEN EQ_TAC THENL
116 [MATCH_ACCEPT_TAC REAL_ISO,
117 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
118 (SPECL [“h:hreal”, “i:hreal”] HREAL_LT_TOTAL) THEN
119 ASM_REWRITE_TAC[REAL_LT_REFL] THEN
120 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ (MATCH_MP REAL_ISO th))) THEN
121 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_TRANS) THEN
122 REWRITE_TAC[REAL_LT_REFL]]
123QED
124
125(* cf. the other REAL_POS exported below *)
126Theorem REAL_POS[local]:
127 !X. real_0 < real_of_hreal X
128Proof
129 GEN_TAC THEN REWRITE_TAC[REAL_BIJ]
130QED
131
132Theorem SUP_ALLPOS_LEMMA1[local]: (* no need to export *)
133 !P y. (!x. P x ==> real_0 < x) ==>
134 ((?x. P x /\ y < x) =
135 (?X. P(real_of_hreal X) /\ y < (real_of_hreal X)))
136Proof
137 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL
138 [DISCH_THEN(X_CHOOSE_THEN “x:real” (fn th => MP_TAC th THEN POP_ASSUM
139 (SUBST1_TAC o SYM o REWRITE_RULE[REAL_BIJ] o C MATCH_MP (CONJUNCT1 th))))
140 THEN DISCH_TAC THEN EXISTS_TAC “hreal_of_real x” THEN ASM_REWRITE_TAC[],
141 DISCH_THEN(X_CHOOSE_THEN “X:hreal” ASSUME_TAC) THEN
142 EXISTS_TAC “real_of_hreal X” THEN ASM_REWRITE_TAC[]]
143QED
144
145Theorem SUP_ALLPOS_LEMMA2[local]: (* no need to export *)
146 !P X. P(real_of_hreal X) :bool = (\h. P(real_of_hreal h)) X
147Proof
148 REPEAT GEN_TAC THEN BETA_TAC THEN REFL_TAC
149QED
150
151Theorem SUP_ALLPOS_LEMMA3[local]: (* no need to export *)
152 !P. (!x. P x ==> real_0 < x) /\
153 (?x. P x) /\
154 (?z. !x. P x ==> x < z)
155 ==> (?X. (\h. P(real_of_hreal h)) X) /\
156 (?Y. !X. (\h. P(real_of_hreal h)) X ==> X hreal_lt Y)
157Proof
158 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC STRIP_ASSUME_TAC) THEN
159 CONJ_TAC THENL
160 [EXISTS_TAC “hreal_of_real x” THEN BETA_TAC THEN
161 FIRST_ASSUM(SUBST1_TAC o REWRITE_RULE[REAL_BIJ] o
162 C MATCH_MP (ASSUME “(P:real->bool) x”)) THEN
163 FIRST_ASSUM ACCEPT_TAC,
164 EXISTS_TAC “hreal_of_real z” THEN BETA_TAC THEN GEN_TAC THEN
165 UNDISCH_TAC “(P:real->bool) x” THEN DISCH_THEN(K ALL_TAC) THEN
166 DISCH_THEN(fn th => EVERY_ASSUM(MP_TAC o C MATCH_MP th)) THEN
167 POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT DISCH_TAC THEN
168 REWRITE_TAC[REAL_ISO_EQ] THEN
169 MP_TAC(SPECL[“real_0”, “real_of_hreal X”, “z:real”] REAL_LT_TRANS) THEN
170 ASM_REWRITE_TAC[REAL_BIJ] THEN
171 DISCH_THEN SUBST_ALL_TAC THEN FIRST_ASSUM ACCEPT_TAC]
172QED
173
174Theorem SUP_ALLPOS_LEMMA4[local]: (* no need to export *)
175 !y. ~(real_0 < y) ==> !x. y < (real_of_hreal x)
176Proof
177 GEN_TAC THEN DISCH_THEN(curry op THEN GEN_TAC o MP_TAC) THEN
178 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
179 (SPECL [“y:real”, “real_0”] REAL_LT_TOTAL) THEN
180 ASM_REWRITE_TAC[REAL_POS] THEN DISCH_THEN(K ALL_TAC) THEN
181 POP_ASSUM(MP_TAC o C CONJ (SPEC “x:hreal” REAL_POS)) THEN
182 DISCH_THEN(ACCEPT_TAC o MATCH_MP REAL_LT_TRANS)
183QED
184
185Theorem REAL_SUP_ALLPOS:
186 !P. (!x. P x ==> real_0 < x) /\ (?x. P x) /\ (?z. !x. P x ==> x < z)
187 ==> (?s. !y. (?x. P x /\ y < x) = y < s)
188Proof
189 let val lemma = TAUT_CONV “a /\ b ==> (a = b)” in
190 GEN_TAC THEN DISCH_TAC THEN
191 EXISTS_TAC “real_of_hreal(hreal_sup(\h. P(real_of_hreal h)))” THEN
192 GEN_TAC THEN
193 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP SUP_ALLPOS_LEMMA1(CONJUNCT1 th)]) THEN
194 ASM_CASES_TAC “real_0 < y” THENL
195 [FIRST_ASSUM(SUBST1_TAC o SYM o REWRITE_RULE[REAL_BIJ]) THEN
196 REWRITE_TAC[GSYM REAL_ISO_EQ] THEN
197 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV)
198 [SUP_ALLPOS_LEMMA2] THEN
199 FIRST_ASSUM(ASSUME_TAC o MATCH_MP HREAL_SUP o MATCH_MP SUP_ALLPOS_LEMMA3)
200 THEN ASM_REWRITE_TAC[],
201 MATCH_MP_TAC lemma THEN CONJ_TAC THENL
202 [FIRST_ASSUM(MP_TAC o MATCH_MP SUP_ALLPOS_LEMMA3) THEN
203 BETA_TAC THEN DISCH_THEN(X_CHOOSE_TAC “X:hreal” o CONJUNCT1) THEN
204 EXISTS_TAC “X:hreal” THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
205 FIRST_ASSUM(MATCH_ACCEPT_TAC o MATCH_MP SUP_ALLPOS_LEMMA4)] end
206QED
207
208(*---------------------------------------------------------------------------*)
209(* Now define the inclusion homomorphism &:num->real. (was in realTheory) *)
210(*---------------------------------------------------------------------------*)
211
212Definition real_of_num[nocompute]:
213 (real_of_num 0 = real_0) /\
214 (real_of_num(SUC n) = real_of_num n + real_1)
215End
216
217val _ = add_numeral_form(#"r", SOME "real_of_num");
218
219Theorem REAL_0:
220 real_0 = &0
221Proof
222 REWRITE_TAC[real_of_num]
223QED
224
225Theorem REAL_1:
226 real_1 = &1
227Proof
228 REWRITE_TAC[num_CONV “1:num”, real_of_num, REAL_ADD_LID]
229QED
230
231(* NOTE: Only theorems involving ‘real_0’ and ‘real_1’ need to be re-educated.
232 A "prime" is added into some exported names to make sure that the original
233 theorems are still accessible.
234 *)
235local val reeducate = REWRITE_RULE[REAL_0, REAL_1] in
236Theorem REAL_10' = reeducate(REAL_10)
237Theorem REAL_ADD_LID' = reeducate(REAL_ADD_LID)
238Theorem REAL_ADD_LINV' = reeducate(REAL_ADD_LINV)
239Theorem REAL_INV_0' = reeducate(REAL_INV_0)
240Theorem REAL_LT_MUL' = reeducate(REAL_LT_MUL)
241Theorem REAL_MUL_LID' = reeducate(REAL_MUL_LID)
242Theorem REAL_MUL_LINV' = reeducate(REAL_MUL_LINV)
243Theorem REAL_SUP_ALLPOS' = reeducate(REAL_SUP_ALLPOS);
244end;
245
246(*---------------------------------------------------------------------------*)
247(* Define subtraction, division and the other orderings (was in realTheory) *)
248(*---------------------------------------------------------------------------*)
249
250Definition real_sub[nocompute]: real_sub x y = x + ~y
251End
252Definition real_lte[nocompute]: real_lte x y = ~(y < x)
253End
254Definition real_gt[nocompute]: real_gt x y = y < x
255End
256Definition real_ge[nocompute]: real_ge x y = (real_lte y x)
257End
258
259Definition real_div[nocompute]: $/ x y = x * inv y
260End
261val _ = set_fixity "/" (Infixl 600);
262val _ = overload_on(GrammarSpecials.decimal_fraction_special, “$/”);
263Overload "/" = “$/”
264
265val _ = add_ML_dependency "realPP"
266val _ = add_user_printer ("real.decimalfractions",
267 “&(NUMERAL x) : real / &(NUMERAL y)”);
268
269Overload "-" = “$-”(* natsub *)
270Overload "<=" = “$<=”(* natlte *)
271Overload ">" = “$>”(* natgt *)
272Overload ">=" = “$>=”(* natge *)
273
274Overload "-" = “$real_sub”
275Overload "<=" = “$real_lte”
276Overload ">" = “$real_gt”
277Overload ">=" = “$real_ge”
278
279Definition real_abs[nocompute]: abs(x) = (if (0 <= x) then x else ~x)
280End
281
282Definition real_pow[nocompute]:
283 ($pow x 0 = &1) /\ ($pow x (SUC n) = x * ($pow x n))
284End
285val _ = set_fixity "pow" (Infixr 700);
286
287Definition real_max[nocompute]: max (x :real) y = if x <= y then y else x
288End
289
290Definition real_min[nocompute]: min (x :real) y = if x <= y then x else y
291End
292
293(* |- !y x. x < y <=> ~(y <= x) *)
294Theorem real_lt[allow_rebind]:
295 !y x. x < y <=> ~(y <= x)
296Proof
297 let
298 val th1 = TAUT_PROVE (“!t u:bool. (t = ~u) ==> (u = ~t)”)
299 val th2 = SPECL [``y <= x``,``x < y``] th1
300 val th3 = SPECL [``y:real``,``x:real``] real_lte
301 in
302 ACCEPT_TAC (GENL [``y:real``, ``x:real``] (MP th2 th3))
303 end
304QED
305
306(* Floor and ceiling (nums) *)
307Definition NUM_FLOOR_def[nocompute] :
308 NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x
309End
310
311Definition NUM_CEILING_def[nocompute] :
312 NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n
313End
314
315Overload flr = “NUM_FLOOR”
316Overload clg = “NUM_CEILING”
317
318(* ------------------------------------------------------------------------- *)
319(* Some elementary "bootstrapping" lemmas needed by RealArith.sml *)
320(* *)
321(* NOTE: The following theorems were from HOL-Light's calc_int.sml, line 66 *)
322(* afterwards. The precise order of theorems are preserved, which is a bit *)
323(* different with their orders when they were also in realTheory. Thus, as *)
324(* a result, some of their proofs are directly ported from HOL-Light, which *)
325(* uses a lot of MESON_TAC instead of manual proof steps. -- Chun Tian *)
326(* *)
327(* NOTE2: any updates here must be also put in "prove_real_assumsScript.sml" *)
328(* ------------------------------------------------------------------------- *)
329
330(* HOL-Light compatible (Don't add quantifiers!), was in iterateTheory
331
332 NOTE: This theorem is not very useful in HOL4, because whenever in proofs
333 from HOL-Light one has something like this:
334
335 AC REAL_ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`
336
337 In HOL4, we must change it to the following code instead:
338
339 jrhUtils.AC (REAL_ADD_ASSOC,REAL_ADD_SYM)
340 “(a + b) + (c + d) = (a + c) + (b + d):real”
341
342 NOTE2: in the follow scripts (until the end of this file), all terms “&n”
343 must be written as “real_of_num n”, while literals “&0” and “&1”
344 must be written as “0r” and “1r”. This is because these code has
345 a copy in "prove_real_assumsScript.sml" where “real_of_num” is
346 interpreted differently.
347 *)
348Theorem REAL_ADD_AC :
349 (m + n = n + m) /\
350 ((m + n) + p = m + (n + p)) /\
351 (m + (n + p) = n + (m + p))
352Proof
353 MESON_TAC[REAL_ADD_ASSOC, REAL_ADD_SYM]
354QED
355
356Theorem REAL_MUL_AC :
357 (m * n = n * m) /\
358 ((m * n) * p = m * (n * p)) /\
359 (m * (n * p) = n * (m * p))
360Proof
361 MESON_TAC[REAL_MUL_ASSOC, REAL_MUL_SYM]
362QED
363
364Theorem REAL_ADD_RINV:
365 !x:real. x + ~x = 0r
366Proof
367 MESON_TAC[REAL_ADD_SYM, REAL_ADD_LINV']
368QED
369
370(* HOL-Light compatible *)
371Theorem REAL_EQ_ADD_LCANCEL:
372 !x y z. (x + y = x + z) <=> (y = z)
373Proof
374 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
375 POP_ASSUM(MP_TAC o AP_TERM “$+ ~x”) THEN
376 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV', REAL_ADD_LID']
377QED
378
379(* HOL-Light compatible *)
380Theorem REAL_EQ_ADD_RCANCEL:
381 !x y z. (x + z = y + z) <=> (x = y)
382Proof
383 MESON_TAC[REAL_ADD_SYM, REAL_EQ_ADD_LCANCEL]
384QED
385
386(* HOL-Light compatible name
387 |- !x y z. x * (y + z) = x * y + x * z
388 *)
389Theorem REAL_ADD_LDISTRIB = REAL_LDISTRIB
390
391Theorem REAL_RDISTRIB:
392 !x y z. (x + y) * z = (x * z) + (y * z)
393Proof
394 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
395 MATCH_ACCEPT_TAC REAL_LDISTRIB
396QED
397
398(* HOL-Light compatible name of the above theorem *)
399Theorem REAL_ADD_RDISTRIB = REAL_RDISTRIB
400
401Theorem REAL_MUL_RZERO:
402 !x. x * 0r = 0r
403Proof
404 MESON_TAC[REAL_EQ_ADD_RCANCEL, REAL_ADD_LDISTRIB, REAL_ADD_LID']
405QED
406
407Theorem REAL_MUL_LZERO:
408 !x. 0r * x = 0r
409Proof
410 MESON_TAC[REAL_MUL_SYM, REAL_MUL_RZERO]
411QED
412
413Theorem REAL_NEG_NEG:
414 !x:real. ~~x = x
415Proof
416 MESON_TAC
417 [REAL_EQ_ADD_RCANCEL, REAL_ADD_LINV', REAL_ADD_SYM, REAL_ADD_LINV']
418QED
419
420Theorem REAL_MUL_RNEG:
421 !x y. x * ~y = ~(x * y)
422Proof
423 MESON_TAC[REAL_EQ_ADD_RCANCEL, REAL_ADD_LDISTRIB, REAL_ADD_LINV',
424 REAL_MUL_RZERO]
425QED
426
427Theorem REAL_MUL_LNEG:
428 !x y. ~x * y = ~(x * y)
429Proof
430 MESON_TAC[REAL_MUL_SYM, REAL_MUL_RNEG]
431QED
432
433Theorem REAL_NEG_ADD:
434 !x y. ~(x + y) = ~x + ~y
435Proof
436 REPEAT GEN_TAC THEN
437 MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL REAL_EQ_ADD_RCANCEL)))) THEN
438 Q.EXISTS_TAC `x + y` THEN REWRITE_TAC[REAL_ADD_LINV'] THEN
439 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
440 “(a + b) + (c + d) = (a + c) + (b + d):real”] THEN
441 REWRITE_TAC[REAL_ADD_LINV', REAL_ADD_LID']
442QED
443
444Theorem REAL_ADD_RID:
445 !x. x + 0r = x
446Proof MESON_TAC[REAL_ADD_SYM, REAL_ADD_LID']
447QED
448
449Theorem REAL_NEG_0:
450 ~0r = 0r
451Proof MESON_TAC[REAL_ADD_LINV', REAL_ADD_RID]
452QED
453
454(* NOTE: REAL_LE_LADD_IMP (and many others below) is primative in HOL Light, i.e.
455 directly come from the quotient process, but in HOL4 it must be derived from
456 other primitives.
457 *)
458Theorem REAL_LT_LADD:
459 !x y z. (x + y) < (x + z) <=> y < z
460Proof
461 REPEAT GEN_TAC THEN EQ_TAC THENL
462 [DISCH_THEN(MP_TAC o Q.SPEC ‘~x’ o MATCH_MP REAL_LT_IADD) THEN
463 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV', REAL_ADD_LID'],
464 MATCH_ACCEPT_TAC REAL_LT_IADD]
465QED
466
467(* HOL-Light compatible name *)
468Theorem REAL_LT_LADD_IMP = REAL_LT_IADD
469
470Theorem REAL_LE_LADD:
471 !x y z. (x + y) <= (x + z) <=> y <= z
472Proof
473 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN
474 AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_LT_LADD
475QED
476
477(* |- !x y z. y <= z ==> x + y <= x + z *)
478Theorem REAL_LE_LADD_IMP = (
479 let
480 val th1 = GSYM (SPEC_ALL REAL_LE_LADD)
481 val th2 = TAUT_PROVE ``(x:bool = y) ==> (x ==> y)``
482 in
483 Q.GENL [‘x’, ‘y’, ‘z’] (MATCH_MP th2 th1)
484 end)
485
486Theorem REAL_LE_LNEG:
487 !x y. ~x <= y <=> 0r <= x + y
488Proof
489 REPEAT GEN_TAC THEN EQ_TAC THEN
490 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THENL
491 [DISCH_THEN(MP_TAC o Q.SPEC `x:real`) THEN
492 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV'],
493 DISCH_THEN(MP_TAC o Q.SPEC `~x`) THEN
494 REWRITE_TAC[REAL_ADD_LINV', REAL_ADD_ASSOC, REAL_ADD_LID',
495 ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID']]
496QED
497
498Theorem REAL_LE_NEG2:
499 !x y. ~x <= ~y <=> y <= x
500Proof
501 REPEAT GEN_TAC THEN
502 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) empty_rewrites [GSYM REAL_NEG_NEG] THEN
503 REWRITE_TAC[REAL_LE_LNEG] THEN
504 AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_ADD_SYM
505QED
506
507Theorem REAL_LE_RNEG:
508 !x y. x <= ~y <=> x + y <= 0r
509Proof
510 REPEAT GEN_TAC THEN
511 GEN_REWR_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_NEG_NEG] THEN
512 REWRITE_TAC[REAL_LE_LNEG, GSYM REAL_NEG_ADD] THEN
513 GEN_REWR_TAC RAND_CONV [GSYM REAL_LE_NEG2] THEN
514 AP_THM_TAC THEN AP_TERM_TAC THEN
515 REWRITE_TAC[GSYM REAL_ADD_LINV'] THEN
516 REWRITE_TAC[REAL_NEG_ADD, REAL_NEG_NEG] THEN
517 MATCH_ACCEPT_TAC REAL_ADD_SYM
518QED
519
520Theorem REAL:
521 !n. real_of_num (SUC n) = real_of_num n + 1r
522Proof
523 GEN_TAC THEN REWRITE_TAC[real_of_num] THEN
524 REWRITE_TAC[REAL_1]
525QED
526
527Theorem REAL_ADD:
528 !m n. real_of_num m + real_of_num n = real_of_num(m + n)
529Proof
530 INDUCT_TAC THEN REWRITE_TAC[REAL, ADD, REAL_ADD_LID'] THEN
531 RULE_ASSUM_TAC GSYM THEN GEN_TAC THEN ASM_REWRITE_TAC[] THEN
532 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))
533QED
534
535(* HOL-Light compatible name of the above theorem *)
536Theorem REAL_OF_NUM_ADD = REAL_ADD;
537
538Theorem REAL_OF_NUM_SUB:
539 !m n. m <= n ==> (&(n-m):real = &n - &m)
540Proof
541 rw[] >> ‘?d. n=m+d’ by (irule LESS_EQUAL_ADD >> simp[])
542 >> simp[SUB_RIGHT_EQ]
543 >> once_rewrite_tac[GSYM REAL_ADD]
544 >> simp[REAL_ADD_RINV, bossLib.AC REAL_ADD_ASSOC REAL_ADD_SYM,
545 real_sub, REAL_ADD_LID']
546QED
547
548Theorem REAL_MUL:
549 !m n. real_of_num m * real_of_num n = real_of_num(m * n)
550Proof
551 INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO, MULT_CLAUSES, REAL,
552 GSYM REAL_ADD, REAL_RDISTRIB] THEN
553 FIRST_ASSUM(fn th => REWRITE_TAC[GSYM th]) THEN
554 REWRITE_TAC[REAL_MUL_LID']
555QED
556
557(* HOL-Light compatible name of the above theorem *)
558Theorem REAL_OF_NUM_MUL = REAL_MUL;
559
560Theorem REAL_OF_NUM_POW :
561 !x n. (real_of_num x) pow n = real_of_num(x EXP n)
562Proof
563 GEN_TAC THEN INDUCT_TAC THEN
564 ASM_REWRITE_TAC[real_pow, EXP, REAL_OF_NUM_MUL]
565QED
566
567(* NOTE: realTheory.REAL_POW_NEG has different statements! *)
568Theorem REAL_POW_NEG :
569 !x n. (~x) pow n = if EVEN n then x pow n else ~(x pow n)
570Proof
571 GEN_TAC THEN INDUCT_TAC THEN
572 ASM_REWRITE_TAC[real_pow, EVEN] THEN
573 ASM_CASES_TAC “EVEN n” THEN
574 ASM_REWRITE_TAC[REAL_MUL_RNEG, REAL_MUL_LNEG, REAL_NEG_NEG]
575QED
576
577Theorem REAL_NOT_LE:
578 !x y. ~(x <= y) <=> y < x
579Proof
580 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte]
581QED
582
583Theorem REAL_LT_ADDR:
584 !x y. x < x + y <=> 0r < y
585Proof
586 REPEAT GEN_TAC THEN
587 SUBST1_TAC(SYM(SPECL [“x:real”, “0r”, “y:real”] REAL_LT_LADD)) THEN
588 REWRITE_TAC[REAL_ADD_RID]
589QED
590
591Theorem REAL_LT_ANTISYM:
592 !x y. ~(x < y /\ y < x)
593Proof
594 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_TRANS) THEN
595 REWRITE_TAC[REAL_LT_REFL]
596QED
597
598Theorem REAL_LT_GT:
599 !x y. x < y ==> ~(y < x)
600Proof
601 REPEAT GEN_TAC THEN
602 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
603 REWRITE_TAC[REAL_LT_ANTISYM]
604QED
605
606Theorem REAL_LE_LT:
607 !x y. x <= y <=> x < y \/ (x = y)
608Proof
609 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN EQ_TAC THENL
610 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
611 (SPECL [“x:real”, “y:real”] REAL_LT_TOTAL) THEN ASM_REWRITE_TAC[],
612 DISCH_THEN(DISJ_CASES_THEN2
613 (curry op THEN (MATCH_MP_TAC REAL_LT_GT) o ACCEPT_TAC) SUBST1_TAC) THEN
614 MATCH_ACCEPT_TAC REAL_LT_REFL]
615QED
616
617Theorem REAL_LT_LE:
618 !x y. x < y <=> x <= y /\ ~(x = y)
619Proof
620 let val lemma = TAUT_CONV “~(a /\ ~a)” in
621 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT, RIGHT_AND_OVER_OR, lemma]
622 THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
623 POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
624 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_REFL] end
625QED
626
627Theorem REAL_LT_IMP_LE:
628 !x y. x < y ==> x <= y
629Proof
630 REPEAT GEN_TAC THEN DISCH_TAC THEN
631 ASM_REWRITE_TAC[REAL_LE_LT]
632QED
633
634Theorem REAL_LET_TRANS:
635 !x y z. x <= y /\ y < z ==> x < z
636Proof
637 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT, RIGHT_AND_OVER_OR] THEN
638 DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP REAL_LT_TRANS)
639 (CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC))
640QED
641
642Theorem REAL_LE_TRANS:
643 !x y z. x <= y /\ y <= z ==> x <= z
644Proof
645 REPEAT GEN_TAC THEN
646 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_LE_LT] THEN
647 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (DISJ_CASES_THEN2 ASSUME_TAC SUBST1_TAC))
648 THEN REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o C CONJ (ASSUME “y < z”)) THEN
649 DISCH_THEN(ACCEPT_TAC o MATCH_MP REAL_LT_IMP_LE o MATCH_MP REAL_LET_TRANS)
650QED
651
652Theorem REAL_LE_MUL:
653 !x y. 0r <= x /\ 0r <= y ==> 0r <= (x * y)
654Proof
655 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN
656 MAP_EVERY ASM_CASES_TAC [“0r = x”, “0r = y”] THEN
657 ASM_REWRITE_TAC[] THEN TRY(FIRST_ASSUM(SUBST1_TAC o SYM)) THEN
658 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO] THEN
659 DISCH_TAC THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_MUL' THEN
660 ASM_REWRITE_TAC[]
661QED
662
663Theorem REAL_LT_RADD:
664 !x y z. (x + z) < (y + z) <=> x < y
665Proof
666 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
667 MATCH_ACCEPT_TAC REAL_LT_LADD
668QED
669
670Theorem REAL_LE_RADD:
671 !x y z. (x + z) <= (y + z) <=> x <= y
672Proof
673 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN
674 AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_LT_RADD
675QED
676
677Theorem REAL_NEG_LT0 :
678 !x. ~x < 0r <=> 0r < x
679Proof
680 GEN_TAC THEN
681 SUBST1_TAC(SYM(Q.SPECL [‘~x’, ‘0r’, ‘x’] REAL_LT_RADD))
682 THEN REWRITE_TAC[REAL_ADD_LINV', REAL_ADD_LID']
683QED
684
685Theorem REAL_LT_NEGTOTAL:
686 !x. (x = 0r) \/ 0r < x \/ 0r < -x
687Proof
688 GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
689 (Q.SPECL [‘x’, ‘0r’] REAL_LT_TOTAL) THEN
690 ASM_REWRITE_TAC[SYM(REWRITE_RULE[REAL_NEG_NEG] (Q.SPEC ‘~x’ REAL_NEG_LT0))]
691QED
692
693Theorem REAL_LE_NEGTOTAL :
694 !x. 0r <= x \/ 0r <= ~x
695Proof
696 GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN
697 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
698 (SPEC “x:real” REAL_LT_NEGTOTAL) THEN
699 ASM_REWRITE_TAC[]
700QED
701
702Theorem REAL_LNEG_UNIQ:
703 !x y. (x + y = 0r) <=> (x = ~y)
704Proof
705 REPEAT GEN_TAC THEN SUBST1_TAC (SYM(SPEC “y:real” REAL_ADD_LINV')) THEN
706 MATCH_ACCEPT_TAC REAL_EQ_ADD_RCANCEL
707QED
708
709Theorem REAL_RNEG_UNIQ:
710 !x y. (x + y = 0r) <=> (y = ~x)
711Proof
712 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
713 MATCH_ACCEPT_TAC REAL_LNEG_UNIQ
714QED
715
716Theorem REAL_NEG_LMUL:
717 !x y. ~(x * y) = ~x * y
718Proof
719 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
720 REWRITE_TAC[GSYM REAL_LNEG_UNIQ, GSYM REAL_RDISTRIB,
721 REAL_ADD_LINV', REAL_MUL_LZERO]
722QED
723
724Theorem REAL_NEG_RMUL:
725 !x y. ~(x * y) = x * ~y
726Proof
727 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
728 MATCH_ACCEPT_TAC REAL_NEG_LMUL
729QED
730
731Theorem REAL_LE_SQUARE:
732 !x. 0r <= x * x
733Proof
734 GEN_TAC THEN DISJ_CASES_TAC (SPEC “x:real” REAL_LE_NEGTOTAL) THEN
735 POP_ASSUM(MP_TAC o MATCH_MP REAL_LE_MUL o W CONJ) THEN
736 REWRITE_TAC[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
737QED
738
739Theorem REAL_LE_01:
740 0r <= 1r
741Proof
742 SUBST1_TAC(SYM(SPEC “1r” REAL_MUL_LID')) THEN
743 MATCH_ACCEPT_TAC REAL_LE_SQUARE
744QED
745
746Theorem REAL_LT_01:
747 0r < 1r
748Proof
749 REWRITE_TAC[REAL_LT_LE, REAL_LE_01] THEN
750 CONV_TAC(RAND_CONV SYM_CONV) THEN
751 REWRITE_TAC[REAL_10']
752QED
753
754Theorem REAL_LE_ADDR :
755 !x y. x <= x + y <=> 0r <= y
756Proof
757 REPEAT GEN_TAC THEN
758 SUBST1_TAC(SYM(SPECL [“x:real”, “0r”, “y:real”] REAL_LE_LADD)) THEN
759 REWRITE_TAC[REAL_ADD_RID]
760QED
761
762Theorem REAL_LE_REFL:
763 !x. x <= x
764Proof
765 GEN_TAC THEN REWRITE_TAC[real_lte, REAL_LT_REFL]
766QED
767
768(* NOTE: previous the other REAL_POS above was exported in realaxTheory *)
769Theorem REAL_POS:
770 !n. 0r <= real_of_num n
771Proof
772 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
773 MATCH_MP_TAC REAL_LE_TRANS THEN
774 EXISTS_TAC “real_of_num n” THEN ASM_REWRITE_TAC[REAL] THEN
775 REWRITE_TAC[REAL_LE_ADDR, REAL_LE_01]
776QED
777
778Theorem REAL_LE:
779 !m n. real_of_num m <= real_of_num n <=> m <= n
780Proof
781 REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC
782 [REAL, REAL_LE_RADD, ZERO_LESS_EQ, LESS_EQ_MONO, REAL_LE_REFL] THEN
783 REWRITE_TAC[GSYM NOT_LESS, LESS_0] THENL
784 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “real_of_num n” THEN
785 ASM_REWRITE_TAC[ZERO_LESS_EQ, REAL_LE_ADDR, REAL_LE_01],
786 DISCH_THEN(MP_TAC o C CONJ (SPEC “m:num” REAL_POS)) THEN
787 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_TRANS) THEN
788 REWRITE_TAC[REAL_NOT_LE, REAL_LT_ADDR, REAL_LT_01]]
789QED
790
791(* HOL-Light compatible name of the above theorem *)
792Theorem REAL_OF_NUM_LE = REAL_LE;
793
794(* |- !n. 0 <= n *)
795val LE_0 = ZERO_LESS_EQ; (* arithmeticTheory *)
796
797Theorem REAL_ABS_NUM :
798 !n. abs(real_of_num n) = real_of_num n
799Proof
800 REWRITE_TAC[real_abs, REAL_OF_NUM_LE, LE_0]
801QED
802
803Theorem REAL_LTE_TOTAL:
804 !x y. x < y \/ y <= x
805Proof
806 REWRITE_TAC[real_lt] THEN CONV_TAC TAUT
807QED
808
809Theorem REAL_LET_TOTAL:
810 !x y. x <= y \/ y < x
811Proof
812 REWRITE_TAC[real_lt] THEN CONV_TAC TAUT
813QED
814
815Theorem REAL_LTE_TRANS:
816 !x y z. x < y /\ y <= z ==> x < z
817Proof
818 MESON_TAC[real_lt, REAL_LE_TRANS]
819QED
820
821Theorem REAL_LE_ADD:
822 !x y. 0r <= x /\ 0r <= y ==> 0r <= (x + y)
823Proof
824 MESON_TAC[REAL_LE_LADD_IMP, REAL_ADD_RID, REAL_LE_TRANS]
825QED
826
827Theorem REAL_LTE_ANTISYM:
828 !x y. ~(x <= y /\ y < x)
829Proof
830 MESON_TAC[real_lt]
831QED
832
833Theorem REAL_SUB_LE:
834 !x y. 0r <= (x - y) <=> y <= x
835Proof
836 REWRITE_TAC[real_sub, GSYM REAL_LE_LNEG, REAL_LE_NEG2]
837QED
838
839Theorem REAL_NEG_SUB:
840 !x y. ~(x - y) = y - x
841Proof
842 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEG_NEG] THEN
843 REWRITE_TAC[Once REAL_ADD_AC]
844QED
845
846Theorem REAL_SUB_LT:
847 !x y. 0r < x - y <=> y < x
848Proof
849 REWRITE_TAC[real_lt] THEN ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN
850 REWRITE_TAC[REAL_LE_LNEG, REAL_ADD_RID, REAL_SUB_LE]
851QED
852
853Theorem REAL_LE_ANTISYM:
854 !x y. x <= y /\ y <= x <=> (x = y)
855Proof
856 REPEAT GEN_TAC THEN EQ_TAC THENL
857 [REWRITE_TAC[real_lte] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
858 (SPECL [“x:real”, “y:real”] REAL_LT_TOTAL) THEN
859 ASM_REWRITE_TAC[],
860 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LE_REFL]]
861QED
862
863Theorem REAL_NOT_LT:
864 !x y. ~(x < y) <=> y <= x
865Proof
866 REWRITE_TAC[real_lte]
867QED
868
869Theorem REAL_SUB_0:
870 !x y. (x - y = 0r) <=> (x = y)
871Proof
872 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
873 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) empty_rewrites
874 [GSYM REAL_NOT_LT] THEN
875 REWRITE_TAC[REAL_SUB_LE, REAL_SUB_LT] THEN REWRITE_TAC[REAL_NOT_LT]
876QED
877
878Theorem REAL_LTE_ADD:
879 !x y. 0r < x /\ 0r <= y ==> 0r < (x + y)
880Proof
881 MESON_TAC[REAL_LE_LADD_IMP, REAL_ADD_RID, REAL_LTE_TRANS]
882QED
883
884Theorem REAL_LET_ADD:
885 !x y. 0r <= x /\ 0r < y ==> 0r < (x + y)
886Proof
887 MESON_TAC[REAL_LTE_ADD, REAL_ADD_SYM]
888QED
889
890Theorem REAL_LT_ADD:
891 !x y. 0r < x /\ 0r < y ==> 0r < (x + y)
892Proof
893 MESON_TAC[REAL_LT_IMP_LE, REAL_LTE_ADD]
894QED
895
896Theorem REAL_ENTIRE:
897 !x y. (x * y = 0r) <=> (x = 0r) \/ (y = 0r)
898Proof
899 REPEAT GEN_TAC THEN EQ_TAC THENL
900 [ASM_CASES_TAC “x = 0r” THEN ASM_REWRITE_TAC[] THEN
901 RULE_ASSUM_TAC(MATCH_MP REAL_MUL_LINV') THEN
902 DISCH_THEN(MP_TAC o AP_TERM “$* (inv x)”) THEN
903 ASM_REWRITE_TAC[REAL_MUL_ASSOC, REAL_MUL_LID', REAL_MUL_RZERO],
904 DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN
905 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO]]
906QED
907
908Theorem REAL_MUL_RID:
909 !x. x * 1r = x
910Proof
911 MESON_TAC[REAL_MUL_LID', REAL_MUL_SYM]
912QED
913
914Theorem REAL_POW_2:
915 !x. x pow 2 = x * x
916Proof
917 REWRITE_TAC[num_CONV “2:num”, num_CONV “1:num”] THEN
918 REWRITE_TAC[real_pow, REAL_MUL_RID]
919QED
920
921(* This actually shows that real numbers and (+,*,0,1) form a semi-ring *)
922Theorem REAL_POLY_CLAUSES[local] :
923 (!x y z. x + (y + z) = (x + y) + z) /\
924 (!x y. x + y = y + x) /\
925 (!x. 0r + x = x) /\
926 (!x y z. x * (y * z) = (x * y) * z) /\
927 (!x y. x * y = y * x) /\
928 (!x. 1r * x = x) /\
929 (!x. 0r * x = 0r) /\
930 (!x y z. x * (y + z) = x * y + x * z) /\
931 (!x. x pow 0 = 1r) /\
932 (!x n. x pow (SUC n) = x * x pow n)
933Proof
934 REWRITE_TAC[real_pow, REAL_ADD_LDISTRIB, REAL_MUL_LZERO] THEN
935 REWRITE_TAC[REAL_MUL_ASSOC, REAL_ADD_ASSOC, REAL_ADD_LID', REAL_MUL_LID'] THEN
936 REWRITE_TAC[Once REAL_ADD_AC] THEN REWRITE_TAC[Once REAL_MUL_SYM]
937QED
938Theorem REAL_POLY_CLAUSES = MATCH_MP SEMIRING_PTHS REAL_POLY_CLAUSES;
939
940Theorem REAL_POLY_NEG_CLAUSES :
941 (!x. ~x = ~(1r) * x) /\
942 (!x y. x - y = x + ~(1r) * y)
943Proof
944 REWRITE_TAC[REAL_MUL_LNEG, real_sub, REAL_MUL_LID']
945QED
946
947Theorem REAL_LE_TOTAL:
948 !x y. x <= y \/ y <= x
949Proof
950 REPEAT GEN_TAC THEN
951 REWRITE_TAC[real_lte, GSYM DE_MORGAN_THM, REAL_LT_ANTISYM]
952QED
953
954(* NOTE: MESON_TAC (original proof) doesn't work here. METIS_TAC is used *)
955Theorem REAL_ABS_NEG :
956 !x. abs(~x) = abs x
957Proof
958 GEN_TAC THEN
959 REWRITE_TAC[real_abs, REAL_LE_RNEG, REAL_NEG_NEG, REAL_ADD_LID'] THEN
960 METIS_TAC[REAL_LE_TOTAL, REAL_LE_ANTISYM, REAL_NEG_0]
961QED
962
963Theorem REAL_LT_NZ:
964 !n. ~(real_of_num n = 0r) <=> (0r < real_of_num n)
965Proof
966 GEN_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN
967 CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
968 ASM_CASES_TAC “real_of_num n = 0r” THEN
969 ASM_REWRITE_TAC[REAL_LE_REFL, REAL_POS]
970QED
971
972Theorem REAL_INJ:
973 !m n. (real_of_num m = real_of_num n) <=> (m = n)
974Proof
975 let val th = prove(“(m:num = n) <=> m <= n /\ n <= m”,
976 EQ_TAC THENL
977 [DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[LESS_EQ_REFL],
978 MATCH_ACCEPT_TAC LESS_EQUAL_ANTISYM]) in
979 REPEAT GEN_TAC THEN
980 REWRITE_TAC[th, GSYM REAL_LE_ANTISYM, REAL_LE] end
981QED
982
983(* HOL-Light compatible name *)
984Theorem REAL_OF_NUM_EQ = REAL_INJ;
985
986(* This theorem is mainly for RealArith.REAL_LINEAR_PROVER *)
987Theorem REAL_POS_LT :
988 !n. 0r < real_of_num (SUC n)
989Proof
990 GEN_TAC
991 >> REWRITE_TAC [Q.SPEC ‘SUC n’ (GSYM REAL_LT_NZ), REAL_INJ]
992 >> ARITH_TAC
993QED
994
995Theorem REAL_INT_LE_CONV_tth[unlisted] = TAUT_PROVE
996 “(F /\ F = F) /\ (F /\ T = F) /\ (T /\ F = F) /\ (T /\ T = T)”;
997Theorem REAL_INT_LE_CONV_nth[unlisted] = TAUT_PROVE “(~T = F) /\ (~F = T)”;
998
999Theorem REAL_INT_LE_CONV_pth[unlisted]:
1000 (~(&m) <= &n = T) /\
1001 (&m <= (&n : real) = m <= n) /\
1002 (~(&m) <= ~(&n) = n <= m) /\
1003 (&m <= ~(&n) = (m = 0) /\ (n = 0))
1004Proof
1005 REWRITE_TAC[REAL_LE_NEG2]
1006 >> REWRITE_TAC[REAL_LE_LNEG, REAL_LE_RNEG]
1007 >> REWRITE_TAC[REAL_ADD, REAL_OF_NUM_LE, LE_0]
1008 >> REWRITE_TAC[LE, ADD_EQ_0]
1009QED
1010
1011Theorem REAL_INT_LT_CONV_pth[unlisted]:
1012 (&m < ~(&n) = F) /\
1013 (&m < (&n :real) = m < n) /\
1014 (~(&m) < ~(&n) = n < m) /\
1015 (~(&m) < &n = ~((m = 0) /\ (n = 0)))
1016Proof
1017 REWRITE_TAC[REAL_INT_LE_CONV_pth, GSYM NOT_LE, real_lt]
1018 >> CONV_TAC tautLib.TAUT_CONV
1019QED
1020
1021Theorem REAL_INT_GE_CONV_pth[unlisted]:
1022 (&m >= ~(&n) = T) /\
1023 (&m >= (&n :real) = n <= m) /\
1024 (~(&m) >= ~(&n) = m <= n) /\
1025 (~(&m) >= &n = (m = 0) /\ (n = 0))
1026Proof
1027 REWRITE_TAC[REAL_INT_LE_CONV_pth, real_ge]
1028 >> CONV_TAC tautLib.TAUT_CONV
1029QED
1030
1031Theorem REAL_INT_GT_CONV_pth[unlisted]:
1032 (~(&m) > &n = F) /\
1033 (&m > (&n :real) = n < m) /\
1034 (~(&m) > ~(&n) = m < n) /\
1035 (&m > ~(&n) = ~((m = 0) /\ (n = 0)))
1036Proof
1037 REWRITE_TAC[REAL_INT_LT_CONV_pth, real_gt]
1038 >> CONV_TAC tautLib.TAUT_CONV
1039QED
1040
1041Theorem REAL_INT_EQ_CONV_pth[unlisted]:
1042 ((&m = (&n :real)) = (m = n)) /\
1043 ((~(&m) = ~(&n)) = (m = n)) /\
1044 ((~(&m) = &n) = (m = 0) /\ (n = 0)) /\
1045 ((&m = ~(&n)) = (m = 0) /\ (n = 0))
1046Proof
1047 REWRITE_TAC[GSYM REAL_LE_ANTISYM, GSYM LE_ANTISYM]
1048 \\ REWRITE_TAC[REAL_INT_LE_CONV_pth, LE, LE_0]
1049 \\ CONV_TAC tautLib.TAUT_CONV
1050QED
1051
1052Theorem REAL_INT_NEG_CONV_pth[unlisted]:
1053 (~(&0) = &0) /\ (~(~(&x)) = &x)
1054Proof
1055 REWRITE_TAC[REAL_NEG_NEG, REAL_NEG_0]
1056QED
1057
1058Theorem REAL_INT_MUL_CONV_pth0[unlisted]:
1059 (&0 * (&x :real) = &0) /\
1060 (&0 * ~(&x) = &0) /\
1061 ((&x :real) * &0 = &0) /\
1062 (~(&x :real) * &0 = &0)
1063Proof
1064 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO]
1065QED
1066
1067Theorem REAL_INT_MUL_CONV_pth1[unlisted]:
1068 ((&m * &n = &(m * n) :real) /\ (~(&m) * ~(&n) = &(m * n) :real)) /\
1069 ((~(&m) * &n = ~(&(m * n) :real)) /\ (&m * ~(&n) = ~(&(m * n) :real)))
1070Proof
1071 REWRITE_TAC[REAL_MUL_LNEG, REAL_MUL_RNEG, REAL_NEG_NEG]
1072 >> REWRITE_TAC[REAL_OF_NUM_MUL]
1073QED
1074
1075Theorem REAL_PROD_NORM_CONV_pth1[unlisted] = SYM(SPEC ``x:real`` REAL_MUL_RID)
1076Theorem REAL_PROD_NORM_CONV_pth2[unlisted] = SYM(SPEC ``x:real`` REAL_MUL_LID')
1077
1078Theorem REAL_INT_ADD_CONV_pth0[unlisted]:
1079 (~(&m) + &m = &0) /\ (&m + ~(&m) = &0)
1080Proof
1081 REWRITE_TAC[REAL_ADD_LINV', REAL_ADD_RINV]
1082QED
1083
1084Theorem REAL_INT_ADD_CONV_pth1[unlisted]:
1085 (~(&m) + ~(&n :real) = ~(&(m + n))) /\
1086 (~(&m) + &(m + n) = &n) /\
1087 (~(&(m + n)) + &m = ~(&n)) /\
1088 (&(m + n) + ~(&m) = &n) /\
1089 (&m + ~(&(m + n)) = ~(&n)) /\
1090 (&m + &n = &(m + n) :real)
1091Proof
1092 REWRITE_TAC[GSYM REAL_ADD, REAL_NEG_ADD] THEN
1093 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV', REAL_ADD_LID'] THEN
1094 REWRITE_TAC[REAL_ADD_RINV, REAL_ADD_LID'] THEN
1095 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1096 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV', REAL_ADD_LID'] THEN
1097 REWRITE_TAC[REAL_ADD_RINV, REAL_ADD_LID']
1098QED
1099
1100Theorem LINEAR_ADD_pth0a[unlisted]:
1101 &0 + x = x :real
1102Proof
1103 REWRITE_TAC[REAL_ADD_LID']
1104QED
1105
1106Theorem LINEAR_ADD_pth0b[unlisted]:
1107 x + &0 = x :real
1108Proof
1109 REWRITE_TAC[REAL_ADD_RID]
1110QED
1111
1112Theorem LINEAR_ADD_pth1[unlisted]:
1113 ((l1 + r1) + (l2 + r2) = (l1 + l2) + (r1 + r2):real) /\
1114 ((l1 + r1) + tm2 = l1 + (r1 + tm2):real) /\
1115 (tm1 + (l2 + r2) = l2 + (tm1 + r2)) /\
1116 ((l1 + r1) + tm2 = (l1 + tm2) + r1) /\
1117 (tm1 + tm2 = tm2 + tm1) /\
1118 (tm1 + (l2 + r2) = (tm1 + l2) + r2)
1119Proof
1120 REPEAT CONJ_TAC
1121 THEN REWRITE_TAC[REAL_ADD_ASSOC]
1122 THEN TRY (MATCH_ACCEPT_TAC REAL_ADD_SYM) THENL
1123 [REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN AP_TERM_TAC
1124 THEN ONCE_REWRITE_TAC [REAL_ADD_SYM]
1125 THEN Ho_Rewrite.GEN_REWRITE_TAC RAND_CONV [REAL_ADD_SYM]
1126 THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN AP_TERM_TAC
1127 THEN MATCH_ACCEPT_TAC REAL_ADD_SYM,
1128 ONCE_REWRITE_TAC [REAL_ADD_SYM] THEN AP_TERM_TAC
1129 THEN MATCH_ACCEPT_TAC REAL_ADD_SYM,
1130 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN AP_TERM_TAC
1131 THEN MATCH_ACCEPT_TAC REAL_ADD_SYM]
1132QED
1133
1134Theorem REAL_SUM_NORM_CONV_pth1[unlisted]:
1135 ~x = ~(&1) * x
1136Proof
1137 REWRITE_TAC[REAL_MUL_LNEG, REAL_MUL_LID']
1138QED
1139
1140Theorem REAL_SUM_NORM_CONV_pth2[unlisted]:
1141 x - y:real = x + ~(&1) * y
1142Proof
1143 REWRITE_TAC[real_sub, GSYM REAL_SUM_NORM_CONV_pth1]
1144QED
1145
1146Theorem REAL_NEGATE_CANON_pth1[unlisted]:
1147 ((a:real <= b = &0 <= X) = (b < a = &0 < ~X)) /\
1148 ((a:real < b = &0 < X) = (b <= a = &0 <= ~X))
1149Proof
1150 REWRITE_TAC[real_lt, REAL_LE_LNEG, REAL_LE_RNEG] THEN
1151 REWRITE_TAC[REAL_ADD_RID, REAL_ADD_LID'] THEN
1152 CONV_TAC tautLib.TAUT_CONV
1153QED
1154
1155Theorem REAL_NEGATE_CANON_pth2[unlisted]:
1156 ~((~a) * x + z :real) = a * x + ~z
1157Proof
1158 REWRITE_TAC[GSYM REAL_MUL_LNEG, REAL_NEG_ADD, REAL_NEG_NEG]
1159QED
1160
1161Theorem REAL_NEGATE_CANON_pth3[unlisted]:
1162 ~(a * x + z :real) = ~a * x + ~z
1163Proof
1164 REWRITE_TAC[REAL_NEG_ADD, GSYM REAL_MUL_LNEG]
1165QED
1166
1167Theorem REAL_NEGATE_CANON_pth4[unlisted]:
1168 ~(~a * x :real) = a * x
1169Proof
1170 REWRITE_TAC[REAL_MUL_LNEG, REAL_NEG_NEG]
1171QED
1172
1173Theorem REAL_NEGATE_CANON_pth5[unlisted]:
1174 ~(a * x :real) = ~a * x
1175Proof
1176 REWRITE_TAC[REAL_MUL_LNEG]
1177QED
1178
1179Theorem REAL_ATOM_NORM_CONV_pth2[unlisted]:
1180 (a:real < b = c < d:real) = (b <= a = d <= c)
1181Proof
1182 REWRITE_TAC[real_lt] THEN CONV_TAC tautLib.TAUT_CONV
1183QED
1184
1185Theorem REAL_ATOM_NORM_CONV_pth3[unlisted]:
1186 (a:real <= b = c <= d:real) = (b < a = d < c)
1187Proof
1188 REWRITE_TAC[real_lt] THEN CONV_TAC tautLib.TAUT_CONV
1189QED
1190
1191Theorem REAL_INT_POW_CONV_pth1[unlisted]:
1192 (&x pow n = &(x EXP n)) /\
1193 ((~(&x)) pow n = if EVEN n then &(x EXP n) else ~(&(x EXP n)))
1194Proof
1195 REWRITE_TAC[REAL_OF_NUM_POW, REAL_POW_NEG]
1196QED
1197
1198Theorem REAL_INT_POW_CONV_tth[unlisted]:
1199 ((if T then x:real else y) = x) /\ ((if F then x:real else y) = y)
1200Proof
1201 REWRITE_TAC[]
1202QED
1203
1204Theorem REAL_INT_ABS_CONV_pth[unlisted]:
1205 (abs(~(&x)) = &x) /\
1206 (abs(&x) = &x)
1207Proof
1208 REWRITE_TAC[REAL_ABS_NEG, REAL_ABS_NUM]
1209QED
1210
1211Theorem LINEAR_MULT_pth[unlisted]:
1212 x * &0 = &0 :real
1213Proof
1214 REWRITE_TAC[REAL_MUL_RZERO]
1215QED
1216
1217Theorem ADD_INEQS_pth[unlisted]:
1218 ((&0 = a) /\ (&0 = b) ==> (&0 = a + b :real)) /\
1219 ((&0 = a) /\ (&0 <= b) ==> (&0 <= a + b :real)) /\
1220 ((&0 = a) /\ (&0 < b) ==> (&0 < a + b :real)) /\
1221 ((&0 <= a) /\ (&0 = b) ==> (&0 <= a + b :real)) /\
1222 ((&0 <= a) /\ (&0 <= b) ==> (&0 <= a + b :real)) /\
1223 ((&0 <= a) /\ (&0 < b) ==> (&0 < a + b :real)) /\
1224 ((&0 < a) /\ (&0 = b) ==> (&0 < a + b :real)) /\
1225 ((&0 < a) /\ (&0 <= b) ==> (&0 < a + b :real)) /\
1226 ((&0 < a) /\ (&0 < b) ==> (&0 < a + b :real))
1227Proof
1228 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
1229 REPEAT STRIP_TAC THEN
1230 ASM_REWRITE_TAC[REAL_ADD_LID', REAL_ADD_RID] THENL
1231 [MATCH_MP_TAC REAL_LE_TRANS,
1232 MATCH_MP_TAC REAL_LET_TRANS,
1233 MATCH_MP_TAC REAL_LTE_TRANS,
1234 MATCH_MP_TAC REAL_LT_TRANS] THEN
1235 EXISTS_TAC ``a:real`` THEN ASM_REWRITE_TAC[] THEN
1236 Ho_Rewrite.GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN
1237 (MATCH_MP_TAC REAL_LE_LADD_IMP ORELSE MATCH_MP_TAC REAL_LT_LADD_IMP)
1238 THEN ASM_REWRITE_TAC[]
1239QED
1240
1241Theorem MULTIPLY_INEQS_pth[unlisted]:
1242 ((&0 = y) ==> (&0 = x * y :real)) /\
1243 (&0 <= y ==> &0 <= x ==> &0 <= x * y :real) /\
1244 (&0 < y ==> &0 < x ==> &0 < x * y :real)
1245Proof
1246 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
1247 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO] THENL
1248 [MATCH_MP_TAC REAL_LE_MUL,
1249 MATCH_MP_TAC REAL_LT_MUL'] THEN
1250 ASM_REWRITE_TAC[]
1251QED
1252
1253Theorem REAL_SIMPLE_ARITH_REFUTER_trivthm[unlisted]:
1254 &0 < &0 :real = F
1255Proof
1256 REWRITE_TAC[REAL_LE_REFL, real_lt]
1257QED
1258
1259Theorem ZERO_LEFT_CONV_pth[unlisted]:
1260 ((x = y) = (&0 = y + ~x)) /\
1261 (x <= y = &0 <= y + ~x) /\
1262 (x < y = &0 < y + ~x)
1263Proof
1264 REWRITE_TAC[real_lt, GSYM REAL_LE_LNEG, REAL_LE_NEG2] THEN
1265 REWRITE_TAC[GSYM REAL_LE_RNEG, REAL_NEG_NEG] THEN
1266 REWRITE_TAC[GSYM REAL_LE_ANTISYM, GSYM REAL_LE_LNEG,
1267 GSYM REAL_LE_RNEG, REAL_LE_NEG2, REAL_NEG_NEG]
1268QED
1269
1270Theorem ABS_ELIM_THM[unlisted]:
1271 (&0 <= ~(abs(x)) + y = &0 <= x + y /\ &0 <= ~x + y) /\
1272 (&0 < ~(abs(x)) + y = &0 < x + y /\ &0 < ~x + y)
1273Proof
1274 REWRITE_TAC[real_abs] THEN COND_CASES_TAC
1275 THEN ASM_REWRITE_TAC[] THEN
1276 REWRITE_TAC[REAL_NEG_NEG] THEN
1277 REWRITE_TAC [
1278 TAUT_PROVE ``(a = a /\ b) = (a ==> b)``,
1279 TAUT_PROVE ``(b = a /\ b) = (b ==> a)``
1280 ]
1281 THEN REPEAT STRIP_TAC THEN
1282 MAP_FIRST MATCH_MP_TAC [REAL_LE_TRANS, REAL_LTE_TRANS] THEN
1283 FIRST_ASSUM(fn th => EXISTS_TAC(rand(concl th)) THEN
1284 CONJ_TAC THENL [ACCEPT_TAC th, ALL_TAC]) THEN
1285 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1286 MATCH_MP_TAC REAL_LE_LADD_IMP THEN
1287 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ``&0 :real`` THEN
1288 REWRITE_TAC[REAL_LE_LNEG, REAL_LE_RNEG] THEN
1289 ASM_REWRITE_TAC[REAL_ADD_RID, REAL_ADD_LID'] THEN
1290 MP_TAC (SPEC(Term`&0 :real`) (SPEC (Term`x:real`)
1291 REAL_LE_TOTAL))
1292 THEN ASM_REWRITE_TAC[]
1293QED
1294
1295Theorem ABS_CASES_THM[unlisted]:
1296 (abs(x) = x) \/ (abs(x) = ~x)
1297Proof
1298 REWRITE_TAC[real_abs] THEN COND_CASES_TAC
1299 THEN REWRITE_TAC[]
1300QED
1301
1302Theorem ABS_STRONG_CASES_THM[unlisted]:
1303 &0 <= x /\ (abs(x) = x) \/ (&0 <= ~x) /\ (abs(x) = ~x)
1304Proof
1305 REWRITE_TAC[real_abs] THEN COND_CASES_TAC
1306 THEN REWRITE_TAC[] THEN
1307 REWRITE_TAC[REAL_LE_RNEG, REAL_ADD_LID'] THEN
1308 MP_TAC (SPECL [``&0 :real``, ``x:real``] REAL_LE_TOTAL)
1309 THEN ASM_REWRITE_TAC[]
1310QED
1311
1312Theorem atom_CONV_pth[unlisted]:
1313 (~(x:real <= y) = y < x) /\
1314 (~(x:real < y) = y <= x) /\
1315 (~(x = y) = (x:real) < y \/ y < x)
1316Proof
1317 REWRITE_TAC[real_lt] THEN REWRITE_TAC[GSYM DE_MORGAN_THM] THEN
1318 REWRITE_TAC[REAL_LE_ANTISYM] THEN AP_TERM_TAC THEN
1319 MATCH_ACCEPT_TAC EQ_SYM_EQ
1320QED
1321
1322Theorem REAL_LINEAR_PROVER_pth[unlisted] = (* |- &n >= 0 *)
1323 REWRITE_RULE [GSYM real_ge] (SPEC “n:num” REAL_POS);
1324Theorem REAL_LINEAR_PROVER_pth'[unlisted] = (* |- &SUC n > 0 *)
1325 REWRITE_RULE [GSYM real_gt] (SPEC “n:num” REAL_POS_LT);
1326
1327Theorem GEN_REAL_ARITH0_pth_init[unlisted]:
1328 (x < y <=> y - x > &0) /\
1329 (x <= y <=> y - x >= &0) /\
1330 (x > y <=> x - y > &0) /\
1331 (x >= y <=> x - y >= &0) /\
1332 ((x = y) <=> (x - y = &0)) /\
1333 (~(x < y) <=> x - y >= &0) /\
1334 (~(x <= y) <=> x - y > &0) /\
1335 (~(x > y) <=> y - x >= &0) /\
1336 (~(x >= y) <=> y - x > &0) /\
1337 (~(x = y) <=> x - y > &0 \/ ~(x - y) > &0)
1338Proof
1339 REWRITE_TAC[real_gt, real_ge, REAL_SUB_LT, REAL_SUB_LE, REAL_NEG_SUB] >>
1340 REWRITE_TAC[REAL_SUB_0, real_lt] >>
1341 EQ_TAC THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC bool_ss [REAL_LE_REFL] >>
1342 CCONTR_TAC THEN FULL_SIMP_TAC bool_ss [] >>
1343 drule_all $ iffLR REAL_LE_ANTISYM >> ASM_SIMP_TAC bool_ss []
1344QED
1345
1346Theorem GEN_REAL_ARITH0_pth_final[unlisted] = tautLib.TAUT `(~p ==> F) ==> p`;
1347Theorem GEN_REAL_ARITH0_pth_add[unlisted]:
1348 ((x = &0) /\ (y = &0) ==> (x + y = &0 :real)) /\
1349 ((x = &0) /\ y >= &0 ==> x + y >= &0) /\
1350 ((x = &0) /\ y > &0 ==> x + y > &0) /\
1351 (x >= &0 /\ (y = &0) ==> x + y >= &0) /\
1352 (x >= &0 /\ y >= &0 ==> x + y >= &0) /\
1353 (x >= &0 /\ y > &0 ==> x + y > &0) /\
1354 (x > &0 /\ (y = &0) ==> x + y > &0) /\
1355 (x > &0 /\ y >= &0 ==> x + y > &0) /\
1356 (x > &0 /\ y > &0 ==> x + y > &0)
1357Proof
1358 SIMP_TAC arith_ss [REAL_ADD_LID', REAL_ADD_RID, real_ge, real_gt] THEN
1359 REWRITE_TAC[REAL_LE_LT] THEN
1360 REPEAT STRIP_TAC >>
1361 RW_TAC bool_ss [REAL_LT_ADD, REAL_ADD_RID, REAL_ADD_LID']
1362QED
1363
1364Theorem GEN_REAL_ARITH0_pth_mul[unlisted]:
1365 ((x = &0) /\ (y = &0) ==> (x * y = &0 :real)) /\
1366 ((x = &0) /\ y >= &0 ==> (x * y = &0)) /\
1367 ((x = &0) /\ y > &0 ==> (x * y = &0)) /\
1368 (x >= &0 /\ (y = &0) ==> (x * y = &0)) /\
1369 (x >= &0 /\ y >= &0 ==> x * y >= &0) /\
1370 (x >= &0 /\ y > &0 ==> x * y >= &0) /\
1371 (x > &0 /\ (y = &0) ==> (x * y = &0)) /\
1372 (x > &0 /\ y >= &0 ==> x * y >= &0) /\
1373 (x > &0 /\ y > &0 ==> x * y > &0)
1374Proof
1375 SIMP_TAC arith_ss [REAL_MUL_LZERO, REAL_MUL_RZERO, real_ge, real_gt] THEN
1376 SIMP_TAC arith_ss [REAL_LT_LE, REAL_LE_MUL, REAL_ENTIRE]
1377QED
1378
1379Theorem GEN_REAL_ARITH0_pth_emul[unlisted]:
1380 (y = &0) ==> !x. x * y = &0 :real
1381Proof
1382 SIMP_TAC arith_ss [REAL_MUL_RZERO]
1383QED
1384
1385Theorem GEN_REAL_ARITH0_pth_square[unlisted]:
1386 !x. x * x >= &0 :real
1387Proof
1388 REWRITE_TAC[real_ge, REAL_POW_2, REAL_LE_SQUARE]
1389QED
1390
1391Theorem ABSMAXMIN_ELIM_CONV2_pth_abs[unlisted]:
1392 P(abs x) <=> (x >= &0 /\ P x) \/ (&0 > x /\ P (~x))
1393Proof
1394 REWRITE_TAC[real_abs, real_gt, real_ge] THEN COND_CASES_TAC THEN
1395 ASM_REWRITE_TAC[real_lt]
1396QED
1397
1398Theorem ABSMAXMIN_ELIM_CONV2_pth_max[unlisted]:
1399 P(max x y) <=> (y >= x /\ P y) \/ (x > y /\ P x)
1400Proof
1401 REWRITE_TAC[real_max, real_gt, real_ge] THEN
1402 COND_CASES_TAC THEN ASM_REWRITE_TAC[real_lt]
1403QED
1404
1405Theorem ABSMAXMIN_ELIM_CONV2_pth_min[unlisted]:
1406 P(min x y) <=> (y >= x /\ P x) \/ (x > y /\ P y)
1407Proof
1408 REWRITE_TAC[real_min, real_gt, real_ge] THEN
1409 COND_CASES_TAC THEN ASM_REWRITE_TAC[real_lt]
1410QED