Library/floor.ml

   1 (* ========================================================================= *)
   2 (* The integer/rational-valued reals, and the "floor" and "frac" functions.  *)
   3 (* ========================================================================= *)
   4
   5 prioritize_real();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Closure theorems and other lemmas for the integer-valued reals.           *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let INTEGER_CASES = prove
  12  (`integer x <=> (?n. x = &n) \/ (?n. x = -- &n)`,
  13   REWRITE_TAC[is_int; OR_EXISTS_THM]);;
  14
  15 let REAL_ABS_INTEGER_LEMMA = prove
  16  (`!x. integer(x) /\ ~(x = &0) ==> &1 <= abs(x)`,
  17   GEN_TAC THEN REWRITE_TAC[integer] THEN
  18   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  19   ONCE_REWRITE_TAC[REAL_ARITH `(x = &0) <=> (abs(x) = &0)`] THEN
  20   POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN
  21   REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_LE] THEN ARITH_TAC);;
  22
  23 let INTEGER_CLOSED = prove
  24  (`(!n. integer(&n)) /\
  25    (!x y. integer(x) /\ integer(y) ==> integer(x + y)) /\
  26    (!x y. integer(x) /\ integer(y) ==> integer(x - y)) /\
  27    (!x y. integer(x) /\ integer(y) ==> integer(x * y)) /\
  28    (!x r. integer(x) ==> integer(x pow r)) /\
  29    (!x. integer(x) ==> integer(--x)) /\
  30    (!x. integer(x) ==> integer(abs x))`,
  31   REWRITE_TAC[integer] THEN
  32   MATCH_MP_TAC(TAUT
  33    `x /\ c /\ d /\ e /\ f /\ (a /\ e ==> b) /\ a
  34     ==> x /\ a /\ b /\ c /\ d /\ e /\ f`) THEN
  35   REPEAT CONJ_TAC THENL
  36    [REWRITE_TAC[REAL_ABS_NUM] THEN MESON_TAC[];
  37     REWRITE_TAC[REAL_ABS_MUL] THEN MESON_TAC[REAL_OF_NUM_MUL];
  38     REWRITE_TAC[REAL_ABS_POW] THEN MESON_TAC[REAL_OF_NUM_POW];
  39     REWRITE_TAC[REAL_ABS_NEG]; REWRITE_TAC[REAL_ABS_ABS];
  40     REWRITE_TAC[real_sub] THEN MESON_TAC[]; ALL_TAC] THEN
  41   SIMP_TAC[REAL_ARITH `&0 <= a ==> ((abs(x) = a) <=> (x = a) \/ (x = --a))`;
  42            REAL_POS] THEN
  43   REPEAT STRIP_TAC THEN
  44   ASM_REWRITE_TAC[GSYM REAL_NEG_ADD; REAL_OF_NUM_ADD] THENL
  45    [MESON_TAC[]; ALL_TAC; ALL_TAC; MESON_TAC[]] THEN
  46   REWRITE_TAC[REAL_ARITH `(--a + b = c) <=> (a + c = b)`;
  47               REAL_ARITH `(a + --b = c) <=> (b + c = a)`] THEN
  48   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
  49   MESON_TAC[LE_EXISTS; ADD_SYM; LE_CASES]);;
  50
  51 let INTEGER_ADD = prove
  52  (`!x y. integer(x) /\ integer(y) ==> integer(x + y)`,
  53   REWRITE_TAC[INTEGER_CLOSED]);;
  54
  55 let INTEGER_SUB = prove
  56  (`!x y. integer(x) /\ integer(y) ==> integer(x - y)`,
  57   REWRITE_TAC[INTEGER_CLOSED]);;
  58
  59 let INTEGER_MUL = prove
  60  (`!x y. integer(x) /\ integer(y) ==> integer(x * y)`,
  61   REWRITE_TAC[INTEGER_CLOSED]);;
  62
  63 let INTEGER_POW = prove
  64  (`!x n. integer(x) ==> integer(x pow n)`,
  65   REWRITE_TAC[INTEGER_CLOSED]);;
  66
  67 let REAL_LE_INTEGERS = prove
  68  (`!x y. integer(x) /\ integer(y) ==> (x <= y <=> (x = y) \/ x + &1 <= y)`,
  69   REPEAT STRIP_TAC THEN
  70   MP_TAC(SPEC `y - x` REAL_ABS_INTEGER_LEMMA) THEN
  71   ASM_SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
  72
  73 let REAL_LE_CASES_INTEGERS = prove
  74  (`!x y. integer(x) /\ integer(y) ==> x <= y \/ y + &1 <= x`,
  75   REPEAT STRIP_TAC THEN
  76   MP_TAC(SPEC `y - x` REAL_ABS_INTEGER_LEMMA) THEN
  77   ASM_SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
  78
  79 let REAL_LE_REVERSE_INTEGERS = prove
  80  (`!x y. integer(x) /\ integer(y) /\ ~(y + &1 <= x) ==> x <= y`,
  81   MESON_TAC[REAL_LE_CASES_INTEGERS]);;
  82
  83 let REAL_LT_INTEGERS = prove
  84  (`!x y. integer(x) /\ integer(y) ==> (x < y <=> x + &1 <= y)`,
  85   MESON_TAC[REAL_NOT_LT; REAL_LE_CASES_INTEGERS;
  86             REAL_ARITH `x + &1 <= y ==> x < y`]);;
  87
  88 let REAL_EQ_INTEGERS = prove
  89  (`!x y. integer x /\ integer y ==> (x = y <=> abs(x - y) < &1)`,
  90   REWRITE_TAC[REAL_ARITH `x = y <=> ~(x < y \/ y < x)`] THEN
  91   SIMP_TAC[REAL_LT_INTEGERS] THEN REAL_ARITH_TAC);;
  92
  93 let REAL_EQ_INTEGERS_IMP = prove
  94  (`!x y. integer x /\ integer y /\ abs(x - y) < &1 ==> x = y`,
  95   SIMP_TAC[REAL_EQ_INTEGERS]);;
  96
  97 let INTEGER_NEG = prove
  98  (`!x. integer(--x) <=> integer(x)`,
  99   MESON_TAC[INTEGER_CLOSED; REAL_NEG_NEG]);;
 100
 101 let INTEGER_ABS = prove
 102  (`!x. integer(abs x) <=> integer(x)`,
 103   GEN_TAC THEN REWRITE_TAC[real_abs] THEN COND_CASES_TAC THEN
 104   REWRITE_TAC[INTEGER_NEG]);;
 105
 106 let INTEGER_POS = prove
 107  (`!x. &0 <= x ==> (integer(x) <=> ?n. x = &n)`,
 108   SIMP_TAC[integer; real_abs]);;
 109
 110 let INTEGER_ADD_EQ = prove
 111  (`(!x y. integer(x) ==> (integer(x + y) <=> integer(y))) /\
 112    (!x y. integer(y) ==> (integer(x + y) <=> integer(x)))`,
 113   MESON_TAC[REAL_ADD_SUB; REAL_ADD_SYM; INTEGER_CLOSED]);;
 114
 115 let INTEGER_SUB_EQ = prove
 116  (`(!x y. integer(x) ==> (integer(x - y) <=> integer(y))) /\
 117    (!x y. integer(y) ==> (integer(x - y) <=> integer(x)))`,
 118   MESON_TAC[REAL_SUB_ADD; REAL_NEG_SUB; INTEGER_CLOSED]);;
 119
 120 let FORALL_INTEGER = prove
 121  (`!P. (!n. P(&n)) /\ (!x. P x ==> P(--x)) ==> !x. integer x ==> P x`,
 122   MESON_TAC[INTEGER_CASES]);;
 123
 124 let INTEGER_SUM = prove
 125  (`!f:A->real s. (!x. x IN s ==> integer(f x)) ==> integer(sum s f)`,
 126   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_CLOSED THEN
 127   ASM_REWRITE_TAC[INTEGER_CLOSED]);;
 128
 129 let INTEGER_ABS_MUL_EQ_1 = prove
 130  (`!x y. integer x /\ integer y
 131          ==> (abs(x * y) = &1 <=> abs x = &1 /\ abs y = &1)`,
 132   REWRITE_TAC[integer] THEN
 133   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ABS_MUL] THEN
 134   REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_MUL; MULT_EQ_1]);;
 135
 136 let INTEGER_DIV = prove
 137  (`!m n. integer(&m / &n) <=> n = 0 \/ n divides m`,
 138   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 139    [ASM_REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO; INTEGER_CLOSED];
 140     ASM_SIMP_TAC[INTEGER_POS; REAL_POS; REAL_LE_DIV; divides] THEN
 141     ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
 142      `~(n = &0) ==> (x / n = y <=> x = n * y)`] THEN
 143     REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ]]);;
 144
 145 (* ------------------------------------------------------------------------- *)
 146 (* Similar theorems for rational-valued reals.                               *)
 147 (* ------------------------------------------------------------------------- *)
 148
 149 let rational = new_definition
 150  `rational x <=> ?m n. integer m /\ integer n /\ ~(n = &0) /\ x = m / n`;;
 151
 152 let RATIONAL_INTEGER = prove
 153  (`!x. integer x ==> rational x`,
 154   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[rational] THEN
 155   MAP_EVERY EXISTS_TAC [`x:real`; `&1`] THEN
 156   ASM_SIMP_TAC[INTEGER_CLOSED] THEN CONV_TAC REAL_FIELD);;
 157
 158 let RATIONAL_NUM = prove
 159  (`!n. rational(&n)`,
 160   SIMP_TAC[RATIONAL_INTEGER; INTEGER_CLOSED]);;
 161
 162 let RATIONAL_NEG = prove
 163  (`!x. rational(x) ==> rational(--x)`,
 164   REWRITE_TAC[rational; LEFT_IMP_EXISTS_THM] THEN
 165   MAP_EVERY X_GEN_TAC [`x:real`; `m:real`; `n:real`] THEN
 166   STRIP_TAC THEN
 167   MAP_EVERY EXISTS_TAC [`--m:real`; `n:real`] THEN
 168   ASM_SIMP_TAC[INTEGER_CLOSED] THEN CONV_TAC REAL_FIELD);;
 169
 170 let RATIONAL_ABS = prove
 171  (`!x. rational(x) ==> rational(abs x)`,
 172   REWRITE_TAC[real_abs] THEN MESON_TAC[RATIONAL_NEG]);;
 173
 174 let RATIONAL_INV = prove
 175  (`!x. rational(x) ==> rational(inv x)`,
 176   GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
 177   ASM_SIMP_TAC[REAL_INV_0; RATIONAL_NUM] THEN
 178   REWRITE_TAC[rational; LEFT_IMP_EXISTS_THM] THEN
 179   MAP_EVERY X_GEN_TAC [`m:real`; `n:real`] THEN STRIP_TAC THEN
 180   MAP_EVERY EXISTS_TAC [`n:real`; `m:real`] THEN
 181   ASM_SIMP_TAC[INTEGER_CLOSED] THEN
 182   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
 183
 184 let RATIONAL_ADD = prove
 185  (`!x y. rational(x) /\ rational(y) ==> rational(x + y)`,
 186   REPEAT GEN_TAC THEN REWRITE_TAC[rational; LEFT_AND_EXISTS_THM] THEN
 187   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 188   MAP_EVERY X_GEN_TAC [`m1:real`; `n1:real`; `m2:real`; `n2:real`] THEN
 189   STRIP_TAC THEN
 190   MAP_EVERY EXISTS_TAC [`m1 * n2 + m2 * n1:real`; `n1 * n2:real`] THEN
 191   ASM_SIMP_TAC[INTEGER_CLOSED] THEN
 192   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
 193
 194 let RATIONAL_SUB = prove
 195  (`!x y. rational(x) /\ rational(y) ==> rational(x - y)`,
 196   SIMP_TAC[real_sub; RATIONAL_NEG; RATIONAL_ADD]);;
 197
 198 let RATIONAL_MUL = prove
 199  (`!x y. rational(x) /\ rational(y) ==> rational(x * y)`,
 200   REPEAT GEN_TAC THEN REWRITE_TAC[rational; LEFT_AND_EXISTS_THM] THEN
 201   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 202   MAP_EVERY X_GEN_TAC [`m1:real`; `n1:real`; `m2:real`; `n2:real`] THEN
 203   STRIP_TAC THEN
 204   MAP_EVERY EXISTS_TAC [`m1 * m2:real`; `n1 * n2:real`] THEN
 205   ASM_SIMP_TAC[INTEGER_CLOSED] THEN
 206   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
 207
 208 let RATIONAL_DIV = prove
 209  (`!x y. rational(x) /\ rational(y) ==> rational(x / y)`,
 210   SIMP_TAC[real_div; RATIONAL_INV; RATIONAL_MUL]);;
 211
 212 let RATIONAL_POW = prove
 213  (`!x n. rational(x) ==> rational(x pow n)`,
 214   GEN_TAC THEN INDUCT_TAC THEN
 215   ASM_SIMP_TAC[real_pow; RATIONAL_NUM; RATIONAL_MUL]);;
 216
 217 let RATIONAL_CLOSED = prove
 218  (`(!n. rational(&n)) /\
 219    (!x. integer x ==> rational x) /\
 220    (!x y. rational(x) /\ rational(y) ==> rational(x + y)) /\
 221    (!x y. rational(x) /\ rational(y) ==> rational(x - y)) /\
 222    (!x y. rational(x) /\ rational(y) ==> rational(x * y)) /\
 223    (!x y. rational(x) /\ rational(y) ==> rational(x / y)) /\
 224    (!x r. rational(x) ==> rational(x pow r)) /\
 225    (!x. rational(x) ==> rational(--x)) /\
 226    (!x. rational(x) ==> rational(inv x)) /\
 227    (!x. rational(x) ==> rational(abs x))`,
 228   SIMP_TAC[RATIONAL_NUM; RATIONAL_NEG; RATIONAL_ABS; RATIONAL_INV;
 229            RATIONAL_ADD; RATIONAL_SUB; RATIONAL_MUL; RATIONAL_DIV;
 230            RATIONAL_POW; RATIONAL_INTEGER]);;
 231
 232 let RATIONAL_NEG_EQ = prove
 233  (`!x. rational(--x) <=> rational x`,
 234   MESON_TAC[REAL_NEG_NEG; RATIONAL_NEG]);;
 235
 236 let RATIONAL_INV_EQ = prove
 237  (`!x. rational(inv x) <=> rational x`,
 238   MESON_TAC[REAL_INV_INV; RATIONAL_INV]);;
 239
 240 let RATIONAL_ALT = prove
 241  (`!x. rational(x) <=> ?p q. ~(q = 0) /\ abs x = &p / &q`,
 242   GEN_TAC THEN REWRITE_TAC[rational] THEN EQ_TAC THENL
 243    [REWRITE_TAC[integer] THEN STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ABS_DIV] THEN
 244     ASM_MESON_TAC[REAL_OF_NUM_EQ; REAL_ABS_ZERO];
 245     STRIP_TAC THEN FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP
 246      (REAL_ARITH `abs(x:real) = a ==> x = a \/ x = --a`)) THEN
 247     ASM_REWRITE_TAC[real_div; GSYM REAL_MUL_LNEG] THEN
 248     REWRITE_TAC[GSYM real_div] THEN
 249     ASM_MESON_TAC[INTEGER_CLOSED; REAL_OF_NUM_EQ]]);;
 250
 251 (* ------------------------------------------------------------------------- *)
 252 (* The floor and frac functions.                                             *)
 253 (* ------------------------------------------------------------------------- *)
 254
 255 let REAL_ARCH_SIMPLE = prove
 256  (`!x. ?n. x <= &n`,
 257   let lemma = prove(`(!x. (?n. x = &n) ==> P x) <=> !n. P(&n)`,MESON_TAC[]) in
 258   MP_TAC(SPEC `\y. ?n. y = &n` REAL_COMPLETE) THEN REWRITE_TAC[lemma] THEN
 259   MESON_TAC[REAL_LE_SUB_LADD; REAL_OF_NUM_ADD; REAL_LE_TOTAL;
 260             REAL_ARITH `~(M <= M - &1)`]);;
 261
 262 let REAL_TRUNCATE_POS = prove
 263  (`!x. &0 <= x ==> ?n r. &0 <= r /\ r < &1 /\ (x = &n + r)`,
 264   REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real` REAL_ARCH_SIMPLE) THEN
 265   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
 266   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 267   INDUCT_TAC THEN REWRITE_TAC[LT_SUC_LE; CONJUNCT1 LT] THENL
 268    [DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`0`; `&0`] THEN ASM_REAL_ARITH_TAC;
 269     POP_ASSUM_LIST(K ALL_TAC)] THEN
 270   REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
 271   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `n:num`)) THEN
 272   REWRITE_TAC[LE_REFL; REAL_NOT_LE] THEN DISCH_TAC THEN
 273   FIRST_X_ASSUM(DISJ_CASES_THEN STRIP_ASSUME_TAC o REWRITE_RULE[REAL_LE_LT])
 274   THENL
 275    [MAP_EVERY EXISTS_TAC [`n:num`; `x - &n`] THEN ASM_REAL_ARITH_TAC;
 276     MAP_EVERY EXISTS_TAC [`SUC n`; `x - &(SUC n)`] THEN
 277     REWRITE_TAC[REAL_ADD_SUB; GSYM REAL_OF_NUM_SUC] THEN ASM_REAL_ARITH_TAC]);;
 278
 279 let REAL_TRUNCATE = prove
 280  (`!x. ?n r. integer(n) /\ &0 <= r /\ r < &1 /\ (x = n + r)`,
 281   GEN_TAC THEN DISJ_CASES_TAC(SPECL [`x:real`; `&0`] REAL_LE_TOTAL) THENL
 282    [MP_TAC(SPEC `--x` REAL_ARCH_SIMPLE) THEN
 283     REWRITE_TAC[REAL_ARITH `--a <= b <=> &0 <= a + b`] THEN
 284     DISCH_THEN(X_CHOOSE_THEN `n:num`
 285      (MP_TAC o MATCH_MP REAL_TRUNCATE_POS)) THEN
 286     REWRITE_TAC[REAL_ARITH `(a + b = c + d) <=> (a = (c - b) + d)`];
 287     ALL_TAC] THEN
 288   ASM_MESON_TAC[integer; INTEGER_CLOSED; REAL_TRUNCATE_POS]);;
 289
 290 let FLOOR_FRAC =
 291     new_specification ["floor"; "frac"]
 292        (REWRITE_RULE[SKOLEM_THM] REAL_TRUNCATE);;
 293
 294 (* ------------------------------------------------------------------------- *)
 295 (* Useful lemmas about floor and frac.                                       *)
 296 (* ------------------------------------------------------------------------- *)
 297
 298 let FLOOR_UNIQUE = prove
 299  (`!x a. integer(a) /\ a <= x /\ x < a + &1 <=> (floor x = a)`,
 300   REPEAT GEN_TAC THEN EQ_TAC THENL
 301    [STRIP_TAC THEN STRIP_ASSUME_TAC(SPEC `x:real` FLOOR_FRAC) THEN
 302     SUBGOAL_THEN `abs(floor x - a) < &1` MP_TAC THENL
 303      [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 304     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 305     DISCH_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN
 306     MATCH_MP_TAC REAL_ABS_INTEGER_LEMMA THEN CONJ_TAC THENL
 307      [ASM_MESON_TAC[INTEGER_CLOSED]; ASM_REAL_ARITH_TAC];
 308     DISCH_THEN(SUBST1_TAC o SYM) THEN
 309     MP_TAC(SPEC `x:real` FLOOR_FRAC) THEN
 310     SIMP_TAC[] THEN REAL_ARITH_TAC]);;
 311
 312 let FLOOR_EQ_0 = prove
 313  (`!x. (floor x = &0) <=> &0 <= x /\ x < &1`,
 314   GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN
 315   REWRITE_TAC[INTEGER_CLOSED; REAL_ADD_LID]);;
 316
 317 let FLOOR = prove
 318  (`!x. integer(floor x) /\ floor(x) <= x /\ x < floor(x) + &1`,
 319   GEN_TAC THEN MP_TAC(SPEC `x:real` FLOOR_FRAC) THEN
 320   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 321   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 322
 323 let FLOOR_DOUBLE = prove
 324  (`!u. &2 * floor(u) <= floor(&2 * u) /\ floor(&2 * u) <= &2 * floor(u) + &1`,
 325   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_REVERSE_INTEGERS THEN
 326   SIMP_TAC[INTEGER_CLOSED; FLOOR] THEN
 327   MP_TAC(SPEC `u:real` FLOOR) THEN MP_TAC(SPEC `&2 * u` FLOOR) THEN
 328   REAL_ARITH_TAC);;
 329
 330 let FRAC_FLOOR = prove
 331  (`!x. frac(x) = x - floor(x)`,
 332   MP_TAC FLOOR_FRAC THEN MATCH_MP_TAC MONO_FORALL THEN REAL_ARITH_TAC);;
 333
 334 let FLOOR_NUM = prove
 335  (`!n. floor(&n) = &n`,
 336   REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
 337
 338 let REAL_LE_FLOOR = prove
 339  (`!x n. integer(n) ==> (n <= floor x <=> n <= x)`,
 340   REPEAT STRIP_TAC THEN EQ_TAC THENL
 341    [ASM_MESON_TAC[FLOOR; REAL_LE_TRANS]; ALL_TAC] THEN
 342   REWRITE_TAC[GSYM REAL_NOT_LT] THEN ASM_SIMP_TAC[REAL_LT_INTEGERS; FLOOR] THEN
 343   MP_TAC(SPEC `x:real` FLOOR) THEN REAL_ARITH_TAC);;
 344
 345 let REAL_FLOOR_LE = prove
 346  (`!x n. integer n ==> (floor x <= n <=> x - &1 < n)`,
 347   REPEAT STRIP_TAC THEN
 348   ONCE_REWRITE_TAC[REAL_ARITH `x <= y <=> x + &1 <= y + &1`] THEN
 349   ASM_SIMP_TAC[GSYM REAL_LT_INTEGERS; FLOOR; INTEGER_CLOSED] THEN
 350   ONCE_REWRITE_TAC[TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN
 351   ASM_SIMP_TAC[REAL_NOT_LT; REAL_LE_FLOOR; INTEGER_CLOSED] THEN
 352   REAL_ARITH_TAC);;
 353
 354 let FLOOR_POS = prove
 355  (`!x. &0 <= x ==> ?n. floor(x) = &n`,
 356   REPEAT STRIP_TAC THEN MP_TAC(CONJUNCT1(SPEC `x:real` FLOOR)) THEN
 357   REWRITE_TAC[integer] THEN
 358   ASM_SIMP_TAC[real_abs; REAL_LE_FLOOR; FLOOR; INTEGER_CLOSED]);;
 359
 360 let FLOOR_DIV_DIV = prove
 361  (`!m n. ~(m = 0) ==> floor(&n / &m) = &(n DIV m)`,
 362   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN
 363   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT;
 364                REAL_OF_NUM_LE; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; LT_NZ] THEN
 365   FIRST_X_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN ARITH_TAC);;
 366
 367 let FLOOR_MONO = prove
 368  (`!x y. x <= y ==> floor x <= floor y`,
 369   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN
 370   SIMP_TAC[FLOOR; REAL_LT_INTEGERS] THEN
 371   MAP_EVERY (MP_TAC o C SPEC FLOOR) [`x:real`; `y:real`] THEN REAL_ARITH_TAC);;
 372
 373 let REAL_FLOOR_EQ = prove
 374  (`!x. floor x = x <=> integer x`,
 375   REWRITE_TAC[GSYM FLOOR_UNIQUE; REAL_LE_REFL; REAL_ARITH `x < x + &1`]);;
 376
 377 let REAL_FLOOR_LT = prove
 378  (`!x. floor x < x <=> ~(integer x)`,
 379   MESON_TAC[REAL_LT_LE; REAL_FLOOR_EQ; FLOOR]);;
 380
 381 let REAL_FRAC_EQ_0 = prove
 382  (`!x. frac x = &0 <=> integer x`,
 383   REWRITE_TAC[FRAC_FLOOR; REAL_SUB_0] THEN MESON_TAC[REAL_FLOOR_EQ]);;
 384
 385 let REAL_FRAC_POS_LT = prove
 386  (`!x. &0 < frac x <=> ~(integer x)`,
 387   REWRITE_TAC[FRAC_FLOOR; REAL_SUB_LT; REAL_FLOOR_LT]);;
 388
 389 let FRAC_NUM = prove
 390  (`!n. frac(&n) = &0`,
 391   REWRITE_TAC[REAL_FRAC_EQ_0; INTEGER_CLOSED]);;
 392
 393 let REAL_FLOOR_REFL = prove
 394  (`!x. integer x ==> floor x = x`,
 395   REWRITE_TAC[REAL_FLOOR_EQ]);;
 396
 397 let REAL_FRAC_ZERO = prove
 398  (`!x. integer x ==> frac x = &0`,
 399   REWRITE_TAC[REAL_FRAC_EQ_0]);;
 400
 401 let REAL_FLOOR_ADD = prove
 402  (`!x y. floor(x + y) = if frac x + frac y < &1 then floor(x) + floor(y)
 403                         else (floor(x) + floor(y)) + &1`,
 404   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN
 405   CONJ_TAC THENL [ASM_MESON_TAC[INTEGER_CLOSED; FLOOR]; ALL_TAC] THEN
 406   MAP_EVERY (MP_TAC o C SPEC FLOOR_FRAC)[`x:real`; `y:real`; `x + y:real`] THEN
 407   REAL_ARITH_TAC);;
 408
 409 let REAL_FRAC_ADD = prove
 410  (`!x y. frac(x + y) = if frac x + frac y < &1 then frac(x) + frac(y)
 411                        else (frac(x) + frac(y)) - &1`,
 412   REWRITE_TAC[FRAC_FLOOR; REAL_FLOOR_ADD] THEN REAL_ARITH_TAC);;
 413
 414 let FLOOR_POS_LE = prove
 415  (`!x. &0 <= floor x <=> &0 <= x`,
 416   SIMP_TAC[REAL_LE_FLOOR; INTEGER_CLOSED]);;
 417
 418 let FRAC_UNIQUE = prove
 419  (`!x a. integer(x - a) /\ &0 <= a /\ a < &1 <=> frac x = a`,
 420   REWRITE_TAC[FRAC_FLOOR; REAL_ARITH `x - f:real = a <=> f = x - a`] THEN
 421   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN
 422   AP_TERM_TAC THEN REAL_ARITH_TAC);;
 423
 424 let REAL_FRAC_EQ = prove
 425  (`!x. frac x = x <=> &0 <= x /\ x < &1`,
 426   REWRITE_TAC[GSYM FRAC_UNIQUE; REAL_SUB_REFL; INTEGER_CLOSED]);;
 427
 428 let INTEGER_ROUND = prove
 429  (`!x. ?n. integer n /\ abs(x - n) <= &1 / &2`,
 430   GEN_TAC THEN MATCH_MP_TAC(MESON[] `!a. P a \/ P(a + &1) ==> ?x. P x`) THEN
 431   EXISTS_TAC `floor x` THEN MP_TAC(ISPEC `x:real` FLOOR) THEN
 432   SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
 433
 434 (* ------------------------------------------------------------------------- *)
 435 (* Assertions that there are integers between well-spaced reals.             *)
 436 (* ------------------------------------------------------------------------- *)
 437
 438 let INTEGER_EXISTS_BETWEEN_ALT = prove
 439  (`!x y. x + &1 <= y ==> ?n. integer n /\ x < n /\ n <= y`,
 440   REPEAT STRIP_TAC THEN EXISTS_TAC `floor y` THEN
 441   MP_TAC(SPEC `y:real` FLOOR) THEN SIMP_TAC[] THEN ASM_REAL_ARITH_TAC);;
 442
 443 let INTEGER_EXISTS_BETWEEN_LT = prove
 444  (`!x y. x + &1 < y ==> ?n. integer n /\ x < n /\ n < y`,
 445   REPEAT STRIP_TAC THEN ASM_CASES_TAC `integer y` THENL
 446    [EXISTS_TAC `y - &1:real` THEN
 447     ASM_SIMP_TAC[INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC;
 448     FIRST_ASSUM(MP_TAC o MATCH_MP INTEGER_EXISTS_BETWEEN_ALT o
 449       MATCH_MP REAL_LT_IMP_LE) THEN
 450     MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN
 451     ASM_REWRITE_TAC[REAL_LT_LE] THEN ASM_MESON_TAC[]]);;
 452
 453 let INTEGER_EXISTS_BETWEEN = prove
 454  (`!x y. x + &1 <= y ==> ?n. integer n /\ x <= n /\ n < y`,
 455   REPEAT STRIP_TAC THEN ASM_CASES_TAC `integer y` THENL
 456    [EXISTS_TAC `y - &1:real` THEN
 457     ASM_SIMP_TAC[INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC;
 458     FIRST_ASSUM(MP_TAC o MATCH_MP INTEGER_EXISTS_BETWEEN_ALT) THEN
 459     MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN
 460     ASM_REWRITE_TAC[REAL_LT_LE] THENL [ASM_REAL_ARITH_TAC; ASM_MESON_TAC[]]]);;
 461
 462 let INTEGER_EXISTS_BETWEEN_ABS = prove
 463  (`!x y. &1 <= abs(x - y)
 464          ==> ?n. integer n /\ (x <= n /\ n < y \/ y <= n /\ n < x)`,
 465   REPEAT GEN_TAC THEN REWRITE_TAC[real_abs] THEN
 466   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THENL
 467    [MP_TAC(ISPECL [`y:real`; `x:real`] INTEGER_EXISTS_BETWEEN);
 468     MP_TAC(ISPECL [`x:real`; `y:real`] INTEGER_EXISTS_BETWEEN)] THEN
 469   (ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS]) THEN
 470   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 471
 472 let INTEGER_EXISTS_BETWEEN_ABS_LT = prove
 473  (`!x y. &1 < abs(x - y)
 474          ==> ?n. integer n /\ (x < n /\ n < y \/ y < n /\ n < x)`,
 475   REPEAT GEN_TAC THEN REWRITE_TAC[real_abs] THEN
 476   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THENL
 477    [MP_TAC(ISPECL [`y:real`; `x:real`] INTEGER_EXISTS_BETWEEN_LT);
 478     MP_TAC(ISPECL [`x:real`; `y:real`] INTEGER_EXISTS_BETWEEN_LT)] THEN
 479   (ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS]) THEN
 480   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 481
 482 (* ------------------------------------------------------------------------- *)
 483 (* A couple more theorems about real_of_int.                                 *)
 484 (* ------------------------------------------------------------------------- *)
 485
 486 let INT_OF_REAL_OF_INT = prove
 487  (`!i. int_of_real(real_of_int i) = i`,
 488   REWRITE_TAC[int_abstr]);;
 489
 490 let REAL_OF_INT_OF_REAL = prove
 491  (`!x. integer(x) ==> real_of_int(int_of_real x) = x`,
 492   SIMP_TAC[int_rep]);;
 493
 494 (* ------------------------------------------------------------------------- *)
 495 (* Finiteness of bounded set of integers.                                    *)
 496 (* ------------------------------------------------------------------------- *)
 497
 498 let HAS_SIZE_INTSEG_NUM = prove
 499  (`!m n. {x | integer(x) /\ &m <= x /\ x <= &n} HAS_SIZE ((n + 1) - m)`,
 500   REPEAT STRIP_TAC THEN
 501   SUBGOAL_THEN `{x | integer(x) /\ &m <= x /\ x <= &n} =
 502                 IMAGE real_of_num (m..n)`
 503   SUBST1_TAC THENL
 504    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
 505     X_GEN_TAC `x:real` THEN ASM_CASES_TAC `?k. x = &k` THENL
 506      [FIRST_X_ASSUM(CHOOSE_THEN SUBST_ALL_TAC) THEN
 507       REWRITE_TAC[REAL_OF_NUM_LE; INTEGER_CLOSED; REAL_OF_NUM_EQ] THEN
 508       REWRITE_TAC[UNWIND_THM1; IN_NUMSEG];
 509       ASM_MESON_TAC[INTEGER_POS; REAL_ARITH `&n <= x ==> &0 <= x`]];
 510     MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN REWRITE_TAC[HAS_SIZE_NUMSEG] THEN
 511     SIMP_TAC[REAL_OF_NUM_EQ]]);;
 512
 513 let FINITE_INTSEG = prove
 514  (`!a b. FINITE {x | integer(x) /\ a <= x /\ x <= b}`,
 515   REPEAT STRIP_TAC THEN
 516   MP_TAC(SPEC `max (abs a) (abs b)` REAL_ARCH_SIMPLE) THEN
 517   REWRITE_TAC[REAL_MAX_LE; LEFT_IMP_EXISTS_THM] THEN
 518   X_GEN_TAC `n:num` THEN STRIP_TAC THEN
 519   MATCH_MP_TAC FINITE_SUBSET THEN
 520   EXISTS_TAC `{x | integer(x) /\ abs(x) <= &n}` THEN CONJ_TAC THENL
 521    [ALL_TAC; SIMP_TAC[SUBSET; IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC] THEN
 522   MATCH_MP_TAC FINITE_SUBSET THEN
 523   EXISTS_TAC `IMAGE (\x. &x) (0..n) UNION IMAGE (\x. --(&x)) (0..n)` THEN
 524   ASM_SIMP_TAC[FINITE_UNION; FINITE_IMAGE; FINITE_NUMSEG] THEN
 525   REWRITE_TAC[INTEGER_CASES; SUBSET; IN_ELIM_THM] THEN
 526   REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 527   REWRITE_TAC[IN_UNION; IN_IMAGE; REAL_OF_NUM_EQ; REAL_EQ_NEG2] THEN
 528   REWRITE_TAC[UNWIND_THM1; IN_NUMSEG] THEN
 529   REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN
 530   ASM_REAL_ARITH_TAC);;
 531
 532 let HAS_SIZE_INTSEG_INT = prove
 533  (`!a b. integer a /\ integer b
 534          ==> {x | integer(x) /\ a <= x /\ x <= b} HAS_SIZE
 535              if b < a then 0 else num_of_int(int_of_real(b - a + &1))`,
 536   REPEAT STRIP_TAC THEN
 537   SUBGOAL_THEN
 538    `{x | integer(x) /\ a <= x /\ x <= b} =
 539     IMAGE (\n. a + &n) {n | &n <= b - a}`
 540   SUBST1_TAC THENL
 541    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
 542     ASM_SIMP_TAC[IN_ELIM_THM; INTEGER_CLOSED] THEN
 543     CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
 544     X_GEN_TAC `c:real` THEN STRIP_TAC THEN
 545     ONCE_REWRITE_TAC[REAL_ARITH `a + x:real = y <=> y - a = x`] THEN
 546     ASM_SIMP_TAC[GSYM INTEGER_POS; REAL_SUB_LE; INTEGER_CLOSED];
 547     MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
 548
 549     SIMP_TAC[REAL_EQ_ADD_LCANCEL; REAL_OF_NUM_EQ] THEN
 550     COND_CASES_TAC THENL
 551      [ASM_SIMP_TAC[REAL_ARITH `b < a ==> ~(&n <= b - a)`] THEN
 552       REWRITE_TAC[HAS_SIZE_0; EMPTY_GSPEC];
 553       SUBGOAL_THEN `?m. b - a = &m` (CHOOSE_THEN SUBST1_TAC) THENL
 554        [ASM_MESON_TAC[INTEGER_POS; INTEGER_CLOSED; REAL_NOT_LT; REAL_SUB_LE];
 555         REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; GSYM int_of_num;
 556                     NUM_OF_INT_OF_NUM; HAS_SIZE_NUMSEG_LE]]]]);;
 557
 558 let CARD_INTSEG_INT = prove
 559  (`!a b. integer a /\ integer b
 560          ==> CARD {x | integer(x) /\ a <= x /\ x <= b} =
 561              if b < a then 0 else num_of_int(int_of_real(b - a + &1))`,
 562   REPEAT GEN_TAC THEN
 563   DISCH_THEN(MP_TAC o MATCH_MP HAS_SIZE_INTSEG_INT) THEN
 564   SIMP_TAC[HAS_SIZE]);;
 565
 566 let REAL_CARD_INTSEG_INT = prove
 567  (`!a b. integer a /\ integer b
 568          ==> &(CARD {x | integer(x) /\ a <= x /\ x <= b}) =
 569              if b < a then &0 else b - a + &1`,
 570   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[CARD_INTSEG_INT] THEN
 571   COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_OF_INT_OF_REAL] THEN
 572   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM int_of_num_th] THEN
 573   W(MP_TAC o PART_MATCH (lhs o rand) INT_OF_NUM_OF_INT o
 574     rand o lhand o snd) THEN
 575   ANTS_TAC THENL
 576    [ASM_SIMP_TAC[int_le; int_of_num_th; REAL_OF_INT_OF_REAL;
 577                  INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC;
 578     DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC REAL_OF_INT_OF_REAL THEN
 579     ASM_SIMP_TAC[INTEGER_CLOSED]]);;
 580
 581 (* ------------------------------------------------------------------------- *)
 582 (* Yet set of all integers or rationals is infinite.                         *)
 583 (* ------------------------------------------------------------------------- *)
 584
 585 let INFINITE_INTEGER = prove
 586  (`INFINITE integer`,
 587   SUBGOAL_THEN `INFINITE(IMAGE real_of_num (:num))` MP_TAC THENL
 588    [SIMP_TAC[INFINITE_IMAGE_INJ; REAL_OF_NUM_EQ; num_INFINITE]; ALL_TAC] THEN
 589   REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN
 590   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN
 591   REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV] THEN
 592   REWRITE_TAC[IN; INTEGER_CLOSED]);;
 593
 594 let INFINITE_RATIONAL = prove
 595  (`INFINITE rational`,
 596   MP_TAC INFINITE_INTEGER THEN
 597   REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN
 598   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN
 599   REWRITE_TAC[SUBSET; IN; RATIONAL_INTEGER]);;
 600
 601 (* ------------------------------------------------------------------------- *)
 602 (* Arbitrarily good rational approximations.                                 *)
 603 (* ------------------------------------------------------------------------- *)
 604
 605 let RATIONAL_APPROXIMATION = prove
 606  (`!x e. &0 < e ==> ?r. rational r /\ abs(r - x) < e`,
 607   REPEAT STRIP_TAC THEN ABBREV_TAC `n = floor(inv e) + &1` THEN
 608   EXISTS_TAC `floor(n * x) / n` THEN EXPAND_TAC "n" THEN
 609   ASM_SIMP_TAC[RATIONAL_CLOSED; INTEGER_CLOSED; FLOOR] THEN
 610   SUBGOAL_THEN `&0 < n` ASSUME_TAC THENL
 611    [EXPAND_TAC "n" THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < x + &1`) THEN
 612     ASM_SIMP_TAC[FLOOR_POS_LE; REAL_LE_INV_EQ; REAL_LT_IMP_LE];
 613     ASM_SIMP_TAC[REAL_FIELD `&0 < n ==> a / n - b = (a - n * b) / n`] THEN
 614     ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ;
 615                  REAL_LT_IMP_NZ] THEN
 616     MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&1` THEN CONJ_TAC THENL
 617      [MP_TAC(SPEC `n * x:real` FLOOR) THEN REAL_ARITH_TAC;
 618       ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 619       ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN
 620       MATCH_MP_TAC(REAL_ARITH `inv e < n ==> &1 / e < abs n`) THEN
 621       EXPAND_TAC "n" THEN MP_TAC(SPEC `inv e` FLOOR) THEN REAL_ARITH_TAC]]);;
 622
 623 let RATIONAL_BETWEEN = prove
 624  (`!a b. a < b ==> ?q. rational q /\ a < q /\ q < b`,
 625   REPEAT STRIP_TAC THEN
 626   MP_TAC(SPECL [`(a + b) / &2`; `(b - a) / &4`] RATIONAL_APPROXIMATION) THEN
 627   ANTS_TAC THENL [ALL_TAC; MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[]] THEN
 628   ASM_REAL_ARITH_TAC);;
 629
 630 let RATIONAL_APPROXIMATION_STRADDLE = prove
 631  (`!x e. &0 < e
 632          ==> ?a b. rational a /\ rational b /\
 633                    a < x /\ x < b /\ abs(b - a) < e`,
 634   REPEAT STRIP_TAC THEN
 635   MP_TAC(ISPECL [`x - e / &4`; `e / &4`] RATIONAL_APPROXIMATION) THEN
 636   ANTS_TAC THENL
 637    [ASM_REAL_ARITH_TAC;
 638     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC] THEN
 639   MP_TAC(ISPECL [`x + e / &4`; `e / &4`] RATIONAL_APPROXIMATION) THEN
 640   ANTS_TAC THENL
 641    [ASM_REAL_ARITH_TAC;
 642     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC] THEN
 643   ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);;