1signature Tactical =
2sig
3  include Abbrev
4
5  val TAC_PROOF      : goal * tactic -> thm
6  val prove          : term * tactic -> thm
7  val store_thm      : string * term * tactic -> thm
8  val CONV_TAC       : conv -> tactic
9  val THEN           : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
10  val >>             : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
11  val \\             : ('a,'b) gentactic * tactic -> ('a,'b) gentactic
12  (* could be used as
13  val THEN           : tactic * tactic -> tactic
14  val THEN           : list_tactic * tactic -> list_tactic
15  *)
16  val THENL          : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
17  val >|             : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
18  (* could be used as
19  val THENL          : tactic * tactic list -> tactic
20  val THENL          : list_tactic * tactic list -> list_tactic
21  *)
22  val ORELSE         : tactic * tactic -> tactic
23  val ORELSE_LT      : list_tactic * list_tactic -> list_tactic
24  val THEN1          : tactic * tactic -> tactic
25  val >-             : tactic * tactic -> tactic
26  val THEN_LT        : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic
27  val >>>            : ('a,'b) gentactic * list_tactic -> ('a,'b) gentactic
28  (* could be used as
29  val THEN_LT        : tactic * list_tactic -> tactic
30  val THEN_LT        : list_tactic * list_tactic -> list_tactic
31  *)
32  val >>-            : tactic * int -> tactic -> tactic
33  val ??             : ('a -> 'b) * 'a -> 'b
34  val TACS_TO_LT     : tactic list -> list_tactic
35  val NULL_OK_LT     : list_tactic -> list_tactic
36  val ALLGOALS       : tactic -> list_tactic
37  val TRYALL         : tactic -> list_tactic
38  val NTH_GOAL       : tactic -> int -> list_tactic
39  val LASTGOAL       : tactic -> list_tactic
40  val HEADGOAL       : tactic -> list_tactic
41  val SPLIT_LT       : int -> list_tactic * list_tactic -> list_tactic
42  val ROTATE_LT      : int -> list_tactic
43  val REVERSE        : tactic -> tactic
44  val reverse        : tactic -> tactic
45  val REVERSE_LT     : list_tactic
46  val FAIL_TAC       : string -> tactic
47  val NO_TAC         : tactic
48  val FAIL_LT        : string -> list_tactic
49  val NO_LT          : list_tactic
50  val ALL_TAC        : tactic
51  val all_tac        : tactic
52  val ALL_LT         : list_tactic
53  val TRY            : tactic -> tactic
54  val TRY_LT         : list_tactic -> list_tactic
55  val REPEAT         : tactic -> tactic
56  val rpt            : tactic -> tactic
57  val REPEAT_LT      : list_tactic -> list_tactic
58  val VALID          : tactic -> tactic
59  val VALID_LT       : list_tactic -> list_tactic
60  val VALIDATE       : tactic -> tactic
61  val VALIDATE_LT    : list_tactic -> list_tactic
62  val GEN_VALIDATE   : bool -> tactic -> tactic
63  val GEN_VALIDATE_LT: bool -> list_tactic -> list_tactic
64  val ADD_SGS_TAC    : term list -> tactic -> tactic
65  val EVERY          : tactic list -> tactic
66  val EVERY_LT       : list_tactic list -> list_tactic
67  val FIRST          : tactic list -> tactic
68  val MAP_EVERY      : ('a -> tactic) -> 'a list -> tactic
69  val map_every      : ('a -> tactic) -> 'a list -> tactic
70  val MAP_FIRST      : ('a -> tactic) -> 'a list -> tactic
71  val FIRST_PROVE    : tactic list -> tactic
72  val EVERY_ASSUM    : thm_tactic -> tactic
73  val FIRST_ASSUM    : thm_tactic -> tactic
74  val first_assum    : thm_tactic -> tactic
75  val FIRST_X_ASSUM  : thm_tactic -> tactic
76  val first_x_assum  : thm_tactic -> tactic
77  val LAST_ASSUM     : thm_tactic -> tactic
78  val last_assum     : thm_tactic -> tactic
79  val LAST_X_ASSUM   : thm_tactic -> tactic
80  val last_x_assum   : thm_tactic -> tactic
81  val goal_assum     : thm_tactic -> tactic
82  val hdtm_assum     : term -> thm_tactic -> tactic
83  val hdtm_x_assum   : term -> thm_tactic -> tactic
84
85  val ASSUM_LIST     : (thm list -> tactic) -> tactic
86  val POP_ASSUM      : thm_tactic -> tactic
87  val pop_assum      : thm_tactic -> tactic
88  val PRED_ASSUM     : (term -> bool) -> thm_tactic -> tactic
89  val PAT_ASSUM      : term -> thm_tactic -> tactic
90  val PAT_X_ASSUM    : term -> thm_tactic -> tactic
91  val POP_ASSUM_LIST : (thm list -> tactic) -> tactic
92  val SUBGOAL_THEN   : term -> thm_tactic -> tactic
93  val USE_SG_THEN    : thm_tactic -> int -> int -> list_tactic
94  val CHANGED_TAC    : tactic -> tactic
95  val check_delta    : exn -> (goal * goal list -> bool) -> tactic -> tactic
96  val count0         : (term -> int) -> (goal * goal list -> bool)
97  val count_decreases: (term -> int) -> (goal * goal list -> bool)
98
99
100  val Q_TAC0         : {traces : (string * int) list} -> hol_type option ->
101                       (term -> tactic) -> term quotation -> tactic
102  val Q_TAC          : (term -> tactic) -> term quotation -> tactic
103  val QTY_TAC        : hol_type -> (term -> tactic) -> term quotation -> tactic
104
105  val default_prover : term * tactic -> thm
106  val set_prover     : (term * tactic -> thm) -> unit
107  val restore_prover : unit -> unit
108
109end
110