Maps an assertion over natural numbers to equivalent over reals.
DESCRIPTION
Given a term, with arbitrary quantifier alternations over the natural numbers,
NUM_TO_INT_CONV proves its equivalence to a term involving integer operations
and quantifiers. Some preprocessing removes certain natural-specific operations
such as PRE and cutoff subtraction, quantifiers are systematically
relativized to the set of positive integers.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# NUM_TO_INT_CONV `n - m <= n`;;
val it : thm =
|- n - m <= n <=>
(!i. ~(&0 <= i) \/
(~(&m = &n + i) \/ &0 <= &n) /\ (~(&n = &m + i) \/ i <= &n))
USES
Mostly intended as a preprocessing step to allow rules for the integers to
deduce facts about natural numbers too.