floor

　今回は，床関数の性質の一つです．定義に近い形で進めるなら

g `!x m. floor (x + &m) = floor x + &m`;;
e(REPEAT GEN_TAC);;
e(MAP_EVERY ASSUME_TAC [SPEC`x + &m`FLOOR; SPEC`x:real`FLOOR]);;
e(SUBGOAL_TAC""`integer (floor x + &m)`[ASM_SIMP_TAC[INTEGER_CLOSED]]);;
e(ASM_SIMP_TAC[REAL_EQ_INTEGERS] THEN ASM_ARITH_TAC);;

または

g `!x m. floor (x + &m) = floor x + &m`;;
e(REPEAT GEN_TAC);;
e(MAP_EVERY ASSUME_TAC [SPEC`x + &m`FLOOR; 
                        SPEC`x:real`FLOOR; 
                        MESON[FLOOR; INTEGER_CLOSED]`integer (floor x + &m)`]);;
e(ASM_SIMP_TAC[REAL_EQ_INTEGERS] THEN ASM_ARITH_TAC);;

或いは

# [REAL_FLOOR_ADD; FLOOR_FRAC; FRAC_NUM; REAL_ADD_RID; FLOOR_NUM];;
val it : thm list =
  [|- !x y.
          floor (x + y) =
          (if frac x + frac y < &1
           then floor x + floor y
           else (floor x + floor y) + &1);
   |- !x. integer (floor x) /\
          &0 <= frac x /\
          frac x < &1 /\
          x = floor x + frac x;
   |- !n. frac (&n) = &0; |- !x. x + &0 = x; |- !n. floor (&n) = &n]

を参照するなら

# prove(`!x m. floor (x + &m) = floor x + &m`,SIMP_TAC it);;
val it : thm = |- !x m. floor (x + &m) = floor x + &m

となり，符号を考慮して

let thm20120127_1 = prove
 (`!x m. floor (x + &m) = floor x + &m`,
  SIMP_TAC[REAL_FLOOR_ADD; FLOOR_FRAC; FRAC_NUM; REAL_ADD_RID; FLOOR_NUM]);;

let thm20120127_2 = prove
 (`!x m. floor (x - &m) = floor x - &m`,
  MESON_TAC[REAL_EQ_SUB_LADD; REAL_SUB_ADD; thm20120107_1]);;

let thm20120127_3 = prove
 (`!x y. integer y ==> floor (x + y) = floor x + y`,
  REPEAT GEN_TAC THEN SIMP_TAC[is_int] THEN REPEAT STRIP_TAC THENL
  [ASM_SIMP_TAC[thm20120107_1];
   ASM_SIMP_TAC[thm20120107_2; GSYM real_sub]]);;

を得ます．
　なお，最初からintegerで行くなら

let thm20120127_4 = prove
 (`!x y. integer y ==> floor (x + y) = floor x + y`,
  SIMP_TAC[REAL_FLOOR_ADD; FLOOR_FRAC; REAL_FRAC_ZERO; REAL_ADD_RID; REAL_FLOOR_REFL]);;

が簡明です．