RW_TAC : simpset -> thm list -> tactic
STRUCTURE
SYNOPSIS
Simplification with case-splitting and built-in knowledge of declared datatypes.
DESCRIPTION
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
HOL  Kananaskis-13