REAL_INT_REDUCE_CONV : conv
Evaluate subexpressions built up from integer literals of type :real, by
When applied to a term, REAL_INT_REDUCE_CONV performs a recursive bottom-up
evaluation by proof of subterms built from integer literals of type :real
using the unary operators `--', `inv' and `abs', and the binary
arithmetic (`+', `-', `*', `/', `pow') and relational (`<', `<=',
`>', `>=', `=') operators, as well as propagating literals through
logical operations, e.g. T /\ x <=> x, returning a theorem that the original
and reduced terms are equal. The permissible integer literals are of the form
&n or -- &n for numeral n, nonzero in the negative case.
- FAILURE CONDITIONS
Never fails, but may have no effect.
`if &5 pow 4 < &4 pow 5 then (&2 pow 3 - &1) pow 2 + &1 else &99`;;
val it : thm =
|- (if &5 pow 4 < &4 pow 5 then (&2 pow 3 - &1) pow 2 + &1 else &99) = &50
The corresponding INT_REDUCE_CONV works for the type of integers. The more
general function REAL_RAT_REDUCE_CONV works similarly over :real but for
arbitrary rational literals.
- SEE ALSO
NUM_REDUCE_CONV, INT_REDUCE_CONV, REAL_RAT_REDUCE_CONV.