Example (22.1) - ATPとCASのこと

　今回からは， $2$ 以上の任意の整数 $n$ に対して，
　 $\sum_{k=1}^{n}\frac{1}{k}$
は整数にならないことを証明していきます．方針は，この和を整数とおき， $2^x\le n<2^{x+1}$ となる偶数 $2^x$ を掛けると，適当な偶数 $a,c$ ，奇数 $b$ が存在して $1+\frac{a}{b}=c$ となり不合理というものです．

　最初は，任意の正の整数 $n$ に対して，適当な非負の整数 $x$ ，正の奇数 $y$ が存在して $n=2^xy$ となることの証明からです．

g`!n. ~(n = 0) ==> ?x y. n = 2 EXP x * y /\ ODD y`;;
e(MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC);;
e(DISJ_CASES_THEN2 MP_TAC ASSUME_TAC (SPEC_ALL EVEN_OR_ODD));;
e(SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC);;
e(SUBGOAL_THEN `m < n /\ ~(m = 0)` ASSUME_TAC THENL 
  [ASM_ARITH_TAC;
   FIRST_X_ASSUM(MP_TAC o (SPEC`m:num`)) THEN 
   ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC]);;
e(ASM_MESON_TAC[EXP; MULT_ASSOC]);;
e(ASM_MESON_TAC[EXP; MULT_ASSOC; MULT_CLAUSES]);;
(*
e(MAP_EVERY EXISTS_TAC [`SUC x`;`y:num`] THEN 
  ASM_SIMP_TAC[EXP; MULT_ASSOC]);;
e(MAP_EVERY EXISTS_TAC [`0`;`n:num`] THEN 
  ASM_SIMP_TAC[EXP; MULT_ASSOC; MULT_CLAUSES]);;
*)
let base2 = top_thm();;

　その後，試しに検索すると

# search[`2 EXP x`;`ODD y`];;
val it : (string * thm) list =
  [("EVEN_ODD_DECOMPOSITION",
    |- !n. (?k m. ODD m /\ n = 2 EXP k * m) <=> ~(n = 0));
   ("base2", |- !n. ~(n = 0) ==> (?x y. n = 2 EXP x * y /\ ODD y))]

となり，このEVEN_ODD_DECOMPOSITIONはarith.mlで証明されていることが判りましたが，やや長いように思えます．