Puts natural number expressions built using addition, multiplication and powers
in canonical polynomial form.
DESCRIPTION
Given a term t of natural number type built up from other ``atomic''
components (not necessarily simple variables) and numeral constants by
addition, multiplication and exponentiation by constant exponents,
NUM_NORMALIZE_CONV t will return |- t = t' where t' is the result of
putting the term into a normalized form, essentially a multiplied-out
polynomial with a specific ordering of and within monomials.
FAILURE CONDITIONS
Should never fail.
EXAMPLE
# NUM_NORMALIZE_CONV `1 + (1 + x + x EXP 2) * (x + (x * x) EXP 2)`;;
val it : thm =
|- 1 + (1 + x + x EXP 2) * (x + (x * x) EXP 2) =
x EXP 6 + x EXP 5 + x EXP 4 + x EXP 3 + x EXP 2 + x + 1
COMMENTS
This can be used to prove simple algebraic equations, but NUM_RING or
ARITH_RULE are generally more powerful and convenient for that. In
particular, this function does not handle cutoff subtraction or other such
operations.