xref: /seL4-l4v-master/HOL4/src/1/dep_rewrite.sml

(* ===================================================================== *)
(* FILE          : dep_rewrite.sml                                       *)
(* 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 layer of         *)
(* universal quantifications, under which 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.                               *)
(*                                                                    *)
(* 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.        *)
(*                                                                    *)
(* ================================================================== *)
(* ================================================================== *)


structure dep_rewrite :> dep_rewrite =
struct

open HolKernel Parse boolLib Abbrev;




local

val show_rewrites = ref false; (* normally false, set true for tracing   *)

val debug         = false;  (* normally false, set to true for debugging *)
val debug_fail    = false;  (* normally false, set to true for debugging *)
val debug_match   = false;  (* normally false, set to true for debugging *)
val debug_matches = false;  (* normally false, set to true for debugging *)

(* Printing functions: (only needed for debugging) *)
val print_string = TextIO.print;
fun print_newline() = print_string "\n";
fun print_strings []        = ()
   | print_strings (t :: []) = print_string t
   | print_strings (t :: ts) = (print_string t; print_string ",";
                                print_strings ts);
fun print_theorem th = (print_string (thm_to_string th); print_newline());
fun print_terms []        = ()
   | print_terms (t :: []) = print_term t
   | print_terms (t :: ts) = (print_term t; print_string ","; print_terms ts);
fun print_all_thm th =
   let val (ant,conseq) = dest_thm th
   in (print_string "["; print_terms ant; print_string "] |- ";
       print_term conseq; print_newline() )
   end;
fun print_theorems []        = ()
   | print_theorems (t :: ts) = (print_theorem t; print_string "\n";
                                 print_theorems ts);
fun print_goal (asl,gl) = (print_term gl; print_newline());
fun pthm th = (print_all_thm th; th);
(**)

fun TACTIC_ERR{function,message} =
    Feedback.HOL_ERR{origin_structure = "Tactic",
                      origin_function = function,
                      message = message};

fun failwith function =
   ( (**) if debug_fail then
         print_string ("Failure in dep_rewrite: "^function^"\n")
     else (); (**)
    raise TACTIC_ERR{function = function,message = "Failure in dep_rewrite"});



fun UNDER_FORALL_CONV conv tm =
    if is_forall tm then
       RAND_CONV (ABS_CONV (UNDER_FORALL_CONV conv)) tm
    else
       conv tm ;

(* Does multiple conversions of ==> to /\:
val assemble_ants =
      CONV_RULE (REPEATC (UNDER_FORALL_CONV RIGHT_IMP_FORALL_CONV)
                 THENC UNDER_FORALL_CONV (REPEATC (REWR_CONV AND_IMP_INTRO)));
*)

val assemble_ants =
      CONV_RULE (REPEATC (UNDER_FORALL_CONV RIGHT_IMP_FORALL_CONV)
                 THENC UNDER_FORALL_CONV (TRY_CONV (REWR_CONV AND_IMP_INTRO)));

(*
assemble_ants EQ_LIST;
*)

(*
val DEP_PENETRATE_CONV =
    TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV
    THENC PURE_REWRITE_CONV[AND_IMP_INTRO];

val DEP_PENETRATE_RULE = CONV_RULE DEP_PENETRATE_CONV;

val DEP_PENETRATE_ASSUM_TAC =
    RULE_ASSUM_TAC DEP_PENETRATE_RULE;

val DEP_PENETRATE_TAC =
    CONV_TAC DEP_PENETRATE_CONV
    THEN DEP_PENETRATE_ASSUM_TAC;
*)


fun UNDISCH_NOT_NEG th =
  MP th (ASSUME(fst(dest_imp_only(concl th))))
  handle HOL_ERR  _ => failwith "UNDISCH_NOT_NEG";

fun UNDISCH_ALL_NOT_NEG th =
    if is_imp_only(concl th)
       then UNDISCH_ALL_NOT_NEG (UNDISCH_NOT_NEG th)
       else th;


fun DEP_FIND_matches th =
   let
       val tha = (* CONV_RULE (REPEATC
                     (UNDER_FORALL_CONV RIGHT_IMP_FORALL_CONV)) *) th;
       val tm = concl tha
       val (avs,bod) = strip_forall tm
       val (ants,conseq) = strip_imp_only bod
       val th1 = SPECL avs (ASSUME tm)
       val th2 = UNDISCH_ALL_NOT_NEG th1
       val evs = filter(fn v => all (free_in v) ants
                        andalso not(free_in v conseq)) avs
       val th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2)
       val hs = hyp th3
       fun DISCH_ALL hyps th = itlist DISCH hyps th
       val sth = MP (DISCH tm (GEN_ALL (DISCH_ALL hs (UNDISCH th3)))) tha
       val term_to_match =
              (lhs conseq
               handle _ =>
               dest_neg conseq
               handle _ =>
               conseq)
  (*   val _ = (if !show_rewrites then
                  (print_string "Searching for ";
                   print_term term_to_match;
                   print_string "\n")
                  else ())   *)
       val match_fn =
           (HO_PART_MATCH (lhs o snd o strip_imp_only) sth
            handle _ =>
            HO_PART_MATCH (dest_neg o snd o strip_imp_only) sth
            handle _ =>
            HO_PART_MATCH (snd o strip_imp_only) sth)
   in
      match_fn
   end
   handle _ => failwith "DEP_FIND_matches: bad theorem";

fun SUB_matches (f:term->'a) tm =
   ( (* if debug_matches then (print_string "SUB_matches: ";
                    print_term tm; print_newline()) else (); *)
    if is_comb tm then
       (let val {Rator,Rand} = Rsyntax.dest_comb tm in
        (f Rator handle _ => f Rand)
        end)
    else
    if is_abs tm then
       let val {Bvar,Body} = Rsyntax.dest_abs tm in
           f Body
       end
    else failwith "SUB_matches");

fun ONCE_DEPTH_matches (f:term->'a) tm =
     ( (* if debug_matches then
        (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline())
      else (); *)
       (f tm handle _ => (SUB_matches (ONCE_DEPTH_matches f) tm)));




(* ================================================================== *)
(* APPLY_IMP_THEN ttac th is a dependent rewriting function,          *)
(* which takes a goal and produce a 5-tuple containing:               *)
(*                                                                    *)
(*     assumption list,                                               *)
(*     list of hypotheses,                                            *)
(*     list of justification functions for those hypotheses,          *)
(*     list of goals,                                                 *)
(*     and list of justification functions for those goals.           *)
(* ================================================================== *)

local

fun UNDISCH_ALL_NON_NEG th =
   if (is_imp (concl th) andalso not(is_neg(concl th)))
   then UNDISCH_ALL_NON_NEG (UNDISCH th)
   else th;

fun print_goals gl =
   if null gl then print_string "proved\n"
   else (map print_goal gl; ());

fun repeat_apply (f:'a->'b) step stop x =
      f x
    handle (e as HOL_ERR _) =>
      let val x' = step x in
        if stop x x' then raise e
        else repeat_apply f step stop x'
      end;

in

fun APPLY_IMP_THEN ttac th (asl,gl) =
    let val _ = if !show_rewrites then
                   (print_string "Trying ";
                    print_theorem th)
                   else (); (**)
        val matched =
               repeat_apply
                  (fn th => ONCE_DEPTH_matches (DEP_FIND_matches th) gl)
                  assemble_ants
                  (fn th1 => fn th2 => concl th1 ~~ concl th2)
                  th;
(*
ONCE_DEPTH_matches (DEP_FIND_matches th) gl
              handle e =>
               let val th' = assemble_ants th in
                if concl th' = concl th then raise e
                else
                  let val mtchd = ONCE_DEPTH_matches (DEP_FIND_matches th') gl
                  in (if !show_rewrites then
                        print_string "Found deeper match\n"
                      else ();
                      mtchd)
                  end
               end;
*)
(*      val _ = if !show_rewrites then
                      (print_string "match found:\n";
                       print_theorem matched)
                   else (); *)
        val base = UNDISCH_ALL_NON_NEG matched;
        val subgoal = concl base;
(**)    val _ = if !show_rewrites then
                       (print_string "Rewriting ";
                        print_term subgoal;
                        print_string "\n")
                   else (); (**)
        val (gl1,p1) = ( (*REPEAT GEN_TAC THEN*)
                          MATCH_MP_TAC matched) (asl,subgoal)
        val (gl2,p2) = ttac (Thm.ASSUME subgoal) (asl,gl);
    in
     case gl1
       of [(asl1,g1)] =>
       ( if !show_rewrites then
           (print_string "New burden: ";
            print_goals gl1;
            print_string "Revised goal: ";
            print_goals gl2;
            print_newline())
          else ();
         (asl1,[g1],[p1],gl2,p2) )
        | _ => failwith "APPLY_IMP_THEN"
    end

end;

(* ================================================================== *)
(* We now introduce a series of tacticals for dependent rewriting     *)
(* functions, which will be easily understood by relation to the      *)
(* corresponding tacticals for tactics and conversions.               *)
(* ================================================================== *)

(* TAC_DEP turns a tactic into a dependent rewriting function. *)

fun TAC_DEP tac = fn (asl,gl) =>
    let val (gl0,p0) = tac (asl,gl)
    in (asl,[],[],gl0,p0)
    end
    handle _ => failwith "TAC_DEP";



(* DEP_TAC turns a dependent rewriting function into a tactic. *)

fun DEP_TAC dep :tactic = fn g0 =>
    let val (asl1,gls,(pls:validation list),(gl2:goal list),(p2:validation))
            = dep g0 in
    ( (* if debug then
        (print_string "DEP_TAC:\nburdens = [";
         map (fn tm => (print_newline(); print_term tm; print_string ",")) gls;
         print_string "]\ncurrent goals = [";
         map (fn g2 => (print_newline(); print_goal g2; print_string ",")) gl2;
         print_string "]\n")
    else (); *)
    if null gls then (gl2,p2)
    else
    let
        val rgls = op_mk_set aconv (flatten (map strip_conj gls));
        val gl1 = [(asl1,list_mk_conj rgls)];
        val p1 = (fn [th] =>
                  map2 (fn gl => fn p =>
                        p [( (* if debug then
                               (print_string "Prove: ";
                                print_term gl;
                                print_newline();
                                print_string "From: ";
                                print_theorem th;
                                print_newline())
                            else (); *)
                            TAC_PROOF
                              (([], gl),
                                  REPEAT CONJ_TAC
                                  THEN FIRST(map ACCEPT_TAC (CONJUNCTS th)))
                            handle _ => failwith "Burden proof failed"
                                                     )]) gls pls
                   | _ => failwith "DEP_TAC");
    in
      ( (* if debug then
          (print_string "gl1 = \n"; print_goal (hd gl1))
       else (); *)
       case gl2
         of [] =>
           (gl1,(fn thl => itlist Drule.PROVE_HYP (p1 thl) (p2 [])))
          | ((asl2,g2)::gl3) =>
              case gl1 of
                  [(asl1,g1)] =>
                  ((op_intersect aconv asl1 asl2,
                    Rsyntax.mk_conj{conj1=g1,conj2=g2})::gl3,
                   (fn (tha::thl) =>
                          itlist Drule.PROVE_HYP (p1 [CONJUNCT1 tha])
                                                 (p2 ((CONJUNCT2 tha)::thl))
                     | [] => failwith "DEP_TAC"))
                 | _ => failwith "DEP_TAC"
      )
    end)
    end
    handle _ => failwith "DEP_TAC";



fun choplist a b =
   case a
   of [] =>
        ([],b)
    | (h::t) =>
        let val (c,d) = choplist t (tl b) in
            ((hd b)::c, d)
        end;

infix THEN1_DEP;

fun ctac1 THEN1_DEP ctac2 = fn g =>
    let val (asl1,gs1,ps1,gl1,p1) = ctac1 g
    in
    case gl1
    of [] =>
         (asl1,gs1,ps1,gl1,p1)
     | (g1::gl1') =>
         let val (asl2,gs2,ps2,gl2,p2) = ctac2 g1
         in
         (op_intersect aconv asl1 asl2, gs1@gs2, ps1@ps2, gl2@gl1',
          (fn ths => let val (ths1,ths2) = choplist gl2 ths in
                          p1 ((p2 ths1) :: ths2)
                     end))
         end
    end
    handle HOL_ERR _ => failwith "THEN1_DEP";


val ALL_DEP = fn (asl,gl) =>
    (asl,[],[],[(asl,gl)],hd);


infix ORELSE_DEP;

fun ctac1 ORELSE_DEP ctac2 = fn g =>
    ctac1 g handle HOL_ERR _ => ctac2 g;


fun FIRST_DEP cl =
    case cl
    of [] =>
         ALL_DEP
     | (c::cl') =>
         c ORELSE_DEP FIRST_DEP cl';


fun EVERY_DEP cl =
    case cl of
        [] => ALL_DEP
      | (c::cl') => c THEN1_DEP EVERY_DEP cl'
    handle _ => failwith "EVERY_DEP";


fun REPEAT_DEP ctac g =
    ((ctac THEN1_DEP REPEAT_DEP ctac) ORELSE_DEP ALL_DEP) g;


fun CHANGED_DEP ctac g =
    let val (asl,gls,pls,gl,p) = ctac g in
    if goals_eq gl [g] then failwith "CHANGED_DEP"
    else (asl,gls,pls,gl,p)
    end;



(* We define theorem-tactics that take one theorem and rewrite with it. *)

fun REWRITE_THM th = REWRITE_TAC[th];
fun PURE_REWRITE_THM th = PURE_REWRITE_TAC[th];
fun ONCE_REWRITE_THM th = ONCE_REWRITE_TAC[th];
fun PURE_ONCE_REWRITE_THM th = PURE_ONCE_REWRITE_TAC[th];


(* ================================================================== *)
(* End of local declarations.                                         *)
(* Beginning of exported declarations.                                *)
(* ================================================================== *)

in


val show_rewrites = show_rewrites;


(* ================================================================== *)
(* ================================================================== *)
(*                     DEPENDENT REWRITING TACTICS                    *)
(* ================================================================== *)
(* ================================================================== *)

(* ================================================================== *)
(*                                                                    *)
(* 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 fine-grain   *)
(* control of dependent rewriting.                                    *)
(*                                                                    *)
(* ================================================================== *)



fun DEP_ONCE_FIND_THEN (ttac:thm->tactic) ths :tactic =
    DEP_TAC
         (EVERY_DEP (map (fn th => APPLY_IMP_THEN ttac th
                                    ORELSE_DEP TAC_DEP (ttac th))
                          (flatten (map CONJUNCTS ths))))
    handle _ => failwith "DEP_ONCE_FIND_THEN";



val DEP_PURE_ONCE_REWRITE_TAC :(thm list)->tactic =
    DEP_ONCE_FIND_THEN (fn th => Ho_Rewrite.PURE_ONCE_REWRITE_TAC[th]);

fun DEP_ONCE_REWRITE_TAC thl :tactic =
    DEP_PURE_ONCE_REWRITE_TAC thl
    THEN Ho_Rewrite.REWRITE_TAC[];

fun DEP_PURE_ONCE_ASM_REWRITE_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_PURE_ONCE_REWRITE_TAC (asl @ thl));

fun DEP_ONCE_ASM_REWRITE_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_ONCE_REWRITE_TAC (asl @ thl));


val DEP_PURE_ONCE_SUBST_TAC :(thm list)->tactic =
    DEP_ONCE_FIND_THEN (fn th => SUBST1_TAC th ORELSE ALL_TAC);

fun DEP_ONCE_SUBST_TAC thl :tactic =
    DEP_PURE_ONCE_SUBST_TAC thl
    THEN Ho_Rewrite.REWRITE_TAC[];

fun DEP_PURE_ONCE_ASM_SUBST_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_PURE_ONCE_SUBST_TAC (asl @ thl));

fun DEP_ONCE_ASM_SUBST_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_ONCE_SUBST_TAC (asl @ thl));




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



fun DEP_LIST_FIND_THEN (ttac:thm->tactic) thss :tactic =
    DEP_TAC
         (EVERY_DEP (map (fn ths =>
             REPEAT_DEP (CHANGED_DEP
                (EVERY_DEP (map (fn th =>
                                    APPLY_IMP_THEN ttac th
                                    ORELSE_DEP TAC_DEP (ttac th))
                                 (flatten (map CONJUNCTS ths))))))
                          thss))
    handle _ => failwith "DEP_LIST_FIND_THEN";



val DEP_PURE_LIST_REWRITE_TAC :(thm list list)->tactic =
    DEP_LIST_FIND_THEN (fn th => Ho_Rewrite.PURE_REWRITE_TAC[th]);

val DEP_LIST_REWRITE_TAC :(thm list list)->tactic =
    DEP_LIST_FIND_THEN (fn th => Ho_Rewrite.REWRITE_TAC[th]);

fun DEP_PURE_LIST_ASM_REWRITE_TAC thss :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_PURE_LIST_REWRITE_TAC
                                   (map (fn ths => asl @ ths) thss));

fun DEP_LIST_ASM_REWRITE_TAC thss :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_LIST_REWRITE_TAC
                                   (map (fn ths => asl @ ths) thss));




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


fun DEP_FIND_THEN (ttac:thm->tactic) ths :tactic =
    DEP_TAC (REPEAT_DEP (CHANGED_DEP
         (EVERY_DEP (map (fn th => APPLY_IMP_THEN ttac th
                                    ORELSE_DEP TAC_DEP (ttac th))
                          (flatten (map CONJUNCTS ths))))))
    handle _ => failwith "DEP_FIND_THEN";




fun DEP_PURE_REWRITE_TAC thl :tactic =
    REPEAT (CHANGED_TAC (DEP_FIND_THEN
                           (fn th => Ho_Rewrite.PURE_REWRITE_TAC[th]) thl));

fun DEP_REWRITE_TAC thl :tactic =
    REPEAT (CHANGED_TAC (DEP_FIND_THEN
                           (fn th => Ho_Rewrite.REWRITE_TAC[th]) thl));

fun DEP_PURE_ASM_REWRITE_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_PURE_REWRITE_TAC (asl @ thl));

fun DEP_ASM_REWRITE_TAC thl :tactic =
    Tactical.ASSUM_LIST (fn asl => DEP_REWRITE_TAC (asl @ thl));


end

(* ================================================================== *)
(* ================================================================== *)
(*                 END OF DEPENDENT REWRITING TACTICS                 *)
(* ================================================================== *)
(* ================================================================== *)


end;



(* TEST EXAMPLES:

load "dep_rewrite";
open dep_rewrite;
show_rewrites := true;

(* Example theorems to play with: *)

open arithmeticTheory;

(* Implication arithmetic theorems:

val LESS_LESS_EQ_TRANS = |- !m n p. m < n /\ n <= p ==> m < p : thm
val LESS_EQ_LESS_TRANS = |- !m n p. m <= n /\ n < p ==> m < p : thm
val LESS_MULT2 = |- !m n. 0 < m /\ 0 < n ==> 0 < m * n : thm
val CANCEL_SUB = |- !p n m. p <= n /\ p <= m ==> ((n - p = m - p) = n = m)
  : thm
val SUB_CANCEL = |- !p n m. n <= p /\ m <= p ==> ((p - n = p - m) = n = m)
  : thm
val SUB_LESS_EQ_ADD = |- !m p. m <= p ==> (!n. p - m <= n = p <= m + n) : thm
val LESS_EQ_IMP_LESS_SUC = |- !n m. n <= m ==> n < SUC m : thm
val LESS_IMP_LESS_ADD = |- !n m. n < m ==> (!p. n < m + p) : thm
val SUB_SUB = |- !b c. c <= b ==> (!a. a - b - c = (a + c) - b) : thm
val LESS_EQ_SUB_LESS = |- !a b. b <= a ==> (!c. a - b < c = a < b + c) : thm
val LESS_EQ_ADD_SUB = |- !c b. c <= b ==> (!a. (a + b) - c = a + (b - c)) : thm
val LESS_SUB_ADD_LESS = |- !n m i. i < n - m ==> i + m < n : thm
val SUB_LESS_OR = |- !m n. n < m ==> n <= m - 1 : thm
val INV_PRE_LESS_EQ = |- !n. 0 < n ==> (!m. PRE m <= PRE n = m <= n) : thm
val INV_PRE_LESS = |- !m. 0 < m ==> (!n. PRE m < PRE n = m < n) : thm
val MOD_MOD = |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) : thm
val MOD_PLUS =
  |- !n. 0 < n ==> (!j k. (j MOD n + k MOD n) MOD n = (j + k) MOD n) : thm
val MOD_TIMES = |- !n. 0 < n ==> (!q r. (q * n + r) MOD n = r MOD n) : thm
val MOD_MULT = |- !n r. r < n ==> (!q. (q * n + r) MOD n = r) : thm
val ZERO_DIV = |- !n. 0 < n ==> (0 DIV n = 0) : thm
val ZERO_MOD = |- !n. 0 < n ==> (0 MOD n = 0) : thm
val MOD_EQ_0 = |- !n. 0 < n ==> (!k. (k * n) MOD n = 0) : thm
val LESS_MOD = |- !n k. k < n ==> (k MOD n = k) : thm
val DIV_MULT = |- !n r. r < n ==> (!q. (q * n + r) DIV n = q) : thm
val MOD_UNIQUE = |- !n k r. (?q. (k = q * n + r) /\ r < n) ==> (k MOD n = r)
  : thm
val DIV_UNIQUE = |- !n k q. (?r. (k = q * n + r) /\ r < n) ==> (k DIV n = q)
  : thm
val DIV_LESS_EQ = |- !n. 0 < n ==> (!k. k DIV n <= k) : thm
val LESS_EQUAL_ANTISYM = |- !n m. n <= m /\ m <= n ==> (n = m) : thm
val LESS_MONO_MULT = |- !m n p. m <= n ==> m * p <= n * p : thm
val LESS_IMP_LESS_OR_EQ = |- !m n. m < n ==> m <= n : thm
val LESS_EQ_LESS_EQ_MONO = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q
  : thm
val LESS_EQ_TRANS = |- !m n p. m <= n /\ n <= p ==> m <= p : thm
val LESS_MONO_ADD = |- !m n p. m < n ==> m + p < n + p : thm
val ADD_EQ_SUB = |- !m n p. n <= p ==> ((m + n = p) = m = p - n) : thm
val LESS_SUC_NOT = |- !m n. m < n ==> ~(n < SUC m) : thm
val INV_PRE_EQ = |- !m n. 0 < m /\ 0 < n ==> ((PRE m = PRE n) = m = n) : thm
val PRE_SUC_EQ = |- !m n. 0 < n ==> ((m = PRE n) = SUC m = n) : thm
val SUB_ADD = |- !m n. n <= m ==> ((m - n) + n = m) : thm
val LESS_ADD_NONZERO = |- !m n. ~(n = 0) ==> m < m + n : thm
val ADD_INV_0 = |- !m n. (m + n = m) ==> (n = 0) : thm
val LESS_CASES_IMP = |- !m n. ~(m < n) /\ ~(m = n) ==> n < m : thm
val LESS_NOT_SUC = |- !m n. m < n /\ ~(n = SUC m) ==> SUC m < n : thm
val LESS_SUC_EQ_COR = |- !m n. m < n /\ ~(SUC m = n) ==> SUC m < n : thm
val OR_LESS = |- !m n. SUC m <= n ==> m < n : thm
val LESS_OR = |- !m n. m < n ==> SUC m <= n : thm
val FUN_EQ_LEMMA = |- !f x1 x2. f x1 /\ ~(f x2) ==> ~(x1 = x2) : thm
val LESS_TRANS = |- !m n p. m < n /\ n < p ==> m < p : thm
val LESS_MONO_REV = |- !m n. SUC m < SUC n ==> m < n : thm

*)

(*
[LESS_EQ_ADD_SUB,SUB_ADD,SUB_SUB,ADD_EQ_SUB,LESS_TRANS,SUB_LESS_EQ_ADD,
 CANCEL_SUB,LESS_EQ_SUB_LESS,LESS_EQ_LESS_EQ_MONO];
*)


g `(10 + y) - y < 12`;
e(DEP_ONCE_REWRITE_TAC[LESS_EQ_ADD_SUB]);
e(RW_TAC arith_ss []);
drop();

g `(x + y) - (x + 2) <= 2 * y`;
e(ASM_CASES_TAC (--`2 <= y`--));

 e(DEP_REWRITE_TAC[SUB_LESS_EQ_ADD,LESS_EQ_LESS_EQ_MONO]);
 e(RW_TAC arith_ss []);

 val SUB_EQ_0_IMP = GEN_ALL(snd(EQ_IMP_RULE (SPEC_ALL SUB_EQ_0)));
 e(DEP_REWRITE_TAC[SUB_EQ_0_IMP]);
 e(RW_TAC arith_ss []);

drop();

g `(1 + (2 + (3 + (4 + (5 + 6))))) - 5 = 16`;
e(DEP_REWRITE_TAC[LESS_EQ_ADD_SUB]);
e(RW_TAC arith_ss []);
drop();

g `EL (SUC(SUC 0)) (ZIP([1;2;3],ZIP([4;5;6],[7;8;9]))) = (3,6,9)`;
val EL_ZIP = listTheory.EL_ZIP;
e(DEP_REWRITE_TAC[EL_ZIP]);
e(RW_TAC list_ss []);
drop();

g `0 < (@n. 0 < n)`;
e(DEP_ONCE_REWRITE_TAC[SELECT_AX]);
drop();

g `!P f x. P f ==> (x = f x)`;
e(DEP_ONCE_REWRITE_TAC[RIGHT_FORALL_IMP_THM]);
drop();

*)