それでも HOL4 には．．．

METIS があります．HOL Light には MESON しかなく，口惜しい限りです．

load "dividesTheory";
open dividesTheory;
val ARITH_RULE = SIMP_CONV(arith_ss++ARITH_ss)[divides_def];
val lem = ARITH_RULE ``~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5=0:num) /\ ~(6=0:num) /\ ~(7=0:num) /\ ~(8=0:num) /\ (!m:num. m<=9 ==> (m=0) \/ (m=1) \/ (m=2) \/ (m=3) \/ (m=4) \/ (m=5) \/ (m=6) \/ (m=7) \/ (m=8) \/ (m=9) ) /\ ~(divides 2 9) /\ ~(divides 4 9) /\ ~(divides 5 9) /\ ~(divides 6 9) /\ ~(divides 7 9) /\ ~(divides 8 9)``;
METIS_PROVE[ZERO_DIVIDES, DIVIDES_LEQ_OR_ZERO, lem]``!m:num. divides m 9 ==> (m=1) \/ (m=3) \/ (m=9)``;

- val lem = ARITH_RULE ``~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5=0:num) /\ ~(6=0:num) /\ ~(7=0:num) /\ ~(8=0:num) /\ (!m:num. m<=9 ==> (m=0) \/ (m=1) \/ (m=2) \/ (m=3) \/ (m=4) \/ (m=5) \/ (m=6) \/ (m=7) \/ (m=8) \/ (m=9) ) /\ ~(divides 2 9) /\ ~(divides 4 9) /\ ~(divides 5 9) /\ ~(divides 6 9) /\ ~(divides 7 9) /\ ~(divides 8 9)``;
> val lem =
     []
    |- 9 <> 0 /\ 2 <> 0 /\ 4 <> 0 /\ 5 <> 0 /\ 6 <> 0 /\ 7 <> 0 /\ 8 <> 0 /\
       (!m.
          m <= 9 ==>
          (m = 0) \/ (m = 1) \/ (m = 2) \/ (m = 3) \/ (m = 4) \/ (m = 5) \/
          (m = 6) \/ (m = 7) \/ (m = 8) \/ (m = 9)) /\ ~divides 2 9 /\
       ~divides 4 9 /\ ~divides 5 9 /\ ~divides 6 9 /\ ~divides 7 9 /\
       ~divides 8 9 <=> T : thm
- METIS_PROVE[ZERO_DIVIDES, DIVIDES_LEQ_OR_ZERO, lem]``!m:num. divides m 9 ==> (m=1) \/ (m=3) \/ (m=9)``;
metis: r[+0+22]+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+1+0+1+1+1+1+1+1+3+1#
> val it =
     [] |- !m. divides m 9 ==> (m = 1) \/ (m = 3) \/ (m = 9)
     : thm

同じことを HOL Light でやっても

# let lem = ARITH_RULE `~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5=0:num) /\
~(6=0:num) /\ ~(7=0:num) /\ ~(8=0:num) /\ (!m:num. 1<=m /\ m<=9 ==> (m=1) \/ (m=
2) \/ (m=3) \/ (m=4) \/ (m=5) \/ (m=6) \/ (m=7) \/ (m=8) \/ (m=9) ) /\ ~(9 MOD 2
=0:num) /\ ~(9 MOD 4=0:num) /\ ~(9 MOD 5=0:num) /\ ~(9 MOD 6=0:num) /\ ~(9 MOD 7
=0:num) /\ ~(9 MOD 8=0:num)`;;
val lem : thm =
  |- ~(9 = 0) /\
     ~(2 = 0) /\
     ~(4 = 0) /\
     ~(5 = 0) /\
     ~(6 = 0) /\
     ~(7 = 0) /\
     ~(8 = 0) /\
     (!m. 1 <= m /\ m <= 9
          ==> m = 1 \/
              m = 2 \/
              m = 3 \/
              m = 4 \/
              m = 5 \/
              m = 6 \/
              m = 7 \/
              m = 8 \/
              m = 9) /\
     ~(9 MOD 2 = 0) /\
     ~(9 MOD 4 = 0) /\
     ~(9 MOD 5 = 0) /\
     ~(9 MOD 6 = 0) /\
     ~(9 MOD 7 = 0) /\
     ~(9 MOD 8 = 0)
# MESON[DIVIDES_LE_STRONG; DIVIDES_MOD; lem] `m divides 9 ==> m=1 \/ m=3 \/ m=9`
;;
0..0..16..39..160..324..539..925..1401..1967..3947..6083..8708..13922..20425..27
447..42673..60257..79062..121878..171932..226393..358326..511500..674976..113476
9..1664765..2227624..4073497..6188804..8436365..

．．．終わりそうにありません．

ここで参照している２つの定理は，HOL4 にはないので

- val DIVIDES_LE_STRONG = METIS_PROVE[ZERO_DIVIDES, DIVIDES_LEQ_OR_ZERO, ARITH_C
ONV``!m:num. ~(m=0)==>1<=m``]``!m n:num. divides m n ==> (1 <= m /\ m <= n \/ (n
 = 0))``;
metis: r[+0+8]+0+0+0+0+0+0+1+0+1+4+1#
> val DIVIDES_LE_STRONG =
     [] |- !m n. divides m n ==> 1 <= m /\ m <= n \/ (n = 0) : thm

- val DIVIDES_MOD = METIS_PROVE [ARITH_SIMP[]``!b:num. b MOD 1 = 0``, ARITH_SIMP
[]``!a:num. a<>0 /\ a<>0 ==> (0 MOD a = 0)``, compute_divides] ``!m n:num. ~(m =
 0) ==> (divides m n <=> (n MOD m = 0))``;
metis: r[+0+15]+0+0+0+0+0+0+0+0+0+0+0+0+0+1+1#
r[+0+15]+0+0+0+0+0+0+0+0+0+0+1+0+0+0+0+1+2+2+1#
> val DIVIDES_MOD =  [] |- !m n. m <> 0 ==> (divides m n <=> (n MOD m = 0)) :
  thm

のように新作し，同じ仮定を与えて METIS に渡すと

- val lem = ARITH_SIMP[] ``~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5=0:num)
/\ ~(6=0:num) /\ ~(7=0:num) /\ ~(8=0:num) /\ (!m:num. 1<=m /\ m<=9 ==> (m=1) \/
(m=2) \/ (m=3) \/ (m=4) \/ (m=5) \/ (m=6) \/ (m=7) \/ (m=8) \/ (m=9) ) /\ ~(9 MO
D 2=0:num) /\ ~(9 MOD 4=0:num) /\ ~(9 MOD 5=0:num) /\ ~(9 MOD 6=0:num) /\ ~(9 MO
D 7=0:num) /\ ~(9 MOD 8=0:num)``;
> val lem =
     []
    |- 9 <> 0 /\ 2 <> 0 /\ 4 <> 0 /\ 5 <> 0 /\ 6 <> 0 /\ 7 <> 0 /\ 8 <> 0 /\
       (!m.
          1 <= m /\ m <= 9 ==>
          (m = 1) \/ (m = 2) \/ (m = 3) \/ (m = 4) \/ (m = 5) \/ (m = 6) \/
          (m = 7) \/ (m = 8) \/ (m = 9)) /\ 9 MOD 2 <> 0 /\ 9 MOD 4 <> 0 /\
       9 MOD 5 <> 0 /\ 9 MOD 6 <> 0 /\ 9 MOD 7 <> 0 /\ 9 MOD 8 <> 0 <=> T : thm

- METIS_PROVE[DIVIDES_LE_STRONG, DIVIDES_MOD, lem] ``!m:num. divides m 9 ==> (m=
1) \/ (m=3) \/ (m=9)``;
metis: r[+0+23]+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+1+0+1+1+0+2+0+0+0+2+2+0+1+1+
1+1+1+1+1+1+2+1#
> val it =  [] |- !m. divides m 9 ==> (m = 1) \/ (m = 3) \/ (m = 9) : thm

と即答です．勿論，HOL4 に PROVE として実装されている MESON では延々です．