src/Provers/eqsubst.ML
author wenzelm
Wed Apr 26 22:38:05 2006 +0200 (2006-04-26)
changeset 19473 d87a8838afa4
parent 19047 670ce193b618
child 19835 81d6dc597559
permissions -rw-r--r--
tuned;
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@19473
    64
                       Seq.cons (f ft) (maux (IsaFTerm.focus_right ft)))
wenzelm@19473
    65
          | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft))
dixon@15929
    66
          | leaf => Seq.single (f ft)) end
paulson@15481
    67
    in maux ft end;
paulson@15481
    68
dixon@15814
    69
(* search from top, left to right, then down *)
wenzelm@16978
    70
fun search_tlr_valid_f f ft =
dixon@15814
    71
    let
wenzelm@16978
    72
      fun maux ft =
wenzelm@16978
    73
          let
dixon@15814
    74
            val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
wenzelm@16978
    75
          in
wenzelm@16978
    76
          (case (IsaFTerm.focus_of_fcterm ft) of
wenzelm@16978
    77
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
wenzelm@19473
    78
                       Seq.cons hereseq (maux (IsaFTerm.focus_right ft)))
wenzelm@19473
    79
          | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft))
wenzelm@19473
    80
          | leaf => Seq.single hereseq)
dixon@15814
    81
          end
dixon@15814
    82
    in maux ft end;
dixon@15814
    83
dixon@15814
    84
(* search all unifications *)
wenzelm@16978
    85
fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
wenzelm@16978
    86
    IsaFTerm.find_fcterm_matches
wenzelm@16978
    87
      search_tlr_all_f
dixon@16004
    88
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
dixon@16004
    89
      ft;
paulson@15481
    90
dixon@15814
    91
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
wenzelm@16978
    92
fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs  =
wenzelm@16978
    93
    IsaFTerm.find_fcterm_matches
wenzelm@16978
    94
      search_tlr_valid_f
dixon@16004
    95
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
dixon@16004
    96
      ft;
dixon@15929
    97
dixon@15814
    98
dixon@15538
    99
(* apply a substitution in the conclusion of the theorem th *)
dixon@15538
   100
(* cfvs are certified free var placeholders for goal params *)
dixon@15538
   101
(* conclthm is a theorem of for just the conclusion *)
dixon@15538
   102
(* m is instantiation/match information *)
dixon@15538
   103
(* rule is the equation for substitution *)
wenzelm@16978
   104
fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
dixon@15538
   105
    (RWInst.rw m rule conclthm)
dixon@15855
   106
      |> IsaND.unfix_frees cfvs
dixon@15915
   107
      |> RWInst.beta_eta_contract
dixon@15538
   108
      |> (fn r => Tactic.rtac r i th);
paulson@15481
   109
paulson@15481
   110
(* substitute within the conclusion of goal i of gth, using a meta
dixon@15538
   111
equation rule. Note that we assume rule has var indicies zero'd *)
wenzelm@16978
   112
fun prep_concl_subst i gth =
wenzelm@16978
   113
    let
paulson@15481
   114
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   115
      val tgt_term = Thm.prop_of th;
paulson@15481
   116
paulson@15481
   117
      val sgn = Thm.sign_of_thm th;
paulson@15481
   118
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   119
      val trivify = Thm.trivial o ctermify;
paulson@15481
   120
paulson@15481
   121
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   122
      val cfvs = rev (map ctermify fvs);
paulson@15481
   123
dixon@15538
   124
      val conclterm = Logic.strip_imp_concl fixedbody;
dixon@15538
   125
      val conclthm = trivify conclterm;
dixon@15538
   126
      val maxidx = Term.maxidx_of_term conclterm;
wenzelm@16978
   127
      val ft = ((IsaFTerm.focus_right
dixon@16004
   128
                 o IsaFTerm.focus_left
wenzelm@16978
   129
                 o IsaFTerm.fcterm_of_term
dixon@16004
   130
                 o Thm.prop_of) conclthm)
paulson@15481
   131
    in
dixon@16004
   132
      ((cfvs, conclthm), (sgn, maxidx, ft))
paulson@15481
   133
    end;
paulson@15481
   134
paulson@15481
   135
(* substitute using an object or meta level equality *)
wenzelm@18598
   136
fun eqsubst_tac' ctxt searchf instepthm i th =
wenzelm@16978
   137
    let
dixon@16004
   138
      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
wenzelm@18598
   139
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@15538
   140
      fun rewrite_with_thm r =
dixon@15538
   141
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
wenzelm@18598
   142
          in searchf searchinfo lhs
wenzelm@18598
   143
             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
wenzelm@18598
   144
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   145
dixon@15538
   146
wenzelm@19047
   147
(* distinct subgoals *)
dixon@15959
   148
fun distinct_subgoals th =
wenzelm@19047
   149
  the_default th (SINGLE distinct_subgoals_tac th);
dixon@15538
   150
wenzelm@19047
   151
(* General substitution of multiple occurances using one of
dixon@15936
   152
   the given theorems*)
wenzelm@16978
   153
exception eqsubst_occL_exp of
wenzelm@16978
   154
          string * (int list) * (thm list) * int * thm;
wenzelm@16978
   155
fun skip_first_occs_search occ srchf sinfo lhs =
wenzelm@16978
   156
    case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
dixon@16004
   157
      IsaPLib.skipmore _ => Seq.empty
dixon@16004
   158
    | IsaPLib.skipseq ss => Seq.flat ss;
dixon@16004
   159
wenzelm@18598
   160
fun eqsubst_tac ctxt occL thms i th =
dixon@15936
   161
    let val nprems = Thm.nprems_of th in
dixon@15936
   162
      if nprems < i then Seq.empty else
wenzelm@16978
   163
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   164
        fun apply_occ occ th =
wenzelm@18598
   165
            thmseq |> Seq.maps
wenzelm@18598
   166
                    (fn r => eqsubst_tac' ctxt (skip_first_occs_search
dixon@15936
   167
                                    occ searchf_tlr_unify_valid) r
dixon@15936
   168
                                 (i + ((Thm.nprems_of th) - nprems))
dixon@15936
   169
                                 th);
wenzelm@16978
   170
        val sortedoccL =
dixon@16004
   171
            Library.sort (Library.rev_order o Library.int_ord) occL;
dixon@15936
   172
      in
dixon@16004
   173
        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
dixon@15936
   174
      end
dixon@15959
   175
    end
dixon@15959
   176
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
dixon@15959
   177
paulson@15481
   178
paulson@15481
   179
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   180
   the first one, then the second etc *)
wenzelm@18598
   181
fun eqsubst_meth ctxt occL inthms =
wenzelm@16978
   182
    Method.METHOD
dixon@15538
   183
      (fn facts =>
wenzelm@18598
   184
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
paulson@15481
   185
dixon@16004
   186
(* apply a substitution inside assumption j, keeps asm in the same place *)
wenzelm@16978
   187
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
wenzelm@16978
   188
    let
dixon@16004
   189
      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
wenzelm@16978
   190
      val preelimrule =
dixon@16004
   191
          (RWInst.rw m rule pth)
dixon@16004
   192
            |> (Seq.hd o Tactic.prune_params_tac)
dixon@16004
   193
            |> Thm.permute_prems 0 ~1 (* put old asm first *)
dixon@16004
   194
            |> IsaND.unfix_frees cfvs (* unfix any global params *)
dixon@16004
   195
            |> RWInst.beta_eta_contract; (* normal form *)
wenzelm@16978
   196
  (*    val elimrule =
dixon@16004
   197
          preelimrule
dixon@16004
   198
            |> Tactic.make_elim (* make into elim rule *)
dixon@16004
   199
            |> Thm.lift_rule (th2, i); (* lift into context *)
dixon@16007
   200
   *)
dixon@16004
   201
    in
dixon@16004
   202
      (* ~j because new asm starts at back, thus we subtract 1 *)
dixon@16007
   203
      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
dixon@16007
   204
      (Tactic.dtac preelimrule i th2)
dixon@16007
   205
wenzelm@16978
   206
      (* (Thm.bicompose
dixon@16004
   207
                 false (* use unification *)
dixon@16004
   208
                 (true, (* elim resolution *)
dixon@16007
   209
                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
dixon@16007
   210
                 i th2) *)
dixon@16004
   211
    end;
paulson@15481
   212
paulson@15481
   213
dixon@15538
   214
(* prepare to substitute within the j'th premise of subgoal i of gth,
dixon@15538
   215
using a meta-level equation. Note that we assume rule has var indicies
dixon@15538
   216
zero'd. Note that we also assume that premt is the j'th premice of
dixon@15538
   217
subgoal i of gth. Note the repetition of work done for each
dixon@15538
   218
assumption, i.e. this can be made more efficient for search over
dixon@15538
   219
multiple assumptions.  *)
wenzelm@16978
   220
fun prep_subst_in_asm i gth j =
wenzelm@16978
   221
    let
paulson@15481
   222
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   223
      val tgt_term = Thm.prop_of th;
paulson@15481
   224
paulson@15481
   225
      val sgn = Thm.sign_of_thm th;
paulson@15481
   226
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   227
      val trivify = Thm.trivial o ctermify;
paulson@15481
   228
paulson@15481
   229
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   230
      val cfvs = rev (map ctermify fvs);
paulson@15481
   231
haftmann@18011
   232
      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
dixon@15538
   233
      val asm_nprems = length (Logic.strip_imp_prems asmt);
dixon@15538
   234
dixon@15538
   235
      val pth = trivify asmt;
dixon@15538
   236
      val maxidx = Term.maxidx_of_term asmt;
dixon@15538
   237
wenzelm@16978
   238
      val ft = ((IsaFTerm.focus_right
wenzelm@16978
   239
                 o IsaFTerm.fcterm_of_term
dixon@16004
   240
                 o Thm.prop_of) pth)
dixon@16004
   241
    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
paulson@15481
   242
dixon@15538
   243
(* prepare subst in every possible assumption *)
wenzelm@16978
   244
fun prep_subst_in_asms i gth =
dixon@16004
   245
    map (prep_subst_in_asm i gth)
wenzelm@16978
   246
        ((rev o IsaPLib.mk_num_list o length)
dixon@16004
   247
           (Logic.prems_of_goal (Thm.prop_of gth) i));
dixon@15538
   248
dixon@15538
   249
dixon@15538
   250
(* substitute in an assumption using an object or meta level equality *)
wenzelm@18598
   251
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
wenzelm@16978
   252
    let
dixon@16004
   253
      val asmpreps = prep_subst_in_asms i th;
wenzelm@18598
   254
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
dixon@16004
   255
      fun rewrite_with_thm r =
dixon@16004
   256
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
dixon@16004
   257
            fun occ_search occ [] = Seq.empty
dixon@16004
   258
              | occ_search occ ((asminfo, searchinfo)::moreasms) =
wenzelm@16978
   259
                (case searchf searchinfo occ lhs of
dixon@16004
   260
                   IsaPLib.skipmore i => occ_search i moreasms
wenzelm@16978
   261
                 | IsaPLib.skipseq ss =>
dixon@16004
   262
                   Seq.append (Seq.map (Library.pair asminfo)
wenzelm@16978
   263
                                       (Seq.flat ss),
dixon@16004
   264
                               occ_search 1 moreasms))
dixon@16004
   265
                              (* find later substs also *)
wenzelm@16978
   266
          in
wenzelm@18598
   267
            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
dixon@16004
   268
          end;
wenzelm@18598
   269
    in stepthms |> Seq.maps rewrite_with_thm end;
dixon@15538
   270
dixon@16004
   271
wenzelm@16978
   272
fun skip_first_asm_occs_search searchf sinfo occ lhs =
dixon@16004
   273
    IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
dixon@16004
   274
wenzelm@18598
   275
fun eqsubst_asm_tac ctxt occL thms i th =
wenzelm@16978
   276
    let val nprems = Thm.nprems_of th
dixon@15538
   277
    in
dixon@16004
   278
      if nprems < i then Seq.empty else
wenzelm@16978
   279
      let val thmseq = (Seq.of_list thms)
wenzelm@16978
   280
        fun apply_occ occK th =
wenzelm@18598
   281
            thmseq |> Seq.maps
wenzelm@16978
   282
                    (fn r =>
wenzelm@18598
   283
                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
dixon@16004
   284
                                            searchf_tlr_unify_valid) occK r
dixon@16004
   285
                                         (i + ((Thm.nprems_of th) - nprems))
dixon@16004
   286
                                         th);
wenzelm@16978
   287
        val sortedoccs =
dixon@16004
   288
            Library.sort (Library.rev_order o Library.int_ord) occL
dixon@16004
   289
      in
dixon@16004
   290
        Seq.map distinct_subgoals
dixon@16004
   291
                (Seq.EVERY (map apply_occ sortedoccs) th)
dixon@16004
   292
      end
dixon@16004
   293
    end
dixon@16004
   294
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
paulson@15481
   295
paulson@15481
   296
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   297
   the first one, then the second etc *)
wenzelm@18598
   298
fun eqsubst_asm_meth ctxt occL inthms =
wenzelm@16978
   299
    Method.METHOD
dixon@15538
   300
      (fn facts =>
wenzelm@18598
   301
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
paulson@15481
   302
paulson@15481
   303
(* syntax for options, given "(asm)" will give back true, without
paulson@15481
   304
   gives back false *)
paulson@15481
   305
val options_syntax =
paulson@15481
   306
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
paulson@15481
   307
     (Scan.succeed false);
dixon@15936
   308
dixon@15929
   309
val ith_syntax =
dixon@15936
   310
    (Args.parens (Scan.repeat Args.nat))
dixon@15936
   311
      || (Scan.succeed [0]);
paulson@15481
   312
wenzelm@18598
   313
(* combination method that takes a flag (true indicates that subst
wenzelm@18598
   314
should be done to an assumption, false = apply to the conclusion of
wenzelm@18598
   315
the goal) as well as the theorems to use *)
wenzelm@18598
   316
fun subst_meth src =
wenzelm@18988
   317
  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
wenzelm@18598
   318
  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
wenzelm@18598
   319
    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
paulson@15481
   320
wenzelm@18598
   321
wenzelm@16978
   322
val setup =
wenzelm@18833
   323
  Method.add_method ("subst", subst_meth, "single-step substitution");
paulson@15481
   324
wenzelm@16978
   325
end;