1signature formalizeUseful =
2sig
3
4  (* GENERAL *)
5
6  type 'a thunk = unit -> 'a
7  type 'a susp = 'a Susp.susp
8  type ppstream = Portable.ppstream
9  type ('a, 'b) maplet = {redex : 'a, residue : 'b}
10  type ('a, 'b) subst = ('a, 'b) Lib.subst
11
12  (* Error handling *)
13  val ERR : string -> string -> exn
14  val BUG : string -> string -> exn
15  val BUG_to_string : exn -> string
16  val err_BUG : string -> exn -> exn
17
18  (* Success and failure *)
19  val assert : bool -> exn -> unit
20  val try : ('a -> 'b) -> 'a -> 'b
21  val total : ('a -> 'b) -> 'a -> 'b option
22  val can : ('a -> 'b) -> 'a -> bool
23  val partial : exn -> ('a -> 'b option) -> 'a -> 'b
24
25  (* Exception combinators *)
26  val nof : 'a -> 'b
27  val allf : 'a -> 'a
28  val thenf : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
29  val orelsef : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
30  val tryf : ('a -> 'a) -> 'a -> 'a
31  val repeatf : ('a -> 'a) -> 'a -> 'a
32  val repeatplusf : ('a -> 'a) -> 'a -> 'a
33  val firstf : ('a -> 'b) list -> 'a -> 'b
34
35  (* Combinators *)
36  val A : ('a -> 'b) -> 'a -> 'b
37  val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
38  val I : 'a -> 'a
39  val K : 'a -> 'b -> 'a
40  val N : int -> ('a -> 'a) -> 'a -> 'a
41  val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
42  val W : ('a -> 'a -> 'b) -> 'a -> 'b
43  val oo : ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
44
45  (* Pairs *)
46  val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
47  val D : 'a -> 'a * 'a
48  val Df : ('a -> 'b) -> ('a * 'a -> 'b * 'b)
49  val fst : 'a * 'b -> 'a
50  val snd : 'a * 'b -> 'b
51  val add_fst : 'a -> 'b -> 'a * 'b
52  val add_snd : 'a -> 'b -> 'b * 'a
53  val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
54  val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
55  val equal : ''a -> ''a -> bool
56  val pair_to_string : ('a -> string) -> ('b -> string) -> 'a * 'b -> string
57
58  (* Integers *)
59  val plus : int -> int -> int
60  val multiply : int -> int -> int
61  val succ : int -> int
62
63  (* Strings *)
64  val concat : string -> string -> string
65  val int_to_string : int -> string
66  val string_to_int : string -> int
67  val mk_string_fn : string -> string list -> string
68  val dest_string_fn : string -> string -> string list
69  val is_string_fn : string -> string -> bool
70
71  (* Debugging *)
72  val time_n : int -> ('a -> 'b) -> 'a -> unit
73  val tt : ('a -> 'b) -> 'a -> 'b
74  val tt2 : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
75  val tt3 : ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
76  val tt4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
77  val ff : ('a -> 'b) -> 'a -> unit
78  val ff2 : ('a -> 'b -> 'c) -> 'a -> 'b -> unit
79  val ff3 : ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> unit
80  val ff4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> unit
81
82  (* Useful imperative features *)
83  val new_int : unit -> int
84  val random_generator : Random.generator
85  val random_integer : int -> int
86  val random_real : unit -> real
87  val pair_susp : 'a susp -> 'b susp -> ('a * 'b) susp
88  val susp_map : ('a -> 'b) -> 'a susp -> 'b susp
89
90  (* Options *)
91  val is_some : 'a option -> bool
92  val grab : 'a option -> 'a
93  val o_pair : 'a option * 'b -> ('a * 'b) option
94  val pair_o : 'a * 'b option -> ('a * 'b) option
95  val o_pair_o : 'a option * 'b option -> ('a * 'b) option
96  val app_o : ('a -> 'b) -> 'a option -> 'b option
97  val o_app : ('a -> 'b) option -> 'a -> 'b option
98  val o_app_o : ('a -> 'b) option -> 'a option -> 'b option
99  val partial_app_o : ('a -> 'b option) -> 'a option -> 'b option
100  val partial_o_app : ('a -> 'b option) option -> 'a -> 'b option
101  val partial_o_app_o : ('a -> 'b option) option -> 'a option -> 'b option
102  val option_to_list : 'a option -> 'a list
103
104  (* Lists *)
105  val cons : 'a -> 'a list -> 'a list
106  val append : 'a list -> 'a list -> 'a list
107  val wrap : 'a -> 'a list
108  val unwrap : 'a list -> 'a
109  val fold : ('a -> 'b -> 'b) -> 'b -> 'a list -> 'b
110  val trans : ('a -> 'b -> 'b) -> 'b -> 'a list -> 'b
111  val partial_trans : ('a -> 'b -> 'b option) -> 'b -> 'a list -> 'b option
112  val first : ('a -> bool) -> 'a list -> 'a
113  val partial_first : ('a -> 'b option) -> 'a list -> 'b option
114  val forall : ('a -> bool) -> 'a list -> bool
115  val exists : ('a -> bool) -> 'a list -> bool
116  val index : ('a -> bool) -> 'a list -> int
117  val nth : int -> 'a list -> 'a
118  val split_after : int -> 'a list -> 'a list * 'a list
119  val assoc : ''a -> (''a * 'b) list -> 'b
120  val rev_assoc : ''a -> ('b * ''a) list -> 'b
121  val map : ('a -> 'b) -> 'a list -> 'b list
122  val partial_map : ('a -> 'b option) -> 'a list -> 'b list
123  val zip : 'a list -> 'b list -> ('a * 'b) list
124  val zipwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
125  val partial_zipwith : ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
126  val cart : 'a list -> 'b list -> ('a * 'b) list
127  val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
128  val partial_cartwith :
129    ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
130  val list_to_string : ('a -> string) -> 'a list -> string
131
132  (* Lists as sets *)
133  val subset : ''a list -> ''a list -> bool
134  val distinct : ''a list -> bool
135  val union2 : ''a list * ''b list -> ''a list * ''b list -> ''a list * ''b list
136
137  (* Permutations and sorting (order functions should always be <=) *)
138  val rotations : 'a list -> ('a * 'a list) list
139  val rotate : int -> ('a list -> 'a * 'a list)
140  val rotate_random : 'a list -> 'a * 'a list
141  val permutations : 'a list -> 'a list list
142  val permute : int list -> 'a list -> 'a list
143  val permute_random : 'a list -> 'a list
144  val min : ('a -> 'a -> bool) -> 'a list -> 'a
145  val merge : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
146  val sort : ('a -> 'a -> bool) -> 'a list -> 'a list
147  val top_min : ('a -> 'a -> bool option) -> 'a list -> 'a * 'a list
148  val top_sort : ('a -> 'a -> bool option) -> 'a list -> 'a list
149
150  (* Sums *)
151  datatype ('a, 'b) sum = LEFT of 'a | RIGHT of 'b
152
153  (* Streams *)
154  datatype ('a) stream = STREAM_NIL | STREAM_CONS of ('a * 'a stream thunk)
155  val stream_null : 'a stream -> bool
156  val dest_stream_cons : 'a stream -> 'a * 'a stream thunk
157  val stream_hd : 'a stream -> 'a
158  val stream_tl : 'a stream -> 'a stream thunk
159  val stream_to_list : 'a stream -> 'a list
160  val stream_append : 'a stream thunk -> 'a stream thunk -> 'a stream thunk
161  val stream_concat : 'a stream thunk list -> 'a stream thunk
162
163  (* Trees *)
164  datatype ('a, 'b) tree = BRANCH of 'a * ('a, 'b) tree list | LEAF of 'b
165  val tree_size : ('a, 'b) tree -> int
166  val tree_fold : ('a -> 'b list -> 'b) -> ('c -> 'b) -> ('a, 'c) tree -> 'b
167  val tree_trans :
168    ('a -> 'b -> 'b) -> ('c -> 'b -> 'd) -> 'b -> ('a, 'c) tree -> 'd list
169  val tree_partial_trans :
170    ('a -> 'b -> 'b option) -> ('c -> 'b -> 'd option) -> 'b ->
171    ('a, 'c) tree -> 'd list
172
173  (* Pretty-printing *)
174  val pp_map :
175    ('a -> 'b) -> (ppstream -> 'b -> unit) -> ppstream -> 'a -> unit
176  val pp_string : ppstream -> string -> unit
177  val pp_unknown : ppstream -> 'a -> unit
178  val pp_int : ppstream -> int -> unit
179  val pp_pair :
180    (ppstream -> 'a -> unit) -> (ppstream -> 'b -> unit) ->
181    (ppstream -> 'a * 'b -> unit)
182  val pp_list : (ppstream -> 'a -> unit) -> (ppstream -> 'a list -> unit)
183
184  (* Substitutions *)
185  val redex : ('a, 'b) maplet -> 'a
186  val residue : ('a, 'b) maplet -> 'b
187  val maplet_map : ('a -> 'c) * ('b -> 'd) -> ('a, 'b) maplet -> ('c, 'd) maplet
188  val find_redex : ''a -> (''a, 'b) subst -> (''a, 'b) maplet
189  val clean_subst : (''a, ''a) subst -> (''a, ''a) subst
190  val subst_vars : ('a, 'b) subst -> 'a list
191  val subst_map : ('a -> 'c) * ('b -> 'd) -> ('a, 'b) subst -> ('c, 'd) subst
192  val redex_map : ('a -> 'c) -> ('a, 'b) subst -> ('c, 'b) subst
193  val residue_map : ('b -> 'c) -> ('a, 'b) subst -> ('a, 'c) subst
194  val is_renaming_subst : ''b list -> ('a, ''b) subst -> bool
195  val invert_renaming_subst : ''b list -> ('a, ''b) subst -> (''b, 'a) subst
196
197  (* HOL *)
198
199  type hol_type = Type.hol_type
200  type term = Term.term
201  type thm = Thm.thm
202  type goal = term list * term
203  type conv = term -> thm
204  type rule = thm -> thm
205  type validation = thm list -> thm
206  type tactic = goal -> goal list * validation
207  type thm_tactic = thm -> tactic
208  type thm_tactical = thm_tactic -> thm_tactic
209  type vars = term list * hol_type list
210  type vterm = vars * term
211  type vthm = vars * thm
212  type type_subst = (hol_type, hol_type) subst
213  type term_subst = (term, term) subst
214  type substitution = term_subst * type_subst
215  type ho_substitution = substitution * thm thunk
216  type raw_substitution = term_subst * (type_subst * hol_type list)
217  type ho_raw_substitution = raw_substitution * thm thunk
218
219  (* General *)
220  val profile : ('a -> 'b) -> 'a -> 'b
221  val parse_with_goal : term frag list -> goal -> term
222  val PARSE_TAC : (term -> tactic) -> term frag list -> tactic
223
224  (* Term/type substitutions *)
225  val empty_subst : substitution
226  val type_inst : type_subst -> hol_type -> hol_type
227  val inst_ty : type_subst -> term -> term
228  val pinst : substitution -> term -> term
229  val type_subst_vars_in_set : type_subst -> hol_type list -> bool
230  val subst_vars_in_set : substitution -> vars -> bool
231  val type_refine_subst : type_subst -> type_subst -> type_subst
232  val refine_subst : substitution -> substitution -> substitution
233  val type_vars_after_subst : hol_type list -> type_subst -> hol_type list
234  val vars_after_subst : vars -> substitution -> vars
235  val type_invert_subst : hol_type list -> type_subst -> type_subst
236  val invert_subst : vars -> substitution -> substitution
237
238  (* Logic variables *)
239  val empty_vars : vars
240  val is_tyvar : vars -> hol_type -> bool
241  val is_tmvar : vars -> term -> bool
242  val type_new_vars : hol_type list -> hol_type list * (type_subst * type_subst)
243  val term_new_vars : term list -> term list * (term_subst * term_subst)
244  val new_vars : vars -> vars * (substitution * substitution)
245
246  (* Bound variables *)
247  val dest_bv : term list -> term -> int
248  val is_bv : term list -> term -> bool
249  val mk_bv : term list -> int -> term
250
251  (* Types *)
252
253  (* Terms *)
254  val type_vars_in_terms : term list -> hol_type list
255  val list_dest_comb : term -> term * term list
256  val conjuncts : term -> term list
257  val dest_unaryop : string -> term -> term
258  val is_unaryop : string -> (term -> bool)
259  val dest_binop : string -> term -> term * term
260  val is_binop : string -> (term -> bool)
261  val dest_imp : term -> term * term
262  val is_imp : term -> bool
263  val dest_foralls : term -> term list * term
264  val mk_foralls : term list * term -> term
265  val spec : term -> term -> term
266  val specl : term list -> term -> term
267  val var_match : vars -> term -> term -> substitution
268
269  (* Theorems *)
270  val FUN_EQ : thm
271  val SET_EQ : thm
272  val hyps : thm list -> term list
273  val LHS : thm -> term
274  val RHS : thm -> term
275  val INST_TY : type_subst -> thm -> thm
276  val PINST : substitution -> thm -> thm
277
278  (* Conversions *)
279  val FIRSTC : conv list -> conv
280  val TRYC : conv -> conv
281  val REPEATPLUSC : conv -> conv
282  val REPEATC_CUTOFF : int -> conv -> conv
283  val DEPTH_ONCE_CONV : conv -> conv
284  val FORALLS_CONV : conv -> conv
285  val CONJUNCT_CONV : conv -> conv
286  val EXACT_CONV : term -> conv
287  val NEGNEG_CONV : conv
288  val FUN_EQ_CONV : conv
289  val SET_EQ_CONV : conv
290  val N_BETA_CONV : int -> conv
291  val EQ_NEG_BOOL_CONV : conv
292  val GENVAR_ALPHA_CONV : conv
293  val GENVAR_BVARS_CONV : conv
294  val ETA_EXPAND_CONV : term -> conv
295  val GENVAR_ETA_EXPAND_CONV : conv
296
297  (* Rules *)
298  val THENR : rule * rule -> rule
299  val REPEATR : rule -> rule
300  val ORELSER : rule * rule -> rule
301  val TRYR : rule -> rule
302  val ALL_RULE : rule
303  val EVERYR : rule list -> rule
304  val FORALL_IMP : rule
305  val EQ_BOOL_INTRO : rule
306  val GENVAR_BVARS : rule
307  val GENVAR_SPEC : rule
308  val GENVAR_SPEC_ALL : rule
309  val REV_CONJUNCTS : thm list -> thm
310  val REORDER_ASMS : term list -> rule
311  val NEW_CONST_RULE : term -> rule
312  val GENVAR_CONST_RULE : rule
313  val ZAP_CONSTS_RULE : rule
314
315  (* Variable theorem (vthm) operations *)
316  val thm_to_vthm : thm -> vthm
317  val vthm_to_thm : vthm -> thm
318  val clean_vthm : vthm -> vthm
319  val var_GENVAR_SPEC : vthm -> vthm
320  val var_CONJUNCTS : vthm -> vthm list
321  val var_MATCH_MP : thm -> vthm -> vthm
322
323  (* Discharging assumptions onto the lhs of an implication *)
324  val DISCH_CONJ_CONV : conv
325  val DISCH_CONJ : term -> rule
326  val DISCH_CONJUNCTS : term list -> rule
327  val DISCH_CONJUNCTS_ALL : rule
328  val DISCH_CONJUNCTS_FILTER : (term -> bool) -> rule
329  val DISCH_CONJ_TAC : tactic
330  val DISCH_CONJUNCTS_TAC : tactic
331  val UNDISCH_CONJ_CONV : conv
332  val UNDISCH_CONJ : rule
333  val UNDISCH_CONJUNCTS : rule
334  val UNDISCH_CONJ_TAC : term -> tactic
335  val UNDISCH_CONJUNCTS_TAC : tactic
336
337  (* Tactics *)
338  val PURE_CONV_TAC : conv -> tactic
339  val ASMLIST_CASES : tactic -> (term -> tactic) -> tactic
340  val POP_ASSUM_TAC : tactic -> tactic
341  val THEN1 : tactic * tactic -> tactic
342  val REVERSE : tactic -> tactic
343  val TRUTH_TAC : tactic
344  val K_TAC : 'a -> tactic
345  val KILL_TAC : tactic
346  val CONJUNCTS_TAC : tactic
347  val FUN_EQ_TAC : tactic
348  val SET_EQ_TAC : tactic
349  val SUFF_TAC : term -> tactic
350  val KNOW_TAC : term -> tactic
351  val CHECK_ASMS_TAC : tactic
352  val EXACT_MP_TAC : thm_tactic
353  val STRONG_CONJ_TAC : tactic
354  val FORWARD_TAC : (thm list -> thm list) -> tactic
355
356  (* Simple CNF conversion *)
357  val CNF_CONV : conv
358  val CNF_RULE : rule
359  val CNF_EXPAND : thm -> thm list
360  val CNF_TAC : tactic
361
362  (* ASM_MATCH_MP_TAC *)
363  val MATCH_MP_DEPTH : int -> thm list -> thm list -> thm list
364  val ASM_MATCH_MP_TAC_N : int -> thm list -> tactic
365  val ASM_MATCH_MP_TAC : thm list -> tactic
366
367end
368