src/Provers/eqsubst.ML
author dixon
Sun Jun 11 00:28:18 2006 +0200 (2006-06-11)
changeset 19835 81d6dc597559
parent 19473 d87a8838afa4
child 19861 620d90091788
permissions -rw-r--r--
added updated version of IsaPlanner and substitution.
dixon@15538
     1
(*  Title:      Provers/eqsubst.ML
wenzelm@16434
     2
    ID:         $Id$
wenzelm@18598
     3
    Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
paulson@15481
     4
wenzelm@18598
     5
A proof method to perform a substiution using an equation.
wenzelm@18598
     6
*)
dixon@15538
     7
wenzelm@18591
     8
signature EQSUBST =
paulson@15481
     9
sig
wenzelm@18708
    10
  val setup : theory -> theory
paulson@15481
    11
end;
paulson@15481
    12
dixon@19835
    13
structure EqSubst
dixon@19835
    14
(* : EQSUBST *)
dixon@19835
    15
= struct
dixon@16004
    16
dixon@19835
    17
structure Z = Zipper;
dixon@19835
    18
dixon@19835
    19
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
wenzelm@18598
    20
fun prep_meta_eq ctxt =
wenzelm@18598
    21
  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
wenzelm@18598
    22
  in mk #> map Drule.zero_var_indexes end;
wenzelm@18598
    23
paulson@15481
    24
dixon@15915
    25
  (* a type abriviation for match information *)
wenzelm@16978
    26
  type match =
wenzelm@16978
    27
       ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm@16978
    28
        * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm@16978
    29
       * (string * typ) list (* fake named type abs env *)
wenzelm@16978
    30
       * (string * typ) list (* type abs env *)
wenzelm@16978
    31
       * term (* outer term *)
dixon@15550
    32
wenzelm@16978
    33
  type searchinfo =
wenzelm@18598
    34
       theory
dixon@16004
    35
       * int (* maxidx *)
dixon@19835
    36
       * Zipper.T (* focusterm to search under *)
dixon@19835
    37
dixon@19835
    38
dixon@19835
    39
(* skipping non-empty sub-sequences but when we reach the end
dixon@19835
    40
   of the seq, remembering how much we have left to skip. *)
dixon@19835
    41
datatype 'a skipseq = SkipMore of int
dixon@19835
    42
  | SkipSeq of 'a Seq.seq Seq.seq;
dixon@19835
    43
(* given a seqseq, skip the first m non-empty seq's, note deficit *)
dixon@19835
    44
fun skipto_skipseq m s = 
dixon@19835
    45
    let 
dixon@19835
    46
      fun skip_occs n sq = 
dixon@19835
    47
          case Seq.pull sq of 
dixon@19835
    48
            NONE => SkipMore n
dixon@19835
    49
          | SOME (h,t) => 
dixon@19835
    50
            (case Seq.pull h of NONE => skip_occs n t
dixon@19835
    51
             | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
dixon@19835
    52
                         else skip_occs (n - 1) t)
dixon@19835
    53
    in (skip_occs m s) end;
dixon@19835
    54
dixon@19835
    55
(* note: outerterm is the taget with the match replaced by a bound 
dixon@19835
    56
         variable : ie: "P lhs" beocmes "%x. P x" 
dixon@19835
    57
         insts is the types of instantiations of vars in lhs
dixon@19835
    58
         and typinsts is the type instantiations of types in the lhs
dixon@19835
    59
         Note: Final rule is the rule lifted into the ontext of the 
dixon@19835
    60
         taget thm. *)
dixon@19835
    61
fun mk_foo_match mkuptermfunc Ts t = 
dixon@19835
    62
    let 
dixon@19835
    63
      val ty = Term.type_of t
dixon@19835
    64
      val bigtype = (rev (map snd Ts)) ---> ty
dixon@19835
    65
      fun mk_foo 0 t = t
dixon@19835
    66
        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
dixon@19835
    67
      val num_of_bnds = (length Ts)
dixon@19835
    68
      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
dixon@19835
    69
      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
dixon@19835
    70
    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
dixon@19835
    71
dixon@19835
    72
(* T is outer bound vars, n is number of locally bound vars *)
dixon@19835
    73
(* THINK: is order of Ts correct...? or reversed? *)
dixon@19835
    74
fun fakefree_badbounds Ts t = 
dixon@19835
    75
    let val (FakeTs,Ts,newnames) = 
dixon@19835
    76
            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
dixon@19835
    77
                           let val newname = Term.variant usednames n
dixon@19835
    78
                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
dixon@19835
    79
                               (newname,ty)::Ts, 
dixon@19835
    80
                               newname::usednames) end)
dixon@19835
    81
                       ([],[],[])
dixon@19835
    82
                       Ts
dixon@19835
    83
    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
dixon@19835
    84
dixon@19835
    85
(* before matching we need to fake the bound vars that are missing an
dixon@19835
    86
abstraction. In this function we additionally construct the
dixon@19835
    87
abstraction environment, and an outer context term (with the focus
dixon@19835
    88
abstracted out) for use in rewriting with RWInst.rw *)
dixon@19835
    89
fun prep_zipper_match z = 
dixon@19835
    90
    let 
dixon@19835
    91
      val t = Z.trm z  
dixon@19835
    92
      val c = Z.ctxt z
dixon@19835
    93
      val Ts = Z.C.nty_ctxt c
dixon@19835
    94
      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
dixon@19835
    95
      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
dixon@19835
    96
    in
dixon@19835
    97
      (t', (FakeTs', Ts', absterm))
dixon@19835
    98
    end;
dixon@19835
    99
dixon@19835
   100
(* Matching and Unification with exception handled *)
dixon@19835
   101
fun clean_match thy (a as (pat, t)) =
dixon@19835
   102
  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
dixon@19835
   103
  in SOME (Vartab.dest tyenv, Vartab.dest tenv)
dixon@19835
   104
  end handle Pattern.MATCH => NONE;
dixon@19835
   105
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
dixon@19835
   106
fun clean_unify sgn ix (a as (pat, tgt)) =
dixon@19835
   107
    let
dixon@19835
   108
      (* type info will be re-derived, maybe this can be cached
dixon@19835
   109
         for efficiency? *)
dixon@19835
   110
      val pat_ty = Term.type_of pat;
dixon@19835
   111
      val tgt_ty = Term.type_of tgt;
dixon@19835
   112
      (* is it OK to ignore the type instantiation info?
dixon@19835
   113
         or should I be using it? *)
dixon@19835
   114
      val typs_unify =
dixon@19835
   115
          SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
dixon@19835
   116
            handle Type.TUNIFY => NONE;
dixon@19835
   117
    in
dixon@19835
   118
      case typs_unify of
dixon@19835
   119
        SOME (typinsttab, ix2) =>
dixon@19835
   120
        let
dixon@19835
   121
      (* is it right to throw away the flexes?
dixon@19835
   122
         or should I be using them somehow? *)
dixon@19835
   123
          fun mk_insts env =
dixon@19835
   124
            (Vartab.dest (Envir.type_env env),
dixon@19835
   125
             Envir.alist_of env);
dixon@19835
   126
          val initenv = Envir.Envir {asol = Vartab.empty,
dixon@19835
   127
                                     iTs = typinsttab, maxidx = ix2};
dixon@19835
   128
          val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
dixon@19835
   129
	            handle UnequalLengths => Seq.empty
dixon@19835
   130
		               | Term.TERM _ => Seq.empty;
dixon@19835
   131
          fun clean_unify' useq () =
dixon@19835
   132
              (case (Seq.pull useq) of
dixon@19835
   133
                 NONE => NONE
dixon@19835
   134
               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
dixon@19835
   135
	      handle UnequalLengths => NONE
dixon@19835
   136
                   | Term.TERM _ => NONE;
dixon@19835
   137
        in
dixon@19835
   138
          (Seq.make (clean_unify' useq))
dixon@19835
   139
        end
dixon@19835
   140
      | NONE => Seq.empty
dixon@19835
   141
    end;
dixon@19835
   142
dixon@19835
   143
(* Matching and Unification for zippers *)
dixon@19835
   144
(* Note: Ts is a modified version of the original names of the outer
dixon@19835
   145
bound variables. New names have been introduced to make sure they are
dixon@19835
   146
unique w.r.t all names in the term and each other. usednames' is
dixon@19835
   147
oldnames + new names. *)
dixon@19835
   148
fun clean_match_z thy pat z = 
dixon@19835
   149
    let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
dixon@19835
   150
      case clean_match thy (pat, t) of 
dixon@19835
   151
        NONE => NONE 
dixon@19835
   152
      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
dixon@19835
   153
(* ix = max var index *)
dixon@19835
   154
fun clean_unify_z sgn ix pat z = 
dixon@19835
   155
    let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
dixon@19835
   156
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
dixon@19835
   157
            (clean_unify sgn ix (t, pat)) end;
dixon@19835
   158
dixon@15550
   159
dixon@15538
   160
(* FOR DEBUGGING...
dixon@15538
   161
type trace_subst_errT = int (* subgoal *)
wenzelm@16978
   162
        * thm (* thm with all goals *)
dixon@15538
   163
        * (Thm.cterm list (* certified free var placeholders for vars *)
wenzelm@16978
   164
           * thm)  (* trivial thm of goal concl *)
dixon@15538
   165
            (* possible matches/unifiers *)
wenzelm@16978
   166
        * thm (* rule *)
wenzelm@16978
   167
        * (((indexname * typ) list (* type instantiations *)
wenzelm@16978
   168
              * (indexname * term) list ) (* term instantiations *)
wenzelm@16978
   169
             * (string * typ) list (* Type abs env *)
wenzelm@16978
   170
             * term) (* outer term *);
dixon@15538
   171
dixon@15538
   172
val trace_subst_err = (ref NONE : trace_subst_errT option ref);
dixon@15538
   173
val trace_subst_search = ref false;
dixon@15538
   174
exception trace_subst_exp of trace_subst_errT;
dixon@19835
   175
*)
dixon@19835
   176
dixon@19835
   177
dixon@19835
   178
fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
dixon@19835
   179
  | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
dixon@19835
   180
  | bot_left_leaf_of x = x;
dixon@15538
   181
dixon@19835
   182
fun valid_match_start z =
dixon@19835
   183
    (case bot_left_leaf_of (Z.trm z) of 
dixon@19835
   184
       Const _ => true
dixon@19835
   185
     | Free _ => true
dixon@19835
   186
     | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
dixon@19835
   187
     | _ => false); (* avoid vars - always suceeds uninterestingly. *)
dixon@19835
   188
                      
dixon@15814
   189
(* search from top, left to right, then down *)
dixon@19835
   190
val search_tlr_all = ZipperSearch.all_td_lr;
paulson@15481
   191
dixon@15814
   192
(* search from top, left to right, then down *)
dixon@19835
   193
fun search_tlr_valid validf =
dixon@19835
   194
    let 
dixon@19835
   195
      fun sf_valid_td_lr z = 
dixon@19835
   196
          let val here = if validf z then [Z.Here z] else [] in
dixon@19835
   197
            case Z.trm z 
dixon@19835
   198
             of _ $ _ => here @ [Z.LookIn (Z.move_down_left z),
dixon@19835
   199
                                 Z.LookIn (Z.move_down_right z)]
dixon@19835
   200
              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
dixon@19835
   201
              | _ => here
dixon@19835
   202
          end;
dixon@19835
   203
    in Z.lzy_search sf_valid_td_lr end;
dixon@15814
   204
dixon@15814
   205
(* search all unifications *)
dixon@19835
   206
fun searchf_tlr_unify_all (sgn, maxidx, z) lhs =
dixon@19835
   207
    Seq.map (clean_unify_z sgn maxidx lhs) 
dixon@19835
   208
            (Z.limit_apply search_tlr_all z);
paulson@15481
   209
dixon@15814
   210
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
dixon@19835
   211
fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs  =
dixon@19835
   212
    Seq.map (clean_unify_z sgn maxidx lhs) 
dixon@19835
   213
            (Z.limit_apply (search_tlr_valid valid_match_start) z);
dixon@15929
   214
dixon@15814
   215
dixon@15538
   216
(* apply a substitution in the conclusion of the theorem th *)
dixon@15538
   217
(* cfvs are certified free var placeholders for goal params *)
dixon@15538
   218
(* conclthm is a theorem of for just the conclusion *)
dixon@15538
   219
(* m is instantiation/match information *)
dixon@15538
   220
(* rule is the equation for substitution *)
wenzelm@16978
   221
fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
dixon@15538
   222
    (RWInst.rw m rule conclthm)
dixon@15855
   223
      |> IsaND.unfix_frees cfvs
dixon@15915
   224
      |> RWInst.beta_eta_contract
dixon@15538
   225
      |> (fn r => Tactic.rtac r i th);
paulson@15481
   226
paulson@15481
   227
(* substitute within the conclusion of goal i of gth, using a meta
dixon@15538
   228
equation rule. Note that we assume rule has var indicies zero'd *)
wenzelm@16978
   229
fun prep_concl_subst i gth =
wenzelm@16978
   230
    let
paulson@15481
   231
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   232
      val tgt_term = Thm.prop_of th;
paulson@15481
   233
paulson@15481
   234
      val sgn = Thm.sign_of_thm th;
paulson@15481
   235
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   236
      val trivify = Thm.trivial o ctermify;
paulson@15481
   237
paulson@15481
   238
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   239
      val cfvs = rev (map ctermify fvs);
paulson@15481
   240
dixon@15538
   241
      val conclterm = Logic.strip_imp_concl fixedbody;
dixon@15538
   242
      val conclthm = trivify conclterm;
dixon@15538
   243
      val maxidx = Term.maxidx_of_term conclterm;
dixon@19835
   244
      val ft = ((Z.move_down_right (* ==> *)
dixon@19835
   245
                 o Z.move_down_left (* Trueprop *)
dixon@19835
   246
                 o Z.mktop
dixon@16004
   247
                 o Thm.prop_of) conclthm)
paulson@15481
   248
    in
dixon@16004
   249
      ((cfvs, conclthm), (sgn, maxidx, ft))
paulson@15481
   250
    end;
paulson@15481
   251
paulson@15481
   252
(* substitute using an object or meta level equality *)
wenzelm@18598
   253
fun eqsubst_tac' ctxt searchf instepthm i th =
wenzelm@16978
   254
    let
dixon@16004
   255
      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
wenzelm@18598
   256
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@15538
   257
      fun rewrite_with_thm r =
dixon@15538
   258
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
wenzelm@18598
   259
          in searchf searchinfo lhs
wenzelm@18598
   260
             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
wenzelm@18598
   261
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   262
dixon@15538
   263
wenzelm@19047
   264
(* distinct subgoals *)
dixon@15959
   265
fun distinct_subgoals th =
wenzelm@19047
   266
  the_default th (SINGLE distinct_subgoals_tac th);
dixon@15538
   267
wenzelm@19047
   268
(* General substitution of multiple occurances using one of
dixon@15936
   269
   the given theorems*)
dixon@19835
   270
dixon@19835
   271
wenzelm@16978
   272
exception eqsubst_occL_exp of
wenzelm@16978
   273
          string * (int list) * (thm list) * int * thm;
wenzelm@16978
   274
fun skip_first_occs_search occ srchf sinfo lhs =
dixon@19835
   275
    case (skipto_skipseq occ (srchf sinfo lhs)) of
dixon@19835
   276
      SkipMore _ => Seq.empty
dixon@19835
   277
    | SkipSeq ss => Seq.flat ss;
dixon@16004
   278
wenzelm@18598
   279
fun eqsubst_tac ctxt occL thms i th =
dixon@15936
   280
    let val nprems = Thm.nprems_of th in
dixon@15936
   281
      if nprems < i then Seq.empty else
wenzelm@16978
   282
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   283
        fun apply_occ occ th =
wenzelm@18598
   284
            thmseq |> Seq.maps
dixon@19835
   285
                    (fn r => eqsubst_tac' 
dixon@19835
   286
                               ctxt 
dixon@19835
   287
                               (skip_first_occs_search
dixon@19835
   288
                                  occ searchf_tlr_unify_valid) r
dixon@15936
   289
                                 (i + ((Thm.nprems_of th) - nprems))
dixon@15936
   290
                                 th);
wenzelm@16978
   291
        val sortedoccL =
dixon@16004
   292
            Library.sort (Library.rev_order o Library.int_ord) occL;
dixon@15936
   293
      in
dixon@16004
   294
        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
dixon@15936
   295
      end
dixon@15959
   296
    end
dixon@15959
   297
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
dixon@15959
   298
paulson@15481
   299
paulson@15481
   300
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   301
   the first one, then the second etc *)
wenzelm@18598
   302
fun eqsubst_meth ctxt occL inthms =
wenzelm@16978
   303
    Method.METHOD
dixon@15538
   304
      (fn facts =>
wenzelm@18598
   305
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
paulson@15481
   306
dixon@16004
   307
(* apply a substitution inside assumption j, keeps asm in the same place *)
wenzelm@16978
   308
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
wenzelm@16978
   309
    let
dixon@16004
   310
      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
wenzelm@16978
   311
      val preelimrule =
dixon@16004
   312
          (RWInst.rw m rule pth)
dixon@16004
   313
            |> (Seq.hd o Tactic.prune_params_tac)
dixon@16004
   314
            |> Thm.permute_prems 0 ~1 (* put old asm first *)
dixon@16004
   315
            |> IsaND.unfix_frees cfvs (* unfix any global params *)
dixon@16004
   316
            |> RWInst.beta_eta_contract; (* normal form *)
wenzelm@16978
   317
  (*    val elimrule =
dixon@16004
   318
          preelimrule
dixon@16004
   319
            |> Tactic.make_elim (* make into elim rule *)
dixon@16004
   320
            |> Thm.lift_rule (th2, i); (* lift into context *)
dixon@16007
   321
   *)
dixon@16004
   322
    in
dixon@16004
   323
      (* ~j because new asm starts at back, thus we subtract 1 *)
dixon@16007
   324
      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
dixon@16007
   325
      (Tactic.dtac preelimrule i th2)
dixon@16007
   326
wenzelm@16978
   327
      (* (Thm.bicompose
dixon@16004
   328
                 false (* use unification *)
dixon@16004
   329
                 (true, (* elim resolution *)
dixon@16007
   330
                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
dixon@16007
   331
                 i th2) *)
dixon@16004
   332
    end;
paulson@15481
   333
paulson@15481
   334
dixon@15538
   335
(* prepare to substitute within the j'th premise of subgoal i of gth,
dixon@15538
   336
using a meta-level equation. Note that we assume rule has var indicies
dixon@15538
   337
zero'd. Note that we also assume that premt is the j'th premice of
dixon@15538
   338
subgoal i of gth. Note the repetition of work done for each
dixon@15538
   339
assumption, i.e. this can be made more efficient for search over
dixon@15538
   340
multiple assumptions.  *)
wenzelm@16978
   341
fun prep_subst_in_asm i gth j =
wenzelm@16978
   342
    let
paulson@15481
   343
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   344
      val tgt_term = Thm.prop_of th;
paulson@15481
   345
paulson@15481
   346
      val sgn = Thm.sign_of_thm th;
paulson@15481
   347
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   348
      val trivify = Thm.trivial o ctermify;
paulson@15481
   349
paulson@15481
   350
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   351
      val cfvs = rev (map ctermify fvs);
paulson@15481
   352
haftmann@18011
   353
      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
dixon@15538
   354
      val asm_nprems = length (Logic.strip_imp_prems asmt);
dixon@15538
   355
dixon@15538
   356
      val pth = trivify asmt;
dixon@15538
   357
      val maxidx = Term.maxidx_of_term asmt;
dixon@15538
   358
dixon@19835
   359
      val ft = ((Z.move_down_right (* trueprop *)
dixon@19835
   360
                 o Z.mktop
dixon@16004
   361
                 o Thm.prop_of) pth)
dixon@16004
   362
    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
paulson@15481
   363
dixon@15538
   364
(* prepare subst in every possible assumption *)
wenzelm@16978
   365
fun prep_subst_in_asms i gth =
dixon@16004
   366
    map (prep_subst_in_asm i gth)
dixon@19835
   367
        ((fn l => Library.upto (1, length l))
dixon@16004
   368
           (Logic.prems_of_goal (Thm.prop_of gth) i));
dixon@15538
   369
dixon@15538
   370
dixon@15538
   371
(* substitute in an assumption using an object or meta level equality *)
wenzelm@18598
   372
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
wenzelm@16978
   373
    let
dixon@16004
   374
      val asmpreps = prep_subst_in_asms i th;
wenzelm@18598
   375
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@16004
   376
      fun rewrite_with_thm r =
dixon@16004
   377
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
dixon@16004
   378
            fun occ_search occ [] = Seq.empty
dixon@16004
   379
              | occ_search occ ((asminfo, searchinfo)::moreasms) =
wenzelm@16978
   380
                (case searchf searchinfo occ lhs of
dixon@19835
   381
                   SkipMore i => occ_search i moreasms
dixon@19835
   382
                 | SkipSeq ss =>
dixon@16004
   383
                   Seq.append (Seq.map (Library.pair asminfo)
wenzelm@16978
   384
                                       (Seq.flat ss),
dixon@16004
   385
                               occ_search 1 moreasms))
dixon@16004
   386
                              (* find later substs also *)
wenzelm@16978
   387
          in
wenzelm@18598
   388
            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
dixon@16004
   389
          end;
wenzelm@18598
   390
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   391
dixon@16004
   392
wenzelm@16978
   393
fun skip_first_asm_occs_search searchf sinfo occ lhs =
dixon@19835
   394
    skipto_skipseq occ (searchf sinfo lhs);
dixon@16004
   395
wenzelm@18598
   396
fun eqsubst_asm_tac ctxt occL thms i th =
wenzelm@16978
   397
    let val nprems = Thm.nprems_of th
dixon@15538
   398
    in
dixon@16004
   399
      if nprems < i then Seq.empty else
wenzelm@16978
   400
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   401
        fun apply_occ occK th =
wenzelm@18598
   402
            thmseq |> Seq.maps
wenzelm@16978
   403
                    (fn r =>
wenzelm@18598
   404
                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
dixon@16004
   405
                                            searchf_tlr_unify_valid) occK r
dixon@16004
   406
                                         (i + ((Thm.nprems_of th) - nprems))
dixon@16004
   407
                                         th);
wenzelm@16978
   408
        val sortedoccs =
dixon@16004
   409
            Library.sort (Library.rev_order o Library.int_ord) occL
dixon@16004
   410
      in
dixon@16004
   411
        Seq.map distinct_subgoals
dixon@16004
   412
                (Seq.EVERY (map apply_occ sortedoccs) th)
dixon@16004
   413
      end
dixon@16004
   414
    end
dixon@16004
   415
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
paulson@15481
   416
paulson@15481
   417
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   418
   the first one, then the second etc *)
wenzelm@18598
   419
fun eqsubst_asm_meth ctxt occL inthms =
wenzelm@16978
   420
    Method.METHOD
dixon@15538
   421
      (fn facts =>
wenzelm@18598
   422
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
paulson@15481
   423
paulson@15481
   424
(* syntax for options, given "(asm)" will give back true, without
paulson@15481
   425
   gives back false *)
paulson@15481
   426
val options_syntax =
paulson@15481
   427
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
paulson@15481
   428
     (Scan.succeed false);
dixon@15936
   429
dixon@15929
   430
val ith_syntax =
dixon@15936
   431
    (Args.parens (Scan.repeat Args.nat))
dixon@15936
   432
      || (Scan.succeed [0]);
paulson@15481
   433
wenzelm@18598
   434
(* combination method that takes a flag (true indicates that subst
wenzelm@18598
   435
should be done to an assumption, false = apply to the conclusion of
wenzelm@18598
   436
the goal) as well as the theorems to use *)
wenzelm@18598
   437
fun subst_meth src =
wenzelm@18988
   438
  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
wenzelm@18598
   439
  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
wenzelm@18598
   440
    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
paulson@15481
   441
wenzelm@18598
   442
wenzelm@16978
   443
val setup =
wenzelm@18833
   444
  Method.add_method ("subst", subst_meth, "single-step substitution");
paulson@15481
   445
wenzelm@16978
   446
end;