INTEGER_RULE : term -> thm

SYNOPSIS

Automatically prove elementary divisibility property over the integers.

DESCRIPTION

INTEGER_RULE is a partly heuristic rule that can often automatically prove elementary ``divisibility'' properties of the integers. 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. The examples below may give a feel for what can be done.

FAILURE CONDITIONS

Fails if the goal is not accessible to the methods used.

EXAMPLE

All sorts of elementary Boolean combinations of divisibility and congruence properties can be solved, e.g.

  # INTEGER_RULE
     `!x y n:int. (x == y) (mod n) ==> (n divides x <=> n divides y)`;;
  ...
  val it : thm = |- !x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)

  # INTEGER_RULE
     `!a b d:int. d divides gcd(a,b) <=> d divides a /\ d divides b`;;
  ...
  val it : thm =
   |- !a b d. d divides gcd (a,b) <=> d divides a /\ d divides b

including some less obvious ones:

  # INTEGER_RULE
     `!x y. coprime(x * y,x pow 2 + y pow 2) <=> coprime(x,y)`;;
  ...
  val it : thm = |- !x y. coprime (x * y,x pow 2 + y pow 2) <=> coprime (x,y)

A limited class of existential goals is solvable too, e.g. a classic sufficient condition for a linear congruence to have a solution:

  # INTEGER_RULE `!a b n:int. coprime(a,n) ==> ?x. (a * x == b) (mod n)`;;
  ...
  val it : thm = |- !a b n. coprime (a,n) ==> (?x. (a * x == b) (mod n))

or the two-number Chinese Remainder Theorem:

  # INTEGER_RULE
    `!a b u v:int. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`;;
  ...
  val it : thm =
  |- !a b u v. coprime (a,b) ==> (?x. (x == u) (mod a) /\ (x == v) (mod b))