src/Provers/eqsubst.ML
author wenzelm
Wed Apr 04 23:29:33 2007 +0200 (2007-04-04)
changeset 22596 d0d2af4db18f
parent 22578 b0eb5652f210
child 22727 473c7f67c64f
permissions -rw-r--r--
rep_thm/cterm/ctyp: removed obsolete sign field;
     1 (*  Title:      Provers/eqsubst.ML
     2     ID:         $Id$
     3     Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
     4 
     5 A proof method to perform a substiution using an equation.
     6 *)
     7 
     8 signature EQSUBST =
     9 sig
    10   (* a type abriviation for match information *)
    11   type match =
    12        ((indexname * (sort * typ)) list (* type instantiations *)
    13         * (indexname * (typ * term)) list) (* term instantiations *)
    14        * (string * typ) list (* fake named type abs env *)
    15        * (string * typ) list (* type abs env *)
    16        * term (* outer term *)
    17 
    18   type searchinfo =
    19        theory
    20        * int (* maxidx *)
    21        * Zipper.T (* focusterm to search under *)
    22 
    23     exception eqsubst_occL_exp of
    24        string * int list * Thm.thm list * int * Thm.thm
    25     
    26     (* low level substitution functions *)
    27     val apply_subst_in_asm :
    28        int ->
    29        Thm.thm ->
    30        Thm.thm ->
    31        (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
    32     val apply_subst_in_concl :
    33        int ->
    34        Thm.thm ->
    35        Thm.cterm list * Thm.thm ->
    36        Thm.thm -> match -> Thm.thm Seq.seq
    37 
    38     (* matching/unification within zippers *)
    39     val clean_match_z :
    40        Context.theory -> Term.term -> Zipper.T -> match option
    41     val clean_unify_z :
    42        Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
    43 
    44     (* skipping things in seq seq's *)
    45 
    46    (* skipping non-empty sub-sequences but when we reach the end
    47       of the seq, remembering how much we have left to skip. *)
    48     datatype 'a skipseq = SkipMore of int
    49       | SkipSeq of 'a Seq.seq Seq.seq;
    50 
    51     val skip_first_asm_occs_search :
    52        ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    53        'a -> int -> 'b -> 'c skipseq
    54     val skip_first_occs_search :
    55        int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    56     val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    57 
    58     (* tactics *)
    59     val eqsubst_asm_tac :
    60        Proof.context ->
    61        int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    62     val eqsubst_asm_tac' :
    63        Proof.context ->
    64        (searchinfo -> int -> Term.term -> match skipseq) ->
    65        int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    66     val eqsubst_tac :
    67        Proof.context ->
    68        int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    69     val eqsubst_tac' :
    70        Proof.context ->
    71        (searchinfo -> Term.term -> match Seq.seq) 
    72        -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    73 
    74 
    75     val fakefree_badbounds :
    76        (string * Term.typ) list ->
    77        Term.term ->
    78        (string * Term.typ) list * (string * Term.typ) list * Term.term
    79 
    80     val mk_foo_match :
    81        (Term.term -> Term.term) ->
    82        ('a * Term.typ) list -> Term.term -> Term.term
    83 
    84     (* preparing substitution *)
    85     val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    86     val prep_concl_subst :
    87        int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    88     val prep_subst_in_asm :
    89        int -> Thm.thm -> int ->
    90        (Thm.cterm list * int * int * Thm.thm) * searchinfo
    91     val prep_subst_in_asms :
    92        int -> Thm.thm ->
    93        ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
    94     val prep_zipper_match :
    95        Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
    96 
    97     (* search for substitutions *)
    98     val valid_match_start : Zipper.T -> bool
    99     val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   100     val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   101     val searchf_lr_unify_all :
   102        searchinfo -> Term.term -> match Seq.seq Seq.seq
   103     val searchf_lr_unify_valid :
   104        searchinfo -> Term.term -> match Seq.seq Seq.seq
   105 
   106 
   107     (* syntax tools *)
   108     val ith_syntax : Args.T list -> int list * Args.T list
   109     val options_syntax : Args.T list -> bool * Args.T list
   110 
   111     (* Isar level hooks *)
   112     val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   113     val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   114     val subst_meth : Method.src -> Proof.context -> Proof.method
   115     val setup : theory -> theory
   116 
   117 end;
   118 
   119 structure EqSubst
   120 : EQSUBST
   121 = struct
   122 
   123 structure Z = Zipper;
   124 
   125 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
   126 fun prep_meta_eq ctxt =
   127   let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
   128   in mk #> map Drule.zero_var_indexes end;
   129 
   130 
   131   (* a type abriviation for match information *)
   132   type match =
   133        ((indexname * (sort * typ)) list (* type instantiations *)
   134         * (indexname * (typ * term)) list) (* term instantiations *)
   135        * (string * typ) list (* fake named type abs env *)
   136        * (string * typ) list (* type abs env *)
   137        * term (* outer term *)
   138 
   139   type searchinfo =
   140        theory
   141        * int (* maxidx *)
   142        * Zipper.T (* focusterm to search under *)
   143 
   144 
   145 (* skipping non-empty sub-sequences but when we reach the end
   146    of the seq, remembering how much we have left to skip. *)
   147 datatype 'a skipseq = SkipMore of int
   148   | SkipSeq of 'a Seq.seq Seq.seq;
   149 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
   150 fun skipto_skipseq m s = 
   151     let 
   152       fun skip_occs n sq = 
   153           case Seq.pull sq of 
   154             NONE => SkipMore n
   155           | SOME (h,t) => 
   156             (case Seq.pull h of NONE => skip_occs n t
   157              | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   158                          else skip_occs (n - 1) t)
   159     in (skip_occs m s) end;
   160 
   161 (* note: outerterm is the taget with the match replaced by a bound 
   162          variable : ie: "P lhs" beocmes "%x. P x" 
   163          insts is the types of instantiations of vars in lhs
   164          and typinsts is the type instantiations of types in the lhs
   165          Note: Final rule is the rule lifted into the ontext of the 
   166          taget thm. *)
   167 fun mk_foo_match mkuptermfunc Ts t = 
   168     let 
   169       val ty = Term.type_of t
   170       val bigtype = (rev (map snd Ts)) ---> ty
   171       fun mk_foo 0 t = t
   172         | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   173       val num_of_bnds = (length Ts)
   174       (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   175       val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   176     in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   177 
   178 (* T is outer bound vars, n is number of locally bound vars *)
   179 (* THINK: is order of Ts correct...? or reversed? *)
   180 fun fakefree_badbounds Ts t = 
   181     let val (FakeTs,Ts,newnames) = 
   182             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   183                            let val newname = Name.variant usednames n
   184                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   185                                (newname,ty)::Ts, 
   186                                newname::usednames) end)
   187                        ([],[],[])
   188                        Ts
   189     in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   190 
   191 (* before matching we need to fake the bound vars that are missing an
   192 abstraction. In this function we additionally construct the
   193 abstraction environment, and an outer context term (with the focus
   194 abstracted out) for use in rewriting with RWInst.rw *)
   195 fun prep_zipper_match z = 
   196     let 
   197       val t = Z.trm z  
   198       val c = Z.ctxt z
   199       val Ts = Z.C.nty_ctxt c
   200       val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   201       val absterm = mk_foo_match (Z.C.apply c) Ts' t'
   202     in
   203       (t', (FakeTs', Ts', absterm))
   204     end;
   205 
   206 (* Matching and Unification with exception handled *)
   207 fun clean_match thy (a as (pat, t)) =
   208   let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   209   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   210   end handle Pattern.MATCH => NONE;
   211 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   212 fun clean_unify sgn 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 sgn (pat_ty, tgt_ty) (Term.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              Envir.alist_of env);
   232           val initenv = Envir.Envir {asol = Vartab.empty,
   233                                      iTs = typinsttab, maxidx = ix2};
   234           val useq = Unify.smash_unifiers sgn [a] initenv
   235 	            handle 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 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         * (Thm.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 = (ref NONE : trace_subst_errT option ref);
   279 val trace_subst_search = 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 (Z.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 [Z.Here z] else [] in
   303             case Z.trm z 
   304              of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
   305                          @ here 
   306                          @ [Z.LookIn (Z.move_down_right z)]
   307               | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
   308               | _ => here
   309           end;
   310     in Z.lzy_search sf_valid_td_lr end;
   311 
   312 (* search all unifications *)
   313 fun searchf_lr_unify_all (sgn, maxidx, z) lhs =
   314     Seq.map (clean_unify_z sgn maxidx lhs) 
   315             (Z.limit_apply search_lr_all z);
   316 
   317 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
   318 fun searchf_lr_unify_valid (sgn, maxidx, z) lhs  =
   319     Seq.map (clean_unify_z sgn maxidx lhs) 
   320             (Z.limit_apply (search_lr_valid valid_match_start) z);
   321 
   322 
   323 (* apply a substitution in the conclusion of the theorem th *)
   324 (* cfvs are certified free var placeholders for goal params *)
   325 (* conclthm is a theorem of for just the conclusion *)
   326 (* m is instantiation/match information *)
   327 (* rule is the equation for substitution *)
   328 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   329     (RWInst.rw m rule conclthm)
   330       |> IsaND.unfix_frees cfvs
   331       |> RWInst.beta_eta_contract
   332       |> (fn r => Tactic.rtac r i th);
   333 
   334 (* substitute within the conclusion of goal i of gth, using a meta
   335 equation rule. Note that we assume rule has var indicies zero'd *)
   336 fun prep_concl_subst i gth =
   337     let
   338       val th = Thm.incr_indexes 1 gth;
   339       val tgt_term = Thm.prop_of th;
   340 
   341       val sgn = Thm.theory_of_thm th;
   342       val ctermify = Thm.cterm_of sgn;
   343       val trivify = Thm.trivial o ctermify;
   344 
   345       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   346       val cfvs = rev (map ctermify fvs);
   347 
   348       val conclterm = Logic.strip_imp_concl fixedbody;
   349       val conclthm = trivify conclterm;
   350       val maxidx = Term.maxidx_of_term conclterm;
   351       val ft = ((Z.move_down_right (* ==> *)
   352                  o Z.move_down_left (* Trueprop *)
   353                  o Z.mktop
   354                  o Thm.prop_of) conclthm)
   355     in
   356       ((cfvs, conclthm), (sgn, maxidx, ft))
   357     end;
   358 
   359 (* substitute using an object or meta level equality *)
   360 fun eqsubst_tac' ctxt searchf instepthm i th =
   361     let
   362       val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   363       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   364       fun rewrite_with_thm r =
   365           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   366           in searchf searchinfo lhs
   367              |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   368     in stepthms |> Seq.maps rewrite_with_thm end;
   369 
   370 
   371 (* distinct subgoals *)
   372 fun distinct_subgoals th =
   373   the_default th (SINGLE distinct_subgoals_tac th);
   374 
   375 (* General substitution of multiple occurances using one of
   376    the given theorems*)
   377 
   378 
   379 exception eqsubst_occL_exp of
   380           string * (int list) * (thm list) * int * thm;
   381 fun skip_first_occs_search occ srchf sinfo lhs =
   382     case (skipto_skipseq occ (srchf sinfo lhs)) of
   383       SkipMore _ => Seq.empty
   384     | SkipSeq ss => Seq.flat ss;
   385 
   386 fun eqsubst_tac ctxt occL thms i th =
   387     let val nprems = Thm.nprems_of th in
   388       if nprems < i then Seq.empty else
   389       let val thmseq = (Seq.of_list thms)
   390         fun apply_occ occ th =
   391             thmseq |> Seq.maps
   392                     (fn r => eqsubst_tac' 
   393                                ctxt 
   394                                (skip_first_occs_search
   395                                   occ searchf_lr_unify_valid) r
   396                                  (i + ((Thm.nprems_of th) - nprems))
   397                                  th);
   398         val sortedoccL =
   399             Library.sort (Library.rev_order o Library.int_ord) occL;
   400       in
   401         Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   402       end
   403     end
   404     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   405 
   406 
   407 (* inthms are the given arguments in Isar, and treated as eqstep with
   408    the first one, then the second etc *)
   409 fun eqsubst_meth ctxt occL inthms =
   410     Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   411 
   412 (* apply a substitution inside assumption j, keeps asm in the same place *)
   413 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   414     let
   415       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   416       val preelimrule =
   417           (RWInst.rw m rule pth)
   418             |> (Seq.hd o prune_params_tac)
   419             |> Thm.permute_prems 0 ~1 (* put old asm first *)
   420             |> IsaND.unfix_frees cfvs (* unfix any global params *)
   421             |> RWInst.beta_eta_contract; (* normal form *)
   422   (*    val elimrule =
   423           preelimrule
   424             |> Tactic.make_elim (* make into elim rule *)
   425             |> Thm.lift_rule (th2, i); (* lift into context *)
   426    *)
   427     in
   428       (* ~j because new asm starts at back, thus we subtract 1 *)
   429       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   430       (Tactic.dtac preelimrule i th2)
   431 
   432       (* (Thm.bicompose
   433                  false (* use unification *)
   434                  (true, (* elim resolution *)
   435                   elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   436                  i th2) *)
   437     end;
   438 
   439 
   440 (* prepare to substitute within the j'th premise of subgoal i of gth,
   441 using a meta-level equation. Note that we assume rule has var indicies
   442 zero'd. Note that we also assume that premt is the j'th premice of
   443 subgoal i of gth. Note the repetition of work done for each
   444 assumption, i.e. this can be made more efficient for search over
   445 multiple assumptions.  *)
   446 fun prep_subst_in_asm i gth j =
   447     let
   448       val th = Thm.incr_indexes 1 gth;
   449       val tgt_term = Thm.prop_of th;
   450 
   451       val sgn = Thm.theory_of_thm th;
   452       val ctermify = Thm.cterm_of sgn;
   453       val trivify = Thm.trivial o ctermify;
   454 
   455       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   456       val cfvs = rev (map ctermify fvs);
   457 
   458       val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   459       val asm_nprems = length (Logic.strip_imp_prems asmt);
   460 
   461       val pth = trivify asmt;
   462       val maxidx = Term.maxidx_of_term asmt;
   463 
   464       val ft = ((Z.move_down_right (* trueprop *)
   465                  o Z.mktop
   466                  o Thm.prop_of) pth)
   467     in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   468 
   469 (* prepare subst in every possible assumption *)
   470 fun prep_subst_in_asms i gth =
   471     map (prep_subst_in_asm i gth)
   472         ((fn l => Library.upto (1, length l))
   473            (Logic.prems_of_goal (Thm.prop_of gth) i));
   474 
   475 
   476 (* substitute in an assumption using an object or meta level equality *)
   477 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   478     let
   479       val asmpreps = prep_subst_in_asms i th;
   480       val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   481       fun rewrite_with_thm r =
   482           let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   483             fun occ_search occ [] = Seq.empty
   484               | occ_search occ ((asminfo, searchinfo)::moreasms) =
   485                 (case searchf searchinfo occ lhs of
   486                    SkipMore i => occ_search i moreasms
   487                  | SkipSeq ss =>
   488                    Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   489                                (occ_search 1 moreasms))
   490                               (* find later substs also *)
   491           in
   492             occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   493           end;
   494     in stepthms |> Seq.maps rewrite_with_thm end;
   495 
   496 
   497 fun skip_first_asm_occs_search searchf sinfo occ lhs =
   498     skipto_skipseq occ (searchf sinfo lhs);
   499 
   500 fun eqsubst_asm_tac ctxt occL thms i th =
   501     let val nprems = Thm.nprems_of th
   502     in
   503       if nprems < i then Seq.empty else
   504       let val thmseq = (Seq.of_list thms)
   505         fun apply_occ occK th =
   506             thmseq |> Seq.maps
   507                     (fn r =>
   508                         eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   509                                             searchf_lr_unify_valid) occK r
   510                                          (i + ((Thm.nprems_of th) - nprems))
   511                                          th);
   512         val sortedoccs =
   513             Library.sort (Library.rev_order o Library.int_ord) occL
   514       in
   515         Seq.map distinct_subgoals
   516                 (Seq.EVERY (map apply_occ sortedoccs) th)
   517       end
   518     end
   519     handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   520 
   521 (* inthms are the given arguments in Isar, and treated as eqstep with
   522    the first one, then the second etc *)
   523 fun eqsubst_asm_meth ctxt occL inthms =
   524     Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   525 
   526 (* syntax for options, given "(asm)" will give back true, without
   527    gives back false *)
   528 val options_syntax =
   529     (Args.parens (Args.$$$ "asm") >> (K true)) ||
   530      (Scan.succeed false);
   531 
   532 val ith_syntax =
   533     (Args.parens (Scan.repeat Args.nat))
   534       || (Scan.succeed [0]);
   535 
   536 (* combination method that takes a flag (true indicates that subst
   537 should be done to an assumption, false = apply to the conclusion of
   538 the goal) as well as the theorems to use *)
   539 fun subst_meth src =
   540   Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   541   #> (fn (((asmflag, occL), inthms), ctxt) =>
   542     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   543 
   544 
   545 val setup =
   546   Method.add_method ("subst", subst_meth, "single-step substitution");
   547 
   548 end;