1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
\DOC NUM_NORMALIZE_CONV
\TYPE {NUM_NORMALIZE_CONV : term -> thm}
\SYNOPSIS
Puts natural number expressions built using addition, multiplication and powers
in canonical polynomial form.
\DESCRIBE
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
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.
\SEEALSO
ARITH_RULE, NUM_REDUCE_CONV, NUM_RING, REAL_POLY_CONV,
SEMIRING_NORMALIZERS_CONV.
\ENDDOC
|
