REDUCE_CONV : conv

- STRUCTURE
- SYNOPSIS
- Performs arithmetic or boolean reduction at all levels possible.
- LIBRARY
- reduce
- DESCRIPTION
- The conversion REDUCE_CONV attempts to apply, in bottom-up order to all suitable redexes, one of the following conversions from the reduce library (only one can succeed):In particular, it will prove the appropriate reduction for an arbitrarily complicated expression constructed from numerals and the boolean constants T and F.
ADD_CONV AND_CONV BEQ_CONV COND_CONV DIV_CONV EXP_CONV GE_CONV GT_CONV IMP_CONV LE_CONV LT_CONV MOD_CONV MUL_CONV NEQ_CONV NOT_CONV OR_CONV PRE_CONV SBC_CONV SUC_CONV

- FAILURE
- Never fails, but may give a reflexive equation.
- EXAMPLE
#REDUCE_CONV "(2=3) = F";; |- ((2 = 3) = F) = T #REDUCE_CONV "(100 < 200) => (2 EXP (8 DIV 2)) | (3 EXP ((26 EXP 0) * 3))";; |- (100 < 200 => 2 EXP (8 DIV 2) | 3 EXP ((26 EXP 0) * 3)) = 16 #REDUCE_CONV "(15 = 16) \/ (15 < 16)";; |- (15 = 16) \/ 15 < 16 = T #REDUCE_CONV "0 + x";; |- 0 + x = 0 + x

- SEEALSO

HOL Kananaskis-14