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