REAL_RAT_REDUCE_CONV : conv

SYNOPSIS
Evaluate subexpressions built up from rational literals of type :real, by proof.

DESCRIPTION
When applied to a term, REAL_RAT_REDUCE_CONV performs a recursive bottom-up evaluation by proof of subterms built from rational 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 rational literals are integer literals (&n or -- &n), ratios (&p / &q or -- &p / &q), or decimals (#DDD.DDDD or #DDD.DDDDeNN). Any numeric result is always put in the form &p / &q or -- &p / &q with q > 1 and p and q sharing no common factor, or simply &p or -- &p when that is impossible.

FAILURE CONDITIONS
Never fails, but may have no effect.

EXAMPLE
  # REAL_RAT_REDUCE_CONV
     `#3.1415926535 < &355 / &113 /\ &355 / &113 < &3 + &1 / &7`;;
  val it : thm =
    |- #3.1415926535 < &355 / &113 /\ &355 / &113 < &3 + &1 / &7 <=> T

SEE ALSO
NUM_REDUCE_CONV, REAL_RAT_ABS_CONV, REAL_RAT_ADD_CONV, REAL_RAT_DIV_CONV, REAL_RAT_EQ_CONV, REAL_RAT_GE_CONV, REAL_RAT_GT_CONV, REAL_RAT_INV_CONV, REAL_RAT_LE_CONV, REAL_RAT_LT_CONV, REAL_RAT_MAX_CONV, REAL_RAT_MIN_CONV, REAL_RAT_MUL_CONV, REAL_RAT_NEG_CONV, REAL_RAT_POW_CONV, REAL_RAT_RED_CONV, REAL_RAT_SGN_CONV, REAL_RAT_SUB_CONV.