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