Negates real polynomial while retaining canonical form.
DESCRIPTION
For many purposes it is useful to retain polynomials in a canonical form. For
more information on the usual normal form in HOL Light, see the function
REAL_POLY_CONV, which converts a polynomial to normal form while proving the
equivalence of the original and normalized forms. The function
REAL_POLY_NEG_CONV is a more delicate conversion that, given a term --p
where p is a real polynomial in normal form, returns a theorem |- --p = p'
where p' is in normal form.
FAILURE CONDITIONS
Fails if applied to a term that is not the negation of a real term. If negation
is applied to a polynomial in non-normal form, the overall normalization is not
guaranteed.
EXAMPLE
# REAL_POLY_NEG_CONV `--(x pow 2 + -- &1)`;;
val it : thm = |- --(x pow 2 + -- &1) = -- &1 * x pow 2 + &1
USES
More delicate polynomial operations than simply the direct normalization with
REAL_POLY_CONV.