1signature intSyntax =
2sig
3  include Abbrev
4
5  (* terms and types *)
6  val int_ty         : hol_type
7  val zero_tm        : term
8  val one_tm         : term
9  val negate_tm      : term
10  val absval_tm      : term
11  val plus_tm        : term
12  val minus_tm       : term
13  val mult_tm        : term
14  val div_tm         : term
15  val mod_tm         : term
16  val quot_tm        : term
17  val rem_tm         : term
18  val exp_tm         : term
19  val int_eq_tm      : term
20  val less_tm        : term
21  val leq_tm         : term
22  val great_tm       : term
23  val geq_tm         : term
24  val divides_tm     : term
25  val min_tm         : term
26  val max_tm         : term
27  val LEAST_INT_tm   : term
28  val Num_tm         : term (* the coercion from :int -> :num *)
29  val int_injection  : term (* the injection from :num -> :int *)
30
31  (* discriminators, constructors, etc *)
32
33  val is_int_literal : term -> bool
34  val int_of_term    : term -> Arbint.int
35  val term_of_int    : Arbint.int -> term
36
37  val mk_injected    : term -> term
38  val dest_injected  : term -> term
39  val is_injected    : term -> bool
40
41  val mk_Num         : term -> term
42  val dest_Num       : term -> term
43  val is_Num         : term -> bool
44
45  val is_negated     : term -> bool  (* if a term is of form ~ e *)
46  val mk_negated     : term -> term
47  val dest_negated   : term -> term
48
49  val is_plus        : term -> bool
50  val mk_plus        : (term * term) -> term
51  val dest_plus      : term -> (term * term)
52  val list_mk_plus   : (* non-empty *) term list -> term
53  val strip_plus     : term -> term list
54
55  val is_minus       : term -> bool
56  val dest_minus     : term -> (term * term)
57  val mk_minus       : (term * term) -> term
58
59  val is_mult        : term -> bool
60  val mk_mult        : (term * term) -> term
61  val dest_mult      : term -> (term * term)
62  val list_mk_mult   : (* non-empty *) term list -> term
63  val strip_mult     : term -> term list
64
65  val is_exp         : term -> bool
66  val mk_exp         : (term * term) -> term
67  val dest_exp       : term -> (term * term)
68
69  val is_div         : term -> bool
70  val dest_div       : term -> (term * term)
71  val mk_div         : (term * term) -> term
72
73  val is_mod         : term -> bool
74  val dest_mod       : term -> (term * term)
75  val mk_mod         : (term * term) -> term
76
77  val is_quot        : term -> bool
78  val dest_quot      : term -> (term * term)
79  val mk_quot        : (term * term) -> term
80
81  val is_rem         : term -> bool
82  val dest_rem       : term -> (term * term)
83  val mk_rem         : (term * term) -> term
84
85  val is_absval      : term -> bool
86  val mk_absval      : term -> term
87  val dest_absval    : term -> term
88
89  val is_less        : term -> bool
90  val dest_less      : term -> (term * term)
91  val mk_less        : (term * term) -> term
92
93  val is_leq         : term -> bool
94  val dest_leq       : term -> (term * term)
95  val mk_leq         : (term * term) -> term
96
97  val is_great       : term -> bool
98  val dest_great     : term -> (term * term)
99  val mk_great       : (term * term) -> term
100
101  val is_geq         : term -> bool
102  val dest_geq       : term -> (term * term)
103  val mk_geq         : (term * term) -> term
104
105  val is_divides     : term -> bool
106  val dest_divides   : term -> (term * term)
107  val mk_divides     : (term * term) -> term
108
109  val is_min         : term -> bool
110  val dest_min       : term -> (term * term)
111  val mk_min         : (term * term) -> term
112
113  val is_max         : term -> bool
114  val dest_max       : term -> (term * term)
115  val mk_max         : (term * term) -> term
116
117  val is_LEAST_INT   : term -> bool
118  val dest_LEAST_INT : term -> term
119  val mk_LEAST_INT   : term -> term
120
121end
122