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 -> 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 Induct            : tactic
36  val recInduct         : thm -> tactic
37  val Cases_on          : term quotation -> tactic
38  val Induct_on         : term quotation -> tactic
39  val PairCases_on      : term quotation -> tactic
40  val measureInduct_on  : term quotation -> tactic
41  val completeInduct_on : term quotation -> tactic
42  val CASE_TAC          : tactic
43  val pairarg_tac       : tactic
44  val split_pair_case_tac : tactic
45  val CaseEq            : string -> thm
46  val CaseEqs           : string list -> thm
47  val AllCaseEqs        : unit -> thm
48
49  (* Proof automation *)
50
51  val PROVE          : thm list -> term -> thm   (* First order *)
52  val METIS_PROVE    : thm list -> term -> thm   (* First order *)
53  val DECIDE         : term -> thm               (* Cooperating dec. procs *)
54  val PROVE_TAC      : thm list -> tactic
55  val prove_tac      : thm list -> tactic
56  val METIS_TAC      : thm list -> tactic
57  val metis_tac      : thm list -> tactic
58  val DECIDE_TAC     : tactic
59  val decide_tac     : tactic
60
61  (* Simplification *)
62
63  val ++              : simpset * ssfrag -> simpset    (* infix *)
64  val &&              : simpset * thm list -> simpset  (* infix *)
65  val pure_ss         : simpset
66  val bool_ss         : simpset
67  val std_ss          : simpset           (* bool + option + pair + sum *)
68  val arith_ss        : simpset
69  val old_arith_ss    : simpset
70  val list_ss         : simpset
71  val srw_ss          : unit -> simpset
72  val QI_ss           : ssfrag
73  val SQI_ss          : ssfrag
74  val ARITH_ss        : ssfrag            (* arithmetic d.p. + some rewrites *)
75  val old_ARITH_ss    : ssfrag
76  val type_rws        : hol_type -> thm list
77  val rewrites        : thm list -> ssfrag
78  val augment_srw_ss  : ssfrag list -> unit
79  val diminish_srw_ss : string list -> ssfrag list
80  val export_rewrites : string list -> unit
81  val limit           : int -> simpset -> simpset
82
83  (* use these in simplifier's argument list *)
84  val SimpLHS        : thm
85  val SimpRHS        : thm
86  val SimpL          : term -> thm
87  val SimpR          : term -> thm
88
89  val Cong           : thm -> thm
90  val AC             : thm -> thm -> thm
91
92  val SIMP_CONV         : simpset -> thm list -> conv
93  val SIMP_RULE         : simpset -> thm list -> thm -> thm
94  val SIMP_TAC          : simpset -> thm list -> tactic
95  val simp_tac          : simpset -> thm list -> tactic
96  val ASM_SIMP_TAC      : simpset -> thm list -> tactic
97  val asm_simp_tac      : simpset -> thm list -> tactic
98  val FULL_SIMP_TAC     : simpset -> thm list -> tactic
99  val full_simp_tac     : simpset -> thm list -> tactic
100  val REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
101  val rev_full_simp_tac : simpset -> thm list -> tactic
102  val RW_TAC            : simpset -> thm list -> tactic
103  val rw_tac            : simpset -> thm list -> tactic
104  val SRW_TAC           : ssfrag list -> thm list -> tactic
105  val srw_tac           : ssfrag list -> thm list -> tactic
106
107  val NO_STRIP_FULL_SIMP_TAC     : simpset -> thm list -> tactic
108  val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
109
110  val QI_TAC     : tactic
111  val ASM_QI_TAC : tactic
112  val GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic
113
114  (* Call-by-value evaluation *)
115  val EVAL           : conv
116  val EVAL_RULE      : thm -> thm
117  val EVAL_TAC       : tactic
118
119  (* Miscellaneous *)
120
121  val ZAP_TAC        : simpset -> thm list -> tactic
122  val SPOSE_NOT_THEN : (thm -> tactic) -> tactic
123  val spose_not_then : (thm -> tactic) -> tactic
124  val by             : term quotation * tactic -> tactic   (* infix *)
125  val suffices_by    : term quotation * tactic -> tactic   (* infix *)
126  val sg             : term quotation -> tactic
127  val subgoal        : term quotation -> tactic
128  val cheat          : tactic
129  val kall_tac       : 'a -> tactic
130
131  (* Abbreviations  (see also Q structure) *)
132
133  val Abbr             : term quotation -> thm
134  val UNABBREV_ALL_TAC : tactic
135  val REABBREV_TAC     : tactic
136  val WITHOUT_ABBREVS  : tactic -> tactic
137
138  (* more simplification variants *)
139  val fsrw_tac : simpLib.ssfrag list -> thm list -> tactic
140  val simp : thm list -> tactic
141  val csimp : thm list -> tactic
142  val dsimp : thm list -> tactic
143  val lrw : thm list -> tactic
144  val lfs : thm list -> tactic
145  val lrfs : thm list -> tactic
146  val rw : thm list -> tactic
147  val fs : thm list -> tactic
148  val rfs : thm list -> tactic
149
150  (* without loss of generality (from wlogLib) *)
151  val wlog_then : term quotation ->
152                  term quotation list -> thm_tactic -> tactic
153  val wlog_tac : term quotation -> term quotation list -> tactic
154
155  (* useful quotation-based tactics (from Q) *)
156  val qx_gen_tac : term quotation -> tactic
157  val qx_choose_then : term quotation -> thm_tactic -> thm_tactic
158  val qexists_tac : term quotation -> tactic
159  val qsuff_tac : term quotation -> tactic
160  val qid_spec_tac : term quotation -> tactic
161  val qspec_tac : term quotation * term quotation -> tactic
162  val qspec_then : term quotation -> thm_tactic -> thm -> tactic
163  val qspecl_then : term quotation list -> thm_tactic -> thm -> tactic
164  val qhdtm_assum : term quotation -> thm_tactic -> tactic
165  val qhdtm_x_assum : term quotation -> thm_tactic -> tactic
166  val qpat_assum : term quotation -> thm_tactic -> tactic
167  val qpat_x_assum : term quotation -> thm_tactic -> tactic
168  val qpat_abbrev_tac : term quotation -> tactic
169  val qmatch_abbrev_tac : term quotation -> tactic
170  val qho_match_abbrev_tac : term quotation -> tactic
171  val qmatch_rename_tac : term quotation -> tactic
172  val qmatch_assum_abbrev_tac : term quotation -> tactic
173  val qmatch_assum_rename_tac : term quotation -> tactic
174  val qmatch_asmsub_rename_tac : term quotation -> tactic
175  val qmatch_goalsub_rename_tac : term quotation -> tactic
176  val qmatch_asmsub_abbrev_tac : term quotation -> tactic
177  val qmatch_goalsub_abbrev_tac : term quotation -> tactic
178  val rename1 : term quotation -> tactic
179  val rename : term quotation list -> tactic
180  val qabbrev_tac : term quotation -> tactic
181  val qunabbrev_tac : term quotation -> tactic
182  val unabbrev_all_tac : tactic
183  val qx_genl_tac : term quotation list -> tactic
184  val qx_choosel_then : term quotation list -> thm_tactic -> thm_tactic
185
186end
187