有理整数の性質 by EXPAND_CASES_CONV.

# map(fun t-> MATCH_MP t (ARITH_RULE `~(5=0)`))[MOD_MOD_REFL; MOD_ADD_MO
D; MOD_MULT_MOD2];;
val it : thm list =
  [|- !m. m MOD 5 MOD 5 = m MOD 5;
   |- !a b. (a MOD 5 + b MOD 5) MOD 5 = (a + b) MOD 5;
   |- !m p. (m MOD 5 * p MOD 5) MOD 5 = (m * p) MOD 5]
# PV9 ([MATCH_MP (CONV_RULE NUM_REDUCE_CONV(EXPAND_CASES_CONV`!n.n<5==>
~((n EXP 2 + n + 1)MOD 5=0)`)) (ARITH_RULE `n MOD 5<5` ) ; EXP_2;] @ it)
 `!n. ~((n EXP 2 + n + 1) MOD 5 = 0)`;;
-------- Proof 1 --------

THEOREM PROVED

------ process 7788 exit (max_proofs) ------
CPU time (user): 0.479999999996
val it : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)

ヒントなしでも．．．

# [ARITH_RULE `~(5=0)`; MOD_MOD_REFL; MOD_ADD_MOD; MOD_MULT_MOD2];;
val it : thm list =
  [|- ~(5 = 0); |- !m n. ~(n = 0) ==> m MOD n MOD n = m MOD n;
   |- !a b n. ~(n = 0) ==> (a MOD n + b MOD n) MOD n = (a + b) MOD n;
   |- !m n p. ~(n = 0) ==> (m MOD n * p MOD n) MOD n = (m * p) MOD n]
# PV9 ([CONV_RULE NUM_REDUCE_CONV(EXPAND_CASES_CONV`!n.n<5==> ~((n EXP 2
 + n + 1)MOD 5=0)`); ARITH_RULE `!n.n MOD 5<5`; EXP_2;] @ it) `!n. ~((n
EXP 2 + n + 1) MOD 5 = 0)`;;
-------- Proof 1 --------

THEOREM PROVED

------ process 8412 exit (max_proofs) ------
CPU time (user): 357.666
val it : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)
# [ARITH_RULE `~(5=0)`; MOD_MOD_REFL; MOD_ADD_MOD; M||<
<<
となります．そして仮定を替えると
>>
>||
# map(REWRITE_RULE[ARITH_RULE`~(n=0)<=>0<n`])[MOD_MOD_REFL; MOD_ADD_MOD;
 MOD_MULT_MOD2];;
val it : thm list =
  [|- !m n. 0 < n ==> m MOD n MOD n = m MOD n;
   |- !a b n. 0 < n ==> (a MOD n + b MOD n) MOD n = (a + b) MOD n;
   |- !m n p. 0 < n ==> (m MOD n * p MOD n) MOD n = (m * p) MOD n]
# PV9 ([CONV_RULE NUM_REDUCE_CONV(EXPAND_CASES_CONV`!n.n<5==> ~((n EXP 2
 + n + 1)MOD 5=0)`); ARITH_RULE `!n.n MOD 5<5`; EXP_2;] @ it) `!n. ~((n
EXP 2 + n + 1) MOD 5 = 0)`;;
-------- Proof 1 --------

THEOREM PROVED

------ process 10064 exit (max_proofs) ------
CPU time (user): 0.717999999993
val it : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)

のように高速化しますが，仮定の前件に用いる `0 < 5` の証明がないにも拘らず，結論が得られている訳で，一見不可解です．

実は前件の `0 < n` に対して古典論理では `0 < 5 \/ ~(0 < 5)` が定理となり，`0 < 5` の場合は仮定の MOD の性質が適用でき，`~(0 < 5)` の場合には，`!n. n MOD 5<5` と併せて `\n. ~(n MOD 5 = 0)` が得られ，その n として n EXP 2 + n + 1 を用いれば直ちに結論となるという仕組みです．

# PV9 [] `~(0 < 5) /\ (!n. n MOD 5<5) ==> !n. ~((n EXP 2 + n + 1) MOD 5 = 0)` ;;
-------- Proof 1 --------

THEOREM PROVED

------ process 7948 exit (max_proofs) ------
CPU time (user): 0.224000000002
val it : thm =
  |- ~(0 < 5) /\ (!n. n MOD 5 < 5) ==> (!n. ~((n EXP 2 + n + 1) MOD 5 = 0))