Source File | Identifier index | Theory binding index |
---|

(* ===================================================================== *) (* FILE : dep_rewrite.sig *) (* VERSION : 1.1 *) (* DESCRIPTION : Dependent Rewriting Tactics (general purpose) *) (* *) (* AUTHOR : Peter Vincent Homeier *) (* DATE : May 7, 2002 *) (* COPYRIGHT : Copyright (c) 2002 by Peter Vincent Homeier *) (* *) (* ===================================================================== *) (* ================================================================== *) (* ================================================================== *) (* DEPENDENT REWRITING TACTICS *) (* ================================================================== *) (* ================================================================== *) (* *) (* This file contains new tactics for dependent rewriting, *) (* a generalization of the rewriting tactics of standard HOL. *) (* *) (* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with *) (* the standard variations (PURE,ONCE,ASM). In addition, tactics *) (* with LIST instead of ONCE are provided, making 12 tactics in all. *) (* *) (* The argument theorems thm1,... are typically implications. *) (* These tactics identify the consequents of the argument theorems, *) (* and attempt to match these against the current goal. If a match *) (* is found, the goal is rewritten according to the matched instance *) (* of the consequent, after which the corresponding hypotheses of *) (* the argument theorems are added to the goal as new conjuncts on *) (* the left. *) (* *) (* Care needs to be taken that the implications will match the goal *) (* properly, that is, instances where the hypotheses in fact can be *) (* proven. Also, even more commonly than with REWRITE_TAC, *) (* the rewriting process may diverge. *) (* *) (* Each implication theorem for rewriting may have a number of layers *) (* of universal quantification and implications. At the bottom of *) (* these layers is the base, which will either be an equality, a *) (* negation, or a general term. The pattern for matching will be *) (* the left-hand-side of an equality, the term negated of a negation, *) (* or the term itself in the third case. The search is top-to-bottom,*) (* left-to-right, depending on the quantifications of variables. *) (* *) (* To assist in focusing the matching to useful cases, the goal is *) (* searched for a subterm matching the pattern. The matching of the *) (* pattern to subterms is performed by higher-order matching, so for *) (* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``. *) (* *) (* The argument theorems may each be either an implication or not. *) (* For those which are implications, the hypotheses of the instance *) (* of each theorem which matched the goal are added to the goal as *) (* conjuncts on the left side. For those argument theorems which *) (* are not implications, the goal is simply rewritten with them. *) (* This rewriting is also higher order. *) (* *) (* Deep inner universal quantifications of consequents are supported. *) (* Thus, an argument theorem like EQ_LIST: *) (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==> *) (* (CONS h1 l1 = CONS h2 l2)) *) (* before it is used, is internally converted to appear as *) (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==> *) (* (CONS h1 l1 = CONS h2 l2) *) (* *) (* As much as possible, the newly added hypotheses are analyzed to *) (* remove duplicates; thus, several theorems with the same *) (* hypothesis, or several uses of the same theorem, will generate *) (* a minimal additional proof burden. *) (* *) (* The new hypotheses are added as conjuncts rather than as a *) (* separate subgoal to reduce the user's burden of subgoal splits *) (* when creating tactics to prove theorems. If a separate subgoal *) (* is desired, simply use CONJ_TAC after the dependent rewriting to *) (* split the goal into two, where the first contains the hypotheses *) (* and the second contains the rewritten version of the original *) (* goal. *) (* *) (* The tactics including PURE in their name will only use the *) (* listed theorems for all rewriting; otherwise, the standard *) (* rewrites are used for normal rewriting, but they are not *) (* considered for dependent rewriting. *) (* *) (* The tactics including ONCE in their name attempt to use each *) (* theorem in the list, only once, in order, left to right. *) (* The hypotheses added in the process of dependent rewriting are *) (* not rewritten by the ONCE tactics. This gives a more restrained *) (* version of dependent rewriting. *) (* *) (* The tactics with LIST take a list of lists of theorems, and *) (* uses each list of theorems once in order, left-to-right. For *) (* each list of theorems, the goal is rewritten as much as possible, *) (* until no further changes can be achieved in the goal. Hypotheses *) (* are collected from all rewriting and added to the goal, but they *) (* are not themselves rewritten. *) (* *) (* The tactics without ONCE or LIST attempt to reuse all theorems *) (* repeatedly, continuing to rewrite until no changes can be *) (* achieved in the goal. Hypotheses are rewritten as well, and *) (* their hypotheses as well, ad infinitum. *) (* *) (* The tactics with ASM in their name add the assumption list to *) (* the list of theorems used for dependent rewriting. *) (* *) (* There are also three more general tactics provided, *) (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN, *) (* from which the others are constructed. *) (* *) (* The differences among these is that DEP_ONCE_FIND_THEN uses *) (* each of its theorems only once, in order left-to-right as given, *) (* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly *) (* as long as forward progress and change is possible. In contrast *) (* to the others, DEP_LIST_FIND_THEN takes as its argument a list *) (* of lists of theorems, and processes these in order, left-to-right. *) (* For each list of theorems, the goal is rewritten as many times *) (* as they apply. The hypotheses for all these rewritings are *) (* collected into one set, added to the goal after all rewritings. *) (* *) (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the *) (* hypotheses generated as a byproduct of the dependent rewriting; *) (* in contrast, DEP_FIND_THEN will. DEP_ONCE_FIND_THEN and *) (* DEP_LIST_FIND_THEN might be fruitfully applied again to their *) (* results; DEP_FIND_THEN will complete any possible rewriting, *) (* and need not be reapplied. *) (* *) (* These take as argument a thm_tactic, a function which takes a *) (* theorem and yields a tactic. It is this which is used to apply *) (* the instantiated consequent of each successfully matched *) (* implication to the current goal. Usually this is something like *) (* (fn th => REWRITE_TAC[th]), but the user is free to supply any *) (* thm_tactic he wishes. *) (* *) (* One significant note: because of the strategy of adding new *) (* hypotheses as conjuncts to the current goal, it is not fruitful *) (* to add *any* new assumptions to the current goal, as one might *) (* think would happen from using, say, ASSUME_TAC. *) (* *) (* Rather, any such new assumptions introduced by thm_tactic are *) (* specifically removed. Instead, one might wish to try MP_TAC, *) (* which will have the effect of ASSUME_TAC and then undischarging *) (* that assumption to become an antecedent of the goal. Other *) (* thm_tactics may be used, and they may even convert the single *) (* current subgoal into multiple subgoals. If this happens, it is *) (* fine, but note that the control strategy of DEP_FIND_THEN will *) (* continue to attack only the first of the multiple subgoals. *) (* *) (* ================================================================== *) (* ================================================================== *) signature dep_rewrite = sig include Abbrev (* ================================================================== *) (* *) (* The show_rewrites global flag determines whether information is *) (* printed showing the details of the process of matching and *) (* applying implication theorems against the current goal. The *) (* flag causes the following to be displayed: *) (* *) (* - Each implication theorem which is tried for matches against *) (* the current goal, *) (* - When a match is found, the matched version of the rewriting *) (* rule (just the base, not the hypotheses), *) (* - The new burden of hypotheses justifying the matched rewrite, *) (* - The revised goal after the rewrite. *) (* *) (* ================================================================== *) val show_rewrites : bool ref (* ================================================================== *) (* *) (* The tactics including ONCE in their name attempt to use each *) (* theorem in the list, only once, in order, left to right. *) (* The hypotheses added in the process of dependent rewriting are *) (* not rewritten by the ONCE tactics. This gives the most fine-grain *) (* control of dependent rewriting. *) (* *) (* ================================================================== *) val DEP_ONCE_FIND_THEN : thm_tactic -> thm list -> tactic val DEP_PURE_ONCE_REWRITE_TAC : thm list -> tactic val DEP_ONCE_REWRITE_TAC : thm list -> tactic val DEP_PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic val DEP_ONCE_ASM_REWRITE_TAC : thm list -> tactic val DEP_PURE_ONCE_SUBST_TAC : thm list -> tactic val DEP_ONCE_SUBST_TAC : thm list -> tactic val DEP_PURE_ONCE_ASM_SUBST_TAC : thm list -> tactic val DEP_ONCE_ASM_SUBST_TAC : thm list -> tactic (* ================================================================== *) (* *) (* The tactics including LIST in their name take a list of lists of *) (* implication theorems, and attempt to use each list of theorems *) (* once, in order, left to right. Each list of theorems is applied *) (* by rewriting with each theorem in it as many times as they apply. *) (* The hypotheses added in the process of dependent rewriting are *) (* collected from all rewritings, but they are not rewritten by the *) (* LIST tactics. This gives a moderate and more controlled degree *) (* of dependent rewriting than provided by DEP_REWRITE_TAC. *) (* *) (* ================================================================== *) val DEP_LIST_FIND_THEN : thm_tactic -> thm list list -> tactic val DEP_PURE_LIST_REWRITE_TAC : thm list list -> tactic val DEP_LIST_REWRITE_TAC : thm list list -> tactic val DEP_PURE_LIST_ASM_REWRITE_TAC : thm list list -> tactic val DEP_LIST_ASM_REWRITE_TAC : thm list list -> tactic (* ================================================================== *) (* *) (* The tactics without ONCE attept to reuse all theorems until no *) (* changes can be achieved in the goal. Hypotheses are rewritten *) (* and new ones generated from them, continuing until no further *) (* progress is possible. *) (* *) (* ================================================================== *) val DEP_FIND_THEN : thm_tactic -> thm list -> tactic val DEP_PURE_REWRITE_TAC : thm list -> tactic val DEP_REWRITE_TAC : thm list -> tactic val DEP_PURE_ASM_REWRITE_TAC : thm list -> tactic val DEP_ASM_REWRITE_TAC : thm list -> tactic end (* ================================================================== *) (* ================================================================== *) (* END OF DEPENDENT REWRITING TACTICS *) (* ================================================================== *) (* ================================================================== *)

Source File | Identifier index | Theory binding index |
---|