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