Structure dep_rewrite


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
type term = Term.term
type fixity = Parse.fixity
type thm = Thm.thm
type tactic  = Abbrev.tactic
type conv = Abbrev.conv
type thm_tactic = Abbrev.thm_tactic


(* ================================================================== *)
(*                                                                    *)
(* 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

HOL 4, Kananaskis-10