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