1signature BasicProvers =
2sig
3  include Abbrev
4  type simpset = simpLib.simpset
5
6  (* Eliminate v = M or M = v from hypotheses *)
7
8  val VAR_EQ_TAC      : tactic
9  val var_eq_tac      : tactic
10
11  (* First order automatic proof *)
12
13  val PROVE           : thm list -> term -> thm
14  val PROVE_TAC       : thm list -> tactic
15  val prove_tac       : thm list -> tactic
16  val GEN_PROVE_TAC   : int -> int -> int -> thm list -> tactic
17
18  (* Simplification *)
19
20  val bool_ss         : simpset
21  val srw_ss          : unit -> simpset
22  val Abbr            : term quotation -> thm
23  val LEAVE_LETS      : thm
24
25  val RW_TAC          : simpset -> thm list -> tactic
26  val rw_tac          : simpset -> thm list -> tactic
27  val NORM_TAC        : simpset -> thm list -> tactic
28  val SRW_TAC         : simpLib.ssfrag list -> thm list -> tactic
29  val srw_tac         : simpLib.ssfrag list -> thm list -> tactic
30  val augment_srw_ss  : simpLib.ssfrag list -> unit
31  val diminish_srw_ss : string list -> simpLib.ssfrag list
32  val export_rewrites : string list -> unit
33  val thy_ssfrag      : string -> simpLib.ssfrag
34
35  (* LET manoeuvres *)
36  val LET_ELIM_TAC    : tactic
37  val new_let_thms    : thm list -> unit
38
39  (* Compound automated reasoners. *)
40
41  val PRIM_STP_TAC    : simpset -> tactic -> tactic
42  val STP_TAC         : simpset -> tactic -> tactic
43
44  (* Other reasoning support. *)
45  val SPOSE_NOT_THEN    : (thm -> tactic) -> tactic
46  val spose_not_then    : (thm -> tactic) -> tactic
47
48  val by                : term quotation * tactic -> tactic  (* infix *)
49  val byA               : term quotation * tactic -> tactic
50  val suffices_by       : term quotation * tactic -> tactic  (* infix *)
51  val on                : (thm -> tactic) * (term quotation * tactic) -> tactic
52                          (* infix *)
53  val subgoal           : term quotation -> tactic
54  val sg                : term quotation -> tactic
55
56  datatype tmkind
57      = Free of term
58      | Bound of term list * term
59      | Alien of term
60
61  val dest_tmkind       : tmkind -> term
62  val prim_find_subterm : term list -> term -> goal -> tmkind
63  val find_subterm      : term quotation -> goal -> tmkind
64  val primInduct        : tmkind -> tactic -> tactic
65  val Cases             : tactic
66  val Induct            : tactic
67  val Cases_on          : term quotation -> tactic
68  val Induct_on         : term quotation -> tactic
69
70  val PURE_TOP_CASE_TAC : tactic  (* top-most case-split *)
71  val PURE_CASE_TAC     : tactic  (* smallest case-split (concl) *)
72  val PURE_FULL_CASE_TAC: tactic  (* smallest case-split  (goal) *)
73
74  val PURE_CASE_SIMP_CONV : thm list -> conv
75  val CASE_SIMP_CONV    : conv     (* Apply case rewrites in theTypeBase *)
76
77  val CASE_TAC          : tactic   (* PURE_CASE_TAC then simplification *)
78  val TOP_CASE_TAC      : tactic   (* PURE_TOP_CASE_TAC then simplification *)
79  val FULL_CASE_TAC     : tactic   (* PURE_FULL_CASE_TAC then simplification *)
80  val full_case_tac     : tactic
81  val EVERY_CASE_TAC    : tactic   (* Repeat FULL_CASE_TAC *)
82  val every_case_tac    : tactic
83
84end
85