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