1\DOC DEP_REWRITE_TAC
2
3\TYPE {DEP_REWRITE_TAC : thm list -> tactic}
4
5\SYNOPSIS
6Rewrites a goal using implications of equalites, adding proof obligations as required.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12In a call {DEP_REWRITE_TAC [thm1,...]},
13the argument theorems {thm1,...} are typically implications.
14The tactic identifies the consequents of the argument theorems,
15and attempt to match these against the current goal.  If a match
16is found, the goal is rewritten according to the matched instance
17of the consequent, after which the corresponding hypotheses of
18the argument theorems are added to the goal as new conjuncts on
19the left.
20
21Care needs to be taken that the implications will match the goal
22properly, that is, instances where the hypotheses in fact can be
23proven.  Also, even more commonly than with {REWRITE_TAC},
24the rewriting process may diverge.
25
26Each implication theorem for rewriting may have a number of layers
27of universal quantification and implications.  At the bottom of
28these layers is the base, which will either be an equality, a
29negation, or a general term.  The pattern for matching will be
30the left-hand-side of an equality, the term negated of a negation,
31or the term itself in the third case.  The search is top-to-bottom
32left-to-right, depending on the quantifications of variables.
33
34To assist in focusing the matching to useful cases, the goal is
35searched for a subterm matching the pattern.  The matching of the
36pattern to subterms is performed by higher-order matching, so for
37example, {!x. P x} will match the term {!n. (n+m) < 4*n}.
38
39The argument theorems may each be either an implication or not.
40For those which are implications, the hypotheses of the instance
41of each theorem which matched the goal are added to the goal as
42conjuncts on the left side.  For those argument theorems which
43are not implications, the goal is simply rewritten with them.
44This rewriting is also higher order.
45
46\COMMENTS
47Deep inner universal quantifications of consequents are supported.
48Thus, an argument theorem like {EQ_LIST}:
49{
50|- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>
51                 (CONS h1 l1 = CONS h2 l2))
52}
53before it is used, is internally converted to appear as
54{
55|- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>
56                 (CONS h1 l1 = CONS h2 l2)
57}
58
59As much as possible, the newly added hypotheses are analyzed to
60remove duplicates; thus, several theorems with the same
61hypothesis, or several uses of the same theorem, will generate
62a minimal additional proof burden.
63
64The new hypotheses are added as conjuncts rather than as a
65separate subgoal to reduce the user's burden of subgoal splits
66when creating tactics to prove theorems.  If a separate subgoal
67is desired, simply use {CONJ_TAC} after the dependent rewriting to
68split the goal into two, where the first contains the hypotheses
69and the second contains the rewritten version of the original
70goal.
71
72\SEEALSO
73dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC, dep_rewrite.DEP_ONCE_REWRITE_TAC, dep_rewrite.DEP_PURE_ONCE_ASM_REWRITE_TAC, dep_rewrite.DEP_ONCE_ASM_REWRITE_TAC, dep_rewrite.DEP_PURE_ONCE_SUBST_TAC, dep_rewrite.DEP_ONCE_SUBST_TAC, dep_rewrite.DEP_PURE_ONCE_ASM_SUBST_TAC, dep_rewrite.DEP_ONCE_ASM_SUBST_TAC, dep_rewrite.DEP_PURE_LIST_REWRITE_TAC, dep_rewrite.DEP_LIST_REWRITE_TAC, dep_rewrite.DEP_PURE_LIST_ASM_REWRITE_TAC, dep_rewrite.DEP_LIST_ASM_REWRITE_TAC, dep_rewrite.DEP_PURE_REWRITE_TAC, dep_rewrite.DEP_REWRITE_TAC, dep_rewrite.DEP_PURE_ASM_REWRITE_TAC, dep_rewrite.DEP_ASM_REWRITE_TAC, dep_rewrite.DEP_FIND_THEN, dep_rewrite.DEP_LIST_FIND_THEN, dep_rewrite.DEP_ONCE_FIND_THEN.
74\ENDDOC
75