src/Tools/eqsubst.ML
author wenzelm
Thu May 30 14:37:06 2013 +0200 (2013-05-30)
changeset 52236 fb82b42eb498
parent 52235 6aff6b8bec13
child 52237 ab3ba550cbe7
permissions -rw-r--r--
tuned -- prefer terminology of tactic / goal state;
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
paulson@15481
    59
wenzelm@52234
    60
type match =
wenzelm@52235
    61
  ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm@52235
    62
   * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm@52235
    63
  * (string * typ) list (* fake named type abs env *)
wenzelm@52235
    64
  * (string * typ) list (* type abs env *)
wenzelm@52235
    65
  * term; (* outer term *)
dixon@15550
    66
wenzelm@52234
    67
type searchinfo =
wenzelm@52235
    68
  theory
wenzelm@52235
    69
  * int (* maxidx *)
wenzelm@52235
    70
  * Zipper.T; (* focusterm to search under *)
dixon@19835
    71
dixon@19835
    72
dixon@19835
    73
(* skipping non-empty sub-sequences but when we reach the end
dixon@19835
    74
   of the seq, remembering how much we have left to skip. *)
wenzelm@52234
    75
datatype 'a skipseq =
wenzelm@52234
    76
  SkipMore of int |
wenzelm@52234
    77
  SkipSeq of 'a Seq.seq Seq.seq;
wenzelm@52234
    78
dixon@19835
    79
(* given a seqseq, skip the first m non-empty seq's, note deficit *)
wenzelm@49339
    80
fun skipto_skipseq m s =
wenzelm@52234
    81
  let
wenzelm@52234
    82
    fun skip_occs n sq =
wenzelm@52234
    83
      (case Seq.pull sq of
wenzelm@52234
    84
        NONE => SkipMore n
wenzelm@52234
    85
      | SOME (h,t) =>
wenzelm@52234
    86
        (case Seq.pull h of
wenzelm@52234
    87
          NONE => skip_occs n t
wenzelm@52234
    88
        | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
wenzelm@52234
    89
  in skip_occs m s end;
dixon@19835
    90
wenzelm@49339
    91
(* note: outerterm is the taget with the match replaced by a bound
wenzelm@52234
    92
   variable : ie: "P lhs" beocmes "%x. P x"
wenzelm@52234
    93
   insts is the types of instantiations of vars in lhs
wenzelm@52234
    94
   and typinsts is the type instantiations of types in the lhs
wenzelm@52234
    95
   Note: Final rule is the rule lifted into the ontext of the
wenzelm@52234
    96
   taget thm. *)
wenzelm@49339
    97
fun mk_foo_match mkuptermfunc Ts t =
wenzelm@52234
    98
  let
wenzelm@52234
    99
    val ty = Term.type_of t
wenzelm@52235
   100
    val bigtype = rev (map snd Ts) ---> ty
wenzelm@52234
   101
    fun mk_foo 0 t = t
wenzelm@52234
   102
      | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
wenzelm@52235
   103
    val num_of_bnds = length Ts
wenzelm@52234
   104
    (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
wenzelm@52234
   105
    val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
wenzelm@52234
   106
  in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
dixon@19835
   107
dixon@19835
   108
(* T is outer bound vars, n is number of locally bound vars *)
dixon@19835
   109
(* THINK: is order of Ts correct...? or reversed? *)
wenzelm@49339
   110
fun mk_fake_bound_name n = ":b_" ^ n;
wenzelm@49339
   111
fun fakefree_badbounds Ts t =
wenzelm@52234
   112
  let val (FakeTs, Ts, newnames) =
wenzelm@52234
   113
    List.foldr (fn ((n, ty), (FakeTs, Ts, usednames)) =>
wenzelm@52234
   114
      let
wenzelm@52234
   115
        val newname = singleton (Name.variant_list usednames) n
wenzelm@52234
   116
      in
wenzelm@52234
   117
        ((mk_fake_bound_name newname, ty) :: FakeTs,
wenzelm@52234
   118
          (newname, ty) :: Ts,
wenzelm@52234
   119
          newname :: usednames)
wenzelm@52234
   120
      end) ([], [], []) Ts
wenzelm@52234
   121
  in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
dixon@19835
   122
dixon@19835
   123
(* before matching we need to fake the bound vars that are missing an
wenzelm@52235
   124
   abstraction. In this function we additionally construct the
wenzelm@52235
   125
   abstraction environment, and an outer context term (with the focus
wenzelm@52235
   126
   abstracted out) for use in rewriting with RWInst.rw *)
wenzelm@49339
   127
fun prep_zipper_match z =
wenzelm@52234
   128
  let
wenzelm@52234
   129
    val t = Zipper.trm z
wenzelm@52234
   130
    val c = Zipper.ctxt z
wenzelm@52234
   131
    val Ts = Zipper.C.nty_ctxt c
wenzelm@52234
   132
    val (FakeTs', Ts', t') = fakefree_badbounds Ts t
wenzelm@52234
   133
    val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
wenzelm@52234
   134
  in
wenzelm@52234
   135
    (t', (FakeTs', Ts', absterm))
wenzelm@52234
   136
  end;
dixon@19835
   137
wenzelm@49339
   138
(* Unification with exception handled *)
dixon@19835
   139
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
wenzelm@52235
   140
fun clean_unify thy ix (a as (pat, tgt)) =
wenzelm@52234
   141
  let
wenzelm@52234
   142
    (* type info will be re-derived, maybe this can be cached
wenzelm@52234
   143
       for efficiency? *)
wenzelm@52234
   144
    val pat_ty = Term.type_of pat;
wenzelm@52234
   145
    val tgt_ty = Term.type_of tgt;
wenzelm@52235
   146
    (* FIXME is it OK to ignore the type instantiation info?
wenzelm@52234
   147
       or should I be using it? *)
wenzelm@52234
   148
    val typs_unify =
wenzelm@52235
   149
      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
wenzelm@52234
   150
        handle Type.TUNIFY => NONE;
wenzelm@52234
   151
  in
wenzelm@52234
   152
    (case typs_unify of
wenzelm@52234
   153
      SOME (typinsttab, ix2) =>
dixon@19835
   154
        let
wenzelm@52234
   155
          (* FIXME is it right to throw away the flexes?
wenzelm@52234
   156
             or should I be using them somehow? *)
dixon@19835
   157
          fun mk_insts env =
dixon@19835
   158
            (Vartab.dest (Envir.type_env env),
wenzelm@32032
   159
             Vartab.dest (Envir.term_env env));
wenzelm@32032
   160
          val initenv =
wenzelm@32032
   161
            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
wenzelm@52235
   162
          val useq = Unify.smash_unifiers thy [a] initenv
wenzelm@52234
   163
            handle ListPair.UnequalLengths => Seq.empty
wenzelm@52234
   164
              | Term.TERM _ => Seq.empty;
dixon@19835
   165
          fun clean_unify' useq () =
wenzelm@52234
   166
            (case (Seq.pull useq) of
wenzelm@52234
   167
               NONE => NONE
wenzelm@52234
   168
             | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
wenzelm@52234
   169
            handle ListPair.UnequalLengths => NONE
wenzelm@52234
   170
              | Term.TERM _ => NONE;
dixon@19835
   171
        in
dixon@19835
   172
          (Seq.make (clean_unify' useq))
dixon@19835
   173
        end
wenzelm@52234
   174
    | NONE => Seq.empty)
wenzelm@52234
   175
  end;
dixon@19835
   176
wenzelm@49339
   177
(* Unification for zippers *)
dixon@19835
   178
(* Note: Ts is a modified version of the original names of the outer
wenzelm@52235
   179
   bound variables. New names have been introduced to make sure they are
wenzelm@52235
   180
   unique w.r.t all names in the term and each other. usednames' is
wenzelm@52235
   181
   oldnames + new names. *)
wenzelm@52235
   182
fun clean_unify_z thy maxidx pat z =
wenzelm@52235
   183
  let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
wenzelm@49339
   184
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
wenzelm@52235
   185
      (clean_unify thy maxidx (t, pat))
wenzelm@52234
   186
  end;
dixon@19835
   187
dixon@15550
   188
wenzelm@52234
   189
fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
wenzelm@52234
   190
  | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
dixon@19835
   191
  | bot_left_leaf_of x = x;
dixon@15538
   192
dixon@19975
   193
(* Avoid considering replacing terms which have a var at the head as
dixon@19975
   194
   they always succeed trivially, and uninterestingly. *)
dixon@19835
   195
fun valid_match_start z =
wenzelm@52234
   196
  (case bot_left_leaf_of (Zipper.trm z) of
wenzelm@52234
   197
    Var _ => false
wenzelm@52234
   198
  | _ => true);
dixon@19975
   199
dixon@15814
   200
(* search from top, left to right, then down *)
dixon@19871
   201
val search_lr_all = ZipperSearch.all_bl_ur;
paulson@15481
   202
dixon@15814
   203
(* search from top, left to right, then down *)
dixon@19871
   204
fun search_lr_valid validf =
wenzelm@52234
   205
  let
wenzelm@52234
   206
    fun sf_valid_td_lr z =
wenzelm@52234
   207
      let val here = if validf z then [Zipper.Here z] else [] in
wenzelm@52234
   208
        (case Zipper.trm z of
wenzelm@52234
   209
          _ $ _ =>
wenzelm@52234
   210
            [Zipper.LookIn (Zipper.move_down_left z)] @ here @
wenzelm@52234
   211
            [Zipper.LookIn (Zipper.move_down_right z)]
wenzelm@52234
   212
        | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
wenzelm@52234
   213
        | _ => here)
wenzelm@52234
   214
      end;
wenzelm@52234
   215
  in Zipper.lzy_search sf_valid_td_lr end;
dixon@15814
   216
narboux@23064
   217
(* search from bottom to top, left to right *)
narboux@23064
   218
fun search_bt_valid validf =
wenzelm@52234
   219
  let
wenzelm@52234
   220
    fun sf_valid_td_lr z =
wenzelm@52234
   221
      let val here = if validf z then [Zipper.Here z] else [] in
wenzelm@52234
   222
        (case Zipper.trm z of
wenzelm@52234
   223
          _ $ _ =>
wenzelm@52234
   224
            [Zipper.LookIn (Zipper.move_down_left z),
wenzelm@52234
   225
             Zipper.LookIn (Zipper.move_down_right z)] @ here
wenzelm@52234
   226
        | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
wenzelm@52234
   227
        | _ => here)
wenzelm@52234
   228
      end;
wenzelm@52234
   229
  in Zipper.lzy_search sf_valid_td_lr end;
narboux@23064
   230
wenzelm@52235
   231
fun searchf_unify_gen f (thy, maxidx, z) lhs =
wenzelm@52235
   232
  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
narboux@23064
   233
dixon@15814
   234
(* search all unifications *)
wenzelm@52234
   235
val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
paulson@15481
   236
dixon@15814
   237
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
wenzelm@52234
   238
val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
dixon@15929
   239
wenzelm@52234
   240
val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
dixon@15814
   241
wenzelm@52236
   242
(* apply a substitution in the conclusion of the theorem *)
dixon@15538
   243
(* cfvs are certified free var placeholders for goal params *)
dixon@15538
   244
(* conclthm is a theorem of for just the conclusion *)
dixon@15538
   245
(* m is instantiation/match information *)
dixon@15538
   246
(* rule is the equation for substitution *)
wenzelm@52236
   247
fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
wenzelm@52234
   248
  RWInst.rw ctxt m rule conclthm
wenzelm@52234
   249
  |> IsaND.unfix_frees cfvs
wenzelm@52234
   250
  |> RWInst.beta_eta_contract
wenzelm@52236
   251
  |> (fn r => Tactic.rtac r i st);
paulson@15481
   252
paulson@15481
   253
(* substitute within the conclusion of goal i of gth, using a meta
dixon@15538
   254
equation rule. Note that we assume rule has var indicies zero'd *)
wenzelm@49340
   255
fun prep_concl_subst ctxt i gth =
wenzelm@52234
   256
  let
wenzelm@52234
   257
    val th = Thm.incr_indexes 1 gth;
wenzelm@52234
   258
    val tgt_term = Thm.prop_of th;
paulson@15481
   259
wenzelm@52235
   260
    val thy = Thm.theory_of_thm th;
wenzelm@52235
   261
    val cert = Thm.cterm_of thy;
paulson@15481
   262
wenzelm@52234
   263
    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
wenzelm@52235
   264
    val cfvs = rev (map cert fvs);
paulson@15481
   265
wenzelm@52234
   266
    val conclterm = Logic.strip_imp_concl fixedbody;
wenzelm@52235
   267
    val conclthm = Thm.trivial (cert conclterm);
wenzelm@52234
   268
    val maxidx = Thm.maxidx_of th;
wenzelm@52234
   269
    val ft =
wenzelm@52234
   270
      (Zipper.move_down_right (* ==> *)
wenzelm@52234
   271
       o Zipper.move_down_left (* Trueprop *)
wenzelm@52234
   272
       o Zipper.mktop
wenzelm@52234
   273
       o Thm.prop_of) conclthm
wenzelm@52234
   274
  in
wenzelm@52235
   275
    ((cfvs, conclthm), (thy, maxidx, ft))
wenzelm@52234
   276
  end;
paulson@15481
   277
paulson@15481
   278
(* substitute using an object or meta level equality *)
wenzelm@52236
   279
fun eqsubst_tac' ctxt searchf instepthm i st =
wenzelm@52234
   280
  let
wenzelm@52236
   281
    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
wenzelm@52234
   282
    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
wenzelm@52234
   283
    fun rewrite_with_thm r =
wenzelm@52234
   284
      let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
wenzelm@52234
   285
        searchf searchinfo lhs
wenzelm@52236
   286
        |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
wenzelm@52234
   287
      end;
wenzelm@52234
   288
  in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   289
dixon@15538
   290
wenzelm@19047
   291
(* General substitution of multiple occurances using one of
wenzelm@52235
   292
   the given theorems *)
dixon@19835
   293
wenzelm@16978
   294
fun skip_first_occs_search occ srchf sinfo lhs =
wenzelm@52236
   295
  (case skipto_skipseq occ (srchf sinfo lhs) of
wenzelm@52234
   296
    SkipMore _ => Seq.empty
wenzelm@52234
   297
  | SkipSeq ss => Seq.flat ss);
dixon@16004
   298
dixon@22727
   299
(* The occL is a list of integers indicating which occurence
dixon@22727
   300
w.r.t. the search order, to rewrite. Backtracking will also find later
dixon@22727
   301
occurences, but all earlier ones are skipped. Thus you can use [0] to
dixon@22727
   302
just find all rewrites. *)
dixon@22727
   303
wenzelm@52236
   304
fun eqsubst_tac ctxt occL thms i st =
wenzelm@52236
   305
  let val nprems = Thm.nprems_of st in
wenzelm@52234
   306
    if nprems < i then Seq.empty else
wenzelm@52234
   307
    let
wenzelm@52236
   308
      val thmseq = Seq.of_list thms;
wenzelm@52236
   309
      fun apply_occ occ st =
wenzelm@52234
   310
        thmseq |> Seq.maps (fn r =>
wenzelm@52234
   311
          eqsubst_tac' ctxt
wenzelm@52234
   312
            (skip_first_occs_search occ searchf_lr_unify_valid) r
wenzelm@52236
   313
            (i + (Thm.nprems_of st - nprems)) st);
wenzelm@52234
   314
      val sortedoccL = Library.sort (rev_order o int_ord) occL;
wenzelm@52234
   315
    in
wenzelm@52236
   316
      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccL) st)
wenzelm@52234
   317
    end
wenzelm@52234
   318
  end;
dixon@15959
   319
paulson@15481
   320
paulson@15481
   321
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   322
   the first one, then the second etc *)
wenzelm@52234
   323
fun eqsubst_meth ctxt occL inthms = SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
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@52234
   330
      RWInst.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@52234
   333
      |> IsaND.unfix_frees cfvs (* unfix any global params *)
wenzelm@52234
   334
      |> RWInst.beta_eta_contract; (* 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@52236
   402
fun eqsubst_asm_tac ctxt occL 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@52236
   408
        fun apply_occ occK st =
wenzelm@52234
   409
          thmseq |> Seq.maps (fn r =>
wenzelm@52234
   410
            eqsubst_asm_tac' ctxt
wenzelm@52234
   411
              (skip_first_asm_occs_search searchf_lr_unify_valid) occK r
wenzelm@52236
   412
              (i + (Thm.nprems_of st - nprems)) st);
wenzelm@52234
   413
        val sortedoccs = Library.sort (rev_order o int_ord) occL;
dixon@16004
   414
      in
wenzelm@52236
   415
        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccs) st)
dixon@16004
   416
      end
wenzelm@52234
   417
  end;
paulson@15481
   418
paulson@15481
   419
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   420
   the first one, then the second etc *)
wenzelm@18598
   421
fun eqsubst_asm_meth ctxt occL inthms =
wenzelm@52234
   422
  SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
paulson@15481
   423
wenzelm@18598
   424
(* combination method that takes a flag (true indicates that subst
wenzelm@31301
   425
   should be done to an assumption, false = apply to the conclusion of
wenzelm@31301
   426
   the goal) as well as the theorems to use *)
wenzelm@16978
   427
val setup =
wenzelm@31301
   428
  Method.setup @{binding subst}
wenzelm@44095
   429
    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
wenzelm@44095
   430
        Attrib.thms >>
wenzelm@44095
   431
      (fn ((asm, occL), inthms) => fn ctxt =>
wenzelm@44095
   432
        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
wenzelm@31301
   433
    "single-step substitution";
paulson@15481
   434
wenzelm@16978
   435
end;