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