----------------------------------------------------------------------
RW_TAC                                                       (bossLib)
----------------------------------------------------------------------
RW_TAC : simpset -> thm list -> tactic

SYNOPSIS
Simplification with case-splitting and built-in knowledge of
declared datatypes.

KEYWORDS
simplification, datatype.

DESCRIBE
{RW_TAC} is a simplification tactic that provides conditional and
contextual rewriting, and automatic invocation of conversions and decision
procedures in the course of simplification. An application {RW_TAC ss thl}
adds the theorems in {thl} to the simpset {ss} and proceeds to simplify the
goal.

The process is based upon the simplification procedures in {simpLib},
but is more persistent in attempting to apply rewrite rules. It
automatically incorporates relevant results from datatype declarations
(the most important of these are injectivity and distinctness of
constructors). It uses the current hypotheses when rewriting the
goal. It automatically performs case-splitting on conditional
expressions in the goal. It simplifies any equation between constructors
occurring in the goal or the hypotheses. It automatically substitutes
through the goal any assumption that is an equality {v = M} or {M = v},
if {v} is a variable not occurring in {M}.  It eliminates any boolean
variable or negated boolean variable occurring as a hypothesis. It
breaks down any conjunctions, disjunctions, double negations, or
existentials occurring as hypotheses. It keeps the goal in "stripped"
format so that the resulting goal will not be an implication or
universally quantified.

FAILURE
Never fails, but may diverge.

COMMENTS
The case splits arising from conditionals and disjunctions can result in
many unforeseen subgoals. In that case, {SIMP_TAC} or even {REWRITE_TAC}
should be used.

The automatic incorporation of datatype facts can be slow when operating
in a context with many datatypes (or a few large datatypes). In such cases,
{SRW_TAC} is preferable to {RW_TAC}.

SEEALSO
bossLib.SRW_TAC, bossLib.SIMP_TAC, Rewrite.REWRITE_TAC,
bossLib.Hol_datatype.

----------------------------------------------------------------------