1(* ===================================================================== *) 2(* FILE : dep_rewrite.sig *) 3(* VERSION : 1.1 *) 4(* DESCRIPTION : Dependent Rewriting Tactics (general purpose) *) 5(* *) 6(* AUTHOR : Peter Vincent Homeier *) 7(* DATE : May 7, 2002 *) 8(* COPYRIGHT : Copyright (c) 2002 by Peter Vincent Homeier *) 9(* *) 10(* ===================================================================== *) 11 12(* ================================================================== *) 13(* ================================================================== *) 14(* DEPENDENT REWRITING TACTICS *) 15(* ================================================================== *) 16(* ================================================================== *) 17(* *) 18(* This file contains new tactics for dependent rewriting, *) 19(* a generalization of the rewriting tactics of standard HOL. *) 20(* *) 21(* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with *) 22(* the standard variations (PURE,ONCE,ASM). In addition, tactics *) 23(* with LIST instead of ONCE are provided, making 12 tactics in all. *) 24(* *) 25(* The argument theorems thm1,... are typically implications. *) 26(* These tactics identify the consequents of the argument theorems, *) 27(* and attempt to match these against the current goal. If a match *) 28(* is found, the goal is rewritten according to the matched instance *) 29(* of the consequent, after which the corresponding hypotheses of *) 30(* the argument theorems are added to the goal as new conjuncts on *) 31(* the left. *) 32(* *) 33(* Care needs to be taken that the implications will match the goal *) 34(* properly, that is, instances where the hypotheses in fact can be *) 35(* proven. Also, even more commonly than with REWRITE_TAC, *) 36(* the rewriting process may diverge. *) 37(* *) 38(* Each implication theorem for rewriting may have a number of layers *) 39(* of universal quantification and implications. At the bottom of *) 40(* these layers is the base, which will either be an equality, a *) 41(* negation, or a general term. The pattern for matching will be *) 42(* the left-hand-side of an equality, the term negated of a negation, *) 43(* or the term itself in the third case. The search is top-to-bottom,*) 44(* left-to-right, depending on the quantifications of variables. *) 45(* *) 46(* To assist in focusing the matching to useful cases, the goal is *) 47(* searched for a subterm matching the pattern. The matching of the *) 48(* pattern to subterms is performed by higher-order matching, so for *) 49(* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``. *) 50(* *) 51(* The argument theorems may each be either an implication or not. *) 52(* For those which are implications, the hypotheses of the instance *) 53(* of each theorem which matched the goal are added to the goal as *) 54(* conjuncts on the left side. For those argument theorems which *) 55(* are not implications, the goal is simply rewritten with them. *) 56(* This rewriting is also higher order. *) 57(* *) 58(* Deep inner universal quantifications of consequents are supported. *) 59(* Thus, an argument theorem like EQ_LIST: *) 60(* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==> *) 61(* (CONS h1 l1 = CONS h2 l2)) *) 62(* before it is used, is internally converted to appear as *) 63(* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==> *) 64(* (CONS h1 l1 = CONS h2 l2) *) 65(* *) 66(* As much as possible, the newly added hypotheses are analyzed to *) 67(* remove duplicates; thus, several theorems with the same *) 68(* hypothesis, or several uses of the same theorem, will generate *) 69(* a minimal additional proof burden. *) 70(* *) 71(* The new hypotheses are added as conjuncts rather than as a *) 72(* separate subgoal to reduce the user's burden of subgoal splits *) 73(* when creating tactics to prove theorems. If a separate subgoal *) 74(* is desired, simply use CONJ_TAC after the dependent rewriting to *) 75(* split the goal into two, where the first contains the hypotheses *) 76(* and the second contains the rewritten version of the original *) 77(* goal. *) 78(* *) 79(* The tactics including PURE in their name will only use the *) 80(* listed theorems for all rewriting; otherwise, the standard *) 81(* rewrites are used for normal rewriting, but they are not *) 82(* considered for dependent rewriting. *) 83(* *) 84(* The tactics including ONCE in their name attempt to use each *) 85(* theorem in the list, only once, in order, left to right. *) 86(* The hypotheses added in the process of dependent rewriting are *) 87(* not rewritten by the ONCE tactics. This gives a more restrained *) 88(* version of dependent rewriting. *) 89(* *) 90(* The tactics with LIST take a list of lists of theorems, and *) 91(* uses each list of theorems once in order, left-to-right. For *) 92(* each list of theorems, the goal is rewritten as much as possible, *) 93(* until no further changes can be achieved in the goal. Hypotheses *) 94(* are collected from all rewriting and added to the goal, but they *) 95(* are not themselves rewritten. *) 96(* *) 97(* The tactics without ONCE or LIST attempt to reuse all theorems *) 98(* repeatedly, continuing to rewrite until no changes can be *) 99(* achieved in the goal. Hypotheses are rewritten as well, and *) 100(* their hypotheses as well, ad infinitum. *) 101(* *) 102(* The tactics with ASM in their name add the assumption list to *) 103(* the list of theorems used for dependent rewriting. *) 104(* *) 105(* There are also three more general tactics provided, *) 106(* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN, *) 107(* from which the others are constructed. *) 108(* *) 109(* The differences among these is that DEP_ONCE_FIND_THEN uses *) 110(* each of its theorems only once, in order left-to-right as given, *) 111(* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly *) 112(* as long as forward progress and change is possible. In contrast *) 113(* to the others, DEP_LIST_FIND_THEN takes as its argument a list *) 114(* of lists of theorems, and processes these in order, left-to-right. *) 115(* For each list of theorems, the goal is rewritten as many times *) 116(* as they apply. The hypotheses for all these rewritings are *) 117(* collected into one set, added to the goal after all rewritings. *) 118(* *) 119(* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the *) 120(* hypotheses generated as a byproduct of the dependent rewriting; *) 121(* in contrast, DEP_FIND_THEN will. DEP_ONCE_FIND_THEN and *) 122(* DEP_LIST_FIND_THEN might be fruitfully applied again to their *) 123(* results; DEP_FIND_THEN will complete any possible rewriting, *) 124(* and need not be reapplied. *) 125(* *) 126(* These take as argument a thm_tactic, a function which takes a *) 127(* theorem and yields a tactic. It is this which is used to apply *) 128(* the instantiated consequent of each successfully matched *) 129(* implication to the current goal. Usually this is something like *) 130(* (fn th => REWRITE_TAC[th]), but the user is free to supply any *) 131(* thm_tactic he wishes. *) 132(* *) 133(* One significant note: because of the strategy of adding new *) 134(* hypotheses as conjuncts to the current goal, it is not fruitful *) 135(* to add *any* new assumptions to the current goal, as one might *) 136(* think would happen from using, say, ASSUME_TAC. *) 137(* *) 138(* Rather, any such new assumptions introduced by thm_tactic are *) 139(* specifically removed. Instead, one might wish to try MP_TAC, *) 140(* which will have the effect of ASSUME_TAC and then undischarging *) 141(* that assumption to become an antecedent of the goal. Other *) 142(* thm_tactics may be used, and they may even convert the single *) 143(* current subgoal into multiple subgoals. If this happens, it is *) 144(* fine, but note that the control strategy of DEP_FIND_THEN will *) 145(* continue to attack only the first of the multiple subgoals. *) 146(* *) 147(* ================================================================== *) 148(* ================================================================== *) 149 150signature dep_rewrite = 151sig 152include Abbrev 153 154 155(* ================================================================== *) 156(* *) 157(* The show_rewrites global flag determines whether information is *) 158(* printed showing the details of the process of matching and *) 159(* applying implication theorems against the current goal. The *) 160(* flag causes the following to be displayed: *) 161(* *) 162(* - Each implication theorem which is tried for matches against *) 163(* the current goal, *) 164(* - When a match is found, the matched version of the rewriting *) 165(* rule (just the base, not the hypotheses), *) 166(* - The new burden of hypotheses justifying the matched rewrite, *) 167(* - The revised goal after the rewrite. *) 168(* *) 169(* ================================================================== *) 170 171val show_rewrites : bool ref 172 173 174(* ================================================================== *) 175(* *) 176(* The tactics including ONCE in their name attempt to use each *) 177(* theorem in the list, only once, in order, left to right. *) 178(* The hypotheses added in the process of dependent rewriting are *) 179(* not rewritten by the ONCE tactics. This gives the most fine-grain *) 180(* control of dependent rewriting. *) 181(* *) 182(* ================================================================== *) 183 184val DEP_ONCE_FIND_THEN : thm_tactic -> thm list -> tactic 185 186val DEP_PURE_ONCE_REWRITE_TAC : thm list -> tactic 187val DEP_ONCE_REWRITE_TAC : thm list -> tactic 188val DEP_PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic 189val DEP_ONCE_ASM_REWRITE_TAC : thm list -> tactic 190 191val DEP_PURE_ONCE_SUBST_TAC : thm list -> tactic 192val DEP_ONCE_SUBST_TAC : thm list -> tactic 193val DEP_PURE_ONCE_ASM_SUBST_TAC : thm list -> tactic 194val DEP_ONCE_ASM_SUBST_TAC : thm list -> tactic 195 196 197(* ================================================================== *) 198(* *) 199(* The tactics including LIST in their name take a list of lists of *) 200(* implication theorems, and attempt to use each list of theorems *) 201(* once, in order, left to right. Each list of theorems is applied *) 202(* by rewriting with each theorem in it as many times as they apply. *) 203(* The hypotheses added in the process of dependent rewriting are *) 204(* collected from all rewritings, but they are not rewritten by the *) 205(* LIST tactics. This gives a moderate and more controlled degree *) 206(* of dependent rewriting than provided by DEP_REWRITE_TAC. *) 207(* *) 208(* ================================================================== *) 209 210val DEP_LIST_FIND_THEN : thm_tactic -> thm list list -> tactic 211 212val DEP_PURE_LIST_REWRITE_TAC : thm list list -> tactic 213val DEP_LIST_REWRITE_TAC : thm list list -> tactic 214val DEP_PURE_LIST_ASM_REWRITE_TAC : thm list list -> tactic 215val DEP_LIST_ASM_REWRITE_TAC : thm list list -> tactic 216 217 218(* ================================================================== *) 219(* *) 220(* The tactics without ONCE attept to reuse all theorems until no *) 221(* changes can be achieved in the goal. Hypotheses are rewritten *) 222(* and new ones generated from them, continuing until no further *) 223(* progress is possible. *) 224(* *) 225(* ================================================================== *) 226 227val DEP_FIND_THEN : thm_tactic -> thm list -> tactic 228 229val DEP_PURE_REWRITE_TAC : thm list -> tactic 230val DEP_REWRITE_TAC : thm list -> tactic 231val DEP_PURE_ASM_REWRITE_TAC : thm list -> tactic 232val DEP_ASM_REWRITE_TAC : thm list -> tactic 233 234 235end 236 237(* ================================================================== *) 238(* ================================================================== *) 239(* END OF DEPENDENT REWRITING TACTICS *) 240(* ================================================================== *) 241(* ================================================================== *) 242