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