1\DOC RW_TAC
2
3\TYPE {RW_TAC : simpset -> thm list -> tactic}
4
5\SYNOPSIS
6Simplification with case-splitting and built-in knowledge of
7declared datatypes.
8
9\KEYWORDS
10simplification, datatype.
11
12\DESCRIBE
13{RW_TAC} is a simplification tactic that provides conditional and
14contextual rewriting, and automatic invocation of conversions and decision
15procedures in the course of simplification. An application {RW_TAC ss thl}
16adds the theorems in {thl} to the simpset {ss} and proceeds to simplify the
17goal.
18
19The process is based upon the simplification procedures in {simpLib},
20but is more persistent in attempting to apply rewrite rules. It
21automatically incorporates relevant results from datatype declarations
22(the most important of these are injectivity and distinctness of
23constructors). It uses the current hypotheses when rewriting the
24goal. It automatically performs case-splitting on conditional
25expressions in the goal. It simplifies any equation between constructors
26occurring in the goal or the hypotheses. It automatically substitutes
27through the goal any assumption that is an equality {v = M} or {M = v},
28if {v} is a variable not occurring in {M}.  It eliminates any boolean
29variable or negated boolean variable occurring as a hypothesis. It
30breaks down any conjunctions, disjunctions, double negations, or
31existentials occurring as hypotheses. It keeps the goal in "stripped"
32format so that the resulting goal will not be an implication or
33universally quantified.
34
35\FAILURE
36Never fails, but may diverge.
37
38\COMMENTS
39The case splits arising from conditionals and disjunctions can result in
40many unforeseen subgoals. In that case, {SIMP_TAC} or even {REWRITE_TAC}
41should be used.
42
43The automatic incorporation of datatype facts can be slow when operating
44in a context with many datatypes (or a few large datatypes). In such cases,
45{SRW_TAC} is preferable to {RW_TAC}.
46
47\SEEALSO
48bossLib.SRW_TAC, bossLib.SIMP_TAC, Rewrite.REWRITE_TAC, bossLib.Hol_datatype.
49
50\ENDDOC
51