NUM_RED_CONV : term -> thm

SYNOPSIS

Performs one arithmetic or relational operation on natural number numerals by proof.

DESCRIPTION

When applied to a term that is either a unary operator application `SUC n`, `PRE n` or `FACT n` for a numeral n, or a relational operator application `m < n`, `m <= n`, `m > n`, `m >= n` or `m = n`, or a binary arithmetic operation `m + n`, `m - n`, `m * n`, `m EXP n`, `m DIV n` or `m MOD n` applied to numerals m and n, the conversion NUM_RED_CONV will `reduce' it and return a theorem asserting its equality to the reduced form.

FAILURE CONDITIONS

NUM_RED_CONV tm fails if tm is not of one of the forms specified.

EXAMPLE

  # NUM_RED_CONV `2 + 2`;;
  val it : thm = |- 2 + 2 = 4

  # NUM_RED_CONV `1089 < 2231`;;
  val it : thm = |- 1089 < 2231 <=> T

  # NUM_RED_CONV `FACT 11`;;
  val it : thm = |- FACT 11 = 39916800

Note that the immediate operands must be numerals. For deeper reduction of combinations of numerals, use NUM_REDUCE_CONV:

  # NUM_RED_CONV `(432 - 234) + 198`;;
  Exception: Failure "REWRITES_CONV".

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

USES

Access to this `one-step' reduction is not usually especially useful, but if you want to add a conversion conv for some other operator on numbers, you can conveniently incorporate it into NUM_REDUCE_CONV with

  # let NUM_REDUCE_CONV' = DEPTH_CONV(REAL_RAT_RED_CONV ORELSEC conv);;