real.ml

   1 (* ========================================================================= *)
   2 (* More basic properties of the reals.                                       *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (*              (c) Copyright, Valentina Bruno 2010                          *)
   9 (* ========================================================================= *)
  10
  11 needs "realarith.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Additional commutativity properties of the inclusion map.                 *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let REAL_OF_NUM_LT = prove
  18  (`!m n. &m < &n <=> m < n`,
  19   REWRITE_TAC[real_lt; GSYM NOT_LE; REAL_OF_NUM_LE]);;
  20
  21 let REAL_OF_NUM_GE = prove
  22  (`!m n. &m >= &n <=> m >= n`,
  23   REWRITE_TAC[GE; real_ge; REAL_OF_NUM_LE]);;
  24
  25 let REAL_OF_NUM_GT = prove
  26  (`!m n. &m > &n <=> m > n`,
  27   REWRITE_TAC[GT; real_gt; REAL_OF_NUM_LT]);;
  28
  29 let REAL_OF_NUM_MAX = prove
  30  (`!m n. max (&m) (&n) = &(MAX m n)`,
  31   REWRITE_TAC[REAL_OF_NUM_LE; MAX; real_max; GSYM COND_RAND]);;
  32
  33 let REAL_OF_NUM_MIN = prove
  34  (`!m n. min (&m) (&n) = &(MIN m n)`,
  35   REWRITE_TAC[REAL_OF_NUM_LE; MIN; real_min; GSYM COND_RAND]);;
  36
  37 let REAL_OF_NUM_SUC = prove
  38  (`!n. &n + &1 = &(SUC n)`,
  39   REWRITE_TAC[ADD1; REAL_OF_NUM_ADD]);;
  40
  41 let REAL_OF_NUM_SUB = prove
  42  (`!m n. m <= n ==> (&n - &m = &(n - m))`,
  43   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
  44   STRIP_TAC THEN ASM_REWRITE_TAC[ADD_SUB2] THEN
  45   REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
  46   ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
  47   REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC] THEN
  48   MESON_TAC[REAL_ADD_LINV; REAL_ADD_SYM; REAL_ADD_LID]);;
  49
  50 (* ------------------------------------------------------------------------- *)
  51 (* A few theorems we need to prove explicitly for later.                     *)
  52 (* ------------------------------------------------------------------------- *)
  53
  54 let REAL_MUL_AC = prove
  55  (`(m * n = n * m) /\
  56    ((m * n) * p = m * (n * p)) /\
  57    (m * (n * p) = n * (m * p))`,
  58   REWRITE_TAC[REAL_MUL_ASSOC; EQT_INTRO(SPEC_ALL REAL_MUL_SYM)] THEN
  59   AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_MUL_SYM);;
  60
  61 let REAL_ADD_RDISTRIB = prove
  62  (`!x y z. (x + y) * z = x * z + y * z`,
  63   MESON_TAC[REAL_MUL_SYM; REAL_ADD_LDISTRIB]);;
  64
  65 let REAL_LT_LADD_IMP = prove
  66  (`!x y z. y < z ==> x + y < x + z`,
  67   REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
  68   REWRITE_TAC[real_lt] THEN
  69   DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THEN
  70   DISCH_THEN(MP_TAC o SPEC `--x`) THEN
  71   REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LINV; REAL_ADD_LID]);;
  72
  73 let REAL_LT_MUL = prove
  74  (`!x y. &0 < x /\ &0 < y ==> &0 < x * y`,
  75   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN
  76   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
  77   STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ENTIRE] THEN
  78   MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]);;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* Tactic version of REAL_ARITH.                                             *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84 let REAL_ARITH_TAC = CONV_TAC REAL_ARITH;;
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* Prove all the linear theorems we can blow away automatically.             *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 let REAL_EQ_ADD_LCANCEL_0 = prove
  91  (`!x y. (x + y = x) <=> (y = &0)`,
  92   REAL_ARITH_TAC);;
  93
  94 let REAL_EQ_ADD_RCANCEL_0 = prove
  95  (`!x y. (x + y = y) <=> (x = &0)`,
  96   REAL_ARITH_TAC);;
  97
  98 let REAL_LNEG_UNIQ = prove
  99  (`!x y. (x + y = &0) <=> (x = --y)`,
 100   REAL_ARITH_TAC);;
 101
 102 let REAL_RNEG_UNIQ = prove
 103  (`!x y. (x + y = &0) <=> (y = --x)`,
 104   REAL_ARITH_TAC);;
 105
 106 let REAL_NEG_LMUL = prove
 107  (`!x y. --(x * y) = (--x) * y`,
 108   REAL_ARITH_TAC);;
 109
 110 let REAL_NEG_RMUL = prove
 111  (`!x y. --(x * y) = x * (--y)`,
 112   REAL_ARITH_TAC);;
 113
 114 let REAL_NEGNEG = prove
 115  (`!x. --(--x) = x`,
 116   REAL_ARITH_TAC);;
 117
 118 let REAL_NEG_MUL2 = prove
 119  (`!x y. (--x) * (--y) = x * y`,
 120   REAL_ARITH_TAC);;
 121
 122 let REAL_LT_LADD = prove
 123  (`!x y z. (x + y) < (x + z) <=> y < z`,
 124   REAL_ARITH_TAC);;
 125
 126 let REAL_LT_RADD = prove
 127  (`!x y z. (x + z) < (y + z) <=> x < y`,
 128   REAL_ARITH_TAC);;
 129
 130 let REAL_LT_ANTISYM = prove
 131  (`!x y. ~(x < y /\ y < x)`,
 132   REAL_ARITH_TAC);;
 133
 134 let REAL_LT_GT = prove
 135  (`!x y. x < y ==> ~(y < x)`,
 136   REAL_ARITH_TAC);;
 137
 138 let REAL_NOT_EQ = prove
 139  (`!x y. ~(x = y) <=> x < y \/ y < x`,
 140   REAL_ARITH_TAC);;
 141
 142 let REAL_NOT_LE = prove
 143  (`!x y. ~(x <= y) <=> y < x`,
 144   REAL_ARITH_TAC);;
 145
 146 let REAL_LET_ANTISYM = prove
 147  (`!x y. ~(x <= y /\ y < x)`,
 148   REAL_ARITH_TAC);;
 149
 150 let REAL_NEG_LT0 = prove
 151  (`!x. (--x) < &0 <=> &0 < x`,
 152   REAL_ARITH_TAC);;
 153
 154 let REAL_NEG_GT0 = prove
 155  (`!x. &0 < (--x) <=> x < &0`,
 156   REAL_ARITH_TAC);;
 157
 158 let REAL_NEG_LE0 = prove
 159  (`!x. (--x) <= &0 <=> &0 <= x`,
 160   REAL_ARITH_TAC);;
 161
 162 let REAL_NEG_GE0 = prove
 163  (`!x. &0 <= (--x) <=> x <= &0`,
 164   REAL_ARITH_TAC);;
 165
 166 let REAL_LT_TOTAL = prove
 167  (`!x y. (x = y) \/ x < y \/ y < x`,
 168   REAL_ARITH_TAC);;
 169
 170 let REAL_LT_NEGTOTAL = prove
 171  (`!x. (x = &0) \/ (&0 < x) \/ (&0 < --x)`,
 172   REAL_ARITH_TAC);;
 173
 174 let REAL_LE_01 = prove
 175  (`&0 <= &1`,
 176   REAL_ARITH_TAC);;
 177
 178 let REAL_LT_01 = prove
 179  (`&0 < &1`,
 180   REAL_ARITH_TAC);;
 181
 182 let REAL_LE_LADD = prove
 183  (`!x y z. (x + y) <= (x + z) <=> y <= z`,
 184   REAL_ARITH_TAC);;
 185
 186 let REAL_LE_RADD = prove
 187  (`!x y z. (x + z) <= (y + z) <=> x <= y`,
 188   REAL_ARITH_TAC);;
 189
 190 let REAL_LT_ADD2 = prove
 191  (`!w x y z. w < x /\ y < z ==> (w + y) < (x + z)`,
 192   REAL_ARITH_TAC);;
 193
 194 let REAL_LE_ADD2 = prove
 195  (`!w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z)`,
 196   REAL_ARITH_TAC);;
 197
 198 let REAL_LT_LNEG = prove
 199  (`!x y. --x < y <=> &0 < x + y`,
 200   REWRITE_TAC[real_lt; REAL_LE_RNEG; REAL_ADD_AC]);;
 201
 202 let REAL_LT_RNEG = prove
 203  (`!x y. x < --y <=> x + y < &0`,
 204   REWRITE_TAC[real_lt; REAL_LE_LNEG; REAL_ADD_AC]);;
 205
 206 let REAL_LT_ADDNEG = prove
 207  (`!x y z. y < (x + (--z)) <=> (y + z) < x`,
 208   REAL_ARITH_TAC);;
 209
 210 let REAL_LT_ADDNEG2 = prove
 211  (`!x y z. (x + (--y)) < z <=> x < (z + y)`,
 212   REAL_ARITH_TAC);;
 213
 214 let REAL_LT_ADD1 = prove
 215  (`!x y. x <= y ==> x < (y + &1)`,
 216   REAL_ARITH_TAC);;
 217
 218 let REAL_SUB_ADD = prove
 219  (`!x y. (x - y) + y = x`,
 220   REAL_ARITH_TAC);;
 221
 222 let REAL_SUB_ADD2 = prove
 223  (`!x y. y + (x - y) = x`,
 224   REAL_ARITH_TAC);;
 225
 226 let REAL_SUB_REFL = prove
 227  (`!x. x - x = &0`,
 228   REAL_ARITH_TAC);;
 229
 230 let REAL_LE_DOUBLE = prove
 231  (`!x. &0 <= x + x <=> &0 <= x`,
 232   REAL_ARITH_TAC);;
 233
 234 let REAL_LE_NEGL = prove
 235  (`!x. (--x <= x) <=> (&0 <= x)`,
 236   REAL_ARITH_TAC);;
 237
 238 let REAL_LE_NEGR = prove
 239  (`!x. (x <= --x) <=> (x <= &0)`,
 240   REAL_ARITH_TAC);;
 241
 242 let REAL_NEG_EQ_0 = prove
 243  (`!x. (--x = &0) <=> (x = &0)`,
 244   REAL_ARITH_TAC);;
 245
 246 let REAL_ADD_SUB = prove
 247  (`!x y. (x + y) - x = y`,
 248   REAL_ARITH_TAC);;
 249
 250 let REAL_NEG_EQ = prove
 251  (`!x y. (--x = y) <=> (x = --y)`,
 252   REAL_ARITH_TAC);;
 253
 254 let REAL_NEG_MINUS1 = prove
 255  (`!x. --x = (--(&1)) * x`,
 256   REAL_ARITH_TAC);;
 257
 258 let REAL_LT_IMP_NE = prove
 259  (`!x y. x < y ==> ~(x = y)`,
 260   REAL_ARITH_TAC);;
 261
 262 let REAL_LE_ADDR = prove
 263  (`!x y. x <= x + y <=> &0 <= y`,
 264   REAL_ARITH_TAC);;
 265
 266 let REAL_LE_ADDL = prove
 267  (`!x y. y <= x + y <=> &0 <= x`,
 268   REAL_ARITH_TAC);;
 269
 270 let REAL_LT_ADDR = prove
 271  (`!x y. x < x + y <=> &0 < y`,
 272   REAL_ARITH_TAC);;
 273
 274 let REAL_LT_ADDL = prove
 275  (`!x y. y < x + y <=> &0 < x`,
 276   REAL_ARITH_TAC);;
 277
 278 let REAL_SUB_SUB = prove
 279  (`!x y. (x - y) - x = --y`,
 280   REAL_ARITH_TAC);;
 281
 282 let REAL_LT_ADD_SUB = prove
 283  (`!x y z. (x + y) < z <=> x < (z - y)`,
 284   REAL_ARITH_TAC);;
 285
 286 let REAL_LT_SUB_RADD = prove
 287  (`!x y z. (x - y) < z <=> x < z + y`,
 288   REAL_ARITH_TAC);;
 289
 290 let REAL_LT_SUB_LADD = prove
 291  (`!x y z. x < (y - z) <=> (x + z) < y`,
 292   REAL_ARITH_TAC);;
 293
 294 let REAL_LE_SUB_LADD = prove
 295  (`!x y z. x <= (y - z) <=> (x + z) <= y`,
 296   REAL_ARITH_TAC);;
 297
 298 let REAL_LE_SUB_RADD = prove
 299  (`!x y z. (x - y) <= z <=> x <= z + y`,
 300   REAL_ARITH_TAC);;
 301
 302 let REAL_LT_NEG = prove
 303  (`!x y. --x < --y <=> y < x`,
 304   REAL_ARITH_TAC);;
 305
 306 let REAL_LE_NEG = prove
 307  (`!x y. --x <= --y <=> y <= x`,
 308   REAL_ARITH_TAC);;
 309
 310 let REAL_ADD2_SUB2 = prove
 311  (`!a b c d. (a + b) - (c + d) = (a - c) + (b - d)`,
 312   REAL_ARITH_TAC);;
 313
 314 let REAL_SUB_LZERO = prove
 315  (`!x. &0 - x = --x`,
 316   REAL_ARITH_TAC);;
 317
 318 let REAL_SUB_RZERO = prove
 319  (`!x. x - &0 = x`,
 320   REAL_ARITH_TAC);;
 321
 322 let REAL_LET_ADD2 = prove
 323  (`!w x y z. w <= x /\ y < z ==> (w + y) < (x + z)`,
 324   REAL_ARITH_TAC);;
 325
 326 let REAL_LTE_ADD2 = prove
 327  (`!w x y z. w < x /\ y <= z ==> w + y < x + z`,
 328   REAL_ARITH_TAC);;
 329
 330 let REAL_SUB_LNEG = prove
 331  (`!x y. (--x) - y = --(x + y)`,
 332   REAL_ARITH_TAC);;
 333
 334 let REAL_SUB_RNEG = prove
 335  (`!x y. x - (--y) = x + y`,
 336   REAL_ARITH_TAC);;
 337
 338 let REAL_SUB_NEG2 = prove
 339  (`!x y. (--x) - (--y) = y - x`,
 340   REAL_ARITH_TAC);;
 341
 342 let REAL_SUB_TRIANGLE = prove
 343  (`!a b c. (a - b) + (b - c) = a - c`,
 344   REAL_ARITH_TAC);;
 345
 346 let REAL_EQ_SUB_LADD = prove
 347  (`!x y z. (x = y - z) <=> (x + z = y)`,
 348   REAL_ARITH_TAC);;
 349
 350 let REAL_EQ_SUB_RADD = prove
 351  (`!x y z. (x - y = z) <=> (x = z + y)`,
 352   REAL_ARITH_TAC);;
 353
 354 let REAL_SUB_SUB2 = prove
 355  (`!x y. x - (x - y) = y`,
 356   REAL_ARITH_TAC);;
 357
 358 let REAL_ADD_SUB2 = prove
 359  (`!x y. x - (x + y) = --y`,
 360   REAL_ARITH_TAC);;
 361
 362 let REAL_EQ_IMP_LE = prove
 363  (`!x y. (x = y) ==> x <= y`,
 364   REAL_ARITH_TAC);;
 365
 366 let REAL_POS_NZ = prove
 367  (`!x. &0 < x ==> ~(x = &0)`,
 368   REAL_ARITH_TAC);;
 369
 370 let REAL_DIFFSQ = prove
 371  (`!x y. (x + y) * (x - y) = (x * x) - (y * y)`,
 372   REAL_ARITH_TAC);;
 373
 374 let REAL_EQ_NEG2 = prove
 375  (`!x y. (--x = --y) <=> (x = y)`,
 376   REAL_ARITH_TAC);;
 377
 378 let REAL_LT_NEG2 = prove
 379  (`!x y. --x < --y <=> y < x`,
 380   REAL_ARITH_TAC);;
 381
 382 let REAL_SUB_LDISTRIB = prove
 383  (`!x y z. x * (y - z) = x * y - x * z`,
 384   REAL_ARITH_TAC);;
 385
 386 let REAL_SUB_RDISTRIB = prove
 387  (`!x y z. (x - y) * z = x * z - y * z`,
 388   REAL_ARITH_TAC);;
 389
 390 (* ------------------------------------------------------------------------- *)
 391 (* Theorems about "abs".                                                     *)
 392 (* ------------------------------------------------------------------------- *)
 393
 394 let REAL_ABS_ZERO = prove
 395  (`!x. (abs(x) = &0) <=> (x = &0)`,
 396   REAL_ARITH_TAC);;
 397
 398 let REAL_ABS_0 = prove
 399  (`abs(&0) = &0`,
 400   REAL_ARITH_TAC);;
 401
 402 let REAL_ABS_1 = prove
 403  (`abs(&1) = &1`,
 404   REAL_ARITH_TAC);;
 405
 406 let REAL_ABS_TRIANGLE = prove
 407  (`!x y. abs(x + y) <= abs(x) + abs(y)`,
 408   REAL_ARITH_TAC);;
 409
 410 let REAL_ABS_TRIANGLE_LE = prove
 411  (`!x y z.abs(x) + abs(y - x) <= z ==> abs(y) <= z`,
 412   REAL_ARITH_TAC);;
 413
 414 let REAL_ABS_TRIANGLE_LT = prove
 415  (`!x y z.abs(x) + abs(y - x) < z ==> abs(y) < z`,
 416   REAL_ARITH_TAC);;
 417
 418 let REAL_ABS_POS = prove
 419  (`!x. &0 <= abs(x)`,
 420   REAL_ARITH_TAC);;
 421
 422 let REAL_ABS_SUB = prove
 423  (`!x y. abs(x - y) = abs(y - x)`,
 424   REAL_ARITH_TAC);;
 425
 426 let REAL_ABS_NZ = prove
 427  (`!x. ~(x = &0) <=> &0 < abs(x)`,
 428   REAL_ARITH_TAC);;
 429
 430 let REAL_ABS_ABS = prove
 431  (`!x. abs(abs(x)) = abs(x)`,
 432   REAL_ARITH_TAC);;
 433
 434 let REAL_ABS_LE = prove
 435  (`!x. x <= abs(x)`,
 436   REAL_ARITH_TAC);;
 437
 438 let REAL_ABS_REFL = prove
 439  (`!x. (abs(x) = x) <=> &0 <= x`,
 440   REAL_ARITH_TAC);;
 441
 442 let REAL_ABS_BETWEEN = prove
 443  (`!x y d. &0 < d /\ ((x - d) < y) /\ (y < (x + d)) <=> abs(y - x) < d`,
 444   REAL_ARITH_TAC);;
 445
 446 let REAL_ABS_BOUND = prove
 447  (`!x y d. abs(x - y) < d ==> y < (x + d)`,
 448   REAL_ARITH_TAC);;
 449
 450 let REAL_ABS_STILLNZ = prove
 451  (`!x y. abs(x - y) < abs(y) ==> ~(x = &0)`,
 452   REAL_ARITH_TAC);;
 453
 454 let REAL_ABS_CASES = prove
 455  (`!x. (x = &0) \/ &0 < abs(x)`,
 456   REAL_ARITH_TAC);;
 457
 458 let REAL_ABS_BETWEEN1 = prove
 459  (`!x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z`,
 460   REAL_ARITH_TAC);;
 461
 462 let REAL_ABS_SIGN = prove
 463  (`!x y. abs(x - y) < y ==> &0 < x`,
 464   REAL_ARITH_TAC);;
 465
 466 let REAL_ABS_SIGN2 = prove
 467  (`!x y. abs(x - y) < --y ==> x < &0`,
 468   REAL_ARITH_TAC);;
 469
 470 let REAL_ABS_CIRCLE = prove
 471  (`!x y h. abs(h) < (abs(y) - abs(x)) ==> abs(x + h) < abs(y)`,
 472   REAL_ARITH_TAC);;
 473
 474 let REAL_SUB_ABS = prove
 475  (`!x y. (abs(x) - abs(y)) <= abs(x - y)`,
 476   REAL_ARITH_TAC);;
 477
 478 let REAL_ABS_SUB_ABS = prove
 479  (`!x y. abs(abs(x) - abs(y)) <= abs(x - y)`,
 480   REAL_ARITH_TAC);;
 481
 482 let REAL_ABS_BETWEEN2 = prove
 483  (`!x0 x y0 y. x0 < y0 /\ &2 * abs(x - x0) < (y0 - x0) /\
 484                           &2 * abs(y - y0) < (y0 - x0)
 485         ==> x < y`,
 486   REAL_ARITH_TAC);;
 487
 488 let REAL_ABS_BOUNDS = prove
 489  (`!x k. abs(x) <= k <=> --k <= x /\ x <= k`,
 490   REAL_ARITH_TAC);;
 491
 492 let REAL_BOUNDS_LE = prove
 493  (`!x k. --k <= x /\ x <= k <=> abs(x) <= k`,
 494   REAL_ARITH_TAC);;
 495
 496 let REAL_BOUNDS_LT = prove
 497  (`!x k. --k < x /\ x < k <=> abs(x) < k`,
 498   REAL_ARITH_TAC);;
 499
 500 (* ------------------------------------------------------------------------- *)
 501 (* Theorems about max and min.                                               *)
 502 (* ------------------------------------------------------------------------- *)
 503
 504 let REAL_MIN_MAX = prove
 505  (`!x y. min x y = --(max (--x) (--y))`,
 506   REAL_ARITH_TAC);;
 507
 508 let REAL_MAX_MIN = prove
 509  (`!x y. max x y = --(min (--x) (--y))`,
 510   REAL_ARITH_TAC);;
 511
 512 let REAL_MAX_MAX = prove
 513  (`!x y. x <= max x y /\ y <= max x y`,
 514   REAL_ARITH_TAC);;
 515
 516 let REAL_MIN_MIN = prove
 517  (`!x y. min x y <= x /\ min x y <= y`,
 518   REAL_ARITH_TAC);;
 519
 520 let REAL_MAX_SYM = prove
 521  (`!x y. max x y = max y x`,
 522   REAL_ARITH_TAC);;
 523
 524 let REAL_MIN_SYM = prove
 525  (`!x y. min x y = min y x`,
 526   REAL_ARITH_TAC);;
 527
 528 let REAL_LE_MAX = prove
 529  (`!x y z. z <= max x y <=> z <= x \/ z <= y`,
 530   REAL_ARITH_TAC);;
 531
 532 let REAL_LE_MIN = prove
 533  (`!x y z. z <= min x y <=> z <= x /\ z <= y`,
 534   REAL_ARITH_TAC);;
 535
 536 let REAL_LT_MAX = prove
 537  (`!x y z. z < max x y <=> z < x \/ z < y`,
 538   REAL_ARITH_TAC);;
 539
 540 let REAL_LT_MIN = prove
 541  (`!x y z. z < min x y <=> z < x /\ z < y`,
 542   REAL_ARITH_TAC);;
 543
 544 let REAL_MAX_LE = prove
 545  (`!x y z. max x y <= z <=> x <= z /\ y <= z`,
 546   REAL_ARITH_TAC);;
 547
 548 let REAL_MIN_LE = prove
 549  (`!x y z. min x y <= z <=> x <= z \/ y <= z`,
 550   REAL_ARITH_TAC);;
 551
 552 let REAL_MAX_LT = prove
 553  (`!x y z. max x y < z <=> x < z /\ y < z`,
 554   REAL_ARITH_TAC);;
 555
 556 let REAL_MIN_LT = prove
 557  (`!x y z. min x y < z <=> x < z \/ y < z`,
 558   REAL_ARITH_TAC);;
 559
 560 let REAL_MAX_ASSOC = prove
 561  (`!x y z. max x (max y z) = max (max x y) z`,
 562   REAL_ARITH_TAC);;
 563
 564 let REAL_MIN_ASSOC = prove
 565  (`!x y z. min x (min y z) = min (min x y) z`,
 566   REAL_ARITH_TAC);;
 567
 568 let REAL_MAX_ACI = prove
 569  (`(max x y = max y x) /\
 570    (max (max x y) z = max x (max y z)) /\
 571    (max x (max y z) = max y (max x z)) /\
 572    (max x x = x) /\
 573    (max x (max x y) = max x y)`,
 574   REAL_ARITH_TAC);;
 575
 576 let REAL_MIN_ACI = prove
 577  (`(min x y = min y x) /\
 578    (min (min x y) z = min x (min y z)) /\
 579    (min x (min y z) = min y (min x z)) /\
 580    (min x x = x) /\
 581    (min x (min x y) = min x y)`,
 582   REAL_ARITH_TAC);;
 583
 584 (* ------------------------------------------------------------------------- *)
 585 (* To simplify backchaining, just as in the natural number case.             *)
 586 (* ------------------------------------------------------------------------- *)
 587
 588 let REAL_LE_IMP =
 589   let pth = PURE_ONCE_REWRITE_RULE[IMP_CONJ] REAL_LE_TRANS in
 590   fun th -> GEN_ALL(MATCH_MP pth (SPEC_ALL th));;
 591
 592 let REAL_LET_IMP =
 593   let pth = PURE_ONCE_REWRITE_RULE[IMP_CONJ] REAL_LET_TRANS in
 594   fun th -> GEN_ALL(MATCH_MP pth (SPEC_ALL th));;
 595
 596 (* ------------------------------------------------------------------------- *)
 597 (* Now a bit of nonlinear stuff.                                             *)
 598 (* ------------------------------------------------------------------------- *)
 599
 600 let REAL_ABS_MUL = prove
 601  (`!x y. abs(x * y) = abs(x) * abs(y)`,
 602   REPEAT GEN_TAC THEN
 603   DISJ_CASES_TAC (SPEC `x:real` REAL_LE_NEGTOTAL) THENL
 604    [ALL_TAC;
 605     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_ABS_NEG]] THEN
 606   (DISJ_CASES_TAC (SPEC `y:real` REAL_LE_NEGTOTAL) THENL
 607     [ALL_TAC;
 608      GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_ABS_NEG]]) THEN
 609   ASSUM_LIST(MP_TAC o MATCH_MP REAL_LE_MUL o end_itlist CONJ o rev) THEN
 610   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN DISCH_TAC THENL
 611    [ALL_TAC;
 612     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ABS_NEG];
 613     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ABS_NEG];
 614     ALL_TAC] THEN
 615   ASM_REWRITE_TAC[real_abs; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
 616
 617 let REAL_POW_LE = prove
 618  (`!x n. &0 <= x ==> &0 <= x pow n`,
 619   REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN
 620   INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_POS] THEN
 621   MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]);;
 622
 623 let REAL_POW_LT = prove
 624  (`!x n. &0 < x ==> &0 < x pow n`,
 625   REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN
 626   INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LT_01] THEN
 627   MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);;
 628
 629 let REAL_ABS_POW = prove
 630  (`!x n. abs(x pow n) = abs(x) pow n`,
 631   GEN_TAC THEN INDUCT_TAC THEN
 632   ASM_REWRITE_TAC[real_pow; REAL_ABS_NUM; REAL_ABS_MUL]);;
 633
 634 let REAL_LE_LMUL = prove
 635  (`!x y z. &0 <= x /\ y <= z ==> x * y <= x * z`,
 636   ONCE_REWRITE_TAC[REAL_ARITH `x <= y <=> &0 <= y - x`] THEN
 637   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_SUB_RZERO; REAL_LE_MUL]);;
 638
 639 let REAL_LE_RMUL = prove
 640  (`!x y z. x <= y /\ &0 <= z ==> x * z <= y * z`,
 641   MESON_TAC[REAL_MUL_SYM; REAL_LE_LMUL]);;
 642
 643 let REAL_LT_LMUL = prove
 644  (`!x y z. &0 < x /\ y < z ==> x * y < x * z`,
 645   ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> &0 < y - x`] THEN
 646   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_SUB_RZERO; REAL_LT_MUL]);;
 647
 648 let REAL_LT_RMUL = prove
 649  (`!x y z. x < y /\ &0 < z ==> x * z < y * z`,
 650   MESON_TAC[REAL_MUL_SYM; REAL_LT_LMUL]);;
 651
 652 let REAL_EQ_MUL_LCANCEL = prove
 653  (`!x y z. (x * y = x * z) <=> (x = &0) \/ (y = z)`,
 654   REPEAT GEN_TAC THEN
 655   ONCE_REWRITE_TAC[REAL_ARITH `(x = y) <=> (x - y = &0)`] THEN
 656   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ENTIRE; REAL_SUB_RZERO]);;
 657
 658 let REAL_EQ_MUL_RCANCEL = prove
 659  (`!x y z. (x * z = y * z) <=> (x = y) \/ (z = &0)`,
 660   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 661   REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN
 662   MESON_TAC[]);;
 663
 664 let REAL_MUL_LINV_UNIQ = prove
 665  (`!x y. (x * y = &1) ==> (inv(y) = x)`,
 666   REPEAT GEN_TAC THEN
 667   ASM_CASES_TAC `y = &0` THEN
 668   ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 669   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV) THEN
 670   ASM_REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
 671   DISCH_THEN(ACCEPT_TAC o SYM));;
 672
 673 let REAL_MUL_RINV_UNIQ = prove
 674  (`!x y. (x * y = &1) ==> (inv(x) = y)`,
 675   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 676   MATCH_ACCEPT_TAC REAL_MUL_LINV_UNIQ);;
 677
 678 let REAL_INV_INV = prove
 679  (`!x. inv(inv x) = x`,
 680   GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
 681   ASM_REWRITE_TAC[REAL_INV_0] THEN
 682   MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN
 683   MATCH_MP_TAC REAL_MUL_LINV THEN
 684   ASM_REWRITE_TAC[]);;
 685
 686 let REAL_EQ_INV2 = prove
 687  (`!x y. inv(x) = inv(y) <=> x = y`,
 688   MESON_TAC[REAL_INV_INV]);;
 689
 690 let REAL_INV_EQ_0 = prove
 691  (`!x. inv(x) = &0 <=> x = &0`,
 692   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_INV_0] THEN
 693   ONCE_REWRITE_TAC[GSYM REAL_INV_INV] THEN ASM_REWRITE_TAC[REAL_INV_0]);;
 694
 695 let REAL_LT_INV = prove
 696  (`!x. &0 < x ==> &0 < inv(x)`,
 697   GEN_TAC THEN
 698   REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `inv(x)` REAL_LT_NEGTOTAL) THEN
 699   ASM_REWRITE_TAC[] THENL
 700    [RULE_ASSUM_TAC(REWRITE_RULE[REAL_INV_EQ_0]) THEN ASM_REWRITE_TAC[];
 701     DISCH_TAC THEN SUBGOAL_THEN `&0 < --(inv x) * x` MP_TAC THENL
 702      [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[];
 703       REWRITE_TAC[REAL_MUL_LNEG]]] THEN
 704   SUBGOAL_THEN `inv(x) * x = &1` SUBST1_TAC THENL
 705    [MATCH_MP_TAC REAL_MUL_LINV THEN
 706     UNDISCH_TAC `&0 < x` THEN REAL_ARITH_TAC;
 707     REWRITE_TAC[REAL_LT_RNEG; REAL_ADD_LID; REAL_OF_NUM_LT; ARITH]]);;
 708
 709 let REAL_LT_INV_EQ = prove
 710  (`!x. &0 < inv x <=> &0 < x`,
 711   GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[REAL_LT_INV] THEN
 712   GEN_REWRITE_TAC (funpow 2 RAND_CONV) [GSYM REAL_INV_INV] THEN
 713   REWRITE_TAC[REAL_LT_INV]);;
 714
 715 let REAL_INV_NEG = prove
 716  (`!x. inv(--x) = --(inv x)`,
 717   GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
 718   ASM_REWRITE_TAC[REAL_NEG_0; REAL_INV_0] THEN
 719   MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN
 720   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
 721   MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]);;
 722
 723 let REAL_LE_INV_EQ = prove
 724  (`!x. &0 <= inv x <=> &0 <= x`,
 725   REWRITE_TAC[REAL_LE_LT; REAL_LT_INV_EQ; REAL_INV_EQ_0] THEN
 726   MESON_TAC[REAL_INV_EQ_0]);;
 727
 728 let REAL_LE_INV = prove
 729  (`!x. &0 <= x ==> &0 <= inv(x)`,
 730   REWRITE_TAC[REAL_LE_INV_EQ]);;
 731
 732 let REAL_MUL_RINV = prove
 733  (`!x. ~(x = &0) ==> (x * inv(x) = &1)`,
 734   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 735   REWRITE_TAC[REAL_MUL_LINV]);;
 736
 737 let REAL_INV_1 = prove
 738  (`inv(&1) = &1`,
 739   MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN
 740   REWRITE_TAC[REAL_MUL_LID]);;
 741
 742 let REAL_INV_EQ_1 = prove
 743  (`!x. inv(x) = &1 <=> x = &1`,
 744   MESON_TAC[REAL_INV_INV; REAL_INV_1]);;
 745
 746 let REAL_DIV_1 = prove
 747  (`!x. x / &1 = x`,
 748   REWRITE_TAC[real_div; REAL_INV_1; REAL_MUL_RID]);;
 749
 750 let REAL_DIV_REFL = prove
 751  (`!x. ~(x = &0) ==> (x / x = &1)`,
 752   GEN_TAC THEN REWRITE_TAC[real_div; REAL_MUL_RINV]);;
 753
 754 let REAL_DIV_RMUL = prove
 755  (`!x y. ~(y = &0) ==> ((x / y) * y = x)`,
 756   SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID]);;
 757
 758 let REAL_DIV_LMUL = prove
 759  (`!x y. ~(y = &0) ==> (y * (x / y) = x)`,
 760   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_DIV_RMUL]);;
 761
 762 let REAL_ABS_INV = prove
 763  (`!x. abs(inv x) = inv(abs x)`,
 764   GEN_TAC THEN CONV_TAC SYM_CONV THEN
 765   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_INV_0; REAL_ABS_0] THEN
 766   MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN
 767   REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
 768   POP_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_RINV) THEN
 769   REWRITE_TAC[REAL_ABS_1]);;
 770
 771 let REAL_ABS_DIV = prove
 772  (`!x y. abs(x / y) = abs(x) / abs(y)`,
 773   REWRITE_TAC[real_div; REAL_ABS_INV; REAL_ABS_MUL]);;
 774
 775 let REAL_INV_MUL = prove
 776  (`!x y. inv(x * y) = inv(x) * inv(y)`,
 777   REPEAT GEN_TAC THEN
 778   MAP_EVERY ASM_CASES_TAC [`x = &0`; `y = &0`] THEN
 779   ASM_REWRITE_TAC[REAL_INV_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
 780   MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN
 781   ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * (c * d) = (a * c) * (b * d)`] THEN
 782   EVERY_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) THEN
 783   REWRITE_TAC[REAL_MUL_LID]);;
 784
 785 let REAL_INV_DIV = prove
 786  (`!x y. inv(x / y) = y / x`,
 787   REWRITE_TAC[real_div; REAL_INV_INV; REAL_INV_MUL] THEN
 788   MATCH_ACCEPT_TAC REAL_MUL_SYM);;
 789
 790 let REAL_POW_MUL = prove
 791  (`!x y n. (x * y) pow n = (x pow n) * (y pow n)`,
 792   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 793   ASM_REWRITE_TAC[real_pow; REAL_MUL_LID; REAL_MUL_AC]);;
 794
 795 let REAL_POW_INV = prove
 796  (`!x n. (inv x) pow n = inv(x pow n)`,
 797   GEN_TAC THEN INDUCT_TAC THEN
 798   ASM_REWRITE_TAC[real_pow; REAL_INV_1; REAL_INV_MUL]);;
 799
 800 let REAL_INV_POW = prove
 801  (`!x n. inv(x pow n) = (inv x) pow n`,
 802   REWRITE_TAC[REAL_POW_INV]);;
 803
 804 let REAL_POW_DIV = prove
 805  (`!x y n. (x / y) pow n = (x pow n) / (y pow n)`,
 806   REWRITE_TAC[real_div; REAL_POW_MUL; REAL_POW_INV]);;
 807
 808 let REAL_DIV_EQ_0 = prove
 809  (`!x y. x / y = &0 <=> x = &0 \/ y = &0`,
 810   REWRITE_TAC[real_div; REAL_INV_EQ_0; REAL_ENTIRE]);;
 811
 812 let REAL_POW_ADD = prove
 813  (`!x m n. x pow (m + n) = x pow m * x pow n`,
 814   GEN_TAC THEN INDUCT_TAC THEN
 815   ASM_REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_MUL_LID; REAL_MUL_ASSOC]);;
 816
 817 let REAL_POW_NZ = prove
 818  (`!x n. ~(x = &0) ==> ~(x pow n = &0)`,
 819   GEN_TAC THEN INDUCT_TAC THEN
 820   REWRITE_TAC[real_pow; REAL_OF_NUM_EQ; ARITH] THEN
 821   ASM_MESON_TAC[REAL_ENTIRE]);;
 822
 823 let REAL_POW_SUB = prove
 824  (`!x m n. ~(x = &0) /\ m <= n ==> (x pow (n - m) = x pow n / x pow m)`,
 825   REPEAT GEN_TAC THEN
 826   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 827   REWRITE_TAC[LE_EXISTS] THEN
 828   DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
 829   REWRITE_TAC[ADD_SUB2] THEN REWRITE_TAC[REAL_POW_ADD] THEN
 830   REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 831   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
 832   REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 833   CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_LINV THEN
 834   MATCH_MP_TAC REAL_POW_NZ THEN ASM_REWRITE_TAC[]);;
 835
 836 let REAL_LT_IMP_NZ = prove
 837  (`!x. &0 < x ==> ~(x = &0)`,
 838   REAL_ARITH_TAC);;
 839
 840 let REAL_LT_LCANCEL_IMP = prove
 841  (`!x y z. &0 < x /\ x * y < x * z ==> y < z`,
 842   REPEAT GEN_TAC THEN
 843   DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN DISCH_THEN
 844    (MP_TAC o uncurry CONJ o (MATCH_MP REAL_LT_INV F_F I) o CONJ_PAIR) THEN
 845   DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_LMUL) THEN
 846   POP_ASSUM(ASSUME_TAC o MATCH_MP REAL_MUL_LINV o MATCH_MP REAL_LT_IMP_NZ) THEN
 847   ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID]);;
 848
 849 let REAL_LT_RCANCEL_IMP = prove
 850  (`!x y z. &0 < z /\ x * z < y * z ==> x < y`,
 851   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_LT_LCANCEL_IMP]);;
 852
 853 let REAL_LE_LCANCEL_IMP = prove
 854  (`!x y z. &0 < x /\ x * y <= x * z ==> y <= z`,
 855   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT; REAL_EQ_MUL_LCANCEL] THEN
 856   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_LT_REFL] THEN
 857   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN
 858   MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
 859   EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]);;
 860
 861 let REAL_LE_RCANCEL_IMP = prove
 862  (`!x y z. &0 < z /\ x * z <= y * z ==> x <= y`,
 863   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_LE_LCANCEL_IMP]);;
 864
 865 let REAL_LE_RMUL_EQ = prove
 866  (`!x y z. &0 < z ==> (x * z <= y * z <=> x <= y)`,
 867   MESON_TAC[REAL_LE_RMUL; REAL_LE_RCANCEL_IMP; REAL_LT_IMP_LE]);;
 868
 869 let REAL_LE_LMUL_EQ = prove
 870  (`!x y z. &0 < z ==> (z * x <= z * y <=> x <= y)`,
 871   MESON_TAC[REAL_LE_RMUL_EQ; REAL_MUL_SYM]);;
 872
 873 let REAL_LT_RMUL_EQ = prove
 874  (`!x y z. &0 < z ==> (x * z < y * z <=> x < y)`,
 875   SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_RMUL_EQ]);;
 876
 877 let REAL_LT_LMUL_EQ = prove
 878  (`!x y z. &0 < z ==> (z * x < z * y <=> x < y)`,
 879   SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LMUL_EQ]);;
 880
 881 let REAL_LE_MUL_EQ = prove
 882  (`(!x y. &0 < x ==> (&0 <= x * y <=> &0 <= y)) /\
 883    (!x y. &0 < y ==> (&0 <= x * y <=> &0 <= x))`,
 884   MESON_TAC[REAL_LE_LMUL_EQ; REAL_LE_RMUL_EQ; REAL_MUL_LZERO; REAL_MUL_RZERO]);;
 885
 886 let REAL_LT_MUL_EQ = prove
 887  (`(!x y. &0 < x ==> (&0 < x * y <=> &0 < y)) /\
 888    (!x y. &0 < y ==> (&0 < x * y <=> &0 < x))`,
 889   MESON_TAC[REAL_LT_LMUL_EQ; REAL_LT_RMUL_EQ; REAL_MUL_LZERO; REAL_MUL_RZERO]);;
 890
 891 let REAL_MUL_POS_LT = prove
 892  (`!x y. &0 < x * y <=> &0 < x /\ &0 < y \/ x < &0 /\ y < &0`,
 893   REPEAT STRIP_TAC THEN
 894   STRIP_ASSUME_TAC(SPEC `x:real` REAL_LT_NEGTOTAL) THEN
 895   STRIP_ASSUME_TAC(SPEC `y:real` REAL_LT_NEGTOTAL) THEN
 896   ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL] THEN
 897   ASSUM_LIST(MP_TAC o MATCH_MP REAL_LT_MUL o end_itlist CONJ) THEN
 898   REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
 899
 900 let REAL_MUL_POS_LE = prove
 901  (`!x y. &0 <= x * y <=>
 902          x = &0 \/ y = &0 \/ &0 < x /\ &0 < y \/ x < &0 /\ y < &0`,
 903   REWRITE_TAC[REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
 904   REWRITE_TAC[REAL_MUL_POS_LT; REAL_ENTIRE] THEN REAL_ARITH_TAC);;
 905
 906 let REAL_LE_RDIV_EQ = prove
 907  (`!x y z. &0 < z ==> (x <= y / z <=> x * z <= y)`,
 908   REPEAT STRIP_TAC THEN
 909   FIRST_ASSUM(fun th ->
 910     GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)]) THEN
 911   ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV;
 912                REAL_MUL_RID; REAL_LT_IMP_NZ]);;
 913
 914 let REAL_LE_LDIV_EQ = prove
 915  (`!x y z. &0 < z ==> (x / z <= y <=> x <= y * z)`,
 916   REPEAT STRIP_TAC THEN
 917   FIRST_ASSUM(fun th ->
 918     GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)]) THEN
 919   ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV;
 920                REAL_MUL_RID; REAL_LT_IMP_NZ]);;
 921
 922 let REAL_LT_RDIV_EQ = prove
 923  (`!x y z. &0 < z ==> (x < y / z <=> x * z < y)`,
 924   SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LDIV_EQ]);;
 925
 926 let REAL_LT_LDIV_EQ = prove
 927  (`!x y z. &0 < z ==> (x / z < y <=> x < y * z)`,
 928   SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_RDIV_EQ]);;
 929
 930 let REAL_EQ_RDIV_EQ = prove
 931  (`!x y z. &0 < z ==> ((x = y / z) <=> (x * z = y))`,
 932   REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
 933   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ]);;
 934
 935 let REAL_EQ_LDIV_EQ = prove
 936  (`!x y z. &0 < z ==> ((x / z = y) <=> (x = y * z))`,
 937   REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
 938   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ]);;
 939
 940 let REAL_LT_DIV2_EQ = prove
 941  (`!x y z. &0 < z ==> (x / z < y / z <=> x < y)`,
 942   SIMP_TAC[real_div; REAL_LT_RMUL_EQ; REAL_LT_INV_EQ]);;
 943
 944 let REAL_LE_DIV2_EQ = prove
 945  (`!x y z. &0 < z ==> (x / z <= y / z <=> x <= y)`,
 946   SIMP_TAC[real_div; REAL_LE_RMUL_EQ; REAL_LT_INV_EQ]);;
 947
 948 let REAL_MUL_2 = prove
 949  (`!x. &2 * x = x + x`,
 950   REAL_ARITH_TAC);;
 951
 952 let REAL_POW_EQ_0 = prove
 953  (`!x n. (x pow n = &0) <=> (x = &0) /\ ~(n = 0)`,
 954   GEN_TAC THEN INDUCT_TAC THEN
 955   ASM_REWRITE_TAC[NOT_SUC; real_pow; REAL_ENTIRE] THENL
 956    [REAL_ARITH_TAC;
 957     CONV_TAC TAUT]);;
 958
 959 let REAL_LE_MUL2 = prove
 960  (`!w x y z. &0 <= w /\ w <= x /\ &0 <= y /\ y <= z
 961              ==> w * y <= x * z`,
 962   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 963   EXISTS_TAC `w * z` THEN CONJ_TAC THENL
 964    [MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LE_RMUL] THEN
 965   ASM_REWRITE_TAC[] THEN
 966   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `y:real` THEN
 967   ASM_REWRITE_TAC[]);;
 968
 969 let REAL_LT_MUL2 = prove
 970  (`!w x y z. &0 <= w /\ w < x /\ &0 <= y /\ y < z
 971              ==> w * y < x * z`,
 972   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 973   EXISTS_TAC `w * z` THEN CONJ_TAC THENL
 974    [MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LT_RMUL] THEN
 975   ASM_REWRITE_TAC[] THENL
 976    [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
 977     MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `y:real` THEN
 978     ASM_REWRITE_TAC[]]);;
 979
 980 let REAL_LT_SQUARE = prove
 981  (`!x. (&0 < x * x) <=> ~(x = &0)`,
 982   GEN_TAC THEN REWRITE_TAC[REAL_LT_LE; REAL_LE_SQUARE] THEN
 983   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [EQ_SYM_EQ] THEN
 984   REWRITE_TAC[REAL_ENTIRE]);;
 985
 986 let REAL_POW_1 = prove
 987  (`!x. x pow 1 = x`,
 988   REWRITE_TAC[num_CONV `1`] THEN
 989   REWRITE_TAC[real_pow; REAL_MUL_RID]);;
 990
 991 let REAL_POW_ONE = prove
 992  (`!n. &1 pow n = &1`,
 993   INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID]);;
 994
 995 let REAL_LT_INV2 = prove
 996  (`!x y. &0 < x /\ x < y ==> inv(y) < inv(x)`,
 997   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN
 998   EXISTS_TAC `x * y` THEN CONJ_TAC THENL
 999    [MATCH_MP_TAC REAL_LT_MUL THEN
1000     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC;
1001     SUBGOAL_THEN `(inv x * x = &1) /\ (inv y * y = &1)` ASSUME_TAC THENL
1002      [CONJ_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN
1003       POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC;
1004       ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID] THEN
1005       GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
1006       ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RID]]]);;
1007
1008 let REAL_LE_INV2 = prove
1009  (`!x y. &0 < x /\ x <= y ==> inv(y) <= inv(x)`,
1010   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN
1011   ASM_CASES_TAC `x:real = y` THEN ASM_REWRITE_TAC[] THEN
1012   STRIP_TAC THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_INV2 THEN
1013   ASM_REWRITE_TAC[]);;
1014
1015 let REAL_LT_LINV = prove
1016  (`!x y. &0 < y /\ inv y < x ==> inv x < y`,
1017   REPEAT STRIP_TAC THEN MP_TAC (SPEC `y:real` REAL_LT_INV) THEN
1018   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1019   MP_TAC (SPECL [`(inv y:real)`; `x:real`] REAL_LT_INV2) THEN
1020   ASM_REWRITE_TAC[REAL_INV_INV]);;
1021
1022 let REAL_LT_RINV = prove
1023  (`!x y. &0 < x /\ x < inv y ==> y < inv x`,
1024   REPEAT STRIP_TAC THEN MP_TAC (SPEC `x:real` REAL_LT_INV) THEN
1025   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1026   MP_TAC (SPECL [`x:real`; `inv y:real`] REAL_LT_INV2) THEN
1027   ASM_REWRITE_TAC[REAL_INV_INV]);;
1028
1029 let REAL_LE_LINV = prove
1030  (`!x y. &0 < y /\ inv y <= x ==> inv x <= y`,
1031   REPEAT STRIP_TAC THEN MP_TAC (SPEC `y:real` REAL_LT_INV) THEN
1032   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1033   MP_TAC (SPECL [`(inv y:real)`; `x:real`] REAL_LE_INV2) THEN
1034   ASM_REWRITE_TAC[REAL_INV_INV]);;
1035
1036 let REAL_LE_RINV = prove
1037  (`!x y. &0 < x /\ x <= inv y ==> y <= inv x`,
1038   REPEAT STRIP_TAC THEN MP_TAC (SPEC `x:real` REAL_LT_INV) THEN
1039   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1040   MP_TAC (SPECL [`x:real`; `inv y:real`] REAL_LE_INV2) THEN
1041   ASM_REWRITE_TAC[REAL_INV_INV]);;
1042
1043 let REAL_INV_LE_1 = prove
1044  (`!x. &1 <= x ==> inv(x) <= &1`,
1045   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN
1046   MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
1047
1048 let REAL_INV_1_LE = prove
1049  (`!x. &0 < x /\ x <= &1 ==> &1 <= inv(x)`,
1050   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN
1051   MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
1052
1053 let REAL_INV_LT_1 = prove
1054  (`!x. &1 < x ==> inv(x) < &1`,
1055   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN
1056   MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
1057
1058 let REAL_INV_1_LT = prove
1059  (`!x. &0 < x /\ x < &1 ==> &1 < inv(x)`,
1060   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN
1061   MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
1062
1063 let REAL_SUB_INV = prove
1064  (`!x y. ~(x = &0) /\ ~(y = &0) ==> (inv(x) - inv(y) = (y - x) / (x * y))`,
1065   REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; REAL_INV_MUL] THEN
1066   SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_LID] THEN
1067   REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN
1068   SIMP_TAC[REAL_DIV_LMUL]);;
1069
1070 let REAL_DOWN = prove
1071  (`!d. &0 < d ==> ?e. &0 < e /\ e < d`,
1072   GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `d / &2` THEN
1073   ASSUME_TAC(REAL_ARITH `&0 < &2`) THEN
1074   ASSUME_TAC(MATCH_MP REAL_MUL_LINV (REAL_ARITH `~(&2 = &0)`)) THEN
1075   CONJ_TAC THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `&2` THEN
1076   ASM_REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_RID] THEN
1077   UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);;
1078
1079 let REAL_DOWN2 = prove
1080  (`!d1 d2. &0 < d1 /\ &0 < d2 ==> ?e. &0 < e /\ e < d1 /\ e < d2`,
1081   REPEAT GEN_TAC THEN STRIP_TAC THEN
1082   DISJ_CASES_TAC(SPECL [`d1:real`; `d2:real`] REAL_LE_TOTAL) THENL
1083    [MP_TAC(SPEC `d1:real` REAL_DOWN);
1084     MP_TAC(SPEC `d2:real` REAL_DOWN)] THEN
1085   ASM_REWRITE_TAC[] THEN
1086   DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1087   EXISTS_TAC `e:real` THEN
1088   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
1089   REAL_ARITH_TAC);;
1090
1091 let REAL_POW_LE2 = prove
1092  (`!n x y. &0 <= x /\ x <= y ==> x pow n <= y pow n`,
1093   INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LE_REFL] THEN
1094   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
1095   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1096    [MATCH_MP_TAC REAL_POW_LE THEN ASM_REWRITE_TAC[];
1097     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
1098
1099 let REAL_POW_LE_1 = prove
1100  (`!n x. &1 <= x ==> &1 <= x pow n`,
1101   REPEAT STRIP_TAC THEN
1102   MP_TAC(SPECL [`n:num`; `&1`; `x:real`] REAL_POW_LE2) THEN
1103   ASM_REWRITE_TAC[REAL_POW_ONE; REAL_POS]);;
1104
1105 let REAL_POW_1_LE = prove
1106  (`!n x. &0 <= x /\ x <= &1 ==> x pow n <= &1`,
1107   REPEAT STRIP_TAC THEN
1108   MP_TAC(SPECL [`n:num`; `x:real`; `&1`] REAL_POW_LE2) THEN
1109   ASM_REWRITE_TAC[REAL_POW_ONE]);;
1110
1111 let REAL_POW_MONO = prove
1112  (`!m n x. &1 <= x /\ m <= n ==> x pow m <= x pow n`,
1113   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
1114   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1115   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
1116   REWRITE_TAC[REAL_POW_ADD] THEN
1117   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
1118   MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
1119    [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN
1120     REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
1121     MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[];
1122     MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[]]);;
1123
1124 let REAL_POW_LT2 = prove
1125  (`!n x y. ~(n = 0) /\ &0 <= x /\ x < y ==> x pow n < y pow n`,
1126   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; real_pow] THEN REPEAT STRIP_TAC THEN
1127   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
1128   MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1129    [MATCH_MP_TAC REAL_POW_LE THEN ASM_REWRITE_TAC[];
1130     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
1131
1132 let REAL_POW_LT_1 = prove
1133  (`!n x. ~(n = 0) /\ &1 < x ==> &1 < x pow n`,
1134   REPEAT STRIP_TAC THEN
1135   MP_TAC(SPECL [`n:num`; `&1`; `x:real`] REAL_POW_LT2) THEN
1136   ASM_REWRITE_TAC[REAL_POW_ONE; REAL_POS]);;
1137
1138 let REAL_POW_1_LT = prove
1139  (`!n x. ~(n = 0) /\ &0 <= x /\ x < &1 ==> x pow n < &1`,
1140   REPEAT STRIP_TAC THEN
1141   MP_TAC(SPECL [`n:num`; `x:real`; `&1`] REAL_POW_LT2) THEN
1142   ASM_REWRITE_TAC[REAL_POW_ONE]);;
1143
1144 let REAL_POW_MONO_LT = prove
1145  (`!m n x. &1 < x /\ m < n ==> x pow m < x pow n`,
1146   REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS] THEN
1147   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1148   DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN
1149   REWRITE_TAC[REAL_POW_ADD] THEN
1150   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
1151   MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
1152    [MATCH_MP_TAC REAL_POW_LT THEN
1153     MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `&1` THEN
1154     ASM_REWRITE_TAC[REAL_OF_NUM_LT; ARITH];
1155     SPEC_TAC(`d:num`,`d:num`) THEN
1156     INDUCT_TAC THEN ONCE_REWRITE_TAC[real_pow] THENL
1157      [ASM_REWRITE_TAC[real_pow; REAL_MUL_RID]; ALL_TAC] THEN
1158     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
1159     MATCH_MP_TAC REAL_LT_MUL2 THEN
1160     ASM_REWRITE_TAC[REAL_OF_NUM_LE; ARITH]]);;
1161
1162 let REAL_POW_POW = prove
1163  (`!x m n. (x pow m) pow n = x pow (m * n)`,
1164   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1165   ASM_REWRITE_TAC[real_pow; MULT_CLAUSES; REAL_POW_ADD]);;
1166
1167 let REAL_EQ_RCANCEL_IMP = prove
1168  (`!x y z. ~(z = &0) /\ (x * z = y * z) ==> (x = y)`,
1169   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
1170   REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_SUB_RDISTRIB; REAL_ENTIRE] THEN
1171   CONV_TAC TAUT);;
1172
1173 let REAL_EQ_LCANCEL_IMP = prove
1174  (`!x y z. ~(z = &0) /\ (z * x = z * y) ==> (x = y)`,
1175   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_EQ_RCANCEL_IMP);;
1176
1177 let REAL_LT_DIV = prove
1178  (`!x y. &0 < x /\ &0 < y ==> &0 < x / y`,
1179   SIMP_TAC[REAL_LT_MUL; REAL_LT_INV_EQ; real_div]);;
1180
1181 let REAL_LE_DIV = prove
1182  (`!x y. &0 <= x /\ &0 <= y ==> &0 <= x / y`,
1183   SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; real_div]);;
1184
1185 let REAL_DIV_POW2 = prove
1186  (`!x m n. ~(x = &0)
1187            ==> (x pow m / x pow n = if n <= m then x pow (m - n)
1188                                     else inv(x pow (n - m)))`,
1189   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1190   ASM_SIMP_TAC[REAL_POW_SUB] THEN
1191   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN
1192   AP_TERM_TAC THEN REWRITE_TAC[REAL_INV_DIV] THEN
1193   UNDISCH_TAC `~(n:num <= m)` THEN REWRITE_TAC[NOT_LE] THEN
1194   DISCH_THEN(MP_TAC o MATCH_MP LT_IMP_LE) THEN
1195   ASM_SIMP_TAC[REAL_POW_SUB]);;
1196
1197 let REAL_DIV_POW2_ALT = prove
1198  (`!x m n. ~(x = &0)
1199            ==> (x pow m / x pow n = if n < m then x pow (m - n)
1200                                     else inv(x pow (n - m)))`,
1201   REPEAT STRIP_TAC THEN
1202   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN
1203   ONCE_REWRITE_TAC[REAL_INV_DIV] THEN
1204   ASM_SIMP_TAC[GSYM NOT_LE; REAL_DIV_POW2] THEN
1205   ASM_CASES_TAC `m <= n:num` THEN
1206   ASM_REWRITE_TAC[REAL_INV_INV]);;
1207
1208 let REAL_LT_POW2 = prove
1209  (`!n. &0 < &2 pow n`,
1210   SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH]);;
1211
1212 let REAL_LE_POW2 = prove
1213  (`!n. &1 <= &2 pow n`,
1214   GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow 0` THEN
1215   SIMP_TAC[REAL_POW_MONO; LE_0; REAL_OF_NUM_LE; ARITH] THEN
1216   REWRITE_TAC[real_pow; REAL_LE_REFL]);;
1217
1218 let REAL_POW2_ABS = prove
1219  (`!x. abs(x) pow 2 = x pow 2`,
1220   GEN_TAC THEN REWRITE_TAC[real_abs] THEN
1221   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_NEG; ARITH_EVEN]);;
1222
1223 let REAL_LE_SQUARE_ABS = prove
1224  (`!x y. abs(x) <= abs(y) <=> x pow 2 <= y pow 2`,
1225   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
1226   MESON_TAC[REAL_POW_LE2; REAL_ABS_POS; NUM_EQ_CONV `2 = 0`;
1227             REAL_POW_LT2; REAL_NOT_LE]);;
1228
1229 let REAL_LT_SQUARE_ABS = prove
1230  (`!x y. abs(x) < abs(y) <=> x pow 2 < y pow 2`,
1231   REWRITE_TAC[GSYM REAL_NOT_LE; REAL_LE_SQUARE_ABS]);;
1232
1233 let REAL_EQ_SQUARE_ABS = prove
1234  (`!x y. abs x = abs y <=> x pow 2 = y pow 2`,
1235   REWRITE_TAC[GSYM REAL_LE_ANTISYM; REAL_LE_SQUARE_ABS]);;
1236
1237 let REAL_LE_POW_2 = prove
1238  (`!x. &0 <= x pow 2`,
1239   REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
1240
1241 let REAL_LT_POW_2 = prove
1242  (`!x. &0 < x pow 2 <=> ~(x = &0)`,
1243   REWRITE_TAC[REAL_LE_POW_2; REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
1244   REWRITE_TAC[REAL_POW_EQ_0; ARITH]);;
1245
1246 let REAL_SOS_EQ_0 = prove
1247  (`!x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0`,
1248   REPEAT GEN_TAC THEN EQ_TAC THEN
1249   SIMP_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_LID] THEN
1250   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
1251    `x + y = &0 ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
1252   REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]);;
1253
1254 let REAL_POW_ZERO = prove
1255  (`!n. &0 pow n = if n = 0 then &1 else &0`,
1256   INDUCT_TAC THEN REWRITE_TAC[real_pow; NOT_SUC; REAL_MUL_LZERO]);;
1257
1258 let REAL_POW_MONO_INV = prove
1259  (`!m n x. &0 <= x /\ x <= &1 /\ n <= m ==> x pow m <= x pow n`,
1260   REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = &0` THENL
1261    [ASM_REWRITE_TAC[REAL_POW_ZERO] THEN
1262     REPEAT(COND_CASES_TAC THEN REWRITE_TAC[REAL_POS; REAL_LE_REFL]) THEN
1263     UNDISCH_TAC `n:num <= m` THEN ASM_REWRITE_TAC[LE];
1264     GEN_REWRITE_TAC BINOP_CONV [GSYM REAL_INV_INV] THEN
1265     MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[GSYM REAL_POW_INV] THEN
1266     CONJ_TAC THENL
1267      [MATCH_MP_TAC REAL_POW_LT THEN REWRITE_TAC[REAL_LT_INV_EQ];
1268       MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[] THEN
1269       MATCH_MP_TAC REAL_INV_1_LE] THEN
1270     ASM_REWRITE_TAC[REAL_LT_LE]]);;
1271
1272 let REAL_POW_LE2_REV = prove
1273  (`!n x y. ~(n = 0) /\ &0 <= y /\ x pow n <= y pow n ==> x <= y`,
1274   MESON_TAC[REAL_POW_LT2; REAL_NOT_LE]);;
1275
1276 let REAL_POW_LT2_REV = prove
1277  (`!n x y. &0 <= y /\ x pow n < y pow n ==> x < y`,
1278   MESON_TAC[REAL_POW_LE2; REAL_NOT_LE]);;
1279
1280 let REAL_POW_EQ = prove
1281  (`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y /\ x pow n = y pow n ==> x = y`,
1282   REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN MESON_TAC[REAL_POW_LE2_REV]);;
1283
1284 let REAL_POW_EQ_ABS = prove
1285  (`!n x y. ~(n = 0) /\ x pow n = y pow n ==> abs x = abs y`,
1286   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `n:num` THEN
1287   ASM_REWRITE_TAC[REAL_ABS_POS; GSYM REAL_ABS_POW]);;
1288
1289 let REAL_POW_EQ_1_IMP = prove
1290  (`!x n. ~(n = 0) /\ x pow n = &1 ==> abs(x) = &1`,
1291   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_ABS_NUM] THEN
1292   MATCH_MP_TAC REAL_POW_EQ_ABS THEN EXISTS_TAC `n:num` THEN
1293   ASM_REWRITE_TAC[REAL_POW_ONE]);;
1294
1295 let REAL_POW_EQ_1 = prove
1296  (`!x n. x pow n = &1 <=> abs(x) = &1 /\ (x < &0 ==> EVEN(n)) \/ n = 0`,
1297   REPEAT GEN_TAC THEN
1298   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[real_pow] THEN
1299   ASM_CASES_TAC `abs(x) = &1` THENL
1300    [ALL_TAC; ASM_MESON_TAC[REAL_POW_EQ_1_IMP]] THEN
1301   ASM_REWRITE_TAC[] THEN
1302   FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (REAL_ARITH
1303    `abs x = a ==> x = a \/ x = --a`)) THEN
1304   ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE] THEN
1305   REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
1306
1307 let REAL_POW_LT2_ODD = prove
1308  (`!n x y. x < y /\ ODD n ==> x pow n < y pow n`,
1309   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1310   ASM_REWRITE_TAC[ARITH] THEN STRIP_TAC THEN
1311   DISJ_CASES_TAC(SPEC `y:real` REAL_LE_NEGTOTAL) THENL
1312    [DISJ_CASES_TAC(REAL_ARITH `&0 <= x \/ &0 < --x`) THEN
1313     ASM_SIMP_TAC[REAL_POW_LT2] THEN
1314     SUBGOAL_THEN `&0 < --x pow n /\ &0 <= y pow n` MP_TAC THENL
1315      [ASM_SIMP_TAC[REAL_POW_LE; REAL_POW_LT];
1316       ASM_REWRITE_TAC[REAL_POW_NEG; GSYM NOT_ODD] THEN REAL_ARITH_TAC];
1317     SUBGOAL_THEN `--y pow n < --x pow n` MP_TAC THENL
1318      [MATCH_MP_TAC REAL_POW_LT2 THEN ASM_REWRITE_TAC[];
1319       ASM_REWRITE_TAC[REAL_POW_NEG; GSYM NOT_ODD]] THEN
1320     REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
1321
1322 let REAL_POW_LE2_ODD = prove
1323  (`!n x y. x <= y /\ ODD n ==> x pow n <= y pow n`,
1324   REWRITE_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC THEN
1325   ASM_SIMP_TAC[REAL_POW_LT2_ODD]);;
1326
1327 let REAL_POW_LT2_ODD_EQ = prove
1328  (`!n x y. ODD n ==> (x pow n < y pow n <=> x < y)`,
1329   MESON_TAC[REAL_POW_LT2_ODD; REAL_POW_LE2_ODD; REAL_NOT_LE]);;
1330
1331 let REAL_POW_LE2_ODD_EQ = prove
1332  (`!n x y. ODD n ==> (x pow n <= y pow n <=> x <= y)`,
1333   MESON_TAC[REAL_POW_LT2_ODD; REAL_POW_LE2_ODD; REAL_NOT_LE]);;
1334
1335 let REAL_POW_EQ_ODD_EQ = prove
1336  (`!n x y. ODD n ==> (x pow n = y pow n <=> x = y)`,
1337   SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_POW_LE2_ODD_EQ]);;
1338
1339 let REAL_POW_EQ_ODD = prove
1340  (`!n x y. ODD n /\ x pow n = y pow n ==> x = y`,
1341   MESON_TAC[REAL_POW_EQ_ODD_EQ]);;
1342
1343 let REAL_POW_EQ_EQ = prove
1344  (`!n x y. x pow n = y pow n <=>
1345            if EVEN n then n = 0 \/ abs x = abs y else x = y`,
1346   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1347   ASM_REWRITE_TAC[real_pow; ARITH] THEN COND_CASES_TAC THEN
1348   ASM_SIMP_TAC[REAL_POW_EQ_ODD_EQ; GSYM NOT_EVEN] THEN
1349   EQ_TAC THENL [ASM_MESON_TAC[REAL_POW_EQ_ABS]; ALL_TAC] THEN
1350   REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN DISCH_TAC THEN
1351   FIRST_X_ASSUM(X_CHOOSE_THEN `m:num` SUBST1_TAC o
1352     REWRITE_RULE[EVEN_EXISTS]) THEN ASM_REWRITE_TAC[GSYM REAL_POW_POW]);;
1353
1354 (* ------------------------------------------------------------------------- *)
1355 (* Some basic forms of the Archimedian property.                             *)
1356 (* ------------------------------------------------------------------------- *)
1357
1358 let REAL_ARCH_SIMPLE = prove
1359  (`!x. ?n. x <= &n`,
1360   let lemma = prove(`(!x. (?n. x = &n) ==> P x) <=> !n. P(&n)`,MESON_TAC[]) in
1361   MP_TAC(SPEC `\y. ?n. y = &n` REAL_COMPLETE) THEN REWRITE_TAC[lemma] THEN
1362   MESON_TAC[REAL_LE_SUB_LADD; REAL_OF_NUM_ADD; REAL_LE_TOTAL;
1363             REAL_ARITH `~(M <= M - &1)`]);;
1364
1365 let REAL_ARCH_LT = prove
1366  (`!x. ?n. x < &n`,
1367   MESON_TAC[REAL_ARCH_SIMPLE; REAL_OF_NUM_ADD;
1368             REAL_ARITH `x <= n ==> x < n + &1`]);;
1369
1370 let REAL_ARCH = prove
1371  (`!x. &0 < x ==> !y. ?n. y < &n * x`,
1372   MESON_TAC[REAL_ARCH_LT; REAL_LT_LDIV_EQ]);;
1373
1374 (* ------------------------------------------------------------------------- *)
1375 (* The sign of a real number, as a real number.                              *)
1376 (* ------------------------------------------------------------------------- *)
1377
1378 let real_sgn = new_definition
1379  `(real_sgn:real->real) x =
1380         if &0 < x then &1 else if x < &0 then -- &1 else &0`;;
1381
1382 let REAL_SGN_0 = prove
1383  (`real_sgn(&0) = &0`,
1384   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1385
1386 let REAL_SGN_NEG = prove
1387  (`!x. real_sgn(--x) = --(real_sgn x)`,
1388   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1389
1390 let REAL_SGN_ABS = prove
1391  (`!x. real_sgn(x) * abs(x) = x`,
1392   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1393
1394 let REAL_EQ_SGN_ABS = prove
1395  (`!x y:real. x = y <=> real_sgn x = real_sgn y /\ abs x = abs y`,
1396   MESON_TAC[REAL_SGN_ABS]);;
1397
1398 let REAL_ABS_SGN = prove
1399  (`!x. abs(real_sgn x) = real_sgn(abs x)`,
1400   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1401
1402 let REAL_SGN = prove
1403  (`!x. real_sgn x = x / abs x`,
1404   GEN_TAC THEN ASM_CASES_TAC `x = &0` THENL
1405    [ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_SGN_0];
1406     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_SGN_ABS] THEN
1407     ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_ABS_ZERO;
1408                  REAL_MUL_RINV; REAL_MUL_RID]]);;
1409
1410 let REAL_SGN_MUL = prove
1411  (`!x y. real_sgn(x * y) = real_sgn(x) * real_sgn(y)`,
1412   REWRITE_TAC[REAL_SGN; REAL_ABS_MUL; real_div; REAL_INV_MUL] THEN
1413   REAL_ARITH_TAC);;
1414
1415 let REAL_SGN_INV = prove
1416  (`!x. real_sgn(inv x) = real_sgn x`,
1417   REWRITE_TAC[real_sgn; REAL_LT_INV_EQ; GSYM REAL_INV_NEG;
1418               REAL_ARITH `x < &0 <=> &0 < --x`]);;
1419
1420 let REAL_SGN_DIV = prove
1421  (`!x y. real_sgn(x / y) = real_sgn(x) / real_sgn(y)`,
1422   REWRITE_TAC[REAL_SGN; REAL_ABS_DIV] THEN
1423   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV] THEN
1424   REAL_ARITH_TAC);;
1425
1426 let REAL_SGN_EQ = prove
1427  (`(!x. real_sgn x = &0 <=> x = &0) /\
1428    (!x. real_sgn x = &1 <=> x > &0) /\
1429    (!x. real_sgn x = -- &1 <=> x < &0)`,
1430   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1431
1432 let REAL_SGN_CASES = prove
1433  (`!x. real_sgn x = &0 \/ real_sgn x = &1 \/ real_sgn x = -- &1`,
1434   REWRITE_TAC[real_sgn] THEN MESON_TAC[]);;
1435
1436 let REAL_SGN_INEQS = prove
1437  (`(!x. &0 <= real_sgn x <=> &0 <= x) /\
1438    (!x. &0 < real_sgn x <=> &0 < x) /\
1439    (!x. &0 >= real_sgn x <=> &0 >= x) /\
1440    (!x. &0 > real_sgn x <=> &0 > x) /\
1441    (!x. &0 = real_sgn x <=> &0 = x) /\
1442    (!x. real_sgn x <= &0 <=> x <= &0) /\
1443    (!x. real_sgn x < &0 <=> x < &0) /\
1444    (!x. real_sgn x >= &0 <=> x >= &0) /\
1445    (!x. real_sgn x > &0 <=> x > &0) /\
1446    (!x. real_sgn x = &0 <=> x = &0)`,
1447   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1448
1449 let REAL_SGN_POW = prove
1450  (`!x n. real_sgn(x pow n) = real_sgn(x) pow n`,
1451   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_SGN_MUL; real_pow] THEN
1452   REWRITE_TAC[real_sgn; REAL_LT_01]);;
1453
1454 let REAL_SGN_POW_2 = prove
1455  (`!x. real_sgn(x pow 2) = real_sgn(abs x)`,
1456   REWRITE_TAC[real_sgn] THEN
1457   SIMP_TAC[GSYM REAL_NOT_LE; REAL_ABS_POS; REAL_LE_POW_2;
1458            REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN
1459   REWRITE_TAC[REAL_POW_EQ_0; REAL_ABS_ZERO; ARITH]);;
1460
1461 let REAL_SGN_REAL_SGN = prove
1462  (`!x. real_sgn(real_sgn x) = real_sgn x`,
1463   REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
1464
1465 let REAL_INV_SGN = prove
1466  (`!x. real_inv(real_sgn x) = real_sgn x`,
1467   GEN_TAC THEN REWRITE_TAC[real_sgn] THEN
1468   REPEAT COND_CASES_TAC THEN
1469   REWRITE_TAC[REAL_INV_0; REAL_INV_1; REAL_INV_NEG]);;
1470
1471 (* ------------------------------------------------------------------------- *)
1472 (* Useful "without loss of generality" lemmas.                               *)
1473 (* ------------------------------------------------------------------------- *)
1474
1475 let REAL_WLOG_LE = prove
1476  (`(!x y. P x y <=> P y x) /\ (!x y. x <= y ==> P x y) ==> !x y. P x y`,
1477   MESON_TAC[REAL_LE_TOTAL]);;
1478
1479 let REAL_WLOG_LT = prove
1480  (`(!x. P x x) /\ (!x y. P x y <=> P y x) /\ (!x y. x < y ==> P x y)
1481    ==> !x y. P x y`,
1482   MESON_TAC[REAL_LT_TOTAL]);;