src/Provers/eqsubst.ML
author wenzelm
Fri Feb 10 02:22:16 2006 +0100 (2006-02-10)
changeset 18988 d6e5fa2ba8b8
parent 18833 bead1a4e966b
child 19047 670ce193b618
permissions -rw-r--r--
Args/Attrib syntax: Context.generic;
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
wenzelm@18708
    10
  val setup : theory -> theory
paulson@15481
    11
end;
paulson@15481
    12
wenzelm@18598
    13
structure EqSubst: EQSUBST =
wenzelm@18598
    14
struct
dixon@16004
    15
wenzelm@18598
    16
fun prep_meta_eq ctxt =
wenzelm@18598
    17
  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
wenzelm@18598
    18
  in mk #> map Drule.zero_var_indexes end;
wenzelm@18598
    19
paulson@15481
    20
dixon@15915
    21
  (* a type abriviation for match information *)
wenzelm@16978
    22
  type match =
wenzelm@16978
    23
       ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm@16978
    24
        * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm@16978
    25
       * (string * typ) list (* fake named type abs env *)
wenzelm@16978
    26
       * (string * typ) list (* type abs env *)
wenzelm@16978
    27
       * term (* outer term *)
dixon@15550
    28
wenzelm@16978
    29
  type searchinfo =
wenzelm@18598
    30
       theory
dixon@16004
    31
       * int (* maxidx *)
dixon@16004
    32
       * BasicIsaFTerm.FcTerm (* focusterm to search under *)
dixon@15550
    33
dixon@15538
    34
(* FOR DEBUGGING...
dixon@15538
    35
type trace_subst_errT = int (* subgoal *)
wenzelm@16978
    36
        * thm (* thm with all goals *)
dixon@15538
    37
        * (Thm.cterm list (* certified free var placeholders for vars *)
wenzelm@16978
    38
           * thm)  (* trivial thm of goal concl *)
dixon@15538
    39
            (* possible matches/unifiers *)
wenzelm@16978
    40
        * thm (* rule *)
wenzelm@16978
    41
        * (((indexname * typ) list (* type instantiations *)
wenzelm@16978
    42
              * (indexname * term) list ) (* term instantiations *)
wenzelm@16978
    43
             * (string * typ) list (* Type abs env *)
wenzelm@16978
    44
             * term) (* outer term *);
dixon@15538
    45
dixon@15538
    46
val trace_subst_err = (ref NONE : trace_subst_errT option ref);
dixon@15538
    47
val trace_subst_search = ref false;
dixon@15538
    48
exception trace_subst_exp of trace_subst_errT;
dixon@15538
    49
 *)
dixon@15538
    50
dixon@15814
    51
(* search from top, left to right, then down *)
wenzelm@16978
    52
fun search_tlr_all_f f ft =
paulson@15481
    53
    let
wenzelm@16978
    54
      fun maux ft =
wenzelm@16978
    55
          let val t' = (IsaFTerm.focus_of_fcterm ft)
wenzelm@16978
    56
            (* val _ =
wenzelm@16978
    57
                if !trace_subst_search then
dixon@15538
    58
                  (writeln ("Examining: " ^ (TermLib.string_of_term t'));
dixon@15538
    59
                   TermLib.writeterm t'; ())
dixon@15538
    60
                else (); *)
wenzelm@16978
    61
          in
wenzelm@16978
    62
          (case t' of
wenzelm@16978
    63
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
wenzelm@16978
    64
                       Seq.cons(f ft,
paulson@15481
    65
                                  maux (IsaFTerm.focus_right ft)))
dixon@15929
    66
          | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
dixon@15929
    67
          | leaf => Seq.single (f ft)) end
paulson@15481
    68
    in maux ft end;
paulson@15481
    69
dixon@15814
    70
(* search from top, left to right, then down *)
wenzelm@16978
    71
fun search_tlr_valid_f f ft =
dixon@15814
    72
    let
wenzelm@16978
    73
      fun maux ft =
wenzelm@16978
    74
          let
dixon@15814
    75
            val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
wenzelm@16978
    76
          in
wenzelm@16978
    77
          (case (IsaFTerm.focus_of_fcterm ft) of
wenzelm@16978
    78
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
wenzelm@16978
    79
                       Seq.cons(hereseq,
dixon@15814
    80
                                  maux (IsaFTerm.focus_right ft)))
dixon@15929
    81
          | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
dixon@15929
    82
          | leaf => Seq.single (hereseq))
dixon@15814
    83
          end
dixon@15814
    84
    in maux ft end;
dixon@15814
    85
dixon@15814
    86
(* search all unifications *)
wenzelm@16978
    87
fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
wenzelm@16978
    88
    IsaFTerm.find_fcterm_matches
wenzelm@16978
    89
      search_tlr_all_f
dixon@16004
    90
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
dixon@16004
    91
      ft;
paulson@15481
    92
dixon@15814
    93
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
wenzelm@16978
    94
fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs  =
wenzelm@16978
    95
    IsaFTerm.find_fcterm_matches
wenzelm@16978
    96
      search_tlr_valid_f
dixon@16004
    97
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
dixon@16004
    98
      ft;
dixon@15929
    99
dixon@15814
   100
dixon@15538
   101
(* apply a substitution in the conclusion of the theorem th *)
dixon@15538
   102
(* cfvs are certified free var placeholders for goal params *)
dixon@15538
   103
(* conclthm is a theorem of for just the conclusion *)
dixon@15538
   104
(* m is instantiation/match information *)
dixon@15538
   105
(* rule is the equation for substitution *)
wenzelm@16978
   106
fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
dixon@15538
   107
    (RWInst.rw m rule conclthm)
dixon@15855
   108
      |> IsaND.unfix_frees cfvs
dixon@15915
   109
      |> RWInst.beta_eta_contract
dixon@15538
   110
      |> (fn r => Tactic.rtac r i th);
paulson@15481
   111
paulson@15481
   112
(* substitute within the conclusion of goal i of gth, using a meta
dixon@15538
   113
equation rule. Note that we assume rule has var indicies zero'd *)
wenzelm@16978
   114
fun prep_concl_subst i gth =
wenzelm@16978
   115
    let
paulson@15481
   116
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   117
      val tgt_term = Thm.prop_of th;
paulson@15481
   118
paulson@15481
   119
      val sgn = Thm.sign_of_thm th;
paulson@15481
   120
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   121
      val trivify = Thm.trivial o ctermify;
paulson@15481
   122
paulson@15481
   123
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   124
      val cfvs = rev (map ctermify fvs);
paulson@15481
   125
dixon@15538
   126
      val conclterm = Logic.strip_imp_concl fixedbody;
dixon@15538
   127
      val conclthm = trivify conclterm;
dixon@15538
   128
      val maxidx = Term.maxidx_of_term conclterm;
wenzelm@16978
   129
      val ft = ((IsaFTerm.focus_right
dixon@16004
   130
                 o IsaFTerm.focus_left
wenzelm@16978
   131
                 o IsaFTerm.fcterm_of_term
dixon@16004
   132
                 o Thm.prop_of) conclthm)
paulson@15481
   133
    in
dixon@16004
   134
      ((cfvs, conclthm), (sgn, maxidx, ft))
paulson@15481
   135
    end;
paulson@15481
   136
paulson@15481
   137
(* substitute using an object or meta level equality *)
wenzelm@18598
   138
fun eqsubst_tac' ctxt searchf instepthm i th =
wenzelm@16978
   139
    let
dixon@16004
   140
      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
wenzelm@18598
   141
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@15538
   142
      fun rewrite_with_thm r =
dixon@15538
   143
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
wenzelm@18598
   144
          in searchf searchinfo lhs
wenzelm@18598
   145
             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
wenzelm@18598
   146
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   147
dixon@15538
   148
dixon@16004
   149
(* Tactic.distinct_subgoals_tac -- fails to free type variables *)
dixon@15959
   150
wenzelm@16978
   151
(* custom version of distinct subgoals that works with term and
wenzelm@16978
   152
   type variables. Asssumes th is in beta-eta normal form.
dixon@15959
   153
   Also, does nothing if flexflex contraints are present. *)
dixon@15959
   154
fun distinct_subgoals th =
dixon@15959
   155
    if List.null (Thm.tpairs_of th) then
dixon@15959
   156
      let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
dixon@15959
   157
        val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
dixon@15959
   158
      in
wenzelm@16978
   159
        IsaND.unfix_frees_and_tfrees
dixon@15959
   160
          fixes
wenzelm@16978
   161
          (Drule.implies_intr_list
wenzelm@16978
   162
             (Library.gen_distinct
dixon@15959
   163
                (fn (x, y) => Thm.term_of x = Thm.term_of y)
dixon@15959
   164
                cprems) fixedthconcl)
dixon@15959
   165
      end
dixon@15959
   166
    else th;
dixon@15538
   167
wenzelm@16978
   168
(* General substiuttion of multiple occurances using one of
dixon@15936
   169
   the given theorems*)
wenzelm@16978
   170
exception eqsubst_occL_exp of
wenzelm@16978
   171
          string * (int list) * (thm list) * int * thm;
wenzelm@16978
   172
fun skip_first_occs_search occ srchf sinfo lhs =
wenzelm@16978
   173
    case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
dixon@16004
   174
      IsaPLib.skipmore _ => Seq.empty
dixon@16004
   175
    | IsaPLib.skipseq ss => Seq.flat ss;
dixon@16004
   176
wenzelm@18598
   177
fun eqsubst_tac ctxt occL thms i th =
dixon@15936
   178
    let val nprems = Thm.nprems_of th in
dixon@15936
   179
      if nprems < i then Seq.empty else
wenzelm@16978
   180
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   181
        fun apply_occ occ th =
wenzelm@18598
   182
            thmseq |> Seq.maps
wenzelm@18598
   183
                    (fn r => eqsubst_tac' ctxt (skip_first_occs_search
dixon@15936
   184
                                    occ searchf_tlr_unify_valid) r
dixon@15936
   185
                                 (i + ((Thm.nprems_of th) - nprems))
dixon@15936
   186
                                 th);
wenzelm@16978
   187
        val sortedoccL =
dixon@16004
   188
            Library.sort (Library.rev_order o Library.int_ord) occL;
dixon@15936
   189
      in
dixon@16004
   190
        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
dixon@15936
   191
      end
dixon@15959
   192
    end
dixon@15959
   193
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
dixon@15959
   194
paulson@15481
   195
paulson@15481
   196
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   197
   the first one, then the second etc *)
wenzelm@18598
   198
fun eqsubst_meth ctxt occL inthms =
wenzelm@16978
   199
    Method.METHOD
dixon@15538
   200
      (fn facts =>
wenzelm@18598
   201
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
paulson@15481
   202
dixon@16004
   203
(* apply a substitution inside assumption j, keeps asm in the same place *)
wenzelm@16978
   204
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
wenzelm@16978
   205
    let
dixon@16004
   206
      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
wenzelm@16978
   207
      val preelimrule =
dixon@16004
   208
          (RWInst.rw m rule pth)
dixon@16004
   209
            |> (Seq.hd o Tactic.prune_params_tac)
dixon@16004
   210
            |> Thm.permute_prems 0 ~1 (* put old asm first *)
dixon@16004
   211
            |> IsaND.unfix_frees cfvs (* unfix any global params *)
dixon@16004
   212
            |> RWInst.beta_eta_contract; (* normal form *)
wenzelm@16978
   213
  (*    val elimrule =
dixon@16004
   214
          preelimrule
dixon@16004
   215
            |> Tactic.make_elim (* make into elim rule *)
dixon@16004
   216
            |> Thm.lift_rule (th2, i); (* lift into context *)
dixon@16007
   217
   *)
dixon@16004
   218
    in
dixon@16004
   219
      (* ~j because new asm starts at back, thus we subtract 1 *)
dixon@16007
   220
      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
dixon@16007
   221
      (Tactic.dtac preelimrule i th2)
dixon@16007
   222
wenzelm@16978
   223
      (* (Thm.bicompose
dixon@16004
   224
                 false (* use unification *)
dixon@16004
   225
                 (true, (* elim resolution *)
dixon@16007
   226
                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
dixon@16007
   227
                 i th2) *)
dixon@16004
   228
    end;
paulson@15481
   229
paulson@15481
   230
dixon@15538
   231
(* prepare to substitute within the j'th premise of subgoal i of gth,
dixon@15538
   232
using a meta-level equation. Note that we assume rule has var indicies
dixon@15538
   233
zero'd. Note that we also assume that premt is the j'th premice of
dixon@15538
   234
subgoal i of gth. Note the repetition of work done for each
dixon@15538
   235
assumption, i.e. this can be made more efficient for search over
dixon@15538
   236
multiple assumptions.  *)
wenzelm@16978
   237
fun prep_subst_in_asm i gth j =
wenzelm@16978
   238
    let
paulson@15481
   239
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   240
      val tgt_term = Thm.prop_of th;
paulson@15481
   241
paulson@15481
   242
      val sgn = Thm.sign_of_thm th;
paulson@15481
   243
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   244
      val trivify = Thm.trivial o ctermify;
paulson@15481
   245
paulson@15481
   246
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   247
      val cfvs = rev (map ctermify fvs);
paulson@15481
   248
haftmann@18011
   249
      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
dixon@15538
   250
      val asm_nprems = length (Logic.strip_imp_prems asmt);
dixon@15538
   251
dixon@15538
   252
      val pth = trivify asmt;
dixon@15538
   253
      val maxidx = Term.maxidx_of_term asmt;
dixon@15538
   254
wenzelm@16978
   255
      val ft = ((IsaFTerm.focus_right
wenzelm@16978
   256
                 o IsaFTerm.fcterm_of_term
dixon@16004
   257
                 o Thm.prop_of) pth)
dixon@16004
   258
    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
paulson@15481
   259
dixon@15538
   260
(* prepare subst in every possible assumption *)
wenzelm@16978
   261
fun prep_subst_in_asms i gth =
dixon@16004
   262
    map (prep_subst_in_asm i gth)
wenzelm@16978
   263
        ((rev o IsaPLib.mk_num_list o length)
dixon@16004
   264
           (Logic.prems_of_goal (Thm.prop_of gth) i));
dixon@15538
   265
dixon@15538
   266
dixon@15538
   267
(* substitute in an assumption using an object or meta level equality *)
wenzelm@18598
   268
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
wenzelm@16978
   269
    let
dixon@16004
   270
      val asmpreps = prep_subst_in_asms i th;
wenzelm@18598
   271
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@16004
   272
      fun rewrite_with_thm r =
dixon@16004
   273
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
dixon@16004
   274
            fun occ_search occ [] = Seq.empty
dixon@16004
   275
              | occ_search occ ((asminfo, searchinfo)::moreasms) =
wenzelm@16978
   276
                (case searchf searchinfo occ lhs of
dixon@16004
   277
                   IsaPLib.skipmore i => occ_search i moreasms
wenzelm@16978
   278
                 | IsaPLib.skipseq ss =>
dixon@16004
   279
                   Seq.append (Seq.map (Library.pair asminfo)
wenzelm@16978
   280
                                       (Seq.flat ss),
dixon@16004
   281
                               occ_search 1 moreasms))
dixon@16004
   282
                              (* find later substs also *)
wenzelm@16978
   283
          in
wenzelm@18598
   284
            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
dixon@16004
   285
          end;
wenzelm@18598
   286
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   287
dixon@16004
   288
wenzelm@16978
   289
fun skip_first_asm_occs_search searchf sinfo occ lhs =
dixon@16004
   290
    IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
dixon@16004
   291
wenzelm@18598
   292
fun eqsubst_asm_tac ctxt occL thms i th =
wenzelm@16978
   293
    let val nprems = Thm.nprems_of th
dixon@15538
   294
    in
dixon@16004
   295
      if nprems < i then Seq.empty else
wenzelm@16978
   296
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   297
        fun apply_occ occK th =
wenzelm@18598
   298
            thmseq |> Seq.maps
wenzelm@16978
   299
                    (fn r =>
wenzelm@18598
   300
                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
dixon@16004
   301
                                            searchf_tlr_unify_valid) occK r
dixon@16004
   302
                                         (i + ((Thm.nprems_of th) - nprems))
dixon@16004
   303
                                         th);
wenzelm@16978
   304
        val sortedoccs =
dixon@16004
   305
            Library.sort (Library.rev_order o Library.int_ord) occL
dixon@16004
   306
      in
dixon@16004
   307
        Seq.map distinct_subgoals
dixon@16004
   308
                (Seq.EVERY (map apply_occ sortedoccs) th)
dixon@16004
   309
      end
dixon@16004
   310
    end
dixon@16004
   311
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
paulson@15481
   312
paulson@15481
   313
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   314
   the first one, then the second etc *)
wenzelm@18598
   315
fun eqsubst_asm_meth ctxt occL inthms =
wenzelm@16978
   316
    Method.METHOD
dixon@15538
   317
      (fn facts =>
wenzelm@18598
   318
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
paulson@15481
   319
paulson@15481
   320
(* syntax for options, given "(asm)" will give back true, without
paulson@15481
   321
   gives back false *)
paulson@15481
   322
val options_syntax =
paulson@15481
   323
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
paulson@15481
   324
     (Scan.succeed false);
dixon@15936
   325
dixon@15929
   326
val ith_syntax =
dixon@15936
   327
    (Args.parens (Scan.repeat Args.nat))
dixon@15936
   328
      || (Scan.succeed [0]);
paulson@15481
   329
wenzelm@18598
   330
(* combination method that takes a flag (true indicates that subst
wenzelm@18598
   331
should be done to an assumption, false = apply to the conclusion of
wenzelm@18598
   332
the goal) as well as the theorems to use *)
wenzelm@18598
   333
fun subst_meth src =
wenzelm@18988
   334
  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
wenzelm@18598
   335
  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
wenzelm@18598
   336
    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
paulson@15481
   337
wenzelm@18598
   338
wenzelm@16978
   339
val setup =
wenzelm@18833
   340
  Method.add_method ("subst", subst_meth, "single-step substitution");
paulson@15481
   341
wenzelm@16978
   342
end;