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