1(* ===================================================================== *)
2(* FILE          : numLib.sig                                            *)
3(* DESCRIPTION   : useful proof support for :num.                        *)
4(*                                                                       *)
5(* ===================================================================== *)
6
7
8signature numLib =
9sig
10 include numSyntax
11
12 val EXISTS_LEAST_CONV        : conv
13 val EXISTS_GREATEST_CONV     : conv
14 val SUC_ELIM_CONV            : conv
15 val SUC_TO_NUMERAL_DEFN_CONV : conv
16 val num_CONV                 : conv
17
18 val SUC_RULE                 : rule
19
20 val INDUCT_TAC               : tactic
21 val completeInduct_on        : term quotation -> tactic
22 val measureInduct_on         : term quotation -> tactic
23
24 val LEAST_ELIM_TAC           : tactic
25
26 val REDUCE_CONV              : conv
27 val REDUCE_RULE              : thm -> thm
28 val REDUCE_TAC               : tactic
29
30 val ARITH_CONV               : conv
31 val ARITH_PROVE              : conv
32 val ARITH_TAC                : tactic
33
34 val BOUNDED_FORALL_CONV      : conv -> conv
35 val BOUNDED_EXISTS_CONV      : conv -> conv
36
37 val std_ss                   : simpLib.simpset
38 val arith_ss                 : simpLib.simpset
39
40 val DECIDE                   : conv
41 val DECIDE_TAC               : tactic
42
43 val prefer_num               : unit -> unit
44 val deprecate_num            : unit -> unit
45end
46