1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC REAL_IDEAL_CONV
\TYPE {REAL_IDEAL_CONV : term list -> term -> thm}
\SYNOPSIS
Produces identity proving ideal membership over the reals.
\DESCRIBE
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
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)
}
\SEEALSO
ideal_cofactors, real_ideal_cofactors, REAL_RING, RING, RING_AND_IDEAL_CONV.
\ENDDOC
|
