src/Provers/eqsubst.ML
author wenzelm
Thu Aug 09 23:53:51 2007 +0200 (2007-08-09)
changeset 24209 8a2c8d623e43
parent 23064 6ee131d1a618
child 27033 6ef5134fc631
permissions -rw-r--r--
schedule: misc cleanup, more precise task model;
     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 -> (* list of occurences to rewrite, use [0] for any *)
    69        Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    70     val eqsubst_tac' :
    71        Proof.context -> (* proof context *)
    72        (searchinfo -> Term.term -> match Seq.seq) (* search function *)
    73        -> Thm.thm (* equation theorem to rewrite with *)
    74        -> int (* subgoal number in goal theorem *)
    75        -> Thm.thm (* goal theorem *)
    76        -> Thm.thm Seq.seq (* rewritten goal theorem *)
    77 
    78 
    79     val fakefree_badbounds :
    80        (string * Term.typ) list ->
    81        Term.term ->
    82        (string * Term.typ) list * (string * Term.typ) list * Term.term
    83 
    84     val mk_foo_match :
    85        (Term.term -> Term.term) ->
    86        ('a * Term.typ) list -> Term.term -> Term.term
    87 
    88     (* preparing substitution *)
    89     val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    90     val prep_concl_subst :
    91        int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    92     val prep_subst_in_asm :
    93        int -> Thm.thm -> int ->
    94        (Thm.cterm list * int * int * Thm.thm) * searchinfo
    95     val prep_subst_in_asms :
    96        int -> Thm.thm ->
    97        ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
    98     val prep_zipper_match :
    99        Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
   100 
   101     (* search for substitutions *)
   102     val valid_match_start : Zipper.T -> bool
   103     val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   104     val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   105     val searchf_lr_unify_all :
   106        searchinfo -> Term.term -> match Seq.seq Seq.seq
   107     val searchf_lr_unify_valid :
   108        searchinfo -> Term.term -> match Seq.seq Seq.seq
   109     val searchf_bt_unify_valid :
   110        searchinfo -> Term.term -> match Seq.seq Seq.seq
   111 
   112     (* syntax tools *)
   113     val ith_syntax : Args.T list -> int list * Args.T list
   114     val options_syntax : Args.T list -> bool * Args.T list
   115 
   116     (* Isar level hooks *)
   117     val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   118     val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   119     val subst_meth : Method.src -> Proof.context -> Proof.method
   120     val setup : theory -> theory
   121 
   122 end;
   123 
   124 structure EqSubst
   125 : EQSUBST
   126 = struct
   127 
   128 structure Z = Zipper;
   129 
   130 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
   131 fun prep_meta_eq ctxt =
   132   let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
   133   in mk #> map Drule.zero_var_indexes end;
   134 
   135 
   136   (* a type abriviation for match information *)
   137   type match =
   138        ((indexname * (sort * typ)) list (* type instantiations *)
   139         * (indexname * (typ * term)) list) (* term instantiations *)
   140        * (string * typ) list (* fake named type abs env *)
   141        * (string * typ) list (* type abs env *)
   142        * term (* outer term *)
   143 
   144   type searchinfo =
   145        theory
   146        * int (* maxidx *)
   147        * Zipper.T (* focusterm to search under *)
   148 
   149 
   150 (* skipping non-empty sub-sequences but when we reach the end
   151    of the seq, remembering how much we have left to skip. *)
   152 datatype 'a skipseq = SkipMore of int
   153   | SkipSeq of 'a Seq.seq Seq.seq;
   154 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
   155 fun skipto_skipseq m s = 
   156     let 
   157       fun skip_occs n sq = 
   158           case Seq.pull sq of 
   159             NONE => SkipMore n
   160           | SOME (h,t) => 
   161             (case Seq.pull h of NONE => skip_occs n t
   162              | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   163                          else skip_occs (n - 1) t)
   164     in (skip_occs m s) end;
   165 
   166 (* note: outerterm is the taget with the match replaced by a bound 
   167          variable : ie: "P lhs" beocmes "%x. P x" 
   168          insts is the types of instantiations of vars in lhs
   169          and typinsts is the type instantiations of types in the lhs
   170          Note: Final rule is the rule lifted into the ontext of the 
   171          taget thm. *)
   172 fun mk_foo_match mkuptermfunc Ts t = 
   173     let 
   174       val ty = Term.type_of t
   175       val bigtype = (rev (map snd Ts)) ---> ty
   176       fun mk_foo 0 t = t
   177         | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   178       val num_of_bnds = (length Ts)
   179       (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   180       val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   181     in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   182 
   183 (* T is outer bound vars, n is number of locally bound vars *)
   184 (* THINK: is order of Ts correct...? or reversed? *)
   185 fun fakefree_badbounds Ts t = 
   186     let val (FakeTs,Ts,newnames) = 
   187             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   188                            let val newname = Name.variant usednames n
   189                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   190                                (newname,ty)::Ts, 
   191                                newname::usednames) end)
   192                        ([],[],[])
   193                        Ts
   194     in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   195 
   196 (* before matching we need to fake the bound vars that are missing an
   197 abstraction. In this function we additionally construct the
   198 abstraction environment, and an outer context term (with the focus
   199 abstracted out) for use in rewriting with RWInst.rw *)
   200 fun prep_zipper_match z = 
   201     let 
   202       val t = Z.trm z  
   203       val c = Z.ctxt z
   204       val Ts = Z.C.nty_ctxt c
   205       val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   206       val absterm = mk_foo_match (Z.C.apply c) Ts' t'
   207     in
   208       (t', (FakeTs', Ts', absterm))
   209     end;
   210 
   211 (* Matching and Unification with exception handled *)
   212 fun clean_match thy (a as (pat, t)) =
   213   let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   214   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   215   end handle Pattern.MATCH => NONE;
   216 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   217 fun clean_unify sgn 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 sgn (pat_ty, tgt_ty) (Term.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 sgn [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 = Term.maxidx_of_term conclterm;
   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 = Term.maxidx_of_term asmt;
   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     (Args.parens (Scan.repeat Args.nat))
   562       || (Scan.succeed [0]);
   563 
   564 (* combination method that takes a flag (true indicates that subst
   565 should be done to an assumption, false = apply to the conclusion of
   566 the goal) as well as the theorems to use *)
   567 fun subst_meth src =
   568   Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   569   #> (fn (((asmflag, occL), inthms), ctxt) =>
   570     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   571 
   572 
   573 val setup =
   574   Method.add_method ("subst", subst_meth, "single-step substitution");
   575 
   576 end;