Vincent, how does this tactic compare to the dependent rewriting package in
src/1/dep_rewrite.{sig,sml}? It appears at first glance to address the same
problem you are working on. Here is part of the .sig header comment:
(* ================================================================== *)
(* ================================================================== *)
(* 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. *)
(* *)
(* ================================================================== *)
(* ================================================================== *)
The dependent rewriting package has been part of HOL for many years.
Perhaps if you desire some additional functionality, it could be folded
into this package?
Cheers,
Peter
On Thu, Jul 11, 2013 at 6:08 AM, Vincent Aravantinos <
[email protected]> wrote:
> Hi list,
>
> I developed a new tactic that takes a theorem of the form P ==> l = r and
> replaces l by r in a goal adding whatever it needs to make it work properly
> (typically conjunction with P; but can also be an implication or even
> existentials).
>
> This is a follow-up of the discussion I started a few months ago (
> http://sourceforge.net/mailarchive/message.php?msg_id=30133516), the
> major difference being that it solves the problem raised by Michael Norrish
> (i.e., it could not work under the scope of a quantifier) in a systematic
> and (in my opinion) elegant way.
>
> This change entails that the tactic is much more modular and thus can be
> chained very smoothly. Many preprocessing options also allows it to be a
> (sometimes more powerful) replacement for REWRITE_TAC, SIMP_TAC and even
> MATCH_MP_TAC. Please look at the (draft) manual for more info.
>
> The code is available at: https://github.com/aravantv/impconv (HOL Light
> only for now)
> To install, type:
> # needs "target_rewrite.ml";;
> The pdf manual is available in the directory "manual".
>
> The development of this tactic required quite some work that might be
> useful in other context. This is undocumented for now but is described in a
> paper which is currently under review.
>
> Regards,
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Group
> http://users.encs.concordia.ca/~vincent/
>
>
> ------------------------------------------------------------------------------
> See everything from the browser to the database with AppDynamics
> Get end-to-end visibility with application monitoring from AppDynamics
> Isolate bottlenecks and diagnose root cause in seconds.
> Start your free trial of AppDynamics Pro today!
> http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
