SIMP_TAC : simpset -> thm list -> tactic
STRUCTURE
SYNOPSIS
Simplifies the goal, using the given simpset and the additional theorems listed.
LIBRARY
simpLib
DESCRIPTION
SIMP_TAC adds the theorems of the second argument to the simpset argument as rewrites and then applies the resulting simpset to the conclusion of the goal. The exact behaviour of a simpset when applied to a term is described further in the entry for SIMP_CONV.

With simple simpsets, SIMP_TAC is similar in effect to REWRITE_TAC; it transforms the conclusion of a goal by using the (equational) theorems given and those already in the simpset as rewrite rules over the structure of the conclusion of the goal.

Just as ASM_REWRITE_TAC includes the assumptions of a goal in the rewrite rules that REWRITE_TAC uses, ASM_SIMP_TAC adds the assumptions of a goal to the rewrites and then performs simplification.

FAILURE
SIMP_TAC never fails, though it may diverge.
EXAMPLE
SIMP_TAC and the arith_ss simpset combine to prove quite difficult seeming goals:
   - val (_, p) = SIMP_TAC arith_ss []
                 ([], Term`P x /\ (x = y + 3) ==> P x /\ y < x`);

   > val p = fn : thm list -> thm

   - p [];
   > val it = |- P x /\ (x = y + 3) ==> P x /\ y < x : thm
SIMP_TAC is similar to REWRITE_TAC if used with just the bool_ss simpset. Here it is used in conjunction with the arithmetic theorem GREATER_DEF, |- !m n. m > n = n < m, to advance a goal:
   - SIMP_TAC bool_ss [GREATER_DEF]  ([], Term`T /\ 5 > 4 \/ F`);
   > val it = ([([], `4 < 5`)], fn) : subgoals

COMMENTS
The simplification library is described further in other documentation, but its full capabilities are still rather opaque.
USES
Simplification is one of the most powerful tactics available to the HOL user. It can be used both to solve goals entirely or to make progress with them. However, poor simpsets or a poor choice of rewrites can still result in divergence, or poor performance.

SEEALSO
HOL  Kananaskis-13