hol88-contrib-source 2.02.19940316-35 / usr / share / hol88-2.02.19940316 / contrib / rewriting / imp.ml

%


Author:          R. A. Fleming

Affiliation:     Hewlett Packard Laboratories, Bristol

Address:         Hewlett Packard Laboratories,
                 Filton Road,
                 Stoke Gifford
                 Bristol BS12 6QZ
                 U.K.

Tel:             +44 272 799910

Fax:             +44 272 890554

Email:           ..!mcvax!ukc!hplb!raf
                 raf@hplb.hpl.hp.com

File:            "Implicational (= conditional) rewriting" tactics for HOL

Date:            16/11/90
                 25/2/91      bug on FIRST_ICONV, SEL_REWRITE_ICONV fixed
                              <=> deleted for Hol version 12


The following file does implicational rewriting.  This is rewriting using laws
of the form
                    !x0...xn. a ==> (b = c)

IMP_REWRITE_RULE tac thml (ASSUMPTIONS |- t) yields the theorem
NEW_ASSUMPTIONS, ASSUMPTIONS |- t' where t' is a rewrite of t, where the
NEW_ASSUMPTIONS are generated by the side-conditions on the implicational
rewrite laws.  An attempt is made to discharge these assumptions using the
user-supplied tactic tac, in which case they do not appear in
NEW_ASSUMPTIONS.

IMP_REWRITE_TAC tac thml (gl, g) is similar, yielding a new goal (newgl,
gl, g') where g' is a rewrite of g, and the new subgoals are generated by
the side-conditions on the implicational rewrite laws.

IMP_SEL_REWRITE_RULE tac thml (ASSUMPTIONS |-t) yields the theorem
ASSUMPTIONS |- t' with no new assumptions.  Rewriting wrt implication
rewrite laws is only done at those places at which the side conditions can
be discharged using the tactic tac.  (It means "selective rewrite".  Anyone
with better names?)

IMP_SEL_REWRITE_TAC tac thml (gl, g) is similar, yielding a new goal (gl,
g') where g' is a rewrite of g, and no new subgoals are generated.
Rewriting wrt implication rewrite laws is only done at those places at
which the side conditions can be discharged using the tactic tac.

Attempts to prove side-conditions can effectively be turned off by using
NO_TAC as the tactic parameter.

A default tactic (called SIDECOND_TAC below) deals with many of the simpler
cases.  (This is just REPEAT GEN_TAC THEN STRIP_TAC THEN
ASM_REWRITE_TAC[].)

The side-condition prover is aware of the context in which it sits.
E.g. in the term a==>b, when rewriting b using the implicational rewrite
law a==>(x=y), it is assumed that a is true, so the side condition is
discharged.  The following table indicates what extra assumptions are made
in proving side-conditions when rewriting the term b:

             a ==> b       assumes         a
             b ==> a                       ~a
             a/\b                          a
             b/\a                          a
             a\/b                          ~a
             b\/a                          ~a
             a=>b|c                        a
             a=>c|b                        ~a

There is a slight difference between this rewriting and ordinary rewriting
in the choice of what variables to instantiate.  Given a theorem
                              !x. A[x,y]
only the parameters x are ever instantiated.  (This is unlike the
conventional rewrite rules which always do an automatic generalisation
first.)  The reason for this is that implicational rewrites, more so that
ordinary ones, are liable to introduce new variables.  E.g.  
                  cond(x,y) ==> (e(x) = f(y))
are to be expected.  The user can choose the particular values of the new
variables y by SPEC-ing the laws prior to use.  (This can also be used just
to control the points at which rewriting occurs.)  (There is nothing
special about the logic of implicational rewriting here.  The same strategy
could have been used for conventional rewriting, but the choice was made to
allow users to provide ungeneralised laws instead.)

%

% is_imp is rather too general on my current system: %

let is_implies tm =  (rator (rator tm) = "==>")?false;;

ml_curried_infix `THENTRYIC`;;

let c_cnv1 THENTRYIC c_cnv2 = \l t.
  let thm = c_cnv1 l t in
  (TRANS thm (c_cnv2 l (rand (concl thm))) ? thm);;

letrec REPEATIC c_cnv l t = (c_cnv THENTRYIC (REPEATIC c_cnv)) l t;;

let ONCE_OR_MOREIC c_cnv = c_cnv THENTRYIC (REPEATIC c_cnv);;

ml_curried_infix `ORELSEIC`;;

let c_cnv1 ORELSEIC c_cnv2 = \l t. ((c_cnv1 l t) ? (c_cnv2 l t));;

let TRYBOTHIC c_cnv1 c_cnv2 = (c_cnv1 THENTRYIC c_cnv2) ORELSEIC c_cnv2;;

%

The following laws are used to construct subterm conversions.  They take an
age to load.  (I couldn't be bothered to find more efficient ways of
proving these.)

%

let PROVE_ICONV_THM (tm, gl) = PROVE(gl,
REPEAT GEN_TAC THEN
DISJ_CASES_TAC (SPEC tm BOOL_CASES_AX) THEN
ASM_REWRITE_TAC [] THEN
STRIP_TAC THEN
ASM_REWRITE_TAC []);;

let [CONJ1_ICONV_THM;CONJ2_ICONV_THM;IMP1_ICONV_THM;IMP2_ICONV_THM;
     DISJ1_ICONV_THM;DISJ2_ICONV_THM;COND2_ICONV_THM;COND3_ICONV_THM] =
    map PROVE_ICONV_THM
    ["b:bool","!a a' b. (b ==> (a = a')) ==> (a /\ b = a' /\ b)";
     "a:bool","!a b b'. (a ==> (b = b')) ==> (a /\ b = a /\ b')";
     "b:bool","!a a' b. (~b ==> (a = a')) ==> (a ==> b = a' ==> b)";
     "a:bool","!a b b'. (a ==> (b = b')) ==> (a ==> b = a ==> b')";
     "b:bool","!a a' b. (~b ==> (a = a')) ==> (a \/ b = a' \/ b)";
     "a:bool","!a b b'. (~a ==> (b = b')) ==> (a \/ b = a \/ b')";
     "a:bool","!a b b' (c:*). (a ==> (b = b')) ==> (a => b | c = a => b' | c)";
     "a:bool","!a b c (c':*). (~a ==> (c = c')) ==> (a => b | c = a => b | c')"];;

let COND1_ICONV_THM = PROVE ("!a a' b (c:*). (a = a') ==> (a => b | c = a' => b | c)",
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;

let ICONV_addterm x (u,v) = (x.u,v);;

let CONJ1_ICONV iconv l tm =
let a,b = dest_conj tm in
let thm = iconv (ICONV_addterm b l) a in
MATCH_MP CONJ1_ICONV_THM (DISCH b thm);;

let CONJ2_ICONV iconv l tm =
let a,b = dest_conj tm in
let thm = iconv (ICONV_addterm a l) b in
MATCH_MP CONJ2_ICONV_THM (DISCH a thm);;

let DISJ1_ICONV iconv l tm =
let a,b = dest_disj tm in
let thm = iconv (ICONV_addterm (mk_neg b) l) a in
MATCH_MP DISJ1_ICONV_THM (DISCH (mk_neg b) thm);;

let DISJ2_ICONV iconv l tm =
let a,b = dest_disj tm in
let thm = iconv (ICONV_addterm (mk_neg a) l) b in
MATCH_MP DISJ2_ICONV_THM (DISCH (mk_neg a) thm);;

let IMP1_ICONV iconv l tm =
let a,b = dest_imp tm in
let thm = iconv (ICONV_addterm (mk_neg b) l) a in
MATCH_MP IMP1_ICONV_THM (DISCH (mk_neg b) thm);;

let IMP2_ICONV iconv l tm =
let a,b = dest_imp tm in
let thm = iconv (ICONV_addterm a l) b in
MATCH_MP IMP2_ICONV_THM (DISCH a thm);;

let COND1_ICONV iconv l tm =
let a,b,c = dest_cond tm in
let thm = iconv l a in
PART_MATCH lhs (MATCH_MP COND1_ICONV_THM thm) tm;;

let COND2_ICONV iconv l tm =
let a,b,c = dest_cond tm in
let thm = iconv (ICONV_addterm a l) b in
PART_MATCH lhs (MATCH_MP COND2_ICONV_THM (DISCH a thm)) tm;;

let COND3_ICONV iconv l tm =
let a,b,c = dest_cond tm in
let thm = iconv (ICONV_addterm (mk_neg a) l) c in
PART_MATCH lhs (MATCH_MP COND3_ICONV_THM (DISCH (mk_neg a) thm)) tm;;

let universify_hyp x ass thm =
if mem x (frees ass) then
PROVE_HYP (SPEC x (ASSUME (mk_forall(x,ass)))) thm
else thm;;

let ABS_ICONV iconv l tm =
let x,b = dest_abs tm in
let thm = iconv l b in
ABS x (itlist (universify_hyp x) (hyp thm) thm);;

%

Note that this conversion does not always yield rewrites when they are valid.
This is due to clashes of variables in hypotheses with bound variables in the
term being rewritten.  No attempt has been made to fix this, as this is in
line with the standard rewriting tactics.  (The alternative is also rather
inefficient.) 

%

let SUBTERM_ICONV icnv l t =
  if is_var t or is_const t then fail
  else if is_conj t then 
    (TRYBOTHIC (CONJ1_ICONV icnv) (CONJ2_ICONV icnv)) l t
  else if is_disj t then
    (TRYBOTHIC (DISJ1_ICONV icnv) (DISJ2_ICONV icnv)) l t
  else if is_implies t then
     (TRYBOTHIC (IMP1_ICONV icnv) (IMP2_ICONV icnv)) l t
  else if is_cond t then
     (TRYBOTHIC (COND1_ICONV icnv) (TRYBOTHIC (COND2_ICONV icnv) (COND3_ICONV icnv))) l t
  else if is_comb t then
    let a,b = dest_comb t in
      ((let a_thm = icnv l a in
         ((MK_COMB (a_thm, icnv l b))
            ? AP_THM a_thm b))
        ? AP_TERM a (icnv l b))
  else ABS_ICONV icnv l t;;

letrec TOP_DOWN_ICONV c_cnv l t =
  (TRYBOTHIC c_cnv (SUBTERM_ICONV (TOP_DOWN_ICONV c_cnv))) l t;;

letrec BOTTOM_UP_ICONV c_cnv l t =
  (TRYBOTHIC (SUBTERM_ICONV (BOTTOM_UP_ICONV c_cnv)) c_cnv) l t;;

letrec TRY_ONCE_DEPTH_ICONV c_cnv l t =
  (c_cnv ORELSEIC (SUBTERM_ICONV (TRY_ONCE_DEPTH_ICONV c_cnv))) l t;;

letrec TRY_TOP_DEPTH_ICONV c_cnv l t =
  letrec aux1 l t = (SUBTERM_ICONV (TRY_TOP_DEPTH_ICONV c_cnv) THENTRYIC aux2) l t
     and aux2 l t = ((ONCE_OR_MOREIC c_cnv) THENTRYIC aux1) l t
in ((TRYBOTHIC (ONCE_OR_MOREIC c_cnv) aux1) l t);;

%

In making implicational rewrite laws, laws not of the appropriate form are
made so, transforming A ==> B where B is not an equality into A ==> (B =
T), and laws B which are not implications into T ==> B.  Notable
transformations are

       A = (B = C)                     to        A ==> (B = C)
       A1 ==> ... ==> An ==> (B = C)   to        A1 /\ ... /\ An ==> (B = C)
%

letrec strip_implicands tm =
  (let a,b = dest_imp tm in
   let u,v = strip_implicands b in
   (a.u,v))?([],tm);;

letrec toplevel_CONJUNCTS thm =
  (let a,b = CONJ_PAIR thm in
   a.(toplevel_CONJUNCTS b))
  ?[thm];;

let IMPS_CONJS_IMP thm =
let u,v = strip_implicands (concl thm) in
let w = end_itlist (curry mk_conj) u in
DISCH w (LIST_MP (toplevel_CONJUNCTS (ASSUME w)) thm);;

let mk_imp_eq_rewrites th =
letrec split_thm th =
   let th = GSPEC th in
   let c = concl th in
   if is_conj c then (flat (map split_thm (CONJUNCTS th)))
   else if is_implies c then
   let a,b = dest_imp c in
    if is_eq b then [th] else
    let th' = MP th (ASSUME a) in
    if is_conj b 
    then flat (map (split_thm o (DISCH a)) 
                 (CONJUNCTS th')) else
    if is_neg b then [(DISCH a (MP (SPEC (dest_neg b) NOT_F) th'))] else
    if is_implies b then split_thm (IMPS_CONJS_IMP th) else
    [(DISCH a (EQT_INTRO th'))]
   else if is_eq c then
     if is_eq (rhs c) then split_thm (fst (EQ_IMP_RULE th))
     else split_thm (DISCH "T" th)
   else split_thm (DISCH "T" th) in
let f = frees (concl th) in
map (\x.f,x) (split_thm th);;

let mk_imp_eq_rewrites_list = flat o (map mk_imp_eq_rewrites);;

%

rewrite_ICONV f thm tac l tm does rewriting of term tm wrt rewrite rule
thm.  It is assumed that the term lies within the "scope" of a list of
implicans.  E.g. in the term a ==> (b /\ (c ==> d \/ e)), the term e lies
within the "scope" of a, b, c and ~d.  The side-conditions of the conditional
rewrite may be discharged by appeal to these.

Attempts to prove the side-conditions are wrt a user supplied tactic tac.
If this fails, they get put on the assumption list of the theorem generated
by the conversion.  In the case above, the side-condition generated by
rewriting the term e using the implicational rewrite x ==> (y = z) is ~d /\
c /\ b /\ a ==> x.

The parameter f contains the free terms of the theorem.  The point of this
extra parameter is to allow the user more control over how a theorem is
instantiated.  Given a theorem
                              !x. A[x,y]
only the parameter x are ever instantiated in doing a rewrite.  (This is
unlike the conventional rewrite rules which always do an automatic
generalisation first.)  The reason for the extra twiddle is that
implicational rewrites, more so that ordinary ones, are liable to introduce
new variables.  E.g. laws of the form
                  cond(x,y) ==> (e(x) = f(y))
are to be expected.  The user can choose the particular values of the new
variables y by SPEC-ing the laws prior to use.

%

let check_subst frees subs =
 not (exists (\f.exists (\x. snd x = f) subs) frees);;

let mk_conjs_imp u a =
  (mk_imp((end_itlist (\x y. mk_conj(x,y)) u),a))?a;;

let mk_imp_prf tac (u,ass) a =
if a = "T" then TRUTH
else if (mem a u) or (mem a ass) then ASSUME a
else if null u
then ((TAC_PROOF ((ass, a), tac))?ASSUME a)
else let us = LIST_CONJ (map ASSUME u) in
     ((MP (TAC_PROOF ((ass, mk_imp((end_itlist (\x y. mk_conj(x,y)) u),a)), tac))
          us)
     ? (MP (ASSUME (mk_imp (concl us, a))) us));;

% updated to keep in line with hol 12 rewriting :

let rewrite_ICONV f thm tac implicans =
    let pat = fst (dest_eq (snd (dest_imp (concl thm)))) in
    let matchfn = \t.
      let u = match pat t in
      if check_subst f (fst u) then u else fail in
    \tm. let thm' = INST_TY_TERM (matchfn tm) thm in
         let a,b = dest_imp (concl thm') in
         MP thm' (mk_imp_prf tac implicans a);;
%

let mk_imp_prf_sel tac (u,ass) a =
if a = "T" then TRUTH
else if (mem a u) or (mem a ass) % why was this ever here? or (null u) % then ASSUME a
else if null u
then TAC_PROOF ((ass, a), tac)
else MP (TAC_PROOF ((ass, mk_imp((end_itlist (\x y. mk_conj(x,y)) u),a)), tac))
        (LIST_CONJ (map ASSUME u));;

% updated to keep in line with hol 12 rewriting :

let SEL_REWRITE_ICONV f thm tac implicans =
    let pat = fst (dest_eq (snd (dest_imp (concl thm)))) in
    let matchfn = \t.
      let u = match pat t in
      if check_subst f (fst u) then u else fail in
    \tm. let thm' = INST_TY_TERM (matchfn tm) thm in
         let a,b = dest_imp (concl thm') in
          MP thm' (mk_imp_prf_sel tac implicans a);;

%

let GEN_rewrite_ICONV mk_imp_prf_fun f thm tac implicans =
  let mtch = match (fst (dest_eq (snd (dest_imp (concl thm))))) in
  ((\tm. let u = mtch tm in
         if check_subst f (fst u) 
         then let instth = INST_TY_TERM u thm in
         let a,(x,y) = (I # dest_eq) (dest_imp (concl instth)) in
         let instth' = if (x = tm) then instth
                                   else let B = genvar (type_of tm) in
                                        SUBST [ALPHA x tm, B] (mk_imp (a, mk_eq (B,y))) instth in
         let a,b = dest_imp (concl instth') in
         MP instth' (mk_imp_prf_fun tac implicans a)
         else fail)? failwith `rewrite_ICONV: lhs of implicans doesn't match term`)
  ? failwith `rewrite_ICONV: theorem not of the right form`;;

let rewrite_ICONV = GEN_rewrite_ICONV mk_imp_prf
and SEL_rewrite_ICONV = GEN_rewrite_ICONV mk_imp_prf_sel;;

let mk_ICONV_net rewrite thl =
 itlist
  enter_term
  (map (\f,th. (lhs(rand(concl th)),rewrite f th)) (mk_imp_eq_rewrites_list thl))
  nil_term_net;;

let basic_ICONV_rewrites =
[REFL_CLAUSE;
 EQ_CLAUSES;
 NOT_CLAUSES;
 AND_CLAUSES;
 OR_CLAUSES;
 IMP_CLAUSES;
 COND_CLAUSES;
 FORALL_SIMP;
 EXISTS_SIMP;
 ABS_SIMP;
 PAIR;
 FST;
 SND];;

let basic_ICONV_net = mk_ICONV_net rewrite_ICONV basic_ICONV_rewrites;;

let basic_SEL_ICONV_net = mk_ICONV_net SEL_rewrite_ICONV basic_ICONV_rewrites;;

letrec FIRST_ICONV c_cnvl tac implicans tm = ((hd c_cnvl) tac implicans tm)?
                                             (FIRST_ICONV (tl c_cnvl) tac implicans tm);;

let REWRITES_ICONV net tac implicans tm = FIRST_ICONV (lookup_term net tm) tac implicans tm;;

let GEN_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml =
TERM_WALK_ICONV 
  (REWRITES_ICONV 
     (merge_term_nets(mk_ICONV_net rewrite_ICONV thml)
                     basic_net) 
   tac);;

let GEN_SEL_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml =
TERM_WALK_ICONV 
  (REWRITES_ICONV 
     (merge_term_nets(mk_ICONV_net SEL_rewrite_ICONV thml)
                     basic_net) 
   tac);;

let REWRITE_ICONV = GEN_REWRITE_ICONV TRY_TOP_DEPTH_ICONV basic_ICONV_net
and ONCE_REWRITE_ICONV = GEN_REWRITE_ICONV TRY_ONCE_DEPTH_ICONV basic_ICONV_net
and PURE_REWRITE_ICONV = GEN_REWRITE_ICONV TRY_TOP_DEPTH_ICONV nil_term_net
and PURE_ONCE_REWRITE_ICONV =  GEN_REWRITE_ICONV TRY_ONCE_DEPTH_ICONV nil_term_net;;

let SEL_REWRITE_ICONV = GEN_SEL_REWRITE_ICONV TRY_TOP_DEPTH_ICONV basic_SEL_ICONV_net
and ONCE_SEL_REWRITE_ICONV = GEN_SEL_REWRITE_ICONV TRY_ONCE_DEPTH_ICONV basic_SEL_ICONV_net
and PURE_SEL_REWRITE_ICONV = GEN_SEL_REWRITE_ICONV TRY_TOP_DEPTH_ICONV nil_term_net
and PURE_ONCE_SEL_REWRITE_ICONV =  GEN_SEL_REWRITE_ICONV TRY_ONCE_DEPTH_ICONV nil_term_net;;

let ICONV_TAC ICONV : tactic = \(gl, g).
let thm = ICONV ([],gl) g in
let new_subgoals = map (\x. (gl,x)) (subtract (hyp thm) gl) in
let right = snd (dest_eq (concl thm)) in
if right = "T"
then (new_subgoals, \prfs. itlist PROVE_HYP prfs (EQ_MP (SYM thm) TRUTH))
else ((gl,snd (dest_eq (concl thm))).new_subgoals, 
      \prfs. itlist PROVE_HYP (tl prfs) (EQ_MP (SYM thm) (hd prfs)));;

% 

The following is a simple tactic which handles many simple cases.

%

let SIDECOND_TAC = REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [];;

let GEN_IMP_REWRITE_TAC TERM_WALK_ICONV basic_net tac thml : tactic = 
  ICONV_TAC (GEN_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml);;

let IMP_REWRITE_TAC = GEN_IMP_REWRITE_TAC TRY_TOP_DEPTH_ICONV basic_ICONV_net
and IMP_PURE_REWRITE_TAC = GEN_IMP_REWRITE_TAC TRY_TOP_DEPTH_ICONV nil_term_net
and IMP_ONCE_REWRITE_TAC = GEN_IMP_REWRITE_TAC TRY_ONCE_DEPTH_ICONV basic_ICONV_net
and IMP_PURE_ONCE_REWRITE_TAC = GEN_IMP_REWRITE_TAC TRY_ONCE_DEPTH_ICONV nil_term_net;;

let GEN_IMP_SEL_REWRITE_TAC TERM_WALK_ICONV basic_net tac thml : tactic = 
  ICONV_TAC (GEN_SEL_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml);;

let IMP_SEL_REWRITE_TAC = GEN_IMP_SEL_REWRITE_TAC TRY_TOP_DEPTH_ICONV basic_SEL_ICONV_net
and IMP_PURE_SEL_REWRITE_TAC = GEN_IMP_SEL_REWRITE_TAC TRY_TOP_DEPTH_ICONV nil_term_net
and IMP_ONCE_SEL_REWRITE_TAC = GEN_IMP_SEL_REWRITE_TAC TRY_ONCE_DEPTH_ICONV basic_SEL_ICONV_net
and IMP_PURE_ONCE_SEL_REWRITE_TAC = GEN_IMP_SEL_REWRITE_TAC TRY_ONCE_DEPTH_ICONV nil_term_net;;

let ICONV_RULE ICONV thm = 
EQ_MP (ICONV ([],hyp thm) (concl thm)) thm;;

let GEN_IMP_REWRITE_RULE TERM_WALK_ICONV basic_net tac thml thm =
  ICONV_RULE (GEN_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml) thm;;

let IMP_REWRITE_RULE = GEN_IMP_REWRITE_RULE TRY_TOP_DEPTH_ICONV basic_ICONV_net
and IMP_PURE_REWRITE_RULE = GEN_IMP_REWRITE_RULE TRY_TOP_DEPTH_ICONV nil_term_net
and IMP_ONCE_REWRITE_RULE = GEN_IMP_REWRITE_RULE TRY_ONCE_DEPTH_ICONV basic_ICONV_net
and IMP_PURE_ONCE_REWRITE_RULE = GEN_IMP_REWRITE_RULE TRY_ONCE_DEPTH_ICONV nil_term_net;;

let GEN_IMP_SEL_REWRITE_RULE TERM_WALK_ICONV basic_net tac thml thm =
  ICONV_RULE (GEN_SEL_REWRITE_ICONV TERM_WALK_ICONV basic_net tac thml) thm;;

let IMP_SEL_REWRITE_RULE = GEN_IMP_SEL_REWRITE_RULE TRY_TOP_DEPTH_ICONV basic_SEL_ICONV_net
and IMP_PURE_SEL_REWRITE_RULE = GEN_IMP_SEL_REWRITE_RULE TRY_TOP_DEPTH_ICONV nil_term_net
and IMP_ONCE_SEL_REWRITE_RULE = GEN_IMP_SEL_REWRITE_RULE TRY_ONCE_DEPTH_ICONV basic_SEL_ICONV_net
and IMP_PURE_ONCE_SEL_REWRITE_RULE = GEN_IMP_SEL_REWRITE_RULE TRY_ONCE_DEPTH_ICONV nil_term_net;;

let IMP_ONCE_ASM_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_ONCE_REWRITE_TAC tac (thml@asl))
and IMP_ASM_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_REWRITE_TAC tac (thml@asl))
and IMP_PURE_ONCE_ASM_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_PURE_ONCE_REWRITE_TAC tac (thml@asl))
and IMP_PURE_ASM_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_PURE_REWRITE_TAC tac (thml@asl));;

let IMP_ONCE_ASM_SEL_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_ONCE_SEL_REWRITE_TAC tac (thml@asl))
and IMP_ASM_SEL_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_SEL_REWRITE_TAC tac (thml@asl))
and IMP_PURE_ONCE_ASM_SEL_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_PURE_ONCE_SEL_REWRITE_TAC tac (thml@asl))
and IMP_PURE_ASM_SEL_REWRITE_TAC tac thml = ASSUM_LIST (\asl. IMP_PURE_SEL_REWRITE_TAC tac (thml@asl));;

%

The following two conversions deal with doing conversions on subterms.
SEARCH_ICONV f does an ICONV on all terms satisfying the predicate f.
SUBTERM_ICONV t does an ICONV on all subterms t.  They can be composed to
do more delicate work.  Of course the various (composable) "steering"
conversions like CONJ1_ICONV can also be used to direct conversions to
specific sub-terms.  I have not, however, supplied a full set of these.

%

let SEARCH_ICONV f h_cnv =
  TRY_ONCE_DEPTH_ICONV (\tml t. if f t then h_cnv tml t else fail);;

let SUBTERM_ICONV t = SEARCH_ICONV (\u. t = u);;

%

The following rules are useful for preprocessing implicational rewrites:

%

%

IMP_GEN_SYM transforms A ==> (X = Y) to A ==> (Y = x)

%

let GEN_IMP_SYM = GEN_ALL o (CONV_RULE (RAND_CONV SYM_CONV)) o SPEC_ALL;;