MESON

　MESONは非常に優秀なproverであり，例えば

# let lemma = `!x:real. ?n:num. &1 <= x ==> &1 <= &n /\ floor x = &n`;;
val lemma : term = `!x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n`

の証明に必要な

# [FLOOR; integer; ABS_REFL; REAL_LE_FLOOR; INTEGER_CLOSED; REAL_LE_01; 
REAL_LE_TRANS];;
val it : thm list =
  [|- !x. integer (floor x) /\ floor x <= x /\ x < floor x + &1;
   |- !x. integer x <=> (?n. abs x = &n); |- !x. abs x = x <=> &0 <= x;
   |- !x n. integer n ==> (n <= floor x <=> n <= x);
   |- (!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));
   |- &0 <= &1; |- !x y z. x <= y /\ y <= z ==> x <= z]

を与えると

# MESON it lemma;;
0..0..0..1..2..3..4..5..6..13..20..27..40..53..66..100..134..168..245..322..399.
.586..773..960..1286..1612..1938..solved at 25598
val it : thm = |- !x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n

のように自動的に証明してくれます．
　そして，僅かなヒント（つまり，検索の範囲を狭めてやれば）を与えれば，検索ステップは大幅に減少します．

# MESON [integer; FLOOR; ABS_REFL; INTEGER_CLOSED; REAL_LE_FLOOR; REAL_LE_01; 
SPECL[`&0`;`&1`]REAL_LE_TRANS] lemma;;
0..0..0..1..2..3..4..5..6..11..16..21..30..39..48..66..84..102..148..194..240..346..452..558..735..912..1089..solved at 3637
val it : thm = |- !x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n
# MESON [integer; FLOOR; ABS_REFL; INTEGER_CLOSED; REAL_LE_FLOOR; 
REAL_ARITH `&1<= x ==> &0 <= x`] lemma;;
0..0..0..1..2..3..4..5..6..11..16..21..30..39..48..64..80..96..135..174..213..292..371..450..solved at 1525
val it : thm = |- !x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n
# MESON [integer; CONJUNCT1(SPEC_ALL FLOOR); ABS_REFL; SPEC`1`(CONJUNCT1 INTEGER_CLOSED); SPECL[`x:real`;`&1`]REAL_LE_FLOOR; REAL_ARITH `&1 <= x ==> &0 <= x`] lemma;;
0..0..solved at 2
0..0..0..1..2..3..5..7..9..14..19..24..34..44..54..72..90..108..150..192..234..solved at 1010
val it : thm = |- !x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n

　もし，MESONを使わずに，conversionやMPなどで済ませるなら，例えば

# let lemma001,lemma002,lemma003,lemma004,lemma005,lemma006=
  MP(fst(EQ_IMP_RULE(SPEC`floor x`integer)))(CONJUNCT1(SPEC_ALL FLOOR)),
  snd(EQ_IMP_RULE(MP(SPECL[`x:real`;`&1`]REAL_LE_FLOOR)(SPEC`1`(CONJUNCT1 INTEGER_CLOSED)))),
  IMP_TRANS(SPEC`floor x`(REAL_ARITH`!x. &1 <= x ==> &0 <= x`))(fst(EQ_IMP_RULE(SPEC`floor x`(GSYM ABS_REFL)))),
  CONV_RULE(REWRITE_CONV[UNDISCH lemma003])lemma001,
  DISCH_ALL(CONJ (ASSUME `&1 <= floor x`) lemma004),
  GEN`x:num`(CONV_RULE(REWRITE_CONV[RIGHT_AND_EXISTS_THM; RIGHT_IMP_EXISTS_THM; REAL_ARITH`a<=b /\ b=c <=> a<=c /\ b=c`])(IMP_TRANS lemma002 lemma005));;
val lemma001 : thm = |- ?n. abs (floor x) = &n
val lemma002 : thm = |- &1 <= x ==> &1 <= floor x
val lemma003 : thm = |- &1 <= floor x ==> abs (floor x) = floor x
val lemma004 : thm = &1 <= floor x |- ?n. floor x = &n
val lemma005 : thm = |- &1 <= floor x ==> &1 <= floor x /\ (?n. floor x = &n)
val lemma006 : thm = |- !x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n

のようになります．