NUMBER_RULE : term -> thm
Automatically prove elementary divisibility property over the natural numbers.
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 CONDITIONS
Fails if the goal is not accessible to the methods used.
Here is a typical example, which would be rather tedious to prove manually:
`!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(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')
- SEE ALSO
ARITH_RULE, INTEGER_RULE, NUMBER_TAC, NUM_RING.