1signature boolSyntax =
2sig
3  type thm      = Thm.thm
4  type term     = Term.term
5  type hol_type = Type.hol_type
6
7
8  (* Constants *)
9
10  val equality       : term
11  val implication    : term
12  val select         : term
13  val T              : term
14  val F              : term
15  val universal      : term
16  val existential    : term
17  val exists1        : term
18  val conjunction    : term
19  val disjunction    : term
20  val negation       : term
21  val conditional    : term
22  val bool_case      : term
23  val literal_case   : term
24  val let_tm         : term
25  val arb            : term
26  val the_value      : term
27  val bounded_tm     : term
28  val IN_tm          : term
29  val res_forall_tm  : term
30  val res_exists_tm  : term
31  val res_exists1_tm : term
32  val res_select_tm  : term
33  val res_abstract_tm: term
34
35  (* Construction routines *)
36
37  val mk_eq                  : term * term -> term
38  val mk_imp                 : term * term -> term
39  val mk_select              : term * term -> term
40  val mk_forall              : term * term -> term
41  val mk_exists              : term * term -> term
42  val mk_exists1             : term * term -> term
43  val mk_conj                : term * term -> term
44  val mk_disj                : term * term -> term
45  val mk_neg                 : term -> term
46  val mk_let                 : term * term -> term
47  val mk_cond                : term * term * term -> term
48  val mk_bool_case           : term * term * term -> term
49  val mk_literal_case        : term * term -> term
50  val mk_arb                 : hol_type -> term
51  val mk_itself              : hol_type -> term
52  val mk_res_forall          : term * term * term -> term
53  val mk_res_exists          : term * term * term -> term
54  val mk_res_exists_unique   : term * term * term -> term
55  val mk_res_select          : term * term * term -> term
56  val mk_res_abstract        : term * term * term -> term
57  val mk_icomb               : term * term -> term
58  val mk_IN                  : term * term -> term
59
60  (* Destruction routines *)
61
62  val dest_eq                : term -> term * term
63  val dest_eq_ty             : term -> term * term * hol_type
64  val lhs                    : term -> term
65  val rhs                    : term -> term
66  val lhand                  : term -> term
67  val rand                   : term -> term
68  val rator                  : term -> term
69  val dest_imp               : term -> term * term
70  val dest_imp_only          : term -> term * term
71  val dest_select            : term -> term * term
72  val dest_forall            : term -> term * term
73  val dest_exists            : term -> term * term
74  val dest_exists1           : term -> term * term
75  val dest_conj              : term -> term * term
76  val dest_disj              : term -> term * term
77  val dest_neg               : term -> term
78  val dest_let               : term -> term * term
79  val dest_cond              : term -> term * term * term
80  val dest_bool_case         : term -> term * term * term
81  val dest_literal_case      : term -> term * term
82  val dest_arb               : term -> hol_type
83  val dest_itself            : term -> hol_type
84  val dest_res_forall        : term -> term * term * term
85  val dest_res_exists        : term -> term * term * term
86  val dest_res_exists_unique : term -> term * term * term
87  val dest_res_select        : term -> term * term * term
88  val dest_res_abstract      : term -> term * term * term
89  val dest_IN                : term -> term * term
90
91
92  (* Query routines *)
93
94  val is_eq                  : term -> bool
95  val is_imp                 : term -> bool
96  val is_imp_only            : term -> bool
97  val is_select              : term -> bool
98  val is_forall              : term -> bool
99  val is_exists              : term -> bool
100  val is_exists1             : term -> bool
101  val is_conj                : term -> bool
102  val is_disj                : term -> bool
103  val is_neg                 : term -> bool
104  val is_cond                : term -> bool
105  val is_bool_case           : term -> bool
106  val is_literal_case        : term -> bool
107  val is_let                 : term -> bool
108  val is_arb                 : term -> bool
109  val is_the_value           : term -> bool
110  val is_res_forall          : term -> bool
111  val is_res_exists          : term -> bool
112  val is_res_exists_unique   : term -> bool
113  val is_res_select          : term -> bool
114  val is_res_abstract        : term -> bool
115  val is_IN                  : term -> bool
116
117  (* Construction of a term from a list of terms *)
118
119  val list_mk_abs            : term list * term -> term
120  val list_mk_forall         : term list * term -> term
121  val list_mk_exists         : term list * term -> term
122  val list_mk_imp            : term list * term -> term
123  val list_mk_conj           : term list -> term
124  val list_mk_disj           : term list -> term
125  val list_mk_fun            : hol_type list * hol_type -> hol_type
126  val list_mk_res_forall     : (term * term) list * term -> term
127  val list_mk_res_exists     : (term * term) list * term -> term
128  val list_mk_icomb          : term * term list -> term
129
130  val gen_all                : term -> term
131
132  (* Destructing a term to a list of terms *)
133
134  val strip_comb             : term -> term * term list
135  val strip_abs              : term -> term list * term
136  val strip_imp              : term -> term list * term
137  val strip_imp_only         : term -> term list * term
138  val strip_forall           : term -> term list * term
139  val strip_exists           : term -> term list * term
140  val strip_conj             : term -> term list
141  val strip_disj             : term -> term list
142  val strip_neg              : term -> term * int
143  val strip_res_forall       : term -> (term * term) list * term
144  val strip_res_exists       : term -> (term * term) list * term
145  val strip_fun              : hol_type -> hol_type list * hol_type
146
147  val dest_strip_comb        : term -> string * term list
148
149  (* Connecting signature operations with grammar operations. *)
150
151  val new_type              : string * int -> unit
152  val new_infix_type        : {Name:string, Arity:int,
153                               ParseName:string option, Prec:int,
154                               Assoc:Parse.associativity} -> unit
155
156  val new_constant          : string * hol_type -> unit
157  val new_infix             : string * hol_type * int -> unit
158  val new_binder            : string * hol_type -> unit
159  val delete_const          : string -> unit
160  val new_type_definition   : string * thm -> thm
161  val new_infixl_definition : string * term * int -> thm
162  val new_infixr_definition : string * term * int -> thm
163  val new_binder_definition : string * term -> thm
164
165
166  (* Lifter from ML bool to HOL bool *)
167
168  val lift_bool : hol_type -> bool -> term
169
170  (* Algebraic properties *)
171
172  val comm_tm     : term
173  val assoc_tm    : term
174  val idem_tm     : term
175  val ldistrib_tm : term
176  val rdistrib_tm : term
177
178  (* sets and aconv *)
179  val ~~ : term * term -> bool
180  val !~ : term * term -> bool
181  val singt : term -> term HOLset.set
182  val listset : term list -> term HOLset.set
183  val FVs : term -> term HOLset.set
184  val FVLset : term list -> term HOLset.set
185  val ES : term HOLset.set
186
187
188end
189