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
|
\DOC INT_RED_CONV
\TYPE {INT_RED_CONV : term -> thm}
\SYNOPSIS
Performs one arithmetic or relational operation on integer literals of type
{:int}.
\DESCRIBE
When applied to any of the terms {`--c`}, {`abs c`}, {`c1 + c2`}, {`c1 - c2`},
{`c1 * c2`}, {`c pow n`}, {`c1 <= c2`}, {`c1 < c2`}, {`c1 >= c2`}, {`c1 > c2`},
{`c1 = c2`}, where {c}, {c1} and {c2} are integer literals of type {:int} and
{n} is a numeral of type {:num}, {INT_RED_CONV} returns a theorem
asserting the equivalence of the term to a canonical integer (for the
arithmetic operators) or a truth-value (for the relational operators). The
integer literals are terms of the form {&n} or {-- &n} (with nonzero {n} in the
latter case).
\FAILURE
Fails if applied to an inappropriate term.
\USES
More convenient for most purposes is {INT_REDUCE_CONV}, which applies
these evaluation conversions recursively at depth, or still more generally
{REAL_RAT_REDUCE_CONV} which applies to any rational numbers, not just
integers. Still, access to this `one-step' reduction can be handy if you want to
add a conversion {conv} for some other operator on int number literals, which
you can conveniently incorporate it into {INT_REDUCE_CONV} with
{
# let INT_REDUCE_CONV' =
DEPTH_CONV(INT_RED_CONV ORELSEC conv);;
}
\SEEALSO
INT_REDUCE_CONV, REAL_RAT_RED_CONV.
\ENDDOC
|
