REAL_IDEAL_CONV : term list -> term -> thm

SYNOPSIS

Produces identity proving ideal membership over the reals.

DESCRIPTION

The call REAL_IDEAL_CONV [`p1`; ...; `pn`] `p`, where all the terms have type :real and can be considered as polynomials, will test whether p is in the ideal generated by the p1,...,pn. If so, it will return a corresponding theorem |- p = q1 * p1 + ... + qn * pn showing how to express p in terms of the other polynomials via some `cofactors' qi.

FAILURE CONDITIONS

Fails if the terms are ill-typed, or if ideal membership fails.

EXAMPLE

In the case of a singleton list, this just corresponds to dividing one multivariate polynomial by another, e.g.

  # REAL_IDEAL_CONV [`x - &1`] `x pow 4 - &1`;;
  1 basis elements and 0 critical pairs
  val it : thm =
    |- x pow 4 - &1 = (&1 * x pow 3 + &1 * x pow 2 + &1 * x + &1) * (x - &1)