src/Pure/tactical.ML
author haftmann
Mon, 06 Feb 2017 20:56:34 +0100
changeset 64990 c6a7de505796
parent 62916 621afc4607ec
child 76051 854e9223767f
permissions -rw-r--r--
more explicit errors in pathological cases
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32169
fbada8ed12e6 renamed Pure/tctical.ML to Pure/tactical.ML;
wenzelm
parents: 32168
diff changeset
     1
(*  Title:      Pure/tactical.ML
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2158
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
16179
fa7e70be26b0 header;
wenzelm
parents: 15574
diff changeset
     4
Tacticals.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
4602
0e034d76932e added THEN_ALL_NEW;
wenzelm
parents: 4270
diff changeset
     7
infix 1 THEN THEN' THEN_ALL_NEW;
46463
3d0629a9ffca elininated unused INTLEAVE;
wenzelm
parents: 43278
diff changeset
     8
infix 0 ORELSE APPEND ORELSE' APPEND';
671
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
     9
infix 0 THEN_ELSE;
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
    10
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature TACTICAL =
11916
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
    12
sig
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    13
  type tactic = thm -> thm Seq.seq
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    14
  val THEN: tactic * tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    15
  val ORELSE: tactic * tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    16
  val APPEND: tactic * tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    17
  val THEN_ELSE: tactic * (tactic*tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    18
  val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    19
  val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    20
  val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    21
  val all_tac: tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    22
  val no_tac: tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    23
  val DETERM: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    24
  val COND: (thm -> bool) -> tactic -> tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    25
  val TRY: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    26
  val EVERY: tactic list -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    27
  val EVERY': ('a -> tactic) list -> 'a -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    28
  val EVERY1: (int -> tactic) list -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    29
  val FIRST: tactic list -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    30
  val FIRST': ('a -> tactic) list -> 'a -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    31
  val FIRST1: (int -> tactic) list -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    32
  val RANGE: (int -> tactic) list -> int -> tactic
56491
a8ccf3d6a6e4 proper context for print_tac;
wenzelm
parents: 56231
diff changeset
    33
  val print_tac: Proof.context -> string -> tactic
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    34
  val REPEAT_DETERM_N: int -> tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    35
  val REPEAT_DETERM: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    36
  val REPEAT: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    37
  val REPEAT_DETERM1: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    38
  val REPEAT1: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    39
  val FILTER: (thm -> bool) -> tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    40
  val CHANGED: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    41
  val CHANGED_PROP: tactic -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    42
  val ALLGOALS: (int -> tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    43
  val SOMEGOAL: (int -> tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    44
  val FIRSTGOAL: (int -> tactic) -> tactic
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 60941
diff changeset
    45
  val HEADGOAL: (int -> tactic) -> tactic
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    46
  val REPEAT_SOME: (int -> tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    47
  val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    48
  val REPEAT_FIRST: (int -> tactic) -> tactic
703
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
    49
  val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    50
  val TRYALL: (int -> tactic) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    51
  val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    52
  val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
49865
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46492
diff changeset
    53
  val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    54
  val CHANGED_GOAL: (int -> tactic) -> int -> tactic
34885
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
    55
  val SOLVED': (int -> tactic) -> int -> tactic
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    56
  val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    57
  val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    58
  val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    59
  val PRIMITIVE: (thm -> thm) -> tactic
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    60
  val SINGLE: tactic -> thm -> thm option
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
    61
  val CONVERSION: conv -> int -> tactic
11916
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
    62
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
13108
wenzelm
parents: 12851
diff changeset
    64
structure Tactical : TACTICAL =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(**** Tactics ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
(*A tactic maps a proof tree to a sequence of proof trees:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
    if length of sequence = 0 then the tactic does not apply;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
    if length > 1 then backtracking on the alternatives can occur.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 3991
diff changeset
    73
type tactic = thm -> thm Seq.seq;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(*** LCF-style tacticals ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(*the tactical THEN performs one tactic followed by another*)
17344
8b2f56aff711 Seq.maps;
wenzelm
parents: 16510
diff changeset
    79
fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
  Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
  Does not backtrack to tac2 if tac1 was initially chosen. *)
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    85
fun (tac1 ORELSE tac2) st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
    86
  (case Seq.pull (tac1 st) of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
    87
    NONE => tac2 st
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
    88
  | some => Seq.make (fn () => some));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
(*The tactical APPEND combines the results of two tactics.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  Like ORELSE, but allows backtracking on both tac1 and tac2.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
  The tactic tac2 is not applied until needed.*)
13108
wenzelm
parents: 12851
diff changeset
    94
fun (tac1 APPEND tac2) st =
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19646
diff changeset
    95
  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
671
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
    97
(*Conditional tactic.
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2158
diff changeset
    98
        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2158
diff changeset
    99
        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
671
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
   100
*)
13108
wenzelm
parents: 12851
diff changeset
   101
fun (tac THEN_ELSE (tac1, tac2)) st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   102
  (case Seq.pull (tac st) of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   103
    NONE => tac2 st  (*failed; try tactic 2*)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   104
  | some => Seq.maps tac1 (Seq.make (fn () => some)));  (*succeeded; use tactic 1*)
671
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
   105
e0be228a9c5b Pure/tctical/THEN_ELSE: new
lcp
parents: 631
diff changeset
   106
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
(*Versions for combining tactic-valued functions, as in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
     SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   109
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   110
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   111
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*passes all proofs through unchanged;  identity of THEN*)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 3991
diff changeset
   114
fun all_tac st = Seq.single st;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(*passes no proofs through;  identity of ORELSE and APPEND*)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 3991
diff changeset
   117
fun no_tac st  = Seq.empty;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
12851
e87496286934 generic DETERM;
wenzelm
parents: 12262
diff changeset
   121
fun DETERM tac = Seq.DETERM tac;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(*Conditional tactical: testfun controls which tactic to use next.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   125
fun COND testfun thenf elsef =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   126
  (fn st => if testfun st then thenf st else elsef st);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(*Do the tactic or else do nothing*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
fun TRY tac = tac ORELSE all_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   131
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   132
(*** List-oriented tactics ***)
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   133
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   134
local
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   135
  (*This version of EVERY avoids backtracking over repeated states*)
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   136
13108
wenzelm
parents: 12851
diff changeset
   137
  fun EVY (trail, []) st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   138
        Seq.make (fn () => SOME (st, Seq.make (fn () => Seq.pull (evyBack trail))))
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   139
    | EVY (trail, tac :: tacs) st =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   140
        (case Seq.pull (tac st) of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   141
          NONE => evyBack trail  (*failed: backtrack*)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   142
        | SOME (st', q) => EVY ((st', q, tacs) :: trail, tacs) st')
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 3991
diff changeset
   143
  and evyBack [] = Seq.empty (*no alternatives*)
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   144
    | evyBack ((st', q, tacs) :: trail) =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   145
        (case Seq.pull q of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   146
          NONE => evyBack trail
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   147
        | SOME (st, q') =>
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   148
            if Thm.eq_thm (st', st)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   149
            then evyBack ((st', q', tacs) :: trail)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   150
            else EVY ((st, q', tacs) :: trail, tacs) st);
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   151
in
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   152
  (* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   153
  fun EVERY tacs = EVY ([], tacs);
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   154
end;
2627
4ee01bb55a44 added THEN_MAYBE and THEN_MAYBE'
oheimb
parents: 2580
diff changeset
   155
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   157
(* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2627
diff changeset
   158
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
(*Apply every tactic to 1*)
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   161
fun EVERY1 tacs = EVERY' tacs 1;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
23178
07ba6b58b3d2 simplified/unified list fold;
wenzelm
parents: 23139
diff changeset
   164
fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   166
(* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
23178
07ba6b58b3d2 simplified/unified list fold;
wenzelm
parents: 23139
diff changeset
   167
fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
(*Apply first tactic to 1*)
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   170
fun FIRST1 tacs = FIRST' tacs 1;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
11916
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
   172
(*Apply tactics on consecutive subgoals*)
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
   173
fun RANGE [] _ = all_tac
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
   174
  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
82139d3dcdd7 added RANGE (from Isar/proof.ML);
wenzelm
parents: 11887
diff changeset
   175
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
(*Print the current proof state and pass it on.*)
56491
a8ccf3d6a6e4 proper context for print_tac;
wenzelm
parents: 56231
diff changeset
   178
fun print_tac ctxt msg st =
a8ccf3d6a6e4 proper context for print_tac;
wenzelm
parents: 56231
diff changeset
   179
 (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   180
  Seq.single st);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
13108
wenzelm
parents: 12851
diff changeset
   183
(*Deterministic REPEAT: only retains the first outcome;
703
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   184
  uses less space than REPEAT; tail recursive.
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   185
  If non-negative, n bounds the number of repetitions.*)
13108
wenzelm
parents: 12851
diff changeset
   186
fun REPEAT_DETERM_N n tac =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   187
  let
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   188
    fun drep 0 st = SOME (st, Seq.empty)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   189
      | drep n st =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   190
          (case Seq.pull (tac st) of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   191
            NONE => SOME(st, Seq.empty)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   192
          | SOME (st', _) => drep (n - 1) st');
62916
621afc4607ec eliminated ancient TTY-based Tactical.tracify and related global references;
wenzelm
parents: 61841
diff changeset
   193
  in fn st => Seq.make (fn () => drep n st) end;
703
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   194
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   195
(*Allows any number of repetitions*)
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   196
val REPEAT_DETERM = REPEAT_DETERM_N ~1;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
(*General REPEAT: maintains a stack of alternatives; tail recursive*)
13108
wenzelm
parents: 12851
diff changeset
   199
fun REPEAT tac =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   200
  let
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   201
    fun rep qs st =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   202
      (case Seq.pull (tac st) of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   203
        NONE => SOME (st, Seq.make (fn () => repq qs))
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   204
      | SOME (st', q) => rep (q :: qs) st')
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   205
    and repq [] = NONE
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   206
      | repq (q :: qs) =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   207
          (case Seq.pull q of
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   208
            NONE => repq qs
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   209
          | SOME (st, q) => rep (q :: qs) st);
62916
621afc4607ec eliminated ancient TTY-based Tactical.tracify and related global references;
wenzelm
parents: 61841
diff changeset
   210
  in fn st => Seq.make (fn () => rep [] st) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
(*Repeat 1 or more times*)
703
3a5cd2883581 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents: 671
diff changeset
   213
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
fun REPEAT1 tac = tac THEN REPEAT tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
(** Filtering tacticals **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 3991
diff changeset
   219
fun FILTER pred tac st = Seq.filter pred (tac st);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
13650
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13108
diff changeset
   221
(*Accept only next states that change the theorem somehow*)
13108
wenzelm
parents: 12851
diff changeset
   222
fun CHANGED tac st =
wenzelm
parents: 12851
diff changeset
   223
  let fun diff st' = not (Thm.eq_thm (st, st'));
wenzelm
parents: 12851
diff changeset
   224
  in Seq.filter diff (tac st) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
13650
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13108
diff changeset
   226
(*Accept only next states that change the theorem's prop field
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13108
diff changeset
   227
  (changes to signature, hyps, etc. don't count)*)
13108
wenzelm
parents: 12851
diff changeset
   228
fun CHANGED_PROP tac st =
22360
26ead7ed4f4b moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents: 20664
diff changeset
   229
  let fun diff st' = not (Thm.eq_thm_prop (st, st'));
13108
wenzelm
parents: 12851
diff changeset
   230
  in Seq.filter diff (tac st) end;
10821
dcb75538f542 CHANGED_PROP;
wenzelm
parents: 10767
diff changeset
   231
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(*** Tacticals based on subgoal numbering ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
13108
wenzelm
parents: 12851
diff changeset
   235
(*For n subgoals, performs tac(n) THEN ... THEN tac(1)
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   236
  Essential to work backwards since tac(i) may add/delete subgoals at i. *)
13108
wenzelm
parents: 12851
diff changeset
   237
fun ALLGOALS tac st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   238
  let
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   239
    fun doall 0 = all_tac
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   240
      | doall n = tac n THEN doall (n - 1);
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   241
  in doall (Thm.nprems_of st) st end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   243
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1)  *)
13108
wenzelm
parents: 12851
diff changeset
   244
fun SOMEGOAL tac st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   245
  let
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   246
    fun find 0 = no_tac
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   247
      | find n = tac n ORELSE find (n - 1);
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   248
  in find (Thm.nprems_of st) st end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   250
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
  More appropriate than SOMEGOAL in some cases.*)
13108
wenzelm
parents: 12851
diff changeset
   252
fun FIRSTGOAL tac st =
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   253
  let fun find (i, n) = if i > n then no_tac else tac i ORELSE find (i + 1, n)
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   254
  in find (1, Thm.nprems_of st) st end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
46466
61c7214b4885 tuned signature, according to actual usage of these operations;
wenzelm
parents: 46463
diff changeset
   256
(*First subgoal only.*)
61c7214b4885 tuned signature, according to actual usage of these operations;
wenzelm
parents: 46463
diff changeset
   257
fun HEADGOAL tac = tac 1;
61c7214b4885 tuned signature, according to actual usage of these operations;
wenzelm
parents: 46463
diff changeset
   258
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   259
(*Repeatedly solve some using tac. *)
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   260
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   261
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   263
(*Repeatedly solve the first possible subgoal using tac. *)
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   264
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac));
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   265
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   267
(*For n subgoals, tries to apply tac to n,...1  *)
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   268
fun TRYALL tac = ALLGOALS (TRY o tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
(*Make a tactic for subgoal i, if there is one.  *)
23224
e9fb2ff046fc added CSUBGOAL;
wenzelm
parents: 23178
diff changeset
   272
fun CSUBGOAL goalfun i st =
e9fb2ff046fc added CSUBGOAL;
wenzelm
parents: 23178
diff changeset
   273
  (case SOME (Thm.cprem_of st i) handle THM _ => NONE of
16510
606d919ad3c3 tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents: 16179
diff changeset
   274
    SOME goal => goalfun (goal, i) st
606d919ad3c3 tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents: 16179
diff changeset
   275
  | NONE => Seq.empty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
23224
e9fb2ff046fc added CSUBGOAL;
wenzelm
parents: 23178
diff changeset
   277
fun SUBGOAL goalfun =
e9fb2ff046fc added CSUBGOAL;
wenzelm
parents: 23178
diff changeset
   278
  CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
e9fb2ff046fc added CSUBGOAL;
wenzelm
parents: 23178
diff changeset
   279
60941
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   280
fun ASSERT_SUBGOAL (tac: int -> tactic) i st =
e7c761c63c18 tuned whitespace;
wenzelm
parents: 59660
diff changeset
   281
  (Logic.get_goal (Thm.prop_of st) i; tac i st);
49865
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46492
diff changeset
   282
5141
495a4f9af897 CHANGED_GOAL added to declare a more robust stac
paulson
parents: 4602
diff changeset
   283
(*Returns all states that have changed in subgoal i, counted from the LAST
495a4f9af897 CHANGED_GOAL added to declare a more robust stac
paulson
parents: 4602
diff changeset
   284
  subgoal.  For stac, for example.*)
13108
wenzelm
parents: 12851
diff changeset
   285
fun CHANGED_GOAL tac i st =
56231
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   286
  SUBGOAL (fn (t, _) =>
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   287
    let
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   288
      val np = Thm.nprems_of st;
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   289
      val d = np - i;  (*distance from END*)
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   290
      fun diff st' =
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   291
        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   292
        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 52131
diff changeset
   293
    in Seq.filter diff o tac i end) i st;
5141
495a4f9af897 CHANGED_GOAL added to declare a more robust stac
paulson
parents: 4602
diff changeset
   294
34885
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   295
(*Returns all states where some subgoals have been solved.  For
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   296
  subgoal-based tactics this means subgoal i has been solved
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   297
  altogether -- no new subgoals have emerged.*)
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   298
fun SOLVED' tac i st =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 56493
diff changeset
   299
  tac i st |> Seq.filter (fn st' => Thm.nprems_of st' < Thm.nprems_of st);
34885
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   300
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   301
(*Apply second tactic to all subgoals emerging from the first --
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   302
  following usual convention for subgoal-based tactics.*)
4602
0e034d76932e added THEN_ALL_NEW;
wenzelm
parents: 4270
diff changeset
   303
fun (tac1 THEN_ALL_NEW tac2) i st =
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59582
diff changeset
   304
  st |> (tac1 i THEN (fn st' =>
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 60941
diff changeset
   305
    st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));
4602
0e034d76932e added THEN_ALL_NEW;
wenzelm
parents: 4270
diff changeset
   306
34885
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 32738
diff changeset
   307
(*Repeatedly dig into any emerging subgoals.*)
8341
8f0f0ae02b10 added REPEAT_ALL_NEW;
wenzelm
parents: 8149
diff changeset
   308
fun REPEAT_ALL_NEW tac =
8f0f0ae02b10 added REPEAT_ALL_NEW;
wenzelm
parents: 8149
diff changeset
   309
  tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
8f0f0ae02b10 added REPEAT_ALL_NEW;
wenzelm
parents: 8149
diff changeset
   310
15006
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   311
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   312
fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   313
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   314
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   315
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
107e4dfd3b96 Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents: 13664
diff changeset
   316
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
   317
(*Inverse (more or less) of PRIMITIVE*)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   318
fun SINGLE tacf = Option.map fst o Seq.pull o tacf
19455
d828bfab05af cleaned up some diagnostic mathom
haftmann
parents: 19229
diff changeset
   319
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
   320
(*Conversions as tactics*)
23584
9b5ba76de1c2 tuned goal conversion interfaces;
wenzelm
parents: 23561
diff changeset
   321
fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
23561
a531c8da8a9b CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm
parents: 23538
diff changeset
   322
  handle THM _ => Seq.empty
a531c8da8a9b CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm
parents: 23538
diff changeset
   323
    | CTERM _ => Seq.empty
a531c8da8a9b CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm
parents: 23538
diff changeset
   324
    | TERM _ => Seq.empty
a531c8da8a9b CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm
parents: 23538
diff changeset
   325
    | TYPE _ => Seq.empty;
23538
438e5c4ef2c0 added CONVERSION tactical;
wenzelm
parents: 23384
diff changeset
   326
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
end;
1502
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   328
b612093c8bff Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   329
open Tactical;