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