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