src/Tools/eqsubst.ML
author wenzelm
Tue Aug 09 15:50:13 2011 +0200 (2011-08-09)
changeset 44095 3ea5fae095dc
parent 43324 2b47822868e4
child 49339 d1fcb4de8349
permissions -rw-r--r--
misc tuning and simplification;
     1 (*  Title:      Tools/eqsubst.ML
     2     Author:     Lucas Dixon, University of Edinburgh
     3 
     4 A proof method to perform a substiution using an equation.
     5 *)
     6 
     7 signature EQSUBST =
     8 sig
     9   (* a type abbreviation for match information *)
    10   type match =
    11        ((indexname * (sort * typ)) list (* type instantiations *)
    12         * (indexname * (typ * term)) list) (* term instantiations *)
    13        * (string * typ) list (* fake named type abs env *)
    14        * (string * typ) list (* type abs env *)
    15        * term (* outer term *)
    16 
    17   type searchinfo =
    18        theory
    19        * int (* maxidx *)
    20        * Zipper.T (* focusterm to search under *)
    21 
    22     exception eqsubst_occL_exp of
    23        string * int list * thm list * int * thm
    24     
    25     (* low level substitution functions *)
    26     val apply_subst_in_asm :
    27        int ->
    28        thm ->
    29        thm ->
    30        (cterm list * int * 'a * thm) * match -> thm Seq.seq
    31     val apply_subst_in_concl :
    32        int ->
    33        thm ->
    34        cterm list * thm ->
    35        thm -> match -> thm Seq.seq
    36 
    37     (* matching/unification within zippers *)
    38     val clean_match_z :
    39        theory -> term -> Zipper.T -> match option
    40     val clean_unify_z :
    41        theory -> int -> term -> Zipper.T -> match Seq.seq
    42 
    43     (* skipping things in seq seq's *)
    44 
    45    (* skipping non-empty sub-sequences but when we reach the end
    46       of the seq, remembering how much we have left to skip. *)
    47     datatype 'a skipseq = SkipMore of int
    48       | SkipSeq of 'a Seq.seq Seq.seq;
    49 
    50     val skip_first_asm_occs_search :
    51        ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    52        'a -> int -> 'b -> 'c skipseq
    53     val skip_first_occs_search :
    54        int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    55     val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    56 
    57     (* tactics *)
    58     val eqsubst_asm_tac :
    59        Proof.context ->
    60        int list -> thm list -> int -> tactic
    61     val eqsubst_asm_tac' :
    62        Proof.context ->
    63        (searchinfo -> int -> term -> match skipseq) ->
    64        int -> thm -> int -> tactic
    65     val eqsubst_tac :
    66        Proof.context ->
    67        int list -> (* list of occurences to rewrite, use [0] for any *)
    68        thm list -> int -> tactic
    69     val eqsubst_tac' :
    70        Proof.context -> (* proof context *)
    71        (searchinfo -> term -> match Seq.seq) (* search function *)
    72        -> thm (* equation theorem to rewrite with *)
    73        -> int (* subgoal number in goal theorem *)
    74        -> thm (* goal theorem *)
    75        -> thm Seq.seq (* rewritten goal theorem *)
    76 
    77 
    78     val fakefree_badbounds :
    79        (string * typ) list ->
    80        term ->
    81        (string * typ) list * (string * typ) list * term
    82 
    83     val mk_foo_match :
    84        (term -> term) ->
    85        ('a * typ) list -> term -> term
    86 
    87     (* preparing substitution *)
    88     val prep_meta_eq : Proof.context -> thm -> thm list
    89     val prep_concl_subst :
    90        int -> thm -> (cterm list * thm) * searchinfo
    91     val prep_subst_in_asm :
    92        int -> thm -> int ->
    93        (cterm list * int * int * thm) * searchinfo
    94     val prep_subst_in_asms :
    95        int -> thm ->
    96        ((cterm list * int * int * thm) * searchinfo) list
    97     val prep_zipper_match :
    98        Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
    99 
   100     (* search for substitutions *)
   101     val valid_match_start : Zipper.T -> bool
   102     val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   103     val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   104     val searchf_lr_unify_all :
   105        searchinfo -> term -> match Seq.seq Seq.seq
   106     val searchf_lr_unify_valid :
   107        searchinfo -> term -> match Seq.seq Seq.seq
   108     val searchf_bt_unify_valid :
   109        searchinfo -> term -> match Seq.seq Seq.seq
   110 
   111     (* Isar level hooks *)
   112     val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
   113     val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
   114     val setup : theory -> theory
   115 
   116 end;
   117 
   118 structure EqSubst: EQSUBST =
   119 struct
   120 
   121 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
   122 fun prep_meta_eq ctxt =
   123   Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes;
   124 
   125 
   126   (* a type abriviation for match information *)
   127   type match =
   128        ((indexname * (sort * typ)) list (* type instantiations *)
   129         * (indexname * (typ * term)) list) (* term instantiations *)
   130        * (string * typ) list (* fake named type abs env *)
   131        * (string * typ) list (* type abs env *)
   132        * term (* outer term *)
   133 
   134   type searchinfo =
   135        theory
   136        * int (* maxidx *)
   137        * Zipper.T (* focusterm to search under *)
   138 
   139 
   140 (* skipping non-empty sub-sequences but when we reach the end
   141    of the seq, remembering how much we have left to skip. *)
   142 datatype 'a skipseq = SkipMore of int
   143   | SkipSeq of 'a Seq.seq Seq.seq;
   144 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
   145 fun skipto_skipseq m s = 
   146     let 
   147       fun skip_occs n sq = 
   148           case Seq.pull sq of 
   149             NONE => SkipMore n
   150           | SOME (h,t) => 
   151             (case Seq.pull h of NONE => skip_occs n t
   152              | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   153                          else skip_occs (n - 1) t)
   154     in (skip_occs m s) end;
   155 
   156 (* note: outerterm is the taget with the match replaced by a bound 
   157          variable : ie: "P lhs" beocmes "%x. P x" 
   158          insts is the types of instantiations of vars in lhs
   159          and typinsts is the type instantiations of types in the lhs
   160          Note: Final rule is the rule lifted into the ontext of the 
   161          taget thm. *)
   162 fun mk_foo_match mkuptermfunc Ts t = 
   163     let 
   164       val ty = Term.type_of t
   165       val bigtype = (rev (map snd Ts)) ---> ty
   166       fun mk_foo 0 t = t
   167         | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   168       val num_of_bnds = (length Ts)
   169       (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   170       val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   171     in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   172 
   173 (* T is outer bound vars, n is number of locally bound vars *)
   174 (* THINK: is order of Ts correct...? or reversed? *)
   175 fun fakefree_badbounds Ts t = 
   176     let val (FakeTs,Ts,newnames) = 
   177             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   178                            let val newname = singleton (Name.variant_list usednames) n
   179                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   180                                (newname,ty)::Ts, 
   181                                newname::usednames) end)
   182                        ([],[],[])
   183                        Ts
   184     in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   185 
   186 (* before matching we need to fake the bound vars that are missing an
   187 abstraction. In this function we additionally construct the
   188 abstraction environment, and an outer context term (with the focus
   189 abstracted out) for use in rewriting with RWInst.rw *)
   190 fun prep_zipper_match z = 
   191     let 
   192       val t = Zipper.trm z  
   193       val c = Zipper.ctxt z
   194       val Ts = Zipper.C.nty_ctxt c
   195       val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   196       val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
   197     in
   198       (t', (FakeTs', Ts', absterm))
   199     end;
   200 
   201 (* Matching and Unification with exception handled *)
   202 fun clean_match thy (a as (pat, t)) =
   203   let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   204   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   205   end handle Pattern.MATCH => NONE;
   206 
   207 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   208 fun clean_unify thry ix (a as (pat, tgt)) =
   209     let
   210       (* type info will be re-derived, maybe this can be cached
   211          for efficiency? *)
   212       val pat_ty = Term.type_of pat;
   213       val tgt_ty = Term.type_of tgt;
   214       (* is it OK to ignore the type instantiation info?
   215          or should I be using it? *)
   216       val typs_unify =
   217           SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
   218             handle Type.TUNIFY => NONE;
   219     in
   220       case typs_unify of
   221         SOME (typinsttab, ix2) =>
   222         let
   223       (* is it right to throw away the flexes?
   224          or should I be using them somehow? *)
   225           fun mk_insts env =
   226             (Vartab.dest (Envir.type_env env),
   227              Vartab.dest (Envir.term_env env));
   228           val initenv =
   229             Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
   230           val useq = Unify.smash_unifiers thry [a] initenv
   231               handle ListPair.UnequalLengths => Seq.empty
   232                    | Term.TERM _ => Seq.empty;
   233           fun clean_unify' useq () =
   234               (case (Seq.pull useq) of
   235                  NONE => NONE
   236                | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   237               handle ListPair.UnequalLengths => NONE
   238                    | Term.TERM _ => NONE
   239         in
   240           (Seq.make (clean_unify' useq))
   241         end
   242       | NONE => Seq.empty
   243     end;
   244 
   245 (* Matching and Unification for zippers *)
   246 (* Note: Ts is a modified version of the original names of the outer
   247 bound variables. New names have been introduced to make sure they are
   248 unique w.r.t all names in the term and each other. usednames' is
   249 oldnames + new names. *)
   250 fun clean_match_z thy pat z = 
   251     let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   252       case clean_match thy (pat, t) of 
   253         NONE => NONE 
   254       | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   255 (* ix = max var index *)
   256 fun clean_unify_z sgn ix pat z = 
   257     let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   258     Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   259             (clean_unify sgn ix (t, pat)) end;
   260 
   261 
   262 (* FOR DEBUGGING...
   263 type trace_subst_errT = int (* subgoal *)
   264         * thm (* thm with all goals *)
   265         * (cterm list (* certified free var placeholders for vars *)
   266            * thm)  (* trivial thm of goal concl *)
   267             (* possible matches/unifiers *)
   268         * thm (* rule *)
   269         * (((indexname * typ) list (* type instantiations *)
   270               * (indexname * term) list ) (* term instantiations *)
   271              * (string * typ) list (* Type abs env *)
   272              * term) (* outer term *);
   273 
   274 val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
   275 val trace_subst_search = Unsynchronized.ref false;
   276 exception trace_subst_exp of trace_subst_errT;
   277 *)
   278 
   279 
   280 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   281   | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   282   | bot_left_leaf_of x = x;
   283 
   284 (* Avoid considering replacing terms which have a var at the head as
   285    they always succeed trivially, and uninterestingly. *)
   286 fun valid_match_start z =
   287     (case bot_left_leaf_of (Zipper.trm z) of 
   288       Var _ => false 
   289       | _ => true);
   290 
   291 (* search from top, left to right, then down *)
   292 val search_lr_all = ZipperSearch.all_bl_ur;
   293 
   294 (* search from top, left to right, then down *)
   295 fun search_lr_valid validf =
   296     let 
   297       fun sf_valid_td_lr z = 
   298           let val here = if validf z then [Zipper.Here z] else [] in
   299             case Zipper.trm z 
   300              of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] 
   301                          @ here 
   302                          @ [Zipper.LookIn (Zipper.move_down_right z)]
   303               | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
   304               | _ => here
   305           end;
   306     in Zipper.lzy_search sf_valid_td_lr end;
   307 
   308 (* search from bottom to top, left to right *)
   309 
   310 fun search_bt_valid validf =
   311     let 
   312       fun sf_valid_td_lr z = 
   313           let val here = if validf z then [Zipper.Here z] else [] in
   314             case Zipper.trm z 
   315              of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), 
   316                           Zipper.LookIn (Zipper.move_down_right z)] @ here
   317               | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
   318               | _ => here
   319           end;
   320     in Zipper.lzy_search sf_valid_td_lr end;
   321 
   322 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   323     Seq.map (clean_unify_z sgn maxidx lhs) 
   324             (Zipper.limit_apply f z);
   325 
   326 (* search all unifications *)
   327 val searchf_lr_unify_all =
   328     searchf_unify_gen search_lr_all;
   329 
   330 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
   331 val searchf_lr_unify_valid = 
   332     searchf_unify_gen (search_lr_valid valid_match_start);
   333 
   334 val searchf_bt_unify_valid =
   335     searchf_unify_gen (search_bt_valid valid_match_start);
   336 
   337 (* apply a substitution in the conclusion of the theorem th *)
   338 (* cfvs are certified free var placeholders for goal params *)
   339 (* conclthm is a theorem of for just the conclusion *)
   340 (* m is instantiation/match information *)
   341 (* rule is the equation for substitution *)
   342 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   343     (RWInst.rw m rule conclthm)
   344       |> IsaND.unfix_frees cfvs
   345       |> RWInst.beta_eta_contract
   346       |> (fn r => Tactic.rtac r i th);
   347 
   348 (* substitute within the conclusion of goal i of gth, using a meta
   349 equation rule. Note that we assume rule has var indicies zero'd *)
   350 fun prep_concl_subst i gth =
   351     let
   352       val th = Thm.incr_indexes 1 gth;
   353       val tgt_term = Thm.prop_of th;
   354 
   355       val sgn = Thm.theory_of_thm th;
   356       val ctermify = Thm.cterm_of sgn;
   357       val trivify = Thm.trivial o ctermify;
   358 
   359       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   360       val cfvs = rev (map ctermify fvs);
   361 
   362       val conclterm = Logic.strip_imp_concl fixedbody;
   363       val conclthm = trivify conclterm;
   364       val maxidx = Thm.maxidx_of th;
   365       val ft = ((Zipper.move_down_right (* ==> *)
   366                  o Zipper.move_down_left (* Trueprop *)
   367                  o Zipper.mktop
   368                  o Thm.prop_of) conclthm)
   369     in
   370       ((cfvs, conclthm), (sgn, maxidx, ft))
   371     end;
   372 
   373 (* substitute using an object or meta level equality *)
   374 fun eqsubst_tac' ctxt searchf instepthm i th =
   375     let
   376       val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   377       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   378       fun rewrite_with_thm r =
   379           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   380           in searchf searchinfo lhs
   381              |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   382     in stepthms |> Seq.maps rewrite_with_thm end;
   383 
   384 
   385 (* distinct subgoals *)
   386 fun distinct_subgoals th =
   387   the_default th (SINGLE distinct_subgoals_tac th);
   388 
   389 (* General substitution of multiple occurances using one of
   390    the given theorems*)
   391 
   392 
   393 exception eqsubst_occL_exp of
   394           string * (int list) * (thm list) * int * thm;
   395 fun skip_first_occs_search occ srchf sinfo lhs =
   396     case (skipto_skipseq occ (srchf sinfo lhs)) of
   397       SkipMore _ => Seq.empty
   398     | SkipSeq ss => Seq.flat ss;
   399 
   400 (* The occL is a list of integers indicating which occurence
   401 w.r.t. the search order, to rewrite. Backtracking will also find later
   402 occurences, but all earlier ones are skipped. Thus you can use [0] to
   403 just find all rewrites. *)
   404 
   405 fun eqsubst_tac ctxt occL thms i th =
   406     let val nprems = Thm.nprems_of th in
   407       if nprems < i then Seq.empty else
   408       let val thmseq = (Seq.of_list thms)
   409         fun apply_occ occ th =
   410             thmseq |> Seq.maps
   411                     (fn r => eqsubst_tac' 
   412                                ctxt 
   413                                (skip_first_occs_search
   414                                   occ searchf_lr_unify_valid) r
   415                                  (i + ((Thm.nprems_of th) - nprems))
   416                                  th);
   417         val sortedoccL =
   418             Library.sort (Library.rev_order o Library.int_ord) occL;
   419       in
   420         Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   421       end
   422     end
   423     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   424 
   425 
   426 (* inthms are the given arguments in Isar, and treated as eqstep with
   427    the first one, then the second etc *)
   428 fun eqsubst_meth ctxt occL inthms =
   429     SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   430 
   431 (* apply a substitution inside assumption j, keeps asm in the same place *)
   432 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   433     let
   434       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   435       val preelimrule =
   436           (RWInst.rw m rule pth)
   437             |> (Seq.hd o prune_params_tac)
   438             |> Thm.permute_prems 0 ~1 (* put old asm first *)
   439             |> IsaND.unfix_frees cfvs (* unfix any global params *)
   440             |> RWInst.beta_eta_contract; (* normal form *)
   441   (*    val elimrule =
   442           preelimrule
   443             |> Tactic.make_elim (* make into elim rule *)
   444             |> Thm.lift_rule (th2, i); (* lift into context *)
   445    *)
   446     in
   447       (* ~j because new asm starts at back, thus we subtract 1 *)
   448       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   449       (Tactic.dtac preelimrule i th2)
   450 
   451       (* (Thm.bicompose
   452                  false (* use unification *)
   453                  (true, (* elim resolution *)
   454                   elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   455                  i th2) *)
   456     end;
   457 
   458 
   459 (* prepare to substitute within the j'th premise of subgoal i of gth,
   460 using a meta-level equation. Note that we assume rule has var indicies
   461 zero'd. Note that we also assume that premt is the j'th premice of
   462 subgoal i of gth. Note the repetition of work done for each
   463 assumption, i.e. this can be made more efficient for search over
   464 multiple assumptions.  *)
   465 fun prep_subst_in_asm i gth j =
   466     let
   467       val th = Thm.incr_indexes 1 gth;
   468       val tgt_term = Thm.prop_of th;
   469 
   470       val sgn = Thm.theory_of_thm th;
   471       val ctermify = Thm.cterm_of sgn;
   472       val trivify = Thm.trivial o ctermify;
   473 
   474       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   475       val cfvs = rev (map ctermify fvs);
   476 
   477       val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   478       val asm_nprems = length (Logic.strip_imp_prems asmt);
   479 
   480       val pth = trivify asmt;
   481       val maxidx = Thm.maxidx_of th;
   482 
   483       val ft = ((Zipper.move_down_right (* trueprop *)
   484                  o Zipper.mktop
   485                  o Thm.prop_of) pth)
   486     in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   487 
   488 (* prepare subst in every possible assumption *)
   489 fun prep_subst_in_asms i gth =
   490     map (prep_subst_in_asm i gth)
   491         ((fn l => Library.upto (1, length l))
   492            (Logic.prems_of_goal (Thm.prop_of gth) i));
   493 
   494 
   495 (* substitute in an assumption using an object or meta level equality *)
   496 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   497     let
   498       val asmpreps = prep_subst_in_asms i th;
   499       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   500       fun rewrite_with_thm r =
   501           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   502             fun occ_search occ [] = Seq.empty
   503               | occ_search occ ((asminfo, searchinfo)::moreasms) =
   504                 (case searchf searchinfo occ lhs of
   505                    SkipMore i => occ_search i moreasms
   506                  | SkipSeq ss =>
   507                    Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   508                                (occ_search 1 moreasms))
   509                               (* find later substs also *)
   510           in
   511             occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   512           end;
   513     in stepthms |> Seq.maps rewrite_with_thm end;
   514 
   515 
   516 fun skip_first_asm_occs_search searchf sinfo occ lhs =
   517     skipto_skipseq occ (searchf sinfo lhs);
   518 
   519 fun eqsubst_asm_tac ctxt occL thms i th =
   520     let val nprems = Thm.nprems_of th
   521     in
   522       if nprems < i then Seq.empty else
   523       let val thmseq = (Seq.of_list thms)
   524         fun apply_occ occK th =
   525             thmseq |> Seq.maps
   526                     (fn r =>
   527                         eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   528                                             searchf_lr_unify_valid) occK r
   529                                          (i + ((Thm.nprems_of th) - nprems))
   530                                          th);
   531         val sortedoccs =
   532             Library.sort (Library.rev_order o Library.int_ord) occL
   533       in
   534         Seq.map distinct_subgoals
   535                 (Seq.EVERY (map apply_occ sortedoccs) th)
   536       end
   537     end
   538     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   539 
   540 (* inthms are the given arguments in Isar, and treated as eqstep with
   541    the first one, then the second etc *)
   542 fun eqsubst_asm_meth ctxt occL inthms =
   543     SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   544 
   545 (* combination method that takes a flag (true indicates that subst
   546    should be done to an assumption, false = apply to the conclusion of
   547    the goal) as well as the theorems to use *)
   548 val setup =
   549   Method.setup @{binding subst}
   550     (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
   551         Attrib.thms >>
   552       (fn ((asm, occL), inthms) => fn ctxt =>
   553         (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
   554     "single-step substitution";
   555 
   556 end;