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 -> unit
32  val export_rewrites : string list -> unit
33  val delsimps        : string list -> unit
34  val temp_delsimps   : string list -> unit
35  val thy_ssfrag      : string -> simpLib.ssfrag
36  val thy_simpset     : string -> simpset option
37  val temp_setsimpset : simpset -> unit
38  val merge_simpsets  : string list -> simpset
39  datatype srw_update = ADD_SSFRAG of simpLib.ssfrag | REMOVE_RWT of string
40  val simpset_state   : unit -> simpset * bool * srw_update list
41  val logged_update   : {thyname : string} -> (simpset -> simpset) -> unit
42  val logged_addfrags : {thyname : string} -> simpLib.ssfrag list -> unit
43  val do_logged_updates : {theories : string list} -> unit
44  val apply_logged_updates : {theories : string list} -> (simpset -> simpset)
45  val augment_with_typebase : TypeBasePure.typeBase -> simpset -> simpset
46  val temp_set_simpset_ancestry : string list -> unit
47  val set_simpset_ancestry : string list -> unit
48  val recreate_sset_at_parentage : string list -> unit
49
50  (* LET and Abbrev manoeuvres *)
51  val LET_ELIM_TAC    : tactic
52  val new_let_thms    : thm list -> unit
53  val TIDY_ABBREVS    : tactic
54
55  (* Compound automated reasoners. *)
56
57  val PRIM_STP_TAC    : simpset -> tactic -> tactic
58  val STP_TAC         : simpset -> tactic -> tactic
59
60  (* Other reasoning support. *)
61  val SPOSE_NOT_THEN    : (thm -> tactic) -> tactic
62  val spose_not_then    : (thm -> tactic) -> tactic
63
64  val by                : term quotation * tactic -> tactic  (* infix *)
65  val byA               : term quotation * tactic -> tactic
66  val suffices_by       : term quotation * tactic -> tactic  (* infix *)
67  val on                : (thm -> tactic) * (term quotation * tactic) -> tactic
68                          (* infix *)
69  val subgoal           : term quotation -> tactic
70  val sg                : term quotation -> tactic
71
72  datatype tmkind
73      = Free of term
74      | Bound of term list * term
75      | Alien of term
76
77  val dest_tmkind       : tmkind -> term
78  val prim_find_subterm : term list -> term -> goal -> tmkind
79  val find_subterm      : term quotation -> goal -> tmkind
80  val primInduct        : tmkind -> tactic -> tactic
81  val Cases             : tactic
82  val Induct            : tactic
83  val namedCases        : string list -> tactic
84
85  val tmCases_on        : term -> string list -> tactic
86  val Cases_on          : term quotation -> tactic
87  val Induct_on         : term quotation -> tactic
88  val namedCases_on     : term quotation -> string list -> tactic
89
90  val PURE_TOP_CASE_TAC : tactic  (* top-most case-split *)
91  val PURE_CASE_TAC     : tactic  (* smallest case-split (concl) *)
92  val PURE_FULL_CASE_TAC: tactic  (* smallest case-split  (goal) *)
93
94  val PURE_CASE_SIMP_CONV : thm list -> conv
95  val CASE_SIMP_CONV    : conv     (* Apply case rewrites in theTypeBase *)
96
97  val CASE_TAC          : tactic   (* PURE_CASE_TAC then simplification *)
98  val TOP_CASE_TAC      : tactic   (* PURE_TOP_CASE_TAC then simplification *)
99  val FULL_CASE_TAC     : tactic   (* PURE_FULL_CASE_TAC then simplification *)
100  val full_case_tac     : tactic
101  val EVERY_CASE_TAC    : tactic   (* Repeat FULL_CASE_TAC *)
102  val every_case_tac    : tactic
103
104end
105