src/Tools/eqsubst.ML
author wenzelm
Thu May 30 17:26:01 2013 +0200 (2013-05-30)
changeset 52246 54c0d4128b30
parent 52242 2d634bfa1bbf
child 52732 b4da1f2ec73f
permissions -rw-r--r--
tuned signature;
wenzelm@30160
     1
(*  Title:      Tools/eqsubst.ML
wenzelm@29269
     2
    Author:     Lucas Dixon, University of Edinburgh
paulson@15481
     3
wenzelm@52235
     4
Perform a substitution using an equation.
wenzelm@18598
     5
*)
dixon@15538
     6
wenzelm@18591
     7
signature EQSUBST =
paulson@15481
     8
sig
dixon@19871
     9
  type match =
wenzelm@52234
    10
    ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm@52234
    11
      * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm@52234
    12
    * (string * typ) list (* fake named type abs env *)
wenzelm@52234
    13
    * (string * typ) list (* type abs env *)
wenzelm@52234
    14
    * term (* outer term *)
dixon@19871
    15
dixon@19871
    16
  type searchinfo =
wenzelm@52234
    17
    theory
wenzelm@52234
    18
    * int (* maxidx *)
wenzelm@52234
    19
    * Zipper.T (* focusterm to search under *)
dixon@19871
    20
wenzelm@49339
    21
  datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
dixon@19871
    22
wenzelm@52234
    23
  val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq
wenzelm@52234
    24
  val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
wenzelm@52234
    25
  val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq
dixon@19871
    26
wenzelm@49339
    27
  (* tactics *)
wenzelm@52234
    28
  val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
wenzelm@52234
    29
  val eqsubst_asm_tac': Proof.context ->
wenzelm@52234
    30
    (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
wenzelm@52234
    31
  val eqsubst_tac: Proof.context ->
wenzelm@52234
    32
    int list -> (* list of occurences to rewrite, use [0] for any *)
wenzelm@52234
    33
    thm list -> int -> tactic
wenzelm@52234
    34
  val eqsubst_tac': Proof.context ->
wenzelm@52234
    35
    (searchinfo -> term -> match Seq.seq) (* search function *)
wenzelm@52234
    36
    -> thm (* equation theorem to rewrite with *)
wenzelm@52234
    37
    -> int (* subgoal number in goal theorem *)
wenzelm@52234
    38
    -> thm (* goal theorem *)
wenzelm@52234
    39
    -> thm Seq.seq (* rewritten goal theorem *)
dixon@19871
    40
wenzelm@49339
    41
  (* search for substitutions *)
wenzelm@52234
    42
  val valid_match_start: Zipper.T -> bool
wenzelm@52234
    43
  val search_lr_all: Zipper.T -> Zipper.T Seq.seq
wenzelm@52234
    44
  val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
wenzelm@52234
    45
  val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
wenzelm@52234
    46
  val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
wenzelm@52234
    47
  val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
dixon@19871
    48
wenzelm@49339
    49
  val setup : theory -> theory
paulson@15481
    50
end;
paulson@15481
    51
wenzelm@41164
    52
structure EqSubst: EQSUBST =
wenzelm@41164
    53
struct
dixon@19835
    54
dixon@19835
    55
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
wenzelm@18598
    56
fun prep_meta_eq ctxt =
wenzelm@51717
    57
  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
wenzelm@18598
    58
wenzelm@52246
    59
(* make free vars into schematic vars with index zero *)
wenzelm@52246
    60
fun unfix_frees frees =
wenzelm@52246
    61
   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
wenzelm@52246
    62
paulson@15481
    63
wenzelm@52234
    64
type match =
wenzelm@52235
    65
  ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm@52235
    66
   * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm@52235
    67
  * (string * typ) list (* fake named type abs env *)
wenzelm@52235
    68
  * (string * typ) list (* type abs env *)
wenzelm@52235
    69
  * term; (* outer term *)
dixon@15550
    70
wenzelm@52234
    71
type searchinfo =
wenzelm@52235
    72
  theory
wenzelm@52235
    73
  * int (* maxidx *)
wenzelm@52235
    74
  * Zipper.T; (* focusterm to search under *)
dixon@19835
    75
dixon@19835
    76
dixon@19835
    77
(* skipping non-empty sub-sequences but when we reach the end
dixon@19835
    78
   of the seq, remembering how much we have left to skip. *)
wenzelm@52234
    79
datatype 'a skipseq =
wenzelm@52234
    80
  SkipMore of int |
wenzelm@52234
    81
  SkipSeq of 'a Seq.seq Seq.seq;
wenzelm@52234
    82
dixon@19835
    83
(* given a seqseq, skip the first m non-empty seq's, note deficit *)
wenzelm@49339
    84
fun skipto_skipseq m s =
wenzelm@52234
    85
  let
wenzelm@52234
    86
    fun skip_occs n sq =
wenzelm@52234
    87
      (case Seq.pull sq of
wenzelm@52234
    88
        NONE => SkipMore n
wenzelm@52237
    89
      | SOME (h, t) =>
wenzelm@52234
    90
        (case Seq.pull h of
wenzelm@52234
    91
          NONE => skip_occs n t
wenzelm@52234
    92
        | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
wenzelm@52234
    93
  in skip_occs m s end;
dixon@19835
    94
wenzelm@49339
    95
(* note: outerterm is the taget with the match replaced by a bound
wenzelm@52234
    96
   variable : ie: "P lhs" beocmes "%x. P x"
wenzelm@52234
    97
   insts is the types of instantiations of vars in lhs
wenzelm@52234
    98
   and typinsts is the type instantiations of types in the lhs
wenzelm@52234
    99
   Note: Final rule is the rule lifted into the ontext of the
wenzelm@52234
   100
   taget thm. *)
wenzelm@49339
   101
fun mk_foo_match mkuptermfunc Ts t =
wenzelm@52234
   102
  let
wenzelm@52234
   103
    val ty = Term.type_of t
wenzelm@52235
   104
    val bigtype = rev (map snd Ts) ---> ty
wenzelm@52234
   105
    fun mk_foo 0 t = t
wenzelm@52234
   106
      | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
wenzelm@52235
   107
    val num_of_bnds = length Ts
wenzelm@52234
   108
    (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
wenzelm@52234
   109
    val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
wenzelm@52234
   110
  in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
dixon@19835
   111
dixon@19835
   112
(* T is outer bound vars, n is number of locally bound vars *)
dixon@19835
   113
(* THINK: is order of Ts correct...? or reversed? *)
wenzelm@49339
   114
fun mk_fake_bound_name n = ":b_" ^ n;
wenzelm@49339
   115
fun fakefree_badbounds Ts t =
wenzelm@52234
   116
  let val (FakeTs, Ts, newnames) =
wenzelm@52242
   117
    fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
wenzelm@52234
   118
      let
wenzelm@52234
   119
        val newname = singleton (Name.variant_list usednames) n
wenzelm@52234
   120
      in
wenzelm@52234
   121
        ((mk_fake_bound_name newname, ty) :: FakeTs,
wenzelm@52234
   122
          (newname, ty) :: Ts,
wenzelm@52234
   123
          newname :: usednames)
wenzelm@52242
   124
      end) Ts ([], [], [])
wenzelm@52234
   125
  in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
dixon@19835
   126
dixon@19835
   127
(* before matching we need to fake the bound vars that are missing an
wenzelm@52235
   128
   abstraction. In this function we additionally construct the
wenzelm@52235
   129
   abstraction environment, and an outer context term (with the focus
wenzelm@52240
   130
   abstracted out) for use in rewriting with RW_Inst.rw *)
wenzelm@49339
   131
fun prep_zipper_match z =
wenzelm@52234
   132
  let
wenzelm@52234
   133
    val t = Zipper.trm z
wenzelm@52234
   134
    val c = Zipper.ctxt z
wenzelm@52234
   135
    val Ts = Zipper.C.nty_ctxt c
wenzelm@52234
   136
    val (FakeTs', Ts', t') = fakefree_badbounds Ts t
wenzelm@52234
   137
    val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
wenzelm@52234
   138
  in
wenzelm@52234
   139
    (t', (FakeTs', Ts', absterm))
wenzelm@52234
   140
  end;
dixon@19835
   141
wenzelm@49339
   142
(* Unification with exception handled *)
dixon@19835
   143
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
wenzelm@52235
   144
fun clean_unify thy ix (a as (pat, tgt)) =
wenzelm@52234
   145
  let
wenzelm@52234
   146
    (* type info will be re-derived, maybe this can be cached
wenzelm@52234
   147
       for efficiency? *)
wenzelm@52234
   148
    val pat_ty = Term.type_of pat;
wenzelm@52234
   149
    val tgt_ty = Term.type_of tgt;
wenzelm@52235
   150
    (* FIXME is it OK to ignore the type instantiation info?
wenzelm@52234
   151
       or should I be using it? *)
wenzelm@52234
   152
    val typs_unify =
wenzelm@52235
   153
      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
wenzelm@52234
   154
        handle Type.TUNIFY => NONE;
wenzelm@52234
   155
  in
wenzelm@52234
   156
    (case typs_unify of
wenzelm@52234
   157
      SOME (typinsttab, ix2) =>
dixon@19835
   158
        let
wenzelm@52234
   159
          (* FIXME is it right to throw away the flexes?
wenzelm@52234
   160
             or should I be using them somehow? *)
dixon@19835
   161
          fun mk_insts env =
dixon@19835
   162
            (Vartab.dest (Envir.type_env env),
wenzelm@32032
   163
             Vartab.dest (Envir.term_env env));
wenzelm@32032
   164
          val initenv =
wenzelm@32032
   165
            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
wenzelm@52235
   166
          val useq = Unify.smash_unifiers thy [a] initenv
wenzelm@52234
   167
            handle ListPair.UnequalLengths => Seq.empty
wenzelm@52234
   168
              | Term.TERM _ => Seq.empty;
dixon@19835
   169
          fun clean_unify' useq () =
wenzelm@52234
   170
            (case (Seq.pull useq) of
wenzelm@52234
   171
               NONE => NONE
wenzelm@52234
   172
             | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
wenzelm@52234
   173
            handle ListPair.UnequalLengths => NONE
wenzelm@52234
   174
              | Term.TERM _ => NONE;
dixon@19835
   175
        in
dixon@19835
   176
          (Seq.make (clean_unify' useq))
dixon@19835
   177
        end
wenzelm@52234
   178
    | NONE => Seq.empty)
wenzelm@52234
   179
  end;
dixon@19835
   180
wenzelm@49339
   181
(* Unification for zippers *)
dixon@19835
   182
(* Note: Ts is a modified version of the original names of the outer
wenzelm@52235
   183
   bound variables. New names have been introduced to make sure they are
wenzelm@52235
   184
   unique w.r.t all names in the term and each other. usednames' is
wenzelm@52235
   185
   oldnames + new names. *)
wenzelm@52235
   186
fun clean_unify_z thy maxidx pat z =
wenzelm@52235
   187
  let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
wenzelm@49339
   188
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
wenzelm@52235
   189
      (clean_unify thy maxidx (t, pat))
wenzelm@52234
   190
  end;
dixon@19835
   191
dixon@15550
   192
wenzelm@52234
   193
fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
wenzelm@52234
   194
  | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
dixon@19835
   195
  | bot_left_leaf_of x = x;
dixon@15538
   196
dixon@19975
   197
(* Avoid considering replacing terms which have a var at the head as
dixon@19975
   198
   they always succeed trivially, and uninterestingly. *)
dixon@19835
   199
fun valid_match_start z =
wenzelm@52234
   200
  (case bot_left_leaf_of (Zipper.trm z) of
wenzelm@52234
   201
    Var _ => false
wenzelm@52234
   202
  | _ => true);
dixon@19975
   203
dixon@15814
   204
(* search from top, left to right, then down *)
dixon@19871
   205
val search_lr_all = ZipperSearch.all_bl_ur;
paulson@15481
   206
dixon@15814
   207
(* search from top, left to right, then down *)
dixon@19871
   208
fun search_lr_valid validf =
wenzelm@52234
   209
  let
wenzelm@52234
   210
    fun sf_valid_td_lr z =
wenzelm@52234
   211
      let val here = if validf z then [Zipper.Here z] else [] in
wenzelm@52234
   212
        (case Zipper.trm z of
wenzelm@52234
   213
          _ $ _ =>
wenzelm@52234
   214
            [Zipper.LookIn (Zipper.move_down_left z)] @ here @
wenzelm@52234
   215
            [Zipper.LookIn (Zipper.move_down_right z)]
wenzelm@52234
   216
        | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
wenzelm@52234
   217
        | _ => here)
wenzelm@52234
   218
      end;
wenzelm@52234
   219
  in Zipper.lzy_search sf_valid_td_lr end;
dixon@15814
   220
narboux@23064
   221
(* search from bottom to top, left to right *)
narboux@23064
   222
fun search_bt_valid validf =
wenzelm@52234
   223
  let
wenzelm@52234
   224
    fun sf_valid_td_lr z =
wenzelm@52234
   225
      let val here = if validf z then [Zipper.Here z] else [] in
wenzelm@52234
   226
        (case Zipper.trm z of
wenzelm@52234
   227
          _ $ _ =>
wenzelm@52234
   228
            [Zipper.LookIn (Zipper.move_down_left z),
wenzelm@52234
   229
             Zipper.LookIn (Zipper.move_down_right z)] @ here
wenzelm@52234
   230
        | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
wenzelm@52234
   231
        | _ => here)
wenzelm@52234
   232
      end;
wenzelm@52234
   233
  in Zipper.lzy_search sf_valid_td_lr end;
narboux@23064
   234
wenzelm@52235
   235
fun searchf_unify_gen f (thy, maxidx, z) lhs =
wenzelm@52235
   236
  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
narboux@23064
   237
dixon@15814
   238
(* search all unifications *)
wenzelm@52234
   239
val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
paulson@15481
   240
dixon@15814
   241
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
wenzelm@52234
   242
val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
dixon@15929
   243
wenzelm@52234
   244
val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
dixon@15814
   245
wenzelm@52236
   246
(* apply a substitution in the conclusion of the theorem *)
dixon@15538
   247
(* cfvs are certified free var placeholders for goal params *)
dixon@15538
   248
(* conclthm is a theorem of for just the conclusion *)
dixon@15538
   249
(* m is instantiation/match information *)
dixon@15538
   250
(* rule is the equation for substitution *)
wenzelm@52236
   251
fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
wenzelm@52240
   252
  RW_Inst.rw ctxt m rule conclthm
wenzelm@52246
   253
  |> unfix_frees cfvs
wenzelm@52239
   254
  |> Conv.fconv_rule Drule.beta_eta_conversion
wenzelm@52236
   255
  |> (fn r => Tactic.rtac r i st);
paulson@15481
   256
paulson@15481
   257
(* substitute within the conclusion of goal i of gth, using a meta
dixon@15538
   258
equation rule. Note that we assume rule has var indicies zero'd *)
wenzelm@49340
   259
fun prep_concl_subst ctxt i gth =
wenzelm@52234
   260
  let
wenzelm@52234
   261
    val th = Thm.incr_indexes 1 gth;
wenzelm@52234
   262
    val tgt_term = Thm.prop_of th;
paulson@15481
   263
wenzelm@52235
   264
    val thy = Thm.theory_of_thm th;
wenzelm@52235
   265
    val cert = Thm.cterm_of thy;
paulson@15481
   266
wenzelm@52234
   267
    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
wenzelm@52235
   268
    val cfvs = rev (map cert fvs);
paulson@15481
   269
wenzelm@52234
   270
    val conclterm = Logic.strip_imp_concl fixedbody;
wenzelm@52235
   271
    val conclthm = Thm.trivial (cert conclterm);
wenzelm@52234
   272
    val maxidx = Thm.maxidx_of th;
wenzelm@52234
   273
    val ft =
wenzelm@52234
   274
      (Zipper.move_down_right (* ==> *)
wenzelm@52234
   275
       o Zipper.move_down_left (* Trueprop *)
wenzelm@52234
   276
       o Zipper.mktop
wenzelm@52234
   277
       o Thm.prop_of) conclthm
wenzelm@52234
   278
  in
wenzelm@52235
   279
    ((cfvs, conclthm), (thy, maxidx, ft))
wenzelm@52234
   280
  end;
paulson@15481
   281
paulson@15481
   282
(* substitute using an object or meta level equality *)
wenzelm@52236
   283
fun eqsubst_tac' ctxt searchf instepthm i st =
wenzelm@52234
   284
  let
wenzelm@52236
   285
    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
wenzelm@52234
   286
    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
wenzelm@52234
   287
    fun rewrite_with_thm r =
wenzelm@52234
   288
      let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
wenzelm@52234
   289
        searchf searchinfo lhs
wenzelm@52236
   290
        |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
wenzelm@52234
   291
      end;
wenzelm@52234
   292
  in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   293
dixon@15538
   294
wenzelm@19047
   295
(* General substitution of multiple occurances using one of
wenzelm@52235
   296
   the given theorems *)
dixon@19835
   297
wenzelm@16978
   298
fun skip_first_occs_search occ srchf sinfo lhs =
wenzelm@52236
   299
  (case skipto_skipseq occ (srchf sinfo lhs) of
wenzelm@52234
   300
    SkipMore _ => Seq.empty
wenzelm@52234
   301
  | SkipSeq ss => Seq.flat ss);
dixon@16004
   302
wenzelm@52238
   303
(* The "occs" argument is a list of integers indicating which occurence
dixon@22727
   304
w.r.t. the search order, to rewrite. Backtracking will also find later
dixon@22727
   305
occurences, but all earlier ones are skipped. Thus you can use [0] to
dixon@22727
   306
just find all rewrites. *)
dixon@22727
   307
wenzelm@52238
   308
fun eqsubst_tac ctxt occs thms i st =
wenzelm@52236
   309
  let val nprems = Thm.nprems_of st in
wenzelm@52234
   310
    if nprems < i then Seq.empty else
wenzelm@52234
   311
    let
wenzelm@52236
   312
      val thmseq = Seq.of_list thms;
wenzelm@52236
   313
      fun apply_occ occ st =
wenzelm@52234
   314
        thmseq |> Seq.maps (fn r =>
wenzelm@52234
   315
          eqsubst_tac' ctxt
wenzelm@52234
   316
            (skip_first_occs_search occ searchf_lr_unify_valid) r
wenzelm@52236
   317
            (i + (Thm.nprems_of st - nprems)) st);
wenzelm@52238
   318
      val sorted_occs = Library.sort (rev_order o int_ord) occs;
wenzelm@52234
   319
    in
wenzelm@52238
   320
      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
wenzelm@52234
   321
    end
wenzelm@52234
   322
  end;
dixon@15959
   323
paulson@15481
   324
dixon@16004
   325
(* apply a substitution inside assumption j, keeps asm in the same place *)
wenzelm@52236
   326
fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
wenzelm@52234
   327
  let
wenzelm@52236
   328
    val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
wenzelm@52234
   329
    val preelimrule =
wenzelm@52240
   330
      RW_Inst.rw ctxt m rule pth
wenzelm@52234
   331
      |> (Seq.hd o prune_params_tac)
wenzelm@52234
   332
      |> Thm.permute_prems 0 ~1 (* put old asm first *)
wenzelm@52246
   333
      |> unfix_frees cfvs (* unfix any global params *)
wenzelm@52239
   334
      |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
wenzelm@52234
   335
  in
wenzelm@52234
   336
    (* ~j because new asm starts at back, thus we subtract 1 *)
wenzelm@52235
   337
    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
wenzelm@52236
   338
      (Tactic.dtac preelimrule i st2)
wenzelm@52234
   339
  end;
paulson@15481
   340
paulson@15481
   341
dixon@15538
   342
(* prepare to substitute within the j'th premise of subgoal i of gth,
dixon@15538
   343
using a meta-level equation. Note that we assume rule has var indicies
dixon@15538
   344
zero'd. Note that we also assume that premt is the j'th premice of
dixon@15538
   345
subgoal i of gth. Note the repetition of work done for each
dixon@15538
   346
assumption, i.e. this can be made more efficient for search over
dixon@15538
   347
multiple assumptions.  *)
wenzelm@49340
   348
fun prep_subst_in_asm ctxt i gth j =
wenzelm@52234
   349
  let
wenzelm@52234
   350
    val th = Thm.incr_indexes 1 gth;
wenzelm@52234
   351
    val tgt_term = Thm.prop_of th;
paulson@15481
   352
wenzelm@52235
   353
    val thy = Thm.theory_of_thm th;
wenzelm@52235
   354
    val cert = Thm.cterm_of thy;
paulson@15481
   355
wenzelm@52234
   356
    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
wenzelm@52235
   357
    val cfvs = rev (map cert fvs);
paulson@15481
   358
wenzelm@52234
   359
    val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
wenzelm@52234
   360
    val asm_nprems = length (Logic.strip_imp_prems asmt);
wenzelm@52234
   361
wenzelm@52235
   362
    val pth = Thm.trivial (cert asmt);
wenzelm@52234
   363
    val maxidx = Thm.maxidx_of th;
dixon@15538
   364
wenzelm@52234
   365
    val ft =
wenzelm@52234
   366
      (Zipper.move_down_right (* trueprop *)
wenzelm@52234
   367
         o Zipper.mktop
wenzelm@52234
   368
         o Thm.prop_of) pth
wenzelm@52235
   369
  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
paulson@15481
   370
dixon@15538
   371
(* prepare subst in every possible assumption *)
wenzelm@49340
   372
fun prep_subst_in_asms ctxt i gth =
wenzelm@52234
   373
  map (prep_subst_in_asm ctxt i gth)
wenzelm@52234
   374
    ((fn l => Library.upto (1, length l))
wenzelm@52234
   375
      (Logic.prems_of_goal (Thm.prop_of gth) i));
dixon@15538
   376
dixon@15538
   377
dixon@15538
   378
(* substitute in an assumption using an object or meta level equality *)
wenzelm@52236
   379
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st =
wenzelm@52234
   380
  let
wenzelm@52236
   381
    val asmpreps = prep_subst_in_asms ctxt i st;
wenzelm@52234
   382
    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
wenzelm@52234
   383
    fun rewrite_with_thm r =
wenzelm@52234
   384
      let
wenzelm@52234
   385
        val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
wenzelm@52234
   386
        fun occ_search occ [] = Seq.empty
wenzelm@52234
   387
          | occ_search occ ((asminfo, searchinfo)::moreasms) =
wenzelm@52234
   388
              (case searchf searchinfo occ lhs of
wenzelm@52234
   389
                SkipMore i => occ_search i moreasms
wenzelm@52234
   390
              | SkipSeq ss =>
wenzelm@52234
   391
                  Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
wenzelm@52234
   392
                    (occ_search 1 moreasms)) (* find later substs also *)
wenzelm@52234
   393
      in
wenzelm@52236
   394
        occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i st r)
wenzelm@52234
   395
      end;
wenzelm@52234
   396
  in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   397
dixon@16004
   398
wenzelm@16978
   399
fun skip_first_asm_occs_search searchf sinfo occ lhs =
wenzelm@52234
   400
  skipto_skipseq occ (searchf sinfo lhs);
dixon@16004
   401
wenzelm@52238
   402
fun eqsubst_asm_tac ctxt occs thms i st =
wenzelm@52236
   403
  let val nprems = Thm.nprems_of st in
wenzelm@52234
   404
    if nprems < i then Seq.empty
wenzelm@52234
   405
    else
wenzelm@52234
   406
      let
wenzelm@52234
   407
        val thmseq = Seq.of_list thms;
wenzelm@52238
   408
        fun apply_occ occ st =
wenzelm@52234
   409
          thmseq |> Seq.maps (fn r =>
wenzelm@52234
   410
            eqsubst_asm_tac' ctxt
wenzelm@52238
   411
              (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
wenzelm@52236
   412
              (i + (Thm.nprems_of st - nprems)) st);
wenzelm@52238
   413
        val sorted_occs = Library.sort (rev_order o int_ord) occs;
dixon@16004
   414
      in
wenzelm@52238
   415
        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
dixon@16004
   416
      end
wenzelm@52234
   417
  end;
paulson@15481
   418
wenzelm@18598
   419
(* combination method that takes a flag (true indicates that subst
wenzelm@31301
   420
   should be done to an assumption, false = apply to the conclusion of
wenzelm@31301
   421
   the goal) as well as the theorems to use *)
wenzelm@16978
   422
val setup =
wenzelm@31301
   423
  Method.setup @{binding subst}
wenzelm@44095
   424
    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
wenzelm@44095
   425
        Attrib.thms >>
wenzelm@52238
   426
      (fn ((asm, occs), inthms) => fn ctxt =>
wenzelm@52238
   427
        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
wenzelm@31301
   428
    "single-step substitution";
paulson@15481
   429
wenzelm@16978
   430
end;