1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
\DOC NUMBER_RULE
\TYPE {NUMBER_RULE : term -> thm}
\SYNOPSIS
Automatically prove elementary divisibility property over the natural numbers.
\DESCRIBE
{NUMBER_RULE} is a partly heuristic rule that can often automatically prove
elementary ``divisibility'' properties of the natural numbers. The precise
subset that is dealt with is difficult to describe rigorously, but many
universally quantified combinations of {divides}, {coprime}, {gcd} and
congruences {(x == y) (mod n)} can be proved automatically, as well as some
existentially quantified goals. See a similar rule {INTEGER_RULE} for the
integers for a representative set of examples.
\FAILURE
Fails if the goal is not accessible to the methods used.
\EXAMPLE
Here is a typical example, which would be rather tedious to prove manually:
{
# NUMBER_RULE
`!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
==> coprime(a',b')`;;
...
val it : thm =
|- !a b a' b'.
~(gcd (a,b) = 0) /\ a = a' * gcd (a,b) /\ b = b' * gcd (a,b)
==> coprime (a',b')
}
\SEEALSO
ARITH_RULE, INTEGER_RULE, NUMBER_TAC, NUM_RING.
\ENDDOC
|
