Evaluate subexpressions of goal built up from natural number numerals.
DESCRIPTION
When applied to a goal, NUM_REDUCE_TAC performs a recursive bottom-up
evaluation by proof of subterms of the conclusion built from numerals using the
unary operators `SUC', `PRE' and `FACT' and the binary arithmetic (`+',
`-', `*', `EXP', `DIV', `MOD') and relational (`<', `<=', `>',
`>=', `=') operators, as well as propagating constants through logical
operations, e.g. T /\ x <=> x, returning a new subgoal where all these
subexpressions are reduced.
FAILURE CONDITIONS
Never fails, but may have no effect.
EXAMPLE
# g `1 EXP 3 + 12 EXP 3 = 1729 /\ 9 EXP 3 + 10 EXP 3 = 1729`;;
val it : goalstack = 1 subgoal (1 total)
`1 EXP 3 + 12 EXP 3 = 1729 /\ 9 EXP 3 + 10 EXP 3 = 1729`
# e NUM_REDUCE_TAC;;
val it : goalstack = No subgoals