src/Pure/tactical.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 62916 621afc4607ec
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@32169
     1
(*  Title:      Pure/tactical.ML
paulson@2244
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
wenzelm@16179
     4
Tacticals.
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@4602
     7
infix 1 THEN THEN' THEN_ALL_NEW;
wenzelm@46463
     8
infix 0 ORELSE APPEND ORELSE' APPEND';
lcp@671
     9
infix 0 THEN_ELSE;
lcp@671
    10
clasohm@0
    11
signature TACTICAL =
wenzelm@11916
    12
sig
wenzelm@23538
    13
  type tactic = thm -> thm Seq.seq
wenzelm@23538
    14
  val THEN: tactic * tactic -> tactic
wenzelm@23538
    15
  val ORELSE: tactic * tactic -> tactic
wenzelm@23538
    16
  val APPEND: tactic * tactic -> tactic
wenzelm@23538
    17
  val THEN_ELSE: tactic * (tactic*tactic) -> tactic
wenzelm@23538
    18
  val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
wenzelm@23538
    19
  val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
wenzelm@23538
    20
  val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
wenzelm@23538
    21
  val all_tac: tactic
wenzelm@23538
    22
  val no_tac: tactic
wenzelm@23538
    23
  val DETERM: tactic -> tactic
wenzelm@23538
    24
  val COND: (thm -> bool) -> tactic -> tactic -> tactic
wenzelm@23538
    25
  val TRY: tactic -> tactic
wenzelm@23538
    26
  val EVERY: tactic list -> tactic
wenzelm@23538
    27
  val EVERY': ('a -> tactic) list -> 'a -> tactic
wenzelm@23538
    28
  val EVERY1: (int -> tactic) list -> tactic
wenzelm@23538
    29
  val FIRST: tactic list -> tactic
wenzelm@23538
    30
  val FIRST': ('a -> tactic) list -> 'a -> tactic
wenzelm@23538
    31
  val FIRST1: (int -> tactic) list -> tactic
wenzelm@23538
    32
  val RANGE: (int -> tactic) list -> int -> tactic
wenzelm@56491
    33
  val print_tac: Proof.context -> string -> tactic
wenzelm@23538
    34
  val REPEAT_DETERM_N: int -> tactic -> tactic
wenzelm@23538
    35
  val REPEAT_DETERM: tactic -> tactic
wenzelm@23538
    36
  val REPEAT: tactic -> tactic
wenzelm@23538
    37
  val REPEAT_DETERM1: tactic -> tactic
wenzelm@23538
    38
  val REPEAT1: tactic -> tactic
wenzelm@23538
    39
  val FILTER: (thm -> bool) -> tactic -> tactic
wenzelm@23538
    40
  val CHANGED: tactic -> tactic
wenzelm@23538
    41
  val CHANGED_PROP: tactic -> tactic
wenzelm@23538
    42
  val ALLGOALS: (int -> tactic) -> tactic
wenzelm@23538
    43
  val SOMEGOAL: (int -> tactic) -> tactic
wenzelm@23538
    44
  val FIRSTGOAL: (int -> tactic) -> tactic
wenzelm@61841
    45
  val HEADGOAL: (int -> tactic) -> tactic
wenzelm@23538
    46
  val REPEAT_SOME: (int -> tactic) -> tactic
wenzelm@23538
    47
  val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
wenzelm@23538
    48
  val REPEAT_FIRST: (int -> tactic) -> tactic
lcp@703
    49
  val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
wenzelm@23538
    50
  val TRYALL: (int -> tactic) -> tactic
wenzelm@23538
    51
  val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
wenzelm@23538
    52
  val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
wenzelm@49865
    53
  val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic
wenzelm@23538
    54
  val CHANGED_GOAL: (int -> tactic) -> int -> tactic
wenzelm@34885
    55
  val SOLVED': (int -> tactic) -> int -> tactic
wenzelm@23538
    56
  val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
wenzelm@23538
    57
  val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
wenzelm@23538
    58
  val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
wenzelm@23538
    59
  val PRIMITIVE: (thm -> thm) -> tactic
wenzelm@23538
    60
  val SINGLE: tactic -> thm -> thm option
wenzelm@23538
    61
  val CONVERSION: conv -> int -> tactic
wenzelm@11916
    62
end;
clasohm@0
    63
wenzelm@13108
    64
structure Tactical : TACTICAL =
clasohm@0
    65
struct
clasohm@0
    66
clasohm@0
    67
(**** Tactics ****)
clasohm@0
    68
clasohm@0
    69
(*A tactic maps a proof tree to a sequence of proof trees:
clasohm@0
    70
    if length of sequence = 0 then the tactic does not apply;
clasohm@0
    71
    if length > 1 then backtracking on the alternatives can occur.*)
clasohm@0
    72
wenzelm@4270
    73
type tactic = thm -> thm Seq.seq;
clasohm@0
    74
clasohm@0
    75
clasohm@0
    76
(*** LCF-style tacticals ***)
clasohm@0
    77
clasohm@0
    78
(*the tactical THEN performs one tactic followed by another*)
wenzelm@17344
    79
fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
clasohm@0
    80
clasohm@0
    81
clasohm@0
    82
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
clasohm@0
    83
  Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
clasohm@0
    84
  Does not backtrack to tac2 if tac1 was initially chosen. *)
paulson@1502
    85
fun (tac1 ORELSE tac2) st =
wenzelm@60941
    86
  (case Seq.pull (tac1 st) of
wenzelm@60941
    87
    NONE => tac2 st
wenzelm@60941
    88
  | some => Seq.make (fn () => some));
clasohm@0
    89
clasohm@0
    90
clasohm@0
    91
(*The tactical APPEND combines the results of two tactics.
clasohm@0
    92
  Like ORELSE, but allows backtracking on both tac1 and tac2.
clasohm@0
    93
  The tactic tac2 is not applied until needed.*)
wenzelm@13108
    94
fun (tac1 APPEND tac2) st =
wenzelm@19861
    95
  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
clasohm@0
    96
lcp@671
    97
(*Conditional tactic.
paulson@2244
    98
        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
paulson@2244
    99
        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
lcp@671
   100
*)
wenzelm@13108
   101
fun (tac THEN_ELSE (tac1, tac2)) st =
wenzelm@60941
   102
  (case Seq.pull (tac st) of
wenzelm@60941
   103
    NONE => tac2 st  (*failed; try tactic 2*)
wenzelm@60941
   104
  | some => Seq.maps tac1 (Seq.make (fn () => some)));  (*succeeded; use tactic 1*)
lcp@671
   105
lcp@671
   106
clasohm@0
   107
(*Versions for combining tactic-valued functions, as in
clasohm@0
   108
     SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
paulson@1502
   109
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
paulson@1502
   110
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
paulson@1502
   111
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
clasohm@0
   112
clasohm@0
   113
(*passes all proofs through unchanged;  identity of THEN*)
wenzelm@4270
   114
fun all_tac st = Seq.single st;
clasohm@0
   115
clasohm@0
   116
(*passes no proofs through;  identity of ORELSE and APPEND*)
wenzelm@4270
   117
fun no_tac st  = Seq.empty;
clasohm@0
   118
clasohm@0
   119
clasohm@0
   120
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
wenzelm@12851
   121
fun DETERM tac = Seq.DETERM tac;
clasohm@0
   122
clasohm@0
   123
(*Conditional tactical: testfun controls which tactic to use next.
clasohm@0
   124
  Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
wenzelm@60941
   125
fun COND testfun thenf elsef =
wenzelm@60941
   126
  (fn st => if testfun st then thenf st else elsef st);
clasohm@0
   127
clasohm@0
   128
(*Do the tactic or else do nothing*)
clasohm@0
   129
fun TRY tac = tac ORELSE all_tac;
clasohm@0
   130
wenzelm@60941
   131
paulson@2672
   132
(*** List-oriented tactics ***)
paulson@2672
   133
paulson@2672
   134
local
paulson@2672
   135
  (*This version of EVERY avoids backtracking over repeated states*)
paulson@2672
   136
wenzelm@13108
   137
  fun EVY (trail, []) st =
wenzelm@60941
   138
        Seq.make (fn () => SOME (st, Seq.make (fn () => Seq.pull (evyBack trail))))
wenzelm@60941
   139
    | EVY (trail, tac :: tacs) st =
wenzelm@60941
   140
        (case Seq.pull (tac st) of
wenzelm@60941
   141
          NONE => evyBack trail  (*failed: backtrack*)
wenzelm@60941
   142
        | SOME (st', q) => EVY ((st', q, tacs) :: trail, tacs) st')
wenzelm@4270
   143
  and evyBack [] = Seq.empty (*no alternatives*)
wenzelm@60941
   144
    | evyBack ((st', q, tacs) :: trail) =
wenzelm@60941
   145
        (case Seq.pull q of
wenzelm@60941
   146
          NONE => evyBack trail
wenzelm@60941
   147
        | SOME (st, q') =>
wenzelm@60941
   148
            if Thm.eq_thm (st', st)
wenzelm@60941
   149
            then evyBack ((st', q', tacs) :: trail)
wenzelm@60941
   150
            else EVY ((st, q', tacs) :: trail, tacs) st);
paulson@2672
   151
in
wenzelm@60941
   152
  (* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
wenzelm@60941
   153
  fun EVERY tacs = EVY ([], tacs);
paulson@2672
   154
end;
oheimb@2627
   155
clasohm@0
   156
paulson@1502
   157
(* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
paulson@2672
   158
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
clasohm@0
   159
clasohm@0
   160
(*Apply every tactic to 1*)
paulson@1502
   161
fun EVERY1 tacs = EVERY' tacs 1;
clasohm@0
   162
clasohm@0
   163
(* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
wenzelm@23178
   164
fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
clasohm@0
   165
paulson@1502
   166
(* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
wenzelm@23178
   167
fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
clasohm@0
   168
clasohm@0
   169
(*Apply first tactic to 1*)
paulson@1502
   170
fun FIRST1 tacs = FIRST' tacs 1;
clasohm@0
   171
wenzelm@11916
   172
(*Apply tactics on consecutive subgoals*)
wenzelm@11916
   173
fun RANGE [] _ = all_tac
wenzelm@11916
   174
  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
wenzelm@11916
   175
clasohm@0
   176
clasohm@0
   177
(*Print the current proof state and pass it on.*)
wenzelm@56491
   178
fun print_tac ctxt msg st =
wenzelm@56491
   179
 (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
wenzelm@32145
   180
  Seq.single st);
clasohm@0
   181
clasohm@0
   182
wenzelm@13108
   183
(*Deterministic REPEAT: only retains the first outcome;
lcp@703
   184
  uses less space than REPEAT; tail recursive.
lcp@703
   185
  If non-negative, n bounds the number of repetitions.*)
wenzelm@13108
   186
fun REPEAT_DETERM_N n tac =
wenzelm@60941
   187
  let
wenzelm@60941
   188
    fun drep 0 st = SOME (st, Seq.empty)
wenzelm@60941
   189
      | drep n st =
wenzelm@60941
   190
          (case Seq.pull (tac st) of
wenzelm@60941
   191
            NONE => SOME(st, Seq.empty)
wenzelm@60941
   192
          | SOME (st', _) => drep (n - 1) st');
wenzelm@62916
   193
  in fn st => Seq.make (fn () => drep n st) end;
lcp@703
   194
lcp@703
   195
(*Allows any number of repetitions*)
lcp@703
   196
val REPEAT_DETERM = REPEAT_DETERM_N ~1;
clasohm@0
   197
clasohm@0
   198
(*General REPEAT: maintains a stack of alternatives; tail recursive*)
wenzelm@13108
   199
fun REPEAT tac =
wenzelm@60941
   200
  let
wenzelm@60941
   201
    fun rep qs st =
wenzelm@60941
   202
      (case Seq.pull (tac st) of
wenzelm@60941
   203
        NONE => SOME (st, Seq.make (fn () => repq qs))
wenzelm@60941
   204
      | SOME (st', q) => rep (q :: qs) st')
wenzelm@60941
   205
    and repq [] = NONE
wenzelm@60941
   206
      | repq (q :: qs) =
wenzelm@60941
   207
          (case Seq.pull q of
wenzelm@60941
   208
            NONE => repq qs
wenzelm@60941
   209
          | SOME (st, q) => rep (q :: qs) st);
wenzelm@62916
   210
  in fn st => Seq.make (fn () => rep [] st) end;
clasohm@0
   211
clasohm@0
   212
(*Repeat 1 or more times*)
lcp@703
   213
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
clasohm@0
   214
fun REPEAT1 tac = tac THEN REPEAT tac;
clasohm@0
   215
clasohm@0
   216
clasohm@0
   217
(** Filtering tacticals **)
clasohm@0
   218
wenzelm@4270
   219
fun FILTER pred tac st = Seq.filter pred (tac st);
clasohm@0
   220
paulson@13650
   221
(*Accept only next states that change the theorem somehow*)
wenzelm@13108
   222
fun CHANGED tac st =
wenzelm@13108
   223
  let fun diff st' = not (Thm.eq_thm (st, st'));
wenzelm@13108
   224
  in Seq.filter diff (tac st) end;
clasohm@0
   225
paulson@13650
   226
(*Accept only next states that change the theorem's prop field
paulson@13650
   227
  (changes to signature, hyps, etc. don't count)*)
wenzelm@13108
   228
fun CHANGED_PROP tac st =
wenzelm@22360
   229
  let fun diff st' = not (Thm.eq_thm_prop (st, st'));
wenzelm@13108
   230
  in Seq.filter diff (tac st) end;
wenzelm@10821
   231
clasohm@0
   232
clasohm@0
   233
(*** Tacticals based on subgoal numbering ***)
clasohm@0
   234
wenzelm@13108
   235
(*For n subgoals, performs tac(n) THEN ... THEN tac(1)
paulson@1502
   236
  Essential to work backwards since tac(i) may add/delete subgoals at i. *)
wenzelm@13108
   237
fun ALLGOALS tac st =
wenzelm@60941
   238
  let
wenzelm@60941
   239
    fun doall 0 = all_tac
wenzelm@60941
   240
      | doall n = tac n THEN doall (n - 1);
wenzelm@60941
   241
  in doall (Thm.nprems_of st) st end;
clasohm@0
   242
paulson@1502
   243
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1)  *)
wenzelm@13108
   244
fun SOMEGOAL tac st =
wenzelm@60941
   245
  let
wenzelm@60941
   246
    fun find 0 = no_tac
wenzelm@60941
   247
      | find n = tac n ORELSE find (n - 1);
wenzelm@60941
   248
  in find (Thm.nprems_of st) st end;
clasohm@0
   249
paulson@1502
   250
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
clasohm@0
   251
  More appropriate than SOMEGOAL in some cases.*)
wenzelm@13108
   252
fun FIRSTGOAL tac st =
wenzelm@60941
   253
  let fun find (i, n) = if i > n then no_tac else tac i ORELSE find (i + 1, n)
wenzelm@60941
   254
  in find (1, Thm.nprems_of st) st end;
clasohm@0
   255
wenzelm@46466
   256
(*First subgoal only.*)
wenzelm@46466
   257
fun HEADGOAL tac = tac 1;
wenzelm@46466
   258
paulson@1502
   259
(*Repeatedly solve some using tac. *)
paulson@1502
   260
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
paulson@1502
   261
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));
clasohm@0
   262
paulson@1502
   263
(*Repeatedly solve the first possible subgoal using tac. *)
paulson@1502
   264
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac));
paulson@1502
   265
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac));
clasohm@0
   266
paulson@1502
   267
(*For n subgoals, tries to apply tac to n,...1  *)
paulson@1502
   268
fun TRYALL tac = ALLGOALS (TRY o tac);
clasohm@0
   269
clasohm@0
   270
clasohm@0
   271
(*Make a tactic for subgoal i, if there is one.  *)
wenzelm@23224
   272
fun CSUBGOAL goalfun i st =
wenzelm@23224
   273
  (case SOME (Thm.cprem_of st i) handle THM _ => NONE of
wenzelm@16510
   274
    SOME goal => goalfun (goal, i) st
wenzelm@16510
   275
  | NONE => Seq.empty);
clasohm@0
   276
wenzelm@23224
   277
fun SUBGOAL goalfun =
wenzelm@23224
   278
  CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
wenzelm@23224
   279
wenzelm@60941
   280
fun ASSERT_SUBGOAL (tac: int -> tactic) i st =
wenzelm@60941
   281
  (Logic.get_goal (Thm.prop_of st) i; tac i st);
wenzelm@49865
   282
paulson@5141
   283
(*Returns all states that have changed in subgoal i, counted from the LAST
paulson@5141
   284
  subgoal.  For stac, for example.*)
wenzelm@13108
   285
fun CHANGED_GOAL tac i st =
wenzelm@56231
   286
  SUBGOAL (fn (t, _) =>
wenzelm@56231
   287
    let
wenzelm@56231
   288
      val np = Thm.nprems_of st;
wenzelm@56231
   289
      val d = np - i;  (*distance from END*)
wenzelm@56231
   290
      fun diff st' =
wenzelm@56231
   291
        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
wenzelm@56231
   292
        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
wenzelm@56231
   293
    in Seq.filter diff o tac i end) i st;
paulson@5141
   294
wenzelm@34885
   295
(*Returns all states where some subgoals have been solved.  For
wenzelm@34885
   296
  subgoal-based tactics this means subgoal i has been solved
wenzelm@34885
   297
  altogether -- no new subgoals have emerged.*)
wenzelm@34885
   298
fun SOLVED' tac i st =
wenzelm@59582
   299
  tac i st |> Seq.filter (fn st' => Thm.nprems_of st' < Thm.nprems_of st);
wenzelm@34885
   300
wenzelm@34885
   301
(*Apply second tactic to all subgoals emerging from the first --
wenzelm@34885
   302
  following usual convention for subgoal-based tactics.*)
wenzelm@4602
   303
fun (tac1 THEN_ALL_NEW tac2) i st =
wenzelm@59660
   304
  st |> (tac1 i THEN (fn st' =>
wenzelm@61841
   305
    st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));
wenzelm@4602
   306
wenzelm@34885
   307
(*Repeatedly dig into any emerging subgoals.*)
wenzelm@8341
   308
fun REPEAT_ALL_NEW tac =
wenzelm@8341
   309
  tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
wenzelm@8341
   310
skalberg@15006
   311
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
skalberg@15006
   312
fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
skalberg@15006
   313
skalberg@15006
   314
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
skalberg@15006
   315
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
skalberg@15006
   316
wenzelm@23538
   317
(*Inverse (more or less) of PRIMITIVE*)
skalberg@15570
   318
fun SINGLE tacf = Option.map fst o Seq.pull o tacf
haftmann@19455
   319
wenzelm@23538
   320
(*Conversions as tactics*)
wenzelm@23584
   321
fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
wenzelm@23561
   322
  handle THM _ => Seq.empty
wenzelm@23561
   323
    | CTERM _ => Seq.empty
wenzelm@23561
   324
    | TERM _ => Seq.empty
wenzelm@23561
   325
    | TYPE _ => Seq.empty;
wenzelm@23538
   326
clasohm@0
   327
end;
paulson@1502
   328
paulson@1502
   329
open Tactical;