1signature bossLib =
2sig
3  include Abbrev
4  type ssfrag = simpLib.ssfrag
5  type simpset = simpLib.simpset
6
7  (* Make definitions *)
8
9  (* new types *)
10  val Hol_datatype : hol_type quotation -> unit
11  val Datatype : hol_type quotation -> unit
12
13  (* new functions *)
14  val Define       : term quotation -> thm
15  val zDefine      : term quotation -> thm
16  val xDefine      : string -> term quotation -> thm
17  val tDefine      : string -> term quotation -> tactic -> thm
18  val WF_REL_TAC   : term quotation -> tactic
19  val Hol_defn     : string -> term quotation -> DefnBase.defn
20
21  (* new (inductive) relations *)
22  val Hol_reln     : term quotation -> thm * thm * thm
23  val Hol_coreln   : term quotation -> thm * thm * thm
24  val xHol_reln    : string -> term quotation -> thm * thm * thm
25  val xHol_coreln  : string -> term quotation -> thm * thm * thm
26  val export_mono  : string -> unit
27
28  (* Derived rule for specifying new constants.
29     Should have the same effect as Theory.Definition.new_specification. *)
30  val new_specification : string * string list * thm -> thm
31
32  (* Case-splitting and induction operations *)
33
34  val Cases             : tactic
35  val Cases_on          : term quotation -> tactic
36  val tmCases_on        : term -> string list -> tactic
37  val PairCases         : tactic
38  val PairCases_on      : term quotation -> tactic
39  val Induct            : tactic
40  val Induct_on         : term quotation -> tactic
41  val recInduct         : thm -> tactic
42  val namedCases        : string list -> tactic
43  val namedCases_on     : term quotation -> string list -> tactic
44
45  val measureInduct_on  : term quotation -> tactic
46  val completeInduct_on : term quotation -> tactic
47  val using             : tactic * thm -> tactic (* infix *)
48  val usingA            : tactic -> thm -> tactic (* curry of above *)
49
50  val pairarg_tac       : tactic
51  val split_pair_case_tac : tactic
52
53  val CASE_TAC          : tactic
54  val CaseEq            : string -> thm
55  val CaseEqs           : string list -> thm
56  val AllCaseEqs        : unit -> thm
57
58  (* Proof automation *)
59
60  val PROVE          : thm list -> term -> thm   (* First order *)
61  val METIS_PROVE    : thm list -> term -> thm   (* First order *)
62  val DECIDE         : term -> thm               (* Cooperating dec. procs *)
63  val PROVE_TAC      : thm list -> tactic
64  val prove_tac      : thm list -> tactic
65  val METIS_TAC      : thm list -> tactic
66  val metis_tac      : thm list -> tactic
67  val DECIDE_TAC     : tactic
68  val decide_tac     : tactic
69
70  (* Simplification *)
71
72  val ++              : simpset * ssfrag -> simpset    (* infix *)
73  val &&              : simpset * thm list -> simpset  (* infix *)
74  val -*              : simpset * string list -> simpset (* infix *)
75  val pure_ss         : simpset
76  val bool_ss         : simpset
77  val std_ss          : simpset           (* bool + option + pair + sum *)
78  val arith_ss        : simpset
79  val old_arith_ss    : simpset
80  val list_ss         : simpset
81  val srw_ss          : unit -> simpset
82  val QI_ss           : ssfrag
83  val SQI_ss          : ssfrag
84  val ARITH_ss        : ssfrag            (* arithmetic d.p. + some rewrites *)
85  val old_ARITH_ss    : ssfrag
86  val type_rws        : hol_type -> thm list
87  val rewrites        : thm list -> ssfrag
88  val augment_srw_ss  : ssfrag list -> unit
89  val diminish_srw_ss : string list -> unit
90  val export_rewrites : string list -> unit
91  val delsimps        : string list -> unit
92  val temp_delsimps   : string list -> unit
93  val limit           : int -> simpset -> simpset
94
95  (* use these in simplifier's argument list *)
96  val SimpLHS        : thm
97  val SimpRHS        : thm
98  val SimpL          : term -> thm
99  val SimpR          : term -> thm
100
101  val Cong           : thm -> thm
102  val AC             : thm -> thm -> thm
103  val Excl           : string -> thm
104  val Req0           : thm -> thm
105  val ReqD           : thm -> thm
106
107  val SIMP_CONV         : simpset -> thm list -> conv
108  val SIMP_RULE         : simpset -> thm list -> thm -> thm
109  val SIMP_TAC          : simpset -> thm list -> tactic
110  val simp_tac          : simpset -> thm list -> tactic
111  val ASM_SIMP_TAC      : simpset -> thm list -> tactic
112  val asm_simp_tac      : simpset -> thm list -> tactic
113  val FULL_SIMP_TAC     : simpset -> thm list -> tactic
114  val full_simp_tac     : simpset -> thm list -> tactic
115  val REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
116  val rev_full_simp_tac : simpset -> thm list -> tactic
117  val RW_TAC            : simpset -> thm list -> tactic
118  val rw_tac            : simpset -> thm list -> tactic
119  val SRW_TAC           : ssfrag list -> thm list -> tactic
120  val srw_tac           : ssfrag list -> thm list -> tactic
121
122  val NO_STRIP_FULL_SIMP_TAC     : simpset -> thm list -> tactic
123  val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
124
125  val QI_TAC     : tactic
126  val ASM_QI_TAC : tactic
127  val GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic
128
129  (* Call-by-value evaluation *)
130  val EVAL           : conv
131  val EVAL_RULE      : thm -> thm
132  val EVAL_TAC       : tactic
133
134  (* Automate some routine set theory by reduction to FOL *)
135  val SET_TAC        : thm list -> tactic
136  val ASM_SET_TAC    : thm list -> tactic
137  val SET_RULE       : term -> thm
138
139  (* Miscellaneous *)
140
141  val ZAP_TAC        : simpset -> thm list -> tactic
142  val SPOSE_NOT_THEN : (thm -> tactic) -> tactic
143  val spose_not_then : (thm -> tactic) -> tactic
144  val by             : term quotation * tactic -> tactic   (* infix *)
145  val suffices_by    : term quotation * tactic -> tactic   (* infix *)
146  val sg             : term quotation -> tactic
147  val subgoal        : term quotation -> tactic
148  val cheat          : tactic
149  val kall_tac       : 'a -> tactic
150
151  (* Abbreviations  (see also Q structure) *)
152
153  val Abbr             : term quotation -> thm
154  val UNABBREV_ALL_TAC : tactic
155  val REABBREV_TAC     : tactic
156  val WITHOUT_ABBREVS  : tactic -> tactic
157
158  (* name cases of an induction theorem *)
159  val name_ind_cases : term list -> thm -> thm
160
161  (* more simplification variants *)
162  val fsrw_tac : simpLib.ssfrag list -> thm list -> tactic
163  val simp : thm list -> tactic
164  val csimp : thm list -> tactic
165  val dsimp : thm list -> tactic
166  val lrw : thm list -> tactic
167  val lfs : thm list -> tactic
168  val lrfs : thm list -> tactic
169  val rw : thm list -> tactic
170  val fs : thm list -> tactic
171  val rfs : thm list -> tactic
172  val gs : thm list -> tactic
173  val gvs : thm list -> tactic
174  val gns : thm list -> tactic
175  val gnvs : thm list -> tactic
176
177  (* without loss of generality (from wlogLib) *)
178  val wlog_then : term quotation ->
179                  term quotation list -> thm_tactic -> tactic
180  val wlog_tac : term quotation -> term quotation list -> tactic
181
182  (* useful quotation-based tactics (from Q) *)
183  val qx_gen_tac : term quotation -> tactic
184  val qx_genl_tac : term quotation list -> tactic
185  val qx_choose_then : term quotation -> thm_tactic -> thm_tactic
186  val qx_choosel_then : term quotation list -> thm_tactic -> thm_tactic
187  val qexists_tac : term quotation -> tactic
188  val qexistsl_tac : term quotation list -> tactic
189  val qsuff_tac : term quotation -> tactic
190  val qid_spec_tac : term quotation -> tactic
191  val qspec_tac : term quotation * term quotation -> tactic
192  val qspec_then : term quotation -> thm_tactic -> thm -> tactic
193  val qspecl_then : term quotation list -> thm_tactic -> thm -> tactic
194  val qhdtm_assum : term quotation -> thm_tactic -> tactic
195  val qhdtm_x_assum : term quotation -> thm_tactic -> tactic
196  val qpat_assum : term quotation -> thm_tactic -> tactic
197  val qpat_x_assum : term quotation -> thm_tactic -> tactic
198  val qpat_abbrev_tac : term quotation -> tactic
199  val qmatch_abbrev_tac : term quotation -> tactic
200  val qho_match_abbrev_tac : term quotation -> tactic
201  val qmatch_rename_tac : term quotation -> tactic
202  val qmatch_assum_abbrev_tac : term quotation -> tactic
203  val qmatch_assum_rename_tac : term quotation -> tactic
204  val qmatch_asmsub_rename_tac : term quotation -> tactic
205  val qmatch_goalsub_rename_tac : term quotation -> tactic
206  val qmatch_asmsub_abbrev_tac : term quotation -> tactic
207  val qmatch_goalsub_abbrev_tac : term quotation -> tactic
208  val rename1 : term quotation -> tactic
209  val rename : term quotation list -> tactic
210  val qabbrev_tac : term quotation -> tactic
211  val qunabbrev_tac : term quotation -> tactic
212  val qunabbrevl_tac : term quotation list -> tactic
213  val unabbrev_all_tac : tactic
214
215  (* Derived search functions *)
216  val find_consts_thy : string list -> hol_type -> term list
217  val find_consts : hol_type -> term list
218end
219