REAL_POLY_SUB_CONV : term -> thm
Subtracts two real polynomials while retaining canonical form.
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_SUB_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 difference of two real terms. If
these subterms are not polynomials in normal form, the overall normalization is
# REAL_POLY_SUB_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 + -- &1
More delicate polynomial operations that simply the direct normalization with
- SEE ALSO
REAL_ARITH, REAL_POLY_SUB_CONV, REAL_POLY_CONV, REAL_POLY_MUL_CONV,
REAL_POLY_NEG_CONV, REAL_POLY_POW_CONV, REAL_RING.