NUMBER_RULE : term -> thm

SYNOPSIS

Automatically prove elementary divisibility property over the natural numbers.

DESCRIPTION

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.

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')