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