`REAL_POLY_CONV : term -> thm`

SYNOPSIS
Converts a real polynomial into canonical form.

DESCRIPTION
Given a term of type :real that is built up using addition, subtraction, negation, multiplication, and inversion and division of constants, REAL_POLY_CONV converts it into a canonical polynomial form and returns a theorem asserting the equivalence of the original and canonical terms. The basic elements need not simply be variables or constants; anything not built up using the operators given above will be considered `atomic' for the purposes of this conversion, for example inv(x) where x is a variable. The canonical polynomial form is a `multiplied out' sum of products, with the monomials (product terms) ordered according to the canonical OCaml order on terms. In particular, it is just &0 if the polynomial is identically zero.

FAILURE CONDITIONS
Never fails, even if the term has the wrong type; in this case it merely returns a reflexive theorem.

EXAMPLE
This illustrates how terms are `multiplied out':
```  # REAL_POLY_CONV
`(x + &1) * (x pow 2 + &1) * (x pow 4 + &1)`;;
val it : thm =
|- (x + &1) * (x pow 2 + &1) * (x pow 4 + &1) =
x pow 7 + x pow 6 + x pow 5 + x pow 4 + x pow 3 + x pow 2 + x + &1
```
and the following is an example of how a complicated algebraic identity (due to Liouville?) simplifies to zero. Note that division is permissible because it is only by constants.
```  # REAL_POLY_CONV
`((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
(x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) / &6 +
((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
(x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4) / &6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2`;;
val it : thm =
|- ((x1 + x2) pow 4 +
(x1 + x3) pow 4 +
(x1 + x4) pow 4 +
(x2 + x3) pow 4 +
(x2 + x4) pow 4 +
(x3 + x4) pow 4) /
&6 +
((x1 - x2) pow 4 +
(x1 - x3) pow 4 +
(x1 - x4) pow 4 +
(x2 - x3) pow 4 +
(x2 - x4) pow 4 +
(x3 - x4) pow 4) /
&6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2 =
&0
```

USES
Keeping terms in normal form. For simply proving equalities, REAL_RING is more powerful and usually more convenient.