NUM_REDUCE_CONV : term -> thm

SYNOPSIS

Evaluate subexpressions built up from natural number numerals, by proof.

DESCRIPTION

When applied to a term, NUM_REDUCE_CONV performs a recursive bottom-up evaluation by proof of subterms 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 theorem that the original and reduced terms are equal.

FAILURE CONDITIONS

Never fails, but may have no effect.

EXAMPLE

  # NUM_REDUCE_CONV `(432 - 234) + 198`;;
  val it : thm = |- 432 - 234 + 198 = 396

  # NUM_REDUCE_CONV
      `if 100 < 200 then 2 EXP (8 DIV 2) else 3 EXP ((26 EXP 0) * 3)`;;
  val it : thm =
   |- (if 100 < 200 then 2 EXP (8 DIV 2) else 3 EXP (26 EXP 0 * 3)) = 16

  # NUM_REDUCE_CONV `(!x. f(x + 2 + 2) < f(x + 0)) ==> f(12 * x) = f(12 * 12)`;;
  val it : thm =
    |- (!x. f (x + 2 + 2) < f (x + 0)) ==> f (12 * x) = f (12 * 12) <=>
       (!x. f (x + 4) < f (x + 0)) ==> f (12 * x) = f 144