(* ========================================================================= *)
(* The integer/rational-valued reals, and the "floor" and "frac" functions.  *)
(* ========================================================================= *)

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Closure theorems and other lemmas for the integer-valued reals.           *)
(* ------------------------------------------------------------------------- *)

let INTEGER_CASES = 
prove (`integer x <=> (?n. x = &n) \/ (?n. x = -- &n)`,
REWRITE_TAC[is_int; OR_EXISTS_THM]);;
let REAL_ABS_INTEGER_LEMMA = 
prove (`!x. integer(x) /\ ~(x = &0) ==> &1 <= abs(x)`,
GEN_TAC THEN REWRITE_TAC[integer] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ONCE_REWRITE_TAC[REAL_ARITH `(x = &0) <=> (abs(x) = &0)`] THEN POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_LE] THEN ARITH_TAC);;
let INTEGER_CLOSED = 
prove (`(!n. integer(&n)) /\ (!x y. integer(x) /\ integer(y) ==> integer(x + y)) /\ (!x y. integer(x) /\ integer(y) ==> integer(x - y)) /\ (!x y. integer(x) /\ integer(y) ==> integer(x * y)) /\ (!x r. integer(x) ==> integer(x pow r)) /\ (!x. integer(x) ==> integer(--x)) /\ (!x. integer(x) ==> integer(abs x))`,
REWRITE_TAC[integer] THEN MATCH_MP_TAC(TAUT `x /\ c /\ d /\ e /\ f /\ (a /\ e ==> b) /\ a ==> x /\ a /\ b /\ c /\ d /\ e /\ f`) THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_NUM] THEN MESON_TAC[]; REWRITE_TAC[REAL_ABS_MUL] THEN MESON_TAC[REAL_OF_NUM_MUL]; REWRITE_TAC[REAL_ABS_POW] THEN MESON_TAC[REAL_OF_NUM_POW]; REWRITE_TAC[REAL_ABS_NEG]; REWRITE_TAC[REAL_ABS_ABS]; REWRITE_TAC[real_sub] THEN MESON_TAC[]; ALL_TAC] THEN SIMP_TAC[REAL_ARITH `&0 <= a ==> ((abs(x) = a) <=> (x = a) \/ (x = --a))`; REAL_POS] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM REAL_NEG_ADD; REAL_OF_NUM_ADD] THENL [MESON_TAC[]; ALL_TAC; ALL_TAC; MESON_TAC[]] THEN REWRITE_TAC[REAL_ARITH `(--a + b = c) <=> (a + c = b)`; REAL_ARITH `(a + --b = c) <=> (b + c = a)`] THEN REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN MESON_TAC[LE_EXISTS; ADD_SYM; LE_CASES]);;
let INTEGER_ADD = 
prove (`!x y. integer(x) /\ integer(y) ==> integer(x + y)`,
REWRITE_TAC[INTEGER_CLOSED]);;
let INTEGER_SUB = 
prove (`!x y. integer(x) /\ integer(y) ==> integer(x - y)`,
REWRITE_TAC[INTEGER_CLOSED]);;
let INTEGER_MUL = 
prove (`!x y. integer(x) /\ integer(y) ==> integer(x * y)`,
REWRITE_TAC[INTEGER_CLOSED]);;
let INTEGER_POW = 
prove (`!x n. integer(x) ==> integer(x pow n)`,
REWRITE_TAC[INTEGER_CLOSED]);;
let REAL_LE_INTEGERS = 
prove (`!x y. integer(x) /\ integer(y) ==> (x <= y <=> (x = y) \/ x + &1 <= y)`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `y - x` REAL_ABS_INTEGER_LEMMA) THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let REAL_LE_CASES_INTEGERS = 
prove (`!x y. integer(x) /\ integer(y) ==> x <= y \/ y + &1 <= x`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `y - x` REAL_ABS_INTEGER_LEMMA) THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let REAL_LE_REVERSE_INTEGERS = 
prove (`!x y. integer(x) /\ integer(y) /\ ~(y + &1 <= x) ==> x <= y`,
MESON_TAC[REAL_LE_CASES_INTEGERS]);;
let REAL_LT_INTEGERS = 
prove (`!x y. integer(x) /\ integer(y) ==> (x < y <=> x + &1 <= y)`,
MESON_TAC[REAL_NOT_LT; REAL_LE_CASES_INTEGERS; REAL_ARITH `x + &1 <= y ==> x < y`]);;
let REAL_EQ_INTEGERS = 
prove (`!x y. integer x /\ integer y ==> (x = y <=> abs(x - y) < &1)`,
REWRITE_TAC[REAL_ARITH `x = y <=> ~(x < y \/ y < x)`] THEN SIMP_TAC[REAL_LT_INTEGERS] THEN REAL_ARITH_TAC);;
let REAL_EQ_INTEGERS_IMP = 
prove (`!x y. integer x /\ integer y /\ abs(x - y) < &1 ==> x = y`,
SIMP_TAC[REAL_EQ_INTEGERS]);;
let INTEGER_NEG = 
prove (`!x. integer(--x) <=> integer(x)`,
let INTEGER_ABS = 
prove (`!x. integer(abs x) <=> integer(x)`,
GEN_TAC THEN REWRITE_TAC[real_abs] THEN COND_CASES_TAC THEN REWRITE_TAC[INTEGER_NEG]);;
let INTEGER_POS = 
prove (`!x. &0 <= x ==> (integer(x) <=> ?n. x = &n)`,
SIMP_TAC[integer; real_abs]);;
let INTEGER_ADD_EQ = 
prove (`(!x y. integer(x) ==> (integer(x + y) <=> integer(y))) /\ (!x y. integer(y) ==> (integer(x + y) <=> integer(x)))`,
MESON_TAC[REAL_ADD_SUB; REAL_ADD_SYM; INTEGER_CLOSED]);;
let INTEGER_SUB_EQ = 
prove (`(!x y. integer(x) ==> (integer(x - y) <=> integer(y))) /\ (!x y. integer(y) ==> (integer(x - y) <=> integer(x)))`,
let FORALL_INTEGER = 
prove (`!P. (!n. P(&n)) /\ (!x. P x ==> P(--x)) ==> !x. integer x ==> P x`,
MESON_TAC[INTEGER_CASES]);;
let INTEGER_SUM = 
prove (`!f:A->real s. (!x. x IN s ==> integer(f x)) ==> integer(sum s f)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_CLOSED THEN ASM_REWRITE_TAC[INTEGER_CLOSED]);;
let INTEGER_ABS_MUL_EQ_1 = 
prove (`!x y. integer x /\ integer y ==> (abs(x * y) = &1 <=> abs x = &1 /\ abs y = &1)`,
REWRITE_TAC[integer] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ABS_MUL] THEN REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_MUL; MULT_EQ_1]);;
let INTEGER_DIV = 
prove (`!m n. integer(&m / &n) <=> n = 0 \/ n divides m`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO; INTEGER_CLOSED]; ASM_SIMP_TAC[INTEGER_POS; REAL_POS; REAL_LE_DIV; divides] THEN ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD `~(n = &0) ==> (x / n = y <=> x = n * y)`] THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ]]);;
(* ------------------------------------------------------------------------- *) (* Similar theorems for rational-valued reals. *) (* ------------------------------------------------------------------------- *)
let rational = new_definition
 `rational x <=> ?m n. integer m /\ integer n /\ ~(n = &0) /\ x = m / n`;;
let RATIONAL_INTEGER = 
prove (`!x. integer x ==> rational x`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[rational] THEN MAP_EVERY EXISTS_TAC [`x:real`; `&1`] THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN CONV_TAC REAL_FIELD);;
let RATIONAL_NUM = 
prove (`!n. rational(&n)`,
let RATIONAL_NEG = 
prove (`!x. rational(x) ==> rational(--x)`,
REWRITE_TAC[rational; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`x:real`; `m:real`; `n:real`] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`--m:real`; `n:real`] THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN CONV_TAC REAL_FIELD);;
let RATIONAL_ABS = 
prove (`!x. rational(x) ==> rational(abs x)`,
REWRITE_TAC[real_abs] THEN MESON_TAC[RATIONAL_NEG]);;
let RATIONAL_INV = 
prove (`!x. rational(x) ==> rational(inv x)`,
GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[REAL_INV_0; RATIONAL_NUM] THEN REWRITE_TAC[rational; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`m:real`; `n:real`] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`n:real`; `m:real`] THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
let RATIONAL_ADD = 
prove (`!x y. rational(x) /\ rational(y) ==> rational(x + y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[rational; LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`m1:real`; `n1:real`; `m2:real`; `n2:real`] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`m1 * n2 + m2 * n1:real`; `n1 * n2:real`] THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
let RATIONAL_SUB = 
prove (`!x y. rational(x) /\ rational(y) ==> rational(x - y)`,
let RATIONAL_MUL = 
prove (`!x y. rational(x) /\ rational(y) ==> rational(x * y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[rational; LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`m1:real`; `n1:real`; `m2:real`; `n2:real`] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`m1 * m2:real`; `n1 * n2:real`] THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
let RATIONAL_DIV = 
prove (`!x y. rational(x) /\ rational(y) ==> rational(x / y)`,
let RATIONAL_POW = 
prove (`!x n. rational(x) ==> rational(x pow n)`,
GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[real_pow; RATIONAL_NUM; RATIONAL_MUL]);;
let RATIONAL_CLOSED = 
prove (`(!n. rational(&n)) /\ (!x. integer x ==> rational x) /\ (!x y. rational(x) /\ rational(y) ==> rational(x + y)) /\ (!x y. rational(x) /\ rational(y) ==> rational(x - y)) /\ (!x y. rational(x) /\ rational(y) ==> rational(x * y)) /\ (!x y. rational(x) /\ rational(y) ==> rational(x / y)) /\ (!x r. rational(x) ==> rational(x pow r)) /\ (!x. rational(x) ==> rational(--x)) /\ (!x. rational(x) ==> rational(inv x)) /\ (!x. rational(x) ==> rational(abs x))`,
let RATIONAL_NEG_EQ = 
prove (`!x. rational(--x) <=> rational x`,
MESON_TAC[REAL_NEG_NEG; RATIONAL_NEG]);;
let RATIONAL_INV_EQ = 
prove (`!x. rational(inv x) <=> rational x`,
MESON_TAC[REAL_INV_INV; RATIONAL_INV]);;
let RATIONAL_ALT = 
prove (`!x. rational(x) <=> ?p q. ~(q = 0) /\ abs x = &p / &q`,
GEN_TAC THEN REWRITE_TAC[rational] THEN EQ_TAC THENL [REWRITE_TAC[integer] THEN STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ABS_DIV] THEN ASM_MESON_TAC[REAL_OF_NUM_EQ; REAL_ABS_ZERO]; STRIP_TAC THEN FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (REAL_ARITH `abs(x:real) = a ==> x = a \/ x = --a`)) THEN ASM_REWRITE_TAC[real_div; GSYM REAL_MUL_LNEG] THEN REWRITE_TAC[GSYM real_div] THEN ASM_MESON_TAC[INTEGER_CLOSED; REAL_OF_NUM_EQ]]);;
(* ------------------------------------------------------------------------- *) (* The floor and frac functions. *) (* ------------------------------------------------------------------------- *)
let REAL_ARCH_SIMPLE = 
prove (`!x. ?n. x <= &n`,
let lemma = prove(`(!x. (?n. x = &n) ==> P x) <=> !n. P(&n)`,MESON_TAC[]) in
  MP_TAC(SPEC `\y. ?n. y = &n` REAL_COMPLETE) THEN REWRITE_TAC[lemma] THEN
  MESON_TAC[REAL_LE_SUB_LADD; REAL_OF_NUM_ADD; REAL_LE_TOTAL;
            REAL_ARITH `~(M <= M - &1)`]);;
let REAL_TRUNCATE_POS = 
prove (`!x. &0 <= x ==> ?n r. &0 <= r /\ r < &1 /\ (x = &n + r)`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real` REAL_ARCH_SIMPLE) THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN INDUCT_TAC THEN REWRITE_TAC[LT_SUC_LE; CONJUNCT1 LT] THENL [DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`0`; `&0`] THEN ASM_REAL_ARITH_TAC; POP_ASSUM_LIST(K ALL_TAC)] THEN REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `n:num`)) THEN REWRITE_TAC[LE_REFL; REAL_NOT_LE] THEN DISCH_TAC THEN FIRST_X_ASSUM(DISJ_CASES_THEN STRIP_ASSUME_TAC o REWRITE_RULE[REAL_LE_LT]) THENL [MAP_EVERY EXISTS_TAC [`n:num`; `x - &n`] THEN ASM_REAL_ARITH_TAC; MAP_EVERY EXISTS_TAC [`SUC n`; `x - &(SUC n)`] THEN REWRITE_TAC[REAL_ADD_SUB; GSYM REAL_OF_NUM_SUC] THEN ASM_REAL_ARITH_TAC]);;
let REAL_TRUNCATE = 
prove (`!x. ?n r. integer(n) /\ &0 <= r /\ r < &1 /\ (x = n + r)`,
GEN_TAC THEN DISJ_CASES_TAC(SPECL [`x:real`; `&0`] REAL_LE_TOTAL) THENL [MP_TAC(SPEC `--x` REAL_ARCH_SIMPLE) THEN REWRITE_TAC[REAL_ARITH `--a <= b <=> &0 <= a + b`] THEN DISCH_THEN(X_CHOOSE_THEN `n:num` (MP_TAC o MATCH_MP REAL_TRUNCATE_POS)) THEN REWRITE_TAC[REAL_ARITH `(a + b = c + d) <=> (a = (c - b) + d)`]; ALL_TAC] THEN ASM_MESON_TAC[integer; INTEGER_CLOSED; REAL_TRUNCATE_POS]);;
let FLOOR_FRAC =
    new_specification ["floor";
"frac"] (REWRITE_RULE[SKOLEM_THM] REAL_TRUNCATE);; (* ------------------------------------------------------------------------- *) (* Useful lemmas about floor and frac. *) (* ------------------------------------------------------------------------- *)
let FLOOR_UNIQUE = 
prove (`!x a. integer(a) /\ a <= x /\ x < a + &1 <=> (floor x = a)`,
REPEAT GEN_TAC THEN EQ_TAC THENL [STRIP_TAC THEN STRIP_ASSUME_TAC(SPEC `x:real` FLOOR_FRAC) THEN SUBGOAL_THEN `abs(floor x - a) < &1` MP_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_TAC THEN REWRITE_TAC[REAL_NOT_LT] THEN MATCH_MP_TAC REAL_ABS_INTEGER_LEMMA THEN CONJ_TAC THENL [ASM_MESON_TAC[INTEGER_CLOSED]; ASM_REAL_ARITH_TAC]; DISCH_THEN(SUBST1_TAC o SYM) THEN MP_TAC(SPEC `x:real` FLOOR_FRAC) THEN SIMP_TAC[] THEN REAL_ARITH_TAC]);;
let FLOOR_EQ_0 = 
prove (`!x. (floor x = &0) <=> &0 <= x /\ x < &1`,
GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN REWRITE_TAC[INTEGER_CLOSED; REAL_ADD_LID]);;
let FLOOR = 
prove (`!x. integer(floor x) /\ floor(x) <= x /\ x < floor(x) + &1`,
GEN_TAC THEN MP_TAC(SPEC `x:real` FLOOR_FRAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let FLOOR_DOUBLE = 
prove (`!u. &2 * floor(u) <= floor(&2 * u) /\ floor(&2 * u) <= &2 * floor(u) + &1`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_REVERSE_INTEGERS THEN SIMP_TAC[INTEGER_CLOSED; FLOOR] THEN MP_TAC(SPEC `u:real` FLOOR) THEN MP_TAC(SPEC `&2 * u` FLOOR) THEN REAL_ARITH_TAC);;
let FRAC_FLOOR = 
prove (`!x. frac(x) = x - floor(x)`,
MP_TAC FLOOR_FRAC THEN MATCH_MP_TAC MONO_FORALL THEN REAL_ARITH_TAC);;
let FLOOR_NUM = 
prove (`!n. floor(&n) = &n`,
REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let REAL_LE_FLOOR = 
prove (`!x n. integer(n) ==> (n <= floor x <=> n <= x)`,
REPEAT STRIP_TAC THEN EQ_TAC THENL [ASM_MESON_TAC[FLOOR; REAL_LE_TRANS]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN ASM_SIMP_TAC[REAL_LT_INTEGERS; FLOOR] THEN MP_TAC(SPEC `x:real` FLOOR) THEN REAL_ARITH_TAC);;
let REAL_FLOOR_LE = 
prove (`!x n. integer n ==> (floor x <= n <=> x - &1 < n)`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `x <= y <=> x + &1 <= y + &1`] THEN ASM_SIMP_TAC[GSYM REAL_LT_INTEGERS; FLOOR; INTEGER_CLOSED] THEN ONCE_REWRITE_TAC[TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN ASM_SIMP_TAC[REAL_NOT_LT; REAL_LE_FLOOR; INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
let FLOOR_POS = 
prove (`!x. &0 <= x ==> ?n. floor(x) = &n`,
REPEAT STRIP_TAC THEN MP_TAC(CONJUNCT1(SPEC `x:real` FLOOR)) THEN REWRITE_TAC[integer] THEN ASM_SIMP_TAC[real_abs; REAL_LE_FLOOR; FLOOR; INTEGER_CLOSED]);;
let FLOOR_DIV_DIV = 
prove (`!m n. ~(m = 0) ==> floor(&n / &m) = &(n DIV m)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; REAL_OF_NUM_LE; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; LT_NZ] THEN FIRST_X_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN ARITH_TAC);;
let FLOOR_MONO = 
prove (`!x y. x <= y ==> floor x <= floor y`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN SIMP_TAC[FLOOR; REAL_LT_INTEGERS] THEN MAP_EVERY (MP_TAC o C SPEC FLOOR) [`x:real`; `y:real`] THEN REAL_ARITH_TAC);;
let REAL_FLOOR_EQ = 
prove (`!x. floor x = x <=> integer x`,
REWRITE_TAC[GSYM FLOOR_UNIQUE; REAL_LE_REFL; REAL_ARITH `x < x + &1`]);;
let REAL_FLOOR_LT = 
prove (`!x. floor x < x <=> ~(integer x)`,
MESON_TAC[REAL_LT_LE; REAL_FLOOR_EQ; FLOOR]);;
let REAL_FRAC_EQ_0 = 
prove (`!x. frac x = &0 <=> integer x`,
REWRITE_TAC[FRAC_FLOOR; REAL_SUB_0] THEN MESON_TAC[REAL_FLOOR_EQ]);;
let REAL_FRAC_POS_LT = 
prove (`!x. &0 < frac x <=> ~(integer x)`,
let FRAC_NUM = 
prove (`!n. frac(&n) = &0`,
REWRITE_TAC[REAL_FRAC_EQ_0; INTEGER_CLOSED]);;
let REAL_FLOOR_REFL = 
prove (`!x. integer x ==> floor x = x`,
REWRITE_TAC[REAL_FLOOR_EQ]);;
let REAL_FRAC_ZERO = 
prove (`!x. integer x ==> frac x = &0`,
REWRITE_TAC[REAL_FRAC_EQ_0]);;
let REAL_FLOOR_ADD = 
prove (`!x y. floor(x + y) = if frac x + frac y < &1 then floor(x) + floor(y) else (floor(x) + floor(y)) + &1`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN CONJ_TAC THENL [ASM_MESON_TAC[INTEGER_CLOSED; FLOOR]; ALL_TAC] THEN MAP_EVERY (MP_TAC o C SPEC FLOOR_FRAC)[`x:real`; `y:real`; `x + y:real`] THEN REAL_ARITH_TAC);;
let REAL_FRAC_ADD = 
prove (`!x y. frac(x + y) = if frac x + frac y < &1 then frac(x) + frac(y) else (frac(x) + frac(y)) - &1`,
REWRITE_TAC[FRAC_FLOOR; REAL_FLOOR_ADD] THEN REAL_ARITH_TAC);;
let FLOOR_POS_LE = 
prove (`!x. &0 <= floor x <=> &0 <= x`,
let FRAC_UNIQUE = 
prove (`!x a. integer(x - a) /\ &0 <= a /\ a < &1 <=> frac x = a`,
REWRITE_TAC[FRAC_FLOOR; REAL_ARITH `x - f:real = a <=> f = x - a`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN AP_TERM_TAC THEN REAL_ARITH_TAC);;
let REAL_FRAC_EQ = 
prove (`!x. frac x = x <=> &0 <= x /\ x < &1`,
REWRITE_TAC[GSYM FRAC_UNIQUE; REAL_SUB_REFL; INTEGER_CLOSED]);;
let INTEGER_ROUND = 
prove (`!x. ?n. integer n /\ abs(x - n) <= &1 / &2`,
GEN_TAC THEN MATCH_MP_TAC(MESON[] `!a. P a \/ P(a + &1) ==> ?x. P x`) THEN EXISTS_TAC `floor x` THEN MP_TAC(ISPEC `x:real` FLOOR) THEN SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Assertions that there are integers between well-spaced reals. *) (* ------------------------------------------------------------------------- *)
let INTEGER_EXISTS_BETWEEN_ALT = 
prove (`!x y. x + &1 <= y ==> ?n. integer n /\ x < n /\ n <= y`,
REPEAT STRIP_TAC THEN EXISTS_TAC `floor y` THEN MP_TAC(SPEC `y:real` FLOOR) THEN SIMP_TAC[] THEN ASM_REAL_ARITH_TAC);;
let INTEGER_EXISTS_BETWEEN_LT = 
prove (`!x y. x + &1 < y ==> ?n. integer n /\ x < n /\ n < y`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `integer y` THENL [EXISTS_TAC `y - &1:real` THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC; FIRST_ASSUM(MP_TAC o MATCH_MP INTEGER_EXISTS_BETWEEN_ALT o MATCH_MP REAL_LT_IMP_LE) THEN MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_LT_LE] THEN ASM_MESON_TAC[]]);;
let INTEGER_EXISTS_BETWEEN = 
prove (`!x y. x + &1 <= y ==> ?n. integer n /\ x <= n /\ n < y`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `integer y` THENL [EXISTS_TAC `y - &1:real` THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC; FIRST_ASSUM(MP_TAC o MATCH_MP INTEGER_EXISTS_BETWEEN_ALT) THEN MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_LT_LE] THENL [ASM_REAL_ARITH_TAC; ASM_MESON_TAC[]]]);;
let INTEGER_EXISTS_BETWEEN_ABS = 
prove (`!x y. &1 <= abs(x - y) ==> ?n. integer n /\ (x <= n /\ n < y \/ y <= n /\ n < x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[real_abs] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THENL [MP_TAC(ISPECL [`y:real`; `x:real`] INTEGER_EXISTS_BETWEEN); MP_TAC(ISPECL [`x:real`; `y:real`] INTEGER_EXISTS_BETWEEN)] THEN (ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS]) THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
let INTEGER_EXISTS_BETWEEN_ABS_LT = 
prove (`!x y. &1 < abs(x - y) ==> ?n. integer n /\ (x < n /\ n < y \/ y < n /\ n < x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[real_abs] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THENL [MP_TAC(ISPECL [`y:real`; `x:real`] INTEGER_EXISTS_BETWEEN_LT); MP_TAC(ISPECL [`x:real`; `y:real`] INTEGER_EXISTS_BETWEEN_LT)] THEN (ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS]) THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *) (* A couple more theorems about real_of_int. *) (* ------------------------------------------------------------------------- *)
let INT_OF_REAL_OF_INT = 
prove (`!i. int_of_real(real_of_int i) = i`,
REWRITE_TAC[int_abstr]);;
let REAL_OF_INT_OF_REAL = 
prove (`!x. integer(x) ==> real_of_int(int_of_real x) = x`,
SIMP_TAC[int_rep]);;
(* ------------------------------------------------------------------------- *) (* Finiteness of bounded set of integers. *) (* ------------------------------------------------------------------------- *)
let HAS_SIZE_INTSEG_NUM = 
prove (`!m n. {x | integer(x) /\ &m <= x /\ x <= &n} HAS_SIZE ((n + 1) - m)`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `{x | integer(x) /\ &m <= x /\ x <= &n} = IMAGE real_of_num (m..n)` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `x:real` THEN ASM_CASES_TAC `?k. x = &k` THENL [FIRST_X_ASSUM(CHOOSE_THEN SUBST_ALL_TAC) THEN REWRITE_TAC[REAL_OF_NUM_LE; INTEGER_CLOSED; REAL_OF_NUM_EQ] THEN REWRITE_TAC[UNWIND_THM1; IN_NUMSEG]; ASM_MESON_TAC[INTEGER_POS; REAL_ARITH `&n <= x ==> &0 <= x`]]; MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN REWRITE_TAC[HAS_SIZE_NUMSEG] THEN SIMP_TAC[REAL_OF_NUM_EQ]]);;
let FINITE_INTSEG = 
prove (`!a b. FINITE {x | integer(x) /\ a <= x /\ x <= b}`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `max (abs a) (abs b)` REAL_ARCH_SIMPLE) THEN REWRITE_TAC[REAL_MAX_LE; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{x | integer(x) /\ abs(x) <= &n}` THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[SUBSET; IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `IMAGE (\x. &x) (0..n) UNION IMAGE (\x. --(&x)) (0..n)` THEN ASM_SIMP_TAC[FINITE_UNION; FINITE_IMAGE; FINITE_NUMSEG] THEN REWRITE_TAC[INTEGER_CASES; SUBSET; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[IN_UNION; IN_IMAGE; REAL_OF_NUM_EQ; REAL_EQ_NEG2] THEN REWRITE_TAC[UNWIND_THM1; IN_NUMSEG] THEN REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN ASM_REAL_ARITH_TAC);;
let HAS_SIZE_INTSEG_INT = 
prove (`!a b. integer a /\ integer b ==> {x | integer(x) /\ a <= x /\ x <= b} HAS_SIZE if b < a then 0 else num_of_int(int_of_real(b - a + &1))`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `{x | integer(x) /\ a <= x /\ x <= b} = IMAGE (\n. a + &n) {n | &n <= b - a}` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN ASM_SIMP_TAC[IN_ELIM_THM; INTEGER_CLOSED] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN X_GEN_TAC `c:real` THEN STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `a + x:real = y <=> y - a = x`] THEN ASM_SIMP_TAC[GSYM INTEGER_POS; REAL_SUB_LE; INTEGER_CLOSED]; MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN SIMP_TAC[REAL_EQ_ADD_LCANCEL; REAL_OF_NUM_EQ] THEN COND_CASES_TAC THENL [ASM_SIMP_TAC[REAL_ARITH `b < a ==> ~(&n <= b - a)`] THEN REWRITE_TAC[HAS_SIZE_0; EMPTY_GSPEC]; SUBGOAL_THEN `?m. b - a = &m` (CHOOSE_THEN SUBST1_TAC) THENL [ASM_MESON_TAC[INTEGER_POS; INTEGER_CLOSED; REAL_NOT_LT; REAL_SUB_LE]; REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; GSYM int_of_num; NUM_OF_INT_OF_NUM; HAS_SIZE_NUMSEG_LE]]]]);;
let CARD_INTSEG_INT = 
prove (`!a b. integer a /\ integer b ==> CARD {x | integer(x) /\ a <= x /\ x <= b} = if b < a then 0 else num_of_int(int_of_real(b - a + &1))`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP HAS_SIZE_INTSEG_INT) THEN SIMP_TAC[HAS_SIZE]);;
let REAL_CARD_INTSEG_INT = 
prove (`!a b. integer a /\ integer b ==> &(CARD {x | integer(x) /\ a <= x /\ x <= b}) = if b < a then &0 else b - a + &1`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[CARD_INTSEG_INT] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_OF_INT_OF_REAL] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM int_of_num_th] THEN W(MP_TAC o PART_MATCH (lhs o rand) INT_OF_NUM_OF_INT o rand o lhand o snd) THEN ANTS_TAC THENL [ASM_SIMP_TAC[int_le; int_of_num_th; REAL_OF_INT_OF_REAL; INTEGER_CLOSED] THEN ASM_REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC REAL_OF_INT_OF_REAL THEN ASM_SIMP_TAC[INTEGER_CLOSED]]);;
(* ------------------------------------------------------------------------- *) (* Yet set of all integers or rationals is infinite. *) (* ------------------------------------------------------------------------- *)
let INFINITE_INTEGER = 
prove (`INFINITE integer`,
SUBGOAL_THEN `INFINITE(IMAGE real_of_num (:num))` MP_TAC THENL [SIMP_TAC[INFINITE_IMAGE_INJ; REAL_OF_NUM_EQ; num_INFINITE]; ALL_TAC] THEN REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV] THEN REWRITE_TAC[IN; INTEGER_CLOSED]);;
let INFINITE_RATIONAL = 
prove (`INFINITE rational`,
MP_TAC INFINITE_INTEGER THEN REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN REWRITE_TAC[SUBSET; IN; RATIONAL_INTEGER]);;
(* ------------------------------------------------------------------------- *) (* Arbitrarily good rational approximations. *) (* ------------------------------------------------------------------------- *)
let RATIONAL_APPROXIMATION = 
prove (`!x e. &0 < e ==> ?r. rational r /\ abs(r - x) < e`,
REPEAT STRIP_TAC THEN ABBREV_TAC `n = floor(inv e) + &1` THEN EXISTS_TAC `floor(n * x) / n` THEN EXPAND_TAC "n" THEN ASM_SIMP_TAC[RATIONAL_CLOSED; INTEGER_CLOSED; FLOOR] THEN SUBGOAL_THEN `&0 < n` ASSUME_TAC THENL [EXPAND_TAC "n" THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < x + &1`) THEN ASM_SIMP_TAC[FLOOR_POS_LE; REAL_LE_INV_EQ; REAL_LT_IMP_LE]; ASM_SIMP_TAC[REAL_FIELD `&0 < n ==> a / n - b = (a - n * b) / n`] THEN ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ; REAL_LT_IMP_NZ] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&1` THEN CONJ_TAC THENL [MP_TAC(SPEC `n * x:real` FLOOR) THEN REAL_ARITH_TAC; ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN MATCH_MP_TAC(REAL_ARITH `inv e < n ==> &1 / e < abs n`) THEN EXPAND_TAC "n" THEN MP_TAC(SPEC `inv e` FLOOR) THEN REAL_ARITH_TAC]]);;
let RATIONAL_BETWEEN = 
prove (`!a b. a < b ==> ?q. rational q /\ a < q /\ q < b`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`(a + b) / &2`; `(b - a) / &4`] RATIONAL_APPROXIMATION) THEN ANTS_TAC THENL [ALL_TAC; MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[]] THEN ASM_REAL_ARITH_TAC);;
let RATIONAL_APPROXIMATION_STRADDLE = 
prove (`!x e. &0 < e ==> ?a b. rational a /\ rational b /\ a < x /\ x < b /\ abs(b - a) < e`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`x - e / &4`; `e / &4`] RATIONAL_APPROXIMATION) THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC] THEN MP_TAC(ISPECL [`x + e / &4`; `e / &4`] RATIONAL_APPROXIMATION) THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC] THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);;