REDUCE_TAC : tactic
STRUCTURE
reduceLib
SYNOPSIS
Performs arithmetic or boolean reduction on a goal at all levels possible.
LIBRARY
reduce
DESCRIPTION
REDUCE_TAC attempts to transform a goal by applying REDUCE_CONV. It will prove any true goal which is constructed from numerals and the boolean constants T and F.
FAILURE
Never fails, but may not advance the goal.
EXAMPLE
The following example takes a couple of minutes’ CPU time: 

   > g ‘((1 EXP 3) + (12 EXP 3) = 1729) /\ ((9 EXP 3) + (10 EXP 3) = 1729)’;

   > e reduceLib.REDUCE_TAC;;
   OK..
   val it = 
      Initial goal proved
      ⊢ 1 EXP 3 + 12 EXP 3 = 1729 ∧ 9 EXP 3 + 10 EXP 3 = 1729 : proof
SEEALSO
RED_CONV, REDUCE_CONV, REDUCE_RULE
HOL  Trindemossen-1