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