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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
\DOC REAL_POLY_CONV
\TYPE {REAL_POLY_CONV : term -> thm}
\SYNOPSIS
Converts a real polynomial into canonical form.
\DESCRIBE
Given a term of type {:real} that is built up using addition, subtraction,
negation, multiplication, and inversion and division of constants,
{REAL_POLY_CONV} converts it into a canonical polynomial form and returns a
theorem asserting the equivalence of the original and canonical terms. The
basic elements need not simply be variables or constants; anything not built up
using the operators given above will be considered `atomic' for the purposes of
this conversion, for example {inv(x)} where {x} is a variable. The canonical
polynomial form is a `multiplied out' sum of products, with the monomials
(product terms) ordered according to the canonical OCaml order on terms. In
particular, it is just {&0} if the polynomial is identically zero.
\FAILURE
Never fails, even if the term has the wrong type; in this case it merely
returns a reflexive theorem.
\EXAMPLE
This illustrates how terms are `multiplied out':
{
# REAL_POLY_CONV
`(x + &1) * (x pow 2 + &1) * (x pow 4 + &1)`;;
val it : thm =
|- (x + &1) * (x pow 2 + &1) * (x pow 4 + &1) =
x pow 7 + x pow 6 + x pow 5 + x pow 4 + x pow 3 + x pow 2 + x + &1
}
\noindent and the following is an example of how a complicated algebraic
identity (due to Liouville?) simplifies to zero. Note that division is
permissible because it is only by constants.
{
# REAL_POLY_CONV
`((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
(x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) / &6 +
((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
(x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4) / &6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2`;;
val it : thm =
|- ((x1 + x2) pow 4 +
(x1 + x3) pow 4 +
(x1 + x4) pow 4 +
(x2 + x3) pow 4 +
(x2 + x4) pow 4 +
(x3 + x4) pow 4) /
&6 +
((x1 - x2) pow 4 +
(x1 - x3) pow 4 +
(x1 - x4) pow 4 +
(x2 - x3) pow 4 +
(x2 - x4) pow 4 +
(x3 - x4) pow 4) /
&6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2 =
&0
}
\USES
Keeping terms in normal form. For simply proving equalities, {REAL_RING} is
more powerful and usually more convenient.
\SEEALSO
INT_POLY_CONV, REAL_ARITH, REAL_RING, SEMIRING_NORMALIZERS_CONV.
\ENDDOC
|
