REAL_POLY_ADD_CONV : term -> thm

SYNOPSIS
Adds two real polynomials 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_ADD_CONV is a more delicate conversion that, given a term p1 + p2 where p1 and p2 are real polynomials in normal form, returns a theorem |- p1 + p2 = p where p is in normal form.

FAILURE CONDITIONS
Fails if applied to a term that is not the sum of two real terms. If these subterms are not polynomials in normal form, the overall normalization is not guaranteed.

EXAMPLE
  # REAL_POLY_ADD_CONV `(x pow 2 + x) + (x pow 2 + -- &1 * x + &1)`;;
  val it : thm =
    |- (x pow 2 + x) + x pow 2 + -- &1 * x + &1 = &2 * x pow 2 + &1

USES
More delicate polynomial operations that simply the direct normalization with REAL_POLY_CONV.

SEE ALSO
REAL_ARITH, REAL_POLY_CONV, REAL_POLY_MUL_CONV, REAL_POLY_NEG_CONV, REAL_POLY_POW_CONV, REAL_POLY_SUB_CONV, REAL_RING.